аюсь написать функцию репликации для списка с индексом длины, используя механизм изGHC.TypeLits, одиночек, а такжеограничения.

Vect тип и подпись дляreplicateVec приведены ниже:

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

replicateVec :: forall n a. SNat n -> a -> Vect n a

Как ты можешь написать этоreplicateVec функционировать?

У меня есть версияreplicateVec который компилирует и проверяет тип, но при запуске он, похоже, входит в бесконечный цикл. Код ниже. Я добавил комментарии, чтобы попытаться сделать законы и доказательства, которые я использую, немного проще для понимания:

{-# 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 -> Type -> Type where
  VNil  :: Vect 0 a
  VCons :: forall n a. a -> Vect (n - 1) a -> Vect n a

deriving instance Show a => 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)) -> 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) => SNat n -> SNat (n - 1)
sNatMinus1 SNat =
  case cmpNatGT0KnownNatLaw @n of
    Sub Dict -> 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)
  -> SNat n
  -> (SNat (n - 1), Dict (KnownNat (n - 1)))
nGT0Proof f snat =
  case nGT0CmpNatLaw f of
    Dict ->
      case cmpNatGT0KnownNatLaw @n of
        Sub d -> (sNatMinus1 snat, d)

replicateVec :: forall n a. SNat n -> a -> 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 -> 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 ->
      case nGT0Proof f snat of
        (snat', Dict) -> VCons a $ replicateVec snat' a

Однако по какой-то причине этоreplicateVec Функция входит в бесконечный цикл, когда я пытаюсь запустить его:

> replicateVec (sing @_ @3) "4"
["4","4","4","4","4","4","4","4","4","4","4","4",^CInterrupted.

Почему это происходит? Как я могу написатьreplicateVec функционировать правильно?