Not quite sure how to implement

LengthList.hs

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

module LengthList
( LengthList (..)
-- examples
, list2
, list3
-- list functions
, zipWith
, length
) where

import Prelude hiding (length, zipWith)
import Data.Proxy (Proxy (..))
import GHC.TypeLits

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

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

-- length-list examples

list2 :: LengthList 2 Char
list2 = Cons 'a' (Cons 'b' Nil)

list3 :: LengthList 3 Char
list3 = Cons 'a' (Cons 'b' (Cons 'c' Nil))

-- list functions duplicated for length-lists

zipWith :: (a -> b -> c)
        -> LengthList (n :: Nat) a
        -> LengthList (n :: Nat) b
        -> LengthList (n :: Nat) c
zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)
zipWith _ Nil Nil = Nil

length :: forall n a. (KnownNat n) => LengthList n a -> Integer
length _ = natVal (Proxy :: Proxy n)

-- conversions

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