Commit 6b70cf61 authored by Ryan Scott's avatar Ryan Scott

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
parent 6b5ec08a
Pipeline #952 passed with stages
in 607 minutes and 59 seconds
......@@ -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
......
......@@ -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
......
......@@ -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)
......
......@@ -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
......
:set -XTypeFamilies -XPolyKinds
type family Id (a :: k)
type instance Id a = a
type Foo x = Maybe
:kind! Id Foo
<interactive>:1:1: error:
The type synonym ‘Foo’ should have 1 argument, but has been given none
......@@ -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'])
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