Unsafer unsafeCoerce.

With GHC-9.0 unsafeCoerce change it seems there is no way to make coercions go away.

{-# LANGUAGE TemplateHaskell #-}
module UC where

import Test.Inspection

import GHC.Exts (Any)
import Unsafe.Coerce (unsafeCoerce)

fromAny :: Any -> Int
fromAny = unsafeCoerce

toAny :: Int -> Any
toAny = unsafeCoerce

weirdId :: Int -> Int
weirdId = fromAny . toAny

normalId :: Int -> Int
normalId = \x -> x

inspect $ 'weirdId === 'normalId

fails with

[1 of 1] Compiling UC               ( src/UC.hs, /code/mess/uc/dist-newstyle/build/x86_64-linux/ghc-9.0.1/uc-0.1.0.0/build/UC.o, /code/mess/uc/dist-newstyle/build/x86_64-linux/ghc-9.0.1/uc-0.1.0.0/build/UC.dyn_o )
src/UC.hs:21:1: weirdId === normalId failed:
    LHS:
        weirdId :: Int -> Int
        [LclIdX,
         Arity=1,
         Str=<S,1*U>,
         Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
                 WorkFree=True, Expandable=True,
                 Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)
                 Tmpl= \ (x [Occ=Once1] :: Int) ->
                         case unsafeEqualityProof @(*) @Any @Int of { UnsafeRefl co ->
                         case unsafeEqualityProof @(*) @Int @Any of { UnsafeRefl co -> x }
                         }}]
        weirdId
          = \ (x [Dmd=<S,1*U>] :: Int) ->
              case unsafeEqualityProof @(*) @Any @Int of
              { UnsafeRefl co [Dmd=<L,A>] ->
              case unsafeEqualityProof @(*) @Int @Any of
              { UnsafeRefl co [Dmd=<L,A>] ->
              x
              }
              }
        
    RHS:
        normalId :: Int -> Int
        [LclIdX,
         Arity=1,
         Str=<S,1*U>,
         Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
                 WorkFree=True, Expandable=True,
                 Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)
                 Tmpl= \ (x [Occ=Once1] :: Int) -> x}]
        normalId = \ (x [Dmd=<S,1*U>] :: Int) -> x
        

src/UC.hs: error:
    inspection testing unsuccessful
         unexpected failures: 1

I think this is a bug. I'd expect

\x -> case unsafeEqualityProof of
        UnsafeRefl co1 -> case unsafeEqualityProof of
          UnsafeRefl co2 -> x

to simplify to

\x -> x

as we know that unsafeEqualityProof never diverges.