Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handler in NotFoundInstance

Reviewed-by: ejgallego

4 files changed, 39 insertions, 10 deletions

diff --git a/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst
new file mode 100644
index 0000000000..5758f35c3d
--- /dev/null
+++ b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  A case of unification raising an anomaly IllTypedInstance
+  (`#13376 <https://github.com/coq/coq/pull/13376>`_,
+  fixes `#13266 <https://github.com/coq/coq/issues/13266>`_,
+  by Hugo Herbelin).
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ca16c52026..cbf539c1e9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1317,6 +1317,7 @@ let check_selected_occs env sigma c occ occs =
      raise (PretypeError (env,sigma,NoOccurrenceFound (c,None)))
      else ()
 
+(* Error local to the module *)
 exception TypingFailed of evar_map
 
 let set_of_evctx l =
@@ -1347,12 +1348,6 @@ let thin_evars env sigma sign c =
   let c' = applyrec (env,0) c in
   (!sigma, c')
 
-exception NotFoundInstance of exn
-let () = CErrors.register_handler (function
-    | NotFoundInstance e ->
-      Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e)
-    | _ -> None)
-
 let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
   try
   let evi = Evd.find_undefined evd evk in
@@ -1495,9 +1490,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
                           List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l ->
                  instantiate_evar evar_unify flags env_rhs evd ev vid
                | _ -> evd)
-           with e when CErrors.noncritical e ->
-             let e, info = Exninfo.capture e in
-             Exninfo.iraise (NotFoundInstance e, info)
+           with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ ->
+              user_err (Pp.str "Cannot find an instance.")
          else
            ((if debug_ho_unification () then
                let evi = Evd.find evd evk in
@@ -1714,7 +1708,7 @@ let solve_unconstrained_impossible_cases env evd =
       let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
       let ty = j_type j in
       let flags = default_flags env in
-      instantiate_evar evar_unify flags env evd' evk ty
+      instantiate_evar evar_unify flags env evd' evk ty (* should we protect from raising IllTypedInstance? *)
     | _ -> evd') evd evd
 
 let solve_unif_constraints_with_heuristics env
diff --git a/test-suite/output/bug_13266.out b/test-suite/output/bug_13266.out
new file mode 100644
index 0000000000..034830f1ac
--- /dev/null
+++ b/test-suite/output/bug_13266.out
@@ -0,0 +1,12 @@
+The command has indeed failed with message:
+Abstracting over the terms "S", "p" and "u" leads to a term
+fun (S0 : Type) (p0 : proc S0) (_ : S0) => p0 = Tick -> True
+which is ill-typed.
+Reason is: Illegal application: 
+The term "@eq" of type "forall A : Type, A -> A -> Prop"
+cannot be applied to the terms
+ "proc S0" : "Prop"
+ "p0" : "proc S0"
+ "Tick" : "proc unit"
+The 3rd term has type "proc unit" which should be coercible to 
+"proc S0".
diff --git a/test-suite/output/bug_13266.v b/test-suite/output/bug_13266.v
new file mode 100644
index 0000000000..e59455a326
--- /dev/null
+++ b/test-suite/output/bug_13266.v
@@ -0,0 +1,18 @@
+Inductive proc : Type -> Type :=
+| Tick : proc unit
+.
+
+Inductive exec :
+  forall T, proc T -> T -> Prop :=
+| ExecTick :
+    exec _ (Tick) tt
+.
+
+Lemma foo :
+  exec _ Tick tt ->
+  True.
+Proof.
+  intros H. 
+  remember Tick as p.
+  Fail induction H.
+Abort.