The Coq mailing list

["Igor Zhirkov" <igorjirkov AT gmail.com>]

Hi all,

I was refreshing my memory on coercions lately and saw some strange behaviour of Variables declared outside sections. MWE in Coq 8.5 :

Record mixin_of (T:Type) := Mixin { bogus: nat }.

Structure pack_type: Type := Pack { type: Type ; _ : mixin_of type }.

Coercion type: pack_type >-> Sortclass.

Variable cT: pack_type.

Check cT.    (* prints cT: pack_type *)

Definition my_struct : mixin_of cT :=

  match cT return mixin_of cT with

    | Pack _ c => c

  end.

Now that gives an error:

Toplevel input, characters 92-93:

Error:

In environment

T : Type

c : mixin_of T

The term "c" has type "mixin_of T" while it is expected to have type

 "mixin_of cT".

Looks strange to me because Check cT found it.

It works however:

* if the code above is inside a section;

* if cT is added to the argument list manually;

The Coq reference manual says that using Variable keyword is equivalent to Local Parameter, but I failed to find any explanation of the Local Parameter itself. (link: https://coq.inria.fr/refman/Reference-Manual003.html#hevea_default36 ).

So, what is actually going on here and why an information about such a variable is lost sometimes?

--Igor