diff options
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 107 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl.hs | 89 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Instance.hs | 15 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 7 |
4 files changed, 165 insertions, 53 deletions
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index cc82f30dbc..61b66f3919 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -2908,9 +2908,9 @@ data ContextKind = TheKind Kind -- ^ a specific kind ----------------------- newExpectedKind :: ContextKind -> TcM Kind -newExpectedKind (TheKind k) = return k -newExpectedKind AnyKind = newMetaKindVar -newExpectedKind OpenKind = newOpenTypeKind +newExpectedKind (TheKind k) = return k +newExpectedKind AnyKind = newMetaKindVar +newExpectedKind OpenKind = newOpenTypeKind ----------------------- expectedKindInCtxt :: UserTypeCtxt -> ContextKind @@ -3579,6 +3579,22 @@ data DataSort | DataInstanceSort NewOrData | DataFamilySort +-- | Local helper type used in 'checkDataKindSig'. +-- +-- Superficially similar to 'ContextKind', but it lacks 'AnyKind' +-- and 'AnyBoxedKind', and instead of @'TheKind' liftedTypeKind@ +-- provides 'LiftedKind', which is much simpler to match on and +-- handle in 'isAllowedDataResKind'. +data AllowedDataResKind + = AnyTYPEKind + | AnyBoxedKind + | LiftedKind + +isAllowedDataResKind :: AllowedDataResKind -> Kind -> Bool +isAllowedDataResKind AnyTYPEKind kind = tcIsRuntimeTypeKind kind +isAllowedDataResKind AnyBoxedKind kind = tcIsBoxedTypeKind kind +isAllowedDataResKind LiftedKind kind = tcIsLiftedTypeKind kind + -- | Checks that the return kind in a data declaration's kind signature is -- permissible. There are three cases: -- @@ -3603,7 +3619,7 @@ checkDataKindSig :: DataSort -> Kind -- any arguments in the kind are stripped checkDataKindSig data_sort kind = do { dflags <- getDynFlags ; traceTc "checkDataKindSig" (ppr kind) - ; checkTc (is_TYPE_or_Type dflags || is_kind_var) + ; checkTc (tYPE_ok dflags || is_kind_var) (err_msg dflags) } where res_kind = snd (tcSplitPiTys kind) @@ -3626,6 +3642,13 @@ checkDataKindSig data_sort kind DataInstanceSort new_or_data -> new_or_data == NewType DataFamilySort -> False + is_datatype :: Bool + is_datatype = + case data_sort of + DataDeclSort DataType -> True + DataInstanceSort DataType -> True + _ -> False + is_data_family :: Bool is_data_family = case data_sort of @@ -3633,27 +3656,30 @@ checkDataKindSig data_sort kind DataInstanceSort{} -> False DataFamilySort -> True + allowed_kind :: DynFlags -> AllowedDataResKind + allowed_kind dflags + | is_newtype && xopt LangExt.UnliftedNewtypes dflags + -- With UnliftedNewtypes, we allow kinds other than Type, but they + -- must still be of the form `TYPE r` since we don't want to accept + -- Constraint or Nat. + -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl. + = AnyTYPEKind + | is_data_family + -- If this is a `data family` declaration, we don't need to check if + -- UnliftedNewtypes is enabled, since data family declarations can + -- have return kind `TYPE r` unconditionally (#16827). + = AnyTYPEKind + | is_datatype && xopt LangExt.UnliftedDatatypes dflags + -- With UnliftedDatatypes, we allow kinds other than Type, but they + -- must still be of the form `TYPE (BoxedRep l)`, so that we don't + -- accept result kinds like `TYPE IntRep`. + -- See Note [Implementation of UnliftedDatatypes] in GHC.Tc.TyCl. + = AnyBoxedKind + | otherwise + = LiftedKind + tYPE_ok :: DynFlags -> Bool - tYPE_ok dflags = - (is_newtype && xopt LangExt.UnliftedNewtypes dflags) - -- With UnliftedNewtypes, we allow kinds other than Type, but they - -- must still be of the form `TYPE r` since we don't want to accept - -- Constraint or Nat. - -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl. - || is_data_family - -- If this is a `data family` declaration, we don't need to check if - -- UnliftedNewtypes is enabled, since data family declarations can - -- have return kind `TYPE r` unconditionally (#16827). - - is_TYPE :: Bool - is_TYPE = tcIsRuntimeTypeKind res_kind - - is_Type :: Bool - is_Type = tcIsLiftedTypeKind res_kind - - is_TYPE_or_Type :: DynFlags -> Bool - is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE - | otherwise = is_Type + tYPE_ok dflags = isAllowedDataResKind (allowed_kind dflags) res_kind -- In the particular case of a data family, permit a return kind of the -- form `:: k` (where `k` is a bare kind variable). @@ -3661,17 +3687,32 @@ checkDataKindSig data_sort kind is_kind_var | is_data_family = isJust (tcGetCastedTyVar_maybe res_kind) | otherwise = False + pp_allowed_kind dflags = + case allowed_kind dflags of + AnyTYPEKind -> ppr tYPETyCon + AnyBoxedKind -> ppr boxedRepDataConTyCon + LiftedKind -> ppr liftedTypeKind + err_msg :: DynFlags -> SDoc err_msg dflags = - sep [ (sep [ pp_dec <+> - text "has non-" <> - (if tYPE_ok dflags then text "TYPE" else ppr liftedTypeKind) - , (if is_data_family then text "and non-variable" else empty) <+> - text "return kind" <+> quotes (ppr res_kind) ]) - , if not (tYPE_ok dflags) && is_TYPE && is_newtype && - not (xopt LangExt.UnliftedNewtypes dflags) - then text "Perhaps you intended to use UnliftedNewtypes" - else empty ] + sep [ sep [ pp_dec <+> + text "has non-" <> + pp_allowed_kind dflags + , (if is_data_family then text "and non-variable" else empty) <+> + text "return kind" <+> quotes (ppr kind) ] + , ext_hint dflags ] + + ext_hint dflags + | tcIsRuntimeTypeKind kind + , is_newtype + , not (xopt LangExt.UnliftedNewtypes dflags) + = text "Perhaps you intended to use UnliftedNewtypes" + | tcIsBoxedTypeKind kind + , is_datatype + , not (xopt LangExt.UnliftedDatatypes dflags) + = text "Perhaps you intended to use UnliftedDatatypes" + | otherwise + = empty -- | Checks that the result kind of a class is exactly `Constraint`, rejecting -- type synonyms and type families that reduce to `Constraint`. See #16826. diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index e1da82d3bb..ec8c2bb66e 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -945,7 +945,7 @@ Each forall'd type variable in a type or kind is one of * Specified: the argument can be inferred at call sites, but may be instantiated with visible type/kind application - * Inferred: the must be inferred at call sites; it + * Inferred: the argument must be inferred at call sites; it is unavailable for use with visible type/kind application. Why have Inferred at all? Because we just can't make user-facing @@ -1115,7 +1115,7 @@ We do kind inference as follows: All this is very similar at the level of terms: see GHC.Tc.Gen.Bind Note [Quantified variables in partial type signatures] - But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon] + But there are some tricky corners: Note [Tricky scoping in generaliseTcTyCon] * Step 4. Extend the type environment with a TcTyCon for S and T, now with their utterly-final polymorphic kinds (needed for recursive @@ -1345,7 +1345,7 @@ getInitialKind strategy ; tc <- kcDeclHeader strategy name flav ktvs $ case m_sig of Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig - Nothing -> return $ dataDeclDefaultResultKind new_or_data + Nothing -> return $ dataDeclDefaultResultKind strategy new_or_data ; return [tc] } getInitialKind InitialKindInfer (FamDecl { tcdFam = decl }) @@ -1454,14 +1454,18 @@ have before standalone kind signatures: -} -- See Note [Data declaration default result kind] -dataDeclDefaultResultKind :: NewOrData -> ContextKind -dataDeclDefaultResultKind NewType = OpenKind - -- See Note [Implementation of UnliftedNewtypes], point <Error Messages>. -dataDeclDefaultResultKind DataType = TheKind liftedTypeKind +dataDeclDefaultResultKind :: InitialKindStrategy -> NewOrData -> ContextKind +dataDeclDefaultResultKind strategy new_or_data + | NewType <- new_or_data + = OpenKind -- See Note [Implementation of UnliftedNewtypes], point <Error Messages>. + | DataType <- new_or_data + , InitialKindCheck (SAKS _) <- strategy + = OpenKind -- See Note [Implementation of UnliftedDatatypes] + | otherwise + = TheKind liftedTypeKind {- Note [Data declaration default result kind] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - When the user has not written an inline result kind annotation on a data declaration, we assume it to be 'Type'. That is, the following declarations D1 and D2 are considered equivalent: @@ -1478,14 +1482,25 @@ accept D4: data D4 :: Type -> Type where MkD4 :: ... -> D4 param -However, there's a twist: for newtypes, we must relax -the assumed result kind to (TYPE r): +However, there are two twists: + + * For unlifted newtypes, we must relax the assumed result kind to (TYPE r): + + newtype D5 where + MkD5 :: Int# -> D5 + + See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note + <Error Messages>. + + * For unlifted datatypes, we must relax the assumed result kind to + (TYPE (BoxedRep l)) in the presence of a SAKS: - newtype D5 where - MkD5 :: Int# -> D5 + type D6 :: Type -> TYPE (BoxedRep Unlifted) + data D6 a = MkD6 a + + Otherwise, it would be impossible to declare unlifted data types in H98 + syntax (which doesn't allow specification of a result kind). -See Note [Implementation of UnliftedNewtypes], STEP 1 and it's sub-note -<Error Messages>. -} --------------------------------- @@ -2252,6 +2267,52 @@ the validity checker), that will not happen. But I cannot think of a non-contriv example that will notice this lack of inference, so it seems better to improve error messages than be able to infer this instantiation. +Note [Implementation of UnliftedDatatypes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Expected behavior of UnliftedDatatypes: + +* Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0265-unlifted-datatypes.rst +* Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265 + +The implementation heavily leans on Note [Implementation of UnliftedNewtypes]. + +In the frontend, the following tweaks have been made in the typechecker: + +* STEP 1: In the inferInitialKinds phase, newExpectedKind gives data type + constructors a result kind of `TYPE r` with a fresh unification variable + `r :: RuntimeRep` when there is a SAKS. (Same as for UnliftedNewtypes.) + Not needed with a CUSK, because it can't specify result kinds. + If there's a GADTSyntax result kind signature, we keep on using that kind. + + Similarly, for data instances without a kind signature, we use + `TYPE r` as the result kind, to support the following code: + + data family F a :: UnliftedType + data instance F Int = TInt + + The ommission of a kind signature for `F` should not mean a result kind + of `Type` (and thus a kind error) here. + +* STEP 2: No change to kcTyClDecl. + +* STEP 3: In GHC.Tc.Gen.HsType.checkDataKindSig, we make sure that the result + kind of the data declaration is actually `Type` or `TYPE (BoxedRep l)`, + for some `l`. If UnliftedDatatypes is not activated, we emit an error with a + suggestion in the latter case. + + Why not start out with `TYPE (BoxedRep l)` in the first place? Because then + we get worse kind error messages in e.g. saks_fail010: + + - Couldn't match expected kind: TYPE ('GHC.Types.BoxedRep t0) + - with actual kind: * -> * + + Expected a type, but found something with kind â* -> *â + In the data type declaration for âTâ + + It seems `TYPE r` already has appropriate pretty-printing support. + +The changes to Core, STG and Cmm are of rather cosmetic nature. +The IRs are already well-equipped to handle unlifted types, and unlifted +datatypes are just a new sub-class thereof. -} tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo]) diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 657e1bffe7..8bfb5370bb 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -727,7 +727,7 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env ; traceTc "tcDataFamInstDecl" $ vcat [ text "Fam tycon:" <+> ppr fam_tc , text "Pats:" <+> ppr pats - , text "visiblities:" <+> ppr (tcbVisibilities fam_tc pats) + , text "visibilities:" <+> ppr (tcbVisibilities fam_tc pats) , text "all_pats:" <+> ppr all_pats , text "ty_binders" <+> ppr ty_binders , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc) @@ -940,12 +940,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity fam_name = tyConName fam_tc data_ctxt = DataKindCtxt fam_name - -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2). + -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, families (2), + -- and Note [Implementation of UnliftedDatatypes]. tc_kind_sig Nothing - = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes - ; if unlifted_newtypes && new_or_data == NewType - then newOpenTypeKind - else pure liftedTypeKind + = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; unlifted_datatypes <- xoptM LangExt.UnliftedDatatypes + ; case new_or_data of + NewType | unlifted_newtypes -> newOpenTypeKind + DataType | unlifted_datatypes -> newOpenTypeKind + _ -> pure liftedTypeKind } -- See Note [Result kind signature for a data family instance] diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index a3cda06cac..b6f5065997 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -23,6 +23,7 @@ module GHC.Tc.Utils.TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind, + newOpenBoxedTypeKind, newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, newAnonMetaTyVar, cloneMetaTyVar, newCycleBreakerTyVar, @@ -1075,6 +1076,12 @@ newOpenFlexiTyVar = do { kind <- newOpenTypeKind ; newFlexiTyVar kind } +newOpenBoxedTypeKind :: TcM TcKind +newOpenBoxedTypeKind + = do { lev <- newFlexiTyVarTy (mkTyConTy levityTyCon) + ; let rr = mkTyConApp boxedRepDataConTyCon [lev] + ; return (tYPE rr) } + newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Instantiate with META type variables -- Note that this works for a sequence of kind, type, and coercion variables |