diff options
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, ['']) |