Commit a1275a76 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

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.
parent d9bb0ee7
...@@ -252,26 +252,24 @@ emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls ...@@ -252,26 +252,24 @@ emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls
; continueWith ct } ; continueWith ct }
emitSuperclasses _ = panic "emit_superclasses of non-class!" emitSuperclasses _ = panic "emit_superclasses of non-class!"
{- {- Note [Adding superclasses]
Note [Adding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~
Since dictionaries are canonicalized only once in their lifetime, the Since dictionaries are canonicalized only once in their lifetime, the
place to add their superclasses is canonicalisation. See Note [Add place to add their superclasses is canonicalisation. See Note [Add
superclasses only during canonicalisation]. Here is what we do: superclasses only during canonicalisation]. Here is what we do:
Deriveds: Do nothing.
Givens: Add all their superclasses as Givens. Givens: Add all their superclasses as Givens.
They may be needed to prove Wanteds
Wanteds: Do nothing.
Wanteds: Add all their superclasses as Derived. Deriveds: Add all their superclasses as Derived.
Not as Wanted: we don't need a proof. The sole reason is to expose functional dependencies
Nor as Given: that leads to superclass loops. in superclasses or equality superclasses.
We also want to ensure minimal constraints to quantify over. For We only do this in the improvement phase, if solving has
instance, if our wanted constraint is (Eq a, Ord a) we'd only like to not succeeded; see Note [The improvement story] in
quantify over Ord a. But we deal with that completely independently TcInteract
in TcSimplify. See Note [Minimize by SuperClasses] in TcSimplify.
Examples of how adding superclasses as Derived is useful Examples of how adding superclasses as Derived is useful
...@@ -292,6 +290,7 @@ 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 [D] F a ~ beta
Now we we get [D] beta ~ b, and can solve that. 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 Example of why adding superclass of a Wanted as a Given would
be terrible, see Note [Do not add superclasses of solved dictionaries] be terrible, see Note [Do not add superclasses of solved dictionaries]
in TcSMonad, which has this example: in TcSMonad, which has this example:
...@@ -348,21 +347,18 @@ situation can't happen. ...@@ -348,21 +347,18 @@ situation can't happen.
newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS () newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
-- Returns superclasses, see Note [Adding superclasses] -- Returns superclasses, see Note [Adding superclasses]
newSCWorkFromFlavored flavor cls xis newSCWorkFromFlavored flavor cls xis
| isDerived flavor | CtWanted {} <- flavor
= return () -- Deriveds don't yield more superclasses because we will = return ()
-- add them transitively in the case of wanteds.
| CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
= do { let sc_theta = immSuperClasses cls xis = do { given_evs <- newGivenEvVars loc (mkEvScSelectors (EvId evar) cls xis)
mk_pr sc_pred i = (sc_pred, EvSuperClass (EvId evar) i)
; given_evs <- newGivenEvVars loc (zipWith mk_pr sc_theta [0..])
; emitWorkNC given_evs } ; emitWorkNC given_evs }
| isEmptyVarSet (tyVarsOfTypes xis) | isEmptyVarSet (tyVarsOfTypes xis)
= return () -- Wanteds with no variables yield no deriveds. = return () -- Wanteds with no variables yield no deriveds.
-- See Note [Improvement from Ground Wanteds] -- 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 = do { let sc_rec_theta = transSuperClasses cls xis
impr_theta = filter isImprovementPred sc_rec_theta impr_theta = filter isImprovementPred sc_rec_theta
loc = ctEvLoc flavor loc = ctEvLoc flavor
......
...@@ -1807,11 +1807,10 @@ simplifyDeriv pred tvs theta ...@@ -1807,11 +1807,10 @@ simplifyDeriv pred tvs theta
; traceTc "simplifyDeriv" $ ; traceTc "simplifyDeriv" $
vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ] vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
; (residual_wanted, _ev_binds1) ; residual_wanted <- solveWantedsTcM wanted
<- solveWantedsTcM (mkSimpleWC wanted)
-- Post: residual_wanted are already zonked
; 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] -- See Note [Exotic derived instance contexts]
get_good :: Ct -> Either PredType Ct get_good :: Ct -> Either PredType Ct
get_good ct | validDerivPred skol_set p get_good ct | validDerivPred skol_set p
......
...@@ -126,23 +126,25 @@ report_unsolved :: Maybe EvBindsVar -- cec_binds ...@@ -126,23 +126,25 @@ report_unsolved :: Maybe EvBindsVar -- cec_binds
-> HoleChoice -- Expression holes -> HoleChoice -- Expression holes
-> HoleChoice -- Type holes -> HoleChoice -- Type holes
-> WantedConstraints -> TcM () -> 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 report_unsolved mb_binds_var defer_errors expr_holes type_holes wanted
| isEmptyWC wanted | isEmptyWC wanted
= return () = return ()
| otherwise | otherwise
= do { traceTc "reportUnsolved (before unflattening)" (ppr wanted) = do { traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
; warn_redundant <- woptM Opt_WarnRedundantConstraints
; wanted <- zonkWC wanted -- Zonk to reveal all information
; env0 <- tcInitTidyEnv ; env0 <- tcInitTidyEnv
-- If we are deferring we are going to need /all/ evidence around, -- If we are deferring we are going to need /all/ evidence around,
-- including the evidence produced by unflattening (zonkWC) -- including the evidence produced by unflattening (zonkWC)
; let tidy_env = tidyFreeTyVars env0 free_tvs ; let tidy_env = tidyFreeTyVars env0 free_tvs
free_tvs = tyVarsOfWC wanted 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_tidy = tidy_env
, cec_defer_type_errors = defer_errors , cec_defer_type_errors = defer_errors
, cec_expr_holes = expr_holes , cec_expr_holes = expr_holes
...@@ -151,10 +153,6 @@ report_unsolved mb_binds_var defer_errors expr_holes type_holes wanted ...@@ -151,10 +153,6 @@ report_unsolved mb_binds_var defer_errors expr_holes type_holes wanted
, cec_warn_redundant = warn_redundant , cec_warn_redundant = warn_redundant
, cec_binds = mb_binds_var } , cec_binds = mb_binds_var }
; traceTc "reportUnsolved (after unflattening):" $
vcat [ pprTvBndrs (varSetElems free_tvs)
, ppr wanted ]
; reportWanteds err_ctxt wanted } ; reportWanteds err_ctxt wanted }
-------------------------------------------- --------------------------------------------
...@@ -286,72 +284,76 @@ This only matters in instance declarations.. ...@@ -286,72 +284,76 @@ This only matters in instance declarations..
reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM () reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics }) reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
= do { ctxt1 <- reportSimples ctxt (mapBag (tidyCt env) insol_given) = do { traceTc "reportWanteds" (vcat [ ptext (sLit "Simples =") <+> ppr simples
; ctxt2 <- reportSimples ctxt1 (mapBag (tidyCt env) insol_wanted) , 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 -- For the simple wanteds, suppress them if there are any
-- insolubles in the tree, to avoid unnecessary clutter -- insolubles in the tree, to avoid unnecessary clutter
; let ctxt2' = ctxt { cec_suppress = cec_suppress ctxt2 ; let ctxt2' = ctxt { cec_suppress = cec_suppress ctxt2
|| anyBag insolubleImplic implics } || 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 -- All the Derived ones have been filtered out of simples
-- by the constraint solver. This is ok; we don't want -- by the constraint solver. This is ok; we don't want
-- to report unsolved Derived goals as errors -- to report unsolved Derived goals as errors
-- See Note [Do not report derived but soluble 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 -- NB ctxt1: don't suppress inner insolubles if there's only a
-- wanted insoluble here; but do suppress inner insolubles -- wanted insoluble here; but do suppress inner insolubles
-- if there's a *given* insoluble here (= inaccessible code) -- if there's a *given* insoluble here (= inaccessible code)
where where
env = cec_tidy ctxt env = cec_tidy ctxt
(insol_given, insol_wanted) = partitionBag isGivenCt insols insol_given = [ ("insoluble1", is_given &&& utterly_wrong, True, mkGroupReporter mkEqErr)
, ("insoluble2", is_given &&& is_equality, True, mkSkolReporter) ]
reportSimples :: ReportErrCtxt -> Cts -> TcM ReportErrCtxt insol_wanted = [ ("insoluble3", utterly_wrong, True, mkGroupReporter mkEqErr)
reportSimples ctxt simples -- Here 'simples' includes insolble goals , ("insoluble4", is_equality, True, mkSkolReporter) ]
= 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
utterly_wrong_given ct (EqPred _ ty1 ty2) reporters = [ ("Holes", is_hole, False, mkHoleReporter)
| isGivenCt ct = isRigid ty1 && isRigid ty2
utterly_wrong_given _ _ = False
utterly_wrong_other _ (EqPred _ ty1 ty2) = isRigid ty1 && isRigid ty2 -- Report equalities of form (a~ty). They are usually
utterly_wrong_other _ _ = False -- 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 is_hole ct _ = isHoleCt ct
skolem_eq _ _ = False
is_equality _ (EqPred {}) = True is_given ct _ = not (isWantedCt ct) -- The Derived ones are actually all from Givens
is_equality _ _ = False 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 _ (ClassPred {}) = True
is_dict _ _ = False is_dict _ _ = False
...@@ -363,6 +365,10 @@ reportSimples ctxt simples -- Here 'simples' includes insolble goals ...@@ -363,6 +365,10 @@ reportSimples ctxt simples -- Here 'simples' includes insolble goals
is_irred _ _ = False is_irred _ _ = False
-- isRigidEqPred :: PredTree -> Bool
-- isRigidEqPred (EqPred NomEq ty1 ty2) = isRigid ty1 && isRigid ty2
-- isRigidEqPred _ = False
--------------- ---------------
isRigid, isRigidOrSkol :: Type -> Bool isRigid, isRigidOrSkol :: Type -> Bool
isRigid ty isRigid ty
...@@ -499,32 +505,33 @@ maybeAddDeferredBinding ctxt err ct ...@@ -499,32 +505,33 @@ maybeAddDeferredBinding ctxt err ct
| otherwise | otherwise
= return () = 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 -- Use the first reporter in the list whose predicate says True
tryReporters ctxt reporters cts tryReporters ctxt reporters cts
= do { traceTc "tryReporters {" (ppr cts) = do { traceTc "tryReporters {" (ppr cts)
; ctxt' <- go ctxt reporters cts ; (ctxt', cts') <- go ctxt reporters cts
; traceTc "tryReporters }" empty ; traceTc "tryReporters }" (ppr cts')
; return ctxt' } ; return (ctxt', cts') }
where where
go ctxt [] cts go ctxt [] cts
| null cts = return ctxt = return (ctxt, cts)
| otherwise = pprPanic "tryReporters" (ppr cts)
go ctxt (r : rs) cts
go ctxt ((str, pred, suppress_after, reporter) : rs) cts = do { (ctxt', cts') <- tryReporter ctxt r cts
| null yeses = do { traceTc "tryReporters: no" (text str) ; go ctxt' rs cts' }
; go ctxt rs cts } -- Carry on with the rest, because we must make
| otherwise = do { traceTc "tryReporters: yes" (text str <+> ppr yeses) -- deferred bindings for them if we have -fdefer-type-errors
; reporter ctxt yeses :: TcM () -- But suppress their error messages
; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
; go ctxt' rs nos } tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
-- Carry on with the rest, because we must make tryReporter ctxt (str, keep_me, suppress_after, reporter) cts
-- deferred bindings for them if we have | null yeses = return (ctxt, cts)
-- -fdefer-type-errors | otherwise = do { traceTc "tryReporter:" (text str <+> ppr yeses)
-- But suppress their error messages ; reporter ctxt yeses
where ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
(yeses, nos) = partition keep_me cts ; return (ctxt', nos) }
keep_me ct = pred ct (classifyPredType (ctPred ct)) where
(yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
-- Add the "arising from..." part to a message about bunch of dicts -- Add the "arising from..." part to a message about bunch of dicts
addArising :: CtOrigin -> SDoc -> SDoc addArising :: CtOrigin -> SDoc -> SDoc
......
...@@ -235,52 +235,6 @@ Solution: always put fmvs on the left, so we get ...@@ -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. 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 ...@@ -1570,9 +1524,12 @@ ctFlavourRole = ctEvFlavourRole . cc_ev
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
-- Very important function! -- Very important function!
-- See Note [eqCanRewrite] -- See Note [eqCanRewrite]
eqCanRewriteFR (Given, NomEq) (_, _) = True -- See Note [Wanteds do not rewrite Wanteds]
eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True -- See Note [Deriveds do rewrite Deriveds]
eqCanRewriteFR _ _ = False eqCanRewriteFR (Given, NomEq) (_, _) = True
eqCanRewriteFR (Given, ReprEq) (_, ReprEq) = True
eqCanRewriteFR (Derived, NomEq) (Derived, _) = True
eqCanRewriteFR _ _ = False
canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool canRewriteOrSame :: CtEvidence -> CtEvidence -> Bool
-- See Note [canRewriteOrSame] -- See Note [canRewriteOrSame]
...@@ -1582,15 +1539,20 @@ canRewriteOrSame ev1 ev2 = ev1 `eqCanRewrite` ev2 || ...@@ -1582,15 +1539,20 @@ canRewriteOrSame ev1 ev2 = ev1 `eqCanRewrite` ev2 ||
canRewriteOrSameFR :: CtFlavourRole -> CtFlavourRole -> Bool canRewriteOrSameFR :: CtFlavourRole -> CtFlavourRole -> Bool
canRewriteOrSameFR fr1 fr2 = fr1 `eqCanRewriteFR` fr2 || fr1 == fr2 canRewriteOrSameFR fr1 fr2 = fr1 `eqCanRewriteFR` fr2 || fr1 == fr2
{- {- Note [eqCanRewrite]
Note [eqCanRewrite]
~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~
(eqCanRewrite ct1 ct2) holds if the constraint ct1 (a CTyEqCan of form (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 tv ~ ty) can be used to rewrite ct2. It must satisfy the properties of
a can-rewrite relation, see Definition [Can-rewrite relation] a can-rewrite relation, see Definition [Can-rewrite relation]
At the moment we don't allow Wanteds to rewrite Wanteds, because that can give With the solver handling Coercible constraints like equality constraints,
rise to very confusing type error messages. A good example is Trac #8450. 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 Here's another
f :: a -> Bool f :: a -> Bool
f x = ( [x,'c'], [x,True] ) `seq` True f x = ( [x,'c'], [x,True] ) `seq` True
...@@ -1599,11 +1561,10 @@ Here we get ...@@ -1599,11 +1561,10 @@ Here we get
[W] a ~ Bool [W] a ~ Bool
but we do not want to complain about Bool ~ Char! but we do not want to complain about Bool ~ Char!
Accordingly, we also don't let Deriveds rewrite Deriveds. Note [Deriveds do rewrite Deriveds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With the solver handling Coercible constraints like equality constraints, However we DO allow Deriveds to rewrite Deriveds, because that's how
the rewrite conditions must take role into account, never allowing improvement works; see Note [The improvement story] in TcInteract.
a representational equality to rewrite a nominal one.
Note [canRewriteOrSame] Note [canRewriteOrSame]
~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~
...@@ -1636,6 +1597,9 @@ unflatten tv_eqs funeqs ...@@ -1636,6 +1597,9 @@ unflatten tv_eqs funeqs
, ptext (sLit "Tv eqs =") <+> pprCts tv_eqs ] , ptext (sLit "Tv eqs =") <+> pprCts tv_eqs ]
-- Step 1: unflatten the CFunEqCans, except if that causes an occurs check -- 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] -- See Note [Unflatten using funeqs first]
; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs ; funeqs <- foldrBagM (unflatten_funeq dflags) emptyCts funeqs
; traceTcS "Unflattening 1" $ braces (pprCts funeqs) ; traceTcS "Unflattening 1" $ braces (pprCts funeqs)
...@@ -1654,7 +1618,10 @@ unflatten tv_eqs funeqs ...@@ -1654,7 +1618,10 @@ unflatten tv_eqs funeqs
; let all_flat = tv_eqs `andCts` funeqs ; let all_flat = tv_eqs `andCts` funeqs
; traceTcS "Unflattening done" $ braces (pprCts all_flat) ; 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 where
---------------- ----------------
unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts unflatten_funeq :: DynFlags -> Ct -> Cts -> TcS Cts
...@@ -1731,7 +1698,7 @@ tryFill dflags tv rhs ev ...@@ -1731,7 +1698,7 @@ tryFill dflags tv rhs ev
OC_OK rhs'' -- Normal case: fill the tyvar OC_OK rhs'' -- Normal case: fill the tyvar
-> do { setEvBindIfWanted ev -> do { setEvBindIfWanted ev
(EvCoercion (mkTcReflCo (ctEvRole ev) rhs'')) (EvCoercion (mkTcReflCo (ctEvRole ev) rhs''))
; setWantedTyBind tv rhs'' ; unifyTyVar tv rhs''
; return True } ; return True }
_ -> -- Occurs check _ -> -- Occurs check
......
This diff is collapsed.
...@@ -62,7 +62,8 @@ module TcRnTypes( ...@@ -62,7 +62,8 @@ module TcRnTypes(
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols, andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
dropDerivedWC, insolubleImplic, trulyInsoluble, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
insolubleImplic, trulyInsoluble,
Implication(..), ImplicStatus(..), isInsolubleStatus, Implication(..), ImplicStatus(..), isInsolubleStatus,
SubGoalDepth, initialSubGoalDepth, SubGoalDepth, initialSubGoalDepth,
...@@ -1275,34 +1276,59 @@ ctEqRel = ctEvEqRel . ctEvidence ...@@ -1275,34 +1276,59 @@ ctEqRel = ctEvEqRel . ctEvidence
dropDerivedWC :: WantedConstraints -> WantedConstraints dropDerivedWC :: WantedConstraints -> WantedConstraints
-- See Note [Dropping derived constraints] -- See Note [Dropping derived constraints]
dropDerivedWC wc@(WC { wc_simple = simples }) dropDerivedWC wc@(WC { wc_simple = simples, wc_insol = insols })
= wc { wc_simple = filterBag isWantedCt simples } = wc { wc_simple = dropDerivedSimples simples
, wc_insol = dropDerivedInsols insols }
-- The wc_impl implications are already (recursively) filtered -- The wc_impl implications are already (recursively) filtered