test-suite/bugs/opened/3490.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
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.