Merge PR #13379: Add a new evar source to refer to evars which are types of evars

Reviewed-by: SkySkimmer

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" ++