[Haskell-cafe] induction on type-level Nat

[Henning Thielemann]

I want to define a list with type-level Nat length:

type family List (n::Nat) :: Type -> Type where
    List 0 = End
    List n = Cons (List (n-1))

data End a = End
data Cons f a = Cons { head :: a, tail :: f a }


But this way, GHC cannot match ‘List (n+1)’ with ‘Cons (List n)’, also not 
with the magic type checker plugings suggested before.

I guess I need a another way to define List or some support for the type 
checker to accept List (n+1) ~ Cons (List n).