is the following function possible at all? decode :: forall (n :: Nat). Vec Type n -> Type -> Type decode Nil t = t decode (Cons x xs) t = x -> (decode xs t)