Print evars instead of metas in Clenv unification failures

Author: yannl35133

proofs/clenv.ml

@@ -409,15 +409,47 @@ let clenv_missing ce =
 
 (******************************************************************)
 
+let rec subst_meta sigma s c =
+  match kind sigma c with
+    | Meta i -> (try Int.Map.find i s with Not_found -> c)
+    | _ -> EConstr.map sigma (subst_meta sigma s) c
+
+let replace_clenv_metas env sigma clnv =
+  let module Metas = Unification.Meta in
+  let metam = clenv_meta_list clnv in
+  let sigma, metamap = List.fold_left (fun (sigma, metamap) mv ->
+    let tymeta = Metas.meta_ftype metam mv in
+    let ty = subst_meta sigma metamap tymeta.rebus in
+    let naming = match Metas.meta_name metam mv with
+      | Name na -> Namegen.IntroIdentifier na
+      | Anonymous -> Namegen.IntroAnonymous
+    in
+    let sigma, ev = Evarutil.new_evar ~naming env sigma ty in
+    sigma, Int.Map.add mv ev metamap)
+    (sigma, Int.Map.empty) (clenv_arguments clnv)
+  in
+  sigma, subst_meta sigma metamap
+
+exception ClenvCannotUnify of env * evar_map * clausenv * econstr * econstr * unification_error option
+
 let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
-  let metas = clenv.metam in
-  let metas, sigma = w_unify ~metas ~flags clenv.env clenv.evd cv_pb t1 t2 in
-  update_clenv_evd clenv sigma metas
+  try
+    let metas = clenv.metam in
+    let metas, sigma = w_unify ~metas ~flags clenv.env clenv.evd cv_pb t1 t2 in
+    update_clenv_evd clenv sigma metas
+  with Pretype_errors.(PretypeError (env, sigma, CannotUnify (t1, t2, reason))) as exn ->
+    let _, info = Exninfo.capture exn in
+    Exninfo.iraise (ClenvCannotUnify (env, sigma, clenv, t1, t2, reason), info)
+
 
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
-  let metas = clenv.metam in
-  let metas, sigma = w_unify_meta_types ~metas ~flags:flags clenv.env clenv.evd in
-  update_clenv_evd clenv sigma metas
+  try
+    let metas = clenv.metam in
+    let metas, sigma = w_unify_meta_types ~metas ~flags:flags clenv.env clenv.evd in
+    update_clenv_evd clenv sigma metas
+  with Pretype_errors.(PretypeError (env, sigma, CannotUnify (t1, t2, reason))) as exn ->
+    let _, info = Exninfo.capture exn in
+    Exninfo.iraise (ClenvCannotUnify (env, sigma, clenv, t1, t2, reason), info)
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv concl =
   let metas = meta_handler clenv.metam in

proofs/clenv.mli

@@ -77,6 +77,10 @@ val case_pf : ?with_evars:bool ->
 
 val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
 
+val replace_clenv_metas : env -> evar_map -> clausenv -> evar_map * (EConstr.constr -> EConstr.constr)
+
+exception ClenvCannotUnify of env * evar_map * clausenv * econstr * econstr * Pretype_errors.unification_error option
+
 (** {6 Pretty-print (debug only) } *)
 val pr_clenv : clausenv -> Pp.t
 

tactics/hints.ml

@@ -1632,33 +1632,12 @@ let pr_hint env sigma h = match h.obj with
   | Extern (_, tac) ->
     str "(*external*) " ++ Gentactic.print_glob env sigma ~level:(LevelLe 0) tac
 
-let rec subst_meta sigma s c =
-  match kind sigma c with
-    | Meta i -> (try Int.Map.find i s with Not_found -> c)
-    | _ -> EConstr.map sigma (subst_meta sigma s) c
-
-let replace_clenv_type_metas env sigma clnv =
-  let module Metas = Unification.Meta in
-  let metam = Clenv.clenv_meta_list clnv in
-  let sigma, metamap = List.fold_left (fun (sigma, metamap) mv ->
-    let tymeta = Metas.meta_ftype metam mv in
-    let ty = subst_meta sigma metamap tymeta.rebus in
-    let naming = match Metas.meta_name metam mv with
-      | Name na -> IntroIdentifier na
-      | Anonymous -> IntroAnonymous
-    in
-    let sigma, ev = Evarutil.new_evar ~naming env sigma ty in
-    sigma, Int.Map.add mv ev metamap)
-    (sigma, Int.Map.empty) (Clenv.clenv_arguments clnv)
-  in
-  sigma, subst_meta sigma metamap (Clenv.clenv_type clnv)
-
 let pr_default_pattern env sigma = function
 | Give_exact h ->
   pr_leconstr_env env sigma h.hint_type
 | Res_pf h | ERes_pf h | Res_pf_THEN_trivial_fail h ->
-  let sigma, c = replace_clenv_type_metas env sigma h.hint_clnv in
-  pr_leconstr_env env sigma c
+  let sigma, f = Clenv.replace_clenv_metas env sigma h.hint_clnv in
+  pr_leconstr_env env sigma (f (Clenv.clenv_type h.hint_clnv))
 | Unfold_nth _ | Extern _ ->
   (* These hints cannot contain DefaultPattern *)
   assert false

vernac/himsg.ml

@@ -1738,6 +1738,9 @@ let rec vernac_interp_error_handler = function
     explain_type_error env (Evd.from_env env) te
   | PretypeError(ctx,sigma,te) ->
     explain_pretype_error ctx sigma te
+  | Clenv.ClenvCannotUnify (env, sigma, clenv, t1, t2, reason) ->
+    let sigma, f = Clenv.replace_clenv_metas env sigma clenv in
+    explain_pretype_error env sigma (CannotUnify (f t1, f t2, reason))
   | PrimNotations.PrimTokenNotationError(kind,ctx,sigma,te) ->
     explain_prim_token_notation_error kind ctx sigma te
   | Typeclasses_errors.TypeClassError(env, sigma, te) ->