This file changes the plusMinusEq law to use Refl (:~:) instead of Dict.

vec-proofs-using-refl-instead-of-dict.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 VectStuff5 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. n :~: ((n - m) + m)
plusMinusEq = unsafeCoerce Refl

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
        Refl ->
          case unsafeKnownNat @n of
            Dict -> VCons a $ replicateVec @(n - 1) a

This is as suggested in https://stackoverflow.com/questions/49709113/replicate-function-for-a-length-indexed-list-using-ghc-typelits-and-singletons/49710029?noredirect=1#comment86456465_49710029.

This can be loaded into GHCI with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package constraints