| Is this intentional? Yes, it's absolutely intentional.
Consider this Core defn f :: forall a b. (a ~# b) -> Int f = /\a b. \(g :: a ~# b). error "urk" Now is `seq f True` equal to True, or to (error "urk"). Definitely the former. So we cannot and must not discard coercion lambda. However, a coercion is represented by a zero-bit value, and takes no space. Simon | -----Original Message----- | From: ghc-devs <ghc-devs-boun...@haskell.org> On Behalf Of Ömer Sinan | Agacan | Sent: 06 October 2019 10:28 | To: ghc-devs <ghc-devs@haskell.org> | Subject: Should coercion binders (arguments or binders in patterns) be | TyVars? | | 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 | https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.has | kell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc- | devs&data=02%7C01%7Csimonpj%40microsoft.com%7Cf7f3feaf26b4452c1e8e08d | 74a3f92f6%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637059509215789548 | &sdata=T9iolaftOD1ncWw1JICW1UJU1X8pyCivNyB7enTS4X8%3D&reserved=0 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs