Anomaly "in Univ.repr: Universe file.v.1700 undefined."

[yiyunliu]

Here's my best effort attempt at minimizing the example:

From Equations Require Import Equations.

Inductive Ki : Type :=
  | Star : Ki.

Inductive Ty : Type :=
  | VarTy : Ty
  | TyFun : Ty -> Ty.

Derive NoConfusion for Ty Ki.

Inductive TyWt : Ty -> Ki -> Type :=
| TyT_One A :
  TyWt A Star ->
  TyWt (TyFun A) Star.

Definition F : Type := True.

Inductive Wt : Ty -> Type :=
| T_App A  :
  F ->
  Wt (TyFun A) ->
  Wt A.

Lemma regularity A (h : Wt A) : TyWt A Star.
  induction h.
  inversion IHh. subst.
  apply H0.
Defined.

Fail Equations regularity' {A} (h : Wt A) : TyWt A Star :=
regularity' (T_App A _ ha)
  with regularity' ha  := { | TyT_One A h0 => h0}.

The anomaly goes away if I make one of the following modifications:

• Remove F from the T_App constructor
• Remove the VarTy constructor from the Ty inductive type
• Replace the h0 in the last line with an underscore. Equations solves the obligation automatically but the resulting definition can't be unfolded by simp.

I'm running coq-8.19.2 and coq-equations 1.3+8.19