Anomaly: Mismatched instance and context when building universe substitution.

[JasonGross]

jgross@cagnode17:~/HoTT$ cat /tmp/foobug.v
Inductive paths A (x : A) : A -> Type := idpath : paths A x x.

Notation "x = y" := (paths _ x y).

Inductive IsTrunc : nat -> Type -> Type :=
| BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
| trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.

Existing Class IsTrunc.
jgross@cagnode17:~/HoTT$ git log -n 1 --oneline
e97084f Deopacify a bit in Functor/Pointwise/Properties
jgross@cagnode17:~/HoTT$ coqc -coqlib coq -debug /tmp/foobug.v
File "/tmp/foobug.v", line 9, characters 0-23:
Anomaly: Mismatched instance and context when building universe substitution.
Please report.
frame @ file "toplevel/vernac.ml", line 420, characters 12-38
raise @ file "toplevel/vernac.ml", line 111, characters 8-56
frame @ file "toplevel/vernac.ml", line 374, characters 27-64
frame @ file "toplevel/vernac.ml", line 348, characters 11-32
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "library/states.ml", line 38, characters 4-7
raise @ file "lib/flags.ml", line 15, characters 10-17
frame @ file "lib/flags.ml", line 11, characters 14-17
raise @ file "toplevel/vernacentries.ml", line 1829, characters 12-13
frame @ file "toplevel/vernacentries.ml", line 1818, characters 4-12
frame @ file "kernel/inductive.ml", line 162, characters 6-38
frame @ file "kernel/inductive.ml", line 56, characters 4-44
raise @ file "lib/errors.ml", line 27, characters 18-39
jgross@cagnode17:~/HoTT$ cat /tmp/foobug2.v
Fixpoint IsTrunc (n : nat) (A : Type) : Type :=
  match n with
    | O => True
    | S _ => False
  end.

Existing Class IsTrunc.
jgross@cagnode17:~/HoTT$ coqc -coqlib coq -debug /tmp/foobug2.v
File "/tmp/foobug2.v", line 7, characters 0-23:
Anomaly: Mismatched instance and context when building universe substitution.
Please report.
frame @ file "toplevel/vernac.ml", line 420, characters 12-38
raise @ file "toplevel/vernac.ml", line 111, characters 8-56
frame @ file "toplevel/vernac.ml", line 374, characters 27-64
frame @ file "toplevel/vernac.ml", line 348, characters 11-32
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "library/states.ml", line 38, characters 4-7
raise @ file "lib/flags.ml", line 15, characters 10-17
frame @ file "lib/flags.ml", line 11, characters 14-17
raise @ file "toplevel/vernacentries.ml", line 1829, characters 12-13
frame @ file "toplevel/vernacentries.ml", line 1818, characters 4-12
frame @ file "kernel/typeops.ml", line 121, characters 34-58
frame @ file "kernel/environ.ml", line 255, characters 18-58
raise @ file "lib/errors.ml", line 27, characters 18-39

It only happens when I pass coqc the -coqlib argument.

[JasonGross]

Alternatively (to passing -coqlib), I can just Set Universe Polymorphism. This is still open in trunk-polyproj.