weird compile error with proof for length indexed vector

weirderror.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.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. CmpNat n 0 ~ 'GT => a -> Vect (n - 1) a -> Vect n a

instance Show a => Show (Vect n a) where
  show = show . toListVect

toListVect :: Vect n a -> [a]
toListVect VNil = []
toListVect (VCons a v) = a : toListVect v

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

nGT0CmpNatLaw :: (Refuted (n :~: 0)) -> Dict (CmpNat n 0 ~ 'GT)
nGT0CmpNatLaw _ = axiom

cmpNatGT0KnownNatLaw :: forall n. (CmpNat n 0 ~ 'GT) :- KnownNat (n - 1)
cmpNatGT0KnownNatLaw = Sub axiom

sNatMinus1 :: forall n. (CmpNat n 0 ~ 'GT) => SNat n -> SNat (n - 1)
sNatMinus1 SNat =
  case cmpNatGT0KnownNatLaw @n of
    Sub Dict -> SNat

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)

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', Dict) ->
          case snatMinus1NGT0Law @n snat' of
            Dict ->
              VCons a $ replicateVec snat' a

vec0 :: Vect 0 Char
vec0 = VNil

vec1 :: Vect 1 Char
vec1 = VCons 'a' vec0

vec2 :: Vect 2 Char
vec2 = VCons 'b' vec1

thisisweird :: Int
thisisweird =
  case replicateVec (sing @_ @2) "4" of
    VCons _ (efe :: Vect 1 String) ->
      case efe of
        VCons _ (jaja :: Vect 0 String) ->
          -- This case causes the following error:
          -- *** Exception: temp/what8.hs:(90,11)-(91,23): Non-exhaustive patterns in case
          case jaja of
            VNil -> 100
            -- But adding a case for VCons causes a compile error:
            --
            -- temp/what8.hs:95:13: error:
            --     • Couldn't match type ‘'EQ’ with ‘'GT’
            --       Inaccessible code in
            --         a pattern with constructor:
            --           VCons :: forall (n :: Nat) a.
            --                    (CmpNat n 0 ~ 'GT) =>
            --                    a -> Vect (n - 1) a -> Vect n a,
            --         in a case alternative
            --     • In the pattern: VCons _ _
            --       In a case alternative: VCons _ _ -> 200
            --       In the expression:
            --         case jaja of
            --           VNil -> 100
            --           VCons _ _ -> 200
            --    |
            -- 95 |             VCons _ _ -> 200
            --    |             ^^^^^^^^^
            -- Failed, no modules loaded.
            --
            -- VCons _ _ -> 200

Running the thisisweird function causes Non-exhaustive patterns in case or a compile error for some reason.

This is apparently because cmpNatGT0KnownNatLaw is wrong: https://stackoverflow.com/a/49710029/3040129