[Git][ghc/ghc][wip/p547] Drop support for kind constraints.
Richard Eisenberg (@rae)
gitlab at gitlab.haskell.org
Tue Nov 22 02:38:33 UTC 2022
Richard Eisenberg pushed to branch wip/p547 at Glasgow Haskell Compiler / GHC
Commits:
54c9a8b7 by Richard Eisenberg at 2022-11-21T21:38:16-05:00
Drop support for kind constraints.
This implements proposal 547 and closes ticket #22298.
See the proposal and ticket for motivation.
- - - - -
18 changed files:
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Validity.hs
- compiler/GHC/Types/Var.hs
- docs/users_guide/exts/data_kinds.rst
Changes:
=====================================
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
@@ -1213,11 +1164,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
@@ -1840,20 +1789,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
=====================================
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
=====================================
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,
@@ -440,38 +440,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) $
@@ -494,10 +485,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
@@ -512,7 +501,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
@@ -525,7 +514,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 = mkNakedKindFunTy af (varType tv) k
+ mk (Bndr tv AnonTCB) k = mkNakedKindFunTy FTF_T_T (varType tv) k
-- mkNakedKindFunTy: see Note [Naked FunTy] in GHC.Builtin.Types
-- | (mkTyConTy tc) returns (TyConApp tc [])
@@ -544,9 +533,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
@@ -556,35 +543,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
@@ -640,7 +599,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
@@ -651,7 +610,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
@@ -668,7 +627,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
@@ -740,12 +699,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) } }
@@ -951,13 +910,15 @@ data TyCon =
}
-- | 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]
tyConUnique :: !Unique, -- ^ Same Unique as the data constructor
tyConName :: Name, -- ^ Same Name as the data constructor
-- See Note [The binders/kind/arity fields of a TyCon]
- tyConBinders :: [TyConPiTyBinder], -- ^ Full binders
- -- TyConPiTyBinder: see Note [Promoted GADT data constructors]
+ tyConBinders :: [TyConBinder], -- ^ Full binders
tyConResKind :: Kind, -- ^ Result kind
tyConKind :: Kind, -- ^ Kind of this TyCon
tyConArity :: Arity, -- ^ Arity
@@ -1017,17 +978,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,
@@ -2044,7 +1994,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
= let tc =
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -1731,7 +1731,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
@@ -1793,7 +1793,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
@@ -2484,9 +2484,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) -----------------------
@@ -2504,10 +2503,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]
@@ -2805,8 +2800,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`
=====================================
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)
=====================================
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]
@@ -890,12 +890,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))
=====================================
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' }
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -2066,14 +2066,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.
=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -916,6 +916,7 @@ instance Diagnostic TcRnMessage where
ConstrainedDataConPE pred
-> text "it has an unpromotable context"
<+> quotes (ppr pred)
+
FamDataConPE -> text "it comes from a data family instance"
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted"
=====================================
compiler/GHC/Tc/Errors/Types.hs
=====================================
@@ -3724,9 +3724,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 PredType -- 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
@@ -3736,28 +3735,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 pred) = text "ConstrainedDataConPE" <+> parens (ppr pred)
+ 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.
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -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 pred)
; 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
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -1079,7 +1079,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' #-}
=====================================
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)
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -387,71 +387,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 at .
-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 at .
-mkEqBoxTy :: Type -> Type -> TcCoercion -> Type
-mkEqBoxTy ty1 ty2 co
- = mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
- where k = typeKind ty1
-
{- *********************************************************************
* *
SkolemTvs (immutable)
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1344,7 +1344,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
@@ -1367,7 +1367,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'
=====================================
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 removal of t
+
+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*
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -682,10 +682,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
=====================================
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`).
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/54c9a8b759e8db0cf39467e74619a6f75a3a2a74
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/54c9a8b759e8db0cf39467e74619a6f75a3a2a74
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221121/d8759991/attachment-0001.html>
More information about the ghc-commits
mailing list