Skip to content

Commit

Permalink
Numerous small changes to the constraint solver
Browse files Browse the repository at this point in the history 
The main thing is that we now keep unsolved Derived constraints in the
wc_flats of a WantedConstraints, rather than discarding them each time.
This actually fixes a poential (admittedly obscure) bug, when we currently
discard a superclass constraint, and may never re-generate it, and may
thereby miss a functional dependency.

Instead, reportErrors filters out Derived constraints that we don't want
to report.

The other changes are all small refactorings following our walk-through.
  • Loading branch information
Simon Peyton Jones committed Jul 23, 2012
1 parent 606b6d5 commit 9c0a6bb
Show file tree
Hide file tree
Showing 6 changed files with 228 additions and 332 deletions.
53 changes: 52 additions & 1 deletion compiler/typecheck/TcErrors.lhs
View file
Expand Up @@ -143,7 +143,8 @@ reportWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = implics }
where
env = cec_tidy ctxt
tidy_insols = mapBag (tidyCt env) insols
tidy_flats = mapBag (tidyCt env) flats
tidy_flats = mapBag (tidyCt env) (keepWanted flats)
-- See Note [Do not report derived but soluble errors]
reportTidyWanteds :: ReportErrCtxt -> Bag Ct -> Bag Ct -> Bag Implication -> TcM ()
reportTidyWanteds ctxt insols flats implics
Expand Down Expand Up @@ -372,6 +373,56 @@ getUserGivens (CEC {cec_encl = ctxt})
, not (null givens) ]
\end{code}

Note [Do not report derived but soluble errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The wc_flats include Derived constraints that have not been solved, but are
not insoluble (in that case they'd be in wc_insols). We do not want to report
these as errors:

* Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
an unsolved [D] Eq a, and we do not want to report that; it's just noise.

* Functional dependencies. For givens, consider
class C a b | a -> b
data T a where
MkT :: C a d => [d] -> T a
f :: C a b => T a -> F Int
f (MkT xs) = length xs
Then we get a [D] b~d. But there *is* a legitimate call to
f, namely f (MkT [True]) :: T Bool, in which b=d. So we should
not reject the program.

For wanteds, something similar
data T a where
MkT :: C Int b => a -> b -> T a
g :: C Int c => c -> ()
f :: T a -> ()
f (MkT x y) = g x
Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
But again f (MkT True True) is a legitimate call.

(We leave the Deriveds in wc_flat until reportErrors, so that we don't lose
derived superclasses between iterations of the solver.)

For functional dependencies, here is a real example,
stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs

class C a b | a -> b
g :: C a b => a -> b -> ()
f :: C a b => a -> b -> ()
f xa xb =
let loop = g xa
in loop xb

We will first try to infer a type for loop, and we will succeed:
C a b' => b' -> ()
Subsequently, we will type check (loop xb) and all is good. But,
recall that we have to solve a final implication constraint:
C a b => (C a b' => .... cts from body of loop .... ))
And now we have a problem as we will generate an equality b ~ b' and fail to
solve it.


%************************************************************************
%* *
Irreducible predicate errors
Expand Down
50 changes: 18 additions & 32 deletions compiler/typecheck/TcHsSyn.lhs
View file
Expand Up @@ -1158,26 +1158,25 @@ zonkEvBinds env binds
zonkEvBind :: ZonkEnv -> EvBind -> TcM EvBind
zonkEvBind env (EvBind var term)
-- This function has some special cases for avoiding re-zonking the
-- same types many types. See Note [Optimized Evidence Binding Zonking]
= case term of
-- Fast path for reflexivity coercions:
-- Special-case fast paths for small coercions
-- NB: could be optimized further! (e.g. SymCo cv)
-- See Note [Optimized Evidence Binding Zonking]
EvCoercion co
| Just ty <- isTcReflCo_maybe co
->
do { zty <- zonkTcTypeToType env ty
; let var' = setVarType var (mkEqPred zty zty)
; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
-> do { zty <- zonkTcTypeToType env ty
; let var' = setVarType var (mkEqPred zty zty)
-- Here we save the task of zonking var's type,
-- because we know just what it is!
; return (EvBind var' (EvCoercion (mkTcReflCo zty))) }
-- Fast path for variable-variable bindings
-- NB: could be optimized further! (e.g. SymCo cv)
| Just cv <- getTcCoVar_maybe co
-> do { let cv' = zonkIdOcc env cv -- Just lazily look up
term' = EvCoercion (TcCoVarCo cv')
var' = setVarType var (varType cv')
; return (EvBind var' term') }
-- Ugly safe and slow path
-- The default path
_ -> do { var' <- {-# SCC "zonkEvBndr" #-} zonkEvBndr env var
; term' <- zonkEvTerm env term
; return (EvBind var' term')
Expand Down Expand Up @@ -1238,29 +1237,16 @@ not the ill-kinded Any BOX).

Note [Optimized Evidence Binding Zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

When optimising evidence binds we may come accross situations where
a coercion is just reflexivity:
When optimising evidence binds we may come across situations where
a coercion looks like
cv = ReflCo ty
In such a case it is a waste of time to zonk both ty and the type
of the coercion, especially if the types involved are huge. For this
reason this case is optimized to only zonk 'ty' and set the type of
the variable to be that zonked type.

Another case that hurts a lot are simple coercion bindings of the form:
cv1 = cv2
cv3 = cv1
cv4 = cv2
etc. In all such cases it is very easy to just get the zonked type of
cv2 and use it to set the type of the LHS coercion variable without zonking
twice. Though this case is funny, it can happen due the way that evidence
from spontaneously solved goals is now used.
See Note [Optimizing Spontaneously Solved Goals] about this.

NB: That these optimizations are independently useful, regardless of the
constraint solver strategy.

DV, TODO: followup on this note mentioning new examples I will add to perf/
or cv1 = cv2
where the type 'ty' is big. In such cases it is a waste of time to zonk both
* The variable on the LHS
* The coercion on the RHS
Rather, we can zonk the coercion, take its type and use that for
the variable. For big coercions this might be a lose, though, so we
just have a fast case for a couple of special cases.


\begin{code}
Expand Down
192 changes: 68 additions & 124 deletions compiler/typecheck/TcInteract.lhs
View file
Expand Up @@ -47,7 +47,6 @@ import Control.Monad ( foldM )
import VarEnv
import qualified Data.Traversable as Traversable
import Data.Maybe ( isJust )
import Control.Monad( when, unless )
import Pair ()
Expand Down Expand Up @@ -763,19 +762,6 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
, cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 })
wi@(CFunEqCan { cc_ev = fl2, cc_fun = tc2
, cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
{- ToDo: Check with Dimitrios
| lhss_match
, isSolved fl1 -- Inert is solved and we can simply ignore it
-- when workitem is given/solved
, isGiven fl2
= irInertConsumed "FunEq/FunEq"
| lhss_match
, isSolved fl2 -- Workitem is solved and we can ignore it when
-- the inert is given/solved
, isGiven fl1
= irWorkItemConsumed "FunEq/FunEq"
-}
| fl1 `canSolve` fl2 && lhss_match
= do { traceTcS "interact with inerts: FunEq/FunEq" $
vcat [ text "workItem =" <+> ppr wi
Expand Down Expand Up @@ -934,12 +920,6 @@ solveOneFromTheOther info ifl workItem
-- so it's safe to continue on from this point
= irInertConsumed ("Solved[DI] " ++ info)
{- ToDo: Check with Dimitrios
| isSolved ifl, isGiven wfl
-- Same if the inert is a GivenSolved -- just get rid of it
= irInertConsumed ("Solved[SI] " ++ info)
-}
| otherwise
= ASSERT( ifl `canSolve` wfl )
-- Because of Note [The Solver Invariant], plus Derived dealt with
Expand Down Expand Up @@ -1443,16 +1423,32 @@ doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
-- (b) See Note [Given constraint that matches an instance declaration]
-- for some design decisions for given dictionaries.
doTopReact inerts workItem@(CDictCan { cc_ev = fl
, cc_class = cls, cc_tyargs = xis, cc_depth = depth })
doTopReact inerts workItem
= do { traceTcS "doTopReact" (ppr workItem)
; instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs (mkClassPred cls xis, arising_sdoc)
; case workItem of
CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
, cc_depth = d }
-> doTopReactDict inerts workItem fl cls xis d
CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
, cc_rhs = xi, cc_depth = d }
-> doTopReactFunEq fl tc args xi d
_ -> -- Any other work item does not react with any top-level equations
return NoTopInt }
--------------------
doTopReactDict :: InertSet -> WorkItem -> CtEvidence -> Class -> [Xi]
-> SubGoalDepth -> TcS TopInteractResult
doTopReactDict inerts workItem fl cls xis depth
= do { instEnvs <- getInstEnvs
; let fd_eqns = improveFromInstEnv instEnvs
(mkClassPred cls xis, arising_sdoc)
; m <- rewriteWithFunDeps fd_eqns xis fl
; case m of
Just (_xis',fd_work) ->
do { emitFDWorkAsDerived fd_work (cc_depth workItem)
do { emitFDWorkAsDerived fd_work depth
; return SomeTopInt { tir_rule = "Dict/Top (fundeps)"
, tir_new_item = ContinueWith workItem } }
Nothing
Expand Down Expand Up @@ -1493,106 +1489,54 @@ doTopReact inerts workItem@(CDictCan { cc_ev = fl
SomeTopInt { tir_rule = "Dict/Top (solved, more work)"
, tir_new_item = Stop } }
-- Otherwise, it's a Given, Derived, or Wanted
doTopReact _inerts workItem@(CFunEqCan { cc_ev = fl, cc_depth = d
, cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
= ASSERT (isSynFamilyTyCon tc) -- No associated data families have reached that far
--------------------
doTopReactFunEq :: CtEvidence -> TyCon -> [Xi] -> Xi
-> SubGoalDepth -> TcS TopInteractResult
doTopReactFunEq fl tc args xi d
= ASSERT (isSynFamilyTyCon tc) -- No associated data families have
-- reached that far
-- First look in the cache of solved funeqs
do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
; case lookupFamHead fun_eq_cache (mkTyConApp tc args) of {
Just ctev -> ASSERT( not (isDerived ctev) )
ASSERT( isEqPred (ctEvPred ctev) )
succeed_with (evTermCoercion (ctEvTerm ctev))
(snd (getEqPredTys (ctEvPred ctev))) ;
Nothing ->
-- No cached solved, so look up in top-level instances
do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
; case match_res of
Nothing -> return NoTopInt
Just (famInst, rep_tys)
-> do { mb_already_solved <- lkpSolvedFunEqCache (mkTyConApp tc args)
; traceTcS "doTopReact: Family instance matches" $
vcat [ text "solved-fun-cache" <+> if isJust mb_already_solved
then text "hit" else text "miss"
, text "workItem =" <+> ppr workItem ]
; let (coe,rhs_ty)
| Just ctev <- mb_already_solved
, not (isDerived ctev)
= ASSERT( isEqPred (ctEvPred ctev) )
(evTermCoercion (ctEvTerm ctev), snd (getEqPredTys (ctEvPred ctev)))
| otherwise
= let coe_ax = famInstAxiom famInst
in (mkTcAxInstCo coe_ax rep_tys,
mkAxInstRHS coe_ax rep_tys)
xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
xcomp _ = panic "No more goals!"
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
; case ctevs of
[ctev] -> updWorkListTcS $ extendWorkListEq $
CNonCanonical { cc_ev = ctev
, cc_depth = d+1 }
ctevs -> -- No subgoal (because it's cached)
ASSERT( null ctevs) return ()
; unless (isDerived fl) $
do { addSolvedFunEq fl
; addToSolved fl }
; return $ SomeTopInt { tir_rule = "Fun/Top"
, tir_new_item = Stop } } }
-- Any other work item does not react with any top-level equations
doTopReact _inerts _workItem = return NoTopInt
lkpSolvedFunEqCache :: TcType -> TcS (Maybe CtEvidence)
lkpSolvedFunEqCache fam_head
= do { (_subst,_inscope) <- getInertEqs
; fun_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
; traceTcS "lkpFunEqCache" $ vcat [ text "fam_head =" <+> ppr fam_head
, text "funeq cache =" <+> ppr fun_cache ]
; return (lookupFamHead fun_cache fam_head) }
{- ToDo; talk to Dimitrios. I have no idea what is happening here
; rewrite_cached (lookupFamHead fun_cache fam_head) }
-- The two different calls do not seem to make a significant difference in
-- terms of hit/miss rate for many memory-critical/performance tests but the
-- latter blows up the space on the heap somehow ... It maybe the niFixTvSubst.
-- So, I am simply disabling it for now, until we investigate a bit more.
-- lookupTypeMap_mod subst cc_rhs fam_head (unCtFamHeadMap fun_cache) }
where rewrite_cached Nothing = return Nothing
rewrite_cached (Just ct@(CFunEqCan { cc_ev = fl, cc_depth = d
, cc_fun = tc, cc_tyargs = xis
, cc_rhs = xi}))
= do { (xis_subst,cos) <- flattenMany d FMFullFlatten fl xis
-- cos :: xis_subst ~ xis
; (xi_subst,co) <- flatten d FMFullFlatten fl xi
-- co :: xi_subst ~ xi
; let flat_fam_head = mkTyConApp tc xis_subst
; unless (flat_fam_head `eqType` fam_head) $
pprPanic "lkpFunEqCache" (vcat [ text "Cached (solved) constraint =" <+> ppr ct
, text "Flattened constr. head =" <+> ppr flat_fam_head ])
; traceTcS "lkpFunEqCache" $ text "Flattened constr. rhs = " <+> ppr xi_subst
; let new_pty = mkTcEqPred (mkTyConApp tc xis_subst) xi_subst
new_co = mkTcTyConAppCo eqTyCon [ mkTcReflCo (defaultKind $ typeKind xi_subst)
, mkTcTyConAppCo tc cos
, co ]
-- new_co :: (F xis_subst ~ xi_subst) ~ (F xis ~ xi)
-- new_co = (~) <k> (F cos) co
; new_fl <- rewriteCtFlavor fl new_pty new_co
; case new_fl of
Nothing
-> return Nothing -- Strange: cached?
Just fl'
-> return $
Just (CFunEqCan { cc_ev = fl'
, cc_depth = d
, cc_fun = tc
, cc_tyargs = xis_subst
, cc_rhs = xi_subst }) }
rewrite_cached (Just other_ct)
= pprPanic "lkpFunEqCache:not family equation!" $ ppr other_ct
-}
; case match_res of {
Nothing -> return NoTopInt ;
Just (famInst, rep_tys) ->
-- Found a top-level instance
do { -- Add it to the solved goals
unless (isDerived fl) $
do { addSolvedFunEq fl
; addToSolved fl }
; let coe_ax = famInstAxiom famInst
; succeed_with (mkTcAxInstCo coe_ax rep_tys)
(mkAxInstRHS coe_ax rep_tys) } } } } }
where
succeed_with :: TcCoercion -> TcType -> TcS TopInteractResult
succeed_with coe rhs_ty
= do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
; case ctevs of
[ctev] -> updWorkListTcS $ extendWorkListEq $
CNonCanonical { cc_ev = ctev
, cc_depth = d+1 }
ctevs -> -- No subgoal (because it's cached)
ASSERT( null ctevs) return ()
; return $ SomeTopInt { tir_rule = "Fun/Top"
, tir_new_item = Stop } }
where
xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
xcomp _ = panic "No more goals!"
xev = XEvTerm xcomp xdecomp
\end{code}


Expand Down

0 comments on commit 9c0a6bb

Please sign in to comment.