Should coercion binders (arguments or binders in patterns) be TyVars?

[Sebastian Graf]

Hi Ömer,

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.

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.

Cheers,
Sebastian

Am So., 6. Okt. 2019 um 10:28 Uhr schrieb Ömer Sinan Ağacan <
omeragacan at gmail.com>:

> 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
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20191006/49da9ae3/attachment.html>