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.
---
 test-suite/bugs/closed/bug_12418.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12418.v

(limited to 'test-suite')

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