Commit c07e7ecb authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Fix #16287 by checking for more unsaturated synonym arguments

Trac #16287 shows that we were checking for unsaturated type synonym
arguments (in `:kind`) when the argument was to a type synonym, but
_not_ when the argument was to some other form of type constructor,
such as a data type. The solution is to use the machinery that
rejects unsaturated type synonym arguments (previously confined to
`check_syn_tc_app`) to `check_arg_type`, which checks these other
forms of arguments. While I was in town, I cleaned up
`check_syn_tc_app` a bit to only invoke `check_arg_type` so as to
minimize the number of different code paths that that function could
go down.
parent 9292a183
......@@ -599,13 +599,13 @@ check_type _ (TyVarTy _) = return ()
check_type ve (AppTy ty1 ty2)
= do { check_type ve ty1
; check_arg_type ve ty2 }
; check_arg_type False ve ty2 }
check_type ve ty@(TyConApp tc tys)
| isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
= check_syn_tc_app ve ty tc tys
| isUnboxedTupleTyCon tc = check_ubx_tuple ve ty tys
| otherwise = mapM_ (check_arg_type ve) tys
| otherwise = mapM_ (check_arg_type False ve) tys
check_type _ (LitTy {}) = return ()
......@@ -693,14 +693,8 @@ check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
tc_arity = tyConArity tc
check_arg :: ExpandMode -> KindOrType -> TcM ()
check_arg expand
| isTypeFamilyTyCon tc
= check_arg_type ve'
| otherwise
= check_type (ve'{ve_rank = synArgMonoType})
where
ve' :: ValidityEnv
ve' = ve{ve_ctxt = arg_ctxt, ve_expand = expand}
check_arg expand =
check_arg_type (isTypeSynonymTyCon tc) (ve{ve_expand = expand})
check_args_only, check_expansion_only :: ExpandMode -> TcM ()
check_args_only expand = mapM_ (check_arg expand) tys
......@@ -713,15 +707,6 @@ check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand })
check_type (ve{ve_expand = expand}) ty'
Nothing -> pprPanic "check_syn_tc_app" (ppr ty)
arg_ctxt :: UserTypeCtxt
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -774,7 +759,9 @@ check_ubx_tuple (ve@ValidityEnv{ve_tidy_env = env}) ty tys
; mapM_ (check_type (ve{ve_rank = rank'})) tys }
----------------------------------------
check_arg_type :: ValidityEnv -> KindOrType -> TcM ()
check_arg_type
:: Bool -- ^ Is this the argument to a type synonym?
-> ValidityEnv -> KindOrType -> TcM ()
-- The sort of type that can instantiate a type variable,
-- or be the argument of a type constructor.
-- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
......@@ -793,11 +780,14 @@ check_arg_type :: ValidityEnv -> KindOrType -> TcM ()
-- But not in user code.
-- Anyway, they are dealt with by a special case in check_tau_type
check_arg_type _ (CoercionTy {}) = return ()
check_arg_type _ _ (CoercionTy {}) = return ()
check_arg_type (ve@ValidityEnv{ve_rank = rank}) ty
check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty
= do { impred <- xoptM LangExt.ImpredicativeTypes
; let rank' = case rank of -- Predictive => must be monotype
-- Rank-n arguments to type synonyms are OK, provided
-- that LiberalTypeSynonyms is enabled.
_ | type_syn -> synArgMonoType
MustBeMonoType -> MustBeMonoType -- Monotype, regardless
_other | impred -> ArbitraryRank
| otherwise -> tyConArgMonoType
......@@ -805,8 +795,17 @@ check_arg_type (ve@ValidityEnv{ve_rank = rank}) ty
-- so that we don't suggest -XImpredicativeTypes in
-- (Ord (forall a.a)) => a -> a
-- and so that if it Must be a monotype, we check that it is!
; check_type (ve{ve_rank = rank'}) ty }
ctxt' :: UserTypeCtxt
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
; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty }
----------------------------------------
forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc)
......
:set -XPolyKinds -XRankNTypes -XTypeFamilies
import Data.Kind
type F1 a = a
type family F2 :: k
data T1 :: (Type -> Type) -> Type
data T2 :: (forall k. k) -> Type
:kind T1 F1
:kind T2 F2
:kind Maybe (T1 F1)
:kind Maybe (T2 F2)
<interactive>:1:1: error:
The type synonym ‘F1’ should have 1 argument, but has been given none
<interactive>:1:1: error:
The type family ‘F2’ should have no arguments, but has been given none
<interactive>:1:1: error:
The type synonym ‘F1’ should have 1 argument, but has been given none
<interactive>:1:1: error:
The type family ‘F2’ should have no arguments, but has been given none
......@@ -3,3 +3,4 @@ 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'])
test('T16287', [], ghci_script, ['T16287.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