The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Conor T McBride a écrit :

> Now, this I find a little odd. Why does this work when the other does
> not? Now the first constraint reads
>
>   V sigma = V ?a
>
> from which one cannot conclude that necessarily ?a = sigma, just that ?a
> must have a V projection coinciding with sigma's. Is this what's
> happening? Of course, ?a = sigma is a very plausible guess under the
> circumstances, even if it is not necessarily the case, so perhaps it's
> good in practice to make that choice. I'm pretty sure that Lego would
> take ?a = sigma here, although I'm not sure that I'd want it to.

At least that's what the implementor of the record layer wanted. 
Equations involving projections have this behaviour (unify the projected 
records, and in case of failure unify the projections themselves), 
altough I'm not sure the implementation is very uniform in this choice. 
This could explain that unification does not go through.

This was jusitified by Amokrane Saibi's ALGEBRA contribution, where 
algebraic structure are seen as records and the carrier set is one field 
of that record. Typically you have a record (say R_ring) stating that 
real numbers make up a ring and its carrier set is R (the set of real 
numbers). Then you often are in a situation where you have to guess a 
ring structure knowing only that its carrier is the same as that of 
R_ring. In this case you are happy that Coq infers that this is R_ring 
(you generally consider only one ring with carrier R).
In other cases that's far from obvious. For instance think of rational 
numbers, if you have to guess a rational  with the same denominator  as 
1/2, it's not clear it's 1/2...
My feeling is that Coq's behaviour is sensible only in the case of 
records with only one "important" field. Or at least such equations 
should be postponed.

Cheers,
Bruno Barras.