diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-04-29 13:43:09 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-04-29 15:05:44 +0100 |
| commit | a1275a762ec04c1159ae37199b1c8f998a5c5499 (patch) | |
| tree | 6d01de796910a7857c5f91661a40592f67d62090 | |
| parent | d9bb0ee78b2104bd5c71508080d068804086ae84 (diff) | |
| download | haskell-a1275a762ec04c1159ae37199b1c8f998a5c5499.tar.gz | |
Improve improvement in the constraint solver
This regrettably-big patch substantially improves the way in which
"improvement" happens in the constraint solver. It was triggered by
trying to crack Trac #10009, but it turned out to solve #10340 as
well.
The big picture, with several of the trickiest examples, is described
in Note [The improvement story] in TcInteract.
The major change is this:
* After solving we explicitly try "improvement", by
- making the unsolved Wanteds into Deriveds
- allowing Deriveds to rewrite Deriveds
This more aggressive rewriting "unlocks" some extra
guess-free unifications.
* The main loop is in TcInteract.solveSimpleWanteds, but I also ended
up refactoring TcSimplify.simpl_loop, and its surrounding code.
Notably, any insolubles from the Givens are pulled out
and treated separately, rather than staying in the inert set
during the solveSimpleWanteds loop.
There are a lot of follow-on changes
* Do not emit generate Derived improvements from Wanteds.
This saves work in the common case where they aren't needed.
* For improvement we should really do type-class reduction on Derived
constraints in doTopReactDict. That entailed changing the GenInst
constructor a bit; a local and minor change
* Some annoying faffing about with dropping derived constraints;
see dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
and their Notes.
* Some substantial refactoring in TcErrors.reportWanteds.
This work wasn't strictly forced, but I got sucked into it.
All the changes are in TcErrors.
* Use TcS.unifyTyVar consistently, rather than setWantedTyBind,
so that unifications are properly tracked.
* Refactoring around solveWantedsTcM, solveWantedsAndDrop.
They previously guaranteed a zonked result, but it's more
straightforward for clients to zonk.
50 files changed, 1278 insertions, 904 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index b8503188c0..78a53fba39 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -252,26 +252,24 @@ emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls ; continueWith ct } emitSuperclasses _ = panic "emit_superclasses of non-class!" -{- -Note [Adding superclasses] -~~~~~~~~~~~~~~~~~~~~~~~~~~ - +{- Note [Adding superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Since dictionaries are canonicalized only once in their lifetime, the place to add their superclasses is canonicalisation. See Note [Add superclasses only during canonicalisation]. Here is what we do: - Deriveds: Do nothing. - Givens: Add all their superclasses as Givens. + They may be needed to prove Wanteds + + Wanteds: Do nothing. - Wanteds: Add all their superclasses as Derived. - Not as Wanted: we don't need a proof. - Nor as Given: that leads to superclass loops. + Deriveds: Add all their superclasses as Derived. + The sole reason is to expose functional dependencies + in superclasses or equality superclasses. -We also want to ensure minimal constraints to quantify over. For -instance, if our wanted constraint is (Eq a, Ord a) we'd only like to -quantify over Ord a. But we deal with that completely independently -in TcSimplify. See Note [Minimize by SuperClasses] in TcSimplify. + We only do this in the improvement phase, if solving has + not succeeded; see Note [The improvement story] in + TcInteract Examples of how adding superclasses as Derived is useful @@ -292,6 +290,7 @@ Examples of how adding superclasses as Derived is useful [D] F a ~ beta Now we we get [D] beta ~ b, and can solve that. +---------- Historical note ----------- Example of why adding superclass of a Wanted as a Given would be terrible, see Note [Do not add superclasses of solved dictionaries] in TcSMonad, which has this example: @@ -348,21 +347,18 @@ situation can't happen. newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS () -- Returns superclasses, see Note [Adding superclasses] newSCWorkFromFlavored flavor cls xis - | isDerived flavor - = return () -- Deriveds don't yield more superclasses because we will - -- add them transitively in the case of wanteds. + | CtWanted {} <- flavor + = return () | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor - = do { let sc_theta = immSuperClasses cls xis - mk_pr sc_pred i = (sc_pred, EvSuperClass (EvId evar) i) - ; given_evs <- newGivenEvVars loc (zipWith mk_pr sc_theta [0..]) + = do { given_evs <- newGivenEvVars loc (mkEvScSelectors (EvId evar) cls xis) ; emitWorkNC given_evs } | isEmptyVarSet (tyVarsOfTypes xis) = return () -- Wanteds with no variables yield no deriveds. -- See Note [Improvement from Ground Wanteds] - | otherwise -- Wanted case, just add those SC that can lead to improvement. + | otherwise -- Derived case, just add those SC that can lead to improvement. = do { let sc_rec_theta = transSuperClasses cls xis impr_theta = filter isImprovementPred sc_rec_theta loc = ctEvLoc flavor diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 6c631df592..b8aa1bf93f 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -1807,11 +1807,10 @@ simplifyDeriv pred tvs theta ; traceTc "simplifyDeriv" $ vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ] - ; (residual_wanted, _ev_binds1) - <- solveWantedsTcM (mkSimpleWC wanted) - -- Post: residual_wanted are already zonked + ; residual_wanted <- solveWantedsTcM wanted - ; let (good, bad) = partitionBagWith get_good (wc_simple residual_wanted) + ; residual_simple <- zonkSimples (wc_simple residual_wanted) + ; let (good, bad) = partitionBagWith get_good residual_simple -- See Note [Exotic derived instance contexts] get_good :: Ct -> Either PredType Ct get_good ct | validDerivPred skol_set p diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index f32215b315..67aed6498b 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -126,23 +126,25 @@ report_unsolved :: Maybe EvBindsVar -- cec_binds -> HoleChoice -- Expression holes -> HoleChoice -- Type holes -> WantedConstraints -> TcM () --- Important precondition: --- WantedConstraints are fully zonked and unflattened, that is, --- zonkWC has already been applied to these constraints. report_unsolved mb_binds_var defer_errors expr_holes type_holes wanted | isEmptyWC wanted = return () | otherwise - = do { traceTc "reportUnsolved (before unflattening)" (ppr wanted) - ; warn_redundant <- woptM Opt_WarnRedundantConstraints + = do { traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted) + ; wanted <- zonkWC wanted -- Zonk to reveal all information ; env0 <- tcInitTidyEnv - -- If we are deferring we are going to need /all/ evidence around, -- including the evidence produced by unflattening (zonkWC) ; let tidy_env = tidyFreeTyVars env0 free_tvs free_tvs = tyVarsOfWC wanted - err_ctxt = CEC { cec_encl = [] + + ; traceTc "reportUnsolved (after zonking and tidying):" $ + vcat [ pprTvBndrs (varSetElems free_tvs) + , ppr wanted ] + + ; warn_redundant <- woptM Opt_WarnRedundantConstraints + ; let err_ctxt = CEC { cec_encl = [] , cec_tidy = tidy_env , cec_defer_type_errors = defer_errors , cec_expr_holes = expr_holes @@ -151,10 +153,6 @@ report_unsolved mb_binds_var defer_errors expr_holes type_holes wanted , cec_warn_redundant = warn_redundant , cec_binds = mb_binds_var } - ; traceTc "reportUnsolved (after unflattening):" $ - vcat [ pprTvBndrs (varSetElems free_tvs) - , ppr wanted ] - ; reportWanteds err_ctxt wanted } -------------------------------------------- @@ -286,72 +284,76 @@ This only matters in instance declarations.. reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM () reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) - = do { ctxt1 <- reportSimples ctxt (mapBag (tidyCt env) insol_given) - ; ctxt2 <- reportSimples ctxt1 (mapBag (tidyCt env) insol_wanted) + = do { traceTc "reportWanteds" (vcat [ ptext (sLit "Simples =") <+> ppr simples + , ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)]) + ; let tidy_insols = bagToList (mapBag (tidyCt env) insols) + tidy_simples = bagToList (mapBag (tidyCt env) simples) + + -- First deal with things that are utterly wrong + -- Like Int ~ Bool (incl nullary TyCons) + -- or Int ~ t a (AppTy on one side) + -- Do this first so that we know the ctxt for the nested implications + ; (ctxt1, insols1) <- tryReporters ctxt insol_given tidy_insols + ; (ctxt2, insols2) <- tryReporters ctxt1 insol_wanted insols1 -- For the simple wanteds, suppress them if there are any -- insolubles in the tree, to avoid unnecessary clutter ; let ctxt2' = ctxt { cec_suppress = cec_suppress ctxt2 || anyBag insolubleImplic implics } - ; _ <- reportSimples ctxt2' (mapBag (tidyCt env) simples) + ; (_, leftovers) <- tryReporters ctxt2' reporters (insols2 ++ tidy_simples) + ; MASSERT2( null leftovers, ppr leftovers ) + + -- TuplePreds should have been expanded away by the constraint + -- simplifier, so they shouldn't show up at this point -- All the Derived ones have been filtered out of simples -- by the constraint solver. This is ok; we don't want -- to report unsolved Derived goals as errors -- See Note [Do not report derived but soluble errors] - ; mapBagM_ (reportImplic ctxt1) implics } + + ; mapBagM_ (reportImplic ctxt1) implics } -- NB ctxt1: don't suppress inner insolubles if there's only a -- wanted insoluble here; but do suppress inner insolubles -- if there's a *given* insoluble here (= inaccessible code) where env = cec_tidy ctxt - (insol_given, insol_wanted) = partitionBag isGivenCt insols - -reportSimples :: ReportErrCtxt -> Cts -> TcM ReportErrCtxt -reportSimples ctxt simples -- Here 'simples' includes insolble goals - = traceTc "reportSimples" (vcat [ ptext (sLit "Simples =") <+> ppr simples - , ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)]) - >> tryReporters ctxt - [ -- First deal with things that are utterly wrong - -- Like Int ~ Bool (incl nullary TyCons) - -- or Int ~ t a (AppTy on one side) - ("Utterly wrong (given)", utterly_wrong_given, True, mkGroupReporter mkEqErr) - , ("Utterly wrong (other)", utterly_wrong_other, True, mkGroupReporter mkEqErr) - , ("Holes", is_hole, False, mkHoleReporter) - - -- Report equalities of form (a~ty). They are usually - -- skolem-equalities, and they cause confusing knock-on - -- effects in other errors; see test T4093b. - , ("Skolem equalities", skolem_eq, True, mkSkolReporter) - - -- Other equalities; also confusing knock on effects - , ("Equalities", is_equality, True, mkGroupReporter mkEqErr) - - , ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) - , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) - , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) - ] - (bagToList simples) - -- TuplePreds should have been expanded away by the constraint - -- simplifier, so they shouldn't show up at this point - where - utterly_wrong_given, utterly_wrong_other, skolem_eq, is_hole, is_dict, - is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool + insol_given = [ ("insoluble1", is_given &&& utterly_wrong, True, mkGroupReporter mkEqErr) + , ("insoluble2", is_given &&& is_equality, True, mkSkolReporter) ] + insol_wanted = [ ("insoluble3", utterly_wrong, True, mkGroupReporter mkEqErr) + , ("insoluble4", is_equality, True, mkSkolReporter) ] - utterly_wrong_given ct (EqPred _ ty1 ty2) - | isGivenCt ct = isRigid ty1 && isRigid ty2 - utterly_wrong_given _ _ = False + reporters = [ ("Holes", is_hole, False, mkHoleReporter) - utterly_wrong_other _ (EqPred _ ty1 ty2) = isRigid ty1 && isRigid ty2 - utterly_wrong_other _ _ = False + -- Report equalities of form (a~ty). They are usually + -- skolem-equalities, and they cause confusing knock-on + -- effects in other errors; see test T4093b. + , ("Skolem equalities", is_skol_eq, True, mkSkolReporter) - is_hole ct _ = isHoleCt ct + -- Other equalities; also confusing knock on effects + , ("Equalities", is_equality, True, mkGroupReporter mkEqErr) + + , ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) + , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) + , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] + + (&&&) :: (Ct->PredTree->Bool) -> (Ct->PredTree->Bool) -> (Ct->PredTree->Bool) + (&&&) p1 p2 ct pred = p1 ct pred && p2 ct pred + + is_skol_eq, is_hole, is_dict, + is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool + + utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigid ty1 && isRigid ty2 + utterly_wrong _ _ = False - skolem_eq _ (EqPred NomEq ty1 ty2) = isRigidOrSkol ty1 && isRigidOrSkol ty2 - skolem_eq _ _ = False + is_hole ct _ = isHoleCt ct - is_equality _ (EqPred {}) = True - is_equality _ _ = False + is_given ct _ = not (isWantedCt ct) -- The Derived ones are actually all from Givens + is_equality ct pred = not (isDerivedCt ct) && (case pred of + EqPred {} -> True + _ -> False) + is_skol_eq ct (EqPred NomEq ty1 ty2) + = not (isDerivedCt ct) && isRigidOrSkol ty1 && isRigidOrSkol ty2 + is_skol_eq _ _ = False is_dict _ (ClassPred {}) = True is_dict _ _ = False @@ -363,6 +365,10 @@ reportSimples ctxt simples -- Here 'simples' includes insolble goals is_irred _ _ = False +-- isRigidEqPred :: PredTree -> Bool +-- isRigidEqPred (EqPred NomEq ty1 ty2) = isRigid ty1 && isRigid ty2 +-- isRigidEqPred _ = False + --------------- isRigid, isRigidOrSkol :: Type -> Bool isRigid ty @@ -499,32 +505,33 @@ maybeAddDeferredBinding ctxt err ct | otherwise = return () -tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM ReportErrCtxt +tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct]) -- Use the first reporter in the list whose predicate says True tryReporters ctxt reporters cts = do { traceTc "tryReporters {" (ppr cts) - ; ctxt' <- go ctxt reporters cts - ; traceTc "tryReporters }" empty - ; return ctxt' } + ; (ctxt', cts') <- go ctxt reporters cts + ; traceTc "tryReporters }" (ppr cts') + ; return (ctxt', cts') } where go ctxt [] cts - | null cts = return ctxt - | otherwise = pprPanic "tryReporters" (ppr cts) - - go ctxt ((str, pred, suppress_after, reporter) : rs) cts - | null yeses = do { traceTc "tryReporters: no" (text str) - ; go ctxt rs cts } - | otherwise = do { traceTc "tryReporters: yes" (text str <+> ppr yeses) - ; reporter ctxt yeses :: TcM () - ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt } - ; go ctxt' rs nos } - -- Carry on with the rest, because we must make - -- deferred bindings for them if we have - -- -fdefer-type-errors - -- But suppress their error messages - where - (yeses, nos) = partition keep_me cts - keep_me ct = pred ct (classifyPredType (ctPred ct)) + = return (ctxt, cts) + + go ctxt (r : rs) cts + = do { (ctxt', cts') <- tryReporter ctxt r cts + ; go ctxt' rs cts' } + -- Carry on with the rest, because we must make + -- deferred bindings for them if we have -fdefer-type-errors + -- But suppress their error messages + +tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct]) +tryReporter ctxt (str, keep_me, suppress_after, reporter) cts + | null yeses = return (ctxt, cts) + | otherwise = do { traceTc "tryReporter:" (text str <+> ppr yeses) + ; reporter ctxt yeses + ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt } + ; return (ctxt', nos) } + where + (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts -- Add the "arising from..." part to a message about bunch of dicts addArising :: CtOrigin -> SDoc -> SDoc diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index ff7b7ff37e..65d260ba61 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -235,52 +235,6 @@ Solution: always put fmvs on the left, so we get is a bad idea. We want to use other constraints on alpha first. -Note [Derived constraints from wanted CTyEqCans] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Is this type ambiguous: (Foo e ~ Maybe e) => Foo e - (indexed-types/should_fail/T4093a) - - [G] Foo e ~ Maybe e - [W] Foo e ~ Foo ee -- ee is a unification variable - [W] Foo ee ~ Maybe ee) ---- - [G] Foo e ~ fsk - [G] fsk ~ Maybe e - - [W] Foo e ~ fmv1 - [W] Foo ee ~ fmv2 - [W] fmv1 ~ fmv2 - [W] fmv2 ~ Maybe ee - ----> fmv1 := fsk by matching LHSs - [W] Foo ee ~ fmv2 - [W] fsk ~ fmv2 - [W] fmv2 ~ Maybe ee - ----> - [W] Foo ee ~ fmv2 - [W] fmv2 ~ Maybe e - [W] fmv2 ~ Maybe ee - -Now maybe we shuld get [D] e ~ ee, and then we'd solve it entirely. -But if in a smilar situation we got [D] Int ~ Bool we'd be back -to complaining about wanted/wanted interactions. Maybe this arises -also for fundeps? - -Here's another example: - f :: [a] -> [b] -> blah - f (e1 :: F Int) (e2 :: F Int) - - we get - F Int ~ fmv - fmv ~ [alpha] - fmv ~ [beta] - - We want: alpha := beta (which might unlock something else). If we - generated [D] [alpha] ~ [beta] we'd be good here. - -Current story: we don't generate these derived constraints. We could, but -we'd want to make them very weak, so we didn't get the Int~Bool complaint. ************************************************************************ @@ -1570,9 +1524,12 @@ ctFlavourRole = ctEvFlavourRole . cc_ev eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool -- Very important function! -- See Note [eqCanRewrite] -eqCanRewriteFR (Given, NomEq) (_, _) = True -eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True -eqCanRewriteFR _ _ = False +-- See Note [Wanteds do not rewrite Wanteds] +-- See Note [Deriveds do rewrite Deriveds] +eqCanRewriteFR (Given, NomEq) (_, _) = True +eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True +eqCanRewriteFR (Derived, NomEq) (Derived, _) = True +eqCanRewriteFR _ _ = False canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool -- See Note [canRewriteOrSame] @@ -1582,15 +1539,20 @@ canRewriteOrSame ev1 ev2 = ev1 `eqCanRewrite` ev2 || canRewriteOrSameFR :: CtFlavourRole -> CtFlavourRole -> Bool canRewriteOrSameFR fr1 fr2 = fr1 `eqCanRewriteFR` fr2 || fr1 == fr2 -{- -Note [eqCanRewrite] +{- Note [eqCanRewrite] ~~~~~~~~~~~~~~~~~~~ (eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of a can-rewrite relation, see Definition [Can-rewrite relation] -At the moment we don't allow Wanteds to rewrite Wanteds, because that can give -rise to very confusing type error messages. A good example is Trac #8450. +With the solver handling Coercible constraints like equality constraints, +the rewrite conditions must take role into account, never allowing +a representational equality to rewrite a nominal one. + +Note [Wanteds do not rewrite Wanteds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We don't allow Wanteds to rewrite Wanteds, because that can give rise +to very confusing type error messages. A good example is Trac #8450. Here's another f :: a -> Bool f x = ( [x,'c'], [x,True] ) `seq` True @@ -1599,11 +1561,10 @@ Here we get [W] a ~ Bool but we do not want to complain about Bool ~ Char! -Accordingly, we also don't let Deriveds rewrite Deriveds. - -With the solver handling Coercible constraints like equality constraints, -the rewrite conditions must take role into account, never allowing -a representational equality to rewrite a nominal one. +Note [Deriveds do rewrite Deriveds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +However we DO allow Deriveds to rewrite Deriveds, because that's how +improvement works; see Note [The improvement story] in TcInteract. Note [canRewriteOrSame] ~~~~~~~~~~~~~~~~~~~~~~~ @@ -1636,6 +1597,9 @@ unflatten tv_eqs funeqs , ptext (sLit "Tv eqs =") <+> pprCts tv_eqs ] -- Step 1: unflatten the CFunEqCans, except if that causes an occurs check + -- Occurs check: consider [W] alpha ~ [F alpha] + -- ==> (flatten) [W] F alpha ~ fmv, [W] alpha ~ [fmv] + -- ==> (unify) [W] F [fmv] ~ fmv -- See Note [Unflatten using funeqs first] ; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs ; traceTcS "Unflattening 1" $ braces (pprCts funeqs) @@ -1654,7 +1618,10 @@ unflatten tv_eqs funeqs ; let all_flat = tv_eqs `andCts` funeqs ; traceTcS "Unflattening done" $ braces (pprCts all_flat) - ; return all_flat } + -- Step 5: zonk the result + -- Motivation: makes them nice and ready for the next step + -- (see TcInteract.solveSimpleWanteds) + ; zonkSimples all_flat } where ---------------- unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts @@ -1731,7 +1698,7 @@ tryFill dflags tv rhs ev OC_OK rhs'' -- Normal case: fill the tyvar -> do { setEvBindIfWanted ev (EvCoercion (mkTcReflCo (ctEvRole ev) rhs'')) - ; setWantedTyBind tv rhs'' + ; unifyTyVar tv rhs'' ; return True } _ -> -- Occurs check diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 2ccfcb1bb6..c0d3a511f2 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -2,7 +2,8 @@ module TcInteract ( solveSimpleGivens, -- Solves [EvVar],GivenLoc - solveSimpleWanteds -- Solves Cts + solveSimpleWanteds, -- Solves Cts + usefulToFloat ) where #include "HsVersions.h" @@ -14,7 +15,7 @@ import TcCanonical import TcFlatten import VarSet import Type -import Kind (isKind, isConstraintKind ) +import Kind ( isKind, isConstraintKind, isSubKind ) import Unify import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId ) import CoAxiom(sfInteractTop, sfInteractInert) @@ -33,6 +34,7 @@ import Inst( tyVarsOfCt ) import TcEvidence import Outputable +import qualified TcRnMonad as TcM import TcRnTypes import TcErrors import TcSMonad @@ -124,12 +126,15 @@ that prepareInertsForImplications will discard the insolubles, so we must keep track of them separately. -} -solveSimpleGivens :: CtLoc -> [EvVar] -> TcS () +solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts +-- Solves the givens, adding them to the inert set +-- Returns any insoluble givens, taking those ones out of the inert set solveSimpleGivens loc givens | null givens -- Shortcut for common case - = return () + = return emptyCts | otherwise - = go (map mk_given_ct givens) + = do { go (map mk_given_ct givens) + ; takeInertInsolubles } where mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id , ctev_pred = evVarPred ev_id @@ -140,27 +145,290 @@ solveSimpleGivens loc givens } solveSimpleWanteds :: Cts -> TcS WantedConstraints -solveSimpleWanteds = go emptyBag +-- NB: 'simples' may contain /derived/ equalities, floated +-- out from a nested implication. So don't discard deriveds! +solveSimpleWanteds simples + = do { traceTcS "solveSimples {" (ppr simples) + ; (n,wc) <- go 1 (emptyWC { wc_simple = simples }) + ; traceTcS "solveSimples end }" $ + vcat [ ptext (sLit "iterations =") <+> ppr n + , ptext (sLit "residual =") <+> ppr wc ] + ; return wc } where - go insols0 wanteds - = do { solveSimples wanteds - ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts - ; unflattened_eqs <- unflatten tv_eqs fun_eqs - -- See Note [Unflatten after solving the simple wanteds] + go :: Int -> WantedConstraints -> TcS (Int, WantedConstraints) + go n wc + | n > 10 + = do { wrapWarnTcS $ TcM.addWarnTc $ + hang (ptext (sLit "solveSimpleWanteds: possible loop?")) + 2 (pprCts simples) + ; return (n,wc) } - ; zonked <- zonkSimples (others `andCts` unflattened_eqs) - -- Postcondition is that the wl_simples are zonked + | isEmptyBag (wc_simple wc) + = return (n,wc) - ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked - -- See Note [Running plugins on unflattened wanteds] - ; let all_insols = insols0 `unionBags` insols `unionBags` insols' + | otherwise + = do { -- Solve + (unifs1, wc1) <- solve_simple_wanteds wc + + -- Try improvement + -- See Note [The improvement story] + ; (unifs2, wc2) <- try_improvement wc1 + + -- Run plugins + ; (rerun_plugin, wc3) <- runTcPluginsWanted wc2 + -- See Note [Running plugins on unflattened wanteds] + + ; if unifs1 || unifs2 || rerun_plugin + then go (n+1) wc3 -- Loop + else return (n,wc3) } + +solve_simple_wanteds :: WantedConstraints -> TcS (Bool, WantedConstraints) +-- Try solving these constraints +-- Return True iff some unification happpened *during unflattening* +-- because this is a form of improvement +-- See Note [The improvement story] +-- Affects the unification state (of course) but not the inert set +solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 }) + = nestTcS $ + do { solveSimples simples1 + ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts + ; (unifs_happened, unflattened_eqs) <- reportUnifications $ + unflatten tv_eqs fun_eqs + -- See Note [Unflatten after solving the simple wanteds] + ; return ( unifs_happened + , WC { wc_simple = others `andCts` unflattened_eqs + , wc_insol = insols1 `andCts` insols2 + , wc_impl = implics1 `unionBags` implics2 }) } + +try_improvement :: WantedConstraints -> TcS (Bool, WantedConstraints) +-- See Note [The improvement story] +-- Try doing improvement on these simple constraints +-- Return True iff some unification happpened +-- Affects the unification state (of course) but not the inert set +try_improvement wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) + | isEmptyBag simples + = return (False, wc) + | otherwise + = nestTcS $ reportUnifications $ + do { traceTcS "try_improvement {" (ppr wc) + ; solveSimples init_derived + ; (_, tv_eqs, fun_eqs, derived_insols, _) <- getUnsolvedInerts + ; derived_eqs <- unflatten tv_eqs fun_eqs + ; let new_derived = filterBag (usefulToFloat is_new) derived_eqs + wc1 = WC { wc_simple = simples1 `andCts` new_derived + , wc_insol = dropDerivedSimples insols `andCts` derived_insols + -- See Note [Insolubles and improvement] + , wc_impl = implics } + ; traceTcS "try_improvement end }" (ppr wc1) + ; return wc1 } + where + is_new pred = not (any (pred `eqType`) init_eq_preds) + -- Sigh: an equality in init_derived may well show up in derived_eqs, + -- if no progress has been made, and we don't want to duplicate it. + -- But happily these lists are both usually very short. + + -- Drop all derived constraints; we are about to re-generate them! + simples1 = dropDerivedSimples simples + init_derived = mapBag mk_derived simples1 + init_eq_preds = [ pred | ct <- bagToList init_derived + , let pred = ctPred ct + , isEqPred pred ] + + mk_derived :: Ct -> Ct -- Always non-canonical (so that we generate superclasses) + mk_derived ct = mkNonCanonical (CtDerived { ctev_pred = pred, ctev_loc = loc }) + where + pred = ctEvPred ev + loc = ctEvLoc ev + ev = ctEvidence ct + + +usefulToFloat :: (TcPredType -> Bool) -> Ct -> Bool +usefulToFloat is_useful_pred ct -- The constraint is un-flattened and de-cannonicalised + = is_meta_var_eq pred && is_useful_pred pred + where + pred = ctPred ct + + -- Float out alpha ~ ty, or ty ~ alpha + -- which might be unified outside + -- See Note [Do not float kind-incompatible equalities] + is_meta_var_eq pred + | EqPred NomEq ty1 ty2 <- classifyPredType pred + , let k1 = typeKind ty1 + k2 = typeKind ty2 + = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of + (Just tv1, _) | isMetaTyVar tv1 + , k2 `isSubKind` k1 + -> True + (_, Just tv2) | isMetaTyVar tv2 + , k1 `isSubKind` k2 + -> True + _ -> False + | otherwise + = False - ; if rerun then do { updInertTcS prepareInertsForImplications - ; go all_insols wanteds' } - else return (WC { wc_simple = wanteds' - , wc_insol = all_insols - , wc_impl = implics }) } +{- Note [The improvement story] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The goal of "improvement" is to use functional depenedencies, +type-function injectivity, etc, to derive some extra equalities that +could let us unify one or more meta-variables, and hence make progress. +Solving a bunch of simple constraints is done in a loop, +(the 'go' loop of 'solveSimpleWanteds'): + 1. Try to solve them; some improvement happens here + 2. Try improvement on any unsolved residual constraints + 3. If step 2 led to any unifications, go back to step 1 + +We actually perform step 2 improvement as follows: + * Make the residual Wanteds into Deriveds + * Solve them, aggressively rewriting Derived with Derived + +Some notes about this + * As well as allowing unification, the aggressive rewriting may also + expose an equality on an /untouchable/ unification variable. We + want to keep this derived equality so that it can float out and + unify there. Hence 'usefulToFloat'. + + * Non-obviously, improvement can also take place during the unflattening + that takes place in step (1). See Example 1 below. + + * During Step 1 we do improvement only for Givens, not for Wanteds; + See Note [When improvement happens during solving] + +----------- Example 1 (Trac #10340) + get :: MonadState s m => m s + instance MonadState s (State s) where ... + + foo :: State Any Any + foo = get + + For 'foo' we instantiate 'get' at types mm ss + [W] MonadState ss mm, [W] mm ss ~ State Any Any + Flatten, and decompose + [W] MnadState ss mm, [W] Any ~ fmv, [W] mm ~ State fmv, [W] fmv ~ ss + NB: orientation of fmv ~ ss; see TcFlatten + Note [Orient equalities with flatten-meta-vars on the left] + Unify mm := State fmv: + [W] MonadState ss (State fmv), [W] Any ~ fmv, [W] fmv ~ ss + Alas the insatnce does not match!! So now we are stuck. + + Unflatten: with fmv := Any, and ss := Any + [W] MonadState Any (State Any) + + Note that the unification of 'ss' represents progress!! We must loop! + +----------- Example 2 (indexed-types/should_fail/T4093a) + Ambiguity check for f: (Foo e ~ Maybe e) => Foo e + + We get [G] Foo e ~ Maybe e + [W] Foo e ~ Foo ee -- ee is a unification variable + [W] Foo ee ~ Maybe ee + + Flatten: [G] Foo e ~ fsk + [G] fsk ~ Maybe e -- (A) + + [W] Foo ee ~ fmv + [W] fmv ~ fsk -- (B) From Foo e ~ Foo ee + [W] fmv ~ Maybe ee + + --> rewrite (B) with (A) + [W] Foo ee ~ fmv + [W] fmv ~ Maybe e + [W] fmv ~ Maybe ee + + But now we are stuck, since we don't rewrite Wanteds with Wanteds + Unflatten: + [W] Foo ee ~ Maybe e + [W] Foo ee ~ Maybe ee + + Improvement; start by flattening again + [D] Foo ee ~ fmv + [D] fmv ~ Maybe e -- (A) + [D] fmv ~ Maybe ee -- (B) + + Now we /can/ rewrite (A) with (B), by aggressive rewriting of Deriveds + and that soon yields ee := e, and all is well + +----------- Example 3 (typecheck/should_compile/Improvement.hs) + type instance F Int = Bool + instance (b~Int) => C Bool b + + [W] w1 : C (F alpha) alpha, [W] w2 : F alpha ~ Bool + + If we rewrote wanteds with wanteds, we could rewrite w1 to + C Bool alpha, use the instance to get alpha ~ Int, and solve + the whole thing. + + In improvement (step 2), we make both constraints Derived, + rewrite one with the other, and do type-class reduction on + the Derived constraint + +----------- Example 4 (Trac #10009, a nasty example): + + f :: (UnF (F b) ~ b) => F b -> () + + g :: forall a. (UnF (F a) ~ a) => a -> () + g _ = f (undefined :: F a) + + For g we get [G] UnF (F a) ~ a + [W] UnF (F beta) ~ beta + [W] F a ~ F beta + Flatten: + [G] g1: F a ~ fsk1 fsk1 := F a + [G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1 + [G] g3: fsk2 ~ a + + [W] w1: F beta ~ fmv1 + [W] w2: UnF fmv1 ~ fmv2 + [W] w3: fmv2 ~ beta + [W] w5: fsk1 ~ fmv1 -- From F a ~ F beta + -- using flat-cache + + Solving (step 1) makes not progress. So unflatten again + [W] w3: UnF (F beta) ~ beta + [W] w5: fsk1 ~ F beta + + Try improvement: + [D] F beta ~ fmv1 + [D] UnF fmv1 ~ fmv2 -- (A) + [D] fmv2 ~ beta + [D] fmv1 ~ fsk1 -- (B) From F a ~ F beta + -- NB: put fmv on left + + --> rewrite (A) with (B), and metch with g2 + [D] F beta ~ fmv1 + [D] fmv2 ~ fsk2 -- (C) + [D] fmv2 ~ beta -- (D) + [D] fmv1 ~ fsk1 + + --> rewrite (D) with (C) and re-orient + [D] F beta ~ fmv1 + [D] fmv2 ~ fsk2 + [D] beta ~ fsk2 -- (E) + [D] fmv1 ~ fsk1 + + -- Now we can unify beta! Halelujah! + + +Note [Insolubles and improvement] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We drop all the derived wanted insolubles before improvement, because +they will all be regenerated by the improvement step. + +We want to keep all the derived insolubles, because they are looked +at by simplifyInfer, to decide whether to generalise. Example: + [W] a ~ Int, [W] a ~ Bool +During improvement we get [D] Int ~ Bool, and indeed the constraints +are insoluble, and we want simplifyInfer to see that, even though we +don't ultimately want to generate an (inexplicable) error message from +it. + +Note [Do not float kind-incompatible equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality. +If we float the equality outwards, we'll get *another* Derived +insoluble equality one level out, so the same error will be reported +twice. So we refrain from floating such equalities +-} -- The main solver loop implements Note [Basic Simplifier Plan] --------------------------------------------------------------- @@ -192,35 +460,47 @@ solveSimples cts -- return new work produced so that 'solveSimpleGivens' can feed it back -- into the main solver. runTcPluginsGiven :: TcS [Ct] -runTcPluginsGiven = do - (givens,_,_) <- fmap splitInertCans getInertCans - if null givens - then return [] - else do - p <- runTcPlugins (givens,[],[]) - let (solved_givens, _, _) = pluginSolvedCts p - updInertCans (removeInertCts solved_givens) - mapM_ emitInsoluble (pluginBadCts p) - return (pluginNewCts p) +runTcPluginsGiven + = do { plugins <- getTcPlugins + ; if null plugins then return [] else + do { givens <- getInertGivens + ; if null givens then return [] else + do { p <- runTcPlugins plugins (givens,[],[]) + ; let (solved_givens, _, _) = pluginSolvedCts p + ; updInertCans (removeInertCts solved_givens) + ; mapM_ emitInsoluble (pluginBadCts p) + ; return (pluginNewCts p) } } } -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on -- them and produce an updated bag of wanteds (possibly with some new -- work) and a bag of insolubles. The boolean indicates whether -- 'solveSimpleWanteds' should feed the updated wanteds back into the -- main solver. -runTcPluginsWanted :: Cts -> TcS (Cts, Cts, Bool) -runTcPluginsWanted zonked_wanteds - | isEmptyBag zonked_wanteds = return (zonked_wanteds, emptyBag, False) - | otherwise = do - (given,derived,_) <- fmap splitInertCans getInertCans - p <- runTcPlugins (given, derived, bagToList zonked_wanteds) - let (solved_givens, solved_deriveds, solved_wanteds) = pluginSolvedCts p - (_, _, wanteds) = pluginInputCts p - updInertCans (removeInertCts $ solved_givens ++ solved_deriveds) - mapM_ setEv solved_wanteds - return ( listToBag $ pluginNewCts p ++ wanteds - , listToBag $ pluginBadCts p - , notNull (pluginNewCts p) ) +runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints) +runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 }) + | isEmptyBag simples1 + = return (False, wc) + | otherwise + = do { plugins <- getTcPlugins + ; if null plugins then return (False, wc) else + + do { given <- getInertGivens + ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs + ; let (wanted, derived) = partition isWantedCt (bagToList simples1) + ; p <- runTcPlugins plugins (given, derived, wanted) + ; let (_, _, solved_wanted) = pluginSolvedCts p + (_, unsolved_derived, unsolved_wanted) = pluginInputCts p + new_wanted = pluginNewCts p + +-- SLPJ: I'm deeply suspicious of this +-- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds) + + ; mapM_ setEv solved_wanted + ; return ( notNull (pluginNewCts p) + , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted + `andCts` listToBag unsolved_derived + , wc_insol = listToBag (pluginBadCts p) `andCts` insols1 + , wc_impl = implics1 } ) } } where setEv :: (EvTerm,Ct) -> TcS () setEv (ev,ct) = case ctEvidence ct of @@ -247,6 +527,9 @@ data TcPluginProgress = TcPluginProgress -- ^ New constraints emitted by plugins } +getTcPlugins :: TcS [TcPluginSolver] +getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) } + -- | Starting from a triple of (given, derived, wanted) constraints, -- invoke each of the typechecker plugins in turn and return -- @@ -260,10 +543,9 @@ data TcPluginProgress = TcPluginProgress -- re-invoked and they will see it later). There is no check that new -- work differs from the original constraints supplied to the plugin: -- the plugin itself should perform this check if necessary. -runTcPlugins :: SplitCts -> TcS TcPluginProgress -runTcPlugins all_cts = do - gblEnv <- getGblEnv - foldM do_plugin initialProgress (tcg_tc_plugins gblEnv) +runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress +runTcPlugins plugins all_cts + = foldM do_plugin initialProgress plugins where do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress do_plugin p solver = do @@ -643,13 +925,17 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = interactGivenIP inerts workItem | otherwise - = do { mapBagM_ (addFunDepWork workItem) - (findDictsByClass (inert_dicts inerts) cls) - -- Create derived fds and keep on going. + = do { -- Try improvement via functional dependencies; + -- but only for Givens and Deriveds + -- See Note [When improvement happens during solving] + unless (isWanted ev_w) $ + mapBagM_ (addFunDepWork workItem) + (findDictsByClass (inert_dicts inerts) cls) -- No need to check flavour; fundeps work between -- any pair of constraints, regardless of flavour - -- Importantly we don't throw workitem back in the - -- worklist bebcause this can cause loops (see #5236) + -- Importantly we don't throw workitem back in the + -- worklist because this can cause loops (see #5236) + ; continueWith workItem } interactDict _ wi = pprPanic "interactDict" (ppr wi) @@ -683,7 +969,7 @@ addFunDepWork work_ct inert_ct -- NB: We do create FDs for given to report insoluble equations that arise -- from pairs of Givens, and also because of floating when we approximate -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs - -- Also see Note [When improvement happens] + -- Also see Note [When improvement happens during solving] where work_pred = ctPred work_ct inert_pred = ctPred inert_ct @@ -762,7 +1048,8 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc , text "inertItem=" <+> ppr ev_i ] ; reactFunEq ev_i fsk_i ev fsk ; stopWith ev "Inert rewrites work item" } - else -- Rewrite intert using work-item + else -- Rewrite inert using work-item + ASSERT2( ev `canRewriteOrSame` ev_i, ppr ev $$ ppr ev_i ) do { traceTcS "reactFunEq (rewrite inert item):" $ vcat [ text "workItem =" <+> ppr workItem , text "inertItem=" <+> ppr ev_i ] @@ -772,7 +1059,9 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc ; reactFunEq ev fsk ev_i fsk_i ; stopWith ev "Work item rewrites inert" } - | Just ops <- isBuiltInSynFamTyCon_maybe tc + | not (isWanted ev) -- Try improvement only for Given/Derived + -- See Note [When improvement happens during solving] + , Just ops <- isBuiltInSynFamTyCon_maybe tc = do { let matching_funeqs = findFunEqsByTyCon funeqs tc ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk) do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev }) @@ -812,11 +1101,10 @@ reactFunEq from_this fsk1 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co) ; emitWorkNC [new_ev] } -reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2 - = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1) - -reactFunEq _ _ solve_this@(CtDerived {}) _ - = pprPanic "reactFunEq" (ppr solve_this) +reactFunEq from_this fuv1 ev fuv2 + = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2) + ; dischargeFmv ev fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1) + ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2) } {- Note [Cache-caused loops] @@ -1019,7 +1307,7 @@ solveByUnification wd tv xi -- with simple kinds like *, not OpenKind or ArgKind -- cf TcUnify.uUnboundKVar - ; setWantedTyBind tv xi' + ; unifyTyVar tv xi' ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) } @@ -1267,54 +1555,63 @@ doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct) -- Try to use type-class instance declarations to simplify the constraint doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls , cc_tyargs = xis }) - | not (isWanted fl) -- Never use instances for Given or Derived constraints - = try_fundeps_and_return + | isGiven fl -- Never use instances for Given constraints + = do { try_fundep_improvement + ; continueWith work_item } | Just ev <- lookupSolvedDict inerts cls xis -- Cached - = do { setWantedEvBind dict_id (ctEvTerm ev); + = do { setEvBindIfWanted fl (ctEvTerm ev); ; stopWith fl "Dict/Top (cached)" } - | otherwise -- Not cached + | isDerived fl -- Use type-class instances for Deriveds, in the hope + -- of generating some improvements + -- C.f. Example 3 of Note [The improvement story] + -- It's easy because no evidence is involved = do { lkup_inst_res <- matchClassInst inerts cls xis dict_loc ; case lkup_inst_res of - GenInst wtvs ev_term -> do { addSolvedDict fl cls xis - ; solve_from_instance wtvs ev_term } - NoInstance -> try_fundeps_and_return } + GenInst preds _ -> do { mapM_ (emitNewDerived dict_loc) preds + ; stopWith fl "Dict/Top (solved)" } + + NoInstance -> do { -- If there is no instance, try improvement + try_fundep_improvement + ; continueWith work_item } } + + | otherwise -- Wanted, but not cached + = do { lkup_inst_res <- matchClassInst inerts cls xis dict_loc + ; case lkup_inst_res of + NoInstance -> continueWith work_item + GenInst theta mk_ev -> do { addSolvedDict fl cls xis + ; solve_from_instance theta mk_ev } } where - dict_id = ASSERT( isWanted fl ) ctEvId fl - dict_pred = mkClassPred cls xis - dict_loc = ctEvLoc fl + dict_pred = mkClassPred cls xis + dict_loc = ctEvLoc fl dict_origin = ctLocOrigin dict_loc - deeper_loc = bumpCtLocDepth dict_loc + deeper_loc = bumpCtLocDepth dict_loc - solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct) + solve_from_instance :: [TcPredType] -> ([EvId] -> EvTerm) -> TcS (StopOrContinue Ct) -- Precondition: evidence term matches the predicate workItem - solve_from_instance evs ev_term - | null evs - = do { traceTcS "doTopReact/found nullary instance for" $ - ppr dict_id - ; setWantedEvBind dict_id ev_term + solve_from_instance theta mk_ev + | null theta + = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl + ; setWantedEvBind (ctEvId fl) (mk_ev []) ; stopWith fl "Dict/Top (solved, no new work)" } | otherwise = do { checkReductionDepth deeper_loc dict_pred - ; traceTcS "doTopReact/found non-nullary instance for" $ - ppr dict_id - ; setWantedEvBind dict_id ev_term - ; let mk_new_wanted ev - = mkNonCanonical (ev {ctev_loc = deeper_loc }) - ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs)) + ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl + ; evc_vars <- mapM (newWantedEvVar deeper_loc) theta + ; setWantedEvBind (ctEvId fl) (mk_ev (map (ctEvId . fst) evc_vars)) + ; emitWorkNC (freshGoals evc_vars) ; stopWith fl "Dict/Top (solved, more work)" } -- We didn't solve it; so try functional dependencies with -- the instance environment, and return - -- NB: even if there *are* some functional dependencies against the - -- instance environment, there might be a unique match, and if - -- so we make sure we get on and solve it first. See Note [Weird fundeps] - try_fundeps_and_return - = do { instEnvs <- getInstEnvs - ; emitFunDepDeriveds $ - improveFromInstEnv instEnvs mk_ct_loc dict_pred - ; continueWith work_item } + -- We just land here for Given and Derived; + -- See Note [When improvement happens during solving] + -- See also Note [Weird fundeps] + try_fundep_improvement + = do { instEnvs <- getInstEnvs + ; emitFunDepDeriveds $ + improveFromInstEnv instEnvs mk_ct_loc dict_pred } mk_ct_loc :: PredType -- From instance decl -> SrcSpan -- also from instance deol @@ -1332,11 +1629,11 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc , cc_tyargs = args , cc_fsk = fsk }) = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families -- have reached this far - ASSERT( not (isDerived old_ev) ) -- CFunEqCan is never Derived -- Look up in top-level instances, or built-in axiom do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS] ; case match_res of { - Nothing -> do { try_improvement; continueWith work_item } ; + Nothing -> do { try_improvement + ; continueWith work_item } ; Just (ax_co, rhs_ty) -- Found a top-level instance @@ -1356,7 +1653,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc ; stopWith old_ev "Fun/Top (given)" } | not (fsk `elemVarSet` tyVarsOfType rhs_ty) - -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty + -> do { dischargeFmv old_ev fsk ax_co rhs_ty ; traceTcS "doTopReactFunEq" $ vcat [ text "old_ev:" <+> ppr old_ev , nest 2 (text ":=") <+> ppr ax_co ] @@ -1373,7 +1670,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc -- new_ev :: alpha ~ rhs_ty -- ufsk := alpha -- final_co :: fam_tc args ~ alpha - ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty + ; dischargeFmv old_ev fsk final_co alpha_ty ; traceTcS "doTopReactFunEq (occurs)" $ vcat [ text "old_ev:" <+> ppr old_ev , nest 2 (text ":=") <+> ppr final_co @@ -1384,7 +1681,9 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc deeper_loc = bumpCtLocDepth loc try_improvement - | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc + | not (isWanted old_ev) -- Try improvement only for Given/Derived constraints + -- See Note [When improvement happens during solving] + , Just ops <- isBuiltInSynFamTyCon_maybe fam_tc = do { inert_eqs <- getInertEqs ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk) ; mapM_ (unifyDerived loc Nominal) eqns } @@ -1438,19 +1737,22 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args loc = ctEvLoc old_ev deeper_loc = bumpCtLocDepth loc -dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS () +dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS () -- (dischargeFmv x fmv co ty) --- [W] x :: F tys ~ fuv --- co :: F tys ~ ty --- Precondition: fuv is not filled, and fuv `notElem` ty +-- [W] ev :: F tys ~ fmv +-- co :: F tys ~ xi +-- Precondition: fmv is not filled, and fuv `notElem` xi -- --- Then set fuv := ty, --- set x := co +-- Then set fmv := xi, +-- set ev := co -- kick out any inert things that are now rewritable -dischargeFmv evar fmv co xi - = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi ) - do { setWantedTyBind fmv xi - ; setWantedEvBind evar (EvCoercion co) +dischargeFmv ev fmv co xi + = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi ) + do { case ev of + CtWanted { ctev_evar = evar } -> setWantedEvBind evar (EvCoercion co) + CtDerived {} -> return () -- Happens during improvement + CtGiven {} -> pprPanic "dischargeFmv" (ppr ev) + ; unifyTyVar fmv xi ; n_kicked <- kickOutRewritable Given NomEq fmv ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } @@ -1580,16 +1882,29 @@ Then it is solvable, but its very hard to detect this on the spot. It's exactly the same with implicit parameters, except that the "aggressive" approach would be much easier to implement. -Note [When improvement happens] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We fire an improvement rule when +Note [When improvement happens during solving] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Improvement for functional dependencies or type-function injectivity +means emitting a Derived equality constraint by iteracting the work +item with an inert item, or with the top-level instances. e.g. + + class C a b | a -> b + [W] C a b, [W] C a c ==> [D] b ~ c - * Two constraints match (modulo the fundep) - e.g. C t1 t2, C t1 t3 where C a b | a->b - The two match because the first arg is identical +We fire the fundep improvement if the "work item" is Given or Derived, +but not Wanted. Reason: -Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a -superclass of a Wanted goal) or if both are Given. + * Given: we want to spot Given/Given inconsistencies because that means + unreachable code. See typecheck/should_fail/FDsFromGivens + + * Derived: during the improvment phase (i.e. when handling Derived + constraints) we also do improvement for functional dependencies. e.g. + And similarly wrt top-level instances. + + * Wanted: spotting fundep improvements is somewhat inefficient, and + and if we can solve without improvement so much the better. + So we don't bother to do this when solving Wanteds, instead + leaving it for the try_improvement loop Example (tcfail138) class L a b | a -> b @@ -1600,15 +1915,15 @@ Example (tcfail138) instance L (Maybe a) a When solving the superclasses of the (C (Maybe a) a) instance, we get - Given: C a b ... and hance by superclasses, (G a, L a b) - Wanted: G (Maybe a) + [G] C a b, and hance by superclasses, [G] G a, [G] L a b + [W] G (Maybe a) Use the instance decl to get - Wanted: C a b' -The (C a b') is inert, so we generate its Derived superclasses (L a b'), -and now we need improvement between that derived superclass an the Given (L a b) + [W] C a beta + +During improvement (see Note [The improvement story]) we generate the superclasses +of (C a beta): [D] L a beta. Now using fundeps, combine with [G] L a b to get +[D] beta ~ b, which is what we want. -Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to -emit Derived FDs for givens as well. Note [Weird fundeps] ~~~~~~~~~~~~~~~~~~~~ @@ -1622,10 +1937,12 @@ Consider class Het a b | a -> b where The two instances don't actually conflict on their fundeps, although it's pretty strange. So they are both accepted. Now try [W] GHet (K Int) (K Bool) -This triggers fudeps from both instance decls; but it also -matches a *unique* instance decl, and we should go ahead and -pick that one right now. Otherwise, if we don't, it ends up -unsolved in the inert set and is reported as an error. +This triggers fudeps from both instance decls; + [D] K Bool ~ K [a] + [D] K Bool ~ K beta +And there's a risk of complaining about Bool ~ [a]. But in fact +the Wanted matches the second instance, so we never get as far +as the fundeps. Trac #7875 is a case in point. @@ -1646,11 +1963,11 @@ Hence a work-item Given overrides an inert-item Given. data LookupInstResult = NoInstance - | GenInst [CtEvidence] EvTerm + | GenInst [TcPredType] ([EvId] -> EvTerm) instance Outputable LookupInstResult where ppr NoInstance = text "NoInstance" - ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t + ppr (GenInst ev _) = text "GenInst" <+> ppr ev matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult @@ -1684,14 +2001,15 @@ matchClassInst _ clas [ ty ] _ $ idType meth -- forall n. KnownNat n => SNat n , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] -- SNat n ~ Integer - = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))) + , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)) + = return (GenInst [] $ (\_ -> ev_tm)) | otherwise = panicTcS (text "Unexpected evidence for" <+> ppr (className clas) $$ vcat (map (ppr . idType) (classMethods clas))) -matchClassInst _ clas [k,t] loc - | className clas == typeableClassName = matchTypeableClass clas k t loc +matchClassInst _ clas [k,t] _ + | className clas == typeableClassName = matchTypeableClass clas k t matchClassInst inerts clas tys loc = do { dflags <- getDynFlags @@ -1737,11 +2055,7 @@ matchClassInst inerts clas tys loc match_one dfun_id mb_inst_tys = do { checkWellStagedDFun pred dfun_id loc ; (tys, theta) <- instDFunType dfun_id mb_inst_tys - ; evc_vars <- mapM (newWantedEvVar loc) theta - ; let new_ev_vars = freshGoals evc_vars - -- new_ev_vars are only the real new variables that can be emitted - dfun_app = EvDFunApp dfun_id tys (map (ctEvId . fst) evc_vars) - ; return $ GenInst new_ev_vars dfun_app } + ; return $ GenInst theta (EvDFunApp dfun_id tys) } unifiable_givens :: Cts unifiable_givens = filterBag matchable $ @@ -1845,8 +2159,8 @@ isCallStackIP _ _ _ -- | Assumes that we've checked that this is the 'Typeable' class, -- and it was applied to the correct argument. -matchTypeableClass :: Class -> Kind -> Type -> CtLoc -> TcS LookupInstResult -matchTypeableClass clas _k t loc +matchTypeableClass :: Class -> Kind -> Type -> TcS LookupInstResult +matchTypeableClass clas _k t -- See Note [No Typeable for qualified types] | isForAllTy t = return NoInstance @@ -1877,14 +2191,11 @@ matchTypeableClass clas _k t loc Typeable f -} doTyApp f tk - | isKind tk = return NoInstance -- We can't solve until we know the ctr. - | otherwise = - do ct1 <- subGoal f - ct2 <- subGoal tk - let realSubs = [ c | (c,Fresh) <- [ct1,ct2] ] - return $ GenInst realSubs - $ EvTypeable $ EvTypeableTyApp (getEv ct1,f) (getEv ct2,tk) - + | isKind tk + = return NoInstance -- We can't solve until we know the ctr. + | otherwise + = return $ GenInst [mk_typeable_pred f, mk_typeable_pred tk] + (\[t1,t2] -> EvTypeable $ EvTypeableTyApp (EvId t1,f) (EvId t2,tk)) -- Representation for concrete kinds. We just use the kind itself, -- but first check to make sure that it is "simple" (i.e., made entirely @@ -1893,13 +2204,10 @@ matchTypeableClass clas _k t loc mapM_ kindRep ks return ki - getEv (ct,_fresh) = ctEvTerm ct - -- Emit a `Typeable` constraint for the given type. - subGoal ty = do let goal = mkClassPred clas [ typeKind ty, ty ] - newWantedEvVar loc goal + mk_typeable_pred ty = mkClassPred clas [ typeKind ty, ty ] - mkSimpEv ev = return (GenInst [] (EvTypeable ev)) + mkSimpEv ev = return (GenInst [] (\_ -> EvTypeable ev)) {- Note [No Typeable for polytype or for constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 0d42334b87..18b5a9639d 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -62,7 +62,8 @@ module TcRnTypes( WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols, - dropDerivedWC, insolubleImplic, trulyInsoluble, + dropDerivedWC, dropDerivedSimples, dropDerivedInsols, + insolubleImplic, trulyInsoluble, Implication(..), ImplicStatus(..), isInsolubleStatus, SubGoalDepth, initialSubGoalDepth, @@ -1275,34 +1276,59 @@ ctEqRel = ctEvEqRel . ctEvidence dropDerivedWC :: WantedConstraints -> WantedConstraints -- See Note [Dropping derived constraints] -dropDerivedWC wc@(WC { wc_simple = simples }) - = wc { wc_simple = filterBag isWantedCt simples } +dropDerivedWC wc@(WC { wc_simple = simples, wc_insol = insols }) + = wc { wc_simple = dropDerivedSimples simples + , wc_insol = dropDerivedInsols insols } -- The wc_impl implications are already (recursively) filtered -{- -Note [Dropping derived constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +dropDerivedSimples :: Cts -> Cts +dropDerivedSimples simples = filterBag isWantedCt simples + -- simples are all Wanted or Derived + +dropDerivedInsols :: Cts -> Cts +-- See Note [Dropping derived constraints] +dropDerivedInsols insols = filterBag keep insols + where -- insols can include Given + keep ct + | isDerivedCt ct = keep_orig (ctLocOrigin (ctLoc ct)) + | otherwise = True + + keep_orig :: CtOrigin -> Bool + keep_orig (KindEqOrigin {}) = True + keep_orig (GivenOrigin {}) = True + keep_orig (FunDepOrigin1 {}) = True + keep_orig (FunDepOrigin2 {}) = True +-- keep_orig (FunDepOrigin1 _ loc _ _) = keep_orig (ctLocOrigin loc) +-- keep_orig (FunDepOrigin2 _ orig _ _) = keep_orig orig + keep_orig _ = False + + +{- Note [Dropping derived constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In general we discard derived constraints at the end of constraint solving; see dropDerivedWC. For example - * If we have an unsolved (Ord a), we don't want to complain about - an unsolved (Eq a) as well. -But we keep Derived *insoluble* constraints because they indicate a solid, -comprehensible error. Particularly: + * If we have an unsolved [W] (Ord a), we don't want to complain about + an unsolved [D] (Eq a) as well. + + * If we have [W] a ~ Int, [W] a ~ Bool, improvement will generate + [D] Int ~ Bool, and we don't want to report that becuase it's incomprehensible. + That is why we don't rewrite wanteds with wanteds! - * Insolubles Givens indicate unreachable code +But (tiresomely) we do keep *some* Derived insolubles: * Insoluble kind equalities (e.g. [D] * ~ (* -> *)) may arise from - a type equality a ~ Int#, say + a type equality a ~ Int#, say. In future they'll be Wanted, not Derived, + but at the moment they are Derived. - * Insoluble derived wanted equalities (e.g. [D] Int ~ Bool) may - arise from functional dependency interactions. We are careful - to keep a good CtOrigin on such constraints (FunDepOrigin1, FunDepOrigin2) - so that we can produce a good error message (Trac #9612) + * Insoluble derived equalities (e.g. [D] Int ~ Bool) may arise from + functional dependency interactions, either between Givens or + Wanteds. It seems sensible to retain these: + - For Givens they reflect unreachable code + - For Wanteds it is arguably better to get a fundep error than + a no-instance error (Trac #9612) -Since we leave these Derived constraints in the residual WantedConstraints, -we must filter them out when we re-process the WantedConstraint, -in TcSimplify.solve_wanteds. +To distinguish these cases we use the CtOrigin. ************************************************************************ @@ -1450,6 +1476,7 @@ unionsWC = foldr andWC emptyWC addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints addSimples wc cts = wc { wc_simple = wc_simple wc `unionBags` cts } + -- Consider: Put the new constraints at the front, so they get solved first addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic } @@ -1471,10 +1498,16 @@ insolubleWC (WC { wc_impl = implics, wc_insol = insols }) || anyBag insolubleImplic implics trulyInsoluble :: Ct -> Bool --- The constraint is in the wc_insol set, but we do not --- treat type-holes, arising from PartialTypeSignatures, --- as "truly insoluble". Yuk. -trulyInsoluble insol = not (isTypeHoleCt insol) +-- The constraint is in the wc_insol set, +-- but we do not treat as truly isoluble +-- a) type-holes, arising from PartialTypeSignatures, +-- b) superclass constraints, arising from the emitInsoluble +-- in TcInstDcls.tcSuperClasses. In fact only equalities +-- are truly-insoluble. +-- Yuk! +trulyInsoluble insol + = isEqPred (ctPred insol) + && not (isTypeHoleCt insol) instance Outputable WantedConstraints where ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n}) @@ -2026,7 +2059,7 @@ data CtOrigin | OccurrenceOf Name -- Occurrence of an overloaded identifier | AppOrigin -- An application of some kind - | SpecPragOrigin UserTypeCtxt -- Specialisation pragma for + | SpecPragOrigin UserTypeCtxt -- Specialisation pragma for -- function or instance | TypeEqOrigin { uo_actual :: TcType diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index be28deb2ca..c0103c9289 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -25,7 +25,7 @@ module TcSMonad ( Freshness(..), freshGoals, isFresh, newTcEvBinds, newWantedEvVar, newWantedEvVarNC, - setWantedTyBind, reportUnifications, + unifyTyVar, reportUnifications, setEvBind, setWantedEvBind, setEvBindIfWanted, newEvVar, newGivenEvVar, newGivenEvVars, newDerived, emitNewDerived, checkReductionDepth, @@ -37,10 +37,10 @@ module TcSMonad ( -- Inerts InertSet(..), InertCans(..), updInertTcS, updInertCans, updInertDicts, updInertIrreds, - getNoGivenEqs, setInertCans, getInertEqs, getInertCans, - emptyInert, getTcSInerts, setTcSInerts, + getNoGivenEqs, setInertCans, getInertEqs, getInertCans, getInertGivens, + emptyInert, getTcSInerts, setTcSInerts, takeInertInsolubles, getUnsolvedInerts, checkAllSolved, - splitInertCans, removeInertCts, + removeInertCts, prepareInertsForImplications, addInertCan, insertInertItemTcS, insertFunEq, emitInsoluble, emitWorkNC, emitWorkCt, @@ -70,7 +70,7 @@ module TcSMonad ( TcLevel, isTouchableMetaTyVarTcS, isFilledMetaTyVar_maybe, isFilledMetaTyVar, - zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples, + zonkTyVarsAndFV, zonkTcType, zonkTcTyVar, zonkSimples, zonkWC, -- References newTcRef, readTcRef, updTcRef, @@ -132,7 +132,7 @@ import Control.Arrow ( first ) import Control.Monad( ap, when, unless, MonadPlus(..) ) import MonadUtils import Data.IORef -import Data.List ( partition, foldl' ) +import Data.List ( foldl' ) #ifdef DEBUG import Digraph @@ -613,6 +613,16 @@ getInertCans = do { inerts <- getTcSInerts; return (inert_cans inerts) } setInertCans :: InertCans -> TcS () setInertCans ics = updInertTcS $ \ inerts -> inerts { inert_cans = ics } +takeInertInsolubles :: TcS Cts +-- Take the insoluble constraints out of the inert set +takeInertInsolubles + = do { is_var <- getTcSInertsRef + ; wrapTcS (do { inerts <- TcM.readTcRef is_var + ; let cans = inert_cans inerts + cans' = cans { inert_insols = emptyBag } + ; TcM.writeTcRef is_var (inerts { inert_cans = cans' }) + ; return (inert_insols cans) }) } + updInertCans :: (InertCans -> InertCans) -> TcS () -- Modify the inert set with the supplied function updInertCans upd_fn @@ -634,7 +644,7 @@ updInertIrreds upd_fn = updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) } -prepareInertsForImplications :: InertSet -> (InertSet) +prepareInertsForImplications :: InertSet -> InertSet -- See Note [Preparing inert set for implications] prepareInertsForImplications is@(IS { inert_cans = cans }) = is { inert_cans = getGivens cans @@ -689,31 +699,50 @@ them into Givens. There can *be* deriving CFunEqCans; see Trac #8129. getInertEqs :: TcS (TyVarEnv EqualCtList) getInertEqs - = do { inert <- getTcSInerts - ; return (inert_eqs (inert_cans inert)) } + = do { inert <- getInertCans + ; return (inert_eqs inert) } + +getInertGivens :: TcS [Ct] +-- Returns the Given constraints in the inert set, +-- with type functions *not* unflattened +getInertGivens + = do { inerts <- getInertCans + ; let all_cts = foldDicts (:) (inert_dicts inerts) + $ foldFunEqs (:) (inert_funeqs inerts) + $ concat (varEnvElts (inert_eqs inerts)) + ; return (filter isGivenCt all_cts) } getUnsolvedInerts :: TcS ( Bag Implication , Cts -- Tyvar eqs: a ~ ty , Cts -- Fun eqs: F a ~ ty , Cts -- Insoluble , Cts ) -- All others +-- Post-condition: the returned simple constraints are all fully zonked +-- (because they come from the inert set) +-- the unsolved implics may not be getUnsolvedInerts = do { IC { inert_eqs = tv_eqs , inert_funeqs = fun_eqs , inert_irreds = irreds, inert_dicts = idicts , inert_insols = insols } <- getInertCans - ; let unsolved_tv_eqs = foldVarEnv (\cts rest -> - foldr add_if_unsolved rest cts) - emptyCts tv_eqs - unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts - unsolved_irreds = Bag.filterBag is_unsolved irreds - unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts - - others = unsolved_irreds `unionBags` unsolved_dicts + ; let unsolved_tv_eqs = foldVarEnv (\cts rest -> + foldr add_if_unsolved rest cts) + emptyCts tv_eqs + unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts + unsolved_irreds = Bag.filterBag is_unsolved irreds + unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts + others = unsolved_irreds `unionBags` unsolved_dicts ; implics <- getWorkListImplics + ; traceTcS "getUnsolvedInerts" $ + vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs + , text "fun eqs =" <+> ppr unsolved_fun_eqs + , text "insols =" <+> ppr insols + , text "others =" <+> ppr others + , text "implics =" <+> ppr implics ] + ; return ( implics, unsolved_tv_eqs, unsolved_fun_eqs, insols, others) } -- Keep even the given insolubles -- so that we can report dead GADT pattern match branches @@ -828,17 +857,6 @@ b) 'a' will have been completely substituted out in the inert set, For an example, see Trac #9211. -} -splitInertCans :: InertCans -> ([Ct], [Ct], [Ct]) --- ^ Extract the (given, derived, wanted) inert constraints -splitInertCans iCans = (given,derived,wanted) - where - allCts = foldDicts (:) (inert_dicts iCans) - $ foldFunEqs (:) (inert_funeqs iCans) - $ concat (varEnvElts (inert_eqs iCans)) - - (derived,other) = partition isDerivedCt allCts - (wanted,given) = partition isWantedCt other - removeInertCts :: [Ct] -> InertCans -> InertCans -- ^ Remove inert constraints from the 'InertCans', for use when a -- typechecker plugin wishes to discard a given. @@ -1447,22 +1465,20 @@ getTcEvBindsMap = do { EvBindsVar ev_ref _ <- getTcEvBinds ; wrapTcS $ TcM.readTcRef ev_ref } -setWantedTyBind :: TcTyVar -> TcType -> TcS () --- Add a type binding --- We never do this twice! -setWantedTyBind tv ty - | ASSERT2( isMetaTyVar tv, ppr tv ) - isFmvTyVar tv +unifyTyVar :: TcTyVar -> TcType -> TcS () +-- Unify a meta-tyvar with a type +-- We keep track of whether we have done any unifications in tcs_unified, +-- but only for *non-flatten* meta-vars +-- +-- We should never unify the same varaiable twice! +unifyTyVar tv ty = ASSERT2( isMetaTyVar tv, ppr tv ) - wrapTcS (TcM.writeMetaTyVar tv ty) - -- Write directly into the mutable tyvar - -- Flatten meta-vars are born and die locally - - | otherwise - = TcS $ \ env -> - do { TcM.traceTc "setWantedTyBind" (ppr tv <+> text ":=" <+> ppr ty) + TcS $ \ env -> + do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty) ; TcM.writeMetaTyVar tv ty - ; TcM.writeTcRef (tcs_unified env) True } + ; unless (isFmvTyVar tv) $ -- Flatten meta-vars are born and die locally + -- so do not track them in tcs_unified + TcM.writeTcRef (tcs_unified env) True } reportUnifications :: TcS a -> TcS (Bool, a) reportUnifications (TcS thing_inside) @@ -1470,7 +1486,8 @@ reportUnifications (TcS thing_inside) do { inner_unified <- TcM.newTcRef False ; res <- thing_inside (env { tcs_unified = inner_unified }) ; dirty <- TcM.readTcRef inner_unified - ; return (dirty, res) } + ; TcM.updTcRef (tcs_unified env) (|| dirty) -- Inner unifications affect + ; return (dirty, res) } -- the outer scope too getDefaultInfo :: TcS ([Type], (Bool, Bool)) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys @@ -1542,6 +1559,9 @@ zonkTcTyVar tv = wrapTcS (TcM.zonkTcTyVar tv) zonkSimples :: Cts -> TcS Cts zonkSimples cts = wrapTcS (TcM.zonkSimples cts) +zonkWC :: WantedConstraints -> TcS WantedConstraints +zonkWC wc = wrapTcS (TcM.zonkWC wc) + {- Note [Do not add duplicate derived insolubles] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1599,27 +1619,35 @@ newFlattenSkolem :: CtFlavour -> CtLoc -> TcType -- F xis -> TcS (CtEvidence, TcTyVar) -- [W] x:: F xis ~ fsk newFlattenSkolem Given loc fam_ty - = do { checkReductionDepth loc fam_ty - ; fsk <- wrapTcS $ - do { uniq <- TcM.newUnique - ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk") - ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) } - ; ev <- newGivenEvVar loc (mkTcEqPred fam_ty (mkTyVarTy fsk), + = do { fsk <- newFsk fam_ty + ; ev <- newGivenEvVar loc (mkTcEqPred fam_ty (mkTyVarTy fsk), EvCoercion (mkTcNomReflCo fam_ty)) - ; return (ev, fsk) } - -newFlattenSkolem _ loc fam_ty -- Make a wanted - = do { checkReductionDepth loc fam_ty - ; fuv <- wrapTcS $ - do { uniq <- TcM.newUnique - ; ref <- TcM.newMutVar Flexi - ; let details = MetaTv { mtv_info = FlatMetaTv - , mtv_ref = ref - , mtv_tclvl = fskTcLevel } - name = TcM.mkTcTyVarName uniq (fsLit "s") - ; return (mkTcTyVar name (typeKind fam_ty) details) } - ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fuv)) - ; return (ev, fuv) } + ; return (ev, fsk) } + +newFlattenSkolem Wanted loc fam_ty + = do { fmv <- newFmv fam_ty + ; ev <- newWantedEvVarNC loc (mkTcEqPred fam_ty (mkTyVarTy fmv)) + ; return (ev, fmv) } + +newFlattenSkolem Derived loc fam_ty + = do { fmv <- newFmv fam_ty + ; ev <- newDerivedNC loc (mkTcEqPred fam_ty (mkTyVarTy fmv)) + ; return (ev, fmv) } + +newFsk, newFmv :: TcType -> TcS TcTyVar +newFsk fam_ty + = wrapTcS $ do { uniq <- TcM.newUnique + ; let name = TcM.mkTcTyVarName uniq (fsLit "fsk") + ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) } + +newFmv fam_ty + = wrapTcS $ do { uniq <- TcM.newUnique + ; ref <- TcM.newMutVar Flexi + ; let details = MetaTv { mtv_info = FlatMetaTv + , mtv_ref = ref + , mtv_tclvl = fskTcLevel } + name = TcM.mkTcTyVarName uniq (fsLit "s") + ; return (mkTcTyVar name (typeKind fam_ty) details) } extendFlatCache :: TyCon -> [Type] -> (TcCoercion, TcType, CtFlavour) -> TcS () extendFlatCache tc xi_args stuff @@ -1793,11 +1821,16 @@ newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) -- Returns Nothing if cached, -- Just pred if not cached newDerived loc pred + = do { mb_ct <- lookupInInerts pred + ; case mb_ct of + Just {} -> return Nothing + Nothing -> do { ev <- newDerivedNC loc pred + ; return (Just ev) } } + +newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence +newDerivedNC loc pred = do { checkReductionDepth loc pred - ; mb_ct <- lookupInInerts pred - ; return (case mb_ct of - Just {} -> Nothing - Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) } + ; return (CtDerived { ctev_pred = pred, ctev_loc = loc }) } -- | Checks if the depth of the given location is too much. Fails if -- it's too big, with an appropriate error message. diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index be5121d181..5f9f417e1c 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -21,7 +21,7 @@ import TcMType as TcM import TcType import TcSMonad as TcS import TcInteract -import Kind ( isKind, isSubKind, defaultKind_maybe ) +import Kind ( isKind, defaultKind_maybe ) import Inst import Unify ( tcMatchTy ) import Type ( classifyPredType, isIPClass, PredTree(..) @@ -63,13 +63,11 @@ simplifyTop :: WantedConstraints -> TcM (Bag EvBind) -- in a degenerate implication, so we do that here instead simplifyTop wanteds = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds - ; ev_binds_var <- TcM.newTcEvBinds - ; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top - ; binds1 <- TcRnMonad.getTcEvBinds ev_binds_var + ; (final_wc, binds1) <- runTcS (simpl_top wanteds) ; traceTc "End simplifyTop }" empty ; traceTc "reportUnsolved {" empty - ; binds2 <- reportUnsolved zonked_final_wc + ; binds2 <- reportUnsolved final_wc ; traceTc "reportUnsolved }" empty ; return (binds1 `unionBags` binds2) } @@ -194,8 +192,7 @@ More details in Note [DefaultTyVar]. simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM () simplifyAmbiguityCheck ty wanteds = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds) - ; ev_binds_var <- TcM.newTcEvBinds - ; zonked_final_wc <- solveWantedsTcMWithEvBinds ev_binds_var wanteds simpl_top + ; (final_wc, _binds) <- runTcS (simpl_top wanteds) ; traceTc "End simplifyAmbiguityCheck }" empty -- Normally report all errors; but with -XAllowAmbiguousTypes @@ -203,8 +200,8 @@ simplifyAmbiguityCheck ty wanteds -- inaccessible code ; allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes ; traceTc "reportUnsolved(ambig) {" empty - ; unless (allow_ambiguous && not (insolubleWC zonked_final_wc)) - (discardResult (reportUnsolved zonked_final_wc)) + ; unless (allow_ambiguous && not (insolubleWC final_wc)) + (discardResult (reportUnsolved final_wc)) ; traceTc "reportUnsolved(ambig) }" empty ; return () } @@ -221,14 +218,11 @@ simplifyDefault :: ThetaType -- Wanted; has no type variables in it simplifyDefault theta = do { traceTc "simplifyInteractive" empty ; wanted <- newWanteds DefaultOrigin theta - ; (unsolved, _binds) <- solveWantedsTcM (mkSimpleWC wanted) + ; unsolved <- solveWantedsTcM wanted ; traceTc "reportUnsolved {" empty -- See Note [Deferring coercion errors to runtime] ; reportAllUnsolved unsolved - -- Postcondition of solveWantedsTcM is that returned - -- constraints are zonked. So Precondition of reportUnsolved - -- is true. ; traceTc "reportUnsolved }" empty ; return () } @@ -304,7 +298,7 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds ; ev_binds_var <- TcM.newTcEvBinds ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ runTcSWithEvBinds ev_binds_var (solveWanteds wanteds) - ; wanted_transformed_incl_derivs <- zonkWC wanted_transformed_incl_derivs + ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs -- Step 4) Candidates for quantification are an approximation of wanted_transformed -- NB: Already the fixpoint of any unifications that may have happened @@ -347,10 +341,10 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds -- Decide what type variables and constraints to quantify ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus - ; (qtvs, bound_theta, mr_bites) + ; (qtvs, bound_theta, mr_bites) <- decideQuantification apply_mr quant_pred_candidates zonked_tau_tvs - -- Emit an implication constraint for the + -- Emit an implication constraint for the -- remaining constraints from the RHS ; bound_ev_vars <- mapM TcM.newEvVar bound_theta ; let skol_info = InferSkol [ (name, mkSigmaTy [] bound_theta ty) @@ -373,7 +367,7 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds -- Promote any type variables that are free in the inferred type -- of the function: -- f :: forall qtvs. bound_theta => zonked_tau - -- These variables now become free in the envt, and hence will show + -- These variables now become free in the envt, and hence will show -- up whenever 'f' is called. They may currently at rhs_tclvl, but -- they had better be unifiable at the outer_tclvl! -- Example: envt mentions alpha[1] @@ -437,7 +431,7 @@ If the MR does apply, mono_tvs includes all the constrained tyvars, and the quantified constraints are empty. -} -decideQuantification +decideQuantification :: Bool -- Apply monomorphism restriction -> [PredType] -> TcTyVarSet -- Constraints and type variables from RHS -> TcM ( [TcTyVar] -- Quantify over these tyvars (skolems) @@ -693,118 +687,88 @@ It does this by keeping track of which errors correspond to which coercion in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors and does not fail if -fdefer-type-errors is on, so that we can continue compilation. The errors are turned into warnings in `reportUnsolved`. - -Note [Zonk after solving] -~~~~~~~~~~~~~~~~~~~~~~~~~ -We zonk the result immediately after constraint solving, for two reasons: - -a) because zonkWC generates evidence, and this is the moment when we - have a suitable evidence variable to hand. - -Note that *after* solving the constraints are typically small, so the -overhead is not great. -} -solveWantedsTcMWithEvBinds :: EvBindsVar - -> WantedConstraints - -> (WantedConstraints -> TcS WantedConstraints) - -> TcM WantedConstraints --- Returns a *zonked* result --- We zonk when we finish primarily to un-flatten out any --- flatten-skolems etc introduced by canonicalisation of --- types involving type funuctions. Happily the result --- is typically much smaller than the input, indeed it is --- often empty. -solveWantedsTcMWithEvBinds ev_binds_var wc tcs_action - = do { traceTc "solveWantedsTcMWithEvBinds" $ text "wanted=" <+> ppr wc - ; wc2 <- runTcSWithEvBinds ev_binds_var (tcs_action wc) - ; zonkWC wc2 } - -- See Note [Zonk after solving] - -solveWantedsTcM :: WantedConstraints -> TcM (WantedConstraints, Bag EvBind) --- Zonk the input constraints, and simplify them --- Return the evidence binds in the BagEvBinds result +solveWantedsTcM :: [CtEvidence] -> TcM WantedConstraints +-- Simplify the input constraints +-- Discard the evidence binds -- Discards all Derived stuff in result --- Postcondition: fully zonked and unflattened constraints +-- Result is /not/ guaranteed zonked solveWantedsTcM wanted - = do { (wanted1, binds) <- runTcS (solveWantedsAndDrop wanted) - ; wanted2 <- zonkWC wanted1 - ; return (wanted2, binds) } + = do { (wanted1, _binds) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted)) + ; return wanted1 } -solveWantedsAndDrop :: WantedConstraints -> TcS (WantedConstraints) +solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints -- Since solveWanteds returns the residual WantedConstraints, -- it should always be called within a runTcS or something similar, -solveWantedsAndDrop wanted = do { wc <- solveWanteds wanted - ; return (dropDerivedWC wc) } +-- Result is not zonked +solveWantedsAndDrop wanted + = do { wc <- solveWanteds wanted + ; return (dropDerivedWC wc) } solveWanteds :: WantedConstraints -> TcS WantedConstraints -- so that the inert set doesn't mindlessly propagate. -- NB: wc_simples may be wanted /or/ derived now -solveWanteds wanteds - = do { traceTcS "solveWanteds {" (ppr wanteds) +solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) + = do { traceTcS "solveWanteds {" (ppr wc) -- Try the simple bit, including insolubles. Solving insolubles a -- second time round is a bit of a waste; but the code is simple -- and the program is wrong anyway, and we don't run the danger -- of adding Derived insolubles twice; see -- TcSMonad Note [Do not add duplicate derived insolubles] - ; traceTcS "solveSimples {" empty - ; solved_simples_wanteds <- solveSimples wanteds - ; traceTcS "solveSimples end }" (ppr solved_simples_wanteds) + ; wc1 <- solveSimpleWanteds simples + ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 - -- solveWanteds iterates when it is able to float equalities - -- equalities out of one or more of the implications. - ; final_wanteds <- simpl_loop 1 solved_simples_wanteds + ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1) + + ; final_wc <- simpl_loop 0 floated_eqs + (WC { wc_simple = simples1, wc_impl = implics2 + , wc_insol = insols `unionBags` insols1 }) ; bb <- getTcEvBindsMap ; traceTcS "solveWanteds }" $ - vcat [ text "final wc =" <+> ppr final_wanteds + vcat [ text "final wc =" <+> ppr final_wc , text "current evbinds =" <+> ppr (evBindMapBinds bb) ] - ; return final_wanteds } - -solveSimples :: WantedConstraints -> TcS WantedConstraints --- Solve the wc_simple component of the WantedConstraints --- No point in looking at wc_insol because they are, well, insoluble --- Do not affect the inerts -solveSimples (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) - = nestTcS $ - do { wc <- solveSimpleWanteds simples - ; return ( wc { wc_impl = implics `unionBags` wc_impl wc - , wc_insol = insols `unionBags` wc_insol wc } ) } + ; return final_wc } -simpl_loop :: Int +simpl_loop :: Int -> Cts -> WantedConstraints -> TcS WantedConstraints -simpl_loop n wanteds@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) +simpl_loop n floated_eqs + wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) | n > 10 - = do { traceTcS "solveWanteds: loop!" empty - ; return wanteds } + = do { traceTcS "solveWanteds: loop!" (ppr wc); return wc } + + | no_floated_eqs + = return wc -- Done! | otherwise = do { traceTcS "simpl_loop, iteration" (int n) - ; (floated_eqs, unsolved_implics) <- solveNestedImplications implics - ; if isEmptyBag floated_eqs - then return (wanteds { wc_impl = unsolved_implics }) - else + -- solveSimples may make progress if either float_eqs hold + ; (unifs_happened1, wc1) <- if no_floated_eqs + then return (False, emptyWC) + else reportUnifications $ + solveSimpleWanteds (floated_eqs `unionBags` simples) + -- Put floated_eqs first so they get solved first + -- NB: the floated_eqs may include /derived/ equalities + -- arising from fundeps inside an implication - do { -- Put floated_eqs into the current inert set before looping - (unifs_happened, solve_simple_res) - <- reportUnifications $ - solveSimples (WC { wc_simple = floated_eqs `unionBags` simples - -- Put floated_eqs first so they get solved first - , wc_insol = emptyBag, wc_impl = emptyBag }) + ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1 - ; let new_wanteds = solve_simple_res `andWC` - WC { wc_simple = emptyBag - , wc_insol = insols - , wc_impl = unsolved_implics } + -- solveImplications may make progress only if unifs2 holds + ; (floated_eqs2, implics2) <- if not unifs_happened1 && isEmptyBag implics1 + then return (emptyBag, implics) + else solveNestedImplications (implics `unionBags` implics1) - ; if not unifs_happened -- See Note [Cutting off simpl_loop] - && isEmptyBag (wc_impl solve_simple_res) - then return new_wanteds - else simpl_loop (n+1) new_wanteds } } + ; simpl_loop (n+1) floated_eqs2 + (WC { wc_simple = simples1, wc_impl = implics2 + , wc_insol = insols `unionBags` insols1 }) } + + where + no_floated_eqs = isEmptyBag floated_eqs solveNestedImplications :: Bag Implication -> TcS (Cts, Bag Implication) @@ -851,22 +815,23 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts) -- Solve the nested constraints - ; (no_given_eqs, residual_wanted) + ; (no_given_eqs, given_insols, residual_wanted) <- nestImplicTcS ev_binds tclvl $ - do { solveSimpleGivens (mkGivenLoc tclvl info env) givens + do { given_insols <- solveSimpleGivens (mkGivenLoc tclvl info env) givens + ; no_eqs <- getNoGivenEqs tclvl skols ; residual_wanted <- solveWanteds wanteds -- solveWanteds, *not* solveWantedsAndDrop, because -- we want to retain derived equalities so we can float -- them out in floatEqualities - ; no_eqs <- getNoGivenEqs tclvl skols - - ; return (no_eqs, residual_wanted) } + ; return (no_eqs, given_insols, residual_wanted) } - ; (floated_eqs, final_wanted) + ; (floated_eqs, residual_wanted) <- floatEqualities skols no_given_eqs residual_wanted + ; let final_wanted = residual_wanted `addInsols` given_insols + ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs , ic_wanted = final_wanted }) @@ -883,7 +848,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl setImplicationStatus :: Implication -> TcS (Maybe Implication) -- Finalise the implication returned from solveImplication: -- * Set the ic_status field --- * Trim the ic_wanted field +-- * Trim the ic_wanted field to remove Derived constraints -- Return Nothing if we can discard the implication altogether setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _ , ic_info = info @@ -892,12 +857,14 @@ setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _ | some_insoluble = return $ Just $ implic { ic_status = IC_Insoluble - , ic_wanted = wc { wc_simple = pruned_simples } } + , ic_wanted = wc { wc_simple = pruned_simples + , wc_insol = pruned_insols } } | some_unsolved = return $ Just $ implic { ic_status = IC_Unsolved - , ic_wanted = wc { wc_simple = pruned_simples } } + , ic_wanted = wc { wc_simple = pruned_simples + , wc_insol = pruned_insols } } | otherwise -- Everything is solved; look at the implications -- See Note [Tracking redundant constraints] @@ -919,6 +886,7 @@ setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _ , ics_dead = dead_givens } final_implic = implic { ic_status = final_status , ic_wanted = wc { wc_simple = pruned_simples + , wc_insol = pruned_insols , wc_impl = pruned_implics } } -- We can only prune the child implications (pruned_implics) -- in the IC_Solved status case, because only then we can @@ -935,7 +903,8 @@ setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _ some_unsolved = not (isEmptyBag simples && isEmptyBag insols) || isNothing mb_implic_needs - pruned_simples = filterBag isWantedCt simples -- Drop Derived constraints + pruned_simples = dropDerivedSimples simples + pruned_insols = dropDerivedInsols insols pruned_implics = filterBag need_to_keep_implic implics mb_implic_needs :: Maybe VarSet @@ -1150,7 +1119,7 @@ promoteTyVar tclvl tv | isFloatedTouchableMetaTyVar tclvl tv = do { cloned_tv <- TcS.cloneMetaTyVar tv ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl - ; setWantedTyBind tv (mkTyVarTy rhs_tv) + ; unifyTyVar tv (mkTyVarTy rhs_tv) ; return rhs_tv } | otherwise = return tv @@ -1171,7 +1140,7 @@ defaultTyVar the_tv = do { tv' <- TcS.cloneMetaTyVar the_tv ; let new_tv = setTyVarKind tv' default_k ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv) - ; setWantedTyBind the_tv (mkTyVarTy new_tv) + ; unifyTyVar the_tv (mkTyVarTy new_tv) ; return new_tv } -- Why not directly derived_pred = mkTcEqPred k default_k? -- See Note [DefaultTyVar] @@ -1453,43 +1422,10 @@ floatEqualities skols no_given_eqs wanteds@(WC { wc_simple = simples }) ; return (float_eqs, wanteds { wc_simple = remaining_simples }) } where skol_set = mkVarSet skols - (float_eqs, remaining_simples) = partitionBag float_me simples - - float_me :: Ct -> Bool - float_me ct -- The constraint is un-flattened and de-cannonicalised - | let pred = ctPred ct - , EqPred NomEq ty1 ty2 <- classifyPredType pred - , tyVarsOfType pred `disjointVarSet` skol_set - , useful_to_float ty1 ty2 - = True - | otherwise - = False - - -- Float out alpha ~ ty, or ty ~ alpha - -- which might be unified outside - -- See Note [Do not float kind-incompatible equalities] - useful_to_float ty1 ty2 - = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of - (Just tv1, _) | isMetaTyVar tv1 - , k2 `isSubKind` k1 - -> True - (_, Just tv2) | isMetaTyVar tv2 - , k1 `isSubKind` k2 - -> True - _ -> False - where - k1 = typeKind ty1 - k2 = typeKind ty2 + (float_eqs, remaining_simples) = partitionBag (usefulToFloat is_useful) simples + is_useful pred = tyVarsOfType pred `disjointVarSet` skol_set -{- -Note [Do not float kind-incompatible equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If we have (t::* ~ s::*->*), we'll get a Derived insoluble equality. -If we float the equality outwards, we'll get *another* Derived -insoluble equality one level out, so the same error will be reported -twice. So we refrain from floating such equalities - -Note [Float equalities from under a skolem binding] +{- Note [Float equalities from under a skolem binding] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Which of the simple equalities can we float out? Obviously, only ones that don't mention the skolem-bound variables. But that is @@ -1537,22 +1473,22 @@ to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be. -} applyDefaultingRules :: WantedConstraints -> TcS Bool - -- True <=> I did some defaulting, reflected in ty_binds +-- True <=> I did some defaulting, by unifying a meta-tyvar +-- Imput WantedConstraints are not necessarily zonked --- Return some extra derived equalities, which express the --- type-class default choice. applyDefaultingRules wanteds | isEmptyWC wanteds = return False | otherwise - = do { traceTcS "applyDefaultingRules { " $ - text "wanteds =" <+> ppr wanteds + = do { info@(default_tys, _) <- getDefaultInfo + ; wanteds <- TcS.zonkWC wanteds - ; info@(default_tys, _) <- getDefaultInfo ; let groups = findDefaultableGroups info wanteds - ; traceTcS "findDefaultableGroups" $ vcat [ text "groups=" <+> ppr groups - , text "info=" <+> ppr info ] + ; traceTcS "applyDefaultingRules {" $ + vcat [ text "wanteds =" <+> ppr wanteds + , text "groups =" <+> ppr groups + , text "info =" <+> ppr info ] ; something_happeneds <- mapM (disambigGroup default_tys) groups @@ -1638,7 +1574,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds) ; if success then -- Success: record the type variable binding, and return - do { setWantedTyBind the_tv default_ty + do { unifyTyVar the_tv default_ty ; wrapWarnTcS $ warnDefaulting wanteds default_ty ; traceTcS "disambigGroup succeeded }" (ppr default_ty) ; return True } diff --git a/testsuite/tests/indexed-types/should_compile/T10340.hs b/testsuite/tests/indexed-types/should_compile/T10340.hs new file mode 100644 index 0000000000..c35c7150ce --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T10340.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} + +module T10340 where + +import GHC.Exts (Any) + +class MonadState s m where + get :: m s + +newtype State s a = State (s -> (s, a)) + +instance MonadState s (State s) where + get = State $ \s -> (s, s) + +foo :: State Any Any +foo = get diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 67309249d4..1cd1ea261a 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -253,4 +253,5 @@ test('T9090', normal, compile, ['']) test('T10020', normal, compile, ['']) test('T10079', normal, compile, ['']) test('T10139', normal, compile, ['']) +test('T10340', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr index 13f9911e6c..b551f39d4c 100644 --- a/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr +++ b/testsuite/tests/indexed-types/should_fail/ExtraTcsUntch.stderr @@ -1,16 +1,18 @@ -ExtraTcsUntch.hs:23:18: - Couldn't match expected type ‘F Int’ with actual type ‘[t]’ +ExtraTcsUntch.hs:23:18: error: + Couldn't match expected type ‘F Int’ with actual type ‘[[t]]’ Relevant bindings include - x :: t (bound at ExtraTcsUntch.hs:21:3) - f :: t -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1) + x :: [t] (bound at ExtraTcsUntch.hs:21:3) + f :: [t] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1) In the first argument of ‘h’, namely ‘[x]’ In the expression: h [x] In an equation for ‘g1’: g1 _ = h [x] -ExtraTcsUntch.hs:25:38: - Couldn't match expected type ‘F Int’ with actual type ‘[[t0]]’ - The type variable ‘t0’ is ambiguous +ExtraTcsUntch.hs:25:38: error: + Couldn't match expected type ‘F Int’ with actual type ‘[[t]]’ + Relevant bindings include + x :: [t] (bound at ExtraTcsUntch.hs:21:3) + f :: [t] -> ((), ((), ())) (bound at ExtraTcsUntch.hs:21:1) In the first argument of ‘h’, namely ‘[[undefined]]’ In the expression: h [[undefined]] In the expression: (h [[undefined]], op x [y]) diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.hs b/testsuite/tests/indexed-types/should_fail/T4093a.hs index 8bc26d69d3..fc611684d4 100644 --- a/testsuite/tests/indexed-types/should_fail/T4093a.hs +++ b/testsuite/tests/indexed-types/should_fail/T4093a.hs @@ -1,45 +1,47 @@ -{-# LANGUAGE TypeFamilies #-}
-module T4093a where
-
-type family Foo x
-type instance Foo () = Maybe ()
-
-hang :: (Foo e ~ Maybe e) => Foo e
-hang = Just ()
-
-
-{- Ambiguity check
-
- [G] Foo e ~ Maybe e
- [W] Foo e ~ Foo e0
- [W] Foo e0 ~ Maybe e0
----
- [G] Foo e ~ fsk
- [G] fsk ~ Maybe e
-
- [W] Foo e ~ fmv1
- [W] Foo e0 ~ fmv2
- [W] fmv1 ~ fmv2
- [W] fmv2 ~ Maybe e0
-
----> fmv1 := fsk
- [G] Foo e ~ fsk
- [G] fsk ~ Maybe e
-
- [W] Foo e0 ~ fmv2
- [W] fsk ~ fmv2
- [W] fmv2 ~ Maybe e0
-
---->
- [G] Foo e ~ fsk
- [G] fsk ~ Maybe e
-
- [W] Foo e0 ~ fmv2
- [W] fmv2 ~ Maybe e
- [W] fmv2 ~ Maybe e0
-
-Now the question is whether we get a derived equality e ~ e0. Currently
-we don't, but we easily could. But then we'd need to be careful not to
-report insoluble Int ~ Bool if we had
- F a ~ Int, F a ~ Bool
--}
\ No newline at end of file +{-# LANGUAGE TypeFamilies #-} +module T4093a where + +type family Foo x +type instance Foo () = Maybe () + +hang :: (Foo e ~ Maybe e) => Foo e +hang = Just () + +-- Type is not ambiguous; should get a complaint +-- for (e ~ ()) arising from the Just () + +{- Ambiguity check + + [G] Foo e ~ Maybe e + [W] Foo e ~ Foo e0 + [W] Foo e0 ~ Maybe e0 +--- + [G] Foo e ~ fsk + [G] fsk ~ Maybe e + + [W] Foo e ~ fmv1 + [W] Foo e0 ~ fmv2 + [W] fmv1 ~ fmv2 + [W] fmv2 ~ Maybe e0 + +---> fmv1 := fsk + [G] Foo e ~ fsk + [G] fsk ~ Maybe e + + [W] Foo e0 ~ fmv2 + [W] fsk ~ fmv2 + [W] fmv2 ~ Maybe e0 + +---> + [G] Foo e ~ fsk + [G] fsk ~ Maybe e + + [W] Foo e0 ~ fmv2 + [W] fmv2 ~ Maybe e + [W] fmv2 ~ Maybe e0 + +Now the question is whether we get a derived equality e ~ e0. Currently +we don't, but we easily could. But then we'd need to be careful not to +report insoluble Int ~ Bool if we had + F a ~ Int, F a ~ Bool +-} diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.stderr b/testsuite/tests/indexed-types/should_fail/T4093a.stderr index 0228a88edf..b1810d3096 100644 --- a/testsuite/tests/indexed-types/should_fail/T4093a.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4093a.stderr @@ -1,14 +1,14 @@ -T4093a.hs:7:9: - Could not deduce: Foo e0 ~ Maybe e +T4093a.hs:8:8: error: + Could not deduce: e ~ () from the context: Foo e ~ Maybe e bound by the type signature for: hang :: (Foo e ~ Maybe e) => Foo e at T4093a.hs:7:9-34 - The type variable ‘e0’ is ambiguous + ‘e’ is a rigid type variable bound by + the type signature for: hang :: (Foo e ~ Maybe e) => Foo e + at T4093a.hs:7:9 Expected type: Foo e - Actual type: Foo e0 - In the ambiguity check for the type signature for ‘hang’: - hang :: forall e. (Foo e ~ Maybe e) => Foo e - To defer the ambiguity check to use sites, enable AllowAmbiguousTypes - In the type signature for ‘hang’: - hang :: (Foo e ~ Maybe e) => Foo e + Actual type: Maybe () + Relevant bindings include hang :: Foo e (bound at T4093a.hs:8:1) + In the expression: Just () + In an equation for ‘hang’: hang = Just () diff --git a/testsuite/tests/indexed-types/should_fail/T4254.stderr b/testsuite/tests/indexed-types/should_fail/T4254.stderr index e69de29bb2..e22fd380ef 100644 --- a/testsuite/tests/indexed-types/should_fail/T4254.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4254.stderr @@ -0,0 +1,4 @@ + +T4254.hs:18:10: warning: + Redundant constraint: FD a b + In the type signature for: fails :: (a ~ Int, FD a b) => a -> Bool diff --git a/testsuite/tests/indexed-types/should_fail/T7729.stderr b/testsuite/tests/indexed-types/should_fail/T7729.stderr index 053d54e264..7be5d5764c 100644 --- a/testsuite/tests/indexed-types/should_fail/T7729.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7729.stderr @@ -1,6 +1,6 @@ -T7729.hs:36:14: - Couldn't match type ‘t0 (BasePrimMonad m)’ with ‘BasePrimMonad m’ +T7729.hs:36:14: error: + Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’ The type variable ‘t0’ is ambiguous Expected type: t0 (BasePrimMonad m) a -> Rand m a Actual type: BasePrimMonad (Rand m) a -> Rand m a diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr index 3093abb1a7..e37e4e907d 100644 --- a/testsuite/tests/indexed-types/should_fail/T9662.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr @@ -1,25 +1,25 @@ -T9662.hs:49:7: - Couldn't match type ‘k’ with ‘n’ +T9662.hs:47:8: error: + Couldn't match type ‘k’ with ‘Int’ ‘k’ is a rigid type variable bound by the type signature for: test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - ‘n’ is a rigid type variable bound by - the type signature for: - test :: Shape (((sh :. k) :. m) :. n) - -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - Expected type: Exp (((sh :. m) :. n) :. k) - -> Exp (((sh :. k) :. m) :. n) - Actual type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. k) :. m) :. n) + Expected type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. m) :. n) :. k) + Actual type: Exp + (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) + -> Exp + (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) Relevant bindings include test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) (bound at T9662.hs:45:1) - In the second argument of ‘backpermute’, namely ‘id’ + In the first argument of ‘backpermute’, namely + ‘(modify + (atom :. atom :. atom :. atom) + (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ In the expression: backpermute (modify @@ -27,27 +27,27 @@ T9662.hs:49:7: (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k))) id -T9662.hs:49:7: - Couldn't match type ‘m’ with ‘k’ +T9662.hs:47:8: error: + Couldn't match type ‘m’ with ‘Int’ ‘m’ is a rigid type variable bound by the type signature for: test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - ‘k’ is a rigid type variable bound by - the type signature for: - test :: Shape (((sh :. k) :. m) :. n) - -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - Expected type: Exp (((sh :. m) :. n) :. k) - -> Exp (((sh :. k) :. m) :. n) - Actual type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. k) :. m) :. n) + Expected type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. m) :. n) :. k) + Actual type: Exp + (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) + -> Exp + (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) Relevant bindings include test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) (bound at T9662.hs:45:1) - In the second argument of ‘backpermute’, namely ‘id’ + In the first argument of ‘backpermute’, namely + ‘(modify + (atom :. atom :. atom :. atom) + (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ In the expression: backpermute (modify @@ -55,27 +55,27 @@ T9662.hs:49:7: (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k))) id -T9662.hs:49:7: - Couldn't match type ‘n’ with ‘m’ +T9662.hs:47:8: error: + Couldn't match type ‘n’ with ‘Int’ ‘n’ is a rigid type variable bound by the type signature for: test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) at T9662.hs:44:9 - ‘m’ is a rigid type variable bound by - the type signature for: - test :: Shape (((sh :. k) :. m) :. n) - -> Shape (((sh :. m) :. n) :. k) - at T9662.hs:44:9 - Expected type: Exp (((sh :. m) :. n) :. k) - -> Exp (((sh :. k) :. m) :. n) - Actual type: Exp (((sh :. k) :. m) :. n) - -> Exp (((sh :. k) :. m) :. n) + Expected type: Exp (((sh :. k) :. m) :. n) + -> Exp (((sh :. m) :. n) :. k) + Actual type: Exp + (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) + -> Exp + (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) Relevant bindings include test :: Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) (bound at T9662.hs:45:1) - In the second argument of ‘backpermute’, namely ‘id’ + In the first argument of ‘backpermute’, namely + ‘(modify + (atom :. atom :. atom :. atom) + (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’ In the expression: backpermute (modify diff --git a/testsuite/tests/module/mod71.stderr b/testsuite/tests/module/mod71.stderr index 12962aa473..53d697e133 100644 --- a/testsuite/tests/module/mod71.stderr +++ b/testsuite/tests/module/mod71.stderr @@ -1,20 +1,12 @@ -mod71.hs:4:9: +mod71.hs:4:9: error: Found hole ‘_’ with type: t1 Where: ‘t1’ is a rigid type variable bound by - the inferred type of f :: (t1 -> a -> t) -> t at mod71.hs:4:1 + the inferred type of f :: Num a => (t1 -> a -> t) -> t + at mod71.hs:4:1 Relevant bindings include x :: t1 -> a -> t (bound at mod71.hs:4:3) f :: (t1 -> a -> t) -> t (bound at mod71.hs:4:1) In the first argument of ‘x’, namely ‘_’ In the expression: x _ 1 In an equation for ‘f’: f x = x _ 1 - -mod71.hs:4:11: - No instance for (Num a) arising from the literal ‘1’ - Possible fix: - add (Num a) to the context of - the inferred type of f :: (t1 -> a -> t) -> t - In the second argument of ‘x’, namely ‘1’ - In the expression: x _ 1 - In an equation for ‘f’: f x = x _ 1 diff --git a/testsuite/tests/typecheck/should_compile/FD3.hs b/testsuite/tests/typecheck/should_compile/FD3.hs index 333c0c31dd..a2f7d003a7 100644 --- a/testsuite/tests/typecheck/should_compile/FD3.hs +++ b/testsuite/tests/typecheck/should_compile/FD3.hs @@ -1,15 +1,24 @@ -{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}
-
--- Trac #1795
-
-module ShouldCompile where
-
-data A a = A
-
-class MkA a b | a -> b where
- mkA :: a -> A b
-
-instance MkA a a where
-
-translate :: (String, a) -> A a
-translate a = mkA a
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-} + +-- Trac #1795 + +module ShouldCompile where + +data A a = A + +class MkA a b | a -> b where + mkA :: a -> A b + +instance MkA a a where + +translate :: (String, a) -> A a +translate a = mkA a + +{- From the call to mkA + +[W] MkA alpha beta +[W] alpha ~ (String,a) +[W] A beta ~ A a + +==> beta:=a, alpha:=(String,a) +-} diff --git a/testsuite/tests/typecheck/should_compile/FD3.stderr b/testsuite/tests/typecheck/should_compile/FD3.stderr index 3bed15a490..179fda19e6 100644 --- a/testsuite/tests/typecheck/should_compile/FD3.stderr +++ b/testsuite/tests/typecheck/should_compile/FD3.stderr @@ -1,14 +1,5 @@ -
-FD3.hs:15:15:
- Couldn't match type ‘a’ with ‘(String, a)’
- ‘a’ is a rigid type variable bound by
- the type signature for: translate :: (String, a) -> A a
- at FD3.hs:14:14
- arising from a functional dependency between:
- constraint ‘MkA (String, a) a’ arising from a use of ‘mkA’
- instance ‘MkA a1 a1’ at FD3.hs:12:10-16
- Relevant bindings include
- a :: (String, a) (bound at FD3.hs:15:11)
- translate :: (String, a) -> A a (bound at FD3.hs:15:1)
- In the expression: mkA a
- In an equation for ‘translate’: translate a = mkA a
+ +FD3.hs:15:15: error: + No instance for (MkA (String, a) a) arising from a use of ‘mkA’ + In the expression: mkA a + In an equation for ‘translate’: translate a = mkA a diff --git a/testsuite/tests/typecheck/should_compile/Improvement.hs b/testsuite/tests/typecheck/should_compile/Improvement.hs new file mode 100644 index 0000000000..fba84ffdec --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/Improvement.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-} +{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} +module Foo where + +type family F a +type instance F Int = Bool + +class C a b where + +instance (b~Int) => C Bool b + +blug :: C (F a) a => a -> F a +blug = error "Urk" + +foo :: Bool +foo = blug undefined + diff --git a/testsuite/tests/typecheck/should_compile/T10009.hs b/testsuite/tests/typecheck/should_compile/T10009.hs new file mode 100644 index 0000000000..aae8a4c364 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T10009.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-warn-redundant-constraints #-} +module T10009 where + + +type family F a +type family UnF a + +f :: (UnF (F b) ~ b) => F b -> () +f = error "urk" + +g :: forall a. (UnF (F a) ~ a) => a -> () +g _ = f (undefined :: F a) + + +{- --------------- +[G] UnF (F a) ~ a + +[W] UnF (F beta) ~ beta +[W] F a ~ F beta + +------------------- +[G] g1: F a ~ fsk1 fsk1 := F a +[G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1 +[G] g3: fsk2 ~ a + +[W] w1: F beta ~ fmv1 +[W] w2: UnF fmv1 ~ fmv2 +[W] w3: fmv2 ~ beta +[W] w5: fsk1 ~ fmv1 -- From F a ~ F beta + -- using flat-cache + +---- No progress in solving ----- +-- Unflatten: + +[W] w3: UnF (F beta) ~ beta +[W] w5: fsk1 ~ F beta + +--- Improvement + +[D] F beta ~ fmv1 +[D] UnF fmv1 ~ fmv2 -- (A) +[D] fmv2 ~ beta +[D] fmv1 ~ fsk1 -- (B) From F a ~ F beta + -- NB: put fmv on left + +--> rewrite (A) with (B), and metch with g2 + +[D] F beta ~ fmv1 +[D] fmv2 ~ fsk2 -- (C) +[D] fmv2 ~ beta -- (D) +[D] fmv1 ~ fsk1 + +--> rewrite (D) with (C) and re-orient + +[D] F beta ~ fmv1 +[D] fmv2 ~ fsk2 +[D] beta ~ fsk2 -- (E) +[D] fmv1 ~ fsk1 + +-- Now we can unify beta! +-} diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index a151274a4d..72fe255680 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -451,3 +451,5 @@ test('T10195', normal, compile, ['']) test('T10109', normal, compile, ['']) test('TcCustomSolverSuper', normal, compile, ['']) test('T10335', normal, compile, ['']) +test('Improvement', normal, compile, ['']) +test('T10009', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs b/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs index 923dfa1bd9..591c3bcca9 100644 --- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs +++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs @@ -1,24 +1,11 @@ {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, GADTs #-} -module FDsFromGivens where +module FDsFromGivens where -class C a b | a -> b where +class C a b | a -> b where cop :: a -> b -> () - -data KCC where - KCC :: C Char Char => () -> KCC - - -{- Failing, as it righteously should! -g1 :: (C Char [a], C Char Bool) => a -> () +{- Failing, as it righteously should! It's inaccessible code -} +g1 :: (C Char [a], C Char Bool) => a -> () g1 x = () --} - -f :: C Char [a] => a -> a -f = undefined - -bar (KCC _) = f - -
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr index 52e8d8a4eb..a2a9928181 100644 --- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr +++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr @@ -1,14 +1,17 @@ -
-FDsFromGivens.hs:21:15:
- Couldn't match type ‘Char’ with ‘[a]’
- arising from a functional dependency between constraints:
- ‘C Char [a]’ arising from a use of ‘f’ at FDsFromGivens.hs:21:15
- ‘C Char Char’
- arising from a pattern with constructor:
- KCC :: C Char Char => () -> KCC,
- in an equation for ‘bar’
- at FDsFromGivens.hs:21:6-10
- Relevant bindings include
- bar :: KCC -> a -> a (bound at FDsFromGivens.hs:21:1)
- In the expression: f
- In an equation for ‘bar’: bar (KCC _) = f
+ +FDsFromGivens.hs:9:7: error: + Couldn't match type ‘[a]’ with ‘Bool’ + arising from a functional dependency between constraints: + ‘C Char Bool’ + arising from the type signature for: + g1 :: (C Char [a], C Char Bool) => a -> () + at FDsFromGivens.hs:9:7-42 + ‘C Char [a]’ + arising from the type signature for: + g1 :: (C Char [a], C Char Bool) => a -> () + at FDsFromGivens.hs:9:7-42 + In the ambiguity check for the type signature for ‘g1’: + g1 :: forall a. (C Char [a], C Char Bool) => a -> () + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + In the type signature for ‘g1’: + g1 :: (C Char [a], C Char Bool) => a -> () diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens2.hs b/testsuite/tests/typecheck/should_fail/FDsFromGivens2.hs new file mode 100644 index 0000000000..83b6e32ccf --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens2.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts, GADTs #-} + +module FDsFromGivens2 where + +class C a b | a -> b where + cop :: a -> b -> () + +data KCC where + KCC :: C Char Char => () -> KCC + +f :: C Char [a] => a -> a +f = undefined + +bar (KCC _) = f diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens2.stderr b/testsuite/tests/typecheck/should_fail/FDsFromGivens2.stderr new file mode 100644 index 0000000000..a738c7ffa4 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens2.stderr @@ -0,0 +1,14 @@ + +FDsFromGivens2.hs:14:15: error: + Couldn't match type ‘Char’ with ‘[a]’ + arising from a functional dependency between constraints: + ‘C Char [a]’ arising from a use of ‘f’ at FDsFromGivens2.hs:14:15 + ‘C Char Char’ + arising from a pattern with constructor: + KCC :: C Char Char => () -> KCC, + in an equation for ‘bar’ + at FDsFromGivens2.hs:14:6-10 + Relevant bindings include + bar :: KCC -> a -> a (bound at FDsFromGivens2.hs:14:1) + In the expression: f + In an equation for ‘bar’: bar (KCC _) = f diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr index 37e7b23d73..1702afcafc 100644 --- a/testsuite/tests/typecheck/should_fail/T1899.stderr +++ b/testsuite/tests/typecheck/should_fail/T1899.stderr @@ -1,13 +1,13 @@ -
-T1899.hs:14:36:
- Couldn't match type ‘a’ with ‘Proposition a1’
- ‘a’ is a rigid type variable bound by
- the type signature for: transRHS :: [a] -> Int -> Constraint a
- at T1899.hs:9:14
- Expected type: [Proposition a1]
- Actual type: [a]
- Relevant bindings include
- varSet :: [a] (bound at T1899.hs:10:11)
- transRHS :: [a] -> Int -> Constraint a (bound at T1899.hs:10:2)
- In the first argument of ‘Auxiliary’, namely ‘varSet’
- In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
+ +T1899.hs:14:36: error: + Couldn't match type ‘a’ with ‘Proposition a0’ + ‘a’ is a rigid type variable bound by + the type signature for: transRHS :: [a] -> Int -> Constraint a + at T1899.hs:9:14 + Expected type: [Proposition a0] + Actual type: [a] + Relevant bindings include + varSet :: [a] (bound at T1899.hs:10:11) + transRHS :: [a] -> Int -> Constraint a (bound at T1899.hs:10:2) + In the first argument of ‘Auxiliary’, namely ‘varSet’ + In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’ diff --git a/testsuite/tests/typecheck/should_fail/T5246.stderr b/testsuite/tests/typecheck/should_fail/T5246.stderr index 454c2b73b3..54d340cc5e 100644 --- a/testsuite/tests/typecheck/should_fail/T5246.stderr +++ b/testsuite/tests/typecheck/should_fail/T5246.stderr @@ -1,5 +1,5 @@ -T5246.hs:11:10: +T5246.hs:11:10: error: Couldn't match type ‘[Char]’ with ‘Int’ arising from a functional dependency between constraints: ‘?x::Int’ arising from a use of ‘foo’ at T5246.hs:11:10-12 diff --git a/testsuite/tests/typecheck/should_fail/T5570.stderr b/testsuite/tests/typecheck/should_fail/T5570.stderr index 15d5c8a19e..45cdfd5679 100644 --- a/testsuite/tests/typecheck/should_fail/T5570.stderr +++ b/testsuite/tests/typecheck/should_fail/T5570.stderr @@ -1,5 +1,5 @@ -T5570.hs:7:16: +T5570.hs:7:16: error: Couldn't match kind ‘*’ with ‘#’ When matching types r0 :: * diff --git a/testsuite/tests/typecheck/should_fail/T5689.stderr b/testsuite/tests/typecheck/should_fail/T5689.stderr index 211ec522a1..f8294f4705 100644 --- a/testsuite/tests/typecheck/should_fail/T5689.stderr +++ b/testsuite/tests/typecheck/should_fail/T5689.stderr @@ -1,32 +1,8 @@ -T5689.hs:10:36: +T5689.hs:10:36: error: Couldn't match expected type ‘Bool’ with actual type ‘t’ Relevant bindings include v :: t (bound at T5689.hs:10:28) r :: IORef (t -> t) (bound at T5689.hs:7:14) In the expression: v In the expression: if v then False else True - -T5689.hs:10:43: - Couldn't match expected type ‘t’ with actual type ‘Bool’ - Relevant bindings include - v :: t (bound at T5689.hs:10:28) - r :: IORef (t -> t) (bound at T5689.hs:7:14) - In the expression: False - In the expression: if v then False else True - -T5689.hs:10:54: - Couldn't match expected type ‘t’ with actual type ‘Bool’ - Relevant bindings include - v :: t (bound at T5689.hs:10:28) - r :: IORef (t -> t) (bound at T5689.hs:7:14) - In the expression: True - In the expression: if v then False else True - -T5689.hs:14:23: - Couldn't match expected type ‘t’ with actual type ‘Bool’ - Relevant bindings include - c :: t -> t (bound at T5689.hs:12:13) - r :: IORef (t -> t) (bound at T5689.hs:7:14) - In the first argument of ‘c’, namely ‘True’ - In the second argument of ‘($)’, namely ‘c True’ diff --git a/testsuite/tests/typecheck/should_fail/T5691.hs b/testsuite/tests/typecheck/should_fail/T5691.hs index 49fc776eac..88cd3d7565 100644 --- a/testsuite/tests/typecheck/should_fail/T5691.hs +++ b/testsuite/tests/typecheck/should_fail/T5691.hs @@ -12,7 +12,7 @@ class Test p where instance Test PrintRuleInterp where test (f :: p a) = - MkPRI $ printRule_ f + MkPRI $ printRule_ f newtype RecDecParser a = MkRD { diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr index b5bf71d959..132df4dacf 100644 --- a/testsuite/tests/typecheck/should_fail/T5691.stderr +++ b/testsuite/tests/typecheck/should_fail/T5691.stderr @@ -1,27 +1,19 @@ -
-T5691.hs:14:9:
- Couldn't match type ‘p’ with ‘PrintRuleInterp’
- Expected type: p a
- Actual type: PrintRuleInterp a
- When checking that the pattern signature: p a
- fits the type of its context: PrintRuleInterp a
- In the pattern: f :: p a
- In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f
-
-T5691.hs:15:24:
- Couldn't match type ‘p’ with ‘PrintRuleInterp’
- Expected type: PrintRuleInterp a
- Actual type: p a
- Relevant bindings include f :: p a (bound at T5691.hs:14:9)
- In the first argument of ‘printRule_’, namely ‘f’
- In the second argument of ‘($)’, namely ‘printRule_ f’
-
-T5691.hs:24:10:
- No instance for (Alternative RecDecParser)
- arising from the superclasses of an instance declaration
- In the instance declaration for ‘MonadPlus RecDecParser’
-
-T5691.hs:24:10:
- No instance for (Monad RecDecParser)
- arising from the superclasses of an instance declaration
- In the instance declaration for ‘MonadPlus RecDecParser’
+ +T5691.hs:14:9: error: + Couldn't match type ‘p’ with ‘PrintRuleInterp’ + Expected type: p a + Actual type: PrintRuleInterp a + When checking that the pattern signature: p a + fits the type of its context: PrintRuleInterp a + In the pattern: f :: p a + In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f + +T5691.hs:24:10: error: + No instance for (Alternative RecDecParser) + arising from the superclasses of an instance declaration + In the instance declaration for ‘MonadPlus RecDecParser’ + +T5691.hs:24:10: error: + No instance for (Monad RecDecParser) + arising from the superclasses of an instance declaration + In the instance declaration for ‘MonadPlus RecDecParser’ diff --git a/testsuite/tests/typecheck/should_fail/T5978.stderr b/testsuite/tests/typecheck/should_fail/T5978.stderr index 263e68ba2d..9fae4e28fe 100644 --- a/testsuite/tests/typecheck/should_fail/T5978.stderr +++ b/testsuite/tests/typecheck/should_fail/T5978.stderr @@ -1,8 +1,8 @@ -T5978.hs:22:11: - Couldn't match type ‘Bool’ with ‘Char’ +T5978.hs:22:11: error: + Couldn't match type ‘Char’ with ‘Bool’ arising from a functional dependency between: - constraint ‘C Double Char’ arising from a use of ‘polyBar’ - instance ‘C Double Bool’ at T5978.hs:8:10-22 + constraint ‘C Float Bool’ arising from a use of ‘polyBar’ + instance ‘C Float Char’ at T5978.hs:7:10-21 In the expression: polyBar id monoFoo In an equation for ‘monoBar’: monoBar = polyBar id monoFoo diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr index 2a022645d8..c6c11e81b7 100644 --- a/testsuite/tests/typecheck/should_fail/T7368.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368.stderr @@ -1,5 +1,5 @@ -T7368.hs:3:10: +T7368.hs:3:10: error: Couldn't match kind ‘* -> *’ with ‘*’ When matching types c0 :: (* -> *) -> * diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr index 79396df9d7..7ee59e129e 100644 --- a/testsuite/tests/typecheck/should_fail/T7368a.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr @@ -1,5 +1,5 @@ -T7368a.hs:8:6: +T7368a.hs:8:6: error: Couldn't match kind ‘*’ with ‘* -> *’ When matching types f :: * -> * diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr index 2b891773c4..0a0f73d47e 100644 --- a/testsuite/tests/typecheck/should_fail/T7453.stderr +++ b/testsuite/tests/typecheck/should_fail/T7453.stderr @@ -1,45 +1,45 @@ -
-T7453.hs:10:30:
- Couldn't match expected type ‘t1’ with actual type ‘t’
- because type variable ‘t1’ would escape its scope
- This (rigid, skolem) type variable is bound by
- the type signature for: z :: Id t1
- at T7453.hs:8:16-19
- Relevant bindings include
- aux :: Id t1 (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)
- In the first argument of ‘Id’, namely ‘v’
- In the expression: Id v
-
-T7453.hs:16:33:
- Couldn't match expected type ‘t2’ with actual type ‘t’
- because type variable ‘t2’ would escape its scope
- This (rigid, skolem) type variable is bound by
- the type signature for: z :: () -> t2
- at T7453.hs:14:16-22
- Relevant bindings include
- aux :: b -> t2 (bound at T7453.hs:16:21)
- z :: () -> t2 (bound at T7453.hs:15:11)
- v :: t (bound at T7453.hs:13:7)
- cast2 :: t -> t1 (bound at T7453.hs:13:1)
- In the first argument of ‘const’, namely ‘v’
- In the expression: const v
-
-T7453.hs:21:15:
- Couldn't match expected type ‘t1’ with actual type ‘a’
- because type variable ‘t1’ would escape its scope
- This (rigid, skolem) type variable is bound by
- the type signature for: z :: t1
- at T7453.hs:20:16
- Relevant bindings include
- aux :: forall b. b -> a (bound at T7453.hs:22:21)
- z :: t1 (bound at T7453.hs:21:11)
- v :: a (bound at T7453.hs:19:7)
- cast3 :: a -> t (bound at T7453.hs:19:1)
- In the expression: v
- In an equation for ‘z’:
- z = v
- where
- aux = const v
+ +T7453.hs:10:30: error: + Couldn't match expected type ‘t1’ with actual type ‘t’ + because type variable ‘t1’ would escape its scope + This (rigid, skolem) type variable is bound by + the type signature for: z :: Id t1 + at T7453.hs:8:16-19 + Relevant bindings include + aux :: Id t1 (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) + In the first argument of ‘Id’, namely ‘v’ + In the expression: Id v + +T7453.hs:16:33: error: + Couldn't match expected type ‘t2’ with actual type ‘t’ + because type variable ‘t2’ would escape its scope + This (rigid, skolem) type variable is bound by + the type signature for: z :: () -> t2 + at T7453.hs:14:16-22 + Relevant bindings include + aux :: b -> t2 (bound at T7453.hs:16:21) + z :: () -> t2 (bound at T7453.hs:15:11) + v :: t (bound at T7453.hs:13:7) + cast2 :: t -> t1 (bound at T7453.hs:13:1) + In the first argument of ‘const’, namely ‘v’ + In the expression: const v + +T7453.hs:21:15: error: + Couldn't match expected type ‘t2’ with actual type ‘t’ + because type variable ‘t2’ would escape its scope + This (rigid, skolem) type variable is bound by + the type signature for: z :: t2 + at T7453.hs:20:16 + Relevant bindings include + aux :: forall b. b -> t2 (bound at T7453.hs:22:21) + z :: t2 (bound at T7453.hs:21:11) + v :: t (bound at T7453.hs:19:7) + cast3 :: t -> t1 (bound at T7453.hs:19:1) + In the expression: v + In an equation for ‘z’: + z = v + where + aux = const v diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr index 65dfb79d2b..1fc2e43755 100644 --- a/testsuite/tests/typecheck/should_fail/T7696.stderr +++ b/testsuite/tests/typecheck/should_fail/T7696.stderr @@ -1,7 +1,11 @@ -
-T7696.hs:7:6:
- Couldn't match type ‘m0 a0’ with ‘()’
- Expected type: ((), w ())
- Actual type: (m0 a0, t0 m0)
- In the expression: f1
- In an equation for ‘f2’: f2 = f1
+ +T7696.hs:7:6: error: + Couldn't match kind ‘* -> *’ with ‘*’ + When matching types + t0 :: (* -> *) -> * + w :: * -> * + Expected type: ((), w ()) + Actual type: (m0 a0, t0 m0) + Relevant bindings include f2 :: ((), w ()) (bound at T7696.hs:7:1) + In the expression: f1 + In an equation for ‘f2’: f2 = f1 diff --git a/testsuite/tests/typecheck/should_fail/T8142.stderr b/testsuite/tests/typecheck/should_fail/T8142.stderr index a084f7afcc..43a3a46be0 100644 --- a/testsuite/tests/typecheck/should_fail/T8142.stderr +++ b/testsuite/tests/typecheck/should_fail/T8142.stderr @@ -1,10 +1,24 @@ -T8142.hs:6:57: - Couldn't match type ‘Nu ((,) t0)’ with ‘g0 (Nu ((,) t0))’ - The type variables ‘t0’, ‘g0’ are ambiguous - Expected type: Nu ((,) t0) -> (t0, g0 (Nu ((,) t0))) - Actual type: Nu ((,) t0) -> (t0, Nu ((,) t0)) +T8142.hs:6:18: error: + Couldn't match type ‘Nu g0’ with ‘Nu g’ + NB: ‘Nu’ is a type function, and may not be injective + The type variable ‘g0’ is ambiguous + Expected type: Nu ((,) t) -> Nu g + Actual type: Nu ((,) t0) -> Nu g0 + When checking that ‘h’ has the inferred type + h :: forall t (g :: * -> *). Nu ((,) t) -> Nu g + Probable cause: the inferred type is ambiguous + In an equation for ‘tracer’: + tracer + = h + where + h = (\ (_, b) -> ((outI . fmap h) b)) . out + +T8142.hs:6:57: error: + Couldn't match type ‘Nu ((,) t)’ with ‘g (Nu ((,) t))’ + Expected type: Nu ((,) t) -> (t, g (Nu ((,) t))) + Actual type: Nu ((,) t) -> (t, Nu ((,) t)) Relevant bindings include - h :: Nu ((,) t0) -> Nu g0 (bound at T8142.hs:6:18) + h :: Nu ((,) t) -> Nu g (bound at T8142.hs:6:18) In the second argument of ‘(.)’, namely ‘out’ In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out diff --git a/testsuite/tests/typecheck/should_fail/T8262.stderr b/testsuite/tests/typecheck/should_fail/T8262.stderr index cfaf5adafa..5d77a6cb4a 100644 --- a/testsuite/tests/typecheck/should_fail/T8262.stderr +++ b/testsuite/tests/typecheck/should_fail/T8262.stderr @@ -1,5 +1,5 @@ -T8262.hs:5:15: +T8262.hs:5:15: error: Couldn't match kind ‘*’ with ‘#’ When matching types a :: * diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr index 8e39968aac..2aaf55b3ff 100644 --- a/testsuite/tests/typecheck/should_fail/T8603.stderr +++ b/testsuite/tests/typecheck/should_fail/T8603.stderr @@ -1,30 +1,21 @@ -
-T8603.hs:13:10:
- No instance for (Applicative RV)
- arising from the superclasses of an instance declaration
- In the instance declaration for ‘Monad RV’
-
-T8603.hs:29:17:
- Couldn't match kind ‘* -> *’ with ‘*’
- When matching types
- t1 :: (* -> *) -> * -> *
- (->) :: * -> * -> *
- Expected type: [Integer] -> StateT s RV t0
- Actual type: t1 ((->) [a0]) (StateT s RV t0)
- The function ‘lift’ is applied to two arguments,
- but its type ‘([a0] -> StateT s RV t0)
- -> t1 ((->) [a0]) (StateT s RV t0)’
- has only one
- In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
- In the expression:
- do { prize <- lift uniform [1, 2, ....];
- return False }
-
-T8603.hs:29:22:
- Couldn't match type ‘RV a0’ with ‘StateT s RV t0’
- Expected type: [a0] -> StateT s RV t0
- Actual type: [a0] -> RV a0
- Relevant bindings include
- testRVState1 :: RVState s Bool (bound at T8603.hs:28:1)
- In the first argument of ‘lift’, namely ‘uniform’
- In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
+ +T8603.hs:13:10: error: + No instance for (Applicative RV) + arising from the superclasses of an instance declaration + In the instance declaration for ‘Monad RV’ + +T8603.hs:29:17: error: + Couldn't match kind ‘* -> *’ with ‘*’ + When matching types + t1 :: (* -> *) -> * -> * + (->) :: * -> * -> * + Expected type: [Integer] -> StateT s RV t0 + Actual type: t1 ((->) [a0]) (StateT s RV t0) + The function ‘lift’ is applied to two arguments, + but its type ‘([a0] -> StateT s RV t0) + -> t1 ((->) [a0]) (StateT s RV t0)’ + has only one + In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3] + In the expression: + do { prize <- lift uniform [1, 2, ....]; + return False } diff --git a/testsuite/tests/typecheck/should_fail/T9612.stderr b/testsuite/tests/typecheck/should_fail/T9612.stderr index 823fee112c..bffceb0baa 100644 --- a/testsuite/tests/typecheck/should_fail/T9612.stderr +++ b/testsuite/tests/typecheck/should_fail/T9612.stderr @@ -1,5 +1,5 @@ -T9612.hs:16:9: +T9612.hs:16:9: error: Couldn't match type ‘[(Int, a)]’ with ‘(Int, a)’ arising from a functional dependency between: constraint ‘MonadWriter (Int, a) (WriterT [(Int, a)] Identity)’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 110f29f465..faca0791a4 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -278,6 +278,7 @@ test('T6022', normal, compile_fail, ['']) test('T5853', normal, compile_fail, ['']) test('T6078', normal, compile_fail, ['']) test('FDsFromGivens', normal, compile_fail, ['']) +test('FDsFromGivens2', normal, compile_fail, ['']) test('T7019', normal, compile_fail,['']) test('T7019a', normal, compile_fail,['']) test('T5978', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_fail/mc25.stderr b/testsuite/tests/typecheck/should_fail/mc25.stderr index 83fe1301d6..ec88439e89 100644 --- a/testsuite/tests/typecheck/should_fail/mc25.stderr +++ b/testsuite/tests/typecheck/should_fail/mc25.stderr @@ -1,5 +1,5 @@ -mc25.hs:9:10: +mc25.hs:9:10: error: No instance for (Functor t1) arising from a use of ‘fmap’ Possible fix: add (Functor t1) to the context of @@ -9,7 +9,7 @@ mc25.hs:9:10: In a stmt of a monad comprehension: then group by x using take In the expression: [x | x <- [1 .. 10], then group by x using take] -mc25.hs:9:46: +mc25.hs:9:46: error: Couldn't match type ‘a -> t’ with ‘Int’ Expected type: (a -> t) -> [a] -> [t1 a] Actual type: Int -> [t1 a] -> [t1 a] diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr index 37f96659cc..6c6f97d932 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr @@ -1,5 +1,5 @@ -tcfail090.hs:11:9: +tcfail090.hs:11:9: error: Couldn't match kind ‘*’ with ‘#’ When matching types a0 :: * diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr index 6ad75f49ca..fdd444d1fc 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr @@ -1,5 +1,5 @@ -tcfail122.hs:8:9: +tcfail122.hs:8:9: error: Couldn't match kind ‘* -> *’ with ‘*’ When matching types c0 :: (* -> *) -> * diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr index 9f5cc09bdf..396d63c9f8 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr @@ -1,5 +1,5 @@ -tcfail123.hs:11:9: +tcfail123.hs:11:9: error: Couldn't match kind ‘*’ with ‘#’ When matching types t0 :: * diff --git a/testsuite/tests/typecheck/should_fail/tcfail143.stderr b/testsuite/tests/typecheck/should_fail/tcfail143.stderr index b36d7a8b37..7c26762a66 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail143.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail143.stderr @@ -1,8 +1,8 @@ -tcfail143.hs:29:9: - Couldn't match type ‘S Z’ with ‘Z’ +tcfail143.hs:29:9: error: + Couldn't match type ‘Z’ with ‘S Z’ arising from a functional dependency between: constraint ‘MinMax (S Z) Z Z Z’ arising from a use of ‘extend’ - instance ‘MinMax a Z Z a’ at tcfail143.hs:11:10-23 + instance ‘MinMax Z b Z b’ at tcfail143.hs:12:10-23 In the expression: n1 `extend` n0 In an equation for ‘t2’: t2 = n1 `extend` n0 diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr index a8ae57b510..48c4ceb406 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr @@ -1,5 +1,5 @@ -tcfail159.hs:9:11: +tcfail159.hs:9:11: error: Couldn't match kind ‘*’ with ‘#’ When matching types t0 :: * diff --git a/testsuite/tests/typecheck/should_fail/tcfail200.stderr b/testsuite/tests/typecheck/should_fail/tcfail200.stderr index 473ff9ebd7..e5bb82267e 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail200.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail200.stderr @@ -1,5 +1,5 @@ -tcfail200.hs:5:15: +tcfail200.hs:5:15: error: Couldn't match kind ‘*’ with ‘#’ When matching types t1 :: * diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr index a69906452c..f548f0e72c 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr @@ -1,6 +1,6 @@ -tcfail201.hs:17:58: - Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’ +tcfail201.hs:17:58: error: + Couldn't match expected type ‘a’ with actual type ‘HsDoc t0’ ‘a’ is a rigid type variable bound by the type signature for: gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b) |