The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

You can use Georges Gonthier's trick of using phantom types to introduce extra projections so to trigger
the canonical structures unification.

Applied to your example, this gives 

Record PType : Type := mk_PType {
 Pcarrier :> Type;
 Ppoint : Pcarrier
}.

Canonical Structure Prop_ : PType := mk_PType Prop True.

(* The phantom  types *)
Inductive phant (p : Type) := Phant.

(* u and v are there to create the unification problem (Phant (Pcarrier ?)) = Prop *)
Definition Par (A B:PType) (u : phant A) (v : phant B) := mk_PType (A -> B) (fun _ => (Ppoint B)).

Notation "A --> B" := (Par _ _ (Phant B) (Phant A)) (at level 70, right associativity).

This should be 

Notation "A --> B" := (Par _ _ (Phant A) (Phant B)) (at level 70, right associativity).

V.