diff options
Diffstat (limited to 'compiler/typecheck/TcValidity.hs')
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 69 |
1 files changed, 66 insertions, 3 deletions
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 8ab63f49cc..d17ac0f567 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -464,6 +464,55 @@ allConstraintsAllowed (TySynKindCtxt {}) = False allConstraintsAllowed (TyFamResKindCtxt {}) = False allConstraintsAllowed _ = 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. +-- +-- An example of something that is unambiguously the type of a term is the +-- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the +-- same type in @type family Foo :: forall a -> a -> a@ is unambiguously the +-- kind of a type, not the type of a term, so it is permitted. +-- +-- For more examples, see +-- @testsuite/tests/dependent/should_compile/T16326_Compile*.hs@ (for places +-- where VDQ is permitted) and +-- @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 (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 + {- Note [Correctness and performance of type synonym validity checking] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -615,9 +664,8 @@ check_type ve (CastTy ty _) = check_type ve ty -- -- Critically, this case must come *after* the case for TyConApp. -- See Note [Liberal type synonyms]. -check_type ve@(ValidityEnv{ ve_tidy_env = env - , ve_rank = rank - , ve_expand = expand }) ty +check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt + , ve_rank = rank, ve_expand = expand }) ty | not (null tvbs && null theta) = do { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank)) ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty) @@ -628,6 +676,12 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env -- Reject forall (a :: Eq b => b). blah -- In a kind signature we don't allow constraints + ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs + || vdqAllowed ctxt) + (illegalVDQTyErr env ty) + -- Reject visible, dependent quantification in the type of a + -- term (e.g., `f :: forall a -> a -> Maybe a`) + ; check_valid_theta env' SigmaCtxt expand theta -- Allow type T = ?x::Int => Int -> Int -- but not type T = ?x::Int @@ -851,6 +905,15 @@ constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) constraintTyErr env ty = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty) +-- | Reject a use of visible, dependent quantification in the type of a term. +illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) +illegalVDQTyErr env ty = + (env, vcat + [ hang (text "Illegal visible, dependent quantification" <+> + text "in the type of a term:") + 2 (ppr_tidy env ty) + , text "(GHC does not yet support this)" ] ) + {- Note [Liberal type synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |