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

[Andres Löh]

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