Merge PR #8217: Fixes #8215: "critical" type inference bug in interpreting evars by name

3 files changed, 53 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index b163517090..8651c8e23a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -81,6 +81,11 @@ Specification language
   variables) may occasionally change type inference in incompatible
   ways, especially regarding the inference of the return clause of "match".
 
+- Fixing a missing check in interpreting instances of existential
+  variables which are bound to local definitions might exceptionally
+  induce an overhead if the cost of checking the conversion of the
+  corresponding definitions is additionally high (PR #8215).
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d10c00fa6e..e3aa90fbcf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -960,20 +960,50 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
 and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
   let f decl (subst,update) =
     let id = NamedDecl.get_id decl in
+    let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
     let t = replace_vars subst (NamedDecl.get_type decl) in
+    let check_body id c =
+      match b, c with
+      | Some b, Some c ->
+         if not (is_conv !!env !evdref b c) then
+           user_err ?loc  (str "Cannot interpret " ++
+             pr_existential_key !evdref evk ++
+             strbrk " in current context: binding for " ++ Id.print id ++
+             strbrk " is not convertible to its expected definition (cannot unify " ++
+             quote (print_constr_env !!env !evdref b) ++
+             strbrk " and " ++
+             quote (print_constr_env !!env !evdref c) ++
+             str ").")
+      | Some b, None ->
+           user_err ?loc  (str "Cannot interpret " ++
+             pr_existential_key !evdref evk ++
+             strbrk " in current context: " ++ Id.print id ++
+             strbrk " should be bound to a local definition.")
+      | None, _ -> () in
+    let check_type id t' =
+      if not (is_conv !!env !evdref t t') then
+        user_err ?loc  (str "Cannot interpret " ++
+          pr_existential_key !evdref evk ++
+          strbrk " in current context: binding for " ++ Id.print id ++
+          strbrk " is not well-typed.") in
     let c, update =
       try
         let c = List.assoc id update in
         let c = pretype k0 resolve_tc (mk_tycon t) env evdref c in
+        check_body id (Some c.uj_val);
         c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
-        let (n,_,t') = lookup_rel_id id (rel_context !!env) in
-        if is_conv !!env !evdref t (lift n t') then mkRel n, update else raise Not_found
+        let (n,b',t') = lookup_rel_id id (rel_context !!env) in
+        check_type id (lift n t');
+        check_body id (Option.map (lift n) b');
+        mkRel n, update
       with Not_found ->
       try
-        let t' = !!env |> lookup_named id |> NamedDecl.get_type in
-        if is_conv !!env !evdref t t' then mkVar id, update else raise Not_found
+        let decl = lookup_named id !!env in
+        check_type id (NamedDecl.get_type decl);
+        check_body id (NamedDecl.get_value decl);
+        mkVar id, update
       with Not_found ->
         user_err ?loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v
new file mode 100644
index 0000000000..c4b29a6354
--- /dev/null
+++ b/test-suite/bugs/closed/8215.v
@@ -0,0 +1,14 @@
+(* Check that instances for local definitions in evars have compatible body *)
+Goal False.
+Proof.
+  pose (n := 1).
+  evar (m:nat).
+  subst n.
+  pose (n := 0).
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clearbody n.
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clear n.
+  pose (n := 0+1).
+  Check ?m. (* Should be ok *)
+Abort.