Fix subject reduction VS cumulative inductives and function eta

Fix #7015

1 files changed, 74 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_7015.v b/test-suite/bugs/closed/bug_7015.v
new file mode 100644
index 0000000000..a57fa94960
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7015.v
@@ -0,0 +1,74 @@
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Printing Universes.
+
+Module Simple.
+
+  (* in the real world foo@{i} might be [@paths@{i} nat] I guess *)
+  Inductive foo : nat -> Type :=.
+
+  (* on [refl (fun x => f x)] this computes to [refl f] *)
+  Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g.
+  Proof.
+    change (f = g) in e. destruct e;reflexivity.
+  Defined.
+
+  Section univs.
+    Universes i j.
+    Constraint i < j. (* fail instead of forcing equality *)
+
+    Definition one : (fun n => foo@{i} n) = fun n => foo@{j} n := eq_refl.
+
+    Definition two : foo@{i} = foo@{j} := eta_out _ _ one.
+
+    Definition two' : foo@{i} = foo@{j} := Eval compute in two.
+
+    Definition three := @eq_refl (foo@{i} = foo@{j}) two.
+    Definition four := Eval compute in three.
+
+    Definition five : foo@{i} = foo@{j} := eq_refl.
+  End univs.
+
+  (* inference tries and succeeds with syntactic equality which doesn't eta expand *)
+  Fail Definition infer@{i j k|i < k, j < k, k < eq.u0}
+    : foo@{i} = foo@{j} :> (nat -> Type@{k})
+    := eq_refl.
+
+End Simple.
+
+Module WithRed.
+  (** this test needs to reduce the parameter's type to work *)
+
+
+  Inductive foo@{i j} (b:bool) (x:if b return Type@{j} then Type@{i} else nat) : Type@{i} := .
+
+  (* on [refl (fun x => f x)] this computes to [refl f] *)
+  Definition eta_out {A B} (f g : forall x : A, B x) (e : (fun x => f x) = (fun x => g x)) : f = g.
+  Proof.
+    change (f = g) in e. destruct e;reflexivity.
+  Defined.
+
+  Section univs.
+    Universes i j k.
+    Constraint i < j. (* fail instead of forcing equality *)
+
+    Definition one : (fun n => foo@{i k} false n) = fun n => foo@{j k} false n := eq_refl.
+
+    Definition two : foo@{i k} false = foo@{j k} false := eta_out _ _ one.
+
+    Definition two' : foo@{i k} false = foo@{j k} false := Eval compute in two.
+
+    (* Failure of SR doesn't just mean that the type changes, sometimes
+     we lose being well-typed entirely. *)
+    Definition three := @eq_refl (foo@{i k} false = foo@{j k} false) two.
+    Definition four := Eval compute in three.
+
+    Definition five : foo@{i k} false = foo@{j k} false := eq_refl.
+  End univs.
+
+  (* inference tries and succeeds with syntactic equality which doesn't eta expand *)
+  Fail Definition infer@{i j k|i < k, j < k, k < eq.u0}
+    : foo@{i k} false = foo@{j k} false :> (nat -> Type@{k})
+    := eq_refl.
+
+End WithRed.