Unneeded unsafe coercions preserved
!1869 (closed) introduced case matches on UnsafeEquality
terms to improve safety of unsafeCoerce
in certain contexts. Unfortunately, those matches sometimes remain when they're not needed. For example, consider the case where we want to imitate the GADT
data AsUnitLoop a b c where
UL :: !a -> AsUnitLoop a () ()
using a newtype
and a pattern synonym for a more compact representation (this is real). We can write
newtype AsUnitLoop a b c = UnsafeUL a
{-# COMPLETE UL #-}
data SafeUnitLoop a b c where
SafeUnitLoop :: !a -> SafeUnitLoop a () ()
mkSafeUnitLoop :: AsUnitLoop a b c -> SafeUnitLoop a b c
mkSafeUnitLoop (UnsafeUL a) = unsafeCoerce (SafeUnitLoop a)
pattern UL :: forall a b c. () => (b ~ (), c ~ ()) => a -> AsUnitLoop a b c
pattern UL a <- (mkSafeUnitLoop -> SafeUnitLoop a)
where
UL a = UnsafeUL a
Now suppose we want to extract the value from an AsUnitLoop
but aren't interested in the type refinement:
getUL :: AsUnitLoop a b c -> a
getUL (UL a) = a
Before 9.0.1, getUL
would (one way or another) be compiled to completely clean code, with no unsafe coercions or case
matches in sight. Now, it gets an unfolding like this:
-- RHS size: {terms: 8, types: 42, coercions: 4, joins: 0/0}
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= \ (@a_a1MV)
(@b_a1MW)
(@c_a1MX)
(ds_d2MW [Occ=Once1] :: AsUnitLoop a_a1MV b_a1MW c_a1MX) ->
case unsafeEqualityProof
@(*)
@(SafeUnitLoop a_a1MV () ())
@(SafeUnitLoop a_a1MV b_a1MW c_a1MX)
of
{ UnsafeRefl co_a2MR ->
ds_d2MW
`cast` (Control.Monad.Logic.Sequence.AsUnitLoop.N:AsUnitLoop[0]
<a_a1MV>_R <b_a1MW>_P <c_a1MX>_P
:: AsUnitLoop a_a1MV b_a1MW c_a1MX ~R# a_a1MV)
}}]
Presumably, the extra size may affect inlining decisions down the line, and the restrictions around the magical case
match could affect other optimizations.
Would it be possible to recognize when the equality produced by matching on unsafeEqualityProof
just isn't needed anymore, and throw the mess away? This would be the case when either:
- The surrounding context provides the (necessary part of the) equality.
- The case branch expression doesn't demand the equality.