summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs7
-rw-r--r--compiler/GHC/Tc/Validity.hs34
-rw-r--r--testsuite/tests/linear/should_fail/LinearKind.stderr7
-rw-r--r--testsuite/tests/linear/should_fail/LinearKind2.hs7
-rw-r--r--testsuite/tests/linear/should_fail/LinearKind2.stderr4
-rw-r--r--testsuite/tests/linear/should_fail/LinearKind3.hs8
-rw-r--r--testsuite/tests/linear/should_fail/LinearKind3.stderr5
-rw-r--r--testsuite/tests/linear/should_fail/all.T2
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)