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

[Ö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