Commit 9c0a6bbb authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Numerous small changes to the constraint solver

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.
parent 606b6d57
......@@ -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
......@@ -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
......
......@@ -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
-> 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')
......@@ -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}
......
......@@ -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 ()
......@@ -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
......@@ -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
......@@ -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
......@@ -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)
; case match_res of {
Nothing -> return NoTopInt ;
Just (famInst, rep_tys) ->
xdecomp x = [EvCoercion (mkTcSymCo coe `mkTcTransCo` evTermCoercion x)]
xcomp [x] = EvCoercion (coe `mkTcTransCo` evTermCoercion x)
xcomp _ = panic "No more goals!"
-- Found a top-level instance
do { -- Add it to the solved goals
unless (isDerived fl) $
do { addSolvedFunEq fl
; addToSolved fl }
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
; 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 ()
; 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
-}
, 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}
......
......@@ -857,7 +857,7 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num xi
cc_ev :: CtEvidence,
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_class :: Class,
cc_tyargs :: [Xi],
......@@ -866,7 +866,7 @@ data Ct
}
| CIrredEvCan { -- These stand for yet-unknown predicates
cc_ev :: CtEvidence,
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_ty :: Xi, -- cc_ty is flat hence it may only be of the form (tv xi1 xi2 ... xin)
-- Since, if it were a type constructor application, that'd make the
-- whole constraint a CDictCan, or CTyEqCan. And it can't be
......@@ -880,7 +880,7 @@ data Ct
-- * typeKind xi `compatKind` typeKind tv
-- See Note [Spontaneous solving and kind compatibility]
-- * We prefer unification variables on the left *JUST* for efficiency
cc_ev :: CtEvidence,
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_tyvar :: TcTyVar,
cc_rhs :: Xi,
......@@ -890,7 +890,7 @@ data Ct
| CFunEqCan { -- F xis ~ xi
-- Invariant: * isSynFamilyTyCon cc_fun
-- * typeKind (F xis) `compatKind` typeKind xi
cc_ev :: CtEvidence,
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
cc_fun :: TyCon, -- A type function
cc_tyargs :: [Xi], -- Either under-saturated or exactly saturated
cc_rhs :: Xi, -- *never* over-saturated (because if so
......@@ -904,9 +904,16 @@ data Ct
cc_ev :: CtEvidence,
cc_depth :: SubGoalDepth
}
\end{code}
Note [Ct/evidence invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If ct :: Ct, then extra fields of 'ct' cache precisely the ctev_pred field
of (cc_ev ct). Eg for CDictCan,
ctev_pred (cc_ev ct) = (cc_class ct) (cc_tyargs ct)
This holds by construction; look at the unique place where CDictCan is
built (in TcCanonical)
\begin{code}
mkNonCanonical :: CtEvidence -> Ct
mkNonCanonical flav = CNonCanonical { cc_ev = flav, cc_depth = 0}
......@@ -915,6 +922,7 @@ ctEvidence :: Ct -> CtEvidence
ctEvidence = cc_ev
ctPred :: Ct -> PredType
-- See Note [Ct/evidence invariant]
ctPred ct = ctEvPred (cc_ev ct)
keepWanted :: Cts -> Cts
......@@ -922,18 +930,6 @@ keepWanted = filterBag isWantedCt
-- DV: there used to be a note here that read:
-- ``Important: use fold*r*Bag to preserve the order of the evidence variables''
-- DV: Is this still relevant?
-- ToDo Check with Dimitrios
{-
ctPred (CNonCanonical { cc_ev = fl }) = ctEvPred fl
ctPred (CDictCan { cc_class = cls, cc_tyargs = xis })
= mkClassPred cls xis
ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
= mkTcEqPred (mkTyVarTy tv) xi
ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
= mkTcEqPred (mkTyConApp fn xis1) xi2
ctPred (CIrredEvCan { cc_ty = xi }) = xi
-}
\end{code}
......@@ -1197,6 +1193,12 @@ At the end, we will hopefully have substituted uf1 := F alpha, and we
will be able to report a more informative error:
'Can't construct the infinite type beta ~ F alpha beta'
Insoluble constraints *do* include Derived constraints. For example,
a functional dependency might give rise to [D] Int ~ Bool, and we must
report that. If insolubles did not contain Deriveds, reportErrors would
never see it.
%************************************************************************
%* *
Pretty printing
......@@ -1233,14 +1235,12 @@ ctev_evar; instead we look at the cte_pred field. The evtm/evar field
may be un-zonked.
\begin{code}
data CtEvidence -- Rename to CtEvidence
data CtEvidence
= Given { ctev_gloc :: GivenLoc
, ctev_pred :: TcPredType
, ctev_evtm :: EvTerm } -- See Note [Evidence field of CtEvidence]
-- Truly given, not depending on subgoals
-- NB: Spontaneous unifications belong here
-- DV TODOs: (i) Consider caching actual evidence _term_
-- (ii) Revisit Note [Optimizing Spontaneously Solved Coercions]
| Wanted { ctev_wloc :: WantedLoc
, ctev_pred :: TcPredType
......
......@@ -140,7 +140,7 @@ import Digraph
import Maybes ( orElse, catMaybes )
import Control.Monad( when, zipWithM )
import Control.Monad( unless, when, zipWithM )
import StaticFlags( opt_PprStyle_Debug )
import Data.IORef
import TrieMap
......@@ -171,7 +171,6 @@ mkKindErrorCtxtTcS ty1 ki1 ty2 ki2
Note [WorkList]
~~~~~~~~~~~~~~~
A WorkList contains canonical and non-canonical items (of all flavors).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.
......@@ -496,8 +495,10 @@ The reason for all this is simply to avoid re-solving goals we have solved alrea
* A solved Given is just given
* A solved Derived is possible; purpose is to avoid creating tons of identical
Derived goals.
* A solved Derived in inert_solved is possible; purpose is to avoid
creating tons of identical Derived goals.
But there are no solved Deriveds in inert_solved_funeqs
\begin{code}
......@@ -517,6 +518,8 @@ data InertSet
-- Not necessarily inert wrt top-level equations (or inert_cans)
, inert_solved_funeqs :: FamHeadMap CtEvidence -- Of form co :: F xis ~ xi
-- No Deriveds
, inert_solved :: PredMap CtEvidence -- All others
-- These two fields constitute a cache of solved (only!) constraints
-- See Note [Solved constraints]
......@@ -1123,11 +1126,16 @@ emitFrozenError :: CtEvidence -> SubGoalDepth -> TcS ()
emitFrozenError fl depth
= do { traceTcS "Emit frozen error" (ppr (ctEvPred fl))
; inert_ref <- getTcSInertsRef
; inerts <- wrapTcS (TcM.readTcRef inert_ref)
; let ct = CNonCanonical { cc_ev = fl
, cc_depth = depth }
inerts_new = inerts { inert_frozen = extendCts (inert_frozen inerts) ct }
; wrapTcS (TcM.writeTcRef inert_ref inerts_new) }
; wrapTcS $ do
{ inerts <- TcM.readTcRef inert_ref
; let old_insols = inert_frozen inerts
ct = CNonCanonical { cc_ev = fl, cc_depth = depth }
inerts_new = inerts { inert_frozen = extendCts old_insols ct }
this_pred = ctEvPred fl
already_there = not (isWanted fl) && anyBag (eqType this_pred . ctPred) old_insols
-- See Note [Do not add duplicate derived insolubles]
; unless already_there $
TcM.writeTcRef inert_ref inerts_new } }
instance HasDynFlags TcS where
getDynFlags = wrapTcS getDynFlags
......@@ -1184,52 +1192,8 @@ setWantedTyBind tv ty
\end{code}
Note [Optimizing Spontaneously Solved Coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Spontaneously solved coercions such as alpha := tau used to be bound as everything else
in the evidence binds. Subsequently they were used for rewriting other wanted or solved
goals. For instance:
WorkItem = [S] g1 : a ~ tau
Inerts = [S] g2 : b ~ [a]
[S] g3 : c ~ [(a,a)]
Would result, eventually, after the workitem rewrites the inerts, in the
following evidence bindings:
g1 = ReflCo tau
g2 = ReflCo [a]
g3 = ReflCo [(a,a)]
g2' = g2 ; [g1]
g3' = g3 ; [(g1,g1)]
This ia annoying because it puts way too much stress to the zonker and
desugarer, since we /know/ at the generation time (spontaneously
solving) that the evidence for a particular evidence variable is the
identity.
For this reason, our solution is to cache inside the GivenSolved
flavor of a constraint the term which is actually solving this
constraint. Whenever we perform a setEvBind, a new flavor is returned
so that if it was a GivenSolved to start with, it remains a
GivenSolved with a new evidence term inside. Then, when we use solved
goals to rewrite other constraints we simply use whatever is in the
GivenSolved flavor and not the constraint cc_id.
In our particular case we'd get the following evidence bindings, eventually:
g1 = ReflCo tau
g2 = ReflCo [a]
g3 = ReflCo [(a,a)]
g2'= ReflCo [a]
g3'= ReflCo [(a,a)]
Since we use smart constructors to get rid of g;ReflCo t ~~> g etc.
\begin{code}
warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
warnTcS loc warn_if doc
| warn_if = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
......@@ -1285,6 +1249,52 @@ isTouchableMetaTyVar_InRange (untch,untch_tcs) tv
\end{code}
Note [Do not add duplicate derived insolubles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In general we do want to add an insoluble (Int ~ Bool) even if there is one
such there already, because they may come from distinct call sites. But for
*derived* insolubles, we only want to report each one once. Why?
(a) A constraint (C r s t) where r -> s, say, may generate the same fundep
equality many times, as the original constraint is sucessively rewritten.
(b) Ditto the successive iterations of the main solver itself, as it traverses
the constraint tree. See example below.
Also for *given* insolubles we may get repeated errors, as we
repeatedly traverse the constraint tree. These are relatively rare
anyway, so removing duplicates seems ok. (Alternatively we could take
the SrcLoc into account.)
Note that the test does not need to be particularly efficient because
it is only used if the program has a type error anyway.
Example of (b): assume a top-level class and instance declaration:
class D a b | a -> b
instance D [a] [a]
Assume we have started with an implication:
forall c. Eq c => { wc_flat = D [c] c [W] }
which we have simplified to:
forall c. Eq c => { wc_flat = D [c] c [W]
, wc_insols = (c ~ [c]) [D] }
For some reason, e.g. because we floated an equality somewhere else,
we might try to re-solve this implication. If we do not do a
keepWanted, then we will end up trying to solve the following
constraints the second time:
(D [c] c) [W]
(c ~ [c]) [D]
which will result in two Deriveds to end up in the insoluble set:
wc_flat = D [c] c [W]
wc_insols = (c ~ [c]) [D], (c ~ [c]) [D]
Note [Touchable meta type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1681,25 +1691,6 @@ getCtCoercion :: EvBindMap -> Ct -> TcCoercion
getCtCoercion _bs ct
= ASSERT( not (isDerivedCt ct) )
evTermCoercion (ctEvTerm (ctEvidence ct))
{- ToDo: check with Dimitrios that we can dump this stuff
WARNING: if we *do* need this stuff, we need to think again about cyclic bindings.
= case lookupEvBind bs cc_id of
-- Given and bound to a coercion term
Just (EvBind _ (EvCoercion co)) -&