Writing replicateVec without needing the magic trick. A little simpler.

vec-proofs.hs

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

module VectStuff2 where

import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Singletons.Decide (Decision(Disproved, Proved), Refuted, (:~:)(Refl), (%~))
import Data.Singletons.Prelude (PNum((-), (+)), SNum((%-)), sing)
import Data.Singletons.TypeLits (KnownNat, Nat, SNat, Sing(SNat), natVal)
-- import GHC.TypeLits (Nat {-CmpNat, KnownNat, Nat, natVal-})
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)

axiom :: Dict a
axiom = unsafeCoerce (Dict :: Dict (a ~ a))

plusMinusEqLaw :: forall n m. Dict (n ~ ((n - m) + m))
plusMinusEqLaw = axiom

nMinus1isSNatProof :: forall n. Refuted (n :~: 0) -> SNat n -> SNat (n - 1)
nMinus1isSNatProof _ SNat = (sing @_ @n) %- (sing @_ @1)

replicateVec :: forall n a. SNat n -> a -> Vect n a
replicateVec snat a =
  case snat %~ (sing @_ @0) of
    Proved Refl -> VNil
    Disproved f ->
      case nMinus1isSNatProof f snat of
        snat'@SNat ->
          case plusMinusEqLaw @n @1 of
            Dict ->
              VCons a $ replicateVec snat' a

This is for https://stackoverflow.com/questions/49709113/replicate-function-for-a-length-indexed-list-using-ghc-typelits-and-singletons.

This can be loaded into GHCI with the following command:

$ stack --resolver nightly-2018-03-18 ghci --package classy-prelude  --package singletons --package containers --package typelits-witnesses --package constraints