Convert type-level lists to term-level sized-vectors

Vector.hs

#!/usr/bin/env stack
-- stack --resolver lts-10.3 script --package ghc-typelits-natnormalise

{-

$ tail -2 Vector.hs
print $ toVector @[1, 2, 3, 4, 5]
print $ toVector @["whomp", "merp", "yarp"]

$ ./Vector.hs
Cons 1 (Cons 2 (Cons 3 (Cons 4 (Cons 5 Nil))))
Cons "whomp" (Cons "merp" (Cons "yarp" Nil))

-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import Data.Kind
import Data.Proxy
import GHC.TypeLits

data Vector :: Nat -> Type -> Type where
  Nil :: Vector 0 a
  Cons :: a -> Vector n a -> Vector (n + 1) a

deriving instance Show a => Show (Vector n a)

type family Length (xs :: [k]) where
  Length '[] = 0
  Length (_ ': xs) = 1 + Length xs

class ToTerm (k :: Type) (t :: k) (e :: Type) | k -> e, t -> e where
  toTerm :: proxy t -> e

instance KnownSymbol s => ToTerm Symbol s String where
  toTerm = symbolVal

instance KnownNat n => ToTerm Nat n Integer where
  toTerm = natVal

class ToVector ts e where
  toVector :: Vector (Length ts) e

instance ToVector '[] e where
  toVector = Nil

instance (ToTerm k t e, ToVector ts e) => ToVector (t ': ts) e where
  toVector = Cons (toTerm (Proxy @t)) (toVector @ts)

main :: IO ()
main = do
  print $ toVector @[1, 2, 3, 4, 5]
  print $ toVector @["whomp", "merp", "yarp"]