Fixes #12418 (inference of return clause meets assert false).

This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.

2 files changed, 30 insertions, 1 deletions

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);
+
+}.