Fix subject reduction VS cumulative inductives and function eta

Fix #7015

3 files changed, 122 insertions, 8 deletions

diff --git a/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst b/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst
new file mode 100644
index 0000000000..1bf62de3fd
--- /dev/null
+++ b/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst
@@ -0,0 +1,5 @@
+- **Fixed:** Incompleteness of conversion checking on problems
+  involving :ref:`eta-expansion` and :ref:`cumulative universe
+  polymorphic inductive types <cumulative>` (`#12738
+  <https://github.com/coq/coq/pull/12738>`_, fixes `#7015
+  <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert).
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0754e9d4cc..7c6b869b4a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -234,6 +234,8 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
 
+exception MustExpand
+
 let get_cumulativity_constraints cv_pb variance u u' =
   match cv_pb with
   | CONV ->
@@ -251,7 +253,8 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
   | Some variances ->
     let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
     if not (Int.equal num_param_arity nargs) then
-      cmp_instances u1 u2 s
+      (* shortcut, not sure if worth doing, could use perf data *)
+      if Univ.Instance.equal u1 u2 then s else raise MustExpand
     else
       cmp_cumul cv_pb variances u1 u2 s
 
@@ -269,7 +272,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
   | Some _ ->
     let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
     if not (Int.equal num_cnstr_args nargs) then
-      cmp_instances u1 u2 s
+      if Univ.Instance.equal u1 u2 then s else raise MustExpand
     else
       (** By invariant, both constructors have a common supertype,
           so they are convertible _at that type_. *)
@@ -336,6 +339,28 @@ let is_irrelevant infos lft c =
   let env = info_env infos.cnv_inf in
   try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
 
+let identity_of_ctx (ctx:Constr.rel_context) =
+  Context.Rel.to_extended_vect mkRel 0 ctx
+
+(* ind -> fun args => ind args *)
+let eta_expand_ind env (ind,u as pind) =
+  let mib = Environ.lookup_mind (fst ind) env in
+  let mip = mib.mind_packets.(snd ind) in
+  let ctx = Vars.subst_instance_context u mip.mind_arity_ctxt in
+  let args = identity_of_ctx ctx in
+  let c = mkApp (mkIndU pind, args) in
+  let c = Term.it_mkLambda_or_LetIn c ctx in
+  inject c
+
+let eta_expand_constructor env ((ind,ctor),u as pctor) =
+  let mib = Environ.lookup_mind (fst ind) env in
+  let mip = mib.mind_packets.(snd ind) in
+  let ctx = Vars.subst_instance_context u (fst mip.mind_nf_lc.(ctor-1)) in
+  let args = identity_of_ctx ctx in
+  let c = mkApp (mkConstructU pctor, args) in
+  let c = Term.it_mkLambda_or_LetIn c ctx in
+  inject c
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
   try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -545,7 +570,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
        end
 
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
-    | (FInd (ind1,u1), FInd (ind2,u2)) ->
+    | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) ->
       if eq_ind ind1 ind2 then
         if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
@@ -556,11 +581,16 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           if not (Int.equal nargs (CClosure.stack_args_size v2))
           then raise NotConvertible
           else
-            let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in
-            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+            match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
+            | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+            | exception MustExpand ->
+              let env = info_env infos.cnv_inf in
+              let hd1 = eta_expand_ind env pind1 in
+              let hd2 = eta_expand_ind env pind2 in
+              eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
       else raise NotConvertible
 
-    | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+    | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
       if Int.equal j1 j2 && eq_ind ind1 ind2 then
         if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
@@ -571,8 +601,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           if not (Int.equal nargs (CClosure.stack_args_size v2))
           then raise NotConvertible
           else
-            let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
-            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+            match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
+            | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+            | exception MustExpand ->
+              let env = info_env infos.cnv_inf in
+              let hd1 = eta_expand_constructor env pctor1 in
+              let hd2 = eta_expand_constructor env pctor2 in
+              eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
       else raise NotConvertible
 
     (* Eta expansion of records *)
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.