Singleton types and sized lists : making size of a list part of its type

Singleton.hs

{-#LANGUAGE GADTs #-}

module Singleton where

data S n = Succ n
data Z = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

data List n a where
   Nil :: List Z a
   Cons :: Nat n => a -> List n a -> List (S n) a

instance Show a => Show (List n a) where
  show Nil = "Nil"
  show (Cons x xs) = show x ++ ":" ++ show xs
         

zzip :: Nat n => List n a -> List n b -> List n (a, b)
zzip Nil Nil = Nil
zzip (Cons x xs) (Cons y ys) = Cons (x,y) (zzip xs ys)


main :: IO ()
main = do
  -- Compilation error because of the size of the list :)
  print $ zzip (Cons "coucou" (Cons "pouet" Nil))  (Cons 'p' (Cons '&' (Cons 't' Nil)))