Closes #13278: take into account elimination constraints in small inversion.

Ideally, if equations t <= ?x were preserving subtyping that could be
simpler. Currently we need however to put a rigid universe as
constraint on the return predicate so that one branch does not force
the return sort to be lower by unification than what another branch
would have needed.

2 files changed, 22 insertions, 2 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 587fc32ecb..312bf4907f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2080,6 +2080,15 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars
         Some (sigma', p, arsign)
   with e when precatchable_exception e -> None
 
+let expected_elimination_sort env tomatchl =
+  List.fold_right (fun (_,tm) s ->
+      match tm with
+      | IsInd (_,IndType(indf,_),_) ->
+        (* Not a degenerated line, see coerce_to_indtype *)
+        let s' = Inductive.elim_sort (Inductive.lookup_mind_specif env (fst (fst (dest_ind_family indf)))) in
+        if Sorts.family_leq s s' then s else s'
+      | NotInd _ -> s) tomatchl Sorts.InType
+
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
  * type and 1 assumption for each term not _syntactically_ in an
@@ -2130,8 +2139,12 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty
     | Some rtntyp ->
       (* We extract the signature of the arity *)
       let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in
-      let sigma, newt = new_sort_variable univ_flexible sigma in
-      let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
+      (* We put a type constraint on the predicate so that one
+         branch type-checked first does not lead to a lower type than
+         another branch; we take into account the possible elimination
+         constraints on the predicate *)
+      let sigma, rtnsort = fresh_sort_in_family sigma (expected_elimination_sort !!env tomatchs) in
+      let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in
       let predccl = nf_evar sigma predcclj.uj_val in
       [sigma, predccl, building_arsign]
   in
diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v
index 44a14174cd..9831a4d205 100644
--- a/test-suite/bugs/closed/bug_13278.v
+++ b/test-suite/bugs/closed/bug_13278.v
@@ -6,3 +6,10 @@ Goal even 1 -> False.
 Proof.
   refine (fun a => match a with end).
 Qed.
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a in even n
+                   return match n with 1 => False | _ => True end : Prop
+                   with evenB => I | evenS _ _ => I end).
+Qed.