GADT shenanigans in Haskell

vect.hs

{-# LANGUAGE DataKinds, StandaloneKindSignatures, GADTs,
             StandaloneDeriving, DerivingStrategies, ScopedTypeVariables,
             TypeOperators, TypeFamilies, ConstraintKinds,
             FlexibleInstances, MultiParamTypeClasses,
             IncoherentInstances, UndecidableSuperClasses,
             TypeApplications, AllowAmbiguousTypes,
             ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors -Wno-unused-imports #-}

module Main where

import Data.Kind ( Type, Constraint )
import Prelude ( IO, Bool(..), Show, (&&), error, undefined, Integer, Num(..), otherwise, Eq(..), (||), print )
import Data.Type.Equality ( (:~:)(..) )
import Unsafe.Coerce ( unsafeCoerce )
import GHC.TypeNats
import Data.Proxy

--data Nat = Zero | Succ Nat

type Vec :: Nat -> Type -> Type
data Vec n a where
  Nil  :: Vec 0 a
  (:>) :: a -> Vec n a -> Vec (n+1) a
infixr 5 :>

deriving stock instance Show a => Show (Vec n a)

type SNat :: Nat -> Type
data SNat n where
  SZero :: SNat 0
  SSucc :: SNat n -> SNat (n+1)

-- x :: SNat (Succ (Succ Zero))
-- x must be SSucc (SSucc SZero)

length :: forall n a. Vec n a -> SNat n
length Nil = SZero
length (_ :> xs) = SSucc (length xs)

{-
replicate
-}

replicate :: SNat n -> a -> Vec n a
-- replicate :: foreach (n :: Nat) -> a -> Vec n a
replicate SZero _ = Nil
replicate (SSucc n) x = x :> replicate n x

fromKnownNat :: forall n. KnownNat n => SNat n
fromKnownNat = go (natVal (Proxy @n))
  where
    go :: Natural -> SNat m
    go 0 = unsafeCoerce SZero
    go k = unsafeCoerce (SSucc (go (k - 1)))

getx :: forall n. KnownNat n => () -> Vec n Integer
getx () = replicate (fromKnownNat @n) 1

main :: IO ()
main = print x
  where x@(_ :> _ :> _ :> Nil) = getx @3 ()