From 47910007a9eff37c9f364a269b46874165711abf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Nov 2020 16:14:48 +0100
Subject: Add a new evar source to refer to evars which are types of evars.

To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.

An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
---
 engine/evar_kinds.ml       |  1 +
 engine/evar_kinds.mli      |  1 +
 engine/evd.ml              |  5 +++++
 engine/evd.mli             |  4 ++++
 engine/termops.ml          |  7 +++++++
 pretyping/pretyping.ml     | 35 +++++++++++++++++++----------------
 test-suite/success/evars.v |  9 +++++++++
 vernac/himsg.ml            |  7 +++++++
 8 files changed, 53 insertions(+), 16 deletions(-)

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 71d68f739e..fb41c4491e 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -40,6 +40,7 @@ type t =
   | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
+  | EvarType of Id.t option * Evar.t (* type of an optionally named evar *)
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
   | QuestionMark of question_mark
   | CasesType of bool (* true = a subterm of the type *)
diff --git a/engine/evar_kinds.mli b/engine/evar_kinds.mli
index ffc57cfd15..b2b39d49be 100644
--- a/engine/evar_kinds.mli
+++ b/engine/evar_kinds.mli
@@ -39,6 +39,7 @@ type t =
   | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
+  | EvarType of Id.t option * Evar.t (* type of an optionally named evar *)
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
   | QuestionMark of question_mark
   | CasesType of bool (* true = a subterm of the type *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 498a9d9825..59eea97ce9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1231,6 +1231,11 @@ let restrict evk filter ?candidates ?src evd =
   let evd = declare_future_goal evk' evd in
   (evd, evk')
 
+let update_source evd evk src =
+  let evar_info = EvMap.find evk evd.undf_evars in
+  let evar_info' = { evar_info with evar_source = src } in
+  { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars }
+
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 1c5c65924c..911e00c23a 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -290,6 +290,10 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
     possibly limiting the instances to a set of candidates (candidates
     are filtered according to the filter) *)
 
+val update_source : evar_map -> Evar.t -> Evar_kinds.t located -> evar_map
+(** To update the source a posteriori, e.g. when an evar type of
+    another evar has to refer to this other evar, with a mutual dependency *)
+
 val get_aliased_evars : evar_map -> Evar.t Evar.Map.t
 (** The map of aliased evars *)
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 693945d5ac..ccd49ca495 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -123,6 +123,13 @@ let pr_evar_source env sigma = function
       str "subterm of pattern-matching return predicate"
   | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id
   | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder"
+  | Evar_kinds.EvarType (ido,evk) ->
+      let pp = match ido with
+        | Some id -> str "?" ++ Id.print id
+        | None ->
+          try pr_existential_key sigma evk
+          with (* defined *) Not_found -> str "an internal placeholder" in
+     str "type of " ++ pp
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let open Globnames in
       let print_constr = print_kconstr in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b70ff20e32..f52dfc51ac 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -472,8 +472,19 @@ let pretype_sort ?loc sigma s =
   let sigma, s = interp_sort ?loc sigma s in
   judge_of_sort ?loc sigma s
 
-let new_type_evar env sigma loc =
-  new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
+let new_typed_evar env sigma ?naming ~src tycon =
+  match tycon with
+  | Some ty ->
+    let sigma, c = new_evar env sigma ~src ?naming ty in
+    sigma, c, ty
+  | None ->
+    let sigma, ty = new_type_evar env sigma ~src in
+    let sigma, c = new_evar env sigma ~src ?naming ty in
+    let evk = fst (destEvar sigma c) in
+    let ido = Evd.evar_ident evk sigma in
+    let src = (fst src,Evar_kinds.EvarType (ido,evk)) in
+    let sigma = update_source sigma (fst (destEvar sigma ty)) src in
+    sigma, c, ty
 
 let mark_obligation_evar sigma k evc =
   match k with
@@ -636,13 +647,9 @@ struct
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j tycon
 
   let pretype_patvar self kind ?loc ~program_mode ~poly resolve_tc tycon env sigma =
-    let sigma, ty =
-      match tycon with
-      | Some ty -> sigma, ty
-      | None -> new_type_evar env sigma loc in
     let k = Evar_kinds.MatchingVar kind in
-    let sigma, uj_val = new_evar env sigma ~src:(loc,k) ty in
-    sigma, { uj_val; uj_type = ty }
+    let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) tycon in
+    sigma, { uj_val; uj_type }
 
   let pretype_hole self (k, naming, ext) =
     fun ?loc ~program_mode ~poly resolve_tc tycon env sigma ->
@@ -653,19 +660,15 @@ struct
         | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id)
         | IntroAnonymous -> IntroAnonymous
         | IntroFresh id -> IntroFresh (interp_ltac_id env id) in
-      let sigma, ty =
-        match tycon with
-        | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma loc in
-      let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
+      let sigma, uj_val, uj_type = new_typed_evar env sigma ~src:(loc,k) ~naming tycon in
       let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in
-      sigma, { uj_val; uj_type = ty }
+      sigma, { uj_val; uj_type }
 
     | Some arg ->
       let sigma, ty =
         match tycon with
         | Some ty -> sigma, ty
-        | None -> new_type_evar env sigma loc in
+        | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in
       let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
       sigma, { uj_val = c; uj_type = ty }
 
@@ -1144,7 +1147,7 @@ struct
         | None ->
           let sigma, p = match tycon with
             | Some ty -> sigma, ty
-            | None -> new_type_evar env sigma loc
+            | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.CasesType false)
           in
           sigma, it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar sigma pred in
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 253b48e4d9..2308656f7c 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -426,3 +426,12 @@ Abort.
 (* (reported as bug #7356) *)
 
 Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z).
+
+(* A printing check in passing *)
+
+Axiom abs : forall T, T.
+Fail Type let x := _ in
+     ltac:(
+       let t := type of x in
+       unify x (abs t);
+     exact 0).
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d86ea90e6..777b3b0c96 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -572,6 +572,13 @@ let rec explain_evar_kind env sigma evk ty =
       strbrk "the type of " ++ Id.print id
   | Evar_kinds.BinderType Anonymous ->
       strbrk "the type of this anonymous binder"
+  | Evar_kinds.EvarType (ido,evk) ->
+      let pp = match ido with
+        | Some id -> str "?" ++ Id.print id
+        | None ->
+          try pr_existential_key sigma evk
+          with (* defined *) Not_found -> strbrk "an internal placeholder" in
+      strbrk "the type of " ++ pp
   | Evar_kinds.ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
       strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++
-- 
cgit v1.2.3