Merge PR #13371: Extend hack to use postponed constraints in retyping to template poly

Reviewed-by: gares
Reviewed-by: herbelin

2 files changed, 35 insertions, 0 deletions

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.