Re: [Haskell-cafe] working through "Part I: Dependent Types in Haskell"

Hi.

init' :: Vector a ('S n) -> Vector a n init' (x1 :- Nil) = Nil init' (x :- xs) = x :- (init' xs)

You need to pattern match further on `xs` in order to make clear that you require it to not be `Nil`. The type checker doesn't look at the first case in order to conclude that you've already ruled that out. So e.g. init' (x :- xs @ (_ :- _)) = x :- (init' xs) works. Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com Registered in England & Wales, OC335890 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England