[Git][ghc/ghc][master] Reject linearity in kinds in checkValidType (#18780)
Marge Bot
gitlab at gitlab.haskell.org
Fri Oct 2 17:53:30 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
1033a720 by Krzysztof Gogolewski at 2020-10-02T13:53:23-04:00
Reject linearity in kinds in checkValidType (#18780)
Patch taken from https://gitlab.haskell.org/ghc/ghc/-/issues/18624#note_300673
- - - - -
8 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Validity.hs
- testsuite/tests/linear/should_fail/LinearKind.stderr
- + testsuite/tests/linear/should_fail/LinearKind2.hs
- + testsuite/tests/linear/should_fail/LinearKind2.stderr
- + testsuite/tests/linear/should_fail/LinearKind3.hs
- + testsuite/tests/linear/should_fail/LinearKind3.stderr
- testsuite/tests/linear/should_fail/all.T
Changes:
=====================================
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
=====================================
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,12 +533,25 @@ typeOrKindCtxt (GhciCtxt {}) = BothTypeAndKindCtxt
-- @Show a => a -> a@ in @type Foo :: Show a => a -> a at . 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
@@ -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 at ValidityEnv{ve_rank = rank}) (FunTy _ _ arg_ty res_ty)
- = do { check_type (ve{ve_rank = arg_rank}) arg_ty
+check_type (ve at 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
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’
=====================================
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
=====================================
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’
=====================================
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
=====================================
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’
=====================================
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)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1033a720abf4a23a30c5cb0dfcb18b2bae3acc68
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1033a720abf4a23a30c5cb0dfcb18b2bae3acc68
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201002/77a973f0/attachment-0001.html>
More information about the ghc-commits
mailing list