Test for bug #3490.

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3490.v b/test-suite/bugs/closed/3490.v
new file mode 100644
index 0000000000..e7a5caa1de
--- /dev/null
+++ b/test-suite/bugs/closed/3490.v
@@ -0,0 +1,27 @@
+Inductive T : Type :=                                                                                        
+| Var : nat -> T                                                                                                 
+| Arr : T -> T -> T.                                                                                             
+
+Inductive Tele : list T -> Type :=                                                                               
+| Tnil  : @Tele nil                                                                                              
+| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
+
+Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
+   : { x : Type & x -> nat -> Type } :=
+     match t return { x : Type & x -> nat -> Type } with
+       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
+       | Tcons ls t' l =>
+         let (result, get) := TeleD ls t' in
+         @existT Type (fun x => x -> nat -> Type)
+                 { v : result & (fix TD (t : T) {struct t} :=
+                                   match  t with
+                                     | Var n =>
+                                       get v n
+                                     | Arr a b => TD a -> TD b
+                                   end) l }
+                 (fun x n =>
+                    match n return Type with
+                      | 0 => projT2 x
+                      | S n => get (projT1 x) n
+                    end)
+     end.