<div dir="ltr"><div>Hi Ömer,</div><div><br></div><div>I'm not sure if there's a case in GHC (yet, because newtype coercions are zero-cost), but coercions in general (as introduced for example in Types and Programming Languages) can carry computational content and thus can't be erased.</div><div><br></div><div>Think of a hypothetical coercion `co :: Int ~ Double`; applying that coercion as in `x |> co` to `x :: Int` would need to `fild` (load the integer in a floating point register) at run-time, so you can't erase it. The fact that we can for newtypes is because `coerce` is basically just the `id` function at runtime.</div><div><br></div><div>Cheers,<br></div><div>Sebastian<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am So., 6. Okt. 2019 um 10:28 Uhr schrieb Ömer Sinan Ağacan <<a href="mailto:omeragacan@gmail.com">omeragacan@gmail.com</a>>:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi,<br>
<br>
I just realized that coercion binders are currently Ids and not TyVars (unlike<br>
other type arguments). This means that we don't drop coercion binders in<br>
CoreToStg. Example:<br>
<br>
    {-# LANGUAGE ScopedTypeVariables, TypeOperators, PolyKinds, GADTs,<br>
       TypeApplications, MagicHash #-}<br>
<br>
    module UnsafeCoerce where<br>
<br>
    import Data.Type.Equality ((:~:)(..))<br>
    import GHC.Prim<br>
    import GHC.Types<br>
<br>
    unsafeEqualityProof :: forall k (a :: k) (b :: k) . a :~: b<br>
    unsafeEqualityProof = error "unsafeEqualityProof evaluated"<br>
<br>
    unsafeCoerce :: forall a b . a -> b<br>
    unsafeCoerce x = case unsafeEqualityProof @_ @a @b of Refl -> x<br>
<br>
If I build this with -ddump-stg this is what I get for `unsafeCoerce`:<br>
<br>
    UnsafeCoerce.unsafeCoerce :: forall a b. a -> b<br>
    [GblId, Arity=1, Unf=OtherCon []] =<br>
        [] \r [x_s2jn]<br>
            case UnsafeCoerce.unsafeEqualityProof of {<br>
              Data.Type.Equality.Refl co_a2fd -> x_s2jn;<br>
            };<br>
<br>
See the binder in `Refl` pattern.<br>
<br>
Unarise drops this binder because it's a "void" argument (doesn't have a runtime<br>
representation), but still it's a bit weird that we drop types but not coercions<br>
in CoreToStg.<br>
<br>
Is this intentional?<br>
<br>
Ömer<br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>