Writing replicateVec without depending on the singleton library and without using structural typing.

vec-proofs-no-singleton.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}

module VectStuff4 where

import Data.Constraint (Dict(Dict))
import Data.Kind (Type)
import Data.Proxy (Proxy(Proxy))
import Data.Type.Equality
import GHC.TypeLits
       (type (+), type (-), KnownNat, Nat, SomeNat(SomeNat),
        natVal, sameNat, someNatVal)
import Unsafe.Coerce (unsafeCoerce)

data Vect :: Nat -> Type -> Type where
  VNil :: Vect 0 a
  VCons :: a -> Vect n a -> Vect (n + 1) a

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

plusMinusEq :: forall n m. Dict (n ~ ((n - m) + m))
plusMinusEq = unsafeCoerce (Dict :: Dict ())

unsafeKnownNat :: forall n. KnownNat n => Dict (KnownNat (n - 1))
unsafeKnownNat =
  let int = natVal (Proxy @n) - 1
  in
  case someNatVal int of
    Nothing -> error "error"
    Just (SomeNat (Proxy :: Proxy x)) ->
      unsafeCoerce (Dict :: Dict (KnownNat x)) int

replicateVec :: forall n a. KnownNat n => a -> Vect n a
replicateVec a =
  case sameNat (Proxy @n) (Proxy @0) of
    Just Refl -> VNil
    Nothing ->
      case plusMinusEq @n @1 of
        Dict ->
          case unsafeKnownNat @n of
            Dict -> VCons a $ replicateVec @(n - 1) a

I think unsafeCoerce (Dict :: Dict (KnownNat x)) int should be unsafeCoerce (Dict :: Dict (KnownNat x)), but I have no idea why it works even with that extra argument. It's probably a combination of very low level implementation details.