diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index c0762daeb26918c977cd9b5703e0d425dcfd8e4a..bbf5ae61817911739905a1a9b7157f779883d3af 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -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
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 2a3b2a4c1f7a103c1b53827f9cd9e4b3ac6c9c74..1ddcd316c1fa0919f7754057f54dc12689dfbd09 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -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')
@@ -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}
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index adff5ea18264cb8817c183f7685023f8aaf96a05..2c2dc54c1b09137c25b19fef613bbcb56e022df1 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -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)
-
- 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}
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index ac35c37df26443e6107814d3ad33709222197b79..0eb1efe509adf8d2e1d6a3175417173c2113c2af 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -857,8 +857,8 @@ type SubGoalDepth = Int -- An ever increasing number used to restrict
data Ct
-- Atomic canonical constraints
= CDictCan { -- e.g. Num xi
- cc_ev :: CtEvidence,
- cc_class :: Class,
+ cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
+ cc_class :: Class,
cc_tyargs :: [Xi],
cc_depth :: SubGoalDepth -- Simplification depth of this constraint
@@ -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
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 4073e4e6f8ab7f83a2d1818e0b774faf7efa4f87..150b400ad5f614a6c989b53cee56bb9e0bcb37f5 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -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}
@@ -516,7 +517,9 @@ data InertSet
-- Key is by family head. We use this field during flattening only
-- Not necessarily inert wrt top-level equations (or inert_cans)
- , inert_solved_funeqs :: FamHeadMap CtEvidence -- Of form co :: F xis ~ xi
+ , 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)) -> co
- -- NB: The constraint could have been rewritten due to spontaneous
- -- unifications but because we are optimizing away mkRefls the evidence
- -- variable may still have type (alpha ~ [beta]). The constraint may
- -- however have a more accurate type (alpha ~ [Int]) (where beta ~ Int has
- -- been previously solved by spontaneous unification). So if we are going
- -- to use the evidence variable for rewriting other constraints, we'd better
- -- make sure it's of the right type!
- -- Always the ctPred type is more accurate, so we just pick that type
-
- _ -> mkTcCoVarCo (setVarType cc_id (ctPred ct))
-
- where
- cc_id = ctId ct
--}
\end{code}
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 152f7445fbe4487c041eb9e4540398381f82cf89..a848e7fdff4f2253bfd5030121b2d2a542978186 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -759,10 +759,10 @@ solve_wanteds wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols
-- Try the flat 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.
- -- Why keepWanted insols? See Note [KeepWanted in SolveWanteds]
- ; let all_flats = flats `unionBags` keepWanted insols
- -- DV: Used to be 'keepWanted insols' but just insols is
+ -- 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]
+ ; let all_flats = flats `unionBags` insols
; impls_from_flats <- solveInteractCts $ bagToList all_flats
@@ -905,10 +905,7 @@ solveImplication tcs_untouchables
; let (res_flat_free, res_flat_bound)
= floatEqualities skols givens unsolved_flats
- ; let res_wanted = WC { wc_flat = keepWanted $ res_flat_bound
- -- I think this keepWanted must eventually go away, but it is
- -- a real code-breaking change.
- -- See Note [KeepWanted in SolveImplication]
+ ; let res_wanted = WC { wc_flat = res_flat_bound
, wc_impl = unsolved_implics
, wc_insol = insols }
@@ -928,81 +925,8 @@ solveImplication tcs_untouchables
\end{code}
-Note [KeepWanted in SolveWanteds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Why do we have:
- let all_flats = flats `unionBags` keepWanted insols
-instead of the simpler:
- let all_flats = flats `unionBags` insols
-in solve_wanteds?
-
-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]
-
-which can result in reporting the same error twice.
-
-So, do we /lose/ some potentially useful information by doing this?
-
-No, because the insoluble Derived/Given are going to be equalities,
-which are going to be derivable anyway from the rest of the flat
-constraints.
-
-
-Note [KeepWanted in SolveImplication]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-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.
-
-I actually think this is a legitimate behaviour (to fail). After all, if we had
-given the inferred signature to foo we would have failed as well, but we have to
-find a workaround because library code breaks.
-
-For now I keep the 'keepWanted' though it seems problematic e.g. we might discard
-a useful Derived!
\begin{code}
-
-
floatEqualities :: [TcTyVar] -> [EvVar] -> Cts -> (Cts, Cts)
-- Post: The returned FlavoredEvVar's are only Wanted or Derived
-- and come from the input wanted ev vars or deriveds