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

[Richard Eisenberg]

And just to close the loop: the more general coercions that Sebastian has talked about would have computational content, but these are well beyond what GHC supports at the moment (and there are no plans to move in that direction).

Richard

> On Oct 6, 2019, at 10:38 PM, Simon Peyton Jones via ghc-devs <ghc-devs at haskell.org> wrote:
> 
> | 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-bounces at haskell.org> On Behalf Of Ömer Sinan
> | Agacan
> | Sent: 06 October 2019 10:28
> | To: ghc-devs <ghc-devs at 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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs