Use specialized function for inductive subtyping inference.

This ensures by construction that we never infer constraints outside
the variance model.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 303cd7146e..1fb3abfe41 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -45,6 +45,15 @@ Section TpLift.
 
 End TpLift.
 
+Record Tp' := { tp' : Tp }.
+
+Definition CTp := Tp.
+(* here we have to reduce a constant to infer the correct subtyping. *)
+Record Tp'' := { tp'' : CTp }.
+
+Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x.
+Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x.
+
 Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
 Proof. reflexivity. Qed.
 
@@ -108,3 +117,10 @@ Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'}
 Definition arrow_lift@{i i' j j' | i' = i, j < j'}
   : Arrow@{i j} -> Arrow@{i' j'}
   := fun x => x.
+
+Inductive Mut1 A :=
+| Base1 : Type -> Mut1 A
+| Node1 : (A -> Mut2 A) -> Mut1 A
+with Mut2 A :=
+     | Base2 : Type -> Mut2 A
+     | Node2 : Mut1 A -> Mut2 A.