Not quite sure how to implement

Lits.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}

module Lits where

import GHC.TypeLits
import Data.Proxy
import Prelude hiding (showList)


-- I have no idea how to write this...

-- fromList :: forall n a . SomeNat n => [a] -> List n a
-- fromList [] = Nil
-- fromList (x:xs) = Cons x (fromList xs)


toList :: List n a -> [a]
toList Nil = []
toList (Cons x xs) = x : toList xs


data List :: Nat -> * -> * where
  Cons :: a -> List (n-1) a -> List n a
  Nil  :: List 0 a


instance Show a => Show (List n a) where
  show = show . toList