4 files changed, 161 insertions, 0 deletions
diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v
new file mode 100644
index 00000000..800c431e
--- /dev/null
+++ b/test-suite/ideal-features/Case9.v
@@ -0,0 +1,12 @@
+(* Exemple soumis par Pierre Corbineau (bug #1671) *)
+
+CoInductive hdlist : unit -> Type :=
+| cons : hdlist tt -> hdlist tt.
+
+Variable P : forall bo, hdlist bo -> Prop.
+Variable all : forall bo l, P bo l.
+
+Definition F (l:hdlist tt) : P tt l := 
+match l in hdlist u return P u l with
+| cons (cons l') => all tt _
+end.
diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v
new file mode 100644
index 00000000..6f9f86a9
--- /dev/null
+++ b/test-suite/ideal-features/complexity/evars_subst.v
@@ -0,0 +1,53 @@
+(* Bug report #932 *)
+(* Expected time < 1.00s *)
+
+(* Let n be the number of let-in. The complexity comes from the fact
+   that each implicit arguments of f was in a larger and larger
+   context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", 
+   "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This
+   type is an evar instantiated on the n variables denoting the "f ?Ti 0".
+   One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the
+   type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another
+   substitution is done leading to 
+   "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]"
+   and so on. At the end, we get a term of exponential size *)
+
+(* A way to cut the complexity could have been to remove the dependency in
+   anonymous variables in evars but this breaks intuitive behaviour
+   (see Case15.v); another approach could be to substitute lazily
+   and/or to simultaneously substitute let binders and evars *)
+
+Variable P : Set -> Set.
+Variable f : forall A : Set, A -> P A.
+
+Time Check
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+ 
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+    f _ 0.
+
diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v
new file mode 100644
index 00000000..6f9f86a9
--- /dev/null
+++ b/test-suite/ideal-features/evars_subst.v
@@ -0,0 +1,53 @@
+(* Bug report #932 *)
+(* Expected time < 1.00s *)
+
+(* Let n be the number of let-in. The complexity comes from the fact
+   that each implicit arguments of f was in a larger and larger
+   context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", 
+   "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This
+   type is an evar instantiated on the n variables denoting the "f ?Ti 0".
+   One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the
+   type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another
+   substitution is done leading to 
+   "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]"
+   and so on. At the end, we get a term of exponential size *)
+
+(* A way to cut the complexity could have been to remove the dependency in
+   anonymous variables in evars but this breaks intuitive behaviour
+   (see Case15.v); another approach could be to substitute lazily
+   and/or to simultaneously substitute let binders and evars *)
+
+Variable P : Set -> Set.
+Variable f : forall A : Set, A -> P A.
+
+Time Check
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+ 
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+  let _ := f _ 0 in
+
+    f _ 0.
+
diff --git a/test-suite/ideal-features/universes.v b/test-suite/ideal-features/universes.v
new file mode 100644
index 00000000..6db4cfe1
--- /dev/null
+++ b/test-suite/ideal-features/universes.v
@@ -0,0 +1,43 @@
+(* Some issues with polymorphic inductive types *)
+
+(* 1- upper constraints with respect to non polymorphic inductive types *)
+
+Unset Elimination Schemes.
+Definition Ty := Type (* Top.1 *).
+
+Inductive Q (A:Type (* Top.2 *)) : Prop := q : A -> Q A.
+Inductive T (B:Type (* Top.3 *)) := t : B -> Q (T B) -> T B.
+(* ajoute Top.4 <= Top.2 inutilement: 
+   4 est l'univers utilisé dans le calcul du type polymorphe de T *)
+Definition C := T Ty.
+(* ajoute Top.1 < Top.3 :
+   Top.3 jour le rôle de pivot pour propager les contraintes supérieures qu'on
+   a sur l'argument B de T: Top.3 sera réutilisé plus tard comme majorant
+   des arguments effectifs de T, propageant à cette occasion les contraintes
+   supérieures sur Top.3 *)
+
+(* We need either that Q is polymorphic on A (though it is in Type) or
+   that the constraint Top.1 < Top.2 is set (and it is not set!) *)
+
+(* 2- upper constraints with respect to unfoldable constants *)
+
+Definition f (A:Type (* Top.1 *)) := True.
+Inductive R := r : f R -> R.
+(* ajoute Top.3 <= Top.1 inutilement: 
+   Top.3 est l'univers utilisé dans le calcul du type polymorphe de R *)
+
+(* mais il manque la contrainte que l'univers de R est plus petit que Top.1
+   ce qui l'empêcherait en fait d'être vraiment polymorphe *)
+
+(* 3- constraints with respect to global constants *)
+
+Inductive S (A:Ty) := s : A -> S A.
+
+(* Q est considéré polymorphique vis à vis de A alors que le type de A
+   n'est pas une variable mais un univers déjà existant *)
+
+(* Malgré tout la contrainte Ty < Ty est ajoutée (car Ty est vu comme
+   un pivot pour propager les contraintes sur le type A, comme si Q était
+   vraiment polymorphique, ce qu'il n'est pas parce que Ty est une
+   constante). Et heureusement qu'elle est ajouté car elle évite de
+   pouvoir typer "Q Ty" *)