Commit 1033a720 authored by Krzysztof Gogolewski's avatar Krzysztof Gogolewski Committed by Marge Bot
Browse files

Reject linearity in kinds in checkValidType (#18780)

Patch taken from ghc/ghc#18624 (comment 300673)
parent 8dd4f405
......@@ -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
......
......@@ -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@. 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@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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
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’
{-# LANGUAGE LinearTypes, KindSignatures, DataKinds #-}
module LinearKind2 where -- T18780
import GHC.Exts
import GHC.Types
data Two :: FUN One Type Type
LinearKind2.hs:7:1: error:
• Illegal linear function in a kind: * %1 -> *
• In the data type declaration for ‘Two’
{-# LANGUAGE LinearTypes, KindSignatures, DataKinds #-}
module LinearKind3 where -- T18780
import GHC.Exts
import GHC.Types
type K = Type %1 -> Type
data T :: K
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’
......@@ -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)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment