Static list with fixed length

FixedList.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}

import GHC.TypeLits

data FixedList :: * -> Nat -> * where
  L    :: FixedList a n
  (:+) :: FixedList a n -> a -> FixedList a (n - 1)

check :: FixedList a 0 -> ()
check _ = ()

type SafeList a = FixedList a 0

instance (Show a) => Show (SafeList a) where
  show = show . reverse . toList
    where
      toList :: FixedList a n -> [a]
      toList L         = []
      toList (xs :+ x) = (:) x $ toList xs

l1 = L :: FixedList a 1
l2 = L :: FixedList a 2
l3 = L :: FixedList a 3
l4 = L :: FixedList a 4
l5 = L :: FixedList a 5
l6 = L :: FixedList a 6
l7 = L :: FixedList a 7
l8 = L :: FixedList a 8
l9 = L :: FixedList a 9