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
---
 pretyping/retyping.ml              | 12 +++++++++---
 test-suite/bugs/closed/bug_13366.v |  5 +++++
 test-suite/bugs/closed/bug_9809.v  | 30 ++++++++++++++++++++++++++++++
 3 files changed, 44 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_13366.v
 create mode 100644 test-suite/bugs/closed/bug_9809.v

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4bd22e76cb..34bcd0982c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t =
     | _ -> raise Not_found
   else raise Not_found
 
+let sort_of_arity_with_constraints env sigma t =
+  try Reductionops.sort_of_arity env sigma t
+  with Reduction.NotArity ->
+  try
+    let t = get_type_from_constraints env sigma t in
+    Reductionops.sort_of_arity env sigma t
+  with Not_found | Reduction.NotArity -> retype_error NotAnArity
+
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
@@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma =
       let mip = lookup_mind_specif env ind in
       let paramtyps = Array.map_to_list (fun arg () ->
           let t = type_of env arg in
-          let s = try Reductionops.sort_of_arity env sigma t
-            with Reduction.NotArity -> retype_error NotAnArity
-          in
+          let s = sort_of_arity_with_constraints env sigma t in
           Sorts.univ_of_sort (ESorts.kind sigma s))
           args
       in
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