test010.idr

data MyNat = MyO | MyS MyNat

%default total

data Bad = MkBad (Bad -> Int) Int
         | MkBad' Int

vapp : Vect n a -> Vect m a -> Vect (n + m) a
vapp []        ys = ys
vapp (x :: xs) ys = x :: vapp xs ys

foo : Bad -> Int
foo (MkBad f i) = f (MkBad' i)
foo (MkBad' x) = x