Using a magic trick to prove laws about replicateVec

cmpnat-proofs2.hs

{-# 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.Proxy (Proxy(Proxy))
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, natVal)
import Unsafe.Coerce (unsafeCoerce)

data Vect :: Nat -> Type -> Type where
  VNil  :: Vect 0 a
  VCons :: forall n a. CmpNat n 0 ~ 'GT => a -> Vect (n - 1) a -> Vect n a

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

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

newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))

magic ::
     forall n m o.
     (Integer -> Integer -> Integer)
  -> (KnownNat n, KnownNat m) :- KnownNat o
magic f =
  Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m))

nMinus1isSNatProof :: forall n. Refuted (n :~: 0) -> SNat n -> Dict (KnownNat (n - 1))
nMinus1isSNatProof _ SNat =
  case magic @n @1 @(n - 1) (-) of
    Sub d -> d

nGT0Proof :: forall n. Refuted (n :~: 0) -> SNat n -> SNat (n - 1)
nGT0Proof f sNat =
  case nMinus1isSNatProof f sNat of
    Dict -> SNat

snatMinus1NGT0Law :: forall n. SNat (n - 1) -> Dict (CmpNat n 0 ~ 'GT)
snatMinus1NGT0Law _ = axiom

replicateVec :: forall n a. SNat n -> a -> Vect n a
replicateVec snat a =
  case snat %~ (sing @_ @0) of
    Proved Refl -> VNil
    Disproved f ->
      case nGT0Proof f snat of
        snat' ->
          case snatMinus1NGT0Law snat' 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.