Arch-dependent coercions?

ArchWS.hs

{-# OPTIONS_GHC -Wno-inaccessible-code -Wno-overlapping-patterns #-}
{-# LANGUAGE GHC2021, GADTs #-}

module ArchWS (ArchWS(..), archWS) where

-- base
import Data.Coerce (Coercible, coerce)
import Data.Type.Coercion (Coercion(..))
import Data.Word (Word32, Word64)
import Data.Int (Int32, Int64)
import Data.Bits (finiteBitSize)
import Unsafe.Coerce (unsafeCoerce)

data ArchWS where
  A32 :: (Coercible Word32 Word, Coercible Int32 Int) => ArchWS
  A64 :: (Coercible Word64 Word, Coercible Int64 Int) => ArchWS
  UNK ::                                                 ArchWS

archWS :: ArchWS
archWS = case wordSize of
  32 -> case unsafeWord32 of
    Coercion -> case unsafeInt32 of
      Coercion -> A32
  64 -> case unsafeWord64 of
    Coercion -> case unsafeInt64 of
      Coercion -> A64
  _  -> UNK
 where
  wordSize :: Int
  wordSize = finiteBitSize (0 :: Word)

  unsafeWord32 :: Coercion Word32 Word
  unsafeWord32 = unsafeCoerce (Coercion @Word @Word)

  unsafeInt32 :: Coercion Int32 Int
  unsafeInt32 = unsafeCoerce (Coercion @Int @Int)

  unsafeWord64 :: Coercion Word64 Word
  unsafeWord64 = unsafeCoerce (Coercion @Word @Word)

  unsafeInt64 :: Coercion Int64 Int
  unsafeInt64 = unsafeCoerce (Coercion @Int @Int)

_test :: IO ()
_test = case archWS of
  A32 -> print (coerce (32 :: Word32) :: Word)
  A64 -> print (coerce (64 :: Word64) :: Word)
  UNK -> putStrLn "unknown"

-- $> _test

<tomsmeding> is there some way I can obtain a Coercible Int Int64? I'm fine if it's in a Maybe that is Nothing whenever this is not a 64-bit system or something
...
<Leary> tomsmeding: Only by cheating egregiously: https://gist.github.com/LSLeary/91103a2fbb35d1c908802fa81d82c110
<Leary> Worse, since GHC can actually see the declarations for all types involved, it knows the Coercible instances are bogus and raises all kinds of warnings ... not sure if that will cause issues in practice.
<tomsmeding> Leary: right -- I tried something like this too, and got the same warnings
<Leary> I mean, it considers the (useful) RHSs of archWS as unreachable, so it's free to compile them away. _test works in the REPL, but might segfault in actual use.
<tomsmeding> beautiful!
<tomsmeding> If it compiles, it works.
<Leary> tomsmeding: Looking at the core under optimisation, it does compile just fine on my GHC 9.10. But I don't see why a future GHC could not choose to treat it as: archWS = case wordSize of { 32 -> case unsafeWord32 of {}; 64 -> case unsafeWord64 of {}; _ -> UNK }, producing core archWS = case patError "ArchWS.hs:20:66-88|case"# of {}.
<tomsmeding> yes
<tomsmeding> we'd need some kind of guarantee from GHC that conjuring up custom Coercible evidence is okay and respected by GHC, and there is no such guarantee currently, I think
<tomsmeding> especially in the context of it being explicitly disallowed to write manual instances for Coercible