1 files changed, 89 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v
new file mode 100644
index 000000000..a5f4ae64a
--- /dev/null
+++ b/test-suite/bugs/closed/2584.v
@@ -0,0 +1,89 @@
+Require Import List.
+
+Set Implicit Arguments.
+
+Definition err : Type := unit. 
+
+Inductive res (A: Type) : Type :=
+| OK: A -> res A
+| Error: err -> res A. 
+
+Implicit Arguments Error [A].
+
+Set Printing Universes.
+
+Section FOO.
+
+Inductive ftyp : Type :=
+  | Funit : ftyp 
+  | Ffun : list ftyp -> ftyp 
+  | Fref : area -> ftyp
+with area : Type := 
+  | Stored : ftyp -> area        
+.
+
+Print ftyp.
+(* yields:
+Inductive ftyp : Type (* Top.27429 *) :=
+    Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
+  with area : Type (* Set *) :=  Stored : ftyp -> area
+*)
+
+Fixpoint tc_wf_type (ftype: ftyp) {struct ftype}: res unit :=
+  match ftype with
+    | Funit => OK tt
+    | Ffun args => 
+       ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
+           match ftypes with
+             | nil => OK tt
+             | t::ts =>
+                 match tc_wf_type t with
+                   | OK tt => tc_wf_types ts
+                   | Error m => Error m 
+                 end 
+           end) args) 
+     | Fref a => tc_wf_area a
+   end
+with tc_wf_area (ar:area): res unit :=
+  match ar with
+    | Stored c => tc_wf_type c
+  end.
+
+End FOO.
+
+Print ftyp.
+(* yields:
+Inductive ftyp : Type (* Top.27465 *) :=
+    Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
+  with area : Set :=  Stored : ftyp -> area
+*)
+
+Fixpoint tc_wf_type' (ftype: ftyp) {struct ftype}: res unit :=
+  match ftype with
+    | Funit => OK tt
+    | Ffun args => 
+       ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
+           match ftypes with
+             | nil => OK tt
+             | t::ts =>
+                 match tc_wf_type' t with
+                   | OK tt => tc_wf_types ts
+                   | Error m => Error m 
+                 end 
+           end) args) 
+     | Fref a => tc_wf_area' a
+   end
+with tc_wf_area' (ar:area): res unit :=
+  match ar with
+    | Stored c => tc_wf_type' c
+  end.
+
+(* yields:
+Error:
+Incorrect elimination of "ar" in the inductive type "area":
+the return type has sort "Type (* max(Set, Top.27424) *)" while it
+should be "Prop" or "Set".
+Elimination of an inductive object of sort Set
+is not allowed on a predicate in sort Type
+because strong elimination on non-small inductive types leads to paradoxes.
+*)
+\ No newline at end of file