From 9a99bad924f3c82107a5ecfa7a906988f0f69309 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 30 Oct 2018 18:07:49 +0100
Subject: [PATCH] Check univ instances in Typing.

---
 kernel/typeops.ml                |  3 +-
 kernel/typeops.mli               |  3 +-
 pretyping/arguments_renaming.mli |  2 ++
 pretyping/typing.ml              | 50 ++++++++++++++++++++++++++------
 4 files changed, 47 insertions(+), 11 deletions(-)

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1bb2d3c79c28..c8fd83c8a908 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 d24002065be7..419332413690 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 6a776dc961e4..6d1b6eefd41b 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 dc3f042431ab..5a969eff6cf4 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -277,6 +277,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 +329,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