Is this use of unsafeCoerce valid?

Main.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Main (main) where

import Data.Functor.Identity
import Data.Proxy
import Data.Type.Equality ((:~:)(..))
import GHC.TypeNats
import Numeric.Natural
import qualified Prelude
import Prelude hiding (length)
import Unsafe.Coerce (unsafeCoerce)

main :: IO ()
main = print $
  let Just v = fromList (knownNat @2) [knownNat @1, knownNat @1]
  in joinWith (\_ w l -> addNat w l) knownNat v

-----
-- parameterized-utils
-----

newtype NatRepr (n::Nat) = NatRepr Natural

instance Show (NatRepr n) where
  show (NatRepr n) = show n

knownNat :: forall n . KnownNat n => NatRepr n
knownNat = NatRepr (natVal (Proxy :: Proxy n))

maxInt :: Natural
maxInt = fromIntegral (maxBound :: Int)

widthVal :: NatRepr n -> Int
widthVal (NatRepr i) | i <= maxInt = fromIntegral i
                     | otherwise   = error ("Width is too large: " ++ show i)

addNat :: NatRepr m -> NatRepr n -> NatRepr (m+n)
addNat (NatRepr m) (NatRepr n) = NatRepr (m+n)

data LeqProof (m :: Nat) (n :: Nat) where
  LeqProof :: (m <= n) => LeqProof m n

testStrictLeq :: forall m n
               . (m <= n)
              => NatRepr m
              -> NatRepr n
              -> Either (LeqProof (m+1) n) (m :~: n)
testStrictLeq (NatRepr m) (NatRepr n)
  | m < n = Left (unsafeCoerce (LeqProof :: LeqProof 0 0))
  | otherwise = Right (unsafeCoerce (Refl :: m :~: m))
{-# NOINLINE testStrictLeq #-}

leqRefl :: forall f n . f n -> LeqProof n n
leqRefl _ = LeqProof

leqSub2 :: LeqProof x_l x_h
        -> LeqProof y_l y_h
        -> LeqProof (x_l-y_h) (x_h-y_l)
leqSub2 LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 0 0)
{-# NOINLINE leqSub2 #-}

leqMulCongr :: LeqProof a x
            -> LeqProof b y
            -> LeqProof (a*b) (x*y)
leqMulCongr LeqProof LeqProof = unsafeCoerce (LeqProof :: LeqProof 1 1)
{-# NOINLINE leqMulCongr #-}

leqMulPos :: forall p q x y
          .  (1 <= x, 1 <= y)
          => p x
          -> q y
          -> LeqProof 1 (x*y)
leqMulPos _ _ = leqMulCongr (LeqProof :: LeqProof 1 x) (LeqProof :: LeqProof 1 y)

lemmaMul :: (1 <= n) => p w -> q n -> (w + (n-1) * w) :~: (n * w)
lemmaMul = unsafeCoerce Refl
{-# NOINLINE lemmaMul #-}

data Vector n a where
  Vector :: (1 <= n) => !(VVector a) -> Vector n a

length :: Vector n a -> NatRepr n
length (Vector xs) = NatRepr (fromIntegral (vlength xs) :: Natural)
{-# INLINE length #-}

nonEmpty :: Vector n a -> LeqProof 1 n
nonEmpty (Vector _) = LeqProof
{-# Inline nonEmpty #-}

uncons :: forall n a.  Vector n a -> (a, Either (n :~: 1) (Vector (n-1) a))
uncons v@(Vector xs) = (vhead xs, mbTail)
  where
  mbTail :: Either (n :~: 1) (Vector (n - 1) a)
  mbTail = case testStrictLeq (knownNat @1) (length v) of
             Left n2_leq_n ->
               do LeqProof <- return (leqSub2 n2_leq_n (leqRefl (knownNat @1)))
                  return (Vector (vtail xs))
             Right Refl    -> Left Refl
{-# Inline uncons #-}

fromList :: (1 <= n) => NatRepr n -> [a] -> Maybe (Vector n a)
fromList n xs
  | widthVal n == vlength v = Just (Vector v)
  | otherwise               = Nothing
  where
  v = vfromList xs
{-# INLINE fromList #-}

joinWithM ::
  forall m f n w.
  (1 <= w, Monad m) =>
  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> m (f (w + l)))
  -> NatRepr w
  -> Vector n (f w)
  -> m (f (n * w))

joinWithM jn w = fmap fst . go
  where
  go :: forall l. Vector l (f w) -> m (f (l * w), NatRepr (l * w))
  go exprs =
    case uncons exprs of
      (a, Left Refl) -> return (a, w)
      (a, Right rest) ->
        case nonEmpty rest                of { LeqProof ->
        case leqMulPos (length rest) w    of { LeqProof ->
        case nonEmpty exprs               of { LeqProof ->
        case lemmaMul w (length exprs)    of { Refl -> do
          (res, sz) <- go rest
          joined <- jn sz a res
          return (joined, addNat w sz)
        }}}}

joinWith ::
  forall f n w.
  (1 <= w) =>
  (forall l. (1 <= l) => NatRepr l -> f w -> f l -> f (w + l))
  -> NatRepr w
  -> Vector n (f w)
  -> f (n * w)
joinWith jn w v = runIdentity $ joinWithM (\n x -> pure . (jn n x)) w v
{-# Inline joinWith #-}

-- The real @parameterized-utils@ library uses 'Vector' from the @vector@
-- library. However, that isn't necessary to trigger the bug, so to avoid
-- incurring a dependency on @vector@, we simulate it with a linked list.
type VVector a = [a]

vfromList :: [a] -> VVector a
vfromList = id

vhead :: VVector a -> a
vhead = head

vlength :: VVector a -> Int
vlength = Prelude.length

vtail :: VVector a -> [a]
vtail = tail

repro.txt

############
# With -O0 #
############

$ rm -f *.hi *.o && /opt/ghc/8.6.5/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 8.6.5 for x86_64_unknown_linux)
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
Aborted (core dumped)

$ rm -f *.hi *.o && /opt/ghc/8.8.4/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 8.8.4 for x86_64_unknown_linux)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
Aborted (core dumped)

$ rm -f *.hi *.o && /opt/ghc/8.10.4/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 8.10.4 for x86_64_unknown_linux)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
Aborted (core dumped)

$ rm -f *.hi *.o && /opt/ghc/9.0.1/bin/ghc -O0 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 9.0.1 for x86_64_unknown_linux)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
Aborted (core dumped)

############
# With -O1 #
############

$ rm -f *.hi *.o && /opt/ghc/8.6.5/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 8.6.5 for x86_64_unknown_linux)
    Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug
Aborted (core dumped)

$ rm -f *.hi *.o && /opt/ghc/8.8.4/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 8.8.4 for x86_64_unknown_linux)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
Aborted (core dumped)

$ rm -f *.hi *.o && /opt/ghc/8.10.4/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
Main: internal error: stg_ap_pp_ret
    (GHC version 8.10.4 for x86_64_unknown_linux)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
Aborted (core dumped)

$ rm -f *.hi *.o && /opt/ghc/9.0.1/bin/ghc -O1 Main.hs && ./Main
[1 of 1] Compiling Main             ( Main.hs, Main.o )
Linking Main ...
2