Coq: `Instance` refreshes parameter names in the global context

[RalfJung]

Version

8.9.dev

Operating system

Linux

Description of the problem

Get an interactive Coq session running with -mangle-names mangled_, and run the following script:

Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Hint Mode Inhabited ! : typeclass_instances.
Arguments populate {_} _ : assert.

Global Instance foo (A: Type): Inhabited (list A).

This results in the following goal state:

  mangled_0 : Type
  ============================
  Inhabited (list mangled_0)

That seems rather wrong, because indeed I named type A explicitly! It shouldn't get mangled.

[Zimmi48]

cc @jashug

[jashug]

Here is an example of the problem without -mangle-names:

Class Inhabited (A : Type) : Type := populate { inhabitant : A }.

Definition A := 42.

Instance foo (A: Type): Inhabited (list A).
(*
1 subgoal
A0 : Type
______________________________________(1/1)
Inhabited (list A0)
*)

Interestingly, Theorem and Lemma don't have this behavior. Instead, they properly introduce A : Type into the context, and error on Theorem (A : nat) (A : Type) : Inhabited (list A). I haven't looked at the code yet, but this seems far more sensible behavior.

So here, -mangled-names is correctly warning you that if you introduce a Definition A into the environment, your proof could break if you explicitly refer to the parameter A in the proof of your instance. That this situation is possible is a problem on Coq's side however.

[jashug]

So Classes.declare_instance_open, particularly in the non program_mode branch, uses tactics, either refine (when a partial term is given after :=) or intro without an explicit name (when no term is given), to add the parameters to the context. Theorem passes an explicit name to intro instead. (Also related #8819)