[Haskell-cafe] induction on type-level Nat

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).