[Existing Class] is broken for reords (polyproj)

[JasonGross]

Set Implicit Arguments.
Set Universe Polymorphism.

Record category :=
  { ob : Type }.

Existing Class category. (*
Toplevel input, characters 0-24:
Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)

[spitters]

This seems reasonable. Just to be sure, I suppose you know that one field classes get translated to definitions.

On Thu, Feb 6, 2014 at 2:24 AM, Jason Gross notifications@github.comwrote:

Set Primitive Projections.Set Implicit Arguments.Set Universe Polymorphism. Record category := { ob : Type }. Existing Class category. (Toplevel input, characters 0-24:Anomaly: Mismatched instance and context when building universe substitution.Please report. )

Reply to this email directly or view it on GitHubhttps://github.com/HoTT/coq/issues/82 .

[JasonGross]

Indeed, I had forgotten that. But this shows up for other records, too:

Set Implicit Arguments.
Set Universe Polymorphism.

Record category :=
  { ob : Type;
    hom : ob -> ob -> Type }.

Existing Class category. (*
Toplevel input, characters 0-24:
Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)

So any classes need to be declared with Class, not Existing Class, and the Coercion variant that makes an existing method a coercion doesn't know how to deal with @ and fails on targets which are primitive projections (https://github.com/HoTT/coq/issues/81), making it impossible to have a class where one of its fields is a coercion. (I can define Coercion field' (arg : category) : @proj ... := field arg., but it's annoying, and messes with rewriting. :-( )

[mattam82]

Fixed in trunk.