diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2019-01-08 07:37:18 -0500 |
---|---|---|
committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2019-01-08 07:37:18 -0500 |
commit | 6b70cf611e5ddc475edaa54b893d20990699ddb8 (patch) | |
tree | b8cacfce9a907079df9475a943caa9e7c8ce0085 | |
parent | 6b5ec08a4a64525bae87a8c2202688ffc6f86aa8 (diff) | |
download | haskell-6b70cf611e5ddc475edaa54b893d20990699ddb8.tar.gz |
Be pickier about unsaturated synonyms in :kind
Summary:
We currently permit any and all uses of unsaturated type
synonyms and type families in GHCi's `:kind` command, which allows
strange interactions like this one:
```
> :set -XTypeFamilies -XPolyKinds
> type family Id (a :: k)
> type instance Id a = a
> type Foo x = Maybe
> :kind! Id Foo
```
This is probably a stretch too far, so this patch moves to disallow
unsaturated synonyms that aren't at the top level (we still want to
allow `:kind Id`, for instance). We do this by augmenting `GhciCtxt`
with an additional `Bool` field to indicate if we are at the
outermost level of the type being passed to `:kind` or not. See
`Note [Unsaturated type synonyms in GHCi]` in `TcValidity` for the
full story.
Test Plan: make test TEST=T16013
Reviewers: goldfire, bgamari
Reviewed By: goldfire
Subscribers: simonpj, goldfire, rwbarton, carter
GHC Trac Issues: #16013
Differential Revision: https://phabricator.haskell.org/D5471
-rw-r--r-- | compiler/typecheck/TcHsType.hs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcRnDriver.hs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcType.hs | 8 | ||||
-rw-r--r-- | compiler/typecheck/TcValidity.hs | 61 | ||||
-rw-r--r-- | testsuite/tests/ghci/should_fail/T16013.script | 5 | ||||
-rw-r--r-- | testsuite/tests/ghci/should_fail/T16013.stderr | 3 | ||||
-rw-r--r-- | testsuite/tests/ghci/should_fail/all.T | 1 |
7 files changed, 71 insertions, 11 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 7f4e379fef..006a97bd55 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1852,7 +1852,7 @@ expectedKindInCtxt :: UserTypeCtxt -> ContextKind -- splice), or only certain kinds (like in type signatures). expectedKindInCtxt (TySynCtxt _) = AnyKind expectedKindInCtxt ThBrackCtxt = AnyKind -expectedKindInCtxt GhciCtxt = AnyKind +expectedKindInCtxt (GhciCtxt {}) = AnyKind -- The types in a 'default' decl can have varying kinds -- See Note [Extended defaults]" in TcEnv expectedKindInCtxt DefaultDeclCtxt = AnyKind diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 54948e00e2..fae0c19394 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -2415,7 +2415,7 @@ tcRnType hsc_env normalise rdr_type ; ty <- zonkTcTypeToType ty -- Do validity checking on type - ; checkValidType GhciCtxt ty + ; checkValidType (GhciCtxt True) ty ; ty' <- if normalise then do { fam_envs <- tcGetFamInstEnvs diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 90d4408126..b2c9b3291f 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -606,7 +606,11 @@ data UserTypeCtxt | GenSigCtxt -- Higher-rank or impredicative situations -- e.g. (f e) where f has a higher-rank type -- We might want to elaborate this - | GhciCtxt -- GHCi command :kind <type> + | GhciCtxt Bool -- GHCi command :kind <type> + -- The Bool indicates if we are checking the outermost + -- type application. + -- See Note [Unsaturated type synonyms in GHCi] in + -- TcValidity. | ClassSCCtxt Name -- Superclasses of a class | SigmaCtxt -- Theta part of a normal for-all type @@ -650,7 +654,7 @@ pprUserTypeCtxt (InstDeclCtxt False) = text "an instance declaration" pprUserTypeCtxt (InstDeclCtxt True) = text "a stand-alone deriving instance declaration" pprUserTypeCtxt SpecInstCtxt = text "a SPECIALISE instance pragma" pprUserTypeCtxt GenSigCtxt = text "a type expected by the context" -pprUserTypeCtxt GhciCtxt = text "a type in a GHCi command" +pprUserTypeCtxt (GhciCtxt {}) = text "a type in a GHCi command" pprUserTypeCtxt (ClassSCCtxt c) = text "the super-classes of class" <+> quotes (ppr c) pprUserTypeCtxt SigmaCtxt = text "the context of a polymorphic type" pprUserTypeCtxt (DataTyCtxt tc) = text "the context of the data type declaration for" <+> quotes (ppr tc) diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 867e202218..64f5bc779c 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -228,7 +228,7 @@ checkAmbiguity ctxt ty wantAmbiguityCheck :: UserTypeCtxt -> Bool wantAmbiguityCheck ctxt = case ctxt of -- See Note [When we don't check for ambiguity] - GhciCtxt -> False + GhciCtxt {} -> False TySynCtxt {} -> False TypeAppCtxt -> False _ -> True @@ -357,7 +357,7 @@ checkValidType ctxt ty ForSigCtxt _ -> rank1 SpecInstCtxt -> rank1 ThBrackCtxt -> rank1 - GhciCtxt -> ArbitraryRank + GhciCtxt {} -> ArbitraryRank TyVarBndrKindCtxt _ -> rank0 DataKindCtxt _ -> rank1 @@ -547,16 +547,63 @@ check_syn_tc_app env ctxt rank ty tc tys in addErrCtxt err_ctxt $ check_type env ctxt rank ty' Nothing -> pprPanic "check_tau_type" (ppr ty) } - | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in - -- GHCi :kind commands; see Trac #7586 + | GhciCtxt True <- ctxt -- Accept outermost under-saturated type synonym or + -- type family constructors in GHCi :kind commands. + -- See Note [Unsaturated type synonyms in GHCi] = mapM_ check_arg tys | otherwise = failWithTc (tyConArityErr tc tys) where tc_arity = tyConArity tc - check_arg | isTypeFamilyTyCon tc = check_arg_type env ctxt rank - | otherwise = check_type env ctxt synArgMonoType + check_arg + | isTypeFamilyTyCon tc = check_arg_type env arg_ctxt rank + | otherwise = check_type env arg_ctxt synArgMonoType + arg_ctxt + | GhciCtxt _ <- ctxt = GhciCtxt False + -- When checking an argument, set the field of GhciCtxt to False to + -- indicate that we are no longer in an outermost position (and thus + -- unsaturated synonyms are no longer allowed). + -- See Note [Unsaturated type synonyms in GHCi] + | otherwise = ctxt + +{- +Note [Unsaturated type synonyms in GHCi] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generally speaking, GHC disallows unsaturated uses of type synonyms or type +families. For instance, if one defines `type Const a b = a`, then GHC will not +permit using `Const` unless it is applied to (at least) two arguments. There is +an exception to this rule, however: GHCi's :kind command. For instance, it +is quite common to look up the kind of a type constructor like so: + + λ> :kind Const + Const :: j -> k -> j + λ> :kind Const Int + Const Int :: k -> Type + +Strictly speaking, the two uses of `Const` above are unsaturated, but this +is an extremely benign (and useful) example of unsaturation, so we allow it +here as a special case. + +That being said, we do not allow unsaturation carte blanche in GHCi. Otherwise, +this GHCi interaction would be possible: + + λ> newtype Fix f = MkFix (f (Fix f)) + λ> type Id a = a + λ> :kind Fix Id + Fix Id :: Type + +This is rather dodgy, so we move to disallow this. We only permit unsaturated +synonyms in GHCi if they are *top-level*—that is, if the synonym is the +outermost type being applied. This allows `Const` and `Const Int` in the +first example, but not `Fix Id` in the second example, as `Id` is not the +outermost type being applied (`Fix` is). + +We track this outermost property in the GhciCtxt constructor of UserTypeCtxt. +A field of True in GhciCtxt indicates that we're in an outermost position. Any +time we invoke `check_arg` to check the validity of an argument, we switch the +field to False. +-} ---------------------------------------- check_ubx_tuple :: TidyEnv -> UserTypeCtxt -> KindOrType @@ -1007,7 +1054,7 @@ okIPCtxt GenSigCtxt = True okIPCtxt (ConArgCtxt {}) = True okIPCtxt (ForSigCtxt {}) = True -- ?? okIPCtxt ThBrackCtxt = True -okIPCtxt GhciCtxt = True +okIPCtxt (GhciCtxt {}) = True okIPCtxt SigmaCtxt = True okIPCtxt (DataTyCtxt {}) = True okIPCtxt (PatSynCtxt {}) = True diff --git a/testsuite/tests/ghci/should_fail/T16013.script b/testsuite/tests/ghci/should_fail/T16013.script new file mode 100644 index 0000000000..287de60656 --- /dev/null +++ b/testsuite/tests/ghci/should_fail/T16013.script @@ -0,0 +1,5 @@ +:set -XTypeFamilies -XPolyKinds +type family Id (a :: k) +type instance Id a = a +type Foo x = Maybe +:kind! Id Foo diff --git a/testsuite/tests/ghci/should_fail/T16013.stderr b/testsuite/tests/ghci/should_fail/T16013.stderr new file mode 100644 index 0000000000..ec60359829 --- /dev/null +++ b/testsuite/tests/ghci/should_fail/T16013.stderr @@ -0,0 +1,3 @@ + +<interactive>:1:1: error: + The type synonym ‘Foo’ should have 1 argument, but has been given none diff --git a/testsuite/tests/ghci/should_fail/all.T b/testsuite/tests/ghci/should_fail/all.T index 01e5c36579..5e0a18c5b8 100644 --- a/testsuite/tests/ghci/should_fail/all.T +++ b/testsuite/tests/ghci/should_fail/all.T @@ -2,3 +2,4 @@ test('T10549', [], ghci_script, ['T10549.script']) test('T10549a', [], ghci_script, ['T10549a.script']) test('T14608', [], ghci_script, ['T14608.script']) test('T15055', normalise_version('ghc'), ghci_script, ['T15055.script']) +test('T16013', [], ghci_script, ['T16013.script']) |