Feature request: warn about unused section parameters

[cpitclaudel]

Description of the problem

The project that I currently work with (bedrock 2) has lots of typeclasses and parameters; most of my files start with something like this:

Section __.
  Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
  Context {locals: map.map String.string word}.
  Context {env: map.map String.string (list String.string * list String.string * Syntax.cmd)}.
  Context {ext_spec: bedrock2.Semantics.ExtSpec}.
  Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
  Context {locals_ok : map.ok locals}.
  Context {env_ok : map.ok env}.
  Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.

In practice, though, it's often the case that some of these are unnecessary — sometimes even most of them.
It would be really nice if Coq warned me about unused section variables when I closed such a section.

Test case:

Section test.
  Context {a b c: nat}.
  Definition x := a + a.
  Goal True. Proof using b. destruct (Nat.eqb b b). all: exact I. Qed.
End test.

(This should warn about c)

[SkySkimmer]

Definition ignore (x:nat) := 0.
Section S.
Variable v : nat.
Definition foo := Eval lazy in ignore v.
Check v.
End S.

should this warn unused v? (foo has type nat after closing the section) (I would say yes)

Can variables matter after the section other than through a kernel object? eg

Section S.
Variable v : nat.
Ltac foo := exact v.
End S.

tactic foo won't exist after the section, so we're fine to warn about v.

[ppedrot]

It's a bit hard to make this work with the delayed proof mechanism. The warning would only be triggered in sequential mode...

[SkySkimmer]

But delayed proofs need Proof using, so they shouldn't be a problem.

[ppedrot]

Ah, yes, indeed.