The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

see tolearn wrote:
> Consider theorem 'prop_eq':
>   
> > Definition prop_eq := fun p q (eq1:p=q)
> >     
>         => (match eq1 in _=qdep return p->qdep
>         with refl_equal => fun p=>p
>         end) : p->q.
>
> Then:
>   
> > Variable (x1 x2 y1 y2:nat) (eq1:x1=y1) (eq2:x2=y2) (lt1:x1<x2).
> > Check prop_eq (x1 < x2) (y1 < y2) (f_equal2 lt eq1 eq2) lt1.
> >     
> gives an error message:
> {{{
> Error: The term "f_equal2 lt eq1 eq2" has type "(x1 < x2) = (y1 < y2)"
>  while it is expected to have type "(x1 < x2) = (y1 < y2)"
> }}}
> The terms actually are identic. Am I missing something? I'm
> using CoqIde, coqtop version 8.1pl1 (Jul. 2007), Linux.
>   

The usual thing to do when you get a message like that is:
   Set Printing All.

Now, running the [Check] command again, you get this more explicit message:
   Error: The term "@f_equal2 nat nat Prop lt x1 y1 x2 y2 eq1 eq2" has type
    "@eq Prop (lt x1 x2) (lt y1 y2)" while it is expected to have type
    "@eq Type (lt x1 x2) (lt y1 y2)"

The essence of the problem is that Coq type inference isn't guaranteed 
to give "principal types."  The types of the first two arguments to 
[prop_eq] were inferred as [Type] where you want [Prop].  This alternate 
definition fixes the problem:
   Definition prop_eq := fun (p q : Prop) (eq1:p=q)
       => (match eq1 in _=qdep return p->qdep
             with refl_equal => fun p=>p
           end) : p->q.