From 22d0e5cf023ce3fc33a8a5c0dd774847aa06e0b0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 18:17:30 +0200
Subject: Fixes #12418 (inference of return clause meets assert false).

This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.
---
 pretyping/cases.ml                 |  2 +-
 test-suite/bugs/closed/bug_12418.v | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_12418.v

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


From dec5edf7c92950881693afe2040d711155cf15b5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 29 May 2020 12:57:32 +0200
Subject: Change log for #12422.

---
 .../12422-master+fix-12418-cases-anomaly.rst                         | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst

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).
-- 
cgit v1.2.3