The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Edsko de Vries wrote:
> Sometimes in the middle of a proof with lots of yet-to-be-decided
> meta-variables, I get strange unification errors. For example:
>
> Error: Impossible to unify "(?1871 * ?1872)%type" with "AttrType"
>
> where AttrType is defined as
>
> Definition AttrType : Set := (PreType * Attr)%type.
>
> (It would seem to me that these two types trivially unify?).

The simple explanation is that unification is of the simplest possible 
kind and doesn't take the definitional equality into account.  This 
includes not unfolding any definitions.