The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

Le 14 déc. 2010 à 16:29, Carsten Varming a écrit :

> On Mon, 13 Dec 2010, Cyril Cohen wrote:
> 
>> Hi,
>> 
>> On 13/12/2010 16:04, Carsten Varming wrote:
>>> The main problem is with the type class resolution.
>>> The type of eqT in
>>> the morphism declaration is (sort T), but the resolution algorithm is
>>> looking for (sort' (str_str' T)), and it doesn't know that (sort T)
>>> and (sort' (str_str' T)) are equal.
>> 
>> Thank you for this answer.
>> 
>> I tried to adapt your fix to the complete case, and now it works in the 
>> trivial cases. However, I still have issues each time the type of the 
>> arguments does not fit exactly the one I declared for the morphism. Here 
>> is a new reduced example of my problem.
> 
> ...
> 
>> Since (sort' (str_str' T)) and sort T are convertible, why does the 
>> resolution fail ?
> 
> I don't know. You would think that evaluating types to a normal form would 
> be the right thing to do, but that not the way it is currently done.

Let's simplify even a bit more:

Require Import Relation_Definitions.

Variable A : Type.

Structure str := Str { sort :> Type }.

Structure str' := Str' { sort' :> Type }.
Canonical Structure str_str' (T : str) := Str' T.

Variable eqT : forall T : str, T -> T -> Prop.
Variable op : forall T : str', T  -> T.

Axiom eqT_op_Proper : 
  forall T : str, ((eqT T:str_str' T -> T -> Prop) ==> eqT T) (op (str_str' 
T):T -> T).


Goal forall T, exists R, Proper (eqT T ==> R) (op (str_str' T)).
intros. econstructor. (* apply (eqT_op_Proper _). fails, same with refine *)
apply (eqT_op_Proper T). (* success *)

The problem is that the unification (noted ~) fails on: (sort' (str_str' ?1)) 
~ (sort T). 
Note that in the first term we don't know what the existential ?1 is.

If we reduced these to normal form we'd get [?1 ~ let (sort) := T in sort] 
and it would succeed,
but we don't reduce terms that contain existentials like that. Instead, 
whenever we encounter 
a unification problem of the form [match c return p with .. end ~ match c' 
return p' with .. end] 
the only considered solution is [p ~ p'], [c ~ c'] and branches are pointwise 
unifiable (i.e. case
expressions are considered rigid). This is a known flaw of the (two) 
unification algorithm(s) inside
Coq.

-- Matthieu