The Coq mailing list

[Carsten Varming <varming AT cmu.edu>]

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.

This is exactly the same problem as above. Adding this does the trick:

Add Parametric Morphism (T : str) : (op' _ : T -> T)
with signature ((@eqT _ : sort'' (str'_str'' (str_str' _)) -> _ -> _) ==> 
(@eqT _))%signature as eqT_opX'.
Admitted.

In

Goal forall (T : str) (a b : T), eqT _ a b -> eqT _ (op' _ (op _ a)) (op' _ 
(op _ b)).

The type of the second eqT is inferred as (str'_str'' (str_str' T)), and 
this type is not in the database.

> 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.

Carsten