replicate of lengthed list

replicate.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}

import Prelude (undefined, Show, Bool(..), ($), print, IO, Integer)
import GHC.TypeLits
import Data.Proxy

data List (len :: Nat) a where
    Null :: List 0 a
    Cons :: a -> List len a -> List (len + 1) a

deriving instance Show a => Show (List l a)

infixr `Cons`

class Replicate' (b :: Bool) (len :: Nat) a where
    replicate' :: proxyA b -> proxyB len -> a -> List len a

instance (Replicate' (1 <=? len) len a, slen ~ (len + 1)) => Replicate' True slen a where
    replicate' _ _ a = 
        Cons a $ replicate' (Proxy :: Proxy (1 <=? len)) (Proxy :: Proxy len) a

instance Replicate' False 0 a where
    replicate' _ _ _ = Null

type Replicate len a = Replicate' (1 <=? len) len a

replicate :: forall proxy len a. Replicate len a => proxy len -> a -> List len a
replicate _ a = replicate' (Proxy :: Proxy (1 <=? len)) (Proxy :: Proxy len) a

length :: forall len a. KnownNat len => List len a -> Integer
length _ = natVal (Proxy :: Proxy len)

main :: IO ()
main = print $ length $ replicate (Proxy :: Proxy 10) 'a'