From f05f75bff70180e979b7e98db7a3c0cb1a093765 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Wed, 11 Dec 2019 15:58:56 +0000 Subject: Don't zap to Any; error instead This changes GHC's treatment of so-called Naughty Quantification Candidates to issue errors, instead of zapping to Any. Close #16775. No new test cases, because existing ones cover this well. --- compiler/basicTypes/OccName.hs | 7 +- compiler/basicTypes/VarEnv.hs | 9 +- compiler/typecheck/TcHsType.hs | 2 +- compiler/typecheck/TcMType.hs | 123 ++++++++++++++------- compiler/typecheck/TcPatSyn.hs | 4 +- compiler/types/TyCoPpr.hs | 7 +- compiler/types/TyCoTidy.hs | 6 +- compiler/utils/Outputable.hs | 11 +- docs/users_guide/8.12.1-notes.rst | 6 + .../tests/dependent/should_compile/T14880-2.hs | 13 --- testsuite/tests/dependent/should_compile/T14880.hs | 15 --- testsuite/tests/dependent/should_compile/T15076.hs | 13 --- .../tests/dependent/should_compile/T15076b.hs | 11 -- testsuite/tests/dependent/should_compile/all.T | 4 - testsuite/tests/dependent/should_fail/T14880-2.hs | 13 +++ .../tests/dependent/should_fail/T14880-2.stderr | 8 ++ testsuite/tests/dependent/should_fail/T14880.hs | 15 +++ .../tests/dependent/should_fail/T14880.stderr | 12 ++ testsuite/tests/dependent/should_fail/T15076.hs | 13 +++ .../tests/dependent/should_fail/T15076.stderr | 11 ++ testsuite/tests/dependent/should_fail/T15076b.hs | 11 ++ .../tests/dependent/should_fail/T15076b.stderr | 11 ++ .../tests/dependent/should_fail/T15825.stderr | 10 +- testsuite/tests/dependent/should_fail/all.T | 4 + .../tests/partial-sigs/should_fail/T14040a.stderr | 57 ++++------ testsuite/tests/patsyn/should_compile/T14552.hs | 43 ------- testsuite/tests/patsyn/should_compile/all.T | 1 - testsuite/tests/patsyn/should_fail/T14552.hs | 43 +++++++ testsuite/tests/patsyn/should_fail/T14552.stderr | 8 ++ testsuite/tests/patsyn/should_fail/all.T | 1 + testsuite/tests/polykinds/T15795.stderr | 9 ++ testsuite/tests/polykinds/T15795a.stderr | 9 ++ testsuite/tests/polykinds/all.T | 4 +- testsuite/tests/typecheck/should_compile/T16946.hs | 12 -- testsuite/tests/typecheck/should_compile/all.T | 1 - .../tests/typecheck/should_fail/T14350.stderr | 80 +++++++++----- testsuite/tests/typecheck/should_fail/T16946.hs | 12 ++ .../tests/typecheck/should_fail/T16946.stderr | 16 +++ testsuite/tests/typecheck/should_fail/all.T | 1 + 39 files changed, 405 insertions(+), 231 deletions(-) delete mode 100644 testsuite/tests/dependent/should_compile/T14880-2.hs delete mode 100644 testsuite/tests/dependent/should_compile/T14880.hs delete mode 100644 testsuite/tests/dependent/should_compile/T15076.hs delete mode 100644 testsuite/tests/dependent/should_compile/T15076b.hs create mode 100644 testsuite/tests/dependent/should_fail/T14880-2.hs create mode 100644 testsuite/tests/dependent/should_fail/T14880-2.stderr create mode 100644 testsuite/tests/dependent/should_fail/T14880.hs create mode 100644 testsuite/tests/dependent/should_fail/T14880.stderr create mode 100644 testsuite/tests/dependent/should_fail/T15076.hs create mode 100644 testsuite/tests/dependent/should_fail/T15076.stderr create mode 100644 testsuite/tests/dependent/should_fail/T15076b.hs create mode 100644 testsuite/tests/dependent/should_fail/T15076b.stderr delete mode 100644 testsuite/tests/patsyn/should_compile/T14552.hs create mode 100644 testsuite/tests/patsyn/should_fail/T14552.hs create mode 100644 testsuite/tests/patsyn/should_fail/T14552.stderr create mode 100644 testsuite/tests/polykinds/T15795.stderr create mode 100644 testsuite/tests/polykinds/T15795a.stderr delete mode 100644 testsuite/tests/typecheck/should_compile/T16946.hs create mode 100644 testsuite/tests/typecheck/should_fail/T16946.hs create mode 100644 testsuite/tests/typecheck/should_fail/T16946.stderr diff --git a/compiler/basicTypes/OccName.hs b/compiler/basicTypes/OccName.hs index 7584fa4380..ac2ad47100 100644 --- a/compiler/basicTypes/OccName.hs +++ b/compiler/basicTypes/OccName.hs @@ -94,7 +94,7 @@ module OccName ( -- * Tidying up TidyOccEnv, emptyTidyOccEnv, initTidyOccEnv, - tidyOccName, avoidClashesOccEnv, + tidyOccName, avoidClashesOccEnv, delTidyOccEnvList, -- FsEnv FastStringEnv, emptyFsEnv, lookupFsEnv, extendFsEnv, mkFsEnv @@ -818,7 +818,7 @@ Every id contributes a type variable to the type signature, and all of them are (id,id,id) :: (a2 -> a2, a1 -> a1, a -> a) -which is a bit unfortunate, as it unfairly renames only one of them. What we +which is a bit unfortunate, as it unfairly renames only two of them. What we would like to see is (id,id,id) :: (a3 -> a3, a2 -> a2, a1 -> a1) @@ -846,6 +846,9 @@ initTidyOccEnv = foldl' add emptyUFM where add env (OccName _ fs) = addToUFM env fs 1 +delTidyOccEnvList :: TidyOccEnv -> [FastString] -> TidyOccEnv +delTidyOccEnvList = delListFromUFM + -- see Note [Tidying multiple names at once] avoidClashesOccEnv :: TidyOccEnv -> [OccName] -> TidyOccEnv avoidClashesOccEnv env occs = go env emptyUFM occs diff --git a/compiler/basicTypes/VarEnv.hs b/compiler/basicTypes/VarEnv.hs index 4c23b1f141..dfdc933b67 100644 --- a/compiler/basicTypes/VarEnv.hs +++ b/compiler/basicTypes/VarEnv.hs @@ -71,13 +71,14 @@ module VarEnv ( -- * TidyEnv and its operation TidyEnv, - emptyTidyEnv, mkEmptyTidyEnv + emptyTidyEnv, mkEmptyTidyEnv, delTidyEnvList ) where import GhcPrelude import qualified Data.IntMap.Strict as IntMap -- TODO: Move this to UniqFM import OccName +import Name import Var import VarSet import UniqSet @@ -424,6 +425,12 @@ emptyTidyEnv = (emptyTidyOccEnv, emptyVarEnv) mkEmptyTidyEnv :: TidyOccEnv -> TidyEnv mkEmptyTidyEnv occ_env = (occ_env, emptyVarEnv) +delTidyEnvList :: TidyEnv -> [Var] -> TidyEnv +delTidyEnvList (occ_env, var_env) vs = (occ_env', var_env') + where + occ_env' = occ_env `delTidyOccEnvList` map (occNameFS . getOccName) vs + var_env' = var_env `delVarEnvList` vs + {- ************************************************************************ * * diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 17c027318b..61980788cd 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1770,7 +1770,7 @@ the surrounding context, we must obey the following dictum: Every metavariable in a type must either be (A) generalized, or (B) promoted, or See Note [Promotion in signatures] - (C) zapped to Any See Note [Naughty quantification candidates] in TcMType + (C) a cause to error See Note [Naughty quantification candidates] in TcMType The kindGeneralize functions do not require pre-zonking; they zonk as they go. diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 0ac553c0ea..c86e3162c0 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -1137,8 +1137,7 @@ So alpha is entirely unconstrained. What then should we do with alpha? During generalization, every metavariable is either (A) promoted, (B) generalized, or (C) zapped -(according again to Note [Recipe for checking a signature] in -TcHsType). +(according to Note [Recipe for checking a signature] in TcHsType). * We can't generalise it. * We can't promote it, because its kind prevents that @@ -1146,11 +1145,14 @@ TcHsType). go into the typing environment (as the type of some let-bound variable, say), and then chaos erupts when we try to instantiate. -So, we zap it, eagerly, to Any. We don't have to do this eager zapping -in terms (say, in `length []`) because terms are never re-examined before -the final zonk (which zaps any lingering metavariables to Any). +Previously, we zapped it to Any. This worked, but it had the unfortunate +effect of causing Any sometimes to appear in error messages. If this +kind of signature happens, the user probably has made a mistake -- no +one really wants Any in their types. So we now error. This must be +a hard error (failure in the monad) to avoid other messages from mentioning +Any. -We do this eager zapping in candidateQTyVars, which always precedes +We do this eager erroring in candidateQTyVars, which always precedes generalisation, because at that moment we have a clear picture of what skolems are in scope within the type itself (e.g. that 'forall arg'). @@ -1235,13 +1237,14 @@ partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred -- See Note [Dependent type variables] candidateQTyVarsOfType :: TcType -- not necessarily zonked -> TcM CandidatesQTvs -candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty +candidateQTyVarsOfType ty = collect_cand_qtvs ty False emptyVarSet mempty ty -- | Like 'candidateQTyVarsOfType', but over a list of types -- The variables to quantify must have a TcLevel strictly greater than -- the ambient level. (See Wrinkle in Note [Naughty quantification candidates]) candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs -candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys +candidateQTyVarsOfTypes tys = foldlM (\acc ty -> collect_cand_qtvs ty False emptyVarSet acc ty) + mempty tys -- | Like 'candidateQTyVarsOfType', but consider every free variable -- to be dependent. This is appropriate when generalizing a *kind*, @@ -1249,11 +1252,12 @@ candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempt -- to Type.) candidateQTyVarsOfKind :: TcKind -- Not necessarily zonked -> TcM CandidatesQTvs -candidateQTyVarsOfKind ty = collect_cand_qtvs True emptyVarSet mempty ty +candidateQTyVarsOfKind ty = collect_cand_qtvs ty True emptyVarSet mempty ty candidateQTyVarsOfKinds :: [TcKind] -- Not necessarily zonked -> TcM CandidatesQTvs -candidateQTyVarsOfKinds tys = foldM (collect_cand_qtvs True emptyVarSet) mempty tys +candidateQTyVarsOfKinds tys = foldM (\acc ty -> collect_cand_qtvs ty True emptyVarSet acc ty) + mempty tys delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars @@ -1262,7 +1266,8 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars , dv_cvs = cvs `delVarSetList` vars } collect_cand_qtvs - :: Bool -- True <=> consider every fv in Type to be dependent + :: TcType -- original type that we started recurring into; for errors + -> Bool -- True <=> consider every fv in Type to be dependent -> VarSet -- Bound variables (locals only) -> CandidatesQTvs -- Accumulating parameter -> Type -- Not necessarily zonked @@ -1272,14 +1277,14 @@ collect_cand_qtvs -- * Looks through meta-tyvars as it goes; -- no need to zonk in advance -- --- * Needs to be monadic anyway, because it does the zap-naughty --- stuff; see Note [Naughty quantification candidates] +-- * Needs to be monadic anyway, because it handles naughty +-- quantification; see Note [Naughty quantification candidates] -- -- * Returns fully-zonked CandidateQTvs, including their kinds -- so that subsequent dependency analysis (to build a well -- scoped telescope) works correctly -collect_cand_qtvs is_dep bound dvs ty +collect_cand_qtvs orig_ty is_dep bound dvs ty = go dvs ty where is_bound tv = tv `elemVarSet` bound @@ -1292,8 +1297,8 @@ collect_cand_qtvs is_dep bound dvs ty go dv (FunTy _ arg res) = foldlM go dv [arg, res] go dv (LitTy {}) = return dv go dv (CastTy ty co) = do dv1 <- go dv ty - collect_cand_qtvs_co bound dv1 co - go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co + collect_cand_qtvs_co orig_ty bound dv1 co + go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty bound dv co go dv (TyVarTy tv) | is_bound tv = return dv @@ -1303,8 +1308,8 @@ collect_cand_qtvs is_dep bound dvs ty Nothing -> go_tv dv tv } go dv (ForAllTy (Bndr tv _) ty) - = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv) - ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty } + = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv) + ; collect_cand_qtvs orig_ty is_dep (bound `extendVarSet` tv) dv1 ty } ----------------- go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv @@ -1322,25 +1327,23 @@ collect_cand_qtvs is_dep bound dvs ty -- (#15795) and to make the naughty check -- (which comes next) works correctly + ; let tv_kind_vars = tyCoVarsOfType tv_kind ; cur_lvl <- getTcLevel ; if | tcTyVarLevel tv <= cur_lvl -> return dv -- this variable is from an outer context; skip -- See Note [Use level numbers ofor quantification] - | intersectsVarSet bound (tyCoVarsOfType tv_kind) + | intersectsVarSet bound tv_kind_vars -- the tyvar must not be from an outer context, but we have -- already checked for this. -- See Note [Naughty quantification candidates] - -> do { traceTc "Zapping naughty quantifier" $ + -> do { traceTc "Naughty quantifier" $ vcat [ ppr tv <+> dcolon <+> ppr tv_kind , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound) - , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $ - tyCoVarsOfType tv_kind) ] + , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet tv_kind_vars) ] - ; writeMetaTyVar tv (anyTypeOfKind tv_kind) - - -- See Note [Recurring into kinds for candidateQTyVars] - ; collect_cand_qtvs True bound dv tv_kind } + ; let escapees = intersectVarSet bound tv_kind_vars + ; naughtyQuantification orig_ty tv escapees } | otherwise -> do { let tv' = tv `setTyVarKind` tv_kind @@ -1349,15 +1352,16 @@ collect_cand_qtvs is_dep bound dvs ty -- See Note [Order of accumulation] -- See Note [Recurring into kinds for candidateQTyVars] - ; collect_cand_qtvs True bound dv' tv_kind } } + ; collect_cand_qtvs orig_ty True bound dv' tv_kind } } -collect_cand_qtvs_co :: VarSet -- bound variables +collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors + -> VarSet -- bound variables -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs -collect_cand_qtvs_co bound = go_co +collect_cand_qtvs_co orig_ty bound = go_co where - go_co dv (Refl ty) = collect_cand_qtvs True bound dv ty - go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs True bound dv ty + go_co dv (Refl ty) = collect_cand_qtvs orig_ty True bound dv ty + go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs orig_ty True bound dv ty go_mco dv1 mco go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2] @@ -1365,8 +1369,8 @@ collect_cand_qtvs_co bound = go_co go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov - dv2 <- collect_cand_qtvs True bound dv1 t1 - collect_cand_qtvs True bound dv2 t2 + dv2 <- collect_cand_qtvs orig_ty True bound dv1 t1 + collect_cand_qtvs orig_ty True bound dv2 t2 go_co dv (SymCo co) = go_co dv co go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2] go_co dv (NthCo _ _ co) = go_co dv co @@ -1385,7 +1389,7 @@ collect_cand_qtvs_co bound = go_co go_co dv (ForAllCo tcv kind_co co) = do { dv1 <- go_co dv kind_co - ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co } + ; collect_cand_qtvs_co orig_ty (bound `extendVarSet` tcv) dv1 co } go_mco dv MRefl = return dv go_mco dv (MCo co) = go_co dv co @@ -1401,7 +1405,7 @@ collect_cand_qtvs_co bound = go_co | cv `elemVarSet` cvs = return dv -- See Note [Recurring into kinds for candidateQTyVars] - | otherwise = collect_cand_qtvs True bound + | otherwise = collect_cand_qtvs orig_ty True bound (dv { dv_cvs = cvs `extendVarSet` cv }) (idType cv) @@ -2305,8 +2309,8 @@ tidySigSkol env cx ty tv_prs %************************************************************************ %* * Levity polymorphism checks -* * -************************************************************************ +* * +************************************************************************* See Note [Levity polymorphism checking] in DsMonad @@ -2351,3 +2355,48 @@ formatLevPolyErr ty where (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty tidy_ki = tidyType tidy_env (tcTypeKind ty) + +{- +%************************************************************************ +%* * + Error messages +* * +************************************************************************* + +-} + +-- See Note [Naughty quantification candidates] +naughtyQuantification :: TcType -- original type user wanted to quantify + -> TcTyVar -- naughty var + -> TyVarSet -- skolems that would escape + -> TcM a +naughtyQuantification orig_ty tv escapees + = do { orig_ty1 <- zonkTcType orig_ty -- in case it's not zonked + + ; escapees' <- mapM zonkTcTyVarToTyVar $ + nonDetEltsUniqSet escapees + -- we'll just be printing, so no harmful non-determinism + + ; let fvs = tyCoVarsOfTypeWellScoped orig_ty1 + env0 = tidyFreeTyCoVars emptyTidyEnv fvs + env = env0 `delTidyEnvList` escapees' + -- this avoids gratuitous renaming of the escaped + -- variables; very confusing to users! + + orig_ty' = tidyType env orig_ty1 + ppr_tidied = pprTyVars . map (tidyTyCoVarOcc env) + doc = pprWithExplicitKindsWhen True $ + vcat [ sep [ text "Cannot generalise type; skolem" <> plural escapees' + , quotes $ ppr_tidied escapees' + , text "would escape" <+> itsOrTheir escapees' <+> text "scope" + ] + , sep [ text "if I tried to quantify" + , ppr_tidied [tv] + , text "in this type:" + ] + , nest 2 (pprTidiedType orig_ty') + , text "(Indeed, I sometimes struggle even printing this correctly," + , text " due to its ill-scoped nature.)" + ] + + ; failWithTcM (env, doc) } diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 1a6d3ea1e4..6984d06907 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -237,7 +237,7 @@ dependentArgErr (arg, bad_cos) ~~-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider data AST a = Sym [a] - class Prj s where { prj :: [a] -> Maybe (s a) + class Prj s where { prj :: [a] -> Maybe (s a) } pattern P x <= Sym (prj -> Just x) Here we get a matcher with this type @@ -261,7 +261,7 @@ mentions the existentials. We can conveniently do that by making the forall ex_tvs. arg_ty After that, Note [Naughty quantification candidates] in TcMType takes -over, and zonks any such naughty variables to Any. +over and errors. Note [Remove redundant provided dicts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/types/TyCoPpr.hs b/compiler/types/TyCoPpr.hs index fbbdfbd7a0..f7a768210b 100644 --- a/compiler/types/TyCoPpr.hs +++ b/compiler/types/TyCoPpr.hs @@ -5,7 +5,7 @@ module TyCoPpr PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen, -- * Pretty-printing types - pprType, pprParendType, pprPrecType, pprPrecTypeX, + pprType, pprParendType, pprTidiedType, pprPrecType, pprPrecTypeX, pprTypeApp, pprTCvBndr, pprTCvBndrs, pprSigmaType, pprTheta, pprParendTheta, pprForAll, pprUserForAll, @@ -81,10 +81,13 @@ See Note [Precedence in types] in BasicTypes. -- See Note [Pretty printing via Iface syntax] in PprTyThing -------------------------------------------------------- -pprType, pprParendType :: Type -> SDoc +pprType, pprParendType, pprTidiedType :: Type -> SDoc pprType = pprPrecType topPrec pprParendType = pprPrecType appPrec +-- already pre-tidied +pprTidiedType = pprIfaceType . toIfaceTypeX emptyVarSet + pprPrecType :: PprPrec -> Type -> SDoc pprPrecType = pprPrecTypeX emptyTidyEnv diff --git a/compiler/types/TyCoTidy.hs b/compiler/types/TyCoTidy.hs index f4639ca303..b6f87c2230 100644 --- a/compiler/types/TyCoTidy.hs +++ b/compiler/types/TyCoTidy.hs @@ -95,8 +95,8 @@ tidyTyCoVarBinders tidy_env tvbs tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv -- ^ Add the free 'TyVar's to the env in tidy form, -- so that we can tidy the type they are free in -tidyFreeTyCoVars (full_occ_env, var_env) tyvars - = fst (tidyOpenTyCoVars (full_occ_env, var_env) tyvars) +tidyFreeTyCoVars tidy_env tyvars + = fst (tidyOpenTyCoVars tidy_env tyvars) --------------- tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) @@ -232,5 +232,3 @@ tidyCo env@(_, subst) co tidyCos :: TidyEnv -> [Coercion] -> [Coercion] tidyCos env = map (tidyCo env) - - diff --git a/compiler/utils/Outputable.hs b/compiler/utils/Outputable.hs index d81c754866..02805c6c7c 100644 --- a/compiler/utils/Outputable.hs +++ b/compiler/utils/Outputable.hs @@ -34,7 +34,7 @@ module Outputable ( sep, cat, fsep, fcat, hang, hangNotEmpty, punctuate, ppWhen, ppUnless, - speakNth, speakN, speakNOf, plural, isOrAre, doOrDoes, + speakNth, speakN, speakNOf, plural, isOrAre, doOrDoes, itsOrTheir, unicodeSyntax, coloured, keyword, @@ -1160,6 +1160,15 @@ doOrDoes :: [a] -> SDoc doOrDoes [_] = text "does" doOrDoes _ = text "do" +-- | Determines the form of possessive appropriate for the length of a list: +-- +-- > itsOrTheir [x] = text "its" +-- > itsOrTheir [x,y] = text "their" +-- > itsOrTheir [] = text "their" -- probably avoid this +itsOrTheir :: [a] -> SDoc +itsOrTheir [_] = text "its" +itsOrTheir _ = text "their" + {- ************************************************************************ * * diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst index 69890b2c10..95a0096c69 100644 --- a/docs/users_guide/8.12.1-notes.rst +++ b/docs/users_guide/8.12.1-notes.rst @@ -18,6 +18,12 @@ Full details Language ~~~~~~~~ +* In obscure scenarios, GHC now rejects programs it previously accepted, but + with unhelpful types. For example, if (with ``-XPartialTypeSignatures``) you + were to write ``x :: forall (f :: forall a (b :: a -> Type). b _). f _``, GHC previously + would have accepted ``x``, but its type would have involved the mysterious ``Any`` + internal type family. Now, GHC rejects, explaining the situation. + Compiler ~~~~~~~~ diff --git a/testsuite/tests/dependent/should_compile/T14880-2.hs b/testsuite/tests/dependent/should_compile/T14880-2.hs deleted file mode 100644 index e7057a3f00..0000000000 --- a/testsuite/tests/dependent/should_compile/T14880-2.hs +++ /dev/null @@ -1,13 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE PartialTypeSignatures #-} -module Bug where - -import Data.Kind -import Data.Proxy - -data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type - -quux :: forall arg. Proxy (Foo arg) -> () -quux (_ :: _) = () diff --git a/testsuite/tests/dependent/should_compile/T14880.hs b/testsuite/tests/dependent/should_compile/T14880.hs deleted file mode 100644 index 91cfb20a4a..0000000000 --- a/testsuite/tests/dependent/should_compile/T14880.hs +++ /dev/null @@ -1,15 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -module Bug where - -import Data.Kind -import Data.Proxy - -data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type - -data Bar :: Type -> Type where - MkBar :: forall x arg. - -- Commenting out the line below makes the issue go away - Foo arg ~ Foo arg => - Bar x diff --git a/testsuite/tests/dependent/should_compile/T15076.hs b/testsuite/tests/dependent/should_compile/T15076.hs deleted file mode 100644 index 0890cf9eab..0000000000 --- a/testsuite/tests/dependent/should_compile/T15076.hs +++ /dev/null @@ -1,13 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE PartialTypeSignatures #-} -module Bug where - -import Data.Kind -import Data.Proxy - -foo :: forall (a :: Type) - (f :: forall (x :: a). Proxy x -> Type). - Proxy f -> () -foo (_ :: _) = () diff --git a/testsuite/tests/dependent/should_compile/T15076b.hs b/testsuite/tests/dependent/should_compile/T15076b.hs deleted file mode 100644 index 15fce826c0..0000000000 --- a/testsuite/tests/dependent/should_compile/T15076b.hs +++ /dev/null @@ -1,11 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeInType #-} -module Bug where - -import Data.Kind -import Data.Proxy - -foo :: forall (a :: Type) - (f :: forall (x :: a). Proxy x -> Type). - Proxy f -> () -foo _ = () diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index 823244ebca..6cc9f12bca 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -54,13 +54,9 @@ test('T15419', normal, compile, ['']) test('T14066h', normal, compile, ['']) test('T15666', normal, compile, ['']) test('T15725', normal, compile, ['']) -test('T14880', normal, compile, ['']) -test('T14880-2', normal, compile, ['']) test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls']) test('InferDependency', normal, compile, ['']) test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls']) -test('T15076', normal, compile, ['']) -test('T15076b', normal, compile, ['']) test('T15076c', normal, compile, ['']) test('T15829', normal, compile, ['']) test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -fprint-explicit-coercions']) diff --git a/testsuite/tests/dependent/should_fail/T14880-2.hs b/testsuite/tests/dependent/should_fail/T14880-2.hs new file mode 100644 index 0000000000..e7057a3f00 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T14880-2.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PartialTypeSignatures #-} +module Bug where + +import Data.Kind +import Data.Proxy + +data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type + +quux :: forall arg. Proxy (Foo arg) -> () +quux (_ :: _) = () diff --git a/testsuite/tests/dependent/should_fail/T14880-2.stderr b/testsuite/tests/dependent/should_fail/T14880-2.stderr new file mode 100644 index 0000000000..2082ca6c34 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T14880-2.stderr @@ -0,0 +1,8 @@ + +T14880-2.hs:12:9: error: + • Cannot generalise type; skolem ‘arg’ would escape its scope + if I tried to quantify (a0 :: arg) in this type: + forall arg. Proxy @{Proxy @{arg} a0 -> *} (Foo arg @a0) -> () + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: quux :: forall arg. Proxy (Foo arg) -> () diff --git a/testsuite/tests/dependent/should_fail/T14880.hs b/testsuite/tests/dependent/should_fail/T14880.hs new file mode 100644 index 0000000000..91cfb20a4a --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T14880.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +module Bug where + +import Data.Kind +import Data.Proxy + +data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type + +data Bar :: Type -> Type where + MkBar :: forall x arg. + -- Commenting out the line below makes the issue go away + Foo arg ~ Foo arg => + Bar x diff --git a/testsuite/tests/dependent/should_fail/T14880.stderr b/testsuite/tests/dependent/should_fail/T14880.stderr new file mode 100644 index 0000000000..a5aa1df8d2 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T14880.stderr @@ -0,0 +1,12 @@ + +T14880.hs:12:5: error: + • Cannot generalise type; skolem ‘arg’ would escape its scope + if I tried to quantify (a0 :: arg) in this type: + forall x arg. + ((Foo arg @a0 :: (Proxy @{arg} a0 -> *)) + ~ (Foo arg @a0 :: (Proxy @{arg} a0 -> *))) => + Bar x + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘MkBar’ + In the data declaration for ‘Bar’ diff --git a/testsuite/tests/dependent/should_fail/T15076.hs b/testsuite/tests/dependent/should_fail/T15076.hs new file mode 100644 index 0000000000..0890cf9eab --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15076.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PartialTypeSignatures #-} +module Bug where + +import Data.Kind +import Data.Proxy + +foo :: forall (a :: Type) + (f :: forall (x :: a). Proxy x -> Type). + Proxy f -> () +foo (_ :: _) = () diff --git a/testsuite/tests/dependent/should_fail/T15076.stderr b/testsuite/tests/dependent/should_fail/T15076.stderr new file mode 100644 index 0000000000..814d459c3c --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15076.stderr @@ -0,0 +1,11 @@ + +T15076.hs:10:8: error: + • Cannot generalise type; skolem ‘a’ would escape its scope + if I tried to quantify (x0 :: a) in this type: + forall a (f :: forall (x :: a). Proxy @{a} x -> *). + Proxy @{Proxy @{a} x0 -> *} (f @x0) -> () + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). + Proxy f -> () diff --git a/testsuite/tests/dependent/should_fail/T15076b.hs b/testsuite/tests/dependent/should_fail/T15076b.hs new file mode 100644 index 0000000000..15fce826c0 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15076b.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeInType #-} +module Bug where + +import Data.Kind +import Data.Proxy + +foo :: forall (a :: Type) + (f :: forall (x :: a). Proxy x -> Type). + Proxy f -> () +foo _ = () diff --git a/testsuite/tests/dependent/should_fail/T15076b.stderr b/testsuite/tests/dependent/should_fail/T15076b.stderr new file mode 100644 index 0000000000..3ee27a82b3 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15076b.stderr @@ -0,0 +1,11 @@ + +T15076b.hs:8:8: error: + • Cannot generalise type; skolem ‘a’ would escape its scope + if I tried to quantify (x0 :: a) in this type: + forall a (f :: forall (x :: a). Proxy @{a} x -> *). + Proxy @{Proxy @{a} x0 -> *} (f @x0) -> () + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). + Proxy f -> () diff --git a/testsuite/tests/dependent/should_fail/T15825.stderr b/testsuite/tests/dependent/should_fail/T15825.stderr index 97582ba952..5d989303a6 100644 --- a/testsuite/tests/dependent/should_fail/T15825.stderr +++ b/testsuite/tests/dependent/should_fail/T15825.stderr @@ -1,6 +1,8 @@ -T15825.hs:14:31: error: - • Illegal type synonym family application ‘GHC.Types.Any - @k’ in instance: - X (a @(GHC.Types.Any @k)) +T15825.hs:14:10: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (x0 :: k) in this type: + forall k (a :: C k). X (a @x0) + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) • In the instance declaration for ‘X (a :: *)’ diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 8ff5a88961..dde686af7a 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -60,3 +60,7 @@ test('T16418', normal, compile_fail, ['']) test('T17541', normal, compile_fail, ['']) test('T17541b', normal, compile_fail, ['']) test('T17131', normal, compile_fail, ['']) +test('T14880', normal, compile_fail, ['']) +test('T14880-2', normal, compile_fail, ['']) +test('T15076', normal, compile_fail, ['']) +test('T15076b', normal, compile_fail, ['']) diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index d03d0dc32b..1d122cf590 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,34 +1,25 @@ -T14040a.hs:34:8: error: - • Cannot apply expression of type ‘Sing wl - -> (forall y. p _0 'WeirdNil) - -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). - Sing x - -> Sing xs - -> p GHC.Types.Any xs - -> p GHC.Types.Any ('WeirdCons x xs)) - -> p _1 wl’ - to a visible type argument ‘(WeirdList z)’ - • In the sixth argument of ‘pWeirdCons’, namely - ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ - In the expression: - pWeirdCons - @z - @x - @xs - x - xs - (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) - In an equation for ‘elimWeirdList’: - elimWeirdList - (SWeirdCons (x :: Sing (x :: z)) - (xs :: Sing (xs :: WeirdList (WeirdList z)))) - pWeirdNil - pWeirdCons - = pWeirdCons - @z - @x - @xs - x - xs - (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) +T14040a.hs:21:18: error: + • Cannot generalise type; skolem ‘z’ would escape its scope + if I tried to quantify (_1 :: WeirdList z) in this type: + forall a1 (wl :: WeirdList a1) + (p :: forall x. x -> WeirdList x -> *). + Sing @(WeirdList a1) wl + -> (forall y. p @x0 _0 ('WeirdNil @x0)) + -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). + Sing @z x + -> Sing @(WeirdList (WeirdList z)) xs + -> p @(WeirdList z) _1 xs + -> p @z _2 ('WeirdCons @z x xs)) + -> p @a1 _3 wl + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + elimWeirdList :: forall (a :: Type) + (wl :: WeirdList a) + (p :: forall (x :: Type). x -> WeirdList x -> Type). + Sing wl + -> (forall (y :: Type). p _ WeirdNil) + -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). + Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) + -> p _ wl diff --git a/testsuite/tests/patsyn/should_compile/T14552.hs b/testsuite/tests/patsyn/should_compile/T14552.hs deleted file mode 100644 index a4a7493530..0000000000 --- a/testsuite/tests/patsyn/should_compile/T14552.hs +++ /dev/null @@ -1,43 +0,0 @@ -{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, ScopedTypeVariables, - KindSignatures, PolyKinds, DataKinds, TypeFamilies, GADTs #-} - -module T14552 where - -import Data.Kind -import Data.Proxy - -data family Sing a - -type a --> b = (a, b) -> Type - -type family F (f::a --> b) (x::a) :: b - -newtype Limit :: (k --> Type) -> Type where - Limit :: (forall xx. Proxy xx -> F f xx) -> Limit f - -data Exp :: [Type] -> Type -> Type where - TLam :: (forall aa. Proxy aa -> Exp xs (F w aa)) - -> Exp xs (Limit w) - -pattern FOO f <- TLam (($ Proxy) -> f) - - -{- -TLam :: forall (xs::[Type]) (b::Type). -- Universal - forall k (w :: k --> Type). -- Existential - (b ~ Limit w) => - => (forall (aa :: k). Proxy aa -> Exp xs (F w aa)) - -> Exp xs b - --} - -{- -mfoo :: Exp xs b - -> (forall k (w :: k --> Type). - (b ~ Limit w) - => Exp xs (F w aa) - -> r) - -> r -mfoo scrut k = case srcut of - TLam g -> k (g Proxy) --} diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 2ac343f635..6ef1928768 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -75,7 +75,6 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])], multimod_compile, ['T14058', '-v0']) test('T14326', normal, compile, ['']) test('T14394', normal, ghci_script, ['T14394.script']) -test('T14552', normal, compile, ['']) test('T14498', normal, compile, ['']) test('T16682', [extra_files(['T16682.hs', 'T16682a.hs'])], multimod_compile, ['T16682', '-v0 -fwarn-incomplete-patterns -fno-code']) diff --git a/testsuite/tests/patsyn/should_fail/T14552.hs b/testsuite/tests/patsyn/should_fail/T14552.hs new file mode 100644 index 0000000000..a4a7493530 --- /dev/null +++ b/testsuite/tests/patsyn/should_fail/T14552.hs @@ -0,0 +1,43 @@ +{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, ScopedTypeVariables, + KindSignatures, PolyKinds, DataKinds, TypeFamilies, GADTs #-} + +module T14552 where + +import Data.Kind +import Data.Proxy + +data family Sing a + +type a --> b = (a, b) -> Type + +type family F (f::a --> b) (x::a) :: b + +newtype Limit :: (k --> Type) -> Type where + Limit :: (forall xx. Proxy xx -> F f xx) -> Limit f + +data Exp :: [Type] -> Type -> Type where + TLam :: (forall aa. Proxy aa -> Exp xs (F w aa)) + -> Exp xs (Limit w) + +pattern FOO f <- TLam (($ Proxy) -> f) + + +{- +TLam :: forall (xs::[Type]) (b::Type). -- Universal + forall k (w :: k --> Type). -- Existential + (b ~ Limit w) => + => (forall (aa :: k). Proxy aa -> Exp xs (F w aa)) + -> Exp xs b + +-} + +{- +mfoo :: Exp xs b + -> (forall k (w :: k --> Type). + (b ~ Limit w) + => Exp xs (F w aa) + -> r) + -> r +mfoo scrut k = case srcut of + TLam g -> k (g Proxy) +-} diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr new file mode 100644 index 0000000000..b9b6b8448b --- /dev/null +++ b/testsuite/tests/patsyn/should_fail/T14552.stderr @@ -0,0 +1,8 @@ + +T14552.hs:22:9: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (aa0 :: k) in this type: + forall k (w :: k --> *). Exp a0 (F @k @(*) w aa0) + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the declaration for pattern synonym ‘FOO’ diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T index 27ebc8bdd4..02cc2cec2c 100644 --- a/testsuite/tests/patsyn/should_fail/all.T +++ b/testsuite/tests/patsyn/should_fail/all.T @@ -46,3 +46,4 @@ test('T15685', normal, compile_fail, ['']) test('T15692', normal, compile, ['']) # It has -fdefer-type-errors inside test('T15694', normal, compile_fail, ['']) test('T16900', normal, compile_fail, ['-fdiagnostics-show-caret']) +test('T14552', normal, compile_fail, ['']) diff --git a/testsuite/tests/polykinds/T15795.stderr b/testsuite/tests/polykinds/T15795.stderr new file mode 100644 index 0000000000..65bfdddecc --- /dev/null +++ b/testsuite/tests/polykinds/T15795.stderr @@ -0,0 +1,9 @@ + +T15795.hs:12:3: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (a0 :: k) in this type: + forall k (b :: k). T @k @a0 b + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘MkT’ + In the data declaration for ‘T’ diff --git a/testsuite/tests/polykinds/T15795a.stderr b/testsuite/tests/polykinds/T15795a.stderr new file mode 100644 index 0000000000..f4757137ce --- /dev/null +++ b/testsuite/tests/polykinds/T15795a.stderr @@ -0,0 +1,9 @@ + +T15795a.hs:9:3: error: + • Cannot generalise type; skolem ‘u’ would escape its scope + if I tried to quantify (cat10 :: u) in this type: + forall u (a :: u). F @u @cat10 a + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘Prod’ + In the data declaration for ‘F’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 74ab266308..4312691755 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -204,8 +204,8 @@ test('T15817', normal, compile, ['']) test('T15874', normal, compile, ['']) test('T14887a', normal, compile, ['']) test('T14847', normal, compile, ['']) -test('T15795', normal, compile, ['']) -test('T15795a', normal, compile, ['']) +test('T15795', normal, compile_fail, ['']) +test('T15795a', normal, compile_fail, ['']) test('T16247', normal, compile_fail, ['']) test('T16247a', normal, compile_fail, ['']) test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script']) diff --git a/testsuite/tests/typecheck/should_compile/T16946.hs b/testsuite/tests/typecheck/should_compile/T16946.hs deleted file mode 100644 index e824f7cec8..0000000000 --- a/testsuite/tests/typecheck/should_compile/T16946.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, FunctionalDependencies #-} -module T16946 where - -import Data.Kind - -class CatMonad (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) | c -> m where - type Id c :: c x x - - xpure :: a -> m (Id c) a - -boom :: forall k (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) a. CatMonad c m => a -> m (Id c) a -boom = xpure diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index c51ff0b36b..80b11ca851 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -685,7 +685,6 @@ test('UnlifNewUnify', normal, compile, ['']) test('UnliftedNewtypesLPFamily', normal, compile, ['']) test('UnliftedNewtypesDifficultUnification', normal, compile, ['']) test('T16832', normal, ghci_script, ['T16832.script']) -test('T16946', normal, compile, ['']) test('T16995', normal, compile, ['']) test('T17007', normal, compile, ['']) test('T17067', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T14350.stderr b/testsuite/tests/typecheck/should_fail/T14350.stderr index eb80d3ec80..955554ab8d 100644 --- a/testsuite/tests/typecheck/should_fail/T14350.stderr +++ b/testsuite/tests/typecheck/should_fail/T14350.stderr @@ -1,30 +1,52 @@ -T14350.hs:59:15: error: - • Couldn't match expected type ‘Proxy a1 - -> Apply (Apply c 'Proxy) (Apply g 'Proxy)’ - with actual type ‘Sing (f @@ t0)’ - • The function ‘applySing’ is applied to three arguments, - but its type ‘Sing f -> Sing t0 -> Sing (f @@ t0)’ has only two - In the expression: applySing f Proxy Proxy - In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy - • Relevant bindings include - x :: Sing x (bound at T14350.hs:59:11) - g :: Sing g (bound at T14350.hs:59:9) - f :: Sing f (bound at T14350.hs:59:7) - dcomp :: Sing f - -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy) - (bound at T14350.hs:59:1) - -T14350.hs:59:27: error: - • Couldn't match expected type ‘Sing t0’ - with actual type ‘Proxy a0’ - • In the second argument of ‘applySing’, namely ‘Proxy’ - In the expression: applySing f Proxy Proxy - In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy - • Relevant bindings include - x :: Sing x (bound at T14350.hs:59:11) - g :: Sing g (bound at T14350.hs:59:9) - f :: Sing f (bound at T14350.hs:59:7) - dcomp :: Sing f - -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy) - (bound at T14350.hs:59:1) +T14350.hs:49:10: error: + • Cannot generalise type; skolem ‘a’ would escape its scope + if I tried to quantify (x0 :: a) in this type: + forall a (b1 :: a ~> *) + (c :: forall (x :: a). Proxy @{a} x ~> ((@@) @{*} @{a} b1 x ~> *)) + (f :: forall (x :: a) (y :: (@@) @{*} @{a} b1 x). + Proxy @{a} x + ~> (Proxy @{Apply @a @(*) b1 x} y + ~> (@@) + @{*} + @{Apply @a @(*) b1 x} + ((@@) + @{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x)) + y)) + (g :: forall (x :: a). Proxy @{a} x ~> (@@) @{*} @{a} b1 x) + (x :: a). + Sing + @(Proxy @{a} x0 + ~> (Proxy @{Apply @a @(*) b1 x0} y0 + ~> Apply + @(Apply @a @(*) b1 x0) + @(*) + (Apply + @(Proxy @{a} x0) + @(Apply @a @(*) b1 x0 ~> *) + (c @x0) + ('Proxy @{a} @x0)) + y0)) + (f @x0 @y0) + -> Sing @(Proxy @{a} x1 ~> Apply @a @(*) b1 x1) (g @x1) + -> Sing @a x + -> (@@) + @{*} + @{Apply @a @(*) b1 x} + ((@@) + @{Apply @a @(*) b1 x ~> *} @{Proxy @{a} x} (c @x) ('Proxy @{a} @x)) + ((@@) + @{Apply @a @(*) b1 x} @{Proxy @{a} x} (g @x) ('Proxy @{a} @x)) + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + dcomp :: forall (a :: Type) + (b :: a ~> Type) + (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type) + (f :: forall (x :: a) (y :: b @@ x). + Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y) + (g :: forall (x :: a). Proxy x ~> b @@ x) + (x :: a). + Sing f + -> Sing g + -> Sing x -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)) diff --git a/testsuite/tests/typecheck/should_fail/T16946.hs b/testsuite/tests/typecheck/should_fail/T16946.hs new file mode 100644 index 0000000000..e824f7cec8 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16946.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, FunctionalDependencies #-} +module T16946 where + +import Data.Kind + +class CatMonad (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) | c -> m where + type Id c :: c x x + + xpure :: a -> m (Id c) a + +boom :: forall k (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) a. CatMonad c m => a -> m (Id c) a +boom = xpure diff --git a/testsuite/tests/typecheck/should_fail/T16946.stderr b/testsuite/tests/typecheck/should_fail/T16946.stderr new file mode 100644 index 0000000000..a923fe778e --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T16946.stderr @@ -0,0 +1,16 @@ + +T16946.hs:11:9: error: + • Cannot generalise type; skolem ‘k’ would escape its scope + if I tried to quantify (y0 :: k) in this type: + forall k (c :: k -> k -> *) + (m :: forall (x :: k) (y :: k). c x y -> * -> *) a. + CatMonad @k c m => + a -> m @y0 @y0 (Id @{k} @y0 c) a + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the type signature: + boom :: forall k + (c :: k -> k -> Type) + (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) + a. + CatMonad c m => a -> m (Id c) a diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index e46f694dd3..e11c239742 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -549,3 +549,4 @@ test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', test('T17355', normal, compile_fail, ['']) test('T17360', normal, compile_fail, ['']) test('T17563', normal, compile_fail, ['']) +test('T16946', normal, compile_fail, ['']) -- cgit v1.2.1