Commit 9591547f authored by dimitris's avatar dimitris

Introducing:

   1) Postponing the application of instances when there
      is a possibility of a given matching. With the addition
      of prioritizing equalities this fixes #5002 and #4981.

   2) Implemented caching of flattening in constraint
      simplification. This improves efficiency (fixes #5030)

   3) Simplified pushing of unsolved wanteds
      (now pushing only equalities) inside implications.
parent 2d520511
......@@ -551,7 +551,7 @@ tidyFlavoredEvVar env (EvVarX v fl)
= EvVarX (tidyEvVar env v) (tidyFlavor env fl)
tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk
tidyFlavor _ fl = fl
tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
......@@ -595,8 +595,8 @@ substFlavoredEvVar subst (EvVarX v fl)
= EvVarX (substEvVar subst v) (substFlavor subst fl)
substFlavor :: TvSubst -> CtFlavor -> CtFlavor
substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
substFlavor _ fl = fl
substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk
substFlavor _ fl = fl
substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
......
This diff is collapsed.
......@@ -16,6 +16,7 @@ import TcSMonad
import TcType
import TypeRep
import Type( isTyVarTy )
import Unify ( tcMatchTys )
import Inst
import InstEnv
......@@ -106,7 +107,7 @@ reportTidyWanteds ctxt (WC { wc_flat = flats, wc_insol = insols, wc_impl = impli
-- because they are unconditionally wrong
-- Moreover, if any of the insolubles are givens, stop right there
-- ignoring nested errors, because the code is inaccessible
= do { let (given, other) = partitionBag (isGiven . evVarX) insols
= do { let (given, other) = partitionBag (isGivenOrSolved . evVarX) insols
insol_implics = filterBag ic_insol implics
; if isEmptyBag given
then do { mapBagM_ (reportInsoluble ctxt) other
......@@ -154,7 +155,8 @@ reportInsoluble ctxt (EvVarX ev flav)
| otherwise
= pprPanic "reportInsoluble" (pprEvVarWithType ev)
where
inaccessible_msg | Given loc <- flav
inaccessible_msg | Given loc GivenOrig <- flav
-- If a GivenSolved then we should not report inaccessible code
= hang (ptext (sLit "Inaccessible code in"))
2 (ppr (ctLocOrigin loc))
| otherwise = empty
......@@ -420,18 +422,18 @@ couldNotDeduce :: [([EvVar], GivenLoc)] -> (ThetaType, CtOrigin) -> SDoc
couldNotDeduce givens (wanteds, orig)
= vcat [ hang (ptext (sLit "Could not deduce") <+> pprTheta wanteds)
2 (pprArising orig)
, vcat pp_givens ]
where
pp_givens
= case givens of
, vcat (pp_givens givens)]
pp_givens :: [([EvVar], GivenLoc)] -> [SDoc]
pp_givens givens
= case givens of
[] -> []
(g:gs) -> ppr_given (ptext (sLit "from the context")) g
: map (ppr_given (ptext (sLit "or from"))) gs
ppr_given herald (gs,loc)
= hang (herald <+> pprEvVarTheta gs)
2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc)
, ptext (sLit "at") <+> ppr (ctLocSpan loc)])
where ppr_given herald (gs,loc)
= hang (herald <+> pprEvVarTheta gs)
2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin loc)
, ptext (sLit "at") <+> ppr (ctLocSpan loc)])
addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt
-- Add on extra info about the types themselves
......@@ -577,6 +579,18 @@ reportOverlap ctxt inst_envs orig pred@(ClassP clas tys)
<+> pprPred pred)
, sep [ptext (sLit "Matching instances") <> colon,
nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])]
, if not (null overlapping_givens) then
sep [ptext (sLit "Matching givens (or their superclasses)") <> colon, nest 2 (vcat overlapping_givens)]
else empty
, if null overlapping_givens && isSingleton matches && null unifiers then
-- Intuitively, some given matched the wanted in their flattened or rewritten (from given equalities)
-- form but the matcher can't figure that out because the constraints are non-flat and non-rewritten
-- so we simply report back the whole given context. Accelerate Smart.hs showed this problem.
sep [ptext (sLit "There exists a (perhaps superclass) match") <> colon, nest 2 (vcat (pp_givens givens))]
else empty
, if not (isSingleton matches)
then -- Two or more matches
empty
......@@ -584,11 +598,39 @@ reportOverlap ctxt inst_envs orig pred@(ClassP clas tys)
ASSERT( not (null unifiers) )
parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
quotes (pprWithCommas ppr (varSetElems (tyVarsOfPred pred))),
ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
ptext (sLit "when compiling the other instance declarations")])]
if null (overlapping_givens) then
vcat [ ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
ptext (sLit "when compiling the other instance declarations")]
else empty])]
where
ispecs = [ispec | (ispec, _) <- matches]
givens = getUserGivens ctxt
overlapping_givens = unifiable_givens givens
unifiable_givens [] = []
unifiable_givens (gg:ggs)
| Just ggdoc <- matchable gg
= ggdoc : unifiable_givens ggs
| otherwise
= unifiable_givens ggs
matchable (evvars,gloc)
= case ev_vars_matching of
[] -> Nothing
_ -> Just $ hang (pprTheta ev_vars_matching)
2 (sep [ ptext (sLit "bound by") <+> ppr (ctLocOrigin gloc)
, ptext (sLit "at") <+> ppr (ctLocSpan gloc)])
where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
ev_var_matches (ClassP clas' tys')
| clas' == clas
, Just _ <- tcMatchTys (tyVarsOfTypes tys) tys tys'
= True
ev_var_matches (ClassP clas' tys') =
any ev_var_matches (immSuperClasses clas' tys')
ev_var_matches _ = False
reportOverlap _ _ _ _ = panic "reportOverlap" -- Not a ClassP
----------------------
......@@ -834,9 +876,9 @@ flattenForAllErrorTcS fl ty _bad_eqs
\begin{code}
setCtFlavorLoc :: CtFlavor -> TcM a -> TcM a
setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing
setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing
setCtFlavorLoc (Given loc) thing = setCtLoc loc thing
setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing
setCtFlavorLoc (Derived loc) thing = setCtLoc loc thing
setCtFlavorLoc (Given loc _gk) thing = setCtLoc loc thing
\end{code}
%************************************************************************
......
......@@ -621,6 +621,9 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
addErrCtxt (instDeclCtxt2 (idType dfun_id)) $
do { -- Instantiate the instance decl with skolem constants
; (inst_tyvars, dfun_theta, inst_head) <- tcSkolDFunType (idType dfun_id)
-- We instantiate the dfun_id with superSkolems.
-- See Note [Subtle interaction of recursion and overlap]
-- and Note [Binding when looking up instances]
; let (clas, inst_tys) = tcSplitDFunHead inst_head
(class_tyvars, sc_theta, _, op_items) = classBigSig clas
sc_theta' = substTheta (zipOpenTvSubst class_tyvars inst_tys) sc_theta
......@@ -699,7 +702,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
listToBag meth_binds)
}
where
skol_info = InstSkol -- See Note [Subtle interaction of recursion and overlap]
skol_info = InstSkol
dfun_ty = idType dfun_id
dfun_id = instanceDFunId ispec
loc = getSrcSpan dfun_id
......
This diff is collapsed.
......@@ -627,8 +627,8 @@ zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
zonkFlavor :: CtFlavor -> TcM CtFlavor
zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
zonkFlavor fl = return fl
zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
zonkFlavor fl = return fl
zonkGivenLoc :: GivenLoc -> TcM GivenLoc
-- GivenLocs may have unification variables inside them!
......
......@@ -40,11 +40,13 @@ module TcRnTypes(
Implication(..),
CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin,
CtOrigin(..), EqOrigin(..),
WantedLoc, GivenLoc, pushErrCtxt,
WantedLoc, GivenLoc, GivenKind(..), pushErrCtxt,
SkolemInfo(..),
CtFlavor(..), pprFlavorArising, isWanted, isGiven, isDerived,
CtFlavor(..), pprFlavorArising, isWanted,
isGivenOrSolved, isGiven_maybe,
isDerived,
FlavoredEvVar,
-- Pretty printing
......@@ -923,35 +925,37 @@ pprWantedEvVar (EvVarX v _) = pprEvVarWithType v
\begin{code}
data CtFlavor
= Given GivenLoc -- We have evidence for this constraint in TcEvBinds
| Derived WantedLoc
-- We have evidence for this constraint in TcEvBinds;
-- *however* this evidence can contain wanteds, so
-- it's valid only provisionally to the solution of
-- these wanteds
| Wanted WantedLoc -- We have no evidence bindings for this constraint.
-- data DerivedOrig = DerSC | DerInst | DerSelf
-- Deriveds are either superclasses of other wanteds or deriveds, or partially
-- solved wanteds from instances, or 'self' dictionaries containing yet wanted
-- superclasses.
= Given GivenLoc GivenKind -- We have evidence for this constraint in TcEvBinds
| Derived WantedLoc -- Derived's are just hints for unifications
| Wanted WantedLoc -- We have no evidence bindings for this constraint.
data GivenKind
= GivenOrig -- Originates in some given, such as signature or pattern match
| GivenSolved -- Is given as result of being solved, maybe provisionally on
-- some other wanted constraints.
instance Outputable CtFlavor where
ppr (Given {}) = ptext (sLit "[G]")
ppr (Wanted {}) = ptext (sLit "[W]")
ppr (Derived {}) = ptext (sLit "[D]")
ppr (Given _ GivenOrig) = ptext (sLit "[G]")
ppr (Given _ GivenSolved) = ptext (sLit "[S]") -- Print [S] for Given/Solved's
ppr (Wanted {}) = ptext (sLit "[W]")
ppr (Derived {}) = ptext (sLit "[D]")
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl ) = pprArisingAt wl
pprFlavorArising (Derived wl) = pprArisingAt wl
pprFlavorArising (Wanted wl) = pprArisingAt wl
pprFlavorArising (Given gl) = pprArisingAt gl
pprFlavorArising (Given gl _) = pprArisingAt gl
isWanted :: CtFlavor -> Bool
isWanted (Wanted {}) = True
isWanted _ = False
isGiven :: CtFlavor -> Bool
isGiven (Given {}) = True
isGiven _ = False
isGivenOrSolved :: CtFlavor -> Bool
isGivenOrSolved (Given {}) = True
isGivenOrSolved _ = False
isGiven_maybe :: CtFlavor -> Maybe GivenKind
isGiven_maybe (Given _ gk) = Just gk
isGiven_maybe _ = Nothing
isDerived :: CtFlavor -> Bool
isDerived (Derived {}) = True
......
This diff is collapsed.
......@@ -747,22 +747,26 @@ solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol =
unsolved_implics
}
givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
-- Extract the *wanted* ones from CanonicalCts
-- and make them into *givens*
givensFromWanteds = foldrBag getWanted emptyBag
givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar
-- Extract the Wanted ones from CanonicalCts and conver to
-- Givens; not Given/Solved, see Note [Preparing inert set for implications]
givensFromWanteds _ctxt = foldrBag getWanted emptyBag
where
getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
getWanted cc givens
| not (isCFrozenErr cc)
, Wanted loc <- cc_flavor cc
, let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
= given `consBag` givens
| otherwise
= givens -- We are not helping anyone by pushing a Derived in!
-- Because if we could not solve it to start with
-- we are not going to do either inside the impl constraint
| pushable_wanted cc
= let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol)
in given `consBag` givens -- and not mkSolvedFlavor,
-- see Note [Preparing inert set for implications]
| otherwise = givens
pushable_wanted :: CanonicalCt -> Bool
pushable_wanted cc
| not (isCFrozenErr cc)
, isWantedCt cc
= isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
| otherwise = False
solveNestedImplications :: InertSet -> CanonicalCts
-> Bag Implication
-> TcS (Bag FlavoredEvVar, Bag Implication)
......@@ -772,15 +776,18 @@ solveNestedImplications just_given_inert unsolved_cans implics
| otherwise
= do { -- See Note [Preparing inert set for implications]
-- Push the unsolved wanteds inwards, but as givens
let pushed_givens = givensFromWanteds unsolved_cans
; simpl_ctx <- getTcSContext
; let pushed_givens = givensFromWanteds simpl_ctx unsolved_cans
tcs_untouchables = filterVarSet isFlexiTcsTv $
tyVarsOfEvVarXs pushed_givens
-- See Note [Extra TcsTv untouchables]
; traceTcS "solveWanteds: preparing inerts for implications {"
(vcat [ppr tcs_untouchables, ppr pushed_givens])
; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
; traceTcS "solveWanteds: } now doing nested implications {" $
vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
......@@ -931,6 +938,42 @@ We were not able to solve (a ~w [beta]) but we can't just assume it as
given because the resulting set is not inert. Hence we have to do a
'solveInteract' step first.
Finally, note that we convert them to [Given] and NOT [Given/Solved].
The reason is that Given/Solved are weaker than Givens and may be discarded.
As an example consider the inference case, where we may have, the following
original constraints:
[Wanted] F Int ~ Int
(F Int ~ a => F Int ~ a)
If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next
given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting
the (F Int ~ a) insoluble. Hence we should really convert the residual
wanteds to plain old Given.
We need only push in unsolved equalities both in checking mode and inference mode:
(1) In checking mode we should not push given dictionaries in because of
example LongWayOverlapping.hs, where we might get strange overlap
errors between far-away constraints in the program. But even in
checking mode, we must still push type family equations. Consider:
type instance F True a b = a
type instance F False a b = b
[w] F c a b ~ gamma
(c ~ True) => a ~ gamma
(c ~ False) => b ~ gamma
Since solveCTyFunEqs happens at the very end of solving, the only way to solve
the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not
merely Given/Solved because it has to interact with the top-level instance
environment) and push it inside the implications. Now, when we come out again at
the end, having solved the implications solveCTyFunEqs will solve this equality.
(2) In inference mode, we recheck the final constraint in checking mode and
hence we will be able to solve inner implications from top-level quantified
constraints nonetheless.
Note [Extra TcsTv untouchables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Furthemore, we record the inert set simplifier-generated unification
......@@ -1029,7 +1072,7 @@ getSolvableCTyFunEqs untch cts
, not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
-- Occurs check: see Note [Solving Family Equations], Point 2
= ASSERT ( not (isGiven fl) )
= ASSERT ( not (isGivenOrSolved fl) )
(cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
dflt_funeq (cts_in, fun_eq_binds) ct
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment