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

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

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'
     | _ ->

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