Surprising force in unsafe coercion

Summary

I hesitate to call this a bug, per se, because what I'm doing is not exactly "supported", but I'd like to understand why this happens and would much rather it didn't. I'm working on @andrewthad's primitive-unlifted package, which offers types for arrays and other structures containing types of kind TYPE 'UnliftedRep. This involves fairly liberal use of unsafe coercions. I've been able to find ways to make things work (at least in simple tests), but one way that seems like it should work actually does not.

Steps to reproduce

{-# language MagicHash #-}
{-# language UnboxedTuples #-}
{-# language UnliftedNewtypes #-}
{-# language KindSignatures #-}
{-# language RoleAnnotations #-}
import GHC.Exts

-- | A mutable array of unlifted things.
newtype MutableUnliftedArray# s (a :: TYPE 'UnliftedRep) = MutableUnliftedArray# (MutableArray# s Any)
type role MutableUnliftedArray# nominal representational

readUnliftedArray# :: MutableUnliftedArray# s a -> Int# -> State# s -> (# State# s, a #)
{-# INLINE readUnliftedArray# #-}
readUnliftedArray# (MutableUnliftedArray# mary) i s
  = case readArray# mary i s of
      (# s', a #) -> (# s', unsafeCoerce# a #)

Compiling with -O2 -ddump-simpl gives the following (-O0 does basically the same thing, but with no unfolding and a bit more mess):

readUnliftedArray# [InlPrag=INLINE (sat-args=3)]
  :: forall s (a :: TYPE 'UnliftedRep).
     MutableUnliftedArray# s a -> Int# -> State# s -> (# State# s, a #)
[GblId,
 Arity=3,
 Caf=NoCafRefs,
 Str=<L,U><L,U><L,U>,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=3,unsat_ok=False,boring_ok=False)
         Tmpl= \ (@ s_a2xI)
                 (@ (a_a2xJ :: TYPE 'UnliftedRep))
                 (ds_d2I1 [Occ=Once] :: MutableUnliftedArray# s_a2xI a_a2xJ)
                 (i_a2ou [Occ=Once] :: Int#)
                 (s1_a2ov [Occ=Once] :: State# s_a2xI) ->
                 case Exts.readArray#
                        @ s_a2xI
                        @ Any
                        (ds_d2I1
                         `cast` (Data.Primitive.Unlifted.Array.Primops.N:MutableUnliftedArray#[0]
                                     <s_a2xI>_N <a_a2xJ>_R
                                 :: MutableUnliftedArray# s_a2xI a_a2xJ
                                    ~R# MutableArray# s_a2xI Any))
                        i_a2ou
                        s1_a2ov
                 of
                 { (# ipv_s2K4 [Occ=Once], ipv1_s2K5 [Occ=Once] #) ->
                 case ipv1_s2K5
                      `cast` (UnsafeCo representational Any a_a2xJ :: Any ~R# a_a2xJ)
                 of wild_Xa [Occ=Once]
                 { __DEFAULT ->
                 (# ipv_s2K4, wild_Xa #)
                 }
                 }}]
readUnliftedArray#
  = \ (@ s_a2xI)
      (@ (a_a2xJ :: TYPE 'UnliftedRep))
      (ds_d2I1 :: MutableUnliftedArray# s_a2xI a_a2xJ)
      (i_a2ou :: Int#)
      (s1_a2ov :: State# s_a2xI) ->
      case Exts.readArray#
             @ s_a2xI
             @ Any
             (ds_d2I1
              `cast` (Data.Primitive.Unlifted.Array.Primops.N:MutableUnliftedArray#[0]
                          <s_a2xI>_N <a_a2xJ>_R
                      :: MutableUnliftedArray# s_a2xI a_a2xJ
                         ~R# MutableArray# s_a2xI Any))
             i_a2ou
             s1_a2ov
      of
      { (# ipv_s2K0, ipv1_s2K1 #) ->
      case ipv1_s2K1
           `cast` (UnsafeCo representational Any a_a2xJ :: Any ~R# a_a2xJ)
      of wild_Xf
      { __DEFAULT ->
      (# ipv_s2K0, wild_Xf #)
      }
      }

The surprising and undesirable feature here is

      case ipv1_s2K1
           `cast` (UnsafeCo representational Any a_a2xJ :: Any ~R# a_a2xJ)
      of wild_Xf
      { __DEFAULT ->

That is, the result of the array read is forced. Since it's actually an unlifted thing, this produces an unchecked exception at runtime.

Expected behavior

I expect the inner case to be omitted. I can get the code I want by changing the definition to

readUnliftedArray# :: MutableUnliftedArray# s a -> Int# -> State# s -> (# State# s, a #)
readUnliftedArray# (MutableUnliftedArray# mary) i s
  = unsafeCoerce# (readArray# mary i s)
{-# INLINE readUnliftedArray# #-}

which produces this Core:

readUnliftedArray#1_r2OY
  :: forall s (a :: TYPE 'UnliftedRep).
     MutableUnliftedArray# s a
     -> Int# -> State# s -> (# State# s, Any #)
[GblId,
 Arity=3,
 Caf=NoCafRefs,
 Str=<L,U><L,U><L,U>,
 Unf=OtherCon []]
readUnliftedArray#1_r2OY
  = \ (@ s_a2y1)
      (@ (a_a2y2 :: TYPE 'UnliftedRep))
      (ds_d2Ii :: MutableUnliftedArray# s_a2y1 a_a2y2)
      (i_a2oS :: Int#)
      (s1_a2oT :: State# s_a2y1) ->
      Exts.readArray#
        @ s_a2y1
        @ Any
        (ds_d2Ii
         `cast` (Data.Primitive.Unlifted.Array.Primops.N:MutableUnliftedArray#[0]
                     <s_a2y1>_N <a_a2y2>_R
                 :: MutableUnliftedArray# s_a2y1 a_a2y2
                    ~R# MutableArray# s_a2y1 Any))
        i_a2oS
        s1_a2oT

readUnliftedArray# [InlPrag=INLINE (sat-args=3)]
  :: forall s (a :: TYPE 'UnliftedRep).
     MutableUnliftedArray# s a -> Int# -> State# s -> (# State# s, a #)
[GblId,
 Arity=3,
 Caf=NoCafRefs,
 Str=<L,U><L,U><L,U>,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=3,unsat_ok=False,boring_ok=True)
         Tmpl= (\ (@ s_X2yM)
                  (@ (a_X2yO :: TYPE 'UnliftedRep))
                  (ds_X2J5 [Occ=Once] :: MutableUnliftedArray# s_X2yM a_X2yO)
                  (i_X2pG [Occ=Once] :: Int#)
                  (s1_X2pI [Occ=Once] :: State# s_X2yM) ->
                  Exts.readArray#
                    @ s_X2yM
                    @ Any
                    (ds_X2J5
                     `cast` (Data.Primitive.Unlifted.Array.Primops.N:MutableUnliftedArray#[0]
                                 <s_X2yM>_N <a_X2yO>_R
                             :: MutableUnliftedArray# s_X2yM a_X2yO
                                ~R# MutableArray# s_X2yM Any))
                    i_X2pG
                    s1_X2pI)
               `cast` (forall (s :: <*>_N) (a :: <TYPE 'UnliftedRep>_N).
                       <MutableUnliftedArray# s a>_R
                       ->_R <Int#>_R
                       ->_R <State# s>_R
                       ->_R ((#,#)
                               <'Exts.TupleRep '[]>_R
                               (UnsafeCo representational 'Exts.LiftedRep 'UnliftedRep)
                               <State# s>_R
                               (UnsafeCo representational Any a))_R
                       :: (forall s (a :: TYPE 'UnliftedRep).
                           MutableUnliftedArray# s a
                           -> Int# -> State# s -> (# State# s, Any #))
                          ~R# (forall s (a :: TYPE 'UnliftedRep).
                               MutableUnliftedArray# s a
                               -> Int# -> State# s -> (# State# s, a #)))}]
readUnliftedArray#
  = readUnliftedArray#1_r2OY
    `cast` (forall (s :: <*>_N) (a :: <TYPE 'UnliftedRep>_N).
            <MutableUnliftedArray# s a>_R
            ->_R <Int#>_R
            ->_R <State# s>_R
            ->_R ((#,#)
                    <'Exts.TupleRep '[]>_R
                    (UnsafeCo representational 'Exts.LiftedRep 'UnliftedRep)
                    <State# s>_R
                    (UnsafeCo representational Any a))_R
            :: (forall s (a :: TYPE 'UnliftedRep).
                MutableUnliftedArray# s a
                -> Int# -> State# s -> (# State# s, Any #))
               ~R# (forall s (a :: TYPE 'UnliftedRep).
                    MutableUnliftedArray# s a
                    -> Int# -> State# s -> (# State# s, a #)))

Environment

• GHC version used: 8.10.1

Optional:

• Operating System:
• System Architecture: