The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT inria.fr>]

On 09/21/2011 05:31 PM, Chad E Brown wrote:

I'm having trouble getting an easy canonical structure to work as I expect. The final Check below doesn't work.

Could someone please let me know what I'm doing wrong, or point me to an appropriate link.

Structure PType : Type := mk_PType {

 Pcarrier :> Type;

 Ppoint : Pcarrier

}.

Canonical Structure Prop_ : PType := mk_PType Prop True.

Check (fun p:PType -> Prop => p Prop).

- Thanks, Chad

The inference of canonical structure only works for projections. You can see this with the command

Print Canonical Projections.

that gives:

True <- Ppoint ( Prop_ )
Prop <- Pcarrier ( Prop_ )


This means that during the unification process, if it has True and expects and Ppoint ?,
it will be able to guess that ? is Prop_.
Only the projections (Ppoint and Pcarrier) trigger this inference.
In your example, you just ask to  unify  Prop to PType which just fails
--
Laurent