On warning about redundant imports

[gallais]

I have pushed a commit on a separate branch to open a discussion on warning about redundant imports.

When I refactor code, I often end up with useless imports and it's a bit of a pain to pinpoint exactly the imports I should drop. I thought I'd try to track them down automatically and generate a warning. Simple enough.

The current implementation I have worked at the interface level once all the implicit and instance arguments have been resolved. This means that unlike Haskell we don't have the caveat "except perhaps to import instances" when claiming that the import is redundant! However it produces some false positives in two cases (AFAICT):

• Whenever the content of the imports is not used by definitions but simply re-exported:

module Prelude where

open import Agda.Builtin.Bool public
open import Agda.Builtin.Nat public

• Whenever the definitions are only using values re-exported by the imported module:

module UnfortunateWarning where

open import Prelude
_ : Bool
_ = 0 == 0

Is there a way to handle these issues based purely on the Interface? Otherwise I guess the solution may be to collect some extra information at scope checking time.

[andreasabel]

Thanks! I am a bit confused, because I thought you would check for unused imported symbols ("redundant imports") as in Haskell, but from the code it seems you only check for unused modules.

The scope (iInsideScope) should have all the information you need to see which symbols are exported by public.

[andreasabel]

@gallais What kind of infos do you need to progress on this issue?

[gallais]

I'm happy with the current feature. I just need to take the time to hide this functionality behind a keystroke because it's (understandably?) a bit slow.

[andreasabel]

Ok. One could also do some sort of reference counting (with two values 0 and >=1) when we look up things in the signature. Or in other works, putting a checkmark at a signature entry if it is used. Then one could complain about names being in scope but not checked in the end.

[gallais]

I've switched to a new branch after rebasing against current stable to take advantage of the caching of warnings in interfaces. I think I'm going to use the WarningMode for this.

@fredrikNordvallForsberg : shouldn't we have a list of WarningModes rather than just a single one in PragmaOptions? We would have to check that they are not self-contradictory but it'd allow to have finer control over what is reported.

[gallais]

So I got something working on https://github.com/agda/agda/tree/issue2503-useless-imports however:

• the highlighting is not preserved through reloads
• modules that are opened public are erroneously reported as useless

[fredrikNordvallForsberg]

@gallais When I introduced WarningMode I think they were all contradicting each other, but it might make sense to change it to a list going forward.

[martinescardo]

Here is feedback (originally given to @nad and @gallais by email and posted here at @nad's request).

Firstly, an interaction with @gallais revealed that to use this you have to either

(1) put {-# OPTIONS -Wuseless-imports #-} in your file, or
(2) run in the command line agda -W useless-imports yourfile.agda.

Secondly, as @gallais said first, this is very slow, and this is why it is not enabled by default. My development TypeTopology on github (with 70 agda files, 15000 lines) took about 5 hours in a standard not-fast-not-slow laptop (where it takes 50 seconds without this option).

An import that is in a module within the main module, or in a where clause, is always reported as redundant.
This is a false positive, so it is not a problem (just mildly annoying :-) ).

This, at the moment, is useful to perform a clean-up, after a refactoring. And it was useful for me in such a situation. But it is not ready for daily use. It needs better algorithms.

Lastly, agda generates a graph of module dependencies. It would be nice to be able to get a graph of definition dependencies (ignoring modules). This would allow people to write algorithms for such things without have to understand or change the Agda implementation. Moreover, such a dependency graph would be extremely useful for many other things. (For example, which definitions and lemmas does my theorem rely on?)