diff options
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 7 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Validity.hs | 34 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/LinearKind.stderr | 7 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/LinearKind2.hs | 7 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/LinearKind2.stderr | 4 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/LinearKind3.hs | 8 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/LinearKind3.stderr | 5 | ||||
| -rw-r--r-- | testsuite/tests/linear/should_fail/all.T | 2 |
8 files changed, 58 insertions, 16 deletions
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 9c778a1b4b..d23c09fd09 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -1041,11 +1041,8 @@ tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind = failWithTc (text "Unexpected type splice:" <+> ppr ty) ---------- Functions and applications -tc_hs_type mode ty@(HsFunTy _ mult ty1 ty2) exp_kind - | mode_tyki mode == KindLevel && not (isUnrestricted mult) - = failWithTc (text "Linear arrows disallowed in kinds:" <+> ppr ty) - | otherwise - = tc_fun_type mode mult ty1 ty2 exp_kind +tc_hs_type mode (HsFunTy _ mult ty1 ty2) exp_kind + = tc_fun_type mode mult ty1 ty2 exp_kind tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind | op `hasKey` funTyConKey diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index e00b39b20e..540480147c 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -525,9 +525,7 @@ typeOrKindCtxt (GhciCtxt {}) = BothTypeAndKindCtxt -- GHCi's :kind command accepts both types and kinds -- | 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".) +-- context for a kind of a type. -- If the 'UserTypeCtxt' can refer to both types and kinds, this function -- conservatively returns 'True'. -- @@ -535,13 +533,26 @@ typeOrKindCtxt (GhciCtxt {}) = BothTypeAndKindCtxt -- @Show a => a -> a@ in @type Foo :: Show a => a -> a@. On the other hand, the -- same type in @foo :: Show a => a -> a@ is unambiguously the type of a term, -- not the kind of a type, so it is permitted. -allConstraintsAllowed :: UserTypeCtxt -> Bool -allConstraintsAllowed ctxt = case typeOrKindCtxt ctxt of +typeLevelUserTypeCtxt :: UserTypeCtxt -> Bool +typeLevelUserTypeCtxt ctxt = case typeOrKindCtxt ctxt of OnlyTypeCtxt -> True OnlyKindCtxt -> False BothTypeAndKindCtxt -> True -- | 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 + +-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the +-- context for a kind of a type, where all function arrows currently +-- must be unrestricted. +linearityAllowed :: UserTypeCtxt -> Bool +linearityAllowed = typeLevelUserTypeCtxt + +-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the -- context for the type of a term, where visible, dependent quantification is -- currently disallowed. If the 'UserTypeCtxt' can refer to both types and -- kinds, this function conservatively returns 'True'. @@ -744,8 +755,12 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt (theta, tau) = tcSplitPhiTy phi (env', tvbs') = tidyTyCoVarBinders env tvbs -check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ _ arg_ty res_ty) - = do { check_type (ve{ve_rank = arg_rank}) arg_ty +check_type (ve@ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt + , ve_rank = rank }) + ty@(FunTy _ mult arg_ty res_ty) + = do { failIfTcM (not (linearityAllowed ctxt) && not (isManyDataConTy mult)) + (linearFunKindErr env ty) + ; check_type (ve{ve_rank = arg_rank}) arg_ty ; check_type (ve{ve_rank = res_rank}) res_ty } where (arg_rank, res_rank) = funArgResRank rank @@ -993,6 +1008,11 @@ illegalVDQTyErr env ty = 2 (ppr_tidy env ty) , text "(GHC does not yet support this)" ] ) +-- | Reject uses of linear function arrows in kinds. +linearFunKindErr :: TidyEnv -> Type -> (TidyEnv, SDoc) +linearFunKindErr env ty = + (env, text "Illegal linear function in a kind:" <+> ppr_tidy env ty) + {- Note [Liberal type synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/testsuite/tests/linear/should_fail/LinearKind.stderr b/testsuite/tests/linear/should_fail/LinearKind.stderr index 9ba3f744cf..c70e90a1b5 100644 --- a/testsuite/tests/linear/should_fail/LinearKind.stderr +++ b/testsuite/tests/linear/should_fail/LinearKind.stderr @@ -1,5 +1,4 @@ -LinearKind.hs:4:11: error: - • Linear arrows disallowed in kinds: * %1 -> * - • In the kind ‘* %1 -> *’ - In the data type declaration for ‘A’ +LinearKind.hs:4:1: error: + • Illegal linear function in a kind: * %1 -> * + • In the data type declaration for ‘A’ diff --git a/testsuite/tests/linear/should_fail/LinearKind2.hs b/testsuite/tests/linear/should_fail/LinearKind2.hs new file mode 100644 index 0000000000..402b67efc4 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearKind2.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE LinearTypes, KindSignatures, DataKinds #-} +module LinearKind2 where -- T18780 + +import GHC.Exts +import GHC.Types + +data Two :: FUN One Type Type diff --git a/testsuite/tests/linear/should_fail/LinearKind2.stderr b/testsuite/tests/linear/should_fail/LinearKind2.stderr new file mode 100644 index 0000000000..0bdf1b0d19 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearKind2.stderr @@ -0,0 +1,4 @@ + +LinearKind2.hs:7:1: error: + • Illegal linear function in a kind: * %1 -> * + • In the data type declaration for ‘Two’ diff --git a/testsuite/tests/linear/should_fail/LinearKind3.hs b/testsuite/tests/linear/should_fail/LinearKind3.hs new file mode 100644 index 0000000000..7d85cb6e96 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearKind3.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE LinearTypes, KindSignatures, DataKinds #-} +module LinearKind3 where -- T18780 + +import GHC.Exts +import GHC.Types + +type K = Type %1 -> Type +data T :: K diff --git a/testsuite/tests/linear/should_fail/LinearKind3.stderr b/testsuite/tests/linear/should_fail/LinearKind3.stderr new file mode 100644 index 0000000000..8e16996baf --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearKind3.stderr @@ -0,0 +1,5 @@ + +LinearKind3.hs:8:1: error: + • Illegal linear function in a kind: * %1 -> * + • In the expansion of type synonym ‘K’ + In the data type declaration for ‘T’ diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T index bcba344268..272e9e2a35 100644 --- a/testsuite/tests/linear/should_fail/all.T +++ b/testsuite/tests/linear/should_fail/all.T @@ -20,6 +20,8 @@ test('LinearPatSyn', normal, compile_fail, ['']) test('LinearGADTNewtype', normal, compile_fail, ['']) test('LinearPartialSig', normal, compile_fail, ['']) test('LinearKind', normal, compile_fail, ['']) +test('LinearKind2', normal, compile_fail, ['']) +test('LinearKind3', normal, compile_fail, ['']) test('LinearVar', normal, compile_fail, ['-XLinearTypes']) test('LinearErrOrigin', normal, compile_fail, ['-XLinearTypes']) test('LinearPolyType', normal, compile_fail, ['']) # not supported yet (#390) |