[Git][ghc/ghc][master] 2 commits: Remove unused ThBrackCtxt and ResSigCtxt
Marge Bot
gitlab at gitlab.haskell.org
Mon Sep 21 20:45:56 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
1a0f8243 by Ryan Scott at 2020-09-21T16:45:47-04:00
Remove unused ThBrackCtxt and ResSigCtxt
Fixes #18715.
- - - - -
2f222b12 by Ryan Scott at 2020-09-21T16:45:47-04:00
Disallow constraints in KindSigCtxt
This patch cleans up how `GHC.Tc.Validity` classifies `UserTypeCtxt`s
that can only refer to kind-level positions, which is important for
rejecting certain classes of programs. In particular, this patch:
* Introduces a new `TypeOrKindCtxt` data type and
`typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt` function, which
determines whether a `UserTypeCtxt` can refer to type-level
contexts, kind-level contexts, or both.
* Defines the existing `allConstraintsAllowed` and `vdqAllowed`
functions in terms of `typeOrKindCtxt`, which avoids code
duplication and ensures that they stay in sync in the future.
The net effect of this patch is that it fixes #18714, in which it was
discovered that `allConstraintsAllowed` incorrectly returned `True`
for `KindSigCtxt`. Because `typeOrKindCtxt` now correctly classifies
`KindSigCtxt` as a kind-level context, this bug no longer occurs.
- - - - -
6 changed files:
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Validity.hs
- + testsuite/tests/typecheck/should_fail/T18714.hs
- + testsuite/tests/typecheck/should_fail/T18714.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -2838,7 +2838,6 @@ expectedKindInCtxt :: UserTypeCtxt -> ContextKind
-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
-expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
-- The types in a 'default' decl can have varying kinds
-- See Note [Extended defaults]" in GHC.Tc.Utils.Env
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -84,15 +84,12 @@ data UserTypeCtxt
-- or (x::t, y) = e
| RuleSigCtxt Name -- LHS of a RULE forall
-- RULE "foo" forall (x :: a -> a). f (Just x) = ...
- | ResSigCtxt -- Result type sig
- -- f x :: t = ....
| ForSigCtxt Name -- Foreign import or export signature
| DefaultDeclCtxt -- Types in a default declaration
| InstDeclCtxt Bool -- An instance declaration
-- True: stand-alone deriving
-- False: vanilla instance declaration
| SpecInstCtxt -- SPECIALISE instance pragma
- | ThBrackCtxt -- Template Haskell type brackets [t| ... |]
| GenSigCtxt -- Higher-rank or impredicative situations
-- e.g. (f e) where f has a higher-rank type
-- We might want to elaborate this
@@ -136,9 +133,7 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
-pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t|...|]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
-pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt = text "a type in a `default' declaration"
pprUserTypeCtxt (InstDeclCtxt False) = text "an instance declaration"
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -348,7 +348,6 @@ checkValidType ctxt ty
rank
= case ctxt of
DefaultDeclCtxt-> MustBeMonoType
- ResSigCtxt -> MustBeMonoType
PatSigCtxt -> rank0
RuleSigCtxt _ -> rank1
TySynCtxt _ -> rank0
@@ -372,7 +371,6 @@ checkValidType ctxt ty
ForSigCtxt _ -> rank1
SpecInstCtxt -> rank1
- ThBrackCtxt -> rank1
GhciCtxt {} -> ArbitraryRank
TyVarBndrKindCtxt _ -> rank0
@@ -472,18 +470,81 @@ forAllAllowed ArbitraryRank = True
forAllAllowed (LimitedRank forall_ok _) = forall_ok
forAllAllowed _ = False
+-- | Indicates whether a 'UserTypeCtxt' represents type-level contexts,
+-- kind-level contexts, or both.
+data TypeOrKindCtxt
+ = OnlyTypeCtxt
+ -- ^ A 'UserTypeCtxt' that only represents type-level positions.
+ | OnlyKindCtxt
+ -- ^ A 'UserTypeCtxt' that only represents kind-level positions.
+ | BothTypeAndKindCtxt
+ -- ^ A 'UserTypeCtxt' that can represent both type- and kind-level positions.
+ deriving Eq
+
+instance Outputable TypeOrKindCtxt where
+ ppr ctxt = text $ case ctxt of
+ OnlyTypeCtxt -> "OnlyTypeCtxt"
+ OnlyKindCtxt -> "OnlyKindCtxt"
+ BothTypeAndKindCtxt -> "BothTypeAndKindCtxt"
+
+-- | Determine whether a 'UserTypeCtxt' can represent type-level contexts,
+-- kind-level contexts, or both.
+typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt
+typeOrKindCtxt (FunSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (InfSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (ExprSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (TypeAppCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (PatSynCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (PatSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (RuleSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (ForSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (DefaultDeclCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (InstDeclCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (SpecInstCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (GenSigCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (ClassSCCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (SigmaCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (DataTyCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (DerivClauseCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (ConArgCtxt {}) = OnlyTypeCtxt
+ -- Although data constructors can be promoted with DataKinds, we always
+ -- validity-check them as though they are the types of terms. We may need
+ -- to revisit this decision if we ever allow visible dependent quantification
+ -- in the types of data constructors.
+
+typeOrKindCtxt (KindSigCtxt {}) = OnlyKindCtxt
+typeOrKindCtxt (StandaloneKindSigCtxt {}) = OnlyKindCtxt
+typeOrKindCtxt (TyVarBndrKindCtxt {}) = OnlyKindCtxt
+typeOrKindCtxt (DataKindCtxt {}) = OnlyKindCtxt
+typeOrKindCtxt (TySynKindCtxt {}) = OnlyKindCtxt
+typeOrKindCtxt (TyFamResKindCtxt {}) = OnlyKindCtxt
+
+typeOrKindCtxt (TySynCtxt {}) = BothTypeAndKindCtxt
+ -- Type synonyms can have types and kinds on their RHSs
+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".)
+-- If the 'UserTypeCtxt' can refer to both types and kinds, this function
+-- conservatively returns 'True'.
+--
+-- An example of something that is unambiguously the kind of a type is the
+-- @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
--- We don't allow arbitrary constraints in kinds
-allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
-allConstraintsAllowed (DataKindCtxt {}) = False
-allConstraintsAllowed (TySynKindCtxt {}) = False
-allConstraintsAllowed (TyFamResKindCtxt {}) = False
-allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
-allConstraintsAllowed _ = True
+allConstraintsAllowed ctxt = case typeOrKindCtxt ctxt of
+ OnlyTypeCtxt -> True
+ OnlyKindCtxt -> False
+ BothTypeAndKindCtxt -> True
-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
-- context for the type of a term, where visible, dependent quantification is
--- currently disallowed.
+-- currently disallowed. If the 'UserTypeCtxt' can refer to both types and
+-- kinds, this function conservatively returns 'True'.
--
-- An example of something that is unambiguously the type of a term is the
-- @forall a -> a -> a@ in @foo :: forall a -> a -> a at . On the other hand, the
@@ -496,40 +557,10 @@ allConstraintsAllowed _ = True
-- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where
-- VDQ is disallowed).
vdqAllowed :: UserTypeCtxt -> Bool
--- Currently allowed in the kinds of types...
-vdqAllowed (KindSigCtxt {}) = True
-vdqAllowed (StandaloneKindSigCtxt {}) = True
-vdqAllowed (TySynCtxt {}) = True
-vdqAllowed (ThBrackCtxt {}) = True
-vdqAllowed (GhciCtxt {}) = True
-vdqAllowed (TyVarBndrKindCtxt {}) = True
-vdqAllowed (DataKindCtxt {}) = True
-vdqAllowed (TySynKindCtxt {}) = True
-vdqAllowed (TyFamResKindCtxt {}) = True
--- ...but not in the types of terms.
-vdqAllowed (ConArgCtxt {}) = False
- -- We could envision allowing VDQ in data constructor types so long as the
- -- constructor is only ever used at the type level, but for now, GHC adopts
- -- the stance that VDQ is never allowed in data constructor types.
-vdqAllowed (FunSigCtxt {}) = False
-vdqAllowed (InfSigCtxt {}) = False
-vdqAllowed (ExprSigCtxt {}) = False
-vdqAllowed (TypeAppCtxt {}) = False
-vdqAllowed (PatSynCtxt {}) = False
-vdqAllowed (PatSigCtxt {}) = False
-vdqAllowed (RuleSigCtxt {}) = False
-vdqAllowed (ResSigCtxt {}) = False
-vdqAllowed (ForSigCtxt {}) = False
-vdqAllowed (DefaultDeclCtxt {}) = False
--- We count class constraints as "types of terms". All of the cases below deal
--- with class constraints.
-vdqAllowed (InstDeclCtxt {}) = False
-vdqAllowed (SpecInstCtxt {}) = False
-vdqAllowed (GenSigCtxt {}) = False
-vdqAllowed (ClassSCCtxt {}) = False
-vdqAllowed (SigmaCtxt {}) = False
-vdqAllowed (DataTyCtxt {}) = False
-vdqAllowed (DerivClauseCtxt {}) = False
+vdqAllowed ctxt = case typeOrKindCtxt ctxt of
+ OnlyTypeCtxt -> False
+ OnlyKindCtxt -> True
+ BothTypeAndKindCtxt -> True
{-
Note [Correctness and performance of type synonym validity checking]
@@ -1329,11 +1360,9 @@ okIPCtxt (InfSigCtxt {}) = True
okIPCtxt ExprSigCtxt = True
okIPCtxt TypeAppCtxt = True
okIPCtxt PatSigCtxt = True
-okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True -- ??
-okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
=====================================
testsuite/tests/typecheck/should_fail/T18714.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T18714 where
+
+import GHC.Exts
+
+type Id a = a
+
+type F = Id (Any :: forall a. Show a => a -> a)
=====================================
testsuite/tests/typecheck/should_fail/T18714.stderr
=====================================
@@ -0,0 +1,7 @@
+
+T18714.hs:11:14: error:
+ • Illegal constraint in a kind: forall a. Show a => a -> a
+ • In the first argument of ‘Id’, namely
+ ‘(Any :: forall a. Show a => a -> a)’
+ In the type ‘Id (Any :: forall a. Show a => a -> a)’
+ In the type declaration for ‘F’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -579,3 +579,4 @@ test('T18357a', normal, compile_fail, [''])
test('T18357b', normal, compile_fail, [''])
test('T18455', normal, compile_fail, [''])
test('T18534', normal, compile_fail, [''])
+test('T18714', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9df77fed8918bb335874a584a829ee32325cefb5...2f222b120e48df1b3d78f5501612d21c2a2dc470
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9df77fed8918bb335874a584a829ee32325cefb5...2f222b120e48df1b3d78f5501612d21c2a2dc470
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/20200921/25b7c7ed/attachment-0001.html>
More information about the ghc-commits
mailing list