Remove equalities constraints from kinds

GHC proposal

This ticket is the subject of GHC Proposal #547

Remove equalities from kinds

After several long discussions, Richard and I have decided that we can remove from GHC the ability for kinds that have equality constraints. For example (saks007):

type family F a where { F Type = True; F _ = False }
type family G a where { G Type = False; G _ = True }

type X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type
data X a b where
  MkX :: X Integer Maybe

Why do we allow such things? Note [Constraints in kinds] in GHC.Core.TyCo.Rep is the place where we describe them in some detail. It says

    Do we allow a type constructor to have a kind like
       S :: Eq a => a -> Type
    No, we do not.  ...blah...

    But we admit one exception: equality.  We /do/ allow, say,
       MkT :: (a ~ b) => a -> b -> Type a b

    Why?  Because we can, without much difficulty.

However the "without much difficulty" turns out to be a lie. It has cost us many hours of conversation, much drafting of Notes, and we kept finding new gotchas. The killer was this: suppose we have

   type T :: forall k. (F k ~ True) => k -> Type

then the innocuous type signature

   f :: T a

is rejected. It would have to elaborate to

   f :: forall k (a :: k) (c :: F k ~ True). T @k @c a

but GHC's kind inference for type signatures never quantifies over coercion variables. This could be fixed by elaborating kind inference, but that is a heavy investment given that we have no compelling application of this feature. Brain cells are a scarce resource; we must spend them wisely.

We thus propose:

1. GHC rejects any user-written kind with a => in it. For example, in these places:

   • type T :: kind
   • data T :: kind
   • x :: forall (a :: kind). ...

2. GHC refuses to promote any data constructor with a => in its user-written type.

3. Revise Section 6.4.10.7 of the manual to reflect these changes.

Red herring 1: Point (2) does not change the behavior of proper GADT constructors, like data T a where MkT :: T Bool. The promoted 'MkT will have type T Bool, just as it always has. No constraints here. This is because we do not do a worker transformation for promoted data constructors.

Red herring 2: We do still allow quantification over coercion variables. See Note [When we quantify over a coercion variable] in GHC.Core.TyCo.Rep. It's a related matter, but not the same! See also #15710, which is about accepting types quantified over coercions in source Haskell. With #15710, we would then be able to accept f :: T a as above, and equality constraints in kinds become more compelling. But there's no technical dependency between the feature under discussion here and #15710.

Checklist of things to remove

• Kill off Note [Constraints in kinds] in GHC.Core.TyCo.Rep Check for all references to this Note!

• Simplify the AnonTCB constructor (see the "only reason") in Note [Constraints in kinds]

• Think about Note [Promoted GADT data constructors] in GHC.Core.TyCon, and maybe kill off TyConPiTyBinder. But also clarify; as Note [Promoted data constructors] (same module) says, we promote GADT data constructors with their wrapper type; no equalities involved. So they should be absolutely fine.

• Remove isConstraintLikeKind magic in mkGADTVars

• Rework Note [DataCon user type variable binders] in DataCon

• Special treatment of equalities in tcInstInvisibleTyBinder. This kills off get_eq_tys_maybe, mkHEqBoxTy, and mkEqBoxTy.

• Related tickets

  • #12102 (closed)