The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/04/2016 11:14 AM, Igor Zhirkov wrote:
> 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 
> [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

Note that this works:

Definition my_struct : mixin_of cT :=
let x := cT in
  match x return (mixin_of x) with
  | Pack _ c => c
  end.

although that might just add to the mystery.

-- Jonathan