title: replicate function for a length-indexed list using GHC.TypeLits and singletons
body: <p>I'm trying to write a replicate function for a length-indexed list using the machinery from <a href="https://hackage.haskell.org/package/base-4.11.0.0/docs/GHC-TypeLits.html" rel="nofollow noreferrer">GHC.TypeLits</a>, <a href="https://hackage.haskell.org/package/singletons-2.4.1" rel="nofollow noreferrer">singletons</a>, and <a href="https://hackage.haskell.org/package/constraints-0.10" rel="nofollow noreferrer">constraints</a>.</p>
  
  <p>The <code>Vect</code> type and signature for <code>replicateVec</code> are given below:</p>
  
  <pre><code>data Vect :: Nat -&gt; Type -&gt; Type where
    VNil  :: Vect 0 a
    VCons :: a -&gt; Vect (n - 1) a -&gt; Vect n a
  
  replicateVec :: forall n a. SNat n -&gt; a -&gt; Vect n a
  </code></pre>
  
  <p>How can you write this <code>replicateVec</code> function?</p>
  
  <hr>
  
  <p>I have a version of <code>replicateVec</code> that compiles and type checks, but it appears to go into an infinite loop when run.  The code is below.  I have added comments to try to make the laws and proofs I am using a little easier to understand:</p>
  
  <pre><code>{-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE TypeInType #-}
  
  module VectStuff 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((-)), sing)
  import Data.Singletons.TypeLits (SNat, Sing(SNat))
  import GHC.TypeLits (CmpNat, KnownNat, Nat)
  import Unsafe.Coerce (unsafeCoerce)
  
  data Vect :: Nat -&gt; Type -&gt; Type where
    VNil  :: Vect 0 a
    VCons :: forall n a. a -&gt; Vect (n - 1) a -&gt; Vect n a
  
  deriving instance Show a =&gt; Show (Vect n a)
  
  -- This is used to define the two laws below.
  axiom :: Dict a
  axiom = unsafeCoerce (Dict :: Dict ())
  
  -- | This law says that if we know that @n@ is not 0, then it MUST be
  -- greater than 0.
  nGT0CmpNatLaw :: (Refuted (n :~: 0)) -&gt; Dict (CmpNat n 0 ~ 'GT)
  nGT0CmpNatLaw _ = axiom
  
  -- | This law says that if we know that @n@ is greater than 0, then we know
  -- that @n - 1@ is also a 'KnownNat'.
  cmpNatGT0KnownNatLaw :: forall n. (CmpNat n 0 ~ 'GT) :- KnownNat (n - 1)
  cmpNatGT0KnownNatLaw = Sub axiom
  
  -- | This is a proof that if we have an @n@ that is greater than 0, then
  -- we can get an @'SNat' (n - 1)@
  sNatMinus1 :: forall n. (CmpNat n 0 ~ 'GT) =&gt; SNat n -&gt; SNat (n - 1)
  sNatMinus1 SNat =
    case cmpNatGT0KnownNatLaw @n of
      Sub Dict -&gt; SNat
  
  -- | This is basically a combination of the other proofs.  If we have a
  -- @SNat n@ and we know that it is not 0, then we can get an @SNat (n -1)@
  -- that we know is a 'KnownNat'.
  nGT0Proof ::
       forall n.
       Refuted (n :~: 0)
    -&gt; SNat n
    -&gt; (SNat (n - 1), Dict (KnownNat (n - 1)))
  nGT0Proof f snat =
    case nGT0CmpNatLaw f of
      Dict -&gt;
        case cmpNatGT0KnownNatLaw @n of
          Sub d -&gt; (sNatMinus1 snat, d)
  
  replicateVec :: forall n a. SNat n -&gt; a -&gt; Vect n a
  replicateVec snat a =
    -- First we check if @snat@ is 0.
    case snat %~ (sing @_ @0) of
      -- If we get a proof that @snat@ is 0, then we just return 'VNil'.
      Proved Refl -&gt; VNil
      -- If we get a proof that @snat@ is not 0, then we use 'nGT0Proof'
      -- to get @n - 1@, and pass that to 'replicateVec' recursively.
      Disproved f -&gt;
        case nGT0Proof f snat of
          (snat', Dict) -&gt; VCons a $ replicateVec snat' a
  </code></pre>
  
  <p>However, for some reason this <code>replicateVec</code> function goes into an endless loop when I try to run it:</p>
  
  <pre><code>&gt; replicateVec (sing @_ @3) "4"
  ["4","4","4","4","4","4","4","4","4","4","4","4",^CInterrupted.
  </code></pre>
  
  <p>Why is this happening?  How can I write the <code>replicateVec</code> function correctly?</p>