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

[Ömer Sinan Ağacan]

> 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.

But they're already erased! They don't have a runtime representation and the
unarise pass eliminates coercion values and binders. See the last paragraph in
my original email.

> 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.

Do we even support such coercions? I think a `co :: Int ~ Double` can only be an
unsafe coercion, which are basically no-op in runtime, so again they can be
erased.

Let me know if I'm mistaken.

Ömer

Sebastian Graf <sgraf1337 at gmail.com>, 6 Eki 2019 Paz, 12:50 tarihinde
şunu yazdı:
>
> 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