diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2016-09-20 23:31:07 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2016-10-21 17:15:48 +0100 |
| commit | 3f5673f34a2f761423027bf46f64f7499708725f (patch) | |
| tree | 6ea3cd863d8f71376727cc7e319817a1533ff33a | |
| parent | d61c7e8d418331e4db783dace9c7ad75306ce05a (diff) | |
| download | haskell-3f5673f34a2f761423027bf46f64f7499708725f.tar.gz | |
A collection of type-inference refactorings.
This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.
1. Modify TcType.ExpType to make a distinct data type,
InferResult for the Infer case, and consequential
refactoring.
2. Define a new function TcUnify.fillInferResult, to fill in
an InferResult. It uses TcMType.promoteTcType to promote
the type to the level of the InferResult.
See TcMType Note [Promoting a type]
This refactoring is in preparation for an improvement
to typechecking pattern bindings, coming next.
I flirted with an elaborate scheme to give better
higher rank inference, but it was just too complicated.
See TcMType Note [Promotion and higher rank types]
3. Add to InferResult a new field ir_inst :: Bool to say
whether or not the type used to fill in the
InferResult should be deeply instantiated. See
TcUnify Note [Deep instantiation of InferResult].
4. Add a TcLevel to SkolemTvs. This will be useful generally
- it's a fast way to see if the type
variable escapes when floating (not used yet)
- it provides a good consistency check when updating a
unification variable (TcMType.writeMetaTyVarRef, the
level_check_ok check)
I originally had another reason (related to the flirting
in (2), but I left it in because it seems like a step in
the right direction.
5. Reduce and simplify the plethora of uExpType,
tcSubType and related functions in TcUnify. It was
such an opaque mess and it's still not great, but it's
better.
6. Simplify the uo_expected field of TypeEqOrigin. Richard
had generatlised it to a ExpType, but it was almost always
a Check type. Now it's back to being a plain TcType which
is much, much easier.
7. Improve error messages by refraining from skolemisation when
it's clear that there's an error: see
TcUnify Note [Don't skolemise unnecessarily]
8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
so I added it
9. Kill off tcs_used_tcvs. Its purpose is to track the
givens used by wanted constraints. For dictionaries etc
we do that via the free vars of the /bindings/ in the
implication constraint ic_binds. But for coercions we
just do update-in-place in the type, rather than
generating a binding. So we need something analogous to
bindings, to track what coercions we have added.
That was the purpose of tcs_used_tcvs. But it only
worked for a /single/ iteration, whereas we may have
multiple iterations of solving an implication. Look
at (the old) 'setImplicationStatus'. If the constraint
is unsolved, it just drops the used_tvs on the floor.
If it becomes solved next time round, we'll pick up
coercions used in that round, but ignore ones used in
the first round.
There was an outright bug. Result = (potentialy) bogus
unused-constraint errors. Constructing a case where this
actually happens seems quite trick so I did not do so.
Solution: expand EvBindsVar to include the (free vars of
the) coercions, so that the coercions are tracked in
essentially the same way as the bindings.
This turned out to be much simpler. Less code, more
correct.
10. Make the ic_binds field in an implication have type
ic_binds :: EvBindsVar
instead of (as previously)
ic_binds :: Maybe EvBindsVar
This is notably simpler, and faster to use -- less
testing of the Maybe. But in the occaional situation
where we don't have anywhere to put the bindings, the
belt-and-braces error check is lost. So I put it back
as an ASSERT in 'setImplicationStatus' (see the use of
'termEvidenceAllowed')
All these changes led to quite bit of error message wibbling
79 files changed, 1322 insertions, 859 deletions
diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 9f671f21dc..eff266090e 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -1218,7 +1218,7 @@ zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta) where zonk_unbound_meta tv = ASSERT( isTcTyVar tv ) - do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk + do { tv' <- skolemiseRuntimeUnk tv -- This is where RuntimeUnks are born: -- otherwise-unconstrained unification variables are -- turned into RuntimeUnks as they leave the diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index f2d3ef014d..e5b802063b 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -225,7 +225,7 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- if deeplyInstantiate ty = (wrap, rho) -- and e :: ty -- then wrap e :: rho --- That is, wrap :: ty "->" rho +-- That is, wrap :: ty ~> rho deeplyInstantiate orig ty | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty @@ -381,7 +381,7 @@ tcInstBinderX _ subst (Anon ty) -- This is the *only* constraint currently handled in types. | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty = do { let origin = TypeEqOrigin { uo_actual = k1 - , uo_expected = mkCheckExpType k2 + , uo_expected = k2 , uo_thing = Nothing } ; co <- case role of Nominal -> unifyKind noThing k1 k2 diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index 8fba643433..09746d3cba 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -33,7 +33,6 @@ import TcEvidence import TcHsType import TcPat import TcMType -import Inst( deeplyInstantiate ) import FamInstEnv( normaliseType ) import FamInst( tcGetFamInstEnvs ) import TyCon @@ -741,7 +740,7 @@ mkExport prag_fn qtvs theta -- an ambiguouse type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int else addErrCtxtM (mk_impedence_match_msg mono_info sel_poly_ty poly_ty) $ - tcSubType_NC sig_ctxt sel_poly_ty (mkCheckExpType poly_ty) + tcSubType_NC sig_ctxt sel_poly_ty poly_ty ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures ; when warn_missing_sigs $ @@ -1117,58 +1116,6 @@ for a non-overloaded function. @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds. The signatures have been dealt with already. - -Note [Pattern bindings] -~~~~~~~~~~~~~~~~~~~~~~~ -The rule for typing pattern bindings is this: - - ..sigs.. - p = e - -where 'p' binds v1..vn, and 'e' may mention v1..vn, -typechecks exactly like - - ..sigs.. - x = e -- Inferred type - v1 = case x of p -> v1 - .. - vn = case x of p -> vn - -Note that - (f :: forall a. a -> a) = id -should not typecheck because - case id of { (f :: forall a. a->a) -> f } -will not typecheck. - -Note [Instantiate when inferring a type] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - f = (*) -As there is no incentive to instantiate the RHS, tcMonoBinds will -produce a type of forall a. Num a => a -> a -> a for `f`. This will then go -through simplifyInfer and such, remaining unchanged. - -There are two problems with this: - 1) If the definition were `g _ = (*)`, we get a very unusual type of - `forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is - surely confusing for users. - - 2) The monomorphism restriction can't work. The MR is dealt with in - simplifyInfer, and simplifyInfer has no way of instantiating. This - could perhaps be worked around, but it may be hard to know even - when instantiation should happen. - -There is an easy solution to both problems: instantiate (deeply) when -inferring a type. So that's what we do. Note that this decision is -user-facing. - -We do this deep instantiation in tcMonoBinds, in the FunBind case -only, and only when we do not have a type signature. Conveniently, -the fun_co_fn field of FunBind gives a place to record the coercion. - -We do not need to do this - * for PatBinds, because we don't have a function type - * for FunBinds where we have a signature, bucause we aren't doing inference -} data MonoBindInfo = MBI { mbi_poly_name :: Name @@ -1193,27 +1140,21 @@ tcMonoBinds is_rec sig_fn no_gen -- e.g. f = \(x::forall a. a->a) -> <body> -- We want to infer a higher-rank type for f setSrcSpan b_loc $ - do { rhs_ty <- newOpenInferExpType - ; (co_fn, matches') - <- tcExtendIdBndrs [TcIdBndr_ExpType name rhs_ty NotTopLevel] $ + do { ((co_fn, matches'), rhs_ty) + <- tcInferInst $ \ exp_ty -> + -- tcInferInst: see TcUnify, + -- Note [Deep instantiation of InferResult] + tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $ -- We extend the error context even for a non-recursive -- function so that in type error messages we show the -- type of the thing whose rhs we are type checking - tcMatchesFun (L nm_loc name) matches rhs_ty - ; rhs_ty <- readExpType rhs_ty - - -- Deeply instantiate the inferred type - -- See Note [Instantiate when inferring a type] - ; let orig = matchesCtOrigin matches - ; rhs_ty <- zonkTcType rhs_ty -- NB: zonk to uncover any foralls - ; (inst_wrap, rhs_ty) <- addErrCtxtM (instErrCtxt name rhs_ty) $ - deeplyInstantiate orig rhs_ty + tcMatchesFun (L nm_loc name) matches exp_ty ; mono_id <- newLetBndr no_gen name rhs_ty ; return (unitBag $ L b_loc $ FunBind { fun_id = L nm_loc mono_id, fun_matches = matches', bind_fvs = fvs, - fun_co_fn = inst_wrap <.> co_fn, fun_tick = [] }, + fun_co_fn = co_fn, fun_tick = [] }, [MBI { mbi_poly_name = name , mbi_sig = Nothing , mbi_mono_id = mono_id }]) } @@ -1297,7 +1238,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) -- See Note [Existentials in pattern bindings] ; ((pat', nosig_mbis), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $ - tcInferInst $ \ exp_ty -> + tcInferNoInst $ \ exp_ty -> tcLetPat inst_sig_fun no_gen pat exp_ty $ mapM lookup_info nosig_names @@ -1761,16 +1702,3 @@ patMonoBindsCtxt :: (OutputableBndrId id, Outputable body) patMonoBindsCtxt pat grhss = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss) -instErrCtxt :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) -instErrCtxt name ty env - = do { let (env', ty') = tidyOpenType env ty - ; return (env', hang (text "When instantiating" <+> quotes (ppr name) <> - text ", initially inferred to have" $$ - text "this overly-general type:") - 2 (ppr ty') $$ - extra) } - where - extra = sdocWithDynFlags $ \dflags -> - ppWhen (xopt LangExt.MonomorphismRestriction dflags) $ - text "NB: This instantiation can be caused by the" <+> - text "monomorphism restriction." diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index f82fc47692..7cf688d2b6 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -142,9 +142,11 @@ reportUnsolved wanted | warn_out_of_scope = HoleWarn | otherwise = HoleDefer - ; report_unsolved (Just binds_var) False type_errors expr_holes + ; report_unsolved binds_var False type_errors expr_holes type_holes out_of_scope_holes wanted - ; getTcEvBinds binds_var } + + ; ev_binds <- getTcEvBindsMap binds_var + ; return (evBindMapBinds ev_binds)} -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on -- However, do not make any evidence bindings, because we don't @@ -155,17 +157,21 @@ reportUnsolved wanted -- and for simplifyDefault. reportAllUnsolved :: WantedConstraints -> TcM () reportAllUnsolved wanted - = report_unsolved Nothing False TypeError HoleError HoleError HoleError wanted + = do { ev_binds <- newTcEvBinds + ; report_unsolved ev_binds False TypeError + HoleError HoleError HoleError wanted } -- | Report all unsolved goals as warnings (but without deferring any errors to -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in -- TcSimplify warnAllUnsolved :: WantedConstraints -> TcM () warnAllUnsolved wanted - = report_unsolved Nothing True TypeWarn HoleWarn HoleWarn HoleWarn wanted + = do { ev_binds <- newTcEvBinds + ; report_unsolved ev_binds True TypeWarn + HoleWarn HoleWarn HoleWarn wanted } -- | Report unsolved goals as errors or warnings. -report_unsolved :: Maybe EvBindsVar -- cec_binds +report_unsolved :: EvBindsVar -- cec_binds -> Bool -- Errors as warnings -> TypeErrorChoice -- Deferred type errors -> HoleChoice -- Expression holes @@ -277,21 +283,15 @@ data ReportErrCtxt -- ic_skols and givens are tidied, rest are not , cec_tidy :: TidyEnv - , cec_binds :: Maybe EvBindsVar - -- Nothing <=> Report all errors, including holes - -- Do not add any evidence bindings, because - -- we have no convenient place to put them - -- See TcErrors.reportAllUnsolved - -- Just ev <=> make some errors (depending on cec_defer) - -- into warnings, and emit evidence bindings - -- into 'ev' for unsolved constraints + , cec_binds :: EvBindsVar -- Make some errors (depending on cec_defer) + -- into warnings, and emit evidence bindings + -- into 'cec_binds' for unsolved constraints , cec_errors_as_warns :: Bool -- Turn all errors into warnings -- (except for Holes, which are -- controlled by cec_type_holes and -- cec_expr_holes) , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime - -- Irrelevant if cec_binds = Nothing -- cec_expr_holes is a union of: -- cec_type_holes - a set of typed holes: '_', '_a', '_foo' @@ -325,7 +325,7 @@ Specifically (see reportWanteds) reportImplic :: ReportErrCtxt -> Implication -> TcM () reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given - , ic_wanted = wanted, ic_binds = m_evb + , ic_wanted = wanted, ic_binds = evb , ic_status = status, ic_info = info , ic_env = tcl_env, ic_tclvl = tc_lvl }) | BracketSkol <- info @@ -356,11 +356,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given -- tree rooted here, or we've come across -- a suppress-worthy constraint higher up (Trac #11541) - , cec_binds = cec_binds ctxt *> m_evb } - -- If cec_binds ctxt is Nothing, that means - -- we're reporting *all* errors. Don't change - -- that behavior just because we're going into - -- an implication. + , cec_binds = evb } dead_givens = case status of IC_Solved { ics_dead = dead } -> dead @@ -754,12 +750,12 @@ addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM () addDeferredBinding ctxt err ct | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct -- Only add deferred bindings for Wanted constraints - , Just ev_binds_var <- cec_binds ctxt -- We have somewhere to put the bindings = do { dflags <- getDynFlags ; let err_msg = pprLocErrMsg err err_fs = mkFastString $ showSDoc dflags $ err_msg $$ text "(deferred type error)" err_tm = EvDelayedError pred err_fs + ev_binds_var = cec_binds ctxt ; case dest of EvVarDest evar @@ -1537,8 +1533,8 @@ mkEqInfoMsg ct ty1 ty2 -- mismatched types for suggestion about -fprint-explicit-kinds (act_ty, exp_ty) = case ctOrigin ct of TypeEqOrigin { uo_actual = act - , uo_expected = Check exp } -> (act, exp) - _ -> (ty1, ty2) + , uo_expected = exp } -> (act, exp) + _ -> (ty1, ty2) invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty , not vis @@ -1706,7 +1702,7 @@ mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool -- NotSwapped means (actual, expected), IsSwapped is the reverse -- First return val is whether or not to print a herald above this msg mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act - , uo_expected = Check exp + , uo_expected = exp , uo_thing = maybe_thing }) m_level printExpanded | KindLevel <- level, occurs_check_error = (True, Nothing, empty) diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index aaa1f0c5cd..ae98d38ad1 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -13,7 +13,7 @@ module TcEvidence ( -- Evidence bindings TcEvBinds(..), EvBindsVar(..), EvBindMap(..), emptyEvBindMap, extendEvBinds, - lookupEvBind, evBindMapBinds, foldEvBindMap, + lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap, EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, sccEvBinds, evBindVar, EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors, @@ -283,8 +283,24 @@ data TcEvBinds | EvBinds -- Immutable after zonking (Bag EvBind) -data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique - -- The Unique is for debug printing only +data EvBindsVar + = EvBindsVar { + ebv_uniq :: Unique, + -- The Unique is for debug printing only + + ebv_binds :: IORef EvBindMap, + -- The main payload: the value-level evidence bindings + -- (dictionaries etc) + + ebv_tcvs :: IORef TyCoVarSet + -- The free vars of the (rhss of) the coercion bindings + -- + -- Coercions don't actually have bindings + -- because we plug them in-place (via a mutable + -- variable); but we keep their free variables + -- so that we can report unused given constraints + -- See Note [Tracking redundant constraints] in TcSimplify + } instance Data.Data TcEvBinds where -- Placeholder; we can't travers into TcEvBinds @@ -325,6 +341,9 @@ extendEvBinds bs ev_bind (eb_lhs ev_bind) ev_bind } +isEmptyEvBindMap :: EvBindMap -> Bool +isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m + lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs) @@ -334,6 +353,9 @@ evBindMapBinds = foldEvBindMap consBag emptyBag foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs) +instance Outputable EvBindMap where + ppr (EvBindMap m) = ppr m + ----------------- -- All evidence is bound by EvBinds; no side effects data EvBind @@ -761,10 +783,11 @@ instance Outputable TcEvBinds where ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs))) instance Outputable EvBindsVar where - ppr (EvBindsVar _ u) = text "EvBindsVar" <> angleBrackets (ppr u) + ppr (EvBindsVar { ebv_uniq = u }) + = text "EvBindsVar" <> angleBrackets (ppr u) instance Uniquable EvBindsVar where - getUnique (EvBindsVar _ u) = u + getUnique (EvBindsVar { ebv_uniq = u }) = u instance Outputable EvBind where ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given }) diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 8ae454c167..c960f6c074 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -141,7 +141,7 @@ tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr) tcInferSigmaNC (L loc expr) = setSrcSpan loc $ - do { (expr', sigma) <- tcInfer (tcExpr expr) + do { (expr', sigma) <- tcInferNoInst (tcExpr expr) ; return (L loc expr', sigma) } tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType) @@ -1176,14 +1176,10 @@ tcInferFun (L loc (HsRecFld f)) ; return (L loc fun, ty) } tcInferFun fun - = do { (fun, fun_ty) <- tcInferSigma fun + = tcInferSigma fun + -- NB: tcInferSigma; see TcUnify + -- Note [Deep instantiation of InferResult] - -- Zonk the function type carefully, to expose any polymorphism - -- E.g. (( \(x::forall a. a->a). blah ) e) - -- We can see the rank-2 type of the lambda in time to generalise e - ; fun_ty' <- zonkTcType fun_ty - - ; return (fun, fun_ty') } ---------------- -- | Type-check the arguments to a function, possibly including visible type @@ -1267,7 +1263,7 @@ tcTupArgs args tys tcSyntaxOp :: CtOrigin -> SyntaxExpr Name -> [SyntaxOpType] -- ^ shape of syntax operator arguments - -> ExpType -- ^ overall result type + -> ExpRhoType -- ^ overall result type -> ([TcSigmaType] -> TcM a) -- ^ Type check any arguments -> TcM (a, SyntaxExpr TcId) -- ^ Typecheck a syntax operator @@ -1365,7 +1361,7 @@ tcSynArgE orig sigma_ty syn_ty thing_inside herald = text "This rebindable syntax expects a function with" go rho_ty (SynType the_ty) - = do { wrap <- tcSubTypeET orig the_ty rho_ty + = do { wrap <- tcSubTypeET orig GenSigCtxt the_ty rho_ty ; result <- thing_inside [] ; return (result, wrap) } @@ -1507,8 +1503,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) then return idHsWrapper -- Fast path; also avoids complaint when we infer -- an ambiguouse type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int - else tcSubType_NC ExprSigCtxt inferred_sigma - (mkCheckExpType my_sigma) + else tcSubType_NC ExprSigCtxt inferred_sigma my_sigma ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma) ; let poly_wrap = wrap @@ -1581,6 +1576,7 @@ tcInferRecSelId (Ambiguous lbl _) ------------------------ tcInferId :: Name -> TcM (HsExpr TcId, TcSigmaType) -- Look up an occurrence of an Id +-- Do not instantiate its type tcInferId id_name | id_name `hasKey` tagToEnumKey = failWithTc (text "tagToEnum# must appear applied to one argument") @@ -1750,7 +1746,7 @@ tcSeq loc fun_name args res_ty -> do { rr_ty <- newFlexiTyVarTy runtimeRepTy ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE rr_ty) -- see Note [Typing rule for seq] - ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg2 res_ty + ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg2 res_ty ; return (term_arg1, term_arg2, mkCheckExpType ty_arg2) } [Left term_arg1, Left term_arg2] -> return (term_arg1, term_arg2, res_ty) @@ -1773,7 +1769,7 @@ tcTagToEnum loc fun_name args res_ty ; arg <- case args of [Right hs_ty_arg, Left term_arg] -> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind - ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg res_ty + ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg res_ty -- other than influencing res_ty, we just -- don't care about a type arg passed in. -- So drop the evidence. diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index efb7dfe30e..618c3c067b 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -1445,8 +1445,9 @@ zonk_tc_ev_binds env (TcEvBinds var) = zonkEvBindsVar env var zonk_tc_ev_binds env (EvBinds bs) = zonkEvBinds env bs zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind) -zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref - ; zonkEvBinds env (evBindMapBinds bs) } +zonkEvBindsVar env (EvBindsVar { ebv_binds = ref }) + = do { bs <- readMutVar ref + ; zonkEvBinds env (evBindMapBinds bs) } zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind) zonkEvBinds env binds @@ -1598,7 +1599,7 @@ zonkTvSkolemising :: UnboundTyVarZonker -- This variant is used for the LHS of rules -- See Note [Zonking the LHS of a RULE]. zonkTvSkolemising tv - = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv + = do { tv' <- skolemiseUnboundMetaTyVar tv ; return (mkTyVarTy tv') } zonkTypeZapping :: UnboundTyVarZonker diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 055159d988..2d3dee92e5 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -853,7 +853,7 @@ checkExpectedKind :: TcType -- the type whose kind we're checking checkExpectedKind ty act_kind exp_kind = do { (ty', act_kind') <- instantiate ty act_kind exp_kind ; let origin = TypeEqOrigin { uo_actual = act_kind' - , uo_expected = mkCheckExpType exp_kind + , uo_expected = exp_kind , uo_thing = Just $ mkTypeErrorThing ty' } ; co_k <- uType origin KindLevel act_kind' exp_kind @@ -1276,7 +1276,8 @@ kcHsTyVarBndrs name cusk open_fam all_kind_vars , hsq_dependent = dep_names }) thing_inside | cusk = do { kv_kinds <- mk_kv_kinds - ; let scoped_kvs = zipWith mk_skolem_tv kv_ns kv_kinds + ; lvl <- getTcLevel + ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $ do { (tc_binders, res_kind, stuff) <- solveEqualities $ bind_telescope hs_tvs thing_inside @@ -1527,14 +1528,16 @@ tcHsTyVarName m_kind name _ -> do { kind <- case m_kind of Just kind -> return kind Nothing -> newMetaKindVar - ; return (mk_skolem_tv name kind, False) }} + ; tv <- newSkolemTyVar name kind + ; return (tv, False) }} -- makes a new skolem tv newSkolemTyVar :: Name -> Kind -> TcM TcTyVar -newSkolemTyVar name kind = return (mk_skolem_tv name kind) +newSkolemTyVar name kind = do { lvl <- getTcLevel + ; return (mk_skolem_tv lvl name kind) } -mk_skolem_tv :: Name -> Kind -> TcTyVar -mk_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv +mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar +mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False) ------------------ kindGeneralizeType :: Type -> TcM Type @@ -1810,7 +1813,7 @@ tcHsPartialSigType ctxt sig_ty ; tau <- zonkTcType tau ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau) - ; traceTc "tcHsPatSigType" (ppr all_tvs) + ; traceTc "tcHsPartialSigType" (ppr all_tvs) ; return (wcs, wcx, all_tvs, theta, tau) } where new_implicit_tv name = do { kind <- newMetaKindVar @@ -1889,7 +1892,7 @@ tcPatSig in_pat_bind sig res_ty ; if null sig_tvs then do { -- Just do the subsumption check and return wrap <- addErrCtxtM (mk_msg sig_ty) $ - tcSubTypeET_NC PatSigCtxt res_ty sig_ty + tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty ; return (sig_ty, [], sig_wcs, wrap) } else do -- Type signature binds at least one scoped type variable @@ -1912,7 +1915,7 @@ tcPatSig in_pat_bind sig res_ty -- Now do a subsumption check of the pattern signature against res_ty ; wrap <- addErrCtxtM (mk_msg sig_ty) $ - tcSubTypeET_NC PatSigCtxt res_ty sig_ty + tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty -- Phew! ; return (sig_ty, sig_tvs, sig_wcs, wrap) diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index ab5b75c056..aa97075449 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -810,7 +810,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) , ic_given = dfun_ev_vars , ic_wanted = mkImplicWC sc_meth_implics , ic_status = IC_Unsolved - , ic_binds = Just dfun_ev_binds_var + , ic_binds = dfun_ev_binds_var , ic_env = env , ic_info = InstSkol } @@ -1017,7 +1017,7 @@ checkInstConstraints thing_inside , ic_given = [] , ic_wanted = wanted , ic_status = IC_Unsolved - , ic_binds = Just ev_binds_var + , ic_binds = ev_binds_var , ic_env = env , ic_info = InstSkol } @@ -1368,8 +1368,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind ; sig_ty <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty ; let local_meth_ty = idType local_meth_id ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $ - tcSubType ctxt (Just sel_id) sig_ty - (mkCheckExpType local_meth_ty) + tcSubType_NC ctxt sig_ty local_meth_ty ; return (sig_ty, hs_wrap) } ; inner_meth_name <- newName (nameOccName sel_name) diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 678661c56d..0f8bf06412 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -30,9 +30,11 @@ module TcMType ( -------------------------------- -- Expected types ExpType(..), ExpSigmaType, ExpRhoType, - mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe, - writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType, - tauifyExpType, + mkCheckExpType, + newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst, + readExpType, readExpType_maybe, + expTypeToType, checkingExpType_maybe, checkingExpType, + tauifyExpType, inferResultToType, promoteTcType, -------------------------------- -- Creating fresh type variables for pm checking @@ -66,7 +68,7 @@ module TcMType ( zonkTidyTcType, zonkTidyOrigin, mkTypeErrorThing, mkTypeErrorThingArgs, tidyEvVar, tidyCt, tidySkolemInfo, - skolemiseUnboundMetaTyVar, + skolemiseUnboundMetaTyVar, skolemiseRuntimeUnk, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkTyCoVarsAndFVList, @@ -335,21 +337,29 @@ test gadt/gadt-escape1. -- actual data definition is in TcType -- | Make an 'ExpType' suitable for inferring a type of kind * or #. -newOpenInferExpType :: TcM ExpType -newOpenInferExpType +newInferExpTypeNoInst :: TcM ExpSigmaType +newInferExpTypeNoInst = newInferExpType False + +newInferExpTypeInst :: TcM ExpRhoType +newInferExpTypeInst = newInferExpType True + +newInferExpType :: Bool -> TcM ExpType +newInferExpType inst = do { rr <- newFlexiTyVarTy runtimeRepTy ; u <- newUnique ; tclvl <- getTcLevel ; let ki = tYPE rr ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki) ; ref <- newMutVar Nothing - ; return (Infer u tclvl ki ref) } + ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl + , ir_kind = ki, ir_ref = ref + , ir_inst = inst })) } -- | Extract a type out of an ExpType, if one exists. But one should always -- exist. Unless you're quite sure you know what you're doing. readExpType_maybe :: ExpType -> TcM (Maybe TcType) -readExpType_maybe (Check ty) = return (Just ty) -readExpType_maybe (Infer _ _ _ ref) = readMutVar ref +readExpType_maybe (Check ty) = return (Just ty) +readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref -- | Extract a type out of an ExpType. Otherwise, panics. readExpType :: ExpType -> TcM TcType @@ -359,30 +369,6 @@ readExpType exp_ty Just ty -> return ty Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) } --- | Write into an 'ExpType'. It must be an 'Infer'. -writeExpType :: ExpType -> TcType -> TcM () -writeExpType (Infer u tc_lvl ki ref) ty - | debugIsOn - = do { ki1 <- zonkTcType (typeKind ty) - ; ki2 <- zonkTcType ki - ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u ) - ; lvl_now <- getTcLevel - ; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now ) - ; cts <- readTcRef ref - ; case cts of - Just already_there -> pprPanic "writeExpType" - (vcat [ ppr u - , ppr ty - , ppr already_there ]) - Nothing -> write } - | otherwise - = write - where - write = do { traceTc "Filling ExpType" $ - ppr u <+> text ":=" <+> ppr ty - ; writeTcRef ref (Just ty) } -writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2) - -- | Returns the expected type when in checking mode. checkingExpType_maybe :: ExpType -> Maybe TcType checkingExpType_maybe (Check ty) = Just ty @@ -397,35 +383,132 @@ checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et) tauifyExpType :: ExpType -> TcM ExpType -- ^ Turn a (Infer hole) type into a (Check alpha), -- where alpha is a fresh unificaiton variable -tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty) -tauifyExpType (Infer u tc_lvl ki ref) = do { ty <- inferTypeToType u tc_lvl ki ref - ; return (Check ty) } +tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty) +tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res + ; return (Check ty) } -- | Extracts the expected type if there is one, or generates a new -- TauTv if there isn't. expTypeToType :: ExpType -> TcM TcType -expTypeToType (Check ty) = return ty -expTypeToType (Infer u tc_lvl ki ref) = inferTypeToType u tc_lvl ki ref - -inferTypeToType :: Unique -> TcLevel -> Kind -> IORef (Maybe TcType) -> TcM Type -inferTypeToType u tc_lvl ki ref - = do { uniq <- newUnique - ; tv_ref <- newMutVar Flexi - ; let details = MetaTv { mtv_info = TauTv - , mtv_ref = tv_ref - , mtv_tclvl = tc_lvl } - name = mkMetaTyVarName uniq (fsLit "t") - tau_tv = mkTcTyVar name ki details - tau = mkTyVarTy tau_tv - -- can't use newFlexiTyVarTy because we need to set the tc_lvl - -- See also Note [TcLevel of ExpType] - +expTypeToType (Check ty) = return ty +expTypeToType (Infer inf_res) = inferResultToType inf_res + +inferResultToType :: InferResult -> TcM Type +inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl + , ir_kind = kind, ir_ref = ref }) + = do { tau_tv <- newMetaTyVarAtLevel tc_lvl kind + -- See Note [TcLevel of ExpType] + ; let tau = mkTyVarTy tau_tv ; writeMutVar ref (Just tau) ; traceTc "Forcing ExpType to be monomorphic:" - (ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau) + (ppr u <+> dcolon <+> ppr kind <+> text ":=" <+> ppr tau) ; return tau } -{- +{- ********************************************************************* +* * + Promoting types +* * +********************************************************************* -} + +promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType) +-- See Note [Promoting a type] +-- promoteTcType level ty = (co, ty') +-- * Returns ty' whose max level is just 'level' +-- and whose kind is the same as 'ty' +-- * and co :: ty ~ ty' +-- * and emits constraints to justify the coercion +promoteTcType dest_lvl ty + = do { cur_lvl <- getTcLevel + ; if (cur_lvl `sameDepthAs` dest_lvl) + then dont_promote_it + else promote_it } + where + promote_it :: TcM (TcCoercion, TcType) + promote_it + = do { prom_tv <- newMetaTyVarAtLevel dest_lvl (typeKind ty) + ; let prom_ty = mkTyVarTy prom_tv + eq_orig = TypeEqOrigin { uo_actual = ty + , uo_expected = prom_ty + , uo_thing = Nothing } + + ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty + ; return (co, prom_ty) } + + dont_promote_it :: TcM (TcCoercion, TcType) + dont_promote_it = return (mkTcNomReflCo ty, ty) + +{- Note [Promoting a type] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (Trac #12427) + + data T where + MkT :: (Int -> Int) -> a -> T + + h y = case y of MkT v w -> v + +We'll infer the RHS type with an expected type ExpType of + (IR { ir_lvl = l, ir_ref = ref, ... ) +where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern +match will increase the level, so we'll end up in tcSubType, trying to +unify the type of v, + v :: Int -> Int +with the expected type. But this attempt takes place at level (l+1), +rightly so, since v's type could have mentioned existential variables, +(like w's does) and we want to catch that. + +So we + - create a new meta-var alpha[l+1] + - fill in the InferRes ref cell 'ref' with alpha + - emit an equality constraint, thus + [W] alpha[l+1] ~ (Int -> Int) + +That constraint will float outwards, as it should, unless v's +type mentions a skolem-captured variable. + +This approach fails if v has a higher rank type; see +Note [Promotion and higher rank types] + + +Note [Promotion and higher rank types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If v had a higher-rank type, say v :: (forall a. a->a) -> Int, +then we'd emit an equality + [W] alpha[l+1] ~ ((forall a. a->a) -> Int) +which will sadly fail because we can't unify a unification variable +with a polytype. But there is nothing really wrong with the program +here. + +We could just about solve this by "promote the type" of v, to expose +its polymorphic "shape" while still leaving constraints that will +prevent existential escape. But we must be careful! Exposing +the "shape" of the type is precisely what we must NOT do under +a GADT pattern match! So in this case we might promote the type +to + (forall a. a->a) -> alpha[l+1] +and emit the constraint + [W] alpha[l+1] ~ Int +Now the poromoted type can fill the ref cell, while the emitted +equality can float or not, according to the usual rules. + +But that's not quite right! We are exposing the arrow! We could +deal with that too: + (forall a. mu[l+1] a a) -> alpha[l+1] +with constraints + [W] alpha[l+1] ~ Int + [W] mu[l+1] ~ (->) +Here we abstract over the '->' inside the forall, in case that +is subject to an equality constraint from a GADT match. + +Note that we kept the outer (->) becuase that's part of +the polymorphic "shape". And becauuse of impredicativity, +GADT matches can't give equalities that affect polymorphic +shape. + +This reasoning just seems too complicated, so I decided not +to do it. These higher-rank notes are just here to record +the thinking. + + ************************************************************************ * * SkolemTvs (immutable) @@ -493,17 +576,22 @@ tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Get the location from the monad; this is a complete freshening operation tcInstSkolTyVars' overlappable subst tvs = do { loc <- getSrcSpanM - ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs } + ; lvl <- getTcLevel + ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs } -mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar -mkTcSkolTyVar loc overlappable uniq old_name kind - = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc) - kind - (SkolemTv overlappable) +mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker +mkTcSkolTyVar lvl loc overlappable + = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc) + kind details + where + details = SkolemTv (pushTcLevel lvl) overlappable + -- NB: skolems bump the level tcInstSigTyVars :: SrcSpan -> [TyVar] - -> TcRnIf gbl lcl (TCvSubst, [TcTyVar]) -tcInstSigTyVars loc = instSkolTyCoVars (mkTcSkolTyVar loc False) + -> TcM (TCvSubst, [TcTyVar]) +tcInstSigTyVars loc tvs + = do { lvl <- getTcLevel + ; instSkolTyCoVars (mkTcSkolTyVar lvl loc False) tvs } ------------------ freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar]) @@ -522,15 +610,15 @@ freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind ------------------ -instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar) - -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar]) +type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar +instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar]) instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst -instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar) +instSkolTyCoVarsX :: TcTyVarMaker -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar]) instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv) -instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar) +instSkolTyCoVarX :: TcTyVarMaker -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar) instSkolTyCoVarX mk_tcv subst tycovar = do { uniq <- newUnique -- using a new unique is critical. See @@ -620,7 +708,7 @@ cloneMetaTyVar tv -- Works for both type and kind variables readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) - readMutVar (metaTvRef tyvar) + readMutVar (metaTyVarRef tyvar) isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable @@ -645,7 +733,7 @@ writeMetaTyVar :: TcTyVar -> TcType -> TcM () writeMetaTyVar tyvar ty | not debugIsOn - = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty + = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty -- Everything from here on only happens if DEBUG is on | not (isTcTyVar tyvar) @@ -669,32 +757,61 @@ writeMetaTyVarRef tyvar ref ty <+> text ":=" <+> ppr ty) ; writeTcRef ref (Indirect ty) } --- Everything from here on only happens if DEBUG is on + -- Everything from here on only happens if DEBUG is on | otherwise = do { meta_details <- readMutVar ref; -- Zonk kinds to allow the error check to work ; zonked_tv_kind <- zonkTcType tv_kind ; zonked_ty_kind <- zonkTcType ty_kind + ; let kind_check_ok = isPredTy tv_kind -- Don't check kinds for updates + -- to coercion variables + || tcEqKind zonked_ty_kind zonked_tv_kind + + kind_msg = hang (text "Ill-kinded update to meta tyvar") + 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind) + <+> text ":=" + <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) + + ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) -- Check for double updates - ; ASSERT2( isFlexi meta_details, - hang (text "Double update of meta tyvar") - 2 (ppr tyvar $$ ppr meta_details) ) - - traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) - ; writeMutVar ref (Indirect ty) - ; when ( not (isPredTy tv_kind) - -- Don't check kinds for updates to coercion variables - && not (zonked_ty_kind `tcEqKind` zonked_tv_kind)) - $ WARN( True, hang (text "Ill-kinded update to meta tyvar") - 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind) - <+> text ":=" - <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) ) - (return ()) } + ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details ) + + -- Check for level OK + -- See Note [Level check when unifying] + ; MASSERT2( level_check_ok, level_check_msg ) + + -- Check Kinds ok + ; MASSERT2( kind_check_ok, kind_msg ) + + -- Do the write + ; writeMutVar ref (Indirect ty) } where tv_kind = tyVarKind tyvar ty_kind = typeKind ty + tv_lvl = tcTyVarLevel tyvar + ty_lvl = tcTypeLevel ty + + level_check_ok = isFmvTyVar tyvar + || not (ty_lvl `strictlyDeeperThan` tv_lvl) + level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty + + double_upd_msg details = hang (text "Double update of meta tyvar") + 2 (ppr tyvar $$ ppr details) + + +{- Note [Level check when unifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When unifying + alpha:lvl := ty +we expect that the TcLevel of 'ty' will be <= lvl. +However, during unflatting we do + fuv:l := ty:(l+1) +which is usually wrong; hence the check isFmmvTyVar in level_check_ok. +See Note [TcLevel assignment] in TcType. +-} + {- % Generating fresh variables for pattern match check -} @@ -705,7 +822,8 @@ genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar] -- Precondition: tyvars should be scoping-ordered -- see Note [Kind substitution when instantiating] -- Get the location from the monad; this is a complete freshening operation -genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs +genInstSkolTyVarsX loc subst tvs + = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs {- ************************************************************************ @@ -785,16 +903,26 @@ newWildCardX subst tv ; return (extendTvSubstWithClone subst tv new_tv, new_tv) } new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) -new_meta_tv_x info subst tyvar +new_meta_tv_x info subst tv = do { uniq <- newUnique ; details <- newMetaDetails info - ; let name = mkSystemName uniq (getOccName tyvar) + ; let name = mkSystemName uniq (getOccName tv) -- See Note [Name of an instantiated type variable] - kind = substTy subst (tyVarKind tyvar) + kind = substTy subst (tyVarKind tv) new_tv = mkTcTyVar name kind details - subst1 = extendTvSubstWithClone subst tyvar new_tv + subst1 = extendTvSubstWithClone subst tv new_tv ; return (subst1, new_tv) } +newMetaTyVarAtLevel :: TcLevel -> TcKind -> TcM TcTyVar +newMetaTyVarAtLevel tc_lvl kind + = do { uniq <- newUnique + ; ref <- newMutVar Flexi + ; let name = mkMetaTyVarName uniq (fsLit "p") + details = MetaTv { mtv_info = TauTv + , mtv_ref = ref + , mtv_tclvl = tc_lvl } + ; return (mkTcTyVar name kind details) } + {- Note [Name of an instantiated type variable] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At the moment we give a unification variable a System Name, which @@ -960,7 +1088,7 @@ zonkQuantifiedTyVar default_kind tv ; return Nothing } | otherwise - = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv + = do { tv' <- skolemiseUnboundMetaTyVar tv ; return (Just tv') } default_kind_var :: TyVar -> TcM Type @@ -988,13 +1116,21 @@ zonkQuantifiedTyVar default_kind tv Indirect ty -> WARN( True, ppr tv $$ ppr ty ) return () } -skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar +skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar +skolemiseRuntimeUnk tv + = skolemise_tv tv RuntimeUnk + +skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar +skolemiseUnboundMetaTyVar tv + = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False) + +skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar -- We have a Meta tyvar with a ref-cell inside it -- Skolemise it, so that -- we are totally out of Meta-tyvar-land -- We create a skolem TyVar, not a regular TyVar -- See Note [Zonking to Skolem] -skolemiseUnboundMetaTyVar tv details +skolemise_tv tv details = ASSERT2( isMetaTyVar tv, ppr tv ) do { span <- getSrcSpanM -- Get the location from "here" -- ie where we are generalising @@ -1448,11 +1584,7 @@ zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act , uo_expected = exp , uo_thing = m_thing }) = do { (env1, act') <- zonkTidyTcType env act - ; mb_exp <- readExpType_maybe exp -- it really should be filled in. - -- unless we're debugging. - ; (env2, exp') <- case mb_exp of - Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty - Nothing -> return (env1, exp) + ; (env2, exp') <- zonkTidyTcType env1 exp ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing ; return ( env3, orig { uo_actual = act' , uo_expected = exp' diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs index 85a7e30fdf..01586c0230 100644 --- a/compiler/typecheck/TcMatches.hs +++ b/compiler/typecheck/TcMatches.hs @@ -869,10 +869,9 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names tup_ty = mkBigCoreTupTy tup_elt_tys ; tcExtendIdEnv tup_ids $ do - { stmts_ty <- newOpenInferExpType - ; (stmts', (ret_op', tup_rets)) - <- tcStmtsAndThen ctxt tcDoStmt stmts stmts_ty $ - \ inner_res_ty -> + { ((stmts', (ret_op', tup_rets)), stmts_ty) + <- tcInferInst $ \ exp_ty -> + tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty -> do { tup_rets <- zipWithM tcCheckId tup_names (map mkCheckExpType tup_elt_tys) -- Unify the types of the "final" Ids (which may @@ -881,14 +880,12 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names <- tcSyntaxOp DoOrigin ret_op [synKnownType tup_ty] inner_res_ty $ \_ -> return () ; return (ret_op', tup_rets) } - ; stmts_ty <- readExpType stmts_ty - ; mfix_res_ty <- newOpenInferExpType - ; (_, mfix_op') - <- tcSyntaxOp DoOrigin mfix_op - [synKnownType (mkFunTy tup_ty stmts_ty)] mfix_res_ty $ + ; ((_, mfix_op'), mfix_res_ty) + <- tcInferInst $ \ exp_ty -> + tcSyntaxOp DoOrigin mfix_op + [synKnownType (mkFunTy tup_ty stmts_ty)] exp_ty $ \ _ -> return () - ; mfix_res_ty <- readExpType mfix_res_ty ; ((thing, new_res_ty), bind_op') <- tcSyntaxOp DoOrigin bind_op @@ -1014,7 +1011,7 @@ tcApplicativeStmts tcApplicativeStmts ctxt pairs rhs_ty thing_inside = do { body_ty <- newFlexiTyVarTy liftedTypeKind ; let arity = length pairs - ; ts <- replicateM (arity-1) $ newOpenInferExpType + ; ts <- replicateM (arity-1) $ newInferExpTypeInst ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; let fun_ty = mkFunTys pat_tys body_ty diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index ea4cf3ec71..9a5fd7d8cb 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -397,7 +397,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty) -- check that overall pattern is more polymorphic than arg type - ; expr_wrap2 <- tcSubTypeET (pe_orig penv) overall_pat_ty inf_arg_ty + ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty -- pattern must have inf_res_ty @@ -502,13 +502,12 @@ tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside ------------------------ -- Literal patterns -tc_pat _ (LitPat simple_lit) pat_ty thing_inside +tc_pat penv (LitPat simple_lit) pat_ty thing_inside = do { let lit_ty = hsLitType simple_lit - ; co <- unifyPatType simple_lit lit_ty pat_ty - -- coi is of kind: pat_ty ~ lit_ty - ; res <- thing_inside + ; wrap <- tcSubTypePat penv pat_ty lit_ty + ; res <- thing_inside ; pat_ty <- readExpType pat_ty - ; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty + ; return ( mkHsWrapPat wrap (LitPat simple_lit) pat_ty , res) } ------------------------ @@ -622,15 +621,6 @@ tc_pat penv (SplicePat (HsSpliced mod_finalizers (HsSplicedPat pat))) tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut ----------------- -unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion --- In patterns we want a coercion from the --- context type (expected) to the actual pattern type --- But we don't want to reverse the args to unifyType because --- that controls the actual/expected stuff in error messages -unifyPatType thing actual_ty expected_ty - = do { coi <- unifyExpType (Just thing) actual_ty expected_ty - ; return (mkTcSymCo coi) } {- Note [Hopping the LIE in lazy patterns] @@ -841,7 +831,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside prov_theta' = substTheta tenv prov_theta req_theta' = substTheta tenv req_theta - ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty' + ; wrap <- tcSubTypePat penv pat_ty ty' ; traceTc "tcPatSynPat" (ppr pat_syn $$ ppr pat_ty $$ ppr ty' $$ diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index dc973da98b..05d98fff1a 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -72,11 +72,9 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details ; (tclvl, wanted, ((lpat', args), pat_ty)) <- pushLevelAndCaptureConstraints $ - do { pat_ty <- newOpenInferExpType - ; stuff <- tcPat PatSyn lpat pat_ty $ - mapM tcLookupId arg_names - ; pat_ty <- readExpType pat_ty - ; return (stuff, pat_ty) } + tcInferInst $ \ exp_ty -> + tcPat PatSyn lpat exp_ty $ + mapM tcLookupId arg_names ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args @@ -390,11 +388,11 @@ tcPatSynMatcher (L loc name) lpat (args, arg_tys) pat_ty = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc ; tv_name <- newNameAt (mkTyVarOcc "r") loc - ; let rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False) - rr = mkTyVarTy rr_tv - res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False) - is_unlifted = null args && null prov_dicts + ; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv + rr = mkTyVarTy rr_tv + res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv res_ty = mkTyVarTy res_tv + is_unlifted = null args && null prov_dicts (cont_args, cont_arg_tys) | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy]) | otherwise = (args, arg_tys) diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs index c40544035c..0363aa114a 100644 --- a/compiler/typecheck/TcPluginM.hs +++ b/compiler/typecheck/TcPluginM.hs @@ -48,8 +48,7 @@ module TcPluginM ( -- * Manipulating evidence bindings newEvVar, setEvBind, - getEvBindsTcPluginM, - getEvBindsTcPluginM_maybe + getEvBindsTcPluginM #endif ) where @@ -64,12 +63,12 @@ import qualified Finder import FamInstEnv ( FamInstEnv ) import TcRnMonad ( TcGblEnv, TcLclEnv, Ct, CtLoc, TcPluginM - , unsafeTcPluginTcM, getEvBindsTcPluginM_maybe + , unsafeTcPluginTcM, getEvBindsTcPluginM , liftIO, traceTc ) import TcMType ( TcTyVar, TcType ) import TcEnv ( TcTyThing ) import TcEvidence ( TcCoercion, CoercionHole - , EvTerm, EvBind, EvBindsVar, mkGivenEvBind ) + , EvTerm, EvBind, mkGivenEvBind ) import TcRnTypes ( CtEvidence(..) ) import Var ( EvVar ) @@ -84,7 +83,6 @@ import Type import Id import InstEnv import FastString -import Maybes import Unique @@ -190,12 +188,4 @@ setEvBind :: EvBind -> TcPluginM () setEvBind ev_bind = do tc_evbinds <- getEvBindsTcPluginM unsafeTcPluginTcM $ TcM.addTcEvBind tc_evbinds ev_bind - --- | Access the 'EvBindsVar' carried by the 'TcPluginM' during --- constraint solving. This must not be invoked from 'tcPluginInit' --- or 'tcPluginStop', or it will panic. -getEvBindsTcPluginM :: TcPluginM EvBindsVar -getEvBindsTcPluginM = fmap (expectJust oops) getEvBindsTcPluginM_maybe - where - oops = "plugin attempted to read EvBindsVar outside the constraint solver" #endif diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 9f94c12b6a..6c800f4695 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -2486,18 +2486,19 @@ withTcPlugins hsc_env m = do plugins <- liftIO (loadTcPlugins hsc_env) case plugins of [] -> m -- Common fast case - _ -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins + _ -> do ev_binds_var <- newTcEvBinds + (solvers,stops) <- unzip `fmap` mapM (startPlugin ev_binds_var) plugins -- This ensures that tcPluginStop is called even if a type -- error occurs during compilation (Fix of #10078) eitherRes <- tryM $ do updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m - mapM_ (flip runTcPluginM Nothing) stops + mapM_ (flip runTcPluginM ev_binds_var) stops case eitherRes of Left _ -> failM Right res -> return res where - startPlugin (TcPlugin start solve stop) = - do s <- runTcPluginM start Nothing + startPlugin ev_binds_var (TcPlugin start solve stop) = + do s <- runTcPluginM start ev_binds_var return (solve s, stop s) loadTcPlugins :: HscEnv -> IO [TcPlugin] diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs index b871daf398..ada89f1e06 100644 --- a/compiler/typecheck/TcRnMonad.hs +++ b/compiler/typecheck/TcRnMonad.hs @@ -91,7 +91,7 @@ module TcRnMonad( -- * Type constraints newTcEvBinds, addTcEvBind, - getTcEvBinds, getTcEvBindsMap, + getTcEvTyCoVars, getTcEvBindsMap, chooseUniqueOccTc, getConstraintVar, setConstraintVar, emitConstraints, emitSimple, emitSimples, @@ -1375,28 +1375,30 @@ debugTc thing -} newTcEvBinds :: TcM EvBindsVar -newTcEvBinds = do { ref <- newTcRef emptyEvBindMap +newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap + ; tcvs_ref <- newTcRef emptyVarSet ; uniq <- newUnique ; traceTc "newTcEvBinds" (text "unique =" <+> ppr uniq) - ; return (EvBindsVar ref uniq) } + ; return (EvBindsVar { ebv_binds = binds_ref + , ebv_tcvs = tcvs_ref + , ebv_uniq = uniq }) } + +getTcEvTyCoVars :: EvBindsVar -> TcM TyCoVarSet +getTcEvTyCoVars (EvBindsVar { ebv_tcvs = ev_ref }) + = readTcRef ev_ref + +getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap +getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) + = readTcRef ev_ref addTcEvBind :: EvBindsVar -> EvBind -> TcM () -- Add a binding to the TcEvBinds by side effect -addTcEvBind (EvBindsVar ev_ref u) ev_bind +addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind = do { traceTc "addTcEvBind" $ ppr u $$ ppr ev_bind ; bnds <- readTcRef ev_ref ; writeTcRef ev_ref (extendEvBinds bnds ev_bind) } -getTcEvBinds :: EvBindsVar -> TcM (Bag EvBind) -getTcEvBinds (EvBindsVar ev_ref _) - = do { bnds <- readTcRef ev_ref - ; return (evBindMapBinds bnds) } - -getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap -getTcEvBindsMap (EvBindsVar ev_ref _) - = readTcRef ev_ref - chooseUniqueOccTc :: (OccSet -> OccName) -> TcM OccName chooseUniqueOccTc fn = do { env <- getGblEnv diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index f5abe16634..c3d18978b4 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -103,6 +103,7 @@ module TcRnTypes( pushErrCtxt, pushErrCtxtSameOrigin, SkolemInfo(..), pprSigSkolInfo, pprSkolInfo, + termEvidenceAllowed, CtEvidence(..), TcEvDest(..), mkGivenLoc, mkKindLoc, toKindLoc, @@ -112,7 +113,7 @@ module TcRnTypes( -- Constraint solver plugins TcPlugin(..), TcPluginResult(..), TcPluginSolver, TcPluginM, runTcPluginM, unsafeTcPluginTcM, - getEvBindsTcPluginM_maybe, + getEvBindsTcPluginM, CtFlavour(..), ctEvFlavour, CtFlavourRole, ctEvFlavourRole, ctFlavourRole, @@ -2150,12 +2151,8 @@ data Implication ic_wanted :: WantedConstraints, -- The wanted - ic_binds :: Maybe EvBindsVar, - -- Points to the place to fill in the + ic_binds :: EvBindsVar, -- Points to the place to fill in the -- abstraction and bindings. - -- is Nothing if we can't deal with - -- non-equality constraints here - -- (this happens in TcS.deferTcSForAllEq) ic_status :: ImplicStatus } @@ -2756,6 +2753,14 @@ data SkolemInfo instance Outputable SkolemInfo where ppr = pprSkolInfo +termEvidenceAllowed :: SkolemInfo -> Bool +-- Whether an implication constraint with this SkolemInfo +-- is permitted to have term-level evidence. There is +-- only one that is not, associated with unifiying +-- forall-types +termEvidenceAllowed (UnifyForAllSkol {}) = False +termEvidenceAllowed _ = True + pprSkolInfo :: SkolemInfo -> SDoc -- Complete the sentence "is a rigid type variable bound by..." pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty @@ -2835,7 +2840,7 @@ data CtOrigin -- function or instance | TypeEqOrigin { uo_actual :: TcType - , uo_expected :: ExpType + , uo_expected :: TcType , uo_thing :: Maybe ErrorThing -- ^ The thing that has type "actual" } @@ -3158,9 +3163,9 @@ type TcPluginSolver = [Ct] -- given -> [Ct] -- wanted -> TcPluginM TcPluginResult -newtype TcPluginM a = TcPluginM (Maybe EvBindsVar -> TcM a) +newtype TcPluginM a = TcPluginM (EvBindsVar -> TcM a) -instance Functor TcPluginM where +instance Functor TcPluginM where fmap = liftM instance Applicative TcPluginM where @@ -3178,7 +3183,7 @@ instance MonadFail.MonadFail TcPluginM where fail x = TcPluginM (const $ fail x) #endif -runTcPluginM :: TcPluginM a -> Maybe EvBindsVar -> TcM a +runTcPluginM :: TcPluginM a -> EvBindsVar -> TcM a runTcPluginM (TcPluginM m) = m -- | This function provides an escape for direct access to @@ -3190,8 +3195,8 @@ unsafeTcPluginTcM = TcPluginM . const -- | Access the 'EvBindsVar' carried by the 'TcPluginM' during -- constraint solving. Returns 'Nothing' if invoked during -- 'tcPluginInit' or 'tcPluginStop'. -getEvBindsTcPluginM_maybe :: TcPluginM (Maybe EvBindsVar) -getEvBindsTcPluginM_maybe = TcPluginM return +getEvBindsTcPluginM :: TcPluginM EvBindsVar +getEvBindsTcPluginM = TcPluginM return data TcPlugin = forall s. TcPlugin diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 37740bd1bc..0174b4aca2 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -41,8 +41,8 @@ module TcSMonad ( getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getLclEnv, - getTcEvBinds, getTcEvBindsFromVar, getTcLevel, - getTcEvBindsMap, + getTcEvBindsVar, getTcLevel, + getTcEvBindsAndTCVs, getTcEvBindsMap, tcLookupClass, -- Inerts @@ -2309,9 +2309,7 @@ should do two things differently: data TcSEnv = TcSEnv { - tcs_ev_binds :: Maybe EvBindsVar, - -- this could be Nothing if we can't deal with non-equality - -- constraints, because, say, we're in a top-level type signature + tcs_ev_binds :: EvBindsVar, tcs_unified :: IORef Int, -- The number of unification variables we have filled @@ -2325,10 +2323,6 @@ data TcSEnv -- See Note [Work list priorities] and tcs_worklist :: IORef WorkList, -- Current worklist - tcs_used_tcvs :: IORef TyCoVarSet, - -- these variables were used when filling holes. Don't discard! - -- See also Note [Tracking redundant constraints] in TcSimplify - tcs_need_deriveds :: Bool -- Keep solving, even if all the unsolved constraints are Derived -- See Note [Solving for Derived constraints] @@ -2386,7 +2380,7 @@ traceTcS :: String -> SDoc -> TcS () traceTcS herald doc = wrapTcS (TcM.traceTc herald doc) runTcPluginTcS :: TcPluginM a -> TcS a -runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBinds +runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar instance HasDynFlags TcS where getDynFlags = wrapTcS getDynFlags @@ -2399,14 +2393,6 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env ; n <- TcM.readTcRef ref ; TcM.writeTcRef ref (n+1) } --- | Mark variables as used filling a coercion hole -useVars :: TyCoVarSet -> TcS () -useVars vars = TcS $ \env -> useVarsTcM (tcs_used_tcvs env) vars - --- | Like 'useVars' but in the TcM monad -useVarsTcM :: IORef TyCoVarSet -> TyCoVarSet -> TcM () -useVarsTcM ref vars = TcM.updTcRef ref (`unionVarSet` vars) - csTraceTcS :: SDoc -> TcS () csTraceTcS doc = wrapTcS $ csTraceTcM 1 (return doc) @@ -2435,7 +2421,7 @@ runTcS :: TcS a -- What to run -> TcM (a, EvBindMap) runTcS tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; res <- runTcSWithEvBinds False (Just ev_binds_var) tcs + ; res <- runTcSWithEvBinds False ev_binds_var tcs ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; return (res, ev_binds) } @@ -2445,14 +2431,16 @@ runTcS tcs runTcSDeriveds :: TcS a -> TcM a runTcSDeriveds tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds True (Just ev_binds_var) tcs } + ; runTcSWithEvBinds True ev_binds_var tcs } -- | This can deal only with equality constraints. runTcSEqualities :: TcS a -> TcM a -runTcSEqualities = runTcSWithEvBinds False Nothing +runTcSEqualities thing_inside + = do { ev_binds_var <- TcM.newTcEvBinds + ; runTcSWithEvBinds False ev_binds_var thing_inside } runTcSWithEvBinds :: Bool -- ^ keep running even if only Deriveds are left? - -> Maybe EvBindsVar + -> EvBindsVar -> TcS a -> TcM a runTcSWithEvBinds solve_deriveds ev_binds_var tcs @@ -2460,15 +2448,11 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef emptyInert ; wl_var <- TcM.newTcRef emptyWorkList - ; used_var <- TcM.newTcRef emptyVarSet -- never read from, but see - -- nestImplicTcS - ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_unified = unified_var , tcs_count = step_count , tcs_inerts = inert_var , tcs_worklist = wl_var - , tcs_used_tcvs = used_var , tcs_need_deriveds = solve_deriveds } -- Run the computation @@ -2479,16 +2463,15 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs csTraceTcM 0 $ return (text "Constraint solver steps =" <+> int count) #ifdef DEBUG - ; whenIsJust ev_binds_var $ \ebv -> - do { ev_binds <- TcM.getTcEvBinds ebv - ; checkForCyclicBinds ev_binds } + ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var + ; checkForCyclicBinds ev_binds #endif ; return res } #ifdef DEBUG -checkForCyclicBinds :: Bag EvBind -> TcM () -checkForCyclicBinds ev_binds +checkForCyclicBinds :: EvBindMap -> TcM () +checkForCyclicBinds ev_binds_map | null cycles = return () | null coercion_cycles @@ -2496,6 +2479,8 @@ checkForCyclicBinds ev_binds | otherwise = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles where + ev_binds = evBindMapBinds ev_binds_map + cycles :: [[EvBind]] cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges] @@ -2511,20 +2496,17 @@ checkForCyclicBinds ev_binds -- Note [Deterministic SCC] in Digraph. #endif -setEvBindsTcS :: Maybe EvBindsVar -> TcS a -> TcS a -setEvBindsTcS m_ref (TcS thing_inside) - = TcS $ \ env -> thing_inside (env { tcs_ev_binds = m_ref }) +setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a +setEvBindsTcS ref (TcS thing_inside) + = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref }) -nestImplicTcS :: Maybe EvBindsVar -> TyCoVarSet -- bound in this implication +nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a - -> TcS (a, TyCoVarSet) -- also returns any vars used when filling - -- coercion holes (for redundant-constraint - -- tracking) -nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside) + -> TcS a +nestImplicTcS ref inner_tclvl (TcS thing_inside) = TcS $ \ TcSEnv { tcs_unified = unified_var , tcs_inerts = old_inert_var , tcs_count = count - , tcs_used_tcvs = used_var , tcs_need_deriveds = solve_deriveds } -> do { inerts <- TcM.readTcRef old_inert_var @@ -2532,35 +2514,21 @@ nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside) -- See Note [Do not inherit the flat cache] ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList - ; new_used_var <- TcM.newTcRef emptyVarSet - ; let nest_env = TcSEnv { tcs_ev_binds = m_ref + ; let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_unified = unified_var , tcs_count = count , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var - , tcs_used_tcvs = new_used_var , tcs_need_deriveds = solve_deriveds } ; res <- TcM.setTcLevel inner_tclvl $ thing_inside nest_env #ifdef DEBUG -- Perform a check that the thing_inside did not cause cycles - ; whenIsJust m_ref $ \ ref -> - do { ev_binds <- TcM.getTcEvBinds ref - ; checkForCyclicBinds ev_binds } + ; ev_binds <- TcM.getTcEvBindsMap ref + ; checkForCyclicBinds ev_binds #endif - ; used_tcvs <- TcM.readTcRef new_used_var - - ; local_ev_vars <- case m_ref of - Nothing -> return emptyVarSet - Just ref -> do { binds <- TcM.getTcEvBinds ref - ; return $ mkVarSet $ map evBindVar $ bagToList binds } - ; let all_locals = bound_tcvs `unionVarSet` local_ev_vars - (inner_used_tcvs, outer_used_tcvs) - = partitionVarSet (`elemVarSet` all_locals) used_tcvs - ; useVarsTcM used_var outer_used_tcvs - - ; return (res, inner_used_tcvs) } + ; return res } {- Note [Do not inherit the flat cache] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2684,21 +2652,22 @@ readTcRef ref = wrapTcS (TcM.readTcRef ref) updTcRef :: TcRef a -> (a->a) -> TcS () updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn) -getTcEvBinds :: TcS (Maybe EvBindsVar) -getTcEvBinds = TcS (return . tcs_ev_binds) - -getTcEvBindsFromVar :: EvBindsVar -> TcS (Bag EvBind) -getTcEvBindsFromVar = wrapTcS . TcM.getTcEvBinds +getTcEvBindsVar :: TcS EvBindsVar +getTcEvBindsVar = TcS (return . tcs_ev_binds) getTcLevel :: TcS TcLevel getTcLevel = wrapTcS TcM.getTcLevel +getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet) +getTcEvBindsAndTCVs ev_binds_var + = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var + ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var + ; return (bnds, tcvs) } + getTcEvBindsMap :: TcS EvBindMap getTcEvBindsMap - = do { ev_binds <- getTcEvBinds - ; case ev_binds of - Just (EvBindsVar ev_ref _) -> wrapTcS $ TcM.readTcRef ev_ref - Nothing -> return emptyEvBindMap } + = do { ev_binds_var <- getTcEvBindsVar + ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var } unifyTyVar :: TcTyVar -> TcType -> TcS () -- Unify a meta-tyvar with a type @@ -2958,10 +2927,17 @@ getEvTerm (Cached evt) = evt setEvBind :: EvBind -> TcS () setEvBind ev_bind - = do { tc_evbinds <- getTcEvBinds - ; case tc_evbinds of - Just evb -> wrapTcS $ TcM.addTcEvBind evb ev_bind - Nothing -> pprPanic "setEvBind" (ppr ev_bind) } + = do { evb <- getTcEvBindsVar + ; wrapTcS $ TcM.addTcEvBind evb ev_bind } + +-- | Mark variables as used filling a coercion hole +useVars :: TyCoVarSet -> TcS () +useVars vars + = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar + ; wrapTcS $ + do { tcvs <- TcM.readTcRef ref + ; let tcvs' = tcvs `unionVarSet` vars + ; TcM.writeTcRef ref tcvs' } } -- | Equalities only setWantedEq :: TcEvDest -> Coercion -> TcS () @@ -3152,6 +3128,10 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2) ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2 ; env <- getLclEnv + ; ev_binds <- newTcEvBinds + -- We have nowhere to put these bindings + -- but TcSimplify.setImplicationStatus + -- checks that we don't actually use them ; let new_tclvl = pushTcLevel (tcl_tclvl env) wc = WC { wc_simple = singleCt (mkNonCanonical ctev) , wc_impl = emptyBag @@ -3162,7 +3142,7 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2) , ic_given = [] , ic_wanted = wc , ic_status = IC_Unsolved - , ic_binds = Nothing -- no place to put binds + , ic_binds = ev_binds , ic_env = env , ic_info = skol_info } ; updWorkListTcS (extendWorkListImplic imp) diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index d146c73094..ddf0bce945 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -573,7 +573,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; psig_theta_vars <- mapM TcM.newEvVar psig_theta ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ - runTcSWithEvBinds False (Just ev_binds_var) $ + runTcSWithEvBinds False ev_binds_var $ do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env psig_givens = mkGivens loc psig_theta_vars ; _ <- solveSimpleGivens psig_givens @@ -692,7 +692,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds , ic_given = full_theta_vars , ic_wanted = wanted_transformed , ic_status = IC_Unsolved - , ic_binds = Just ev_binds_var + , ic_binds = ev_binds_var , ic_info = skol_info , ic_env = tc_lcl_env } ; emitImplication implic @@ -1225,7 +1225,7 @@ solveImplication :: Implication -- Wanted -- Precondition: The TcS monad contains an empty worklist and given-only inerts -- which after trying to solve this implication we must restore to their original value solveImplication imp@(Implic { ic_tclvl = tclvl - , ic_binds = m_ev_binds + , ic_binds = ev_binds_var , ic_skols = skols , ic_given = given_ids , ic_wanted = wanteds @@ -1243,8 +1243,8 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts) -- Solve the nested constraints - ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs) - <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $ + ; (no_given_eqs, given_insols, residual_wanted) + <- nestImplicTcS ev_binds_var tclvl $ do { let loc = mkGivenLoc tclvl info env givens = mkGivens loc given_ids ; given_insols <- solveSimpleGivens givens @@ -1265,35 +1265,33 @@ solveImplication imp@(Implic { ic_tclvl = tclvl <- floatEqualities skols no_given_eqs residual_wanted ; traceTcS "solveImplication 2" - (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs) + (ppr given_insols $$ ppr residual_wanted) ; let final_wanted = residual_wanted `addInsols` given_insols ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs , ic_wanted = final_wanted }) - used_tcvs - ; evbinds <- TcS.getTcEvBindsMap + ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var ; traceTcS "solveImplication end }" $ vcat [ text "no_given_eqs =" <+> ppr no_given_eqs , text "floated_eqs =" <+> ppr floated_eqs , text "res_implic =" <+> ppr res_implic - , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ] + , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds) + , text "implication tvcs =" <+> ppr tcvs ] ; return (floated_eqs, res_implic) } ---------------------- -setImplicationStatus :: Implication -> TyCoVarSet -- needed variables - -> TcS (Maybe Implication) +setImplicationStatus :: Implication -> TcS (Maybe Implication) -- Finalise the implication returned from solveImplication: -- * Set the ic_status field -- * Trim the ic_wanted field to remove Derived constraints -- Return Nothing if we can discard the implication altogether -setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var - , ic_info = info +setImplicationStatus implic@(Implic { ic_binds = ev_binds_var + , ic_info = info , ic_tclvl = tc_lvl , ic_wanted = wc - , ic_given = givens }) - used_tcvs + , ic_given = givens }) | some_insoluble = return $ Just $ implic { ic_status = IC_Insoluble @@ -1308,11 +1306,8 @@ setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var | otherwise -- Everything is solved; look at the implications -- See Note [Tracking redundant constraints] - = do { ev_binds <- case m_ev_binds_var of - Just (EvBindsVar ref _) -> TcS.readTcRef ref - Nothing -> return emptyEvBindMap - ; let all_needs = neededEvVars ev_binds - (used_tcvs `unionVarSet` implic_needs) + = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var + ; let all_needs = neededEvVars ev_binds implic_needs dead_givens | warnRedundantGivens info = filterOut (`elemVarSet` all_needs) givens @@ -1333,9 +1328,14 @@ setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var , wc_impl = pruned_implics } } -- We can only prune the child implications (pruned_implics) -- in the IC_Solved status case, because only then we can - -- accumulate their needed evidence variales into the + -- accumulate their needed evidence variables into the -- IC_Solved final_status field of the parent implication. + -- Check that there are no term-level evidence bindings + -- in the cases where we have no place to put them + ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds) + , ppr info $$ ppr ev_binds ) + ; return $ if discard_entire_implication then Nothing else Just final_implic } @@ -1383,12 +1383,12 @@ warnRedundantGivens (SigSkol ctxt _) warnRedundantGivens (InstSkol {}) = True warnRedundantGivens _ = False -neededEvVars :: EvBindMap -> VarSet -> VarSet +neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet -- Find all the evidence variables that are "needed", -- and then delete all those bound by the evidence bindings --- See note [Tracking redundant constraints] -neededEvVars ev_binds initial_seeds - = needed `minusVarSet` bndrs +-- See Note [Tracking redundant constraints] +neededEvVars (ev_binds, tcvs) initial_seeds + = (needed `unionVarSet` tcvs) `minusVarSet` bndrs where seeds = foldEvBindMap add_wanted initial_seeds ev_binds needed = transCloVarSet also_needs seeds @@ -1457,8 +1457,8 @@ works: * When the constraint solver finishes solving all the wanteds in an implication, it sets its status to IC_Solved - - The ics_dead field, of IC_Solved, records the subset of this implication's - ic_given that are redundant (not needed). + - The ics_dead field, of IC_Solved, records the subset of this + implication's ic_given that are redundant (not needed). - The ics_need field of IC_Solved then records all the in-scope (given) evidence variables bound by the context, that @@ -1471,7 +1471,6 @@ works: a) it is free in the RHS of a Wanted EvBind, b) it is free in the RHS of an EvBind whose LHS is needed, c) it is in the ics_need of a nested implication. - d) it is listed in the tcs_used_tcvs field of the nested TcSEnv * We need to be careful not to discard an implication prematurely, even one that is fully solved, because we might @@ -2053,8 +2052,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds) = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ]) ; fake_ev_binds_var <- TcS.newTcEvBinds ; tclvl <- TcS.getTcLevel - ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet - (pushTcLevel tclvl) try_group + ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group ; if success then -- Success: record the type variable binding, and return diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 5013f470da..159c6dca5c 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -24,13 +24,14 @@ module TcType ( TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, TcKind, TcCoVar, TcTyCoVar, TcTyBinder, TcTyVarBinder, TcTyCon, - ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType, + ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType, SyntaxOpType(..), synKnownType, mkSynFunTys, -- TcLevel TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, strictlyDeeperThan, sameDepthAs, fmvTcLevel, + tcTypeLevel, tcTyVarLevel, maxTcLevel, -------------------------------- -- MetaDetails @@ -40,7 +41,7 @@ module TcType ( isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, isSigTyVar, isOverlappableTyVar, isTyConableTyVar, isFskTyVar, isFmvTyVar, isFlattenTyVar, - isAmbiguousTyVar, metaTvRef, metaTyVarInfo, + isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, isTouchableMetaTyVar, isTouchableOrFmv, @@ -298,19 +299,30 @@ type TcDTyCoVarSet = DTyCoVarSet -- | An expected type to check against during type-checking. -- See Note [ExpType] in TcMType, where you'll also find manipulators. data ExpType = Check TcType - | Infer Unique -- for debugging only - TcLevel -- See Note [TcLevel of ExpType] in TcMType - Kind - (IORef (Maybe TcType)) + | Infer !InferResult + +data InferResult + = IR { ir_uniq :: Unique -- For debugging only + , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in TcMType + , ir_inst :: Bool -- True <=> deeply instantiate before returning + -- i.e. return a RhoType + -- False <=> do not instantaite before returning + -- i.e. return a SigmaType + , ir_kind :: Kind + , ir_ref :: IORef (Maybe TcType) } type ExpSigmaType = ExpType type ExpRhoType = ExpType instance Outputable ExpType where - ppr (Check ty) = ppr ty - ppr (Infer u lvl ki _) - = parens (text "Infer" <> braces (ppr u <> comma <> ppr lvl) - <+> dcolon <+> ppr ki) + ppr (Check ty) = text "Check" <> braces (ppr ty) + ppr (Infer ir) = ppr ir + +instance Outputable InferResult where + ppr (IR { ir_uniq = u, ir_lvl = lvl + , ir_kind = ki, ir_inst = inst }) + = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst) + <+> dcolon <+> ppr ki -- | Make an 'ExpType' suitable for checking. mkCheckExpType :: TcType -> ExpType @@ -420,6 +432,7 @@ we would need to enforce the separation. -- See Note [TyVars and TcTyVars] data TcTyVarDetails = SkolemTv -- A skolem + TcLevel -- Level of the implication that binds it Bool -- True <=> this skolem type variable can be overlapped -- when looking up instances -- See Note [Binding when looking up instances] in InstEnv @@ -437,8 +450,8 @@ data TcTyVarDetails vanillaSkolemTv, superSkolemTv :: TcTyVarDetails -- See Note [Binding when looking up instances] in InstEnv -vanillaSkolemTv = SkolemTv False -- Might be instantiated -superSkolemTv = SkolemTv True -- Treat this as a completely distinct type +vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False -- Might be instantiated +superSkolemTv = SkolemTv (pushTcLevel topTcLevel) True -- Treat this as a completely distinct type ----------------------------- data MetaDetails @@ -467,10 +480,10 @@ instance Outputable MetaDetails where pprTcTyVarDetails :: TcTyVarDetails -> SDoc -- For debugging -pprTcTyVarDetails (SkolemTv True) = text "ssk" -pprTcTyVarDetails (SkolemTv False) = text "sk" pprTcTyVarDetails (RuntimeUnk {}) = text "rt" pprTcTyVarDetails (FlatSkol {}) = text "fsk" +pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl +pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl }) = pp_info <> colon <> ppr tclvl where @@ -655,6 +668,9 @@ We arrange the TcLevels like this The flatten meta-vars are all at level 0, just to make them untouchable. -} +maxTcLevel :: TcLevel -> TcLevel -> TcLevel +maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b) + fmvTcLevel :: TcLevel -> TcLevel -- See Note [TcLevel assignment] fmvTcLevel _ = TcLevel 0 @@ -685,6 +701,24 @@ checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl) = ctxt_tclvl >= tv_tclvl +tcTyVarLevel :: TcTyVar -> TcLevel +tcTyVarLevel tv + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl + SkolemTv tv_lvl _ -> tv_lvl + FlatSkol ty -> tcTypeLevel ty + RuntimeUnk -> topTcLevel + +tcTypeLevel :: TcType -> TcLevel +-- Max level of any free var of the type +tcTypeLevel ty + = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty) + where + add v lvl + | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v + | otherwise = lvl + instance Outputable TcLevel where ppr (TcLevel us) = ppr us @@ -1034,8 +1068,8 @@ isSkolemTyVar tv isOverlappableTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - SkolemTv overlappable -> overlappable - _ -> False + SkolemTv _ overlappable -> overlappable + _ -> False isMetaTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) @@ -1076,6 +1110,12 @@ metaTyVarTcLevel_maybe tv MetaTv { mtv_tclvl = tclvl } -> Just tclvl _ -> Nothing +metaTyVarRef :: TyVar -> IORef MetaDetails +metaTyVarRef tv + = case tcTyVarDetails tv of + MetaTv { mtv_ref = ref } -> ref + _ -> pprPanic "metaTyVarRef" (ppr tv) + setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar setMetaTyVarTcLevel tv tclvl = case tcTyVarDetails tv of @@ -1088,12 +1128,6 @@ isSigTyVar tv MetaTv { mtv_info = SigTv } -> True _ -> False -metaTvRef :: TyVar -> IORef MetaDetails -metaTvRef tv - = case tcTyVarDetails tv of - MetaTv { mtv_ref = ref } -> ref - _ -> pprPanic "metaTvRef" (ppr tv) - isFlexi, isIndirect :: MetaDetails -> Bool isFlexi Flexi = True isFlexi _ = False diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 2712c4a5c5..4b0b749ab0 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -6,23 +6,23 @@ Type subsumption and unification -} -{-# LANGUAGE CPP, MultiWayIf, TupleSections #-} +{-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-} module TcUnify ( -- Full-blown subsumption tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, - tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O, - tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC, + tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, + tcSubTypeDS_NC_O, tcSubTypeET, checkConstraints, buildImplicationFor, -- Various unifications unifyType, unifyTheta, unifyKind, noThing, - uType, unifyExpType, + uType, swapOverTyVars, canSolveByUnification, -------------------------------- -- Holes - tcInfer, + tcInferInst, tcInferNoInst, matchExpectedListTy, matchExpectedPArrTy, matchExpectedTyConApp, @@ -112,14 +112,15 @@ passed in. -} -- Use this one when you have an "expected" type. -matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] +matchExpectedFunTys :: forall a. + SDoc -- See Note [Herald for matchExpectedFunTys] -> Arity -> ExpRhoType -- deeply skolemised -> ([ExpSigmaType] -> ExpRhoType -> TcM a) -- must fill in these ExpTypes here -> TcM (a, HsWrapper) -- If matchExpectedFunTys n ty = (_, wrap) --- then wrap : (t1 -> ... -> tn -> ty_r) "->" ty, +-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, -- where [t1, ..., tn], ty_r are passed to the thing_inside matchExpectedFunTys herald arity orig_ty thing_inside = case orig_ty of @@ -166,14 +167,16 @@ matchExpectedFunTys herald arity orig_ty thing_inside defer acc_arg_tys n (mkCheckExpType ty) ------------ + defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper) defer acc_arg_tys n fun_ty - = do { more_arg_tys <- replicateM n newOpenInferExpType - ; res_ty <- newOpenInferExpType + = do { more_arg_tys <- replicateM n newInferExpTypeNoInst + ; res_ty <- newInferExpTypeInst ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty ; more_arg_tys <- mapM readExpType more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkFunTys more_arg_tys res_ty - ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty + ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty + -- Not a good origin at all :-( ; return (result, wrap) } ------------ @@ -198,7 +201,7 @@ matchActualFunTys :: Outputable a -> TcSigmaType -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) -- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r) --- then wrap : ty "->" (t1 -> ... -> tn -> ty_r) +-- then wrap : ty ~> (t1 -> ... -> tn -> ty_r) matchActualFunTys herald ct_orig mb_thing arity ty = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity @@ -523,82 +526,36 @@ tcSubTypeHR :: Outputable a -> TcSigmaType -> ExpRhoType -> TcM HsWrapper tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt -tcSubType :: Outputable a - => UserTypeCtxt -> Maybe a -- ^ If present, it has type ty_actual - -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper --- Checks that actual <= expected --- Returns HsWrapper :: actual ~ expected -tcSubType ctxt maybe_thing ty_actual ty_expected - = tcSubTypeO origin ctxt ty_actual ty_expected - where - origin = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = mkErrorThing <$> maybe_thing } - - --- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type. --- You probably want this only when looking at patterns, never expressions. -tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -tcSubTypeET orig ty_actual ty_expected - = uExpTypeX orig ty_expected ty_actual - (return . mkWpCastN . mkTcSymCo) - (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a - (mkCheckExpType ty_expected)) - --- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type. --- You probably want this only when looking at patterns, never expressions. --- Does not add context. -tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected - = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual -tcSubTypeET_NC ctxt (Check ty_actual) ty_expected - = tc_sub_type orig orig ctxt ty_actual ty_expected' +------------------------ +tcSubTypeET :: CtOrigin -> UserTypeCtxt + -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper +-- If wrap = tc_sub_type_et t1 t2 +-- => wrap :: t1 ~> t2 +tcSubTypeET orig ctxt (Check ty_actual) ty_expected + = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected where - ty_expected' = mkCheckExpType ty_expected - orig = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected' - , uo_thing = Nothing } + eq_orig = TypeEqOrigin { uo_actual = ty_expected + , uo_expected = ty_actual + , uo_thing = Nothing } +tcSubTypeET _ _ (Infer inf_res) ty_expected + = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected ) + do { co <- fillInferResult ty_expected inf_res + ; return (mkWpCastN (mkTcSymCo co)) } + +------------------------ tcSubTypeO :: CtOrigin -- ^ of the actual type -> UserTypeCtxt -- ^ of the expected type -> TcSigmaType - -> ExpSigmaType + -> ExpRhoType -> TcM HsWrapper -tcSubTypeO origin ctxt ty_actual ty_expected - = addSubTypeCtxt ty_actual ty_expected $ - do { traceTc "tcSubType" (vcat [ pprCtOrigin origin - , pprUserTypeCtxt ctxt - , ppr ty_actual - , ppr ty_expected ]) - ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected } - where - eq_orig | TypeEqOrigin {} <- origin = origin - | otherwise - = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = Nothing } - -tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a -- ^ has type ty_actual - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised (hence "DS") -tcSubTypeDS ctxt m_expr ty_actual ty_expected - = addSubTypeCtxt ty_actual ty_expected $ - tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected - --- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating --- the "actual" type -tcSubTypeDS_O :: Outputable a - => CtOrigin -> UserTypeCtxt - -> Maybe a -> TcSigmaType -> ExpRhoType - -> TcM HsWrapper -tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected +tcSubTypeO orig ctxt ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig , pprUserTypeCtxt ctxt , ppr ty_actual , ppr ty_expected ]) - ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected } + ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected } addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a addSubTypeCtxt ty_actual ty_expected thing_inside @@ -628,26 +585,24 @@ addSubTypeCtxt ty_actual ty_expected thing_inside -- The "_NC" variants do not add a typechecker-error context; -- the caller is assumed to do that -tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper +tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +-- Checks that actual <= expected +-- Returns HsWrapper :: actual ~ expected tcSubType_NC ctxt ty_actual ty_expected = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tc_sub_type origin origin ctxt ty_actual ty_expected } + ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected } where origin = TypeEqOrigin { uo_actual = ty_actual , uo_expected = ty_expected , uo_thing = Nothing } -tcSubTypeDS_NC :: Outputable a - => UserTypeCtxt - -> Maybe a -- ^ If present, this has type ty_actual - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected - = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected } - where - origin = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = mkErrorThing <$> maybe_thing } +tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper +-- Just like tcSubType, but with the additional precondition that +-- ty_expected is deeply skolemised (hence "DS") +tcSubTypeDS orig ctxt ty_actual ty_expected + = addSubTypeCtxt ty_actual ty_expected $ + do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) + ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected } tcSubTypeDS_NC_O :: Outputable a => CtOrigin -- origin used for instantiation only @@ -656,56 +611,72 @@ tcSubTypeDS_NC_O :: Outputable a -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -- Just like tcSubType, but with the additional precondition that -- ty_expected is deeply skolemised -tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et - = uExpTypeX eq_orig ty_actual et - (return . mkWpCastN) - (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual) - where - eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et - , uo_thing = mkErrorThing <$> m_thing } +tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected + = case ty_expected of + Infer inf_res -> fillInferResult_Inst inst_orig ty_actual inf_res + Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty + where + eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty + , uo_thing = mkErrorThing <$> m_thing } --------------- -tc_sub_type :: CtOrigin -- origin used when calling uType - -> CtOrigin -- origin used when instantiating - -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper -tc_sub_type eq_orig inst_orig ctxt ty_actual et - = uExpTypeX eq_orig ty_actual et - (return . mkWpCastN) - (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual) - tc_sub_tc_type :: CtOrigin -- used when calling uType -> CtOrigin -- used when instantiating -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +-- If wrap = tc_sub_type t1 t2 +-- => wrap :: t1 ~> t2 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected - | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types] - = do { lookup_res <- lookupTcTyVar tv_actual - ; case lookup_res of - Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig - ctxt ty_actual' ty_expected - - -- It's tempting to see if tv_actual can unify with a polytype - -- and, if so, call uType; otherwise, skolemise first. But this - -- is wrong, because skolemising will bump the TcLevel and the - -- unification will fail anyway. - -- It's also tempting to call uUnfilledVar directly, but calling - -- uType seems safer in the presence of possible refactoring - -- later. - Unfilled _ -> mkWpCastN <$> - uType eq_orig TypeLevel ty_actual ty_expected } - - | otherwise -- See Note [Deep skolemisation] - = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ - \ _ sk_rho -> + | is_poly ty_expected -- See Note [Don't skolemise unnecessarily] + , not (is_poly ty_actual) + = do { traceTc "tc_sub_tc_type (drop to equality)" $ + vcat [ text "ty_actual =" <+> ppr ty_actual + , text "ty_expected =" <+> ppr ty_expected ] + ; mkWpCastN <$> + uType eq_orig TypeLevel ty_actual ty_expected } + + | otherwise -- This is the general case + = do { traceTc "tc_sub_tc_type (general case)" $ + vcat [ text "ty_actual =" <+> ppr ty_actual + , text "ty_expected =" <+> ppr ty_expected ] + ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ + \ _ sk_rho -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual sk_rho ; return (sk_wrap <.> inner_wrap) } + where + is_poly ty + | isForAllTy ty = True + | Just (_, res) <- splitFunTy_maybe ty = is_poly res + | otherwise = False + -- NB *not* tcSplitFunTy, because here we want + -- to decompose type-class arguments too + + +{- Note [Don't skolemise unnecessarily] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are trying to solve + (Char->Char) <= (forall a. a->a) +We could skolemise the 'forall a', and then complain +that (Char ~ a) is insoluble; but that's a pretty obscure +error. It's better to say that + (Char->Char) ~ (forall a. a->a) +fails. + +In general, + * if the RHS type an outermost forall (i.e. skolemisation + is the next thing we'd do) + * and the LHS has no top-level polymorphism (but looking deeply) +then we can revert to simple equality. +-} --------------- tc_sub_type_ds :: CtOrigin -- used when calling uType -> CtOrigin -- used when instantiating -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised +-- If wrap = tc_sub_type_ds t1 t2 +-- => wrap :: t1 ~> t2 +-- Here is where the work actually happens! +-- Precondition: ty_expected is deeply skolemised tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected = go ty_actual ty_expected where @@ -739,8 +710,8 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected (SigSkol GenSigCtxt exp_arg)) ctxt exp_arg act_arg ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) } - -- arg_wrap :: exp_arg ~ act_arg - -- res_wrap :: act-res ~ exp_res + -- arg_wrap :: exp_arg ~> act_arg + -- res_wrap :: act-res ~> exp_res go ty_a ty_e | let (tvs, theta, _) = tcSplitSigmaTy ty_a @@ -748,8 +719,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a ; body_wrap <- tc_sub_type_ds (eq_orig { uo_actual = in_rho - , uo_expected = - mkCheckExpType ty_expected }) + , uo_expected = ty_expected }) inst_orig ctxt in_rho ty_e ; return (body_wrap <.> in_wrap) } @@ -815,23 +785,124 @@ wrapFunResCoercion arg_tys co_fn_res = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) } ------------------------------------ + +{- ********************************************************************** +%* * + ExpType functions: tcInfer, fillInferResult +%* * +%********************************************************************* -} + -- | Infer a type using a fresh ExpType -- See also Note [ExpType] in TcMType -tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType) -tcInfer tc_check - = do { res_ty <- newOpenInferExpType +-- Does not attempt to instantiate the inferred type +tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tcInferNoInst = tcInfer False + +tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType) +tcInferInst = tcInfer True + +tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tcInfer instantiate tc_check + = do { res_ty <- newInferExpType instantiate ; result <- tc_check res_ty ; res_ty <- readExpType res_ty ; return (result, res_ty) } -{- -************************************************************************ +fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper +-- If wrap = fillInferResult_Inst t1 t2 +-- => wrap :: t1 ~> t2 +-- See Note [Deep instantiation of InferResult] +fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me }) + | instantiate_me + = do { (wrap, rho) <- deeplyInstantiate orig ty + ; co <- fillInferResult rho inf_res + ; return (mkWpCastN co <.> wrap) } + + | otherwise + = do { co <- fillInferResult ty inf_res + ; return (mkWpCastN co) } + +fillInferResult :: TcType -> InferResult -> TcM TcCoercionN +-- If wrap = fillInferResult t1 t2 +-- => wrap :: t1 ~> t2 +fillInferResult ty (IR { ir_uniq = u, ir_lvl = res_lvl + , ir_kind = res_kind, ir_ref = ref }) + = do { (ty_co, ty) <- promoteTcType res_lvl ty + ; ki_co <- uType kind_orig KindLevel ty_kind res_kind + ; let ty_to_fill_with = ty `mkCastTy` ki_co + co = ty_co `mkTcCoherenceRightCo` ki_co + + ; when debugIsOn (check_hole ty_to_fill_with) + + ; traceTc "Filling ExpType" $ + ppr u <+> text ":=" <+> ppr ty_to_fill_with + + ; writeTcRef ref (Just ty) + + ; return co } + where + ty_kind = typeKind ty + kind_orig = TypeEqOrigin { uo_actual = ty_kind + , uo_expected = res_kind + , uo_thing = Nothing } + + check_hole ty -- Debug check only + = do { ki1 <- zonkTcType (typeKind ty) + ; ki2 <- zonkTcType res_kind + ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u ) + ; let ty_lvl = tcTypeLevel ty + ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl), + ppr u $$ ppr res_lvl $$ ppr ty_lvl ) + ; cts <- readTcRef ref + ; case cts of + Just already_there -> pprPanic "writeExpType" + (vcat [ ppr u + , ppr ty + , ppr already_there ]) + Nothing -> return () } + +{- Note [Deep instantiation of InferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In some cases we want to deeply instantiate before filling in +an InferResult, and in some cases not. That's why InferReult +has the ir_inst flag. + +* ir_inst = True: deeply instantantiate + + Consider + f x = (*) + We want to instantiate the type of (*) before returning, else we + will infer the type + f :: forall {a}. a -> forall b. Num b => b -> b -> b + This is surely confusing for users. + + And worse, the the monomorphism restriction won't properly. The MR is + dealt with in simplifyInfer, and simplifyInfer has no way of + instantiating. This could perhaps be worked around, but it may be + hard to know even when instantiation should happen. + + Another reason. Consider + f :: (?x :: Int) => a -> a + g y = let ?x = 3::Int in f + Here want to instantiate f's type so that the ?x::Int constraint + gets discharged by the enclosing implicit-parameter binding. + +* ir_inst = False: do not instantantiate + + Consider this (which uses visible type application): + + (let { f :: forall a. a -> a; f x = x } in f) @Int + + We'll call TcExpr.tcInferFun to infer the type of the (let .. in f) + And we don't want to instantite the type of 'f' when we reach it, + else the outer visible type application won't work +-} + +{- ********************************************************************* * * -\subsection{Generalisation} + Generalisation * * -************************************************************************ --} +********************************************************************* -} -- | Take an "expected type" and strip off quantifiers to expose the -- type underneath, binding the new skolems for the @thing_inside@. @@ -949,7 +1020,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted , ic_given = given , ic_wanted = wanted , ic_status = IC_Unsolved - , ic_binds = Just ev_binds_var + , ic_binds = ev_binds_var , ic_env = env , ic_info = skol_info } @@ -972,19 +1043,9 @@ unifyType :: Outputable a => Maybe a -- ^ If present, has type 'ty1' -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2 where - origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2 + origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 , uo_thing = mkErrorThing <$> thing } --- | Variant of 'unifyType' that takes an 'ExpType' as its second type -unifyExpType :: Outputable a => Maybe a - -> TcTauType -> ExpType -> TcM TcCoercionN -unifyExpType mb_thing ty1 ty2 - = uExpType ty_orig ty1 ty2 - where - ty_orig = TypeEqOrigin { uo_actual = ty1 - , uo_expected = ty2 - , uo_thing = mkErrorThing <$> mb_thing } - -- | Use this instead of 'Nothing' when calling 'unifyType' without -- a good "thing" (where the "thing" has the "actual" type passed in) -- This has an 'Outputable' instance, avoiding amgiguity problems. @@ -993,7 +1054,7 @@ noThing = Nothing unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2 - where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2 + where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 , uo_thing = mkErrorThing <$> thing } --------------- @@ -1020,34 +1081,6 @@ unifyTheta theta1 theta2 uType is the heart of the unifier. -} -uExpType :: CtOrigin -> TcType -> ExpType -> TcM CoercionN -uExpType orig ty1 et - = uExpTypeX orig ty1 et return $ - uType orig TypeLevel ty1 - --- | Tries to unify with an ExpType. If the ExpType is filled in, calls the first --- continuation with the produced coercion. Otherwise, calls the second --- continuation. This can happen either with a Check or with an untouchable --- ExpType that reverts to a tau-type. See Note [TcLevel of ExpType] -uExpTypeX :: CtOrigin -> TcType -> ExpType - -> (TcCoercionN -> TcM a) -- Infer case, co :: TcType ~N ExpType - -> (TcType -> TcM a) -- Check / untouchable case - -> TcM a -uExpTypeX orig ty1 et@(Infer _ tc_lvl ki _) coercion_cont type_cont - = do { cur_lvl <- getTcLevel - ; if cur_lvl `sameDepthAs` tc_lvl - then do { ki_co <- uType kind_orig KindLevel (typeKind ty1) ki - ; writeExpType et (ty1 `mkCastTy` ki_co) - ; coercion_cont $ mkTcNomReflCo ty1 `mkTcCoherenceRightCo` ki_co } - else do { traceTc "Preventing writing to untouchable ExpType" empty - ; tau <- expTypeToType et -- See Note [TcLevel of ExpType] - ; type_cont tau }} - where - kind_orig = KindEqOrigin ty1 Nothing orig (Just TypeLevel) -uExpTypeX _ _ (Check ty2) _ type_cont - = type_cont ty2 - ------------- uType, uType_defer :: CtOrigin -> TypeOrKind @@ -1059,23 +1092,18 @@ uType, uType_defer -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] uType_defer origin t_or_k ty1 ty2 - = do { hole <- newCoercionHole - ; loc <- getCtLocM origin (Just t_or_k) - ; emitSimple $ mkNonCanonical $ - CtWanted { ctev_dest = HoleDest hole - , ctev_pred = mkPrimEqPred ty1 ty2 - , ctev_loc = loc } + = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2 -- Error trace only - -- NB. do *not* call mkErrInfo unless tracing is on, because - -- it is hugely expensive (#5631) + -- NB. do *not* call mkErrInfo unless tracing is on, + -- because it is hugely expensive (#5631) ; whenDOptM Opt_D_dump_tc_trace $ do { ctxt <- getErrCtxt ; doc <- mkErrInfo emptyTidyEnv ctxt - ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1, + ; traceTc "utype_defer" (vcat [ppr co, ppr ty1, ppr ty2, pprCtOrigin origin, doc]) } - ; return (mkHoleCo hole Nominal ty1 ty2) } + ; return co } -------------- uType origin t_or_k orig_ty1 orig_ty2 @@ -1667,9 +1695,330 @@ matchExpectedFunKind num_args_remaining ty = go ; let new_fun = mkFunTy arg_kind res_kind thing = mkTypeErrorThingArgs ty num_args_remaining origin = TypeEqOrigin { uo_actual = k - , uo_expected = mkCheckExpType new_fun + , uo_expected = new_fun , uo_thing = Just thing } ; co <- uType origin KindLevel k new_fun ; return (co, arg_kind, res_kind) } - where + + +{- ********************************************************************* +* * + Occurrence checking +* * +********************************************************************* -} + + +{- Note [Occurs check expansion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid +of occurrences of tv outside type function arguments, if that is +possible; otherwise, it returns Nothing. + +For example, suppose we have + type F a b = [a] +Then + occCheckExpand b (F Int b) = Just [Int] +but + occCheckExpand a (F a Int) = Nothing + +We don't promise to do the absolute minimum amount of expanding +necessary, but we try not to do expansions we don't need to. We +prefer doing inner expansions first. For example, + type F a b = (a, Int, a, [a]) + type G b = Char +We have + occCheckExpand b (F (G b)) = Just (F Char) +even though we could also expand F to get rid of b. + +The two variants of the function are to support TcUnify.checkTauTvUpdate, +which wants to prevent unification with type families. For more on this +point, see Note [Prevent unification with type families] in TcUnify. + +Note [Occurrence checking: look inside kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are considering unifying + (alpha :: *) ~ Int -> (beta :: alpha -> alpha) +This may be an error (what is that alpha doing inside beta's kind?), +but we must not make the mistake of actuallyy unifying or we'll +build an infinite data structure. So when looking for occurrences +of alpha in the rhs, we must look in the kinds of type variables +that occur there. + +NB: we may be able to remove the problem via expansion; see + Note [Occurs check expansion]. So we have to try that. + +Note [Checking for foralls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Unless we have -XImpredicativeTypes (which is a totally unsupported +feature), we do not want to unify + alpha ~ (forall a. a->a) -> Int +So we look for foralls hidden inside the type, and it's convenient +to do that at the same time as the occurs check (which looks for +occurrences of alpha). + +However, it's not just a question of looking for foralls /anywhere/! +Consider + (alpha :: forall k. k->*) ~ (beta :: forall k. k->*) +This is legal; e.g. dependent/should_compile/T11635. + +We don't want to reject it because of the forall in beta's kind, +but (see Note [Occurrence checking: look inside kinds]) we do +need to look in beta's kind. So we carry a flag saying if a 'forall' +is OK, and sitch the flag on when stepping inside a kind. + +Why is it OK? Why does it not count as impredicative polymorphism? +The reason foralls are bad is because we reply on "seeing" foralls +when doing implicit instantiation. But the forall inside the kind is +fine. We'll generate a kind equality constraint + (forall k. k->*) ~ (forall k. k->*) +to check that the kinds of lhs and rhs are compatible. If alpha's +kind had instead been + (alpha :: kappa) +then this kind equality would rightly complain about unifying kappa +with (forall k. k->*) + +-} + +data OccCheckResult a + = OC_OK a + | OC_Bad -- Forall or type family + | OC_Occurs + +instance Functor OccCheckResult where + fmap = liftM + +instance Applicative OccCheckResult where + pure = OC_OK + (<*>) = ap + +instance Monad OccCheckResult where + OC_OK x >>= k = k x + OC_Bad >>= _ = OC_Bad + OC_Occurs >>= _ = OC_Occurs + +occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult () +-- Just for error-message generation; so we return OccCheckResult +-- so the caller can report the right kind of error +-- Check whether +-- a) the given variable occurs in the given type. +-- b) there is a forall in the type (unless we have -XImpredicativeTypes) +occCheckForErrors dflags tv ty + = case preCheck dflags True tv ty of + OC_OK _ -> OC_OK () + OC_Bad -> OC_Bad + OC_Occurs -> case occCheckExpand tv ty of + Nothing -> OC_Occurs + Just _ -> OC_OK () + +---------------- +metaTyVarUpdateOK :: DynFlags + -> TcTyVar -- tv :: k1 + -> TcType -- ty :: k2 + -> Maybe TcType -- possibly-expanded ty +-- (metaTyFVarUpdateOK tv ty) +-- We are about to update the meta-tyvar tv with ty, in +-- our on-the-flyh unifier +-- Check (a) that tv doesn't occur in ty (occurs check) +-- (b) that ty does not have any foralls +-- (in the impredicative case), or type functions +-- +-- We have two possible outcomes: +-- (1) Return the type to update the type variable with, +-- [we know the update is ok] +-- (2) Return Nothing, +-- [the update might be dodgy] +-- +-- Note that "Nothing" does not mean "definite error". For example +-- type family F a +-- type instance F Int = Int +-- consider +-- a ~ F a +-- This is perfectly reasonable, if we later get a ~ Int. For now, though, +-- we return Nothing, leaving it to the later constraint simplifier to +-- sort matters out. +-- +-- See Note [Refactoring hazard: checkTauTvUpdate] + +metaTyVarUpdateOK dflags tv ty + = case preCheck dflags False tv ty of + -- False <=> type families not ok + -- See Note [Prevent unification with type families] + OC_OK _ -> Just ty + OC_Bad -> Nothing -- forall or type function + OC_Occurs -> occCheckExpand tv ty + +preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult () +-- A quick check for +-- (a) a forall type (unless -XImpredivativeTypes) +-- (b) a type family +-- (c) an occurrence of the type variable (occurs check) +-- +-- For (a) and (b) we check only the top level of the type, NOT +-- inside the kinds of variables it mentions. But for (c) we do +-- look in the kinds of course. + +preCheck dflags ty_fam_ok tv ty + = fast_check ty + where + details = tcTyVarDetails tv + impredicative_ok = canUnifyWithPolyType dflags details + + ok :: OccCheckResult () + ok = OC_OK () + + fast_check :: TcType -> OccCheckResult () + fast_check (TyVarTy tv') + | tv == tv' = OC_Occurs + | otherwise = fast_check_occ (tyVarKind tv') + -- See Note [Occurrence checking: look inside kinds] + + fast_check (TyConApp tc tys) + | bad_tc tc = OC_Bad + | otherwise = mapM fast_check tys >> ok + fast_check (LitTy {}) = ok + fast_check (FunTy a r) = fast_check a >> fast_check r + fast_check (AppTy fun arg) = fast_check fun >> fast_check arg + fast_check (CastTy ty co) = fast_check ty >> fast_check_co co + fast_check (CoercionTy co) = fast_check_co co + fast_check (ForAllTy (TvBndr tv' _) ty) + | not impredicative_ok = OC_Bad + | tv == tv' = ok + | otherwise = do { fast_check_occ (tyVarKind tv') + ; fast_check_occ ty } + -- Under a forall we look only for occurrences of + -- the type variable + + -- For kinds, we only do an occurs check; we do not worry + -- about type families or foralls + -- See Note [Checking for foralls] + fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs + | otherwise = ok + + -- For coercions, we are only doing an occurs check here; + -- no bother about impredicativity in coercions, as they're + -- inferred + fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs + | otherwise = ok + + bad_tc :: TyCon -> Bool + bad_tc tc + | not (impredicative_ok || isTauTyCon tc) = True + | not (ty_fam_ok || isFamFreeTyCon tc) = True + | otherwise = False + +occCheckExpand :: TcTyVar -> TcType -> Maybe TcType +-- See Note [Occurs check expansion] +-- We may have needed to do some type synonym unfolding in order to +-- get rid of the variable (or forall), so we also return the unfolded +-- version of the type, which is guaranteed to be syntactically free +-- of the given type variable. If the type is already syntactically +-- free of the variable, then the same type is returned. +occCheckExpand tv ty + = go emptyVarEnv ty + where + go :: VarEnv TyVar -> Type -> Maybe Type + -- The VarEnv carries mappings necessary + -- because of kind expansion + go env (TyVarTy tv') + | tv == tv' = Nothing + | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'') + | otherwise = do { k' <- go env (tyVarKind tv') + ; return (mkTyVarTy $ + setTyVarKind tv' k') } + -- See Note [Occurrence checking: look inside kinds] + + go _ ty@(LitTy {}) = return ty + go env (AppTy ty1 ty2) = do { ty1' <- go env ty1 + ; ty2' <- go env ty2 + ; return (mkAppTy ty1' ty2') } + go env (FunTy ty1 ty2) = do { ty1' <- go env ty1 + ; ty2' <- go env ty2 + ; return (mkFunTy ty1' ty2') } + go env ty@(ForAllTy (TvBndr tv' vis) body_ty) + | tv == tv' = return ty + | otherwise = do { ki' <- go env (tyVarKind tv') + ; let tv'' = setTyVarKind tv' ki' + env' = extendVarEnv env tv' tv'' + ; body' <- go env' body_ty + ; return (ForAllTy (TvBndr tv'' vis) body') } + + -- For a type constructor application, first try expanding away the + -- offending variable from the arguments. If that doesn't work, next + -- see if the type constructor is a type synonym, and if so, expand + -- it and try again. + go env ty@(TyConApp tc tys) + = case mapM (go env) tys of + Just tys' -> return (mkTyConApp tc tys') + Nothing | Just ty' <- coreView ty -> go env ty' + | otherwise -> Nothing + -- Failing that, try to expand a synonym + + go env (CastTy ty co) = do { ty' <- go env ty + ; co' <- go_co env co + ; return (mkCastTy ty' co') } + go env (CoercionTy co) = do { co' <- go_co env co + ; return (mkCoercionTy co') } + + ------------------ + go_co env (Refl r ty) = do { ty' <- go env ty + ; return (mkReflCo r ty') } + -- Note: Coercions do not contain type synonyms + go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args + ; return (mkTyConAppCo r tc args') } + go_co env (AppCo co arg) = do { co' <- go_co env co + ; arg' <- go_co env arg + ; return (mkAppCo co' arg') } + go_co env co@(ForAllCo tv' kind_co body_co) + | tv == tv' = return co + | otherwise = do { kind_co' <- go_co env kind_co + ; let tv'' = setTyVarKind tv' $ + pFst (coercionKind kind_co') + env' = extendVarEnv env tv' tv'' + ; body' <- go_co env' body_co + ; return (ForAllCo tv'' kind_co' body') } + go_co env (CoVarCo c) = do { k' <- go env (varType c) + ; return (mkCoVarCo (setVarType c k')) } + go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args + ; return (mkAxiomInstCo ax ind args') } + go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p + ; ty1' <- go env ty1 + ; ty2' <- go env ty2 + ; return (mkUnivCo p' r ty1' ty2') } + go_co env (SymCo co) = do { co' <- go_co env co + ; return (mkSymCo co') } + go_co env (TransCo co1 co2) = do { co1' <- go_co env co1 + ; co2' <- go_co env co2 + ; return (mkTransCo co1' co2') } + go_co env (NthCo n co) = do { co' <- go_co env co + ; return (mkNthCo n co') } + go_co env (LRCo lr co) = do { co' <- go_co env co + ; return (mkLRCo lr co') } + go_co env (InstCo co arg) = do { co' <- go_co env co + ; arg' <- go_co env arg + ; return (mkInstCo co' arg') } + go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1 + ; co2' <- go_co env co2 + ; return (mkCoherenceCo co1' co2') } + go_co env (KindCo co) = do { co' <- go_co env co + ; return (mkKindCo co') } + go_co env (SubCo co) = do { co' <- go_co env co + ; return (mkSubCo co') } + go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs + ; return (mkAxiomRuleCo ax cs') } + + ------------------ + go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv + go_prov env (PhantomProv co) = PhantomProv <$> go_co env co + go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co + go_prov _ p@(PluginProv _) = return p + go_prov _ p@(HoleProv _) = return p + +canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool +canUnifyWithPolyType dflags details + = case details of + MetaTv { mtv_info = SigTv } -> False + MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags + _other -> True + -- We can have non-meta tyvars in given constraints + diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 49767fe1a8..31859e1a1c 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -206,7 +206,7 @@ checkAmbiguity ctxt ty ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $ captureConstraints $ - tcSubType_NC ctxt ty (mkCheckExpType ty) + tcSubType_NC ctxt ty ty ; simplifyAmbiguityCheck ty wanted ; traceTc "Done ambiguity check for" (ppr ty) } diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 1765ff5fe7..bf92c37034 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -1270,11 +1270,13 @@ splitForAllTyVarBndrs ty = split ty ty [] -- | Checks whether this is a proper forall (with a named binder) isForAllTy :: Type -> Bool +isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty' isForAllTy (ForAllTy {}) = True isForAllTy _ = False -- | Is this a function or forall? isPiTy :: Type -> Bool +isPiTy ty | Just ty' <- coreView ty = isForAllTy ty' isPiTy (ForAllTy {}) = True isPiTy (FunTy {}) = True isPiTy _ = False diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs index d4abeae51b..e5b94b1f38 100644 --- a/compiler/vectorise/Vectorise/Generic/PData.hs +++ b/compiler/vectorise/Vectorise/Generic/PData.hs @@ -44,7 +44,7 @@ buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM FamInst buildDataFamInst name' fam_tc vect_tc rhs = do { axiom_name <- mkDerivedName mkInstTyCoOcc name' - ; (_, tyvars') <- liftDs $ tcInstSigTyVars (getSrcSpan name') tyvars + ; (_, tyvars') <- liftDs $ freshenTyVarBndrs tyvars ; let ax = mkSingleCoAxiom Representational axiom_name tyvars' [] fam_tc pat_tys rep_ty tys' = mkTyVarTys tyvars' rep_ty = mkTyConApp rep_tc tys' diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr index 20f04d01e7..6f9e16f2b4 100644 --- a/testsuite/tests/ado/ado004.stderr +++ b/testsuite/tests/ado/ado004.stderr @@ -30,9 +30,9 @@ TYPE SIGNATURES (Num t, Monad m) => (t -> m a2) -> (a2 -> a2 -> m a1) -> m a1 test6 :: - forall a (m :: * -> *) t. + forall a (m :: * -> *) p. (Num (m a), Monad m) => - (m a -> m (m a)) -> t -> m a + (m a -> m (m a)) -> p -> m a TYPE CONSTRUCTORS COERCION AXIOMS Dependent modules: [] diff --git a/testsuite/tests/annotations/should_fail/annfail10.stderr b/testsuite/tests/annotations/should_fail/annfail10.stderr index 6782f27228..6e7732f938 100644 --- a/testsuite/tests/annotations/should_fail/annfail10.stderr +++ b/testsuite/tests/annotations/should_fail/annfail10.stderr @@ -1,8 +1,8 @@ annfail10.hs:9:1: error: - • Ambiguous type variable ‘t0’ arising from an annotation - prevents the constraint ‘(Data.Data.Data t0)’ from being solved. - Probable fix: use a type annotation to specify what ‘t0’ should be. + • Ambiguous type variable ‘p0’ arising from an annotation + prevents the constraint ‘(Data.Data.Data p0)’ from being solved. + Probable fix: use a type annotation to specify what ‘p0’ should be. These potential instances exist: instance (Data.Data.Data a, Data.Data.Data b) => Data.Data.Data (Either a b) @@ -15,9 +15,9 @@ annfail10.hs:9:1: error: • In the annotation: {-# ANN f 1 #-} annfail10.hs:9:11: error: - • Ambiguous type variable ‘t0’ arising from the literal ‘1’ - prevents the constraint ‘(Num t0)’ from being solved. - Probable fix: use a type annotation to specify what ‘t0’ should be. + • Ambiguous type variable ‘p0’ arising from the literal ‘1’ + prevents the constraint ‘(Num p0)’ from being solved. + Probable fix: use a type annotation to specify what ‘p0’ should be. These potential instances exist: instance Num Integer -- Defined in ‘GHC.Num’ instance Num Double -- Defined in ‘GHC.Float’ diff --git a/testsuite/tests/driver/T2182.stderr b/testsuite/tests/driver/T2182.stderr index b5a5f1d349..770135a338 100644 --- a/testsuite/tests/driver/T2182.stderr +++ b/testsuite/tests/driver/T2182.stderr @@ -1,24 +1,24 @@ T2182.hs:5:5: error: - No instance for (Show (t1 -> t1)) arising from a use of ‘show’ - (maybe you haven't applied a function to enough arguments?) - In the expression: show (\ x -> x) - In an equation for ‘y’: y = show (\ x -> x) + • No instance for (Show (p1 -> p1)) arising from a use of ‘show’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: show (\ x -> x) + In an equation for ‘y’: y = show (\ x -> x) T2182.hs:6:5: error: - No instance for (Eq (t0 -> t0)) arising from a use of ‘==’ - (maybe you haven't applied a function to enough arguments?) - In the expression: (\ x -> x) == (\ y -> y) - In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) + • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: (\ x -> x) == (\ y -> y) + In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) T2182.hs:5:5: error: - No instance for (Show (t1 -> t1)) arising from a use of ‘show’ - (maybe you haven't applied a function to enough arguments?) - In the expression: show (\ x -> x) - In an equation for ‘y’: y = show (\ x -> x) + • No instance for (Show (p1 -> p1)) arising from a use of ‘show’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: show (\ x -> x) + In an equation for ‘y’: y = show (\ x -> x) T2182.hs:6:5: error: - No instance for (Eq (t0 -> t0)) arising from a use of ‘==’ - (maybe you haven't applied a function to enough arguments?) - In the expression: (\ x -> x) == (\ y -> y) - In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) + • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: (\ x -> x) == (\ y -> y) + In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr index 056d451a09..41322f9cbc 100644 --- a/testsuite/tests/gadt/gadt-escape1.stderr +++ b/testsuite/tests/gadt/gadt-escape1.stderr @@ -1,19 +1,19 @@ gadt-escape1.hs:19:58: error: - • Couldn't match type ‘t’ with ‘ExpGADT Int’ - ‘t’ is untouchable - inside the constraints: t1 ~ Int + • Couldn't match type ‘p’ with ‘ExpGADT Int’ + ‘p’ is untouchable + inside the constraints: t ~ Int bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int, in a case alternative at gadt-escape1.hs:19:43-50 - ‘t’ is a rigid type variable bound by - the inferred type of weird1 :: t at gadt-escape1.hs:19:1-58 + ‘p’ is a rigid type variable bound by + the inferred type of weird1 :: p at gadt-escape1.hs:19:1-58 Possible fix: add a type signature for ‘weird1’ - Expected type: t - Actual type: ExpGADT t1 + Expected type: p + Actual type: ExpGADT t • In the expression: a In a case alternative: Hidden (ExpInt _) a -> a In the expression: case (hval :: Hidden) of { Hidden (ExpInt _) a -> a } • Relevant bindings include - weird1 :: t (bound at gadt-escape1.hs:19:1) + weird1 :: p (bound at gadt-escape1.hs:19:1) diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr index e304430b51..6673ff68b0 100644 --- a/testsuite/tests/gadt/gadt13.stderr +++ b/testsuite/tests/gadt/gadt13.stderr @@ -1,17 +1,17 @@ gadt13.hs:15:13: error: - • Couldn't match expected type ‘t’ + • Couldn't match expected type ‘p’ with actual type ‘String -> [Char]’ - ‘t’ is untouchable + ‘p’ is untouchable inside the constraints: a ~ Int bound by a pattern with constructor: I :: Int -> Term Int, in an equation for ‘shw’ at gadt13.hs:15:6-8 - ‘t’ is a rigid type variable bound by - the inferred type of shw :: Term a -> t at gadt13.hs:15:1-30 + ‘p’ is a rigid type variable bound by + the inferred type of shw :: Term a -> p at gadt13.hs:15:1-30 Possible fix: add a type signature for ‘shw’ • Possible cause: ‘(.)’ is applied to too many arguments In the expression: ("I " ++) . shows t In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t • Relevant bindings include - shw :: Term a -> t (bound at gadt13.hs:15:1) + shw :: Term a -> p (bound at gadt13.hs:15:1) diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr index e66226eaea..f75e8c5bff 100644 --- a/testsuite/tests/gadt/gadt7.stderr +++ b/testsuite/tests/gadt/gadt7.stderr @@ -1,20 +1,20 @@ gadt7.hs:16:38: error: - • Couldn't match expected type ‘t’ with actual type ‘t1’ - ‘t’ is untouchable + • Couldn't match expected type ‘p’ with actual type ‘p1’ + ‘p1’ is untouchable inside the constraints: a ~ Int bound by a pattern with constructor: K :: T Int, in a case alternative at gadt7.hs:16:33 - ‘t’ is a rigid type variable bound by - the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44 - ‘t1’ is a rigid type variable bound by - the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44 + ‘p1’ is a rigid type variable bound by + the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44 + ‘p’ is a rigid type variable bound by + the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44 Possible fix: add a type signature for ‘i1b’ • In the expression: y1 In a case alternative: K -> y1 In the expression: case t1 of { K -> y1 } • Relevant bindings include - y1 :: t1 (bound at gadt7.hs:16:16) - y :: t1 (bound at gadt7.hs:16:7) - i1b :: T a -> t1 -> t (bound at gadt7.hs:16:1) + y1 :: p1 (bound at gadt7.hs:16:16) + y :: p1 (bound at gadt7.hs:16:7) + i1b :: T a -> p1 -> p (bound at gadt7.hs:16:1) diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout index 904f0cd3e8..2e86b42713 100644 --- a/testsuite/tests/ghci.debugger/scripts/break012.stdout +++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout @@ -1,14 +1,14 @@ Stopped in Main.g, break012.hs:5:10-18 -_result :: (t, a1 -> a1, (), a -> a -> a) = _ -a :: t = _ +_result :: (p, a1 -> a1, (), a -> a -> a) = _ +a :: p = _ b :: a2 -> a2 = _ c :: () = _ d :: a -> a -> a = _ -a :: t +a :: p b :: a2 -> a2 c :: () d :: a -> a -> a -a = (_t1::t) +a = (_t1::p) b = (_t2::a2 -> a2) c = (_t3::()) d = (_t4::a -> a -> a) diff --git a/testsuite/tests/ghci.debugger/scripts/print022.stdout b/testsuite/tests/ghci.debugger/scripts/print022.stdout index 40d2b59544..5d81c044c4 100644 --- a/testsuite/tests/ghci.debugger/scripts/print022.stdout +++ b/testsuite/tests/ghci.debugger/scripts/print022.stdout @@ -2,7 +2,7 @@ test = C 1 32 1.2 1.23 'x' 1 1.2 1.23 Breakpoint 0 activated at print022.hs:11:7 Stopped in Main.f, print022.hs:11:7 -_result :: t = _ -x :: t = _ +_result :: p = _ +x :: p = _ x = C2 1 (W# 32) (TwoFields 'a' 3) x :: T2 diff --git a/testsuite/tests/ghci/scripts/T11524a.stdout b/testsuite/tests/ghci/scripts/T11524a.stdout index 164e0cf256..27122574e9 100644 --- a/testsuite/tests/ghci/scripts/T11524a.stdout +++ b/testsuite/tests/ghci/scripts/T11524a.stdout @@ -2,7 +2,7 @@ without -fprint-explicit-foralls ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pattern P :: Bool -- Defined at <interactive>:16:1 pattern Pe :: a -> Ex -- Defined at <interactive>:17:1 -pattern Pu :: t -> t -- Defined at <interactive>:18:1 +pattern Pu :: p -> p -- Defined at <interactive>:18:1 pattern Pue :: a -> a1 -> (a, Ex) -- Defined at <interactive>:19:1 pattern Pur :: (Num a, Eq a) => a -> [a] -- Defined at <interactive>:20:1 @@ -26,7 +26,7 @@ with -fprint-explicit-foralls pattern P :: Bool -- Defined at <interactive>:16:1 pattern Pe :: () => forall {a}. a -> Ex -- Defined at <interactive>:17:1 -pattern Pu :: forall {t}. t -> t -- Defined at <interactive>:18:1 +pattern Pu :: forall {p}. p -> p -- Defined at <interactive>:18:1 pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex) -- Defined at <interactive>:19:1 pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a] diff --git a/testsuite/tests/ghci/scripts/T2182ghci.stderr b/testsuite/tests/ghci/scripts/T2182ghci.stderr index 8a8d3dd65b..5f601942ca 100644 --- a/testsuite/tests/ghci/scripts/T2182ghci.stderr +++ b/testsuite/tests/ghci/scripts/T2182ghci.stderr @@ -1,25 +1,25 @@ <interactive>:2:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:10:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:19:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:28:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:49:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it diff --git a/testsuite/tests/indexed-types/should_fail/T12386.hs b/testsuite/tests/indexed-types/should_fail/T12386.hs new file mode 100644 index 0000000000..c07881a6bd --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T12386.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeFamilies #-} + +module T12386 where + +class C a where + type family F a t :: * + + type family T a :: * + type T a = F a diff --git a/testsuite/tests/indexed-types/should_fail/T12386.stderr b/testsuite/tests/indexed-types/should_fail/T12386.stderr new file mode 100644 index 0000000000..66d812e1fd --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T12386.stderr @@ -0,0 +1,7 @@ + +T12386.hs:9:15: error: + • Expecting one more argument to ‘F a’ + Expected a type, but ‘F a’ has kind ‘* -> *’ + • In the type ‘F a’ + In the default type instance declaration for ‘T’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr index f1ae705f5e..9cc8912814 100644 --- a/testsuite/tests/indexed-types/should_fail/T5439.stderr +++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr @@ -1,13 +1,15 @@ -T5439.hs:82:28: error: - • Couldn't match type ‘Attempt (WaitOpResult (WaitOps rs))’ - with ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’ - Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0)) - Actual type: f (Attempt (WaitOpResult (WaitOps rs))) - • In the first argument of ‘complete’, namely ‘ev’ - In the expression: complete ev +T5439.hs:82:33: error: + • Couldn't match expected type ‘Attempt (HElemOf rs)’ + with actual type ‘Attempt (HHead (HDrop n0 l0)) + -> Attempt (HElemOf l0)’ + • In the second argument of ‘($)’, namely + ‘inj $ Failure (e :: SomeException)’ In a stmt of a 'do' block: c <- complete ev $ inj $ Failure (e :: SomeException) + In the expression: + do { c <- complete ev $ inj $ Failure (e :: SomeException); + return $ c || not first } • Relevant bindings include register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool (bound at T5439.hs:64:9) diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr index 0332181394..b7b70b8f4e 100644 --- a/testsuite/tests/indexed-types/should_fail/T7354.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr @@ -1,11 +1,11 @@ T7354.hs:28:11: error: • Occurs check: cannot construct the infinite type: - t ~ Base t1 (Prim [t] t) - Expected type: Prim [t] t -> Base t1 (Prim [t] t) - Actual type: Prim [t] t -> t + p ~ Base t (Prim [p] p) + Expected type: Prim [p] p -> Base t (Prim [p] p) + Actual type: Prim [p] p -> p • In the first argument of ‘ana’, namely ‘alg’ In the expression: ana alg In an equation for ‘foo’: foo = ana alg • Relevant bindings include - foo :: Prim [t] t -> t1 (bound at T7354.hs:28:1) + foo :: Prim [p] p -> t (bound at T7354.hs:28:1) diff --git a/testsuite/tests/parser/should_compile/read014.stderr b/testsuite/tests/parser/should_compile/read014.stderr index 09e79ee52c..228672b7a5 100644 --- a/testsuite/tests/parser/should_compile/read014.stderr +++ b/testsuite/tests/parser/should_compile/read014.stderr @@ -1,7 +1,7 @@ read014.hs:4:1: warning: [-Wmissing-signatures (in -Wall)] Top-level binding with no type signature: - ng1 :: Num a => t -> a -> a + ng1 :: Num a => p -> a -> a read014.hs:4:5: warning: [-Wunused-matches (in -Wextra)] Defined but not used: ‘x’ diff --git a/testsuite/tests/parser/should_fail/T7848.stderr b/testsuite/tests/parser/should_fail/T7848.stderr index f7617ee606..fe949d944a 100644 --- a/testsuite/tests/parser/should_fail/T7848.stderr +++ b/testsuite/tests/parser/should_fail/T7848.stderr @@ -1,10 +1,7 @@ T7848.hs:6:1: error: • Occurs check: cannot construct the infinite type: - t ~ t0 -> t1 -> A -> A -> A -> A -> t2 -> t - • When checking that: - t0 -> t1 -> A -> A -> A -> A -> forall t2. t2 -> t - is more polymorphic than: t + t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t • Relevant bindings include x :: t (bound at T7848.hs:6:1) T7848.hs:10:9: error: diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr index 963bc50d72..2dca583aba 100644 --- a/testsuite/tests/parser/should_fail/readFail003.stderr +++ b/testsuite/tests/parser/should_fail/readFail003.stderr @@ -1,7 +1,7 @@ readFail003.hs:4:27: error: • Occurs check: cannot construct the infinite type: - t ~ (t, [a1], [a]) + a2 ~ (a2, [a1], [a]) • In the expression: a In a pattern binding: ~(a, b, c) @@ -11,6 +11,6 @@ readFail003.hs:4:27: error: where nullity = null • Relevant bindings include - a :: t (bound at readFail003.hs:4:3) + a :: a2 (bound at readFail003.hs:4:3) b :: [a1] (bound at readFail003.hs:4:5) c :: [a] (bound at readFail003.hs:4:7) diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr index ebf2a759b7..c5238bb474 100644 --- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr @@ -1,8 +1,8 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘t2’ - Where: ‘t2’ is a rigid type variable bound by - the inferred type of g :: t2 -> t2 at T10438.hs:(6,9)-(8,21) + • Found type wildcard ‘_’ standing for ‘p2’ + Where: ‘p2’ is a rigid type variable bound by + the inferred type of g :: p2 -> p2 at T10438.hs:(6,9)-(8,21) • In the type signature: x :: _ In an equation for ‘g’: g r @@ -20,7 +20,7 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)] x :: _ x = r • Relevant bindings include - r :: t2 (bound at T10438.hs:6:11) - g :: t2 -> t2 (bound at T10438.hs:6:9) - f :: t1 (bound at T10438.hs:5:5) - foo :: t1 -> forall t. t -> t (bound at T10438.hs:5:1) + r :: p2 (bound at T10438.hs:6:11) + g :: p2 -> p2 (bound at T10438.hs:6:9) + f :: p1 (bound at T10438.hs:5:5) + foo :: p1 -> p -> p (bound at T10438.hs:5:1) diff --git a/testsuite/tests/partial-sigs/should_compile/T11192.stderr b/testsuite/tests/partial-sigs/should_compile/T11192.stderr index 7abf6e5845..8e47c4bb70 100644 --- a/testsuite/tests/partial-sigs/should_compile/T11192.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T11192.stderr @@ -1,8 +1,8 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘Int -> t -> t’ - Where: ‘t’ is a rigid type variable bound by - the inferred type of go :: Int -> t -> t at T11192.hs:8:8-17 + • Found type wildcard ‘_’ standing for ‘Int -> p -> p’ + Where: ‘p’ is a rigid type variable bound by + the inferred type of go :: Int -> p -> p at T11192.hs:8:8-17 • In the type signature: go :: _ In the expression: let @@ -18,11 +18,11 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)] • Relevant bindings include fails :: a (bound at T11192.hs:6:1) T11192.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘t1 -> t -> t’ - Where: ‘t1’ is a rigid type variable bound by - the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17 - ‘t’ is a rigid type variable bound by - the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17 + • Found type wildcard ‘_’ standing for ‘p1 -> p -> p’ + Where: ‘p1’ is a rigid type variable bound by + the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17 + ‘p’ is a rigid type variable bound by + the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17 • In the type signature: go :: _ In the expression: let diff --git a/testsuite/tests/patsyn/should_compile/T11213.stderr b/testsuite/tests/patsyn/should_compile/T11213.stderr index 9c438dd176..838d75c3c7 100644 --- a/testsuite/tests/patsyn/should_compile/T11213.stderr +++ b/testsuite/tests/patsyn/should_compile/T11213.stderr @@ -8,7 +8,7 @@ T11213.hs:20:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)] T11213.hs:21:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)] Pattern synonym with no type signature: - pattern Pu :: forall t. t -> t + pattern Pu :: forall p. p -> p T11213.hs:22:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)] Pattern synonym with no type signature: diff --git a/testsuite/tests/patsyn/should_fail/mono.stderr b/testsuite/tests/patsyn/should_fail/mono.stderr index 20714e7565..8f370ce2f0 100644 --- a/testsuite/tests/patsyn/should_fail/mono.stderr +++ b/testsuite/tests/patsyn/should_fail/mono.stderr @@ -1,8 +1,8 @@ mono.hs:7:4: error: • Couldn't match type ‘Bool’ with ‘Int’ - Expected type: [Int] - Actual type: [Bool] + Expected type: [Bool] + Actual type: [Int] • In the pattern: Single x In an equation for ‘f’: f (Single x) = x diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr index 9f8f62e25e..7a079ff102 100644 --- a/testsuite/tests/polykinds/T7438.stderr +++ b/testsuite/tests/polykinds/T7438.stderr @@ -1,19 +1,19 @@ T7438.hs:6:14: error: - • Couldn't match expected type ‘t’ with actual type ‘t1’ - ‘t’ is untouchable + • Couldn't match expected type ‘p’ with actual type ‘p1’ + ‘p1’ is untouchable inside the constraints: b ~ a bound by a pattern with constructor: Nil :: forall k (a :: k). Thrist a a, in an equation for ‘go’ at T7438.hs:6:4-6 - ‘t’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16 - ‘t1’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16 + ‘p1’ is a rigid type variable bound by + the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16 + ‘p’ is a rigid type variable bound by + the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16 Possible fix: add a type signature for ‘go’ • In the expression: acc In an equation for ‘go’: go Nil acc = acc • Relevant bindings include - acc :: t1 (bound at T7438.hs:6:8) - go :: Thrist a b -> t1 -> t (bound at T7438.hs:6:1) + acc :: p1 (bound at T7438.hs:6:8) + go :: Thrist a b -> p1 -> p (bound at T7438.hs:6:1) diff --git a/testsuite/tests/rebindable/rebindable6.stderr b/testsuite/tests/rebindable/rebindable6.stderr index 241cf76962..712724d28f 100644 --- a/testsuite/tests/rebindable/rebindable6.stderr +++ b/testsuite/tests/rebindable/rebindable6.stderr @@ -25,15 +25,15 @@ rebindable6.hs:110:17: error: return b } rebindable6.hs:111:17: error: - • Ambiguous type variables ‘t1’, ‘t0’ arising from a do statement + • Ambiguous type variables ‘p0’, ‘t0’ arising from a do statement prevents the constraint ‘(HasBind - (IO (Maybe b) -> (Maybe b -> t1) -> t0))’ from being solved. + (IO (Maybe b) -> (Maybe b -> p0) -> t0))’ from being solved. (maybe you haven't applied a function to enough arguments?) Relevant bindings include g :: IO (Maybe b) (bound at rebindable6.hs:108:19) test_do :: IO a -> IO (Maybe b) -> IO b (bound at rebindable6.hs:108:9) - Probable fix: use a type annotation to specify what ‘t1’, ‘t0’ should be. + Probable fix: use a type annotation to specify what ‘p0’, ‘t0’ should be. These potential instance exist: instance HasBind (IO a -> (a -> IO b) -> IO b) -- Defined at rebindable6.hs:51:18 @@ -49,15 +49,15 @@ rebindable6.hs:111:17: error: return b } rebindable6.hs:112:17: error: - • Ambiguous type variable ‘t1’ arising from a use of ‘return’ - prevents the constraint ‘(HasReturn (b -> t1))’ from being solved. + • Ambiguous type variable ‘p0’ arising from a use of ‘return’ + prevents the constraint ‘(HasReturn (b -> p0))’ from being solved. (maybe you haven't applied a function to enough arguments?) Relevant bindings include b :: b (bound at rebindable6.hs:111:23) g :: IO (Maybe b) (bound at rebindable6.hs:108:19) test_do :: IO a -> IO (Maybe b) -> IO b (bound at rebindable6.hs:108:9) - Probable fix: use a type annotation to specify what ‘t1’ should be. + Probable fix: use a type annotation to specify what ‘p0’ should be. These potential instance exist: instance HasReturn (a -> IO a) -- Defined at rebindable6.hs:46:18 • In a stmt of a 'do' block: return b diff --git a/testsuite/tests/rename/should_compile/T12597.stderr b/testsuite/tests/rename/should_compile/T12597.stderr index 8364fd07b3..e3df440372 100644 --- a/testsuite/tests/rename/should_compile/T12597.stderr +++ b/testsuite/tests/rename/should_compile/T12597.stderr @@ -1,3 +1,3 @@ T12597.hs:5:1: warning: [-Wmissing-signatures (in -Wall)] - Top-level binding with no type signature: f :: t -> t + Top-level binding with no type signature: f :: p -> p diff --git a/testsuite/tests/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr index 982686868f..df20e67f3a 100644 --- a/testsuite/tests/roles/should_compile/T8958.stderr +++ b/testsuite/tests/roles/should_compile/T8958.stderr @@ -65,7 +65,8 @@ AbsBinds [a] [] Exported types: T8958.$fRepresentationala [InlPrag=[ALWAYS] CONLIKE] :: forall a. Representational a [LclIdX[DFunId], - Unf=DFun: \ (@ a[ssk]) -> T8958.C:Representational TYPE: a[ssk]] + Unf=DFun: \ (@ a[ssk:2]) -> + T8958.C:Representational TYPE: a[ssk:2]] Binds: $dRepresentational = T8958.C:Representational @ a Evidence: [EvBinds{}]} AbsBinds [a] [] @@ -74,7 +75,7 @@ AbsBinds [a] [] Exported types: T8958.$fNominala [InlPrag=[ALWAYS] CONLIKE] :: forall a. Nominal a [LclIdX[DFunId], - Unf=DFun: \ (@ a[ssk]) -> T8958.C:Nominal TYPE: a[ssk]] + Unf=DFun: \ (@ a[ssk:2]) -> T8958.C:Nominal TYPE: a[ssk:2]] Binds: $dNominal = T8958.C:Nominal @ a Evidence: [EvBinds{}]} diff --git a/testsuite/tests/simplCore/should_compile/noinline01.stderr b/testsuite/tests/simplCore/should_compile/noinline01.stderr index cecaad16f0..b100172381 100644 --- a/testsuite/tests/simplCore/should_compile/noinline01.stderr +++ b/testsuite/tests/simplCore/should_compile/noinline01.stderr @@ -1,7 +1,7 @@ ==================== Pre unarise: ==================== Noinline01.f [InlPrag=INLINE (sat-args=1)] - :: forall t. t -> GHC.Types.Bool + :: forall p. p -> GHC.Types.Bool [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] = \r [eta] GHC.Types.True []; @@ -26,7 +26,7 @@ Noinline01.$trModule :: GHC.Types.Module ==================== STG syntax: ==================== Noinline01.f [InlPrag=INLINE (sat-args=1)] - :: forall t. t -> GHC.Types.Bool + :: forall p. p -> GHC.Types.Bool [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] = \r [eta] GHC.Types.True []; diff --git a/testsuite/tests/th/T11452.stderr b/testsuite/tests/th/T11452.stderr index f59fcbd7d2..32064a9c78 100644 --- a/testsuite/tests/th/T11452.stderr +++ b/testsuite/tests/th/T11452.stderr @@ -7,7 +7,7 @@ T11452.hs:6:14: error: In an equation for ‘impred’: impred = $$([|| \ _ -> () ||]) T11452.hs:6:14: error: - • Cannot instantiate unification variable ‘t0’ + • Cannot instantiate unification variable ‘p0’ with a type involving foralls: forall a. a -> a GHC doesn't yet support impredicative polymorphism • In the Template Haskell quotation [|| \ _ -> () ||] diff --git a/testsuite/tests/th/T2222.stderr b/testsuite/tests/th/T2222.stderr index 4ddf100bf6..3265a5e938 100644 --- a/testsuite/tests/th/T2222.stderr +++ b/testsuite/tests/th/T2222.stderr @@ -1,4 +1,4 @@ -inside b: t_0 +inside b: p_0 inside d: GHC.Types.Bool type of c: GHC.Types.Bool inside f: GHC.Types.Bool diff --git a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr index 696bff740d..6cc24fcaf6 100644 --- a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr +++ b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr @@ -1,6 +1,6 @@ ExPatFail.hs:12:15: error: - • Couldn't match expected type ‘t’ with actual type ‘a’ + • Couldn't match expected type ‘p’ with actual type ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: @@ -11,4 +11,4 @@ ExPatFail.hs:12:15: error: In a pattern binding: MkT y _ = x In the expression: let MkT y _ = x in y • Relevant bindings include - f :: T -> t (bound at ExPatFail.hs:12:1) + f :: T -> p (bound at ExPatFail.hs:12:1) diff --git a/testsuite/tests/typecheck/should_compile/T12427.stderr b/testsuite/tests/typecheck/should_compile/T12427.stderr new file mode 100644 index 0000000000..0519ecba6e --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12427.stderr @@ -0,0 +1 @@ +
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr new file mode 100644 index 0000000000..fc2aece398 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr @@ -0,0 +1,33 @@ + +T12427a.hs:17:29: error: + • Couldn't match expected type ‘p’ + with actual type ‘(forall b. [b] -> [b]) -> Int’ + ‘p’ is untouchable + inside the constraints: () + bound by a pattern with constructor: + T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T, + in a case alternative + at T12427a.hs:17:19-24 + ‘p’ is a rigid type variable bound by + the inferred type of h11 :: T -> p at T12427a.hs:17:1-29 + Possible fix: add a type signature for ‘h11’ + • In the expression: v + In a case alternative: T1 _ v -> v + In the expression: case y of { T1 _ v -> v } + • Relevant bindings include + h11 :: T -> p (bound at T12427a.hs:17:1) + +T12427a.hs:28:6: error: + • Couldn't match expected type ‘p’ + with actual type ‘(forall b. [b] -> [b]) -> Int’ + ‘p’ is untouchable + inside the constraints: () + bound by a pattern with constructor: + T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T, + in a pattern binding + at T12427a.hs:28:1-7 + ‘p’ is a rigid type variable bound by + the inferred type of x1 :: p at T12427a.hs:28:1-19 + Possible fix: add a type signature for ‘x1’ + • In the pattern: T1 _ x1 + In a pattern binding: T1 _ x1 = undefined diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr index d205fa9ced..7d0f0815dc 100644 --- a/testsuite/tests/typecheck/should_compile/tc141.stderr +++ b/testsuite/tests/typecheck/should_compile/tc141.stderr @@ -35,7 +35,7 @@ tc141.hs:13:13: error: in v tc141.hs:15:18: error: - • Couldn't match expected type ‘a2’ with actual type ‘t’ + • Couldn't match expected type ‘a2’ with actual type ‘p’ because type variable ‘a2’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: @@ -50,5 +50,5 @@ tc141.hs:15:18: error: in v • Relevant bindings include v :: a2 (bound at tc141.hs:15:14) - b :: t (bound at tc141.hs:13:5) - g :: a1 -> t -> forall a. a (bound at tc141.hs:13:1) + b :: p (bound at tc141.hs:13:5) + g :: a1 -> p -> a (bound at tc141.hs:13:1) diff --git a/testsuite/tests/typecheck/should_fail/T10495.stderr b/testsuite/tests/typecheck/should_fail/T10495.stderr index e09e60af23..5067d25183 100644 --- a/testsuite/tests/typecheck/should_fail/T10495.stderr +++ b/testsuite/tests/typecheck/should_fail/T10495.stderr @@ -1,8 +1,8 @@ -T10495.hs:5:1: error: +T10495.hs:5:7: error: • Couldn't match representation of type ‘a0’ with that of ‘b0’ arising from a use of ‘coerce’ - • When instantiating ‘foo’, initially inferred to have - this overly-general type: - forall a b. Coercible a b => a -> b - NB: This instantiation can be caused by the monomorphism restriction. + • In the expression: coerce + In an equation for ‘foo’: foo = coerce + • Relevant bindings include + foo :: a0 -> b0 (bound at T10495.hs:5:1) diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr index 7a27229369..fde2daf8c6 100644 --- a/testsuite/tests/typecheck/should_fail/T10619.stderr +++ b/testsuite/tests/typecheck/should_fail/T10619.stderr @@ -17,7 +17,7 @@ T10619.hs:9:15: error: else \ y -> y • Relevant bindings include - foo :: t -> (b -> b) -> b -> b (bound at T10619.hs:8:1) + foo :: p -> (b -> b) -> b -> b (bound at T10619.hs:8:1) T10619.hs:14:15: error: • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’ @@ -37,7 +37,7 @@ T10619.hs:14:15: error: else ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b) • Relevant bindings include - bar :: t -> (b -> b) -> b -> b (bound at T10619.hs:12:1) + bar :: p -> (b -> b) -> b -> b (bound at T10619.hs:12:1) T10619.hs:16:13: error: • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’ diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr index 48bf94d2ce..03c885a577 100644 --- a/testsuite/tests/typecheck/should_fail/T12177.stderr +++ b/testsuite/tests/typecheck/should_fail/T12177.stderr @@ -2,27 +2,24 @@ T12177.hs:3:19: error: • Found hole: _ :: t Where: ‘t’ is a rigid type variable bound by - the inferred type of bar :: t2 -> t1 -> t - at T12177.hs:3:1-19 + the inferred type of bar :: p1 -> p -> t at T12177.hs:3:1-19 • In the expression: _ In the expression: \ x -> _ In the expression: \ x -> \ x -> _ • Relevant bindings include - x :: t1 (bound at T12177.hs:3:14) - bar :: t2 -> t1 -> t (bound at T12177.hs:3:1) + x :: p (bound at T12177.hs:3:14) + bar :: p1 -> p -> t (bound at T12177.hs:3:1) T12177.hs:5:37: error: • Found hole: _ :: t Where: ‘t’ is a rigid type variable bound by - the inferred type of baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t + the inferred type of baz :: p4 -> p3 -> p2 -> p1 -> p -> t at T12177.hs:5:1-37 • In the expression: _ In the expression: \ z -> _ In the expression: \ x -> \ z -> _ • Relevant bindings include - z :: t1 (bound at T12177.hs:5:32) - x :: t2 (bound at T12177.hs:5:26) - y :: t4 (bound at T12177.hs:5:14) - baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t - (bound at T12177.hs:5:1) -
\ No newline at end of file + z :: p (bound at T12177.hs:5:32) + x :: p1 (bound at T12177.hs:5:26) + y :: p3 (bound at T12177.hs:5:14) + baz :: p4 -> p3 -> p2 -> p1 -> p -> t (bound at T12177.hs:5:1) diff --git a/testsuite/tests/typecheck/should_fail/T3102.hs b/testsuite/tests/typecheck/should_fail/T3102.hs index dd5abb25e1..910ac06ee9 100644 --- a/testsuite/tests/typecheck/should_fail/T3102.hs +++ b/testsuite/tests/typecheck/should_fail/T3102.hs @@ -1,5 +1,5 @@ {-# OPTIONS -XImplicitParams -XRankNTypes #-} - module Bug where +module Bug where t :: forall a. ((?p :: Int) => a) -> String t _ = "Hello" @@ -10,3 +10,7 @@ f _ = 3 result :: Int result = f t + +-- This should work. +-- Elaborated result = f (/\a. \x:a. t @a (\p::Int. x)) +-- But it did not work in 8.0.1; fixed in HEAD diff --git a/testsuite/tests/typecheck/should_fail/T3102.stderr b/testsuite/tests/typecheck/should_fail/T3102.stderr index 66979ddf8b..e69de29bb2 100644 --- a/testsuite/tests/typecheck/should_fail/T3102.stderr +++ b/testsuite/tests/typecheck/should_fail/T3102.stderr @@ -1,12 +0,0 @@ - -T3102.hs:11:12: error: - • Couldn't match type ‘a’ with ‘(?p::Int) => a0’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. a -> String - at T3102.hs:11:10-12 - Expected type: a -> String - Actual type: ((?p::Int) => a0) -> String - • In the first argument of ‘f’, namely ‘t’ - In the expression: f t - In an equation for ‘result’: result = f t diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr index 6b8e920004..9157e116f5 100644 --- a/testsuite/tests/typecheck/should_fail/T7453.stderr +++ b/testsuite/tests/typecheck/should_fail/T7453.stderr @@ -1,13 +1,13 @@ T7453.hs:9:15: error: - • Couldn't match type ‘t’ with ‘t1’ - because type variable ‘t1’ would escape its scope + • Couldn't match type ‘p’ with ‘t’ + because type variable ‘t’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - z :: Id t1 + z :: Id t at T7453.hs:8:11-19 - Expected type: Id t1 - Actual type: Id t + Expected type: Id t + Actual type: Id p • In the expression: aux In an equation for ‘z’: z = aux @@ -22,20 +22,20 @@ T7453.hs:9:15: error: where aux = Id v • Relevant bindings include - aux :: Id t (bound at T7453.hs:10:21) - z :: Id t1 (bound at T7453.hs:9:11) - v :: t (bound at T7453.hs:7:7) - cast1 :: t -> a (bound at T7453.hs:7:1) + aux :: Id p (bound at T7453.hs:10:21) + z :: Id t (bound at T7453.hs:9:11) + v :: p (bound at T7453.hs:7:7) + cast1 :: p -> a (bound at T7453.hs:7:1) T7453.hs:15:15: error: - • Couldn't match type ‘t1’ with ‘t2’ - because type variable ‘t2’ would escape its scope + • Couldn't match type ‘p’ with ‘t1’ + because type variable ‘t1’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - z :: () -> t2 + z :: () -> t1 at T7453.hs:14:11-22 - Expected type: () -> t2 - Actual type: () -> t1 + Expected type: () -> t1 + Actual type: () -> p • In the expression: aux In an equation for ‘z’: z = aux @@ -50,17 +50,17 @@ T7453.hs:15:15: error: where aux = const v • Relevant bindings include - aux :: forall b. b -> t1 (bound at T7453.hs:16:21) - z :: () -> t2 (bound at T7453.hs:15:11) - v :: t1 (bound at T7453.hs:13:7) - cast2 :: t1 -> t (bound at T7453.hs:13:1) + aux :: forall b. b -> p (bound at T7453.hs:16:21) + z :: () -> t1 (bound at T7453.hs:15:11) + v :: p (bound at T7453.hs:13:7) + cast2 :: p -> t (bound at T7453.hs:13:1) T7453.hs:21:15: error: - • Couldn't match expected type ‘t2’ with actual type ‘t1’ - because type variable ‘t2’ would escape its scope + • Couldn't match expected type ‘t1’ with actual type ‘p’ + because type variable ‘t1’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - z :: t2 + z :: t1 at T7453.hs:20:11-16 • In the expression: v In an equation for ‘z’: @@ -76,7 +76,7 @@ T7453.hs:21:15: error: where aux = const v • Relevant bindings include - aux :: forall b. b -> t1 (bound at T7453.hs:22:21) - z :: t2 (bound at T7453.hs:21:11) - v :: t1 (bound at T7453.hs:19:7) - cast3 :: t1 -> forall t. t (bound at T7453.hs:19:1) + aux :: forall b. b -> p (bound at T7453.hs:22:21) + z :: t1 (bound at T7453.hs:21:11) + v :: p (bound at T7453.hs:19:7) + cast3 :: p -> t (bound at T7453.hs:19:1) diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr index 8553fdb888..a39b0488c3 100644 --- a/testsuite/tests/typecheck/should_fail/T7734.stderr +++ b/testsuite/tests/typecheck/should_fail/T7734.stderr @@ -1,18 +1,18 @@ T7734.hs:4:13: error: - • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1 + • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t • In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘f’: x `f` y = x x • Relevant bindings include - x :: t2 -> t1 (bound at T7734.hs:4:1) - f :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:4:3) + x :: t1 -> t (bound at T7734.hs:4:1) + f :: (t1 -> t) -> p -> t (bound at T7734.hs:4:3) T7734.hs:5:13: error: - • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1 + • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t • In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘&’: (&) x y = x x • Relevant bindings include - x :: t2 -> t1 (bound at T7734.hs:5:5) - (&) :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:5:1) + x :: t1 -> t (bound at T7734.hs:5:5) + (&) :: (t1 -> t) -> p -> t (bound at T7734.hs:5:1) diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr index ce1b09d51c..f30c49bde6 100644 --- a/testsuite/tests/typecheck/should_fail/T9109.stderr +++ b/testsuite/tests/typecheck/should_fail/T9109.stderr @@ -1,14 +1,14 @@ T9109.hs:8:13: error: - • Couldn't match expected type ‘t’ with actual type ‘Bool’ - ‘t’ is untouchable + • Couldn't match expected type ‘p’ with actual type ‘Bool’ + ‘p’ is untouchable inside the constraints: a ~ Bool bound by a pattern with constructor: GBool :: G Bool, in an equation for ‘foo’ at T9109.hs:8:5-9 - ‘t’ is a rigid type variable bound by - the inferred type of foo :: G a -> t at T9109.hs:8:1-16 + ‘p’ is a rigid type variable bound by + the inferred type of foo :: G a -> p at T9109.hs:8:1-16 Possible fix: add a type signature for ‘foo’ • In the expression: True In an equation for ‘foo’: foo GBool = True - • Relevant bindings include foo :: G a -> t (bound at T9109.hs:8:1) + • Relevant bindings include foo :: G a -> p (bound at T9109.hs:8:1) diff --git a/testsuite/tests/typecheck/should_fail/T9318.stderr b/testsuite/tests/typecheck/should_fail/T9318.stderr index 218ae97b77..c637788a7e 100644 --- a/testsuite/tests/typecheck/should_fail/T9318.stderr +++ b/testsuite/tests/typecheck/should_fail/T9318.stderr @@ -1,7 +1,7 @@ -T9318.hs:12:5: - Couldn't match type ‘Char’ with ‘Bool’ - Expected type: F Int - Actual type: Char - In the pattern: 'x' - In an equation for ‘bar’: bar 'x' = () +T9318.hs:12:5: error: + • Couldn't match type ‘Bool’ with ‘Char’ + Expected type: F Int + Actual type: Char + • In the pattern: 'x' + In an equation for ‘bar’: bar 'x' = () diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr index ff90a738c9..17486dfefa 100644 --- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr +++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr @@ -13,7 +13,7 @@ VtaFail.hs:12:26: error: answer_constraint_fail = addOne @Bool 5 VtaFail.hs:14:17: error: - • Cannot apply expression of type ‘t1 -> t1’ + • Cannot apply expression of type ‘p0 -> p0’ to a visible type argument ‘Int’ • In the expression: (\ x -> x) @Int 12 In an equation for ‘answer_lambda’: diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 98c57e833e..4f2dbc43d5 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -208,7 +208,7 @@ test('T2806', normal, compile_fail, ['']) test('T3323', normal, compile_fail, ['']) test('T3406', normal, compile_fail, ['']) test('T3540', normal, compile_fail, ['']) -test('T3102', normal, compile_fail, ['']) +test('T3102', normal, compile, ['']) test('T3613', normal, compile_fail, ['']) test('fd-loop', normal, compile_fail, ['']) test('T3950', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr index 6755636682..d72a34065e 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr @@ -1,8 +1,8 @@ tcfail002.hs:4:7: error: - • Occurs check: cannot construct the infinite type: t ~ [t] + • Occurs check: cannot construct the infinite type: p ~ [p] • In the expression: z In an equation for ‘c’: c z = z • Relevant bindings include - z :: [t] (bound at tcfail002.hs:4:3) - c :: [t] -> t (bound at tcfail002.hs:3:1) + z :: [p] (bound at tcfail002.hs:4:3) + c :: [p] -> p (bound at tcfail002.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr index 41a55c1ea9..7bf64d841a 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr @@ -1,9 +1,9 @@ tcfail004.hs:3:9: error: - • Couldn't match expected type ‘(t1, t)’ + • Couldn't match expected type ‘(a, b)’ with actual type ‘(Integer, Integer, Integer)’ • In the expression: (1, 2, 3) In a pattern binding: (f, g) = (1, 2, 3) • Relevant bindings include - f :: t1 (bound at tcfail004.hs:3:2) - g :: t (bound at tcfail004.hs:3:4) + f :: a (bound at tcfail004.hs:3:2) + g :: b (bound at tcfail004.hs:3:4) diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr index 77437cf583..56db4cf58b 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr @@ -1,9 +1,9 @@ tcfail005.hs:3:9: error: - • Couldn't match expected type ‘[t]’ + • Couldn't match expected type ‘[a]’ with actual type ‘(Integer, Char)’ • In the expression: (1, 'a') In a pattern binding: (h : i) = (1, 'a') • Relevant bindings include - h :: t (bound at tcfail005.hs:3:2) - i :: [t] (bound at tcfail005.hs:3:4) + h :: a (bound at tcfail005.hs:3:2) + i :: [a] (bound at tcfail005.hs:3:4) diff --git a/testsuite/tests/typecheck/should_fail/tcfail013.stderr b/testsuite/tests/typecheck/should_fail/tcfail013.stderr index f3e815bb6e..3803d9ce95 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail013.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail013.stderr @@ -4,4 +4,4 @@ tcfail013.hs:4:3: error: • In the pattern: True In an equation for ‘f’: f True = 2 • Relevant bindings include - f :: [a] -> t (bound at tcfail013.hs:3:1) + f :: [a] -> p (bound at tcfail013.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail014.stderr b/testsuite/tests/typecheck/should_fail/tcfail014.stderr index a186fb1310..f506bff6f8 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr @@ -1,9 +1,9 @@ tcfail014.hs:5:33: error: - • Occurs check: cannot construct the infinite type: t7 ~ t7 -> t8 + • Occurs check: cannot construct the infinite type: t4 ~ t4 -> t5 • In the first argument of ‘z’, namely ‘z’ In the expression: z z In an equation for ‘h’: h z = z z • Relevant bindings include - z :: t7 -> t8 (bound at tcfail014.hs:5:27) - h :: (t7 -> t8) -> t8 (bound at tcfail014.hs:5:25) + z :: t4 -> t5 (bound at tcfail014.hs:5:27) + h :: (t4 -> t5) -> t5 (bound at tcfail014.hs:5:25) diff --git a/testsuite/tests/typecheck/should_fail/tcfail018.stderr b/testsuite/tests/typecheck/should_fail/tcfail018.stderr index 57060a87db..d5594c7c41 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail018.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail018.stderr @@ -1,5 +1,5 @@ tcfail018.hs:5:10: error: - • No instance for (Num [t0]) arising from the literal ‘1’ + • No instance for (Num [a0]) arising from the literal ‘1’ • In the expression: 1 In a pattern binding: (a : []) = 1 diff --git a/testsuite/tests/typecheck/should_fail/tcfail032.stderr b/testsuite/tests/typecheck/should_fail/tcfail032.stderr index 583e6e3ce5..d2912b2b94 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail032.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail032.stderr @@ -1,6 +1,6 @@ tcfail032.hs:14:8: error: - • Couldn't match expected type ‘a1 -> Int’ with actual type ‘t’ + • Couldn't match expected type ‘a1 -> Int’ with actual type ‘p’ because type variable ‘a1’ would escape its scope This (rigid, skolem) type variable is bound by an expression type signature: @@ -9,5 +9,5 @@ tcfail032.hs:14:8: error: • In the expression: (x :: (Eq a) => a -> Int) In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int) • Relevant bindings include - x :: t (bound at tcfail032.hs:14:3) - f :: t -> forall a. Eq a => a -> Int (bound at tcfail032.hs:14:1) + x :: p (bound at tcfail032.hs:14:3) + f :: p -> a -> Int (bound at tcfail032.hs:14:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail099.stderr b/testsuite/tests/typecheck/should_fail/tcfail099.stderr index f3908f36e4..bc30866ec2 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail099.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail099.stderr @@ -1,6 +1,6 @@ tcfail099.hs:9:20: error: - • Couldn't match expected type ‘a’ with actual type ‘t’ + • Couldn't match expected type ‘a’ with actual type ‘p’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: C :: forall a. (a -> Int) -> DS, @@ -10,6 +10,6 @@ tcfail099.hs:9:20: error: In the expression: f arg In an equation for ‘call’: call (C f) arg = f arg • Relevant bindings include - arg :: t (bound at tcfail099.hs:9:12) + arg :: p (bound at tcfail099.hs:9:12) f :: a -> Int (bound at tcfail099.hs:9:9) - call :: DS -> t -> Int (bound at tcfail099.hs:9:1) + call :: DS -> p -> Int (bound at tcfail099.hs:9:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail104.stderr b/testsuite/tests/typecheck/should_fail/tcfail104.stderr index a0a6595231..44d8e4888c 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail104.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail104.stderr @@ -3,15 +3,15 @@ tcfail104.hs:14:12: error: • Couldn't match type ‘forall a. a -> a’ with ‘Char -> Char’ Expected type: (Char -> Char) -> Char -> Char Actual type: (forall a. a -> a) -> Char -> Char - • When checking that: (forall a. a -> a) -> forall a. a -> a - is more polymorphic than: (Char -> Char) -> Char -> Char - In the expression: (\ (x :: forall a. a -> a) -> x) + • In the expression: (\ (x :: forall a. a -> a) -> x) In the expression: if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x) + In the expression: + (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c' tcfail104.hs:22:15: error: - • Couldn't match expected type ‘forall a. a -> a’ - with actual type ‘Char -> Char’ + • Couldn't match expected type ‘Char -> Char’ + with actual type ‘forall a. a -> a’ • When checking that the pattern signature: forall a. a -> a fits the type of its context: Char -> Char In the pattern: x :: forall a. a -> a diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr index f75f77c38a..85217315ca 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr @@ -16,7 +16,7 @@ tcfail140.hs:12:10: error: In the expression: 3 `f` 4 In an equation for ‘rot’: rot xs = 3 `f` 4 • Relevant bindings include - rot :: t1 -> t (bound at tcfail140.hs:12:1) + rot :: p -> t (bound at tcfail140.hs:12:1) tcfail140.hs:14:15: error: • Couldn't match expected type ‘t -> b’ with actual type ‘Int’ @@ -36,6 +36,6 @@ tcfail140.hs:16:8: error: In the expression: (\ Just x -> x) :: Maybe a -> a tcfail140.hs:19:1: error: - • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’ + • Couldn't match expected type ‘Int’ with actual type ‘p0 -> Bool’ • The equation(s) for ‘g’ have two arguments, but its type ‘Int -> Int’ has only one diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr index a231133fd4..30e27b8bb7 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr @@ -3,7 +3,7 @@ tcfail181.hs:17:9: error: • Could not deduce (Monad m0) arising from a use of ‘foo’ from the context: Monad m bound by the inferred type of - wog :: Monad m => t -> Something (m Bool) e + wog :: Monad m => p -> Something (m Bool) e at tcfail181.hs:17:1-30 The type variable ‘m0’ is ambiguous These potential instances exist: diff --git a/testsuite/tests/warnings/should_compile/T12574.stderr b/testsuite/tests/warnings/should_compile/T12574.stderr index ded88331fa..db435541c1 100644 --- a/testsuite/tests/warnings/should_compile/T12574.stderr +++ b/testsuite/tests/warnings/should_compile/T12574.stderr @@ -1,4 +1,4 @@ T12574.hs:3:1: warning: [-Wmissing-local-signatures] Polymorphic local binding with no type signature: - T12574.id :: forall t. t -> t + T12574.id :: forall p. p -> p |