Skip to content

Error in "refine imports" suggestion #4771

@andreasabel

Description

@andreasabel
Image

That suggestion does not look right:

Refine imports to import Agda.Utils.List1 qualified as List2

If I remove the qualified import of List2 the List2.toList is no longer in scope.
toList is IsList method from GHC.Exts.
So the suggestion is right somehow that we would not need to import Agda.Utils.List2 if Agda.Utils.List1 already reexports IsList. However, the suggestion still does not make sense, practically.

Unfortunately no self-contained reproducer here either. :-(

Metadata

Metadata

Assignees

No one assigned

    Labels

    HackathonThis issue is suitable for hackathon sessionscomponent: imports plugintype: bugSomething isn't right: doesn't work as intended, documentation is missing/outdated, etc..

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions