summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRichard Eisenberg <reisenberg@janestreet.com>2022-11-10 17:36:22 -0500
committerMatthew Pickering <matthewtpickering@gmail.com>2022-12-24 17:34:19 +0000
commit3c3060e4645b12595b187e7dbaa758e8adda15e0 (patch)
tree31209d21cf03de1552fcbad677ea7940fa481da4
parent6d62f6bfbb5a86131e7cbc30993f3fa510d8b3ab (diff)
downloadhaskell-3c3060e4645b12595b187e7dbaa758e8adda15e0.tar.gz
Drop support for kind constraints.wip/p547
This implements proposal 547 and closes ticket #22298. See the proposal and ticket for motivation. Compiler perf improves a bit Metrics: compile_time/bytes allocated ------------------------------------- CoOpt_Singletons(normal) -2.4% GOOD T12545(normal) +1.0% T13035(normal) -13.5% GOOD T18478(normal) +0.9% T9872d(normal) -2.2% GOOD geo. mean -0.2% minimum -13.5% maximum +1.0% Metric Decrease: CoOpt_Singletons T13035 T9872d
-rw-r--r--compiler/GHC/Core/DataCon.hs64
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs107
-rw-r--r--compiler/GHC/Core/TyCon.hs93
-rw-r--r--compiler/GHC/Core/Type.hs16
-rw-r--r--compiler/GHC/CoreToIface.hs9
-rw-r--r--compiler/GHC/Iface/Type.hs9
-rw-r--r--compiler/GHC/Rename/HsType.hs44
-rw-r--r--compiler/GHC/Rename/Module.hs9
-rw-r--r--compiler/GHC/Tc/Errors/Ppr.hs7
-rw-r--r--compiler/GHC/Tc/Errors/Types.hs36
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs34
-rw-r--r--compiler/GHC/Tc/Solver/Rewrite.hs4
-rw-r--r--compiler/GHC/Tc/TyCl.hs3
-rw-r--r--compiler/GHC/Tc/Utils/Instantiate.hs66
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs4
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs-boot1
-rw-r--r--compiler/GHC/Tc/Validity.hs30
-rw-r--r--compiler/GHC/Types/Var.hs4
-rw-r--r--docs/users_guide/exts/data_kinds.rst36
-rw-r--r--testsuite/tests/dependent/should_compile/all.T1
-rw-r--r--testsuite/tests/dependent/should_fail/T13780a.stderr9
-rw-r--r--testsuite/tests/dependent/should_fail/T14845_compile.hs (renamed from testsuite/tests/dependent/should_compile/T14845_compile.hs)0
-rw-r--r--testsuite/tests/dependent/should_fail/T14845_compile.stderr7
-rw-r--r--testsuite/tests/dependent/should_fail/all.T1
-rw-r--r--testsuite/tests/polykinds/T16902.stderr11
-rw-r--r--testsuite/tests/polykinds/T18522-ppr.script4
-rw-r--r--testsuite/tests/polykinds/T18522-ppr.stdout2
-rw-r--r--testsuite/tests/saks/should_compile/all.T1
-rw-r--r--testsuite/tests/saks/should_compile/saks007.hs40
-rw-r--r--testsuite/tests/saks/should_fail/T16758.hs14
-rw-r--r--testsuite/tests/saks/should_fail/all.T1
-rw-r--r--testsuite/tests/saks/should_fail/saks007_fail.stderr13
-rw-r--r--testsuite/tests/typecheck/should_compile/T15141.hs35
-rw-r--r--testsuite/tests/typecheck/should_compile/T17021a.hs15
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T2
-rw-r--r--testsuite/tests/typecheck/should_fail/T12102.stderr6
-rw-r--r--testsuite/tests/typecheck/should_fail/T12102b.hs21
-rw-r--r--testsuite/tests/typecheck/should_fail/T13871.hs (renamed from testsuite/tests/typecheck/should_compile/T13871.hs)0
-rw-r--r--testsuite/tests/typecheck/should_fail/T13871.stderr7
-rw-r--r--testsuite/tests/typecheck/should_fail/T15862.hs6
-rw-r--r--testsuite/tests/typecheck/should_fail/all.T4
41 files changed, 156 insertions, 620 deletions
diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index e3d6331195..1b9a4a1815 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -614,7 +614,7 @@ A DataCon has two different sets of type variables:
(that is, they are TyVars/TyCoVars instead of ForAllTyBinders).
Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinders; but they may differ
-for three reasons, coming next:
+for two reasons, coming next:
--- Reason (R1): Order of quantification in GADT syntax ---
@@ -703,55 +703,6 @@ Putting this all together, all variables used on the left-hand side of an
equation in the dcEqSpec will be in dcUnivTyVars but *not* in
dcUserTyVarBinders.
---- Reason (R3): Kind equalities may have been solved ---
-
-Consider now this case:
-
- type family F a where
- F Type = False
- F _ = True
- type T :: forall k. (F k ~ True) => k -> k -> Type
- data T a b where
- MkT :: T Maybe List
-
-The constraint F k ~ True tells us that T does not want to be indexed by, say,
-Int. Now let's consider the Core types involved:
-
- axiom for F: axF[0] :: F Type ~ False
- axF[1] :: forall a. F a ~ True (a must be apart from Type)
- tycon: T :: forall k. (F k ~ True) -> k -> k -> Type
- wrapper: MkT :: T @(Type -> Type) @(Eq# (axF[1] (Type -> Type)) Maybe List
- worker: MkT :: forall k (c :: F k ~ True) (a :: k) (b :: k).
- (k ~# (Type -> Type), a ~# Maybe, b ~# List) =>
- T @k @c a b
-
-The key observation here is that the worker quantifies over c, while the wrapper
-does not. The worker *must* quantify over c, because c is a universal variable,
-and the result of the worker must be the type constructor applied to a sequence
-of plain type variables. But the wrapper certainly does not need to quantify over
-any evidence that F (Type -> Type) ~ True, as no variables are needed there.
-
-(Aside: the c here is a regular type variable, *not* a coercion variable. This
-is because F k ~ True is a *lifted* equality, not the unlifted ~#. This is why
-we see Eq# in the type of the wrapper: Eq# boxes the unlifted ~# to become a
-lifted ~. See also Note [The equality types story] in GHC.Builtin.Types.Prim about
-Eq# and Note [Constraints in kinds] in GHC.Core.TyCo.Rep about having this constraint
-in the first place.)
-
-In this case, we'll have these fields of the DataCon:
-
- dcUserTyVarBinders = [] -- the wrapper quantifies over nothing
- dcUnivTyVars = [k, c, a, b]
- dcExTyCoVars = [] -- no existentials here, but a different constructor might have
- dcEqSpec = [k ~# (Type -> Type), a ~# Maybe, b ~# List]
-
-Note that c is in the dcUserTyVars, but mentioned neither in the dcUserTyVarBinders nor
-in the dcEqSpec. We thus have Reason (R3): a variable might be missing from the
-dcUserTyVarBinders if its type's kind is Constraint.
-
-(At one point, we thought that the dcEqSpec would have to be non-empty. But that
-wouldn't account for silly cases like type T :: (True ~ True) => Type.)
-
--- End of Reasons ---
INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders
@@ -1230,11 +1181,9 @@ mkDataCon name declared_infix prom_info
-- fresh_names: make sure that the "anonymous" tyvars don't
-- clash in name or unique with the universal/existential ones.
-- Tiresome! And unnecessary because these tyvars are never looked at
- prom_theta_bndrs = [ mkInvisAnonTyConBinder (mkTyVar n t)
- {- Invisible -} | (n,t) <- fresh_names `zip` theta ]
prom_arg_bndrs = [ mkAnonTyConBinder (mkTyVar n t)
{- Visible -} | (n,t) <- dropList theta fresh_names `zip` map scaledThing orig_arg_tys ]
- prom_bndrs = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs
+ prom_bndrs = prom_tv_bndrs ++ prom_arg_bndrs
prom_res_kind = orig_res_ty
promoted = mkPromotedDataCon con name prom_info prom_bndrs
prom_res_kind roles rep_info
@@ -1861,20 +1810,15 @@ checkDataConTyVars dc@(MkData { dcUnivTyVars = univ_tvs
, dcExTyCoVars = ex_tvs
, dcEqSpec = eq_spec })
-- use of sets here: (R1) from the Note
- = mkUnVarSet depleted_worker_vars == mkUnVarSet depleted_wrapper_vars &&
+ = mkUnVarSet depleted_worker_vars == mkUnVarSet wrapper_vars &&
all (not . is_eq_spec_var) wrapper_vars
where
- is_constraint_var v = typeTypeOrConstraint (tyVarKind v) == ConstraintLike
- -- implements (R3) from the Note
-
worker_vars = univ_tvs ++ ex_tvs
eq_spec_tvs = mkUnVarSet (map eqSpecTyVar eq_spec)
is_eq_spec_var = (`elemUnVarSet` eq_spec_tvs) -- (R2) from the Note
- depleted_worker_vars = filterOut (is_eq_spec_var <||> is_constraint_var)
- worker_vars
+ depleted_worker_vars = filterOut is_eq_spec_var worker_vars
wrapper_vars = dataConUserTyVars dc
- depleted_wrapper_vars = filterOut is_constraint_var wrapper_vars
dataConUserTyVarsNeedWrapper :: DataCon -> Bool
-- Check whether the worker and wapper have the same type variables
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 4247e9f8dd..c90ff3b3c9 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -325,113 +325,6 @@ Because the tyvar form above includes r in its result, we must
be careful not to let any variables escape -- thus the last premise
of the rule above.
-Note [Constraints in kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Do we allow a type constructor to have a kind like
- S :: Eq a => a -> Type
-
-No, we do not. Doing so would mean would need a TyConApp like
- S @k @(d :: Eq k) (ty :: k)
- and we have no way to build, or decompose, evidence like
- (d :: Eq k) at the type level.
-
-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. Moreover
-we can promote a GADT data constructor (see TyCon
-Note [Promoted data constructors]), like
- data GT a b where
- MkGT : a -> a -> GT a a
-so programmers might reasonably expect to be able to
-promote MkT as well.
-
-How does this work?
-
-* In GHC.Tc.Validity.checkConstraintsOK we reject kinds that
- have constraints other than (a~b) and (a~~b).
-
-* In Inst.tcInstInvisibleTyBinder we instantiate a call
- of MkT by emitting
- [W] co :: alpha ~# beta
- and producing the elaborated term
- MkT @alpha @beta (Eq# alpha beta co)
- We don't generate a boxed "Wanted"; we generate only a
- regular old /unboxed/ primitive-equality Wanted, and build
- the box on the spot.
-
-* How can we get such a MkT? By promoting a GADT-style data
- constructor, written with an explicit equality constraint.
- data T a b where
- MkT :: (a~b) => a -> b -> T a b
- See DataCon.mkPromotedDataCon
- and Note [Promoted data constructors] in GHC.Core.TyCon
-
-* We support both homogeneous (~) and heterogeneous (~~)
- equality. (See Note [The equality types story]
- in GHC.Builtin.Types.Prim for a primer on these equality types.)
-
-* How do we prevent a MkT having an illegal constraint like
- Eq a? We check for this at use-sites; see GHC.Tc.Gen.HsType.tcTyVar,
- specifically dc_theta_illegal_constraint.
-
-* Notice that nothing special happens if
- K :: (a ~# b) => blah
- because (a ~# b) is not a predicate type, and is never
- implicitly instantiated. (Mind you, it's not clear how you
- could creates a type constructor with such a kind.) See
- Note [Types for coercions, predicates, and evidence]
-
-* The existence of promoted MkT with an equality-constraint
- argument is the (only) reason that the AnonTCB constructor
- of TyConBndrVis carries an FunTyFlag.
- For example, when we promote the data constructor
- MkT :: forall a b. (a~b) => a -> b -> T a b
- we get a PromotedDataCon with tyConBinders
- Bndr (a :: Type) (NamedTCB Inferred)
- Bndr (b :: Type) (NamedTCB Inferred)
- Bndr (_ :: a ~ b) (AnonTCB FTF_C_T)
- Bndr (_ :: a) (AnonTCB FTF_T_T))
- Bndr (_ :: b) (AnonTCB FTF_T_T))
-
-* One might reasonably wonder who *unpacks* these boxes once they are
- made. After all, there is no type-level `case` construct. The
- surprising answer is that no one ever does. Instead, if a GADT
- constructor is used on the left-hand side of a type family equation,
- that occurrence forces GHC to unify the types in question. For
- example:
-
- data G a where
- MkG :: G Bool
-
- type family F (x :: G a) :: a where
- F MkG = False
-
- When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
- unify F's implicit parameter `a` with Bool. This succeeds, making the equation
-
- F Bool (MkG @Bool <Bool>) = False
-
- Note that we never need unpack the coercion. This is because type
- family equations are *not* parametric in their kind variables. That
- is, we could have just said
-
- type family H (x :: G a) :: a where
- H _ = False
-
- The presence of False on the RHS also forces `a` to become Bool,
- giving us
-
- H Bool _ = False
-
- The fact that any of this works stems from the lack of phase
- separation between types and kinds (unlike the very present phase
- separation between terms and types).
-
- Once we have the ability to pattern-match on types below top-level,
- this will no longer cut it, but it seems fine for now.
-
-
Note [Arguments to type constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Because of kind polymorphism, in addition to type application we now
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs
index f08d18ffc2..0311ba32bd 100644
--- a/compiler/GHC/Core/TyCon.hs
+++ b/compiler/GHC/Core/TyCon.hs
@@ -20,10 +20,10 @@ module GHC.Core.TyCon(
PromDataConInfo(..), TyConFlavour(..),
-- * TyConBinder
- TyConBinder, TyConBndrVis(..), TyConPiTyBinder,
+ TyConBinder, TyConBndrVis(..),
mkNamedTyConBinder, mkNamedTyConBinders,
mkRequiredTyConBinder,
- mkAnonTyConBinder, mkAnonTyConBinders, mkInvisAnonTyConBinder,
+ mkAnonTyConBinder, mkAnonTyConBinders,
tyConBinderForAllTyFlag, tyConBndrVisForAllTyFlag, isNamedTyConBinder,
isVisibleTyConBinder, isInvisibleTyConBinder, isVisibleTcbVis,
@@ -445,38 +445,29 @@ See #19367.
************************************************************************
* *
- TyConBinder, TyConPiTyBinder
+ TyConBinder
* *
************************************************************************
-}
type TyConBinder = VarBndr TyVar TyConBndrVis
-type TyConPiTyBinder = VarBndr TyCoVar TyConBndrVis
- -- Only PromotedDataCon has TyConPiTyBinders
- -- See Note [Promoted GADT data constructors]
data TyConBndrVis
- = NamedTCB ForAllTyFlag
- | AnonTCB FunTyFlag
+ = NamedTCB ForAllTyFlag -- ^ A named, forall-bound variable (invisible or not)
+ | AnonTCB -- ^ an ordinary, visible type argument
instance Outputable TyConBndrVis where
ppr (NamedTCB flag) = ppr flag
- ppr (AnonTCB af) = ppr af
+ ppr AnonTCB = text "AnonTCB"
mkAnonTyConBinder :: TyVar -> TyConBinder
-- Make a visible anonymous TyCon binder
mkAnonTyConBinder tv = assert (isTyVar tv) $
- Bndr tv (AnonTCB visArgTypeLike)
+ Bndr tv AnonTCB
mkAnonTyConBinders :: [TyVar] -> [TyConBinder]
mkAnonTyConBinders tvs = map mkAnonTyConBinder tvs
-mkInvisAnonTyConBinder :: TyVar -> TyConBinder
--- Make an /invisible/ anonymous TyCon binder
--- Not used much
-mkInvisAnonTyConBinder tv = assert (isTyVar tv) $
- Bndr tv (AnonTCB invisArgTypeLike)
-
mkNamedTyConBinder :: ForAllTyFlag -> TyVar -> TyConBinder
-- The odd argument order supports currying
mkNamedTyConBinder vis tv = assert (isTyVar tv) $
@@ -499,10 +490,8 @@ tyConBinderForAllTyFlag :: TyConBinder -> ForAllTyFlag
tyConBinderForAllTyFlag (Bndr _ vis) = tyConBndrVisForAllTyFlag vis
tyConBndrVisForAllTyFlag :: TyConBndrVis -> ForAllTyFlag
-tyConBndrVisForAllTyFlag (NamedTCB vis) = vis
-tyConBndrVisForAllTyFlag (AnonTCB af) -- See Note [AnonTCB with constraint arg]
- | isVisibleFunArg af = Required
- | otherwise = Inferred
+tyConBndrVisForAllTyFlag (NamedTCB vis) = vis
+tyConBndrVisForAllTyFlag AnonTCB = Required
isNamedTyConBinder :: TyConBinder -> Bool
-- Identifies kind variables
@@ -517,7 +506,7 @@ isVisibleTyConBinder (Bndr _ tcb_vis) = isVisibleTcbVis tcb_vis
isVisibleTcbVis :: TyConBndrVis -> Bool
isVisibleTcbVis (NamedTCB vis) = isVisibleForAllTyFlag vis
-isVisibleTcbVis (AnonTCB af) = isVisibleFunArg af
+isVisibleTcbVis AnonTCB = True
isInvisibleTyConBinder :: VarBndr tv TyConBndrVis -> Bool
-- Works for IfaceTyConBinder too
@@ -530,7 +519,7 @@ mkTyConKind bndrs res_kind = foldr mk res_kind bndrs
where
mk :: TyConBinder -> Kind -> Kind
mk (Bndr tv (NamedTCB vis)) k = mkForAllTy (Bndr tv vis) k
- mk (Bndr tv (AnonTCB af)) k = mkNakedFunTy af (varType tv) k
+ mk (Bndr tv AnonTCB) k = mkNakedFunTy FTF_T_T (varType tv) k
-- mkNakedFunTy: see Note [Naked FunTy] in GHC.Builtin.Types
-- | (mkTyConTy tc) returns (TyConApp tc [])
@@ -549,9 +538,7 @@ tyConInvisTVBinders tc_bndrs
mk_binder (Bndr tv tc_vis) = mkTyVarBinder vis tv
where
vis = case tc_vis of
- AnonTCB af -- Note [AnonTCB with constraint arg]
- | isInvisibleFunArg af -> InferredSpec
- | otherwise -> SpecifiedSpec
+ AnonTCB -> SpecifiedSpec
NamedTCB Required -> SpecifiedSpec
NamedTCB (Invisible vis) -> vis
@@ -561,35 +548,7 @@ tyConVisibleTyVars tc
= [ tv | Bndr tv vis <- tyConBinders tc
, isVisibleTcbVis vis ]
-{- Note [AnonTCB with constraint arg]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's pretty rare to have an (AnonTCB af) binder with af=FTF_C_T or FTF_C_C.
-The only way it can occur is through equality constraints in kinds. These
-can arise in one of two ways:
-
-* In a PromotedDataCon whose kind has an equality constraint:
-
- 'MkT :: forall a b. (a~b) => blah
-
- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and
- Note [Promoted data constructors] in this module.
-
-* In a data type whose kind has an equality constraint, as in the
- following example from #12102:
-
- data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type
-
-When mapping an (AnonTCB FTF_C_x) to an ForAllTyFlag, in
-tyConBndrVisForAllTyFlag, we use "Inferred" to mean "the user cannot
-specify this arguments, even with visible type/kind application;
-instead the type checker must fill it in.
-
-We map (AnonTCB FTF_T_x) to Required, of course: the user must
-provide it. It would be utterly wrong to do this for constraint
-arguments, which is why AnonTCB must have the FunTyFlag in
-the first place.
-
-Note [Building TyVarBinders from TyConBinders]
+{- Note [Building TyVarBinders from TyConBinders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We sometimes need to build the quantified type of a value from
the TyConBinders of a type or class. For that we need not
@@ -645,7 +604,7 @@ in GHC.Core.TyCo.Rep), so we change it to Specified when making MkT's PiTyBinder
{- Note [The binders/kind/arity fields of a TyCon]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All TyCons have this group of fields
- tyConBinders :: [TyConBinder/TyConPiTyBinder]
+ tyConBinders :: [TyConBinder]
tyConResKind :: Kind
tyConTyVars :: [TyVar] -- Cached = binderVars tyConBinders
-- NB: Currently (Aug 2018), TyCons that own this
@@ -656,7 +615,7 @@ All TyCons have this group of fields
They fit together like so:
-* tyConBinders gives the telescope of type/coercion variables on the LHS of the
+* tyConBinders gives the telescope of type variables on the LHS of the
type declaration. For example:
type App a (b :: k) = a b
@@ -673,7 +632,7 @@ They fit together like so:
* See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in GHC.Core.TyCo.Rep
for what the visibility flag means.
-* Each TyConBinder tyConBinders has a TyVar (sometimes it is TyCoVar), and
+* Each TyConBinder in tyConBinders has a TyVar, and
that TyVar may scope over some other part of the TyCon's definition. Eg
type T a = a -> a
we have
@@ -745,12 +704,12 @@ instance OutputableBndr tv => Outputable (VarBndr tv TyConBndrVis) where
ppr (Bndr v bi) = ppr bi <+> parens (pprBndr LetBind v)
instance Binary TyConBndrVis where
- put_ bh (AnonTCB af) = do { putByte bh 0; put_ bh af }
+ put_ bh AnonTCB = do { putByte bh 0 }
put_ bh (NamedTCB vis) = do { putByte bh 1; put_ bh vis }
get bh = do { h <- getByte bh
; case h of
- 0 -> do { af <- get bh; return (AnonTCB af) }
+ 0 -> return AnonTCB
_ -> do { vis <- get bh; return (NamedTCB vis) } }
@@ -915,6 +874,9 @@ data TyConDetails =
}
-- | Represents promoted data constructor.
+ -- The kind of a promoted data constructor is the *wrapper* type of
+ -- the original data constructor. This type must not have constraints
+ -- (as checked in GHC.Tc.Gen.HsType.tcTyVar).
| PromotedDataCon { -- See Note [Promoted data constructors]
dataCon :: DataCon, -- ^ Corresponding data constructor
tcRepName :: TyConRepName,
@@ -958,17 +920,6 @@ where
tcTyConScopedTyVars are used only for MonoTcTyCons, not PolyTcTyCons.
See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType.
-Note [Promoted GADT data constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Any promoted GADT data constructor will have a type with equality
-constraints in its type; e.g.
- K :: forall a b. (a ~# [b]) => a -> b -> T a
-
-So, when promoted to become a type constructor, the tyConBinders
-will include CoVars. That is why we use [TyConPiTyBinder] for the
-tyconBinders field. TyConPiTyBinder is a synonym for TyConBinder,
-but with the clue that the binder can be a CoVar not just a TyVar.
-
Note [Representation-polymorphic TyCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To check for representation-polymorphism directly in the typechecker,
@@ -1946,7 +1897,7 @@ mkFamilyTyCon name binders res_kind resVar flav parent inj
-- as the data constructor itself; when we pretty-print
-- the TyCon we add a quote; see the Outputable TyCon instance
mkPromotedDataCon :: DataCon -> Name -> TyConRepName
- -> [TyConPiTyBinder] -> Kind -> [Role]
+ -> [TyConBinder] -> Kind -> [Role]
-> PromDataConInfo -> TyCon
mkPromotedDataCon con name rep_name binders res_kind roles rep_info
= mkTyCon name binders res_kind roles $
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 76326b6c50..1ef00b0977 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1732,7 +1732,7 @@ tyConBindersPiTyBinders :: [TyConBinder] -> [PiTyBinder]
tyConBindersPiTyBinders = map to_tyb
where
to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
- to_tyb (Bndr tv (AnonTCB af)) = Anon (tymult (varType tv)) af
+ to_tyb (Bndr tv AnonTCB) = Anon (tymult (varType tv)) FTF_T_T
-- | Make a dependent forall over an 'Inferred' variable
mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
@@ -1794,7 +1794,7 @@ mkTyConBindersPreferAnon vars inner_tkvs = assert (all isTyVar vars)
= ( Bndr v (NamedTCB Required) : binders
, fvs `delVarSet` v `unionVarSet` kind_vars )
| otherwise
- = ( Bndr v (AnonTCB visArgTypeLike) : binders
+ = ( Bndr v AnonTCB : binders
, fvs `unionVarSet` kind_vars )
where
(binders, fvs) = go vs
@@ -2488,9 +2488,8 @@ Here are the key kinding rules for types
-- in GHC.Builtin.Types.Prim
torc is TYPE or CONSTRAINT
- ty : body_torc rep
- bndr_torc is Type or Constraint
- ki : bndr_torc
+ ty : torc rep
+ ki : Type
`a` is a type variable
`a` is not free in rep
(FORALL1) -----------------------
@@ -2508,10 +2507,6 @@ Here are the key kinding rules for types
Note that:
* (FORALL1) rejects (forall (a::Maybe). blah)
-* (FORALL1) accepts (forall (a :: t1~t2) blah), where the type variable
- (not coercion variable!) 'a' has a kind (t1~t2) that in turn has kind
- Constraint. See Note [Constraints in kinds] in GHC.Core.TyCo.Rep.
-
* (FORALL2) Surprise 1:
See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
@@ -2809,8 +2804,7 @@ tyConAppNeedsKindSig spec_inj_pos tc n_args
injective_vars_of_binder :: TyConBinder -> FV
injective_vars_of_binder (Bndr tv vis) =
case vis of
- AnonTCB af | isVisibleFunArg af
- -> injectiveVarsOfType False -- conservative choice
+ AnonTCB -> injectiveVarsOfType False -- conservative choice
(varType tv)
NamedTCB argf | source_of_injectivity argf
-> unitFV tv `unionFV`
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index 4194939082..98595f0403 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -81,6 +81,7 @@ import GHC.Types.Cpr ( topCprSig )
import GHC.Utils.Outputable
import GHC.Utils.Panic
+import GHC.Utils.Panic.Plain
import GHC.Utils.Misc
import Data.Maybe ( isNothing, catMaybes )
@@ -353,12 +354,8 @@ toIfaceAppArgsX fr kind ty_args
ts' = go (extendTCvSubst env tv t) res ts
go env (FunTy { ft_af = af, ft_res = res }) (t:ts)
- = IA_Arg (toIfaceTypeX fr t) argf (go env res ts)
- where
- argf | isVisibleFunArg af = Required
- | otherwise = Inferred
- -- It's rare for a kind to have a constraint argument, but it
- -- can happen. See Note [AnonTCB with constraint arg] in GHC.Core.TyCon.
+ = assert (isVisibleFunArg af)
+ IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
go env ty ts@(t1:ts1)
| not (isEmptyTCvSubst env)
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 3e41a25132..608a16af4b 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -205,7 +205,7 @@ mkIfaceTyConKind :: [IfaceTyConBinder] -> IfaceKind -> IfaceKind
mkIfaceTyConKind bndrs res_kind = foldr mk res_kind bndrs
where
mk :: IfaceTyConBinder -> IfaceKind -> IfaceKind
- mk (Bndr tv (AnonTCB af)) k = IfaceFunTy af many_ty (ifaceBndrType tv) k
+ mk (Bndr tv AnonTCB) k = IfaceFunTy FTF_T_T many_ty (ifaceBndrType tv) k
mk (Bndr tv (NamedTCB vis)) k = IfaceForAllTy (Bndr tv vis) k
ifaceForAllSpecToBndrs :: [IfaceForAllSpecBndr] -> [IfaceForAllBndr]
@@ -892,12 +892,7 @@ pprIfaceTyConBinders suppress_sig = sep . map go
go (Bndr (IfaceTvBndr bndr) vis) =
-- See Note [Pretty-printing invisible arguments]
case vis of
- AnonTCB af
- | isVisibleFunArg af -> ppr_bndr (UseBndrParens True)
- | otherwise -> char '@' <> braces (ppr_bndr (UseBndrParens False))
- -- The above case is rare. (See Note [AnonTCB with constraint arg]
- -- in GHC.Core.TyCon.)
- -- Should we print these differently?
+ AnonTCB -> ppr_bndr (UseBndrParens True)
NamedTCB Required -> ppr_bndr (UseBndrParens True)
NamedTCB Specified -> char '@' <> ppr_bndr (UseBndrParens True)
NamedTCB Inferred -> char '@' <> braces (ppr_bndr (UseBndrParens False))
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index aaaa249ba2..df53523597 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -13,7 +13,7 @@
module GHC.Rename.HsType (
-- Type related stuff
rnHsType, rnLHsType, rnLHsTypes, rnContext, rnMaybeContext,
- rnHsKind, rnLHsKind, rnLHsTypeArgs,
+ rnLHsKind, rnLHsTypeArgs,
rnHsSigType, rnHsWcType, rnHsPatSigTypeBindingVars,
HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
newTyVarNameRn,
@@ -468,35 +468,6 @@ rnImplicitTvBndrs ctx mb_assoc implicit_vs_with_dups thing_inside
{-
rnHsType is here because we call it from loadInstDecl, and I didn't
want a gratuitous knot.
-
-Note [HsQualTy in kinds]
-~~~~~~~~~~~~~~~~~~~~~~
-I was wondering whether HsQualTy could occur only at TypeLevel. But no,
-we can have a qualified type in a kind too. Here is an example:
-
- type family F a where
- F Bool = Nat
- F Nat = Type
-
- type family G a where
- G Type = Type -> Type
- G () = Nat
-
- data X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type where
- MkX :: X 'True '()
-
-See that k1 becomes Bool and k2 becomes (), so the equality is
-satisfied. If I write MkX :: X 'True 'False, compilation fails with a
-suitable message:
-
- MkX :: X 'True '()
- • Couldn't match kind ‘G Bool’ with ‘Nat’
- Expected kind: G Bool
- Actual kind: F Bool
-
-However: in a kind, the constraints in the HsQualTy must all be
-equalities; or at least, any kinds with a class constraint are
-uninhabited. See Note [Constraints in kinds] in GHC.Core.TyCo.Rep.
-}
data RnTyKiEnv
@@ -552,9 +523,6 @@ rnHsType ctxt ty = rnHsTyKi (mkTyKiEnv ctxt TypeLevel RnTypeBody) ty
rnLHsKind :: HsDocContext -> LHsKind GhcPs -> RnM (LHsKind GhcRn, FreeVars)
rnLHsKind ctxt kind = rnLHsTyKi (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
-rnHsKind :: HsDocContext -> HsKind GhcPs -> RnM (HsKind GhcRn, FreeVars)
-rnHsKind ctxt kind = rnHsTyKi (mkTyKiEnv ctxt KindLevel RnTypeBody) kind
-
-- renaming a type only, not a kind
rnLHsTypeArg :: HsDocContext -> LHsTypeArg GhcPs
-> RnM (LHsTypeArg GhcRn, FreeVars)
@@ -610,11 +578,11 @@ rnHsTyKi env ty@(HsForAllTy { hst_tele = tele, hst_body = tau })
, hst_tele = tele' , hst_body = tau' }
, fvs) } }
-rnHsTyKi env ty@(HsQualTy { hst_ctxt = lctxt, hst_body = tau })
- = do { data_kinds <- xoptM LangExt.DataKinds -- See Note [HsQualTy in kinds]
- ; when (not data_kinds && isRnKindLevel env)
- (addErr (dataKindsErr env ty))
- ; (ctxt', fvs1) <- rnTyKiContext env lctxt
+rnHsTyKi env (HsQualTy { hst_ctxt = lctxt, hst_body = tau })
+ = do { -- no need to check type vs kind level here; this is
+ -- checked in the type checker. See
+ -- Note [No constraints in kinds] in GHC.Tc.Validity
+ (ctxt', fvs1) <- rnTyKiContext env lctxt
; (tau', fvs2) <- rnLHsTyKi env tau
; return (HsQualTy { hst_xqual = noExtField, hst_ctxt = ctxt'
, hst_body = tau' }
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 97726a279c..fc6846e566 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2064,14 +2064,7 @@ preceded by `type`, with the following restrictions:
(R3) There are no strictness flags, because they don't make sense at
the type level.
-(R4) The types of the constructors contain no constraints other than
- equality constraints. (This is the same restriction imposed
- on constructors to be promoted with the DataKinds extension in
- dc_theta_illegal_constraint called from GHC.Tc.Gen.HsType.tcTyVar,
- but in that case the restriction is imposed if and when a data
- constructor is used in a type, whereas here it is imposed at
- the point of definition. See also Note [Constraints in kinds]
- in GHC.Core.TyCo.Rep.)
+(R4) The types of the constructors contain no constraints.
(R5) There are no deriving clauses.
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index d13aa6b21d..00b37709bd 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -913,9 +913,10 @@ instance Diagnostic TcRnMessage where
2 (parens reason))
where
reason = case err of
- ConstrainedDataConPE pred
+ ConstrainedDataConPE theta
-> text "it has an unpromotable context"
- <+> quotes (ppr pred)
+ <+> quotes (pprTheta theta)
+
FamDataConPE -> text "it comes from a data family instance"
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted"
@@ -3385,7 +3386,7 @@ pprHoleError ctxt (Hole { hole_ty, hole_occ}) (HoleError sort other_tvs hole_sko
2 (text "standing for" <+> quotes pp_hole_type_with_kind)
ConstraintHole ->
hang (text "Found extra-constraints wildcard standing for")
- 2 (quotes $ pprType hole_ty) -- always kind constraint
+ 2 (quotes $ pprType hole_ty) -- always kind Constraint
hole_kind = typeKind hole_ty
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 335e7c4965..f4d7d85ed1 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -3854,9 +3854,8 @@ data PromotionErr
| FamDataConPE -- Data constructor for a data family
-- See Note [AFamDataCon: not promoting data family constructors]
-- in GHC.Tc.Utils.Env.
- | ConstrainedDataConPE PredType
- -- Data constructor with a non-equality context
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
+ | ConstrainedDataConPE ThetaType -- Data constructor with a context
+ -- See Note [No constraints in kinds] in GHC.Tc.Validity
| PatSynPE -- Pattern synonyms
-- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env
@@ -3866,28 +3865,27 @@ data PromotionErr
| NoDataKindsDC -- -XDataKinds not enabled (for a datacon)
instance Outputable PromotionErr where
- ppr ClassPE = text "ClassPE"
- ppr TyConPE = text "TyConPE"
- ppr PatSynPE = text "PatSynPE"
- ppr FamDataConPE = text "FamDataConPE"
- ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
- <+> parens (ppr pred)
- ppr RecDataConPE = text "RecDataConPE"
- ppr NoDataKindsDC = text "NoDataKindsDC"
- ppr TermVariablePE = text "TermVariablePE"
+ ppr ClassPE = text "ClassPE"
+ ppr TyConPE = text "TyConPE"
+ ppr PatSynPE = text "PatSynPE"
+ ppr FamDataConPE = text "FamDataConPE"
+ ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta)
+ ppr RecDataConPE = text "RecDataConPE"
+ ppr NoDataKindsDC = text "NoDataKindsDC"
+ ppr TermVariablePE = text "TermVariablePE"
pprPECategory :: PromotionErr -> SDoc
pprPECategory = text . capitalise . peCategory
peCategory :: PromotionErr -> String
-peCategory ClassPE = "class"
-peCategory TyConPE = "type constructor"
-peCategory PatSynPE = "pattern synonym"
-peCategory FamDataConPE = "data constructor"
+peCategory ClassPE = "class"
+peCategory TyConPE = "type constructor"
+peCategory PatSynPE = "pattern synonym"
+peCategory FamDataConPE = "data constructor"
peCategory ConstrainedDataConPE{} = "data constructor"
-peCategory RecDataConPE = "data constructor"
-peCategory NoDataKindsDC = "data constructor"
-peCategory TermVariablePE = "term variable"
+peCategory RecDataConPE = "data constructor"
+peCategory NoDataKindsDC = "data constructor"
+peCategory TermVariablePE = "term variable"
-- | Stores the information to be reported in a representation-polymorphism
-- error message.
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 9d9f597db2..a0a2a51cee 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -137,7 +137,7 @@ import GHC.Data.Bag( unitBag )
import Data.Function ( on )
import Data.List.NonEmpty ( NonEmpty(..), nonEmpty )
import qualified Data.List.NonEmpty as NE
-import Data.List ( find, mapAccumL )
+import Data.List ( mapAccumL )
import Control.Monad
import Data.Tuple( swap )
@@ -1613,8 +1613,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
case ki_binder of
-- FunTy with PredTy on LHS, or ForAllTy with Inferred
- Named (Bndr _ Inferred) -> instantiate ki_binder inner_ki
- Anon _ af | isInvisibleFunArg af -> instantiate ki_binder inner_ki
+ Named (Bndr kv Inferred) -> instantiate kv inner_ki
Named (Bndr _ Specified) -> -- Visible kind application
do { traceTc "tcInferTyApps (vis kind app)"
@@ -1644,9 +1643,9 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
---------------- HsValArg: a normal argument (fun ty)
(HsValArg arg : args, Just (ki_binder, inner_ki))
-- next binder is invisible; need to instantiate it
- | isInvisiblePiTyBinder ki_binder -- FunTy with constraint on LHS;
- -- or ForAllTy with Inferred or Specified
- -> instantiate ki_binder inner_ki
+ | Named (Bndr kv flag) <- ki_binder
+ , isInvisibleForAllTyFlag flag -- ForAllTy with Inferred or Specified
+ -> instantiate kv inner_ki
-- "normal" case
| otherwise
@@ -1984,23 +1983,16 @@ tcTyVar name -- Could be a tyvar, a tycon, or a datacon
-- see #15245
promotionErr name FamDataConPE
; let (_, _, _, theta, _, _) = dataConFullSig dc
- ; traceTc "tcTyVar" (ppr dc <+> ppr theta $$ ppr (dc_theta_illegal_constraint theta))
- ; case dc_theta_illegal_constraint theta of
- Just pred -> promotionErr name $
- ConstrainedDataConPE pred
- Nothing -> pure ()
+ ; traceTc "tcTyVar" (ppr dc <+> ppr theta)
+ -- promotionErr: Note [No constraints in kinds] in GHC.Tc.Validity
+ ; unless (null theta) $
+ promotionErr name (ConstrainedDataConPE theta)
; let tc = promoteDataCon dc
; return (mkTyConApp tc [], tyConKind tc) }
APromotionErr err -> promotionErr name err
_ -> wrongThingErr "type" thing name }
- where
- -- We cannot promote a data constructor with a context that contains
- -- constraints other than equalities, so error if we find one.
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
- dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
- dc_theta_illegal_constraint = find (not . isEqPred)
{-
Note [Recursion through the kinds]
@@ -3715,9 +3707,10 @@ splitTyConKind skol_info in_scope avoid_occs kind
Nothing -> (reverse acc, substTy subst kind)
Just (Anon arg af, kind')
- -> go occs' uniqs' subst' (tcb : acc) kind'
+ -> assert (af == FTF_T_T) $
+ go occs' uniqs' subst' (tcb : acc) kind'
where
- tcb = Bndr tv (AnonTCB af)
+ tcb = Bndr tv AnonTCB
arg' = substTy subst (scaledThing arg)
name = mkInternalName uniq occ loc
tv = mkTcTyVar name arg' details
@@ -3858,7 +3851,8 @@ tcbVisibilities tc orig_args
go fun_kind subst all_args@(arg : args)
| Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
= case tcb of
- Anon _ af -> AnonTCB af : go inner_kind subst args
+ Anon _ af -> assert (af == FTF_T_T) $
+ AnonTCB : go inner_kind subst args
Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
where
subst' = extendTCvSubst subst tv arg
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 252e2aba52..6892e9853f 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -1077,7 +1077,7 @@ ty_con_binders_ty_binders' = foldr go ([], False)
where
go (Bndr tv (NamedTCB vis)) (bndrs, _)
= (Named (Bndr tv vis) : bndrs, True)
- go (Bndr tv (AnonTCB af)) (bndrs, n)
- = (Anon (tymult (tyVarKind tv)) af : bndrs, n)
+ go (Bndr tv AnonTCB) (bndrs, n)
+ = (Anon (tymult (tyVarKind tv)) FTF_T_T : bndrs, n)
{-# INLINE go #-}
{-# INLINE ty_con_binders_ty_binders' #-}
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index c5f924cea8..32c64b6c7f 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -4069,8 +4069,7 @@ mkGADTVars tmpl_tvs dc_tvs subst
tv_kind = tyVarKind t_tv
tv_kind' = substTy t_sub tv_kind
t_tv' = setTyVarKind t_tv tv_kind'
- eqs' | isConstraintLikeKind (typeKind tv_kind') = eqs
- | otherwise = (t_tv', r_ty) : eqs
+ eqs' = (t_tv', r_ty) : eqs
| otherwise
= pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index abbee42526..0b6b519028 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -43,7 +43,7 @@ import GHC.Prelude
import GHC.Driver.Session
import GHC.Driver.Env
-import GHC.Builtin.Types ( heqDataCon, eqDataCon, integerTyConName )
+import GHC.Builtin.Types ( heqDataCon, integerTyConName )
import GHC.Builtin.Names
import GHC.Hs
@@ -53,14 +53,12 @@ import GHC.Core.InstEnv
import GHC.Core.Predicate
import GHC.Core ( Expr(..), isOrphan ) -- For the Coercion constructor
import GHC.Core.Type
-import GHC.Core.Multiplicity
-import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr ( debugPprType )
import GHC.Core.Class( Class )
import GHC.Core.DataCon
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
-import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType, unifyKind )
+import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType )
import GHC.Tc.Utils.Zonk
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
@@ -386,71 +384,21 @@ tcInstInvisibleTyBindersN n ty
go n subst kind
| n > 0
- , Just (bndr, body) <- tcSplitPiTy_maybe kind
- , isInvisiblePiTyBinder bndr
- = do { (subst', arg) <- tcInstInvisibleTyBinder subst bndr
+ , Just (bndr, body) <- tcSplitForAllTyVarBinder_maybe kind
+ , isInvisibleForAllTyFlag (binderFlag bndr)
+ = do { (subst', arg) <- tcInstInvisibleTyBinder subst (binderVar bndr)
; (args, inner_ty) <- go (n-1) subst' body
; return (arg:args, inner_ty) }
| otherwise
= return ([], substTy subst kind)
-tcInstInvisibleTyBinder :: Subst -> PiTyVarBinder -> TcM (Subst, TcType)
+tcInstInvisibleTyBinder :: Subst -> TyVar -> TcM (Subst, TcType)
-- Called only to instantiate kinds, in user-written type signatures
-tcInstInvisibleTyBinder subst (Named (Bndr tv _))
+tcInstInvisibleTyBinder subst tv
= do { (subst', tv') <- newMetaTyVarX subst tv
; return (subst', mkTyVarTy tv') }
-tcInstInvisibleTyBinder subst (Anon ty af)
- | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty))
- -- For kinds like (k1 ~ k2) => blah, we want to emit a unification
- -- constraint for (k1 ~# k2) and return the argument (Eq# k1 k2)
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
- -- Equality is the *only* constraint currently handled in types.
- = assert (isInvisibleFunArg af) $
- do { co <- unifyKind Nothing k1 k2
- ; return (subst, mk co) }
-
- | otherwise -- This should never happen
- -- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
- = pprPanic "tcInvisibleTyBinder" (ppr ty)
-
--------------------------------
-get_eq_tys_maybe :: Type
- -> Maybe ( Coercion -> Type
- -- Given a coercion proving t1 ~# t2, produce the
- -- right instantiation for the PiTyVarBinder at hand
- , Type -- t1
- , Type -- t2
- )
--- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
-get_eq_tys_maybe ty
- -- Lifted heterogeneous equality (~~)
- | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
- , tc `hasKey` heqTyConKey
- = Just (mkHEqBoxTy k1 k2, k1, k2)
-
- -- Lifted homogeneous equality (~)
- | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
- , tc `hasKey` eqTyConKey
- = Just (mkEqBoxTy k1 k2, k1, k2)
-
- | otherwise
- = Nothing
-
--- | This takes @a ~# b@ and returns @a ~~ b@.
-mkHEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkHEqBoxTy ty1 ty2 co
- = mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
- where k1 = typeKind ty1
- k2 = typeKind ty2
-
--- | This takes @a ~# b@ and returns @a ~ b@.
-mkEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkEqBoxTy ty1 ty2 co
- = mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
- where k = typeKind ty1
-
{- *********************************************************************
* *
SkolemTvs (immutable)
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 98b8e2ae76..28894d68ed 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1342,7 +1342,7 @@ getDFunTyLitKey (CharTyLit n) = mkOccName Name.varName (show n)
-- Always succeeds, even if it returns an empty list.
tcSplitPiTys :: Type -> ([PiTyVarBinder], Type)
tcSplitPiTys ty
- = assert (all isTyBinder (fst sty) ) -- No CoVar binders here
+ = assert (all isTyBinder (fst sty)) -- No CoVar binders here
sty
where sty = splitPiTys ty
@@ -1365,7 +1365,7 @@ tcSplitForAllTyVarBinder_maybe _ = Nothing
-- returning just the tyvars.
tcSplitForAllTyVars :: Type -> ([TyVar], Type)
tcSplitForAllTyVars ty
- = assert (all isTyVar (fst sty) ) sty
+ = assert (all isTyVar (fst sty)) sty
where sty = splitForAllTyCoVars ty
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot
index 8afdbcd5ed..0d82ea613e 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs-boot
+++ b/compiler/GHC/Tc/Utils/Unify.hs-boot
@@ -12,6 +12,5 @@ import GHC.Tc.Types.Origin ( CtOrigin, TypedThing )
-- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate
unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion
-unifyKind :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 5ac3377a33..949eb90d53 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -520,6 +520,8 @@ typeOrKindCtxt (DataKindCtxt {}) = OnlyKindCtxt
typeOrKindCtxt (TySynKindCtxt {}) = OnlyKindCtxt
typeOrKindCtxt (TyFamResKindCtxt {}) = OnlyKindCtxt
+-- These cases are also described in Note [No constraints in kinds], so any
+-- change here should be reflected in that note.
typeOrKindCtxt (TySynCtxt {}) = BothTypeAndKindCtxt
-- Type synonyms can have types and kinds on their RHSs
typeOrKindCtxt (GhciCtxt {}) = BothTypeAndKindCtxt
@@ -543,7 +545,6 @@ typeLevelUserTypeCtxt ctxt = case typeOrKindCtxt ctxt of
-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
-- context for a kind of a type, where the arbitrary use of constraints is
-- currently disallowed.
--- (See @Note [Constraints in kinds]@ in "GHC.Core.TyCo.Rep".)
allConstraintsAllowed :: UserTypeCtxt -> Bool
allConstraintsAllowed = typeLevelUserTypeCtxt
@@ -931,10 +932,9 @@ checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM ()
checkConstraintsOK ve theta ty
| null theta = return ()
| allConstraintsAllowed (ve_ctxt ve) = return ()
- | otherwise
- = -- We are in a kind, where we allow only equality predicates
- -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep, and #16263
- checkTcM (all isEqPred theta) (env, TcRnConstraintInKind (tidyType env ty))
+ | otherwise -- We are unambiguously in a kind; see
+ -- Note [No constraints in kinds]
+ = failWithTcM (env, TcRnConstraintInKind (tidyType env ty))
where env = ve_tidy_env ve
checkVdqOK :: ValidityEnv -> [TyVarBinder] -> Type -> TcM ()
@@ -945,7 +945,25 @@ checkVdqOK ve tvbs ty = do
no_vdq = all (isInvisibleForAllTyFlag . binderFlag) tvbs
ValidityEnv{ve_tidy_env = env, ve_ctxt = ctxt} = ve
-{-
+{- Note [No constraints in kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC does not allow constraints in kinds. Equality constraints
+in kinds were allowed from GHC 8.0, but this "feature" was removed
+as part of Proposal #547 (https://github.com/ghc-proposals/ghc-proposals/pull/547),
+which contains further context and motivation for the removal.
+
+The lack of constraints in kinds is enforced by checkConstraintsOK, which
+uses the UserTypeCtxt to determine if we are unambiguously checking a kind.
+There are two ambiguous contexts (constructor BothTypeAndKindCtxt of TypeOrKindCtxt)
+as written in typeOfKindCtxt:
+ - TySynCtxt: this is the RHS of a type synonym. We check the expansion of type
+ synonyms for constraints, so this is handled at the usage site of the synonym.
+ - GhciCtxt: This is the type in a :kind command. A constraint here does not cause
+ any trouble, because the type cannot be used to classify a type.
+
+Beyond these two cases, we also promote data constructors. We check for constraints
+in data constructor types in GHC.Tc.Gen.HsType.tcTyVar.
+
Note [Liberal type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index 69ba5b0d22..e95abc0855 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -681,10 +681,6 @@ Currently there are nine different uses of 'VarBndr':
* TyCon.TyConBinder = VarBndr TyVar TyConBndrVis
Binders of a TyCon; see TyCon in GHC.Core.TyCon
-* TyCon.TyConPiTyBinder = VarBndr TyCoVar TyConBndrVis
- Binders of a PromotedDataCon
- See Note [Promoted GADT data constructors] in GHC.Core.TyCon
-
* IfaceType.IfaceForAllBndr = VarBndr IfaceBndr ForAllTyFlag
* IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity
* IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis
diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst
index bf99065907..8194e1f7ae 100644
--- a/docs/users_guide/exts/data_kinds.rst
+++ b/docs/users_guide/exts/data_kinds.rst
@@ -91,17 +91,10 @@ There are only a couple of exceptions to this rule:
type theory just isn’t up to the task of promoting data families, which
requires full dependent types.
-- Data constructors with contexts that contain non-equality constraints cannot
- be promoted. For example: ::
+- Data constructors with contexts cannot be promoted. For example::
data Foo :: Type -> Type where
- MkFoo1 :: a ~ Int => Foo a -- promotable
- MkFoo2 :: a ~~ Int => Foo a -- promotable
- MkFoo3 :: Show a => Foo a -- not promotable
-
- ``MkFoo1`` and ``MkFoo2`` can be promoted, since their contexts
- only involve equality-oriented constraints. However, ``MkFoo3``'s context
- contains a non-equality constraint ``Show a``, and thus cannot be promoted.
+ MkFoo :: Show a => Foo a -- not promotable
.. _promotion-syntax:
@@ -215,28 +208,3 @@ parameter to ``UnEx``, the kind is not escaping the existential, and the
above code is valid.
See also :ghc-ticket:`7347`.
-
-.. _constraints_in_kinds:
-
-Constraints in kinds
---------------------
-
-Kinds can (with :extension:`DataKinds`) contain type constraints. However,
-only equality constraints are supported.
-
-Here is an example of a constrained kind: ::
-
- type family IsTypeLit a where
- IsTypeLit Nat = True
- IsTypeLit Symbol = True
- IsTypeLit a = False
-
- data T :: forall a. (IsTypeLit a ~ True) => a -> Type where
- MkNat :: T 42
- MkSymbol :: T "Don't panic!"
-
-The declarations above are accepted. However, if we add ``MkOther :: T Int``,
-we get an error that the equality constraint is not satisfied; ``Int`` is
-not a type literal. Note that explicitly quantifying with ``forall a`` is
-necessary in order for ``T`` to typecheck
-(see :ref:`complete-kind-signatures`).
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 965e57dd16..5401a11e73 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -41,7 +41,6 @@ test('T14556', normal, compile, [''])
test('T14720', normal, compile, [''])
test('T14066a', normal, compile, [''])
test('T14749', js_broken(22364), compile, [''])
-test('T14845_compile', normal, compile, [''])
test('T14991', normal, compile, [''])
test('DkNameRes', normal, compile, [''])
test('T15346', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr
index 35ec45a24b..60edf6bc25 100644
--- a/testsuite/tests/dependent/should_fail/T13780a.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780a.stderr
@@ -1,10 +1,7 @@
-T13780a.hs:9:40: error: [GHC-25897]
- • Couldn't match kind ‘a’ with ‘Bool’
- Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
- ‘a’ is a rigid type variable bound by
- a family instance declaration
- at T13780a.hs:9:20-31
+T13780a.hs:9:40: error: [GHC-88634]
+ • Data constructor ‘MkFoo’ cannot be used here
+ (it has an unpromotable context ‘a ~ Bool’)
• In the second argument of ‘(~)’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_compile/T14845_compile.hs b/testsuite/tests/dependent/should_fail/T14845_compile.hs
index c059f1d5e9..c059f1d5e9 100644
--- a/testsuite/tests/dependent/should_compile/T14845_compile.hs
+++ b/testsuite/tests/dependent/should_fail/T14845_compile.hs
diff --git a/testsuite/tests/dependent/should_fail/T14845_compile.stderr b/testsuite/tests/dependent/should_fail/T14845_compile.stderr
new file mode 100644
index 0000000000..cfe062ae38
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_compile.stderr
@@ -0,0 +1,7 @@
+
+T14845_compile.hs:15:15: error: [GHC-88634]
+ • Data constructor ‘MkA1’ cannot be used here
+ (it has an unpromotable context ‘a ~ Int’)
+ • In the first argument of ‘SA’, namely ‘MkA1’
+ In the type ‘SA MkA1’
+ In the definition of data constructor ‘SMkA1’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 5de2070a0e..64e5341f8e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -27,6 +27,7 @@ test('T14066f', normal, compile_fail, [''])
test('T14066g', normal, compile_fail, [''])
test('T14845_fail1', normal, compile_fail, [''])
test('T14845_fail2', normal, compile_fail, [''])
+test('T14845_compile', normal, compile_fail, [''])
test('T15245', normal, compile_fail, [''])
test('T15215', normal, compile_fail, [''])
test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
index a918f90b95..baa9777849 100644
--- a/testsuite/tests/polykinds/T16902.stderr
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -1,9 +1,4 @@
-T16902.hs:12:10: error: [GHC-25897]
- • Expected a type, but found something with kind ‘a’
- ‘a’ is a rigid type variable bound by
- the type signature for ‘MkF’
- at T16902.hs:12:3-12
- • In the type ‘F a’
- In the definition of data constructor ‘MkF’
- In the data declaration for ‘F’
+T16902.hs:11:1: error: [GHC-01259]
+ • Illegal constraint in a kind: (a ~~ k) => *
+ • In the data type declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T18522-ppr.script b/testsuite/tests/polykinds/T18522-ppr.script
index 54d3619c6e..e91cc1ce88 100644
--- a/testsuite/tests/polykinds/T18522-ppr.script
+++ b/testsuite/tests/polykinds/T18522-ppr.script
@@ -1,4 +1,4 @@
-:set -XPolyKinds -XDataKinds -XRankNTypes -XTypeFamilies
+:set -XPolyKinds -XDataKinds -XRankNTypes -XTypeFamilies -fprint-explicit-foralls
import Data.Kind (Type)
-type family T :: forall k -> (k ~ k) => forall j -> k -> j -> Type
+type family T :: forall a -> ()
:k T
diff --git a/testsuite/tests/polykinds/T18522-ppr.stdout b/testsuite/tests/polykinds/T18522-ppr.stdout
index 241530bbed..ce5cea6b49 100644
--- a/testsuite/tests/polykinds/T18522-ppr.stdout
+++ b/testsuite/tests/polykinds/T18522-ppr.stdout
@@ -1 +1 @@
-T :: forall k -> (k ~ k) => forall j -> k -> j -> *
+T :: forall {k}. forall (a :: k) -> ()
diff --git a/testsuite/tests/saks/should_compile/all.T b/testsuite/tests/saks/should_compile/all.T
index 78eb3e2331..29c43b4ae1 100644
--- a/testsuite/tests/saks/should_compile/all.T
+++ b/testsuite/tests/saks/should_compile/all.T
@@ -6,7 +6,6 @@ test('saks003', normal, compile, [''])
test('saks004', normal, compile, [''])
test('saks005', normal, compile, [''])
test('saks006', normal, compile, [''])
-test('saks007', normal, compile, [''])
test('saks008', normal, compile, [''])
test('saks009', normal, compile, [''])
test('saks010', normal, compile, [''])
diff --git a/testsuite/tests/saks/should_compile/saks007.hs b/testsuite/tests/saks/should_compile/saks007.hs
deleted file mode 100644
index 0d3a94f9c9..0000000000
--- a/testsuite/tests/saks/should_compile/saks007.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds, ExplicitForAll #-}
-
--- See also: saks007_fail.hs
-module SAKS_007 where
-
-import Data.Kind (Type, Constraint)
-
-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 -- OK: F Type ~ G (Type -> Type)
- -- True ~ True
-
-
-{-
-Let co :: F Type ~ G (Type->Type)
-
-Wrapper data con type:
- $WMkX :: X @Type @(Type->Type) @(Eq# co) Integer Maybe
-
-Worker data con's type:
- MkX :: forall k1 k2 (c :: F k1 ~ G k2) (a :: k1) (b :: k2)
- -> forall . -- No existentials
- ( k1 ~# Type, k2 ~# Type->Type -- EqSpec
- , a ~# Integer, b ~# Maybe )
- => X k1 k2 c a b
-
-f :: forall k. (k ~ Type) => forall (a::k). a->a
-
-
-f :: forall (cv :: a ~# b) => ....ty|>co....
-
-
-X @kk1 @kk2 @(d :: F kk1 ~ G kk2) Integer Maybe
-
-
--} \ No newline at end of file
diff --git a/testsuite/tests/saks/should_fail/T16758.hs b/testsuite/tests/saks/should_fail/T16758.hs
deleted file mode 100644
index 2798156f3c..0000000000
--- a/testsuite/tests/saks/should_fail/T16758.hs
+++ /dev/null
@@ -1,14 +0,0 @@
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE ConstrainedClassMethods #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ExplicitForAll #-}
-
-module T16758 where
-
-import Data.Kind
-
-type C :: forall (a :: Type) -> a ~ Int => Constraint
-class C a where
- f :: C a => a -> Int
diff --git a/testsuite/tests/saks/should_fail/all.T b/testsuite/tests/saks/should_fail/all.T
index 98345aa2ca..a17eed6a2e 100644
--- a/testsuite/tests/saks/should_fail/all.T
+++ b/testsuite/tests/saks/should_fail/all.T
@@ -31,7 +31,6 @@ test('T16727b', normal, compile_fail, [''])
test('T16725', normal, compile_fail, [''])
test('T16826', normal, compile_fail, [''])
test('T16756b', normal, compile_fail, [''])
-test('T16758', normal, compile_fail, [''])
test('T18863a', normal, compile_fail, [''])
test('T18863b', normal, compile_fail, [''])
test('T20916', normal, compile_fail, [''])
diff --git a/testsuite/tests/saks/should_fail/saks007_fail.stderr b/testsuite/tests/saks/should_fail/saks007_fail.stderr
index a299c5be4a..f096aa5e18 100644
--- a/testsuite/tests/saks/should_fail/saks007_fail.stderr
+++ b/testsuite/tests/saks/should_fail/saks007_fail.stderr
@@ -1,8 +1,7 @@
-saks007_fail.hs:15:10: error: [GHC-83865]
- • Couldn't match kind ‘True’ with ‘False’
- Expected: G (*)
- Actual: F (*)
- • In the type ‘X Integer String’
- In the definition of data constructor ‘MkX’
- In the data declaration for ‘X’
+saks007_fail.hs:13:11: error: [GHC-01259]
+ • Illegal constraint in a kind: forall k1 k2.
+ (F k1 ~ G k2) =>
+ k1 -> k2 -> *
+ • In a standalone kind signature for ‘X’:
+ forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type
diff --git a/testsuite/tests/typecheck/should_compile/T15141.hs b/testsuite/tests/typecheck/should_compile/T15141.hs
deleted file mode 100644
index c0cb5d8488..0000000000
--- a/testsuite/tests/typecheck/should_compile/T15141.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# LANGUAGE PolyKinds, TypeFamilies, TypeFamilyDependencies,
- ScopedTypeVariables, TypeOperators, GADTs,
- DataKinds #-}
-
-module T15141 where
-
-import Data.Type.Equality
-import Data.Proxy
-
-type family F a = r | r -> a where
- F () = Bool
-
-data Wumpus where
- Unify :: k1 ~ F k2 => k1 -> k2 -> Wumpus
-
-f :: forall k (a :: k). k :~: Bool -> ()
-f Refl = let x :: Proxy ('Unify a b)
- x = undefined
- in ()
-
-{-
-We want this situation:
-
-forall[1] k[1].
- [G] k ~ Bool
- forall [2] ... . [W] k ~ F kappa[2]
-
-where the inner wanted can be solved only by taking the outer
-given into account. This means that the wanted needs to be floated out.
-More germane to this bug, we need *not* to generalize over kappa.
-
-The code above builds this scenario fairly exactly, and indeed fails
-without the logic in kindGeneralize that excludes constrained variables
-from generalization.
--}
diff --git a/testsuite/tests/typecheck/should_compile/T17021a.hs b/testsuite/tests/typecheck/should_compile/T17021a.hs
index aa78cb2959..41eb3f9d92 100644
--- a/testsuite/tests/typecheck/should_compile/T17021a.hs
+++ b/testsuite/tests/typecheck/should_compile/T17021a.hs
@@ -9,16 +9,5 @@ import GHC.Exts
type family Id x where
Id x = x
---type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
---newtype LevId x = MkLevId x
-
-type LevId2 :: (r ~ Id LiftedRep) => TYPE r -> TYPE r
-newtype LevId2 x = MkLevId2 x
-
-{-
-MkLevId2 :: forall (r :: RuntimeRep).
- forall (c :: r ~ Id LiftedRep) -> -- c is a TyVar
- forall (x :: TYPE r).
- x -> LevId2 @r @c x
-
--} \ No newline at end of file
+type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
+newtype LevId x = MkLevId x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 577ce86d65..0a1edfa866 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -588,7 +588,6 @@ test('T13785', normal, compile, [''])
test('T13804', normal, compile, [''])
test('T13822', js_broken(22364), compile, [''])
test('T13848', normal, compile, [''])
-test('T13871', normal, compile, [''])
test('T13879', normal, compile, [''])
test('T13881', normal, compile, [''])
test('T18851d', normal, compile, [''])
@@ -655,7 +654,6 @@ test('T15431', normal, compile, [''])
test('T15431a', normal, compile, [''])
test('T15428', normal, compile, [''])
test('T15412', normal, compile, [''])
-test('T15141', normal, compile, [''])
test('T15473', normal, compile_fail, [''])
test('T15499', normal, compile, [''])
test('T15586', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12102.stderr b/testsuite/tests/typecheck/should_fail/T12102.stderr
new file mode 100644
index 0000000000..6fd539cfa1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12102.stderr
@@ -0,0 +1,6 @@
+
+T12102.hs:17:1: error: [GHC-01259]
+ • Illegal constraint in a kind: forall a.
+ (IsTypeLit a ~ True) =>
+ a -> *
+ • In the data type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T12102b.hs b/testsuite/tests/typecheck/should_fail/T12102b.hs
deleted file mode 100644
index 8478059c8f..0000000000
--- a/testsuite/tests/typecheck/should_fail/T12102b.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-module T12102b where
-
-import Data.Kind
-import GHC.TypeLits
-
-type family IsTypeLit a where
- IsTypeLit Nat = 'True
- IsTypeLit Symbol = 'True
- IsTypeLit a = 'False
-
-data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
- MkNat :: T 42
- MkSymbol :: T "Don't panic!"
-
-deriving instance Show (T a)
diff --git a/testsuite/tests/typecheck/should_compile/T13871.hs b/testsuite/tests/typecheck/should_fail/T13871.hs
index fa233247ca..fa233247ca 100644
--- a/testsuite/tests/typecheck/should_compile/T13871.hs
+++ b/testsuite/tests/typecheck/should_fail/T13871.hs
diff --git a/testsuite/tests/typecheck/should_fail/T13871.stderr b/testsuite/tests/typecheck/should_fail/T13871.stderr
new file mode 100644
index 0000000000..0961d5f750
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13871.stderr
@@ -0,0 +1,7 @@
+
+T13871.hs:16:18: error: [GHC-88634]
+ • Data constructor ‘MkFoo’ cannot be used here
+ (it has an unpromotable context ‘(a ~ Int, b ~ Char)’)
+ • In the first argument of ‘SFoo’, namely ‘MkFoo’
+ In the type ‘SFoo MkFoo’
+ In the definition of data constructor ‘SMkFoo’
diff --git a/testsuite/tests/typecheck/should_fail/T15862.hs b/testsuite/tests/typecheck/should_fail/T15862.hs
index c98b5939d1..7890b18ce7 100644
--- a/testsuite/tests/typecheck/should_fail/T15862.hs
+++ b/testsuite/tests/typecheck/should_fail/T15862.hs
@@ -28,9 +28,3 @@ data Quux = MkQuux (# Bool | Int #)
quux :: TypeRep MkQuux
quux = typeRep
-
-data Quuz :: (Type ~ Type) => Type where
- MkQuuz :: Quuz
-
-quuz :: TypeRep MkQuuz
-quuz = typeRep
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 7d7b7f0369..b15a50b228 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -421,9 +421,9 @@ test('T12063', [expect_broken(12063)], multimod_compile_fail, ['T12063', '-v0'])
test('T12083a', normal, compile_fail, [''])
test('T12083b', normal, compile_fail, [''])
test('T11974b', normal, compile_fail, [''])
-test('T12102', normal, compile, [''])
-test('T12102b', normal, compile_fail, [''])
+test('T12102', normal, compile_fail, [''])
test('T12151', normal, compile_fail, [''])
+test('T13871', normal, compile_fail, [''])
test('T7437', normal, compile_fail, [''])
test('T12177', normal, compile_fail, [''])
test('T12406', normal, compile_fail, [''])