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:
-
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). ...
-
GHC refuses to promote any data constructor with a
=>
in its user-written type. -
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 offTyConPiTyBinder
. But also clarify; asNote [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 inmkGADTVars
-
Rework
Note [DataCon user type variable binders]
in DataCon -
Special treatment of equalities in
tcInstInvisibleTyBinder
. This kills offget_eq_tys_maybe
,mkHEqBoxTy
, andmkEqBoxTy
. -
Related tickets