Anomaly when declaring canonical structures

[peterlefanulumsdaine]

(Working over b07e5d7, i.e. current stable branch.)

Declaring certain canonical structures fails, with “Anomaly: Mismatched instance and context when building universe substitution. Please report.” The smallest example I’ve found is:

Record Type_Over (X : Type) 
:= { Domain :> Type;
     proj : Domain -> X }.

Definition Self_Over (X : Type)
  := {| Domain := X; proj := (fun x => x) |}.

Canonical Structure Self_Over. (* fails *)

If Self_Over is changed to a monomorphic definition, then the Canonical Structure declaration still fails but with a different error: “Warning: No global reference exists for projection valuefun x : _UNBOUND_REL_1 => x in instance Self_Over of proj, ignoring it.”

As best as I can conjecture, this error seems to occur just when the record has a type parameter.

[mattam82]

Fixed now.