diff options
Diffstat (limited to 'compiler/GHC/Core')
| -rw-r--r-- | compiler/GHC/Core/DataCon.hs | 64 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 107 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCon.hs | 93 | ||||
| -rw-r--r-- | compiler/GHC/Core/Type.hs | 16 |
4 files changed, 31 insertions, 249 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` |