Repeated imports of the same module

Stream: lean4

[Julian Berman]

Should importing the same module multiple times be something the linter catches, or even be an error?

I.e. quite simply

import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Basic

[Alex J. Best]

The style Linter probably should at the very least, I can't think of a good reason someone would do this except by accident.

[Kevin Buzzard]

Manipulation of order of instance discovery

[Niels Voss]

How often is that done? If it's rare maybe it would be better to have the linter catch this by default and have a comment to point out what the multiple import is used for when it does occur.

[James Gallicchio]

wasn't someone working on a code action to automatically remove transitively-imported files? it would hopefully also remove repeated imports like this

[Kevin Buzzard]

I think that manipulation of instance order is a pretty niche use case.

[Mario Carneiro]

ideally there would be a lint against it

[Alex J. Best]

Even if you wanted to manipulate instance discovery order would you ever need to duplicate an import? I'm not sure that would achieve anything (isn't the second time a no-op)

[Kevin Buzzard]

Just to be clear: the instance discovery post was a joke

[Mario Carneiro]

It would be nice if we could e.g. automatically sort imports alphabetically and the like. The soundness of doing so depends on there not being any same-priority conflicts by sibling files

[Alex Keizer]

Maybe such same-priority conflicts should raise an "ambiguous instance" error (at the point of use, not directly at the import, so that downstream users can mitigate the situation with retroactive attributes). It seems like a decently-sized footgun to have behaviour depend on the order of imports

[Sorawee Porncharoenwase]

FWIW, in Racket, multiple imports are intentionally supported. There could be a macro A that expands to the import of module X and Y and macro B that expands to the import of module Y and Z, and it makes sense to be able to use both macro A and B together, even though module Y is imported twice.

[Mario Carneiro]

in lean, you cannot macro expand to an import, the imports are all statically known before elaboration starts