-> TcM ([Inst], TcDictBinds)
tryHardCheckLoop doc wanteds
- = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
+ = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
; return (irreds,binds)
}
where
- try_me _ = ReduceMe AddSCs
+ try_me _ = ReduceMe
-- Here's the try-hard bit
-----------------------------------------------------------
where
env = mkRedEnv (pprInstLoc inst_loc) try_me givens
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ try_me inst | isMethodOrLit inst = ReduceMe
| otherwise = Stop
-- When checking against a given signature
-- we MUST be very gentle: Note [Check gently]
= do { (irreds, binds) <- checkLoop env wanteds
; return (irreds, binds) }
where
- env = mkRedEnv doc try_me []
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ env = mkInferRedEnv doc try_me
+ try_me inst | isMethodOrLit inst = ReduceMe
| otherwise = Stop
\end{code}
; (improved, binds, irreds) <- reduceContext env' wanteds'
- ; if not improved then
+ ; if null irreds || not improved then
return (irreds, binds)
else do
ds2 = $p1 dc
And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
Two more nasty cases are in
tcrun021
tcrun033
+Solution:
+ - Satisfy the superclass context *all by itself*
+ (tcSimplifySuperClasses)
+ - And do so completely; i.e. no left-over constraints
+ to mix with the constraints arising from method declarations
+
+
+Note [Recursive instances and superclases]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this code, which arises in the context of "Scrap Your
+Boilerplate with Class".
+
+ class Sat a
+ class Data ctx a
+ instance Sat (ctx Char) => Data ctx Char
+ instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
+
+ class Data Maybe a => Foo a
+
+ instance Foo t => Sat (Maybe t)
+
+ instance Data Maybe a => Foo a
+ instance Foo a => Foo [a]
+ instance Foo [Char]
+
+In the instance for Foo [a], when generating evidence for the superclasses
+(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
+Using the instance for Data, we therefore need
+ (Sat (Maybe [a], Data Maybe a)
+But we are given (Foo a), and hence its superclass (Data Maybe a).
+So that leaves (Sat (Maybe [a])). Using the instance for Sat means
+we need (Foo [a]). And that is the very dictionary we are bulding
+an instance for! So we must put that in the "givens". So in this
+case we have
+ Given: Foo a, Foo [a]
+ Watend: Data Maybe [a]
+
+BUT we must *not not not* put the *superclasses* of (Foo [a]) in
+the givens, which is what 'addGiven' would normally do. Why? Because
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
+by selecting a superclass from Foo [a], which simply makes a loop.
+
+On the other hand we *must* put the superclasses of (Foo a) in
+the givens, as you can see from the derivation described above.
+
+Conclusion: in the very special case of tcSimplifySuperClasses
+we have one 'given' (namely the "this" dictionary) whose superclasses
+must not be added to 'givens' by addGiven. That is the *whole* reason
+for the red_given_scs field in RedEnv, and the function argument to
+addGiven.
+
\begin{code}
-tcSimplifySuperClasses
+tcSimplifySuperClasses
:: InstLoc
+ -> Inst -- The dict whose superclasses
+ -- are being figured out
-> [Inst] -- Given
-> [Inst] -- Wanted
-> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
+tcSimplifySuperClasses loc this givens sc_wanteds
= do { traceTc (text "tcSimplifySuperClasses")
; (irreds,binds1) <- checkLoop env sc_wanteds
; let (tidy_env, tidy_irreds) = tidyInsts irreds
; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
; return binds1 }
where
- env = mkRedEnv (pprInstLoc loc) try_me givens
- try_me _ = ReduceMe NoSCs
- -- Like tryHardCheckLoop, but with NoSCs
+ env = RedEnv { red_doc = pprInstLoc loc,
+ red_try_me = try_me,
+ red_givens = this:givens,
+ red_given_scs = add_scs,
+ red_stack = (0,[]),
+ red_improve = False } -- No unification vars
+ add_scs g | g==this = NoSCs
+ | otherwise = AddSCs
+
+ try_me _ = ReduceMe -- Try hard, so we completely solve the superclass
+ -- constraints right here. See Note [SUPERCLASS-LOOP 1]
\end{code}
-- BUT do no improvement! See Plan D above
-- HOWEVER, some unification may take place, if we instantiate
-- a method Inst with an equality constraint
- ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe AddSCs)
+ ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
-- Next, figure out the tyvars we will quantify over
; let is_nested_group = isNotTopLevel top_lvl
try_me inst | isFreeWrtTyVars qtvs inst,
(is_nested_group || isDict inst) = Stop
- | otherwise = ReduceMe AddSCs
+ | otherwise = ReduceMe
env = mkNoImproveRedEnv doc try_me
; (_imp, binds, irreds) <- reduceContext env wanteds'
}
-- Sigh: we need to reduce inside implications
- red_env = mkRedEnv doc try_me []
+ red_env = mkInferRedEnv doc try_me
doc = ptext (sLit "Implication constraint in RULE lhs")
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+ try_me inst | isMethodOrLit inst = ReduceMe
| otherwise = Stop -- Be gentle
\end{code}
-- Simplify any methods that mention the implicit parameter
try_me inst | is_free inst = Stop
- | otherwise = ReduceMe NoSCs
+ | otherwise = ReduceMe
\end{code}
, red_try_me :: Inst -> WhatToDo
, red_improve :: Bool -- True <=> do improvement
, red_givens :: [Inst] -- All guaranteed rigid
- -- Always dicts
+ -- Always dicts & equalities
-- but see Note [Rigidity]
+
+ , red_given_scs :: Inst -> WantSCs -- See Note [Recursive instances and superclases]
+
, red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
-- See Note [RedStack]
}
mkRedEnv doc try_me givens
= RedEnv { red_doc = doc, red_try_me = try_me,
red_givens = givens,
+ red_given_scs = const AddSCs,
+ red_stack = (0,[]),
+ red_improve = True }
+
+mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- No givens at all
+mkInferRedEnv doc try_me
+ = RedEnv { red_doc = doc, red_try_me = try_me,
+ red_givens = [],
+ red_given_scs = const AddSCs,
red_stack = (0,[]),
red_improve = True }
mkNoImproveRedEnv doc try_me
= RedEnv { red_doc = doc, red_try_me = try_me,
red_givens = [],
+ red_given_scs = const AddSCs,
red_stack = (0,[]),
red_improve = True }
data WhatToDo
- = ReduceMe WantSCs -- Try to reduce this
- -- If there's no instance, add the inst to the
- -- irreductible ones, but don't produce an error
- -- message of any kind.
- -- It might be quite legitimate such as (Eq a)!
+ = ReduceMe -- Try to reduce this
+ -- If there's no instance, add the inst to the
+ -- irreductible ones, but don't produce an error
+ -- message of any kind.
+ -- It might be quite legitimate such as (Eq a)!
| Stop -- Return as irreducible unless it can
-- be reduced to a constant in one step
wanteds',
normalise_binds,
eq_improved) <- tcReduceEqs givens wanteds
+ ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
+ [ppr givens', ppr wanteds', ppr normalise_binds]
-- Build the Avail mapping from "given_dicts"
; (init_state, _) <- getLIE $ do
- { init_state <- foldlM addGiven emptyAvails givens'
+ { init_state <- foldlM (addGiven (red_given_scs env))
+ emptyAvails givens'
; return init_state
}
; (dict_binds,
bound_dicts,
dict_irreds) <- extractResults avails wanted_dicts
- ; traceTc $ text "reduceContext extractresults" <+> vcat
+ ; traceTc $ text "reduceContext: extractResults" <+> vcat
[ppr avails, ppr wanted_dicts, ppr dict_binds]
-- Solve the wanted *implications*. In doing so, we can provide
-- as "given" all the dicts that were originally given,
-- *or* for which we now have bindings,
-- *or* which are now irreds
- ; let implic_env = env { red_givens = givens ++ bound_dicts ++
- dict_irreds }
+ -- NB: Equality irreds need to be converted, as the recursive
+ -- invocation of the solver will still treat them as wanteds
+ -- otherwise.
+ ; let implic_env = env { red_givens
+ = givens ++ bound_dicts ++
+ map wantedToLocalEqInst dict_irreds }
; (implic_binds_s, implic_irreds_s)
<- mapAndUnzipM (reduceImplication implic_env) wanted_implics
; let implic_binds = unionManyBags implic_binds_s
implic_irreds = concat implic_irreds_s
-- Collect all irreducible instances, and determine whether we should
- -- go round again. We do so in either of three cases:
+ -- go round again. We do so in either of two cases:
-- (1) If dictionary reduction or equality solving led to
-- improvement (i.e., instantiated type variables).
- -- (2) If we managed to normalise any dicts, there is merit in going
- -- around gain, because reduceList may be able to get further.
- -- (3) If we uncovered extra equalities. We will try to solve them
+ -- (2) If we uncovered extra equalities. We will try to solve them
-- in the next iteration.
+
; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
- improvedFlexible = availsImproved avails ||
- eq_improved
- improvedDicts = not $ isEmptyBag normalise_binds
+ avails_improved = availsImproved avails
+ improvedFlexible = avails_improved || eq_improved
extraEqs = (not . null) extra_eqs
- improved = improvedFlexible || improvedDicts || extraEqs
-
-{- Old story
- -- Figure out whether we should go round again. We do so in either
- -- two cases:
- -- (1) If any of the mutable tyvars in givens or irreds has been
- -- filled in by improvement, there is merit in going around
- -- again, because we may make further progress.
- -- (2) If we managed to normalise any dicts, there is merit in going
- -- around gain, because reduceList may be able to get further.
-
- ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
- tyVarsOfInsts (givens ++ all_irreds)
- ; let improvedDicts = not $ isEmptyBag normalise_binds
- improved = improvedMetaTy || improvedDicts
- -}
+ improved = improvedFlexible || extraEqs
+ --
+ improvedHint = (if avails_improved then " [AVAILS]" else "") ++
+ (if eq_improved then " [EQ]" else "") ++
+ (if extraEqs then " [EXTRA EQS]" else "")
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
text "wanted" <+> ppr wanteds0,
text "----",
text "avails" <+> pprAvails avails,
- text "improved =" <+> ppr improved,
+ text "improved =" <+> ppr improved <+> text improvedHint,
text "(all) irreds = " <+> ppr all_irreds,
text "dict-binds = " <+> ppr dict_binds,
text "implic-binds = " <+> ppr implic_binds,
-- Avails has all the superclasses etc (good)
-- It also has all the intermediates of the deduction (good)
-- It does not have duplicates (good)
- -- NB that (?x::t1) and (?x::t2) will be held separately in avails
- -- so that improve will see them separate
+ -- NB that (?x::t1) and (?x::t2) will be held separately in
+ -- avails so that improve will see them separate
; traceTc (text "improveOne" <+> ppr inst)
; unifyEqns eqns }
-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
+unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))]
-> TcM ImprovementDone
unifyEqns [] = return False
unifyEqns eqns
= do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
- ; mapM_ unify eqns
- ; return True }
+ ; improved <- mapM unify eqns
+ ; return $ or improved
+ }
where
unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $ do
- (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
- mapM_ (unif_pr tenv) pairs
- unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
+ = addErrCtxtM (mkEqnMsg what1 what2) $
+ do { let freeTyVars = unionVarSets (map tvs_pr pairs)
+ `minusVarSet` qtvs
+ ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+ ; mapM_ (unif_pr tenv) pairs
+ ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
+ }
+
+ unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
+
+ tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
-pprEquationDoc (eqn, (p1, _), (p2, _)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+pprEquationDoc (eqn, (p1, _), (p2, _))
+ = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
-> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
- = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
- ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
+ = do { pred1' <- zonkTcPredType pred1
+ ; pred2' <- zonkTcPredType pred2
+ ; let { pred1'' = tidyPred tidy_env pred1'
+ ; pred2'' = tidyPred tidy_env pred2' }
; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
-- Base case: we're done!
reduce :: RedEnv -> Inst -> Avails -> TcM Avails
reduce env wanted avails
+
+ -- We don't reduce equalities here (and they must not end up as irreds
+ -- in the Avails!)
+ | isEqInst wanted
+ = return avails
+
-- It's the same as an existing inst, or a superclass thereof
| Just _ <- findAvail avails wanted
= do { traceTc (text "reduce: found " <+> ppr wanted)
Stop -> try_simple (addIrred NoSCs);
-- See Note [No superclasses for Stop]
- ReduceMe want_scs -> do -- It should be reduced
+ ReduceMe -> do -- It should be reduced
{ (avails, lookup_result) <- reduceInst env avails wanted
; case lookup_result of
- NoInstance -> addIrred want_scs avails wanted
+ NoInstance -> addIrred AddSCs avails wanted
-- Add it and its superclasses
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+ GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
GenInst wanteds' rhs
-> do { avails1 <- addIrred NoSCs avails wanted
; avails2 <- reduceList env wanteds' avails1
- ; addWanted want_scs avails2 wanted rhs wanteds' } }
+ ; addWanted AddSCs avails2 wanted rhs wanteds' } }
-- Temporarily do addIrred *before* the reduceList,
-- which has the effect of adding the thing we are trying
-- to prove to the database before trying to prove the things it
\end{code}
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data D r = ZeroD | SuccD (r (D r));
+
+ instance (Eq (r (D r))) => Eq (D r) where
+ ZeroD == ZeroD = True
+ (SuccD a) == (SuccD b) = a == b
+ _ == _ = False;
+
+ equalDC :: D [] -> D [] -> Bool;
+ equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+ d1 : Eq (D [])
+
+by instance decl, holds if
+ d2 : Eq [D []]
+ where d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+ d3 : D []
+ where d2 = dfEqList d3
+ d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+ d3 = d1
+ d2 = dfEqList d3
+ d1 = dfEqD d2
+
+and it'll even run! The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+
Note [SUPERCLASS-LOOP 2]
~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough. Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
+We need to be careful when adding "the constaint we are trying to prove".
+Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
class Ord a => C a where
instance Ord [a] => C [a] where ...
when adding superclasses. It's a bit like the occurs check in unification.
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data D r = ZeroD | SuccD (r (D r));
-
- instance (Eq (r (D r))) => Eq (D r) where
- ZeroD == ZeroD = True
- (SuccD a) == (SuccD b) = a == b
- _ == _ = False;
-
- equalDC :: D [] -> D [] -> Bool;
- equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
- d1 : Eq (D [])
-
-by instance decl, holds if
- d2 : Eq [D []]
- where d1 = dfEqD d2
-
-by instance decl of Eq, holds if
- d3 : D []
- where d2 = dfEqList d3
- d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
- d3 = d1
- d2 = dfEqList d3
- d1 = dfEqD d2
-
-and it'll even run! The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-
%************************************************************************
%* *
tci_tyvars = tvs,
tci_given = extra_givens, tci_wanted = wanteds })
= do { -- Solve the sub-problem
- ; let try_me _ = ReduceMe AddSCs -- Note [Freeness and implications]
+ ; let try_me _ = ReduceMe -- Note [Freeness and implications]
env' = env { red_givens = extra_givens ++ red_givens env
, red_doc = sep [ptext (sLit "reduceImplication for")
<+> ppr name,
-- SLPJ Sept 07: what if improvement happened inside the checkLoop?
-- Then we must iterate the outer loop too!
- ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+ ; let backOff = isEmptyLHsBinds binds && -- no new bindings
+ (not $ null irreds) && -- but still some irreds
+ all (not . isEqInst) wanteds
+ -- we may have instantiated a cotv
+ -- => must make a new implication constraint!
--- Progress is no longer measered by the number of bindings
- ; if (isEmptyLHsBinds binds) && (not $ null irreds) then -- No progress
+ ; traceTc $ text "reduceImplication condition" <+> ppr backOff
+
+ -- Progress is no longer measered by the number of bindings
+ ; if backOff then -- No progress
-- If there are any irreds, we back off and do nothing
return (emptyBag, [orig_implic])
else do
= return (binds, bound_dicts, irreds)
go binds bound_dicts irreds done (w:ws)
+ | isEqInst w
+ = go binds bound_dicts (w:irreds) done' ws
+
| Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
= if w_id `elem` done_ids then
go binds bound_dicts irreds done ws
where
avail = Rhs rhs_expr wanteds
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
- -- Always add superclasses for 'givens'
+addGiven :: (Inst -> WantSCs) -> Avails -> Inst -> TcM Avails
+addGiven want_scs avails given = addAvailAndSCs (want_scs given) avails given (Given given)
+ -- Conditionally add superclasses for 'givens'
+ -- See Note [Recursive instances and superclases]
--
-- No ASSERT( not (given `elemAvails` avails) ) because in an instance
-- decl for Ord t we can add both Ord t and Eq t as 'givens',