Merge PR #8866: Check universe instances in Typing

7 files changed, 69 insertions, 61 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index e341412294..f61dd0c101 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -350,9 +350,6 @@ let map_universes f env =
     { env with env_stratification =
 	 { s with env_universes = f s.env_universes } }
 
-let set_universes env u =
-  { env with env_stratification = { env.env_stratification with env_universes = u } }
-
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
   else map_universes (UGraph.merge_constraints c) env
@@ -405,19 +402,12 @@ let add_constant_key kn cb linkinfo env =
 let add_constant kn cb env =
   add_constant_key kn cb no_link_info env
 
-let constraints_of cb u =
-  match cb.const_universes with
-  | Monomorphic_const _ -> Univ.Constraint.empty
-  | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
-
 (* constant_type gives the type of a constant *)
 let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
-  match cb.const_universes with
-  | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
-  | Polymorphic_const _ctx ->
-    let csts = constraints_of cb u in
-    (subst_instance_constr u cb.const_type, csts)
+  let uctx = Declareops.constant_polymorphic_context cb in
+  let csts = Univ.AUContext.instantiate u uctx in
+  (subst_instance_constr u cb.const_type, csts)
 
 type const_evaluation_result = NoBody | Opaque
 
@@ -425,20 +415,14 @@ exception NotEvaluableConst of const_evaluation_result
 
 let constant_value_and_type env (kn, u) =
   let cb = lookup_constant kn env in
-    if Declareops.constant_is_polymorphic cb then
-      let cst = constraints_of cb u in
-      let b' = match cb.const_body with
-	| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
-	| OpaqueDef _ -> None
-	| Undef _ -> None
-      in
-	b', subst_instance_constr u cb.const_type, cst
-    else 
-      let b' = match cb.const_body with
-	| Def l_body -> Some (Mod_subst.force_constr l_body)
-	| OpaqueDef _ -> None
-	| Undef _ -> None
-      in b', cb.const_type, Univ.Constraint.empty
+  let uctx = Declareops.constant_polymorphic_context cb in
+  let cst = Univ.AUContext.instantiate u uctx in
+  let b' = match cb.const_body with
+    | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
+    | OpaqueDef _ -> None
+    | Undef _ -> None
+  in
+  b', subst_instance_constr u cb.const_type, cst
 
 let body_of_constant_body env cb =
   let otab = opaque_tables env in
@@ -457,9 +441,7 @@ let body_of_constant_body env cb =
 (* constant_type gives the type of a constant *)
 let constant_type_in env (kn,u) =
   let cb = lookup_constant kn env in
-    if Declareops.constant_is_polymorphic cb then
-      subst_instance_constr u cb.const_type
-    else cb.const_type
+  subst_instance_constr u cb.const_type
 
 let constant_value_in env (kn,u) =
   let cb = lookup_constant kn env in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0255581749..c285f907fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -155,11 +155,6 @@ val named_body : variable -> env -> constr option
 val fold_named_context :
   (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-val set_universes : env -> UGraph.t -> env
-(** This is used to update universes during a proof for the sake of
-   evar map-unaware functions, eg [Typing] calling
-   [Typeops.check_hyps_inclusion]. *)
-
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1bb2d3c79c..c8fd83c8a9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -91,7 +91,8 @@ let type_of_variable env id =
 (* Checks if a context of variables can be instantiated by the
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env f c sign =
+let check_hyps_inclusion env ?evars f c sign =
+  let conv env a b = conv env ?evars a b in
   Context.Named.fold_outside
     (fun d1 () ->
       let open Context.Named.Declaration in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d24002065b..4193324136 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -116,4 +116,5 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
+val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+  ('a -> constr) -> 'a -> Constr.named_context -> unit
diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli
index 6a776dc961..6d1b6eefd4 100644
--- a/pretyping/arguments_renaming.mli
+++ b/pretyping/arguments_renaming.mli
@@ -17,6 +17,8 @@ val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit
 (** [Not_found] is raised if no names are defined for [r] *)
 val arguments_names : GlobRef.t -> Name.t list
 
+val rename_type : types -> GlobRef.t -> types
+
 val rename_type_of_constant : env -> pconstant -> types
 val rename_type_of_inductive : env -> pinductive -> types
 val rename_type_of_constructor : env -> pconstructor -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index dc3f042431..b5729d7574 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -218,9 +218,6 @@ let judge_of_cast env sigma cj k tj =
     sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
              uj_type = expected_type }
 
-let enrich_env env sigma =
-  set_universes env @@ Evd.universes sigma
-
 let check_fix env sigma pfix =
   let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   let (idx, (ids, cs, ts)) = pfix in
@@ -277,6 +274,38 @@ let judge_of_letin env name defj typj j =
   { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
     uj_type = subst1 defj.uj_val j.uj_type }
 
+let check_hyps_inclusion env sigma f x hyps =
+  let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
+  let f x = EConstr.Unsafe.to_constr (f x) in
+  Typeops.check_hyps_inclusion env ~evars f x hyps
+
+let type_of_constant env sigma (c,u) =
+  let open Declarations in
+  let cb = Environ.lookup_constant c env in
+  let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in
+  let u = EInstance.kind sigma u in
+  let ty, csts = Environ.constant_type env (c,u) in
+  let sigma = Evd.add_constraints sigma csts in
+  sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c)))
+
+let type_of_inductive env sigma (ind,u) =
+  let open Declarations in
+  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+  let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+  let u = EInstance.kind sigma u in
+  let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
+  let sigma = Evd.add_constraints sigma csts in
+  sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind)))
+
+let type_of_constructor env sigma ((ind,_ as ctor),u) =
+  let open Declarations in
+  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+  let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+  let u = EInstance.kind sigma u in
+  let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
+  let sigma = Evd.add_constraints sigma csts in
+  sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
+
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env sigma cstr =
@@ -297,17 +326,17 @@ let rec execute env sigma cstr =
     | Var id ->
         sigma, judge_of_variable env id
 
-    | Const (c, u) ->
-        let u = EInstance.kind sigma u in
-        sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u)))
+    | Const c ->
+        let sigma, ty = type_of_constant env sigma c in
+        sigma, make_judge cstr ty
 
-    | Ind (ind, u) ->
-        let u = EInstance.kind sigma u in
-        sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u)))
+    | Ind ind ->
+        let sigma, ty = type_of_inductive env sigma ind in
+        sigma, make_judge cstr ty
 
-    | Construct (cstruct, u) ->
-        let u = EInstance.kind sigma u in
-        sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u)))
+    | Construct ctor ->
+        let sigma, ty = type_of_constructor env sigma ctor in
+        sigma, make_judge cstr ty
 
     | Case (ci,p,c,lf) ->
         let sigma, cj = execute env sigma c in
@@ -391,7 +420,6 @@ and execute_recdef env sigma (names,lar,vdef) =
 and execute_array env = Array.fold_left_map (execute env)
 
 let check env sigma c t =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   match Evarconv.cumul env sigma j.uj_type t with
   | None ->
@@ -401,14 +429,12 @@ let check env sigma c t =
 (* Type of a constr *)
 
 let unsafe_type_of env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   j.uj_type
 
 (* Sort of a type *)
 
 let sort_of env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   let sigma, a = type_judgment env sigma j in
   sigma, a.utj_type
@@ -416,7 +442,6 @@ let sort_of env sigma c =
 (* Try to solve the existential variables by typing *)
 
 let type_of ?(refresh=false) env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
     if refresh then
@@ -424,7 +449,6 @@ let type_of ?(refresh=false) env sigma c =
     else sigma, j.uj_type
 
 let solve_evars env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
   sigma, nf_evar sigma j.uj_val
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 25f9bc5576..5cead11a5c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4097,12 +4097,15 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
 let guess_elim isrec dep s hyp0 gl =
   let tmptyp0 =	Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in
-  let evd, elimc =
-    if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl
+  let env = Tacmach.New.pf_env gl in
+  let sigma = Tacmach.New.project gl in
+  let sigma, elimc =
+    if isrec && not (is_nonrec mind)
+    then
+      let gr = lookup_eliminator mind s in
+      Evd.fresh_global env sigma gr
     else
-      let env = Tacmach.New.pf_env gl in
-      let sigma = Tacmach.New.project gl in
-      let u = EInstance.kind (Tacmach.New.project gl) u in
+      let u = EInstance.kind sigma u in
       if dep then
         let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in
         let ind = EConstr.of_constr ind in
@@ -4112,8 +4115,8 @@ let guess_elim isrec dep s hyp0 gl =
         let ind = EConstr.of_constr ind in
         (sigma, ind)
   in
-  let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
-    evd, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+  let elimt = Typing.unsafe_type_of env sigma elimc in
+    sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let sigma = Tacmach.New.project gl in