Merge PR #12422: Fixes #12418: an assert false in inference of return clause

Reviewed-by: gares

3 files changed, 35 insertions, 1 deletions

diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
new file mode 100644
index 0000000000..8f126c5b6f
--- /dev/null
+++ b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match`
+  (`#12422 <https://github.com/coq/coq/pull/12422>`_,
+  fixes `#12418 <https://github.com/coq/coq/pull/12418>`_,
+  by Hugo Herbelin).
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5e3fb9dae3..25353b7c12 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1716,7 +1716,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
           let flags = (default_flags_of TransparentState.full) in
           match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with
           | Success evd -> evdref := evd
-          | UnifFailure _ -> assert false
+          | UnifFailure _ -> evdref := add_conv_pb (Reduction.CONV,!!env,substl inst ev',t) sigma
         end;
         ev'
     | _ ->
diff --git a/test-suite/bugs/closed/bug_12418.v b/test-suite/bugs/closed/bug_12418.v
new file mode 100644
index 0000000000..cf11ea627b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12418.v
@@ -0,0 +1,29 @@
+(* The second "match" below used to raise an anomaly *)
+
+Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
+  { ret : forall {t : Type@{d}}, t -> m t }.
+
+Record state {S : Type} (t : Type) : Type := mkState { runState : t }.
+
+Global Declare Instance Monad_state : forall S, Monad (@state S).
+
+Class Cava  := {
+  constant : bool -> unit;
+  constant_vec : unit;
+}.
+
+Axiom F : forall {A : Type}, (bool -> A) -> Datatypes.unit.
+
+Fail Instance T : Cava := {
+
+  constant b := match b with
+    | true => ret tt
+    | false => ret tt
+    end;
+
+  constant_vec := @F _ (fun b => match b with
+    | true => tt
+    | false => tt
+  end);
+
+}.