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

...

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.

To elaborate, for coercions that have a meaning in runtime I think we use primops, type coercions are not used for this purpose. E.g. for Int to Double coercion, if you really mean boxed Ints and Doubles then you can simply treat Int as Double in runtime (and enjoy the segfaults or worse), if you mean Int# to Double# then you use a primop like int2Double# which does `fild` if necessary. Ömer Ömer Sinan Ağacan , 6 Eki 2019 Paz, 12:55 tarihinde şunu yazdı:

...

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 , 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 :

...

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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs