From 0fff401b5c12a2d0684c8ff4980ebd9716f93905 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 13 Nov 2020 13:17:21 +0100
Subject: Extend hack to use postponed constraints in retyping to template poly

See 742ef62fe8050a6865d06bd644e30cbec0e7eb02

Fix #13366
Fix #9809
---
 test-suite/bugs/closed/bug_13366.v |  5 +++++
 test-suite/bugs/closed/bug_9809.v  | 30 ++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13366.v
 create mode 100644 test-suite/bugs/closed/bug_9809.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13366.v b/test-suite/bugs/closed/bug_13366.v
new file mode 100644
index 0000000000..06918a9266
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13366.v
@@ -0,0 +1,5 @@
+Class Functor (F : Type -> Type) : Type :=
+  fmap : F nat.
+
+Fail Definition blah := sum fmap.
+(* used to be anomaly not an arity *)
diff --git a/test-suite/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v
new file mode 100644
index 0000000000..4a7d2c7fac
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9809.v
@@ -0,0 +1,30 @@
+Section FreeMonad.
+
+  Variable S : Type.
+  Variable P : S -> Type.
+
+  Inductive FreeF A : Type :=
+  | retFree : A -> FreeF A
+  | opr     : forall s, (P s -> FreeF A) -> FreeF A.
+
+End FreeMonad.
+
+Section Fibonnacci.
+
+  Inductive gen_op := call_op : nat -> gen_op.
+  Definition gen_ty (op : gen_op) :=
+    match op with
+    | call_op _ => nat
+    end.
+
+  Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat :=
+    match n  with
+    | 0
+    | 1 => retFree _ _ _ 1
+    | S (S k) =>
+      opr _ _ _ (call_op (S k))
+          (fun r1 => opr _ _ _ (call_op k)
+                      (fun r0 => retFree (* _ _ _ *) (r1 + r0)))
+    end.
+
+End Fibonnacci.
-- 
cgit v1.2.3