Hi, I just realized that coercion binders are currently Ids and not TyVars (unlike other type arguments). This means that we don't drop coercion binders in CoreToStg. Example: {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs, TypeApplications, MagicHash #-} module UnsafeCoerce where import Data.Type.Equality ((:~:)(..)) import GHC.Prim import GHC.Types unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b unsafeEqualityProof = error "unsafeEqualityProof evaluated" unsafeCoerce :: forall a b . a -> b unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x If I build this with -ddump-stg this is what I get for `unsafeCoerce`: UnsafeCoerce.unsafeCoerce :: forall a b. a -> b [GblId, Arity=1, Unf=OtherCon []] = [] \r [x_s2jn] case UnsafeCoerce.unsafeEqualityProof of { Data.Type.Equality.Refl co_a2fd -> x_s2jn; }; See the binder in `Refl` pattern. Unarise drops this binder because it's a "void" argument (doesn't have a runtime representation), but still it's a bit weird that we drop types but not coercions in CoreToStg. Is this intentional? Ömer