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

[Simon Peyton Jones]

| 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