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