Merge PR #12449: Minimize Prop <= i to i := Set

Reviewed-by: mattam82
Ack-by: Janno
Ack-by: gares

3 files changed, 31 insertions, 30 deletions

diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index f33030d6a4..eaf8c65811 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -175,10 +175,7 @@ let define_evar_as_sort env evd (ev,args) =
   let evd' = Evd.define ev (mkSort s) evd in
   Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s
 
-(* Propagation of constraints through application and abstraction:
-   Given a type constraint on a functional term, returns the type
-   constraint on its domain and codomain. If the input constraint is
-   an evar instantiate it with the product of 2 new evars. *)
+(* Unify with unknown array *)
 
 let rec presplit env sigma c =
   let c = Reductionops.whd_all env sigma c in
@@ -189,25 +186,6 @@ let rec presplit env sigma c =
     presplit env sigma (mkApp (lam, args))
   | _ -> sigma, c
 
-let split_tycon ?loc env evd tycon =
-  match tycon with
-  | None -> evd,(make_annot Anonymous Relevant,None,None)
-  | Some c ->
-    let evd, c = presplit env evd c in
-    let evd, na, dom, rng = match EConstr.kind evd c with
-      | Prod (na,dom,rng) -> evd, na, dom, rng
-      | Evar ev ->
-        let (evd,prod) = define_evar_as_product env evd ev in
-        let (na,dom,rng) = destProd evd prod in
-        let anon = {na with binder_name = Anonymous} in
-        evd, anon, dom, rng
-      | _ ->
-        (* XXX no error to allow later coercion? Not sure if possible with funclass *)
-        error_not_product ?loc env evd c
-    in
-    evd, (na, mk_tycon dom, mk_tycon rng)
-
-
 let define_pure_evar_as_array env sigma evk =
   let evi = Evd.find_undefined sigma evk in
   let evenv = evar_env env evi in
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
index e5c3f8baa1..5702e169c8 100644
--- a/pretyping/evardefine.mli
+++ b/pretyping/evardefine.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Names
 open EConstr
 open Evd
 open Environ
@@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
   evar_map * existential
 
-val split_tycon :
-  ?loc:Loc.t -> env ->  evar_map -> type_constraint ->
-    evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint)
-
 val split_as_array : env -> evar_map -> type_constraint ->
   evar_map * type_constraint
 (** If the constraint can be made to look like [array A] return [A],
@@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t
 
 val pr_tycon : env -> evar_map -> type_constraint -> Pp.t
 
+(** Used for bidi heuristic when typing lambdas. Transforms an applied
+    evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *)
+val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b9825b6a92..7597661ca8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -925,7 +925,32 @@ struct
         let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in
         sigma, Some ty'
     in
-    let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in
+    let sigma,name',dom,rng =
+      match tycon' with
+      | None -> sigma,Anonymous, None, None
+      | Some ty ->
+        let sigma, ty = Evardefine.presplit !!env sigma ty in
+        match EConstr.kind sigma ty with
+        | Prod (na,dom,rng) ->
+          sigma, na.binder_name, Some dom, Some rng
+        | Evar ev ->
+          (* define_evar_as_product works badly when impredicativity
+             is possible but not known (#12623). OTOH if we know we
+             are impredicative (typically Prop) we want to keep the
+             information when typing the body. *)
+          let s = Retyping.get_sort_of !!env sigma ty in
+          if Environ.is_impredicative_sort !!env s
+             || Evd.check_leq sigma (Univ.Universe.type1) (Sorts.univ_of_sort s)
+          then
+            let sigma, prod = define_evar_as_product !!env sigma ev in
+            let na,dom,rng = destProd sigma prod in
+            sigma, na.binder_name, Some dom, Some rng
+          else
+            sigma, Anonymous, None, None
+        | _ ->
+          (* XXX no error to allow later coercion? Not sure if possible with funclass *)
+          error_not_product ?loc !!env sigma ty
+    in
     let dom_valcon = valcon_of_tycon dom in
     let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in
     let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in
@@ -934,7 +959,7 @@ struct
     let var',env' = push_rel ~hypnaming sigma var env in
     let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in
     let name = get_name var' in
-    let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in
+    let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
     discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
   let pretype_prod self (name, bk, c1, c2) =