X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=aff019e851b649d76fe60fffdb9a09d77386d26d;hp=1754c9deb882a62c6a2ca7347069efda47feb6d3;hb=aafdba3bce91afb003f5f50e001e141744837bae;hpb=4b305a0208c88ce6ac7a4899a9d565277b7a119c diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 1754c9d..aff019e 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -6,6 +6,13 @@ TcSimplify \begin{code} +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + module TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, tcSimplifyRestricted, @@ -15,7 +22,9 @@ module TcSimplify ( tcSimplifyBracket, tcSimplifyCheckPat, tcSimplifyDeriv, tcSimplifyDefault, - bindInstsOfLocalFuns, bindIrreds, + bindInstsOfLocalFuns, + + misMatchMsg ) where #include "HsVersions.h" @@ -31,6 +40,8 @@ import TcGadt import TcType import TcMType import TcIface +import TcTyFuns +import TypeRep import Var import Name import NameSet @@ -44,12 +55,14 @@ import ErrUtils import BasicTypes import VarSet import VarEnv +import Module import FiniteMap import Bag import Outputable import Maybes import ListSetOps import Util +import UniqSet import SrcLoc import DynFlags @@ -398,14 +411,19 @@ over implicit parameters. See the predicate isFreeWhenInferring. Note [Implicit parameters and ambiguity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -What type should we infer for this? - f x = (show ?y, x::Int) -Since we must quantify over the ?y, the most plausible type is - f :: (Show a, ?y::a) => Int -> (String, Int) -But notice that the type of the RHS is (String,Int), with no type -varibables mentioned at all! The type of f looks ambiguous. But -it isn't, because at a call site we might have - let ?y = 5::Int in f 7 +Only a *class* predicate can give rise to ambiguity +An *implicit parameter* cannot. For example: + foo :: (?x :: [a]) => Int + foo = length ?x +is fine. The call site will suppply a particular 'x' + +Furthermore, the type variables fixed by an implicit parameter +propagate to the others. E.g. + foo :: (Show a, ?x::[a]) => Int + foo = show (?x++?x) +The type of foo looks ambiguous. But it isn't, because at a call site +we might have + let ?x = 5::Int in foo and all is well. In effect, implicit parameters are, well, parameters, so we can take their type variables into account as part of the "tau-tvs" stuff. This is done in the function 'FunDeps.grow'. @@ -641,8 +659,9 @@ tcSimplifyInfer doc tau_tvs wanted = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs) ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars ; gbl_tvs <- tcGetGlobalTyVars - ; let preds = fdPredsOfInsts wanted' - qtvs = grow preds tau_tvs1 `minusVarSet` oclose preds gbl_tvs + ; let preds1 = fdPredsOfInsts wanted' + gbl_tvs1 = oclose preds1 gbl_tvs + qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1 -- See Note [Choosing which variables to quantify] -- To maximise sharing, remove from consideration any @@ -651,8 +670,8 @@ tcSimplifyInfer doc tau_tvs wanted ; extendLIEs free -- To make types simple, reduce as much as possible - ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs1) $$ ppr gbl_tvs $$ - ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound)) + ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ + ppr gbl_tvs1 $$ ppr free $$ ppr bound)) ; (irreds1, binds1) <- tryHardCheckLoop doc bound -- Note [Inference and implication constraints] @@ -682,9 +701,17 @@ tcSimplifyInfer doc tau_tvs wanted -- Then after simplifying we'll get (D a x), and x is fresh -- We must quantify over x else it'll be totally unbound ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1) - ; gbl_tvs <- tcGetGlobalTyVars - ; let preds = fdPredsOfInsts irreds2 -- irreds2 is zonked - qtvs = grow preds tau_tvs2 `minusVarSet` oclose preds gbl_tvs + ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1) + -- Note that we start from gbl_tvs1 + -- We use tcGetGlobalTyVars, then oclose wrt preds2, because + -- we've already put some of the original preds1 into frees + -- E.g. wanteds = C a b (where a->b) + -- gbl_tvs = {a} + -- tau_tvs = {b} + -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and + -- irreds2 will be empty. But we don't want to generalise over b! + ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked + qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2 ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2 ; extendLIEs free @@ -693,11 +720,15 @@ tcSimplifyInfer doc tau_tvs wanted -- We can't abstract over any remaining unsolved -- implications so instead just float them outwards. Ugh. - ; let (q_dicts, implics) = partition isDict irreds3 + ; let (q_dicts0, implics) = partition isAbstractableInst irreds3 ; loc <- getInstLoc (ImplicOrigin doc) - ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics + ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics - ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) } + -- Prepare equality instances for quantification + ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0 + ; q_eqs <- mappM finalizeEqInst q_eqs0 + + ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) } -- NB: when we are done, we might have some bindings, but -- the final qtvs might be empty. See Note [NO TYVARS] below. @@ -730,6 +761,8 @@ approximateImplications doc want_dict irreds = [ d | let tv_set = mkVarSet tvs , d <- get_dicts wanteds , not (tyVarsOfInst d `intersectsVarSet` tv_set)] + get_dict i@(EqInst {}) | want_dict i = [i] + | otherwise = [] get_dict other = pprPanic "approximateImplications" (ppr other) \end{code} @@ -748,7 +781,7 @@ with 'given' implications. So our best approximation is to make (D [a]) part of the inferred context, so we can use that to discharge the implication. Hence -the strange function get_dictsin approximateImplications. +the strange function get_dicts in approximateImplications. The common cases are more clear-cut, when we have things like forall a. C a => C b @@ -772,7 +805,8 @@ tcSimplifyInferCheck TcDictBinds) -- Bindings tcSimplifyInferCheck loc tau_tvs givens wanteds - = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds + = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds) + ; (irreds, binds) <- gentleCheckLoop loc givens wanteds -- Figure out which type variables to quantify over -- You might think it should just be the signature tyvars, @@ -796,6 +830,7 @@ tcSimplifyInferCheck loc tau_tvs givens wanteds -- Now we are back to normal (c.f. tcSimplCheck) ; implic_bind <- bindIrreds loc qtvs' givens irreds + ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind)) ; return (qtvs', binds `unionBags` implic_bind) } \end{code} @@ -878,7 +913,8 @@ tcSimplifyCheck :: InstLoc -> TcM TcDictBinds -- Bindings tcSimplifyCheck loc qtvs givens wanteds = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) - do { (irreds, binds) <- gentleCheckLoop loc givens wanteds + do { traceTc (text "tcSimplifyCheck") + ; (irreds, binds) <- gentleCheckLoop loc givens wanteds ; implic_bind <- bindIrreds loc qtvs givens irreds ; return (binds `unionBags` implic_bind) } @@ -892,7 +928,8 @@ tcSimplifyCheckPat :: InstLoc -> TcM TcDictBinds -- Bindings tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) - do { (irreds, binds) <- gentleCheckLoop loc givens wanteds + do { traceTc (text "tcSimplifyCheckPat") + ; (irreds, binds) <- gentleCheckLoop loc givens wanteds ; implic_bind <- bindIrredsR loc qtvs co_vars reft givens irreds ; return (binds `unionBags` implic_bind) } @@ -913,8 +950,10 @@ bindIrredsR loc qtvs co_vars reft givens irreds | null irreds = return emptyBag | otherwise - = do { let givens' = filter isDict givens - -- The givens can include methods + = do { let givens' = filter isAbstractableInst givens + -- The givens can (redundantly) include methods + -- We want to retain both EqInsts and Dicts + -- There should be no implicadtion constraints -- See Note [Pruning the givens in an implication constraint] -- If there are no 'givens' *and* the refinement is empty @@ -951,31 +990,41 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs reft givens -- Guaranteed all Dicts + -- or EqInsts irreds | null irreds -- If there are no irreds, we are done = return ([], emptyBag) | otherwise -- Otherwise we must generate a binding = do { uniq <- newUnique ; span <- getSrcSpanM + ; let (eq_givens, dict_givens) = partition isEqInst givens + eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens) + -- Urgh! See line 2187 or thereabouts. I believe that all these + -- 'givens' must be a simple CoVar. This MUST be cleaned up. + ; let name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_reft = reft, tci_tyvars = all_tvs, - tci_given = givens, + tci_given = (eq_givens ++ dict_givens), tci_wanted = irreds, tci_loc = loc } - - ; let n_irreds = length irreds - irred_ids = map instToId irreds - tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids) - pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty + ; let -- only create binder for dict_irreds + (eq_irreds, dict_irreds) = partition isEqInst irreds + n_dict_irreds = length dict_irreds + dict_irred_ids = map instToId dict_irreds + tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids) + pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty rhs = L span (mkHsWrap co (HsVar (instToId implic_inst))) - co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs) - bind | n_irreds==1 = VarBind (head irred_ids) rhs - | otherwise = PatBind { pat_lhs = L span pat, - pat_rhs = unguardedGRHSs rhs, - pat_rhs_ty = tup_ty, - bind_fvs = placeHolderNames } - ; -- pprTrace "Make implic inst" (ppr implic_inst) $ - return ([implic_inst], unitBag (L span bind)) } + co = mkWpApps (map instToId dict_givens) + <.> mkWpTyApps eq_tyvar_cos + <.> mkWpTyApps (mkTyVarTys all_tvs) + bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs + | otherwise = PatBind { pat_lhs = L span pat, + pat_rhs = unguardedGRHSs rhs, + pat_rhs_ty = tup_ty, + bind_fvs = placeHolderNames } + ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst + ; return ([implic_inst], unitBag (L span bind)) + } ----------------------------------------------------------- tryHardCheckLoop :: SDoc @@ -983,7 +1032,9 @@ tryHardCheckLoop :: SDoc -> TcM ([Inst], TcDictBinds) tryHardCheckLoop doc wanteds - = checkLoop (mkRedEnv doc try_me []) wanteds + = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds + ; return (irreds,binds) + } where try_me inst = ReduceMe AddSCs -- Here's the try-hard bit @@ -995,7 +1046,9 @@ gentleCheckLoop :: InstLoc -> TcM ([Inst], TcDictBinds) gentleCheckLoop inst_loc givens wanteds - = checkLoop env wanteds + = do { (irreds,binds,_) <- checkLoop env wanteds + ; return (irreds,binds) + } where env = mkRedEnv (pprInstLoc inst_loc) try_me givens @@ -1003,6 +1056,16 @@ gentleCheckLoop inst_loc givens wanteds | otherwise = Stop -- When checking against a given signature -- we MUST be very gentle: Note [Check gently] + +gentleInferLoop :: SDoc -> [Inst] + -> TcM ([Inst], TcDictBinds) +gentleInferLoop doc wanteds + = do { (irreds, binds, _) <- checkLoop env wanteds + ; return (irreds, binds) } + where + env = mkRedEnv doc try_me [] + try_me inst | isMethodOrLit inst = ReduceMe AddSCs + | otherwise = Stop \end{code} Note [Check gently] @@ -1020,7 +1083,7 @@ Inside the pattern match, which binds (a:*, x:a), we know that Hence we have a dictionary for Show [a] available; and indeed we need it. We are going to build an implication contraint forall a. (b~[a]) => Show [a] -Later, we will solve this constraint using the knowledg e(Show b) +Later, we will solve this constraint using the knowledge (Show b) But we MUST NOT reduce (Show [a]) to (Show a), else the whole thing becomes insoluble. So we simplify gently (get rid of literals @@ -1033,28 +1096,68 @@ with tryHardCheckLooop. ----------------------------------------------------------- checkLoop :: RedEnv -> [Inst] -- Wanted - -> TcM ([Inst], TcDictBinds) + -> TcM ([Inst], TcDictBinds, + [Inst]) -- needed givens -- Precondition: givens are completely rigid -- Postcondition: returned Insts are zonked checkLoop env wanteds - = do { -- Givens are skolems, so no need to zonk them - wanteds' <- mappM zonkInst wanteds + = go env wanteds [] + where go env wanteds needed_givens + = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv] + ; env' <- zonkRedEnv env + ; wanteds' <- zonkInsts wanteds + + ; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds' - ; (improved, binds, irreds) <- reduceContext env wanteds' + ; let all_needed_givens = needed_givens ++ more_needed_givens + + ; if not improved then + return (irreds, binds, all_needed_givens) + else do + + -- If improvement did some unification, we go round again. + -- We start again with irreds, not wanteds + -- Using an instance decl might have introduced a fresh type variable + -- which might have been unified, so we'd get an infinite loop + -- if we started again with wanteds! See Note [LOOP] + { (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens + ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } } +\end{code} - ; if not improved then - return (irreds, binds) - else do +Note [Zonking RedEnv] +~~~~~~~~~~~~~~~~~~~~~ +It might appear as if the givens in RedEnv are always rigid, but that is not +necessarily the case for programs involving higher-rank types that have class +contexts constraining the higher-rank variables. An example from tc237 in the +testsuite is + + class Modular s a | s -> a + + wim :: forall a w. Integral a + => a -> (forall s. Modular s a => M s w) -> w + wim i k = error "urk" + + test5 :: (Modular s a, Integral a) => M s a + test5 = error "urk" + + test4 = wim 4 test4' + +Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is +quantified further outside. When type checking test4, we have to check +whether the signature of test5 is an instance of + + (forall s. Modular s a => M s w) + +Consequently, we will get (Modular s t_a), where t_a is a TauTv into the +givens. + +Given the FD of Modular in this example, class improvement will instantiate +t_a to 'a', where 'a' is the skolem from test5's signatures (due to the +Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in +the givens, we will get into a loop as improveOne uses the unification engine +TcGadt.tcUnifyTys, which doesn't know about mutable type variables. - -- If improvement did some unification, we go round again. - -- We start again with irreds, not wanteds - -- Using an instance decl might have introduced a fresh type variable - -- which might have been unified, so we'd get an infinite loop - -- if we started again with wanteds! See Note [LOOP] - { (irreds1, binds1) <- checkLoop env irreds - ; return (irreds1, binds `unionBags` binds1) } } -\end{code} Note [LOOP] ~~~~~~~~~~~ @@ -1126,7 +1229,8 @@ tcSimplifySuperClasses -> [Inst] -- Wanted -> TcM TcDictBinds tcSimplifySuperClasses loc givens sc_wanteds - = do { (irreds, binds1) <- checkLoop env 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 } @@ -1253,7 +1357,8 @@ tcSimplifyRestricted -- Used for restricted binding groups tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- Zonk everything in sight - = do { wanteds' <- mappM zonkInst wanteds + = do { traceTc (text "tcSimplifyRestricted") + ; wanteds' <- zonkInsts wanteds -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type @@ -1265,12 +1370,12 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) - ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' + ; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds' -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) ; gbl_tvs' <- tcGetGlobalTyVars - ; constrained_dicts' <- mappM zonkInst constrained_dicts + ; constrained_dicts' <- zonkInsts constrained_dicts ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs' -- As in tcSimplifyInfer @@ -1314,7 +1419,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds (is_nested_group || isDict inst) = Stop | otherwise = ReduceMe AddSCs env = mkNoImproveRedEnv doc try_me - ; (_imp, binds, irreds) <- reduceContext env wanteds' + ; (_imp, binds, irreds, _) <- reduceContext env wanteds' -- See "Notes on implicit parameters, Question 4: top level" ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured @@ -1404,7 +1509,8 @@ tcSimplifyRuleLhs wanteds -- to fromInteger; this looks fragile to me ; lookup_result <- lookupSimpleInst w' ; case lookup_result of - GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws) + GenInst ws' rhs -> + go dicts (addInstToDictBind binds w rhs) (ws' ++ ws) NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) } \end{code} @@ -1457,12 +1563,12 @@ tcSimplifyIPs :: [Inst] -- The implicit parameters bound here -- makes them the same. tcSimplifyIPs given_ips wanteds - = do { wanteds' <- mappM zonkInst wanteds - ; given_ips' <- mappM zonkInst given_ips + = do { wanteds' <- zonkInsts wanteds + ; given_ips' <- zonkInsts given_ips -- Unusually for checking, we *must* zonk the given_ips ; let env = mkRedEnv doc try_me given_ips' - ; (improved, binds, irreds) <- reduceContext env wanteds' + ; (improved, binds, irreds, _) <- reduceContext env wanteds' ; if not improved then ASSERT( all is_free irreds ) @@ -1522,12 +1628,11 @@ bindInstsOfLocalFuns wanteds local_ids returnM emptyLHsBinds | otherwise - = do { (irreds, binds) <- checkLoop env for_me + = do { (irreds, binds) <- gentleInferLoop doc for_me ; extendLIEs not_for_me ; extendLIEs irreds ; return binds } where - env = mkRedEnv doc try_me [] doc = text "bindInsts" <+> ppr local_ids overloaded_ids = filter is_overloaded local_ids is_overloaded id = isOverloadedTy (idType id) @@ -1536,8 +1641,6 @@ bindInstsOfLocalFuns wanteds local_ids overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them -- so it's worth building a set, so that -- lookup (in isMethodFor) is faster - try_me inst | isMethod inst = ReduceMe NoSCs - | otherwise = Stop \end{code} @@ -1557,6 +1660,8 @@ data RedEnv , red_givens :: [Inst] -- All guaranteed rigid -- Always dicts -- but see Note [Rigidity] + , red_reft :: Refinement -- The refinement to apply to the 'givens' + -- You should think of it as 'given equalities' , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg) -- See Note [RedStack] } @@ -1578,14 +1683,17 @@ data RedEnv mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv mkRedEnv doc try_me givens = RedEnv { red_doc = doc, red_try_me = try_me, - red_givens = givens, red_stack = (0,[]), + red_givens = givens, + red_reft = emptyRefinement, + red_stack = (0,[]), red_improve = True } mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv -- Do not do improvement; no givens mkNoImproveRedEnv doc try_me = RedEnv { red_doc = doc, red_try_me = try_me, - red_givens = [], red_stack = (0,[]), + red_givens = [], red_reft = emptyRefinement, + red_stack = (0,[]), red_improve = True } data WhatToDo @@ -1603,21 +1711,41 @@ data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses -- of a predicate when adding it to the avails -- The reason for this flag is entirely the super-class loop problem -- Note [SUPER-CLASS LOOP 1] + +zonkRedEnv :: RedEnv -> TcM RedEnv +zonkRedEnv env + = do { givens' <- mappM zonkInst (red_givens env) + ; return $ env {red_givens = givens'} + } \end{code} + %************************************************************************ %* * \subsection[reduce]{@reduce@} %* * %************************************************************************ +Note [Ancestor Equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +During context reduction, we add to the wanted equalities also those +equalities that (transitively) occur in superclass contexts of wanted +class constraints. Consider the following code + + class a ~ Int => C a + instance C Int + +If (C a) is wanted, we want to add (a ~ Int), which will be discharged by +substituting Int for a. Hence, we ultimately want (C Int), which we +discharge with the explicit instance. \begin{code} reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, TcDictBinds, -- Dictionary bindings - [Inst]) -- Irreducible + [Inst], -- Irreducible + [Inst]) -- Needed givens reduceContext env wanteds = do { traceTc (text "reduceContext" <+> (vcat [ @@ -1628,32 +1756,112 @@ reduceContext env wanteds text "----------------------" ])) - -- Build the Avail mapping from "givens" - ; init_state <- foldlM addGiven emptyAvails (red_givens env) - -- Do the real work - -- Process non-implication constraints first, so that they are - -- available to help solving the implication constraints - -- ToDo: seems a bit inefficient and ad-hoc - ; let (implics, rest) = partition isImplicInst wanteds - ; avails <- reduceList env (rest ++ implics) init_state - - ; let improved = availsImproved avails - ; (binds, irreds) <- extractResults avails wanteds + ; let givens = red_givens env + (given_eqs0, given_dicts0) = partition isEqInst givens + (wanted_eqs0, wanted_dicts0) = partition isEqInst wanteds + + -- We want to add as wanted equalities those that (transitively) + -- occur in superclass contexts of wanted class constraints. + -- See Note [Ancestor Equalities] + ; ancestor_eqs <- ancestorEqualities wanted_dicts0 + ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs + ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs + + -- 1. Normalise the *given* *equality* constraints + ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0 + + -- 2. Normalise the *given* *dictionary* constraints + -- wrt. the toplevel and given equations + ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs + given_dicts0 + + -- 5. Build the Avail mapping from "given_dicts" + -- Add dicts refined by the current type refinement + ; (init_state, extra_givens) <- getLIE $ do + { init_state <- foldlM addGiven emptyAvails given_dicts + ; let reft = red_reft env + ; if isEmptyRefinement reft then return init_state + else foldlM (addRefinedGiven reft) + init_state given_dicts } + + -- *** ToDo: what to do with the "extra_givens"? For the + -- moment I'm simply discarding them, which is probably wrong + + -- 7. Normalise the *wanted* *dictionary* constraints + -- wrt. the toplevel and given equations + -- NB: normalisation includes zonking as part of what it does + -- so it's important to do it after any unifications + -- that happened as a result of the addGivens + ; (wanted_dicts,normalise_binds1) <- normaliseWantedDicts given_eqs wanted_dicts0 + + -- 6. Solve the *wanted* *dictionary* constraints + -- This may expose some further equational constraints... + ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state) + ; let (binds, irreds1, needed_givens) = extractResults avails wanted_dicts + ; traceTc $ text "reduceContext extractresults" <+> vcat + [ppr avails,ppr wanted_dicts,ppr binds,ppr needed_givens] + + -- *** ToDo: what to do with the "extra_eqs"? For the + -- moment I'm simply discarding them, which is probably wrong + + -- 3. Solve the *wanted* *equation* constraints + ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs + + -- 4. Normalise the *wanted* equality constraints with respect to + -- each other + ; eq_irreds <- normaliseWantedEqs eq_irreds0 + + -- 8. Substitute the wanted *equations* in the wanted *dictionaries* + ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1 + + -- 9. eliminate the artificial skolem constants introduced in 1. + ; eliminate_skolems + + -- Figure out whether we should go round again + -- My current plan is to see if any of the mutable tyvars in + -- givens or irreds has been filled in by improvement. + -- If so, there is merit in going around again, because + -- we may make further progress + -- + -- ToDo: is it only mutable stuff? We may have exposed new + -- equality constraints and should probably go round again + -- then as well. But currently we are dropping them on the + -- floor anyway. + + ; let all_irreds = irreds ++ eq_irreds + ; improved <- anyM isFilledMetaTyVar $ varSetElems $ + tyVarsOfInsts (givens ++ all_irreds) + + -- The old plan (fragile) + -- improveed = availsImproved avails + -- || (not $ isEmptyBag normalise_binds1) + -- || (not $ isEmptyBag normalise_binds2) + -- || (any isEqInst irreds) ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", red_doc env, - text "given" <+> ppr (red_givens env), + text "given" <+> ppr givens, + text "given_eqs" <+> ppr given_eqs, text "wanted" <+> ppr wanteds, + text "wanted_dicts" <+> ppr wanted_dicts, text "----", text "avails" <+> pprAvails avails, text "improved =" <+> ppr improved, - text "irreds = " <+> ppr irreds, + text "(all) irreds = " <+> ppr all_irreds, + text "binds = " <+> ppr binds, + text "needed givens = " <+> ppr needed_givens, text "----------------------" ])) - ; return (improved, binds, irreds) } + ; return (improved, + given_binds `unionBags` normalise_binds1 + `unionBags` normalise_binds2 + `unionBags` binds, + all_irreds, + needed_givens) + } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone tcImproveOne avails inst @@ -1702,7 +1910,8 @@ The main context-reduction function is @reduce@. Here's its game plan. \begin{code} reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state - = do { dopts <- getDOpts + = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state)) + ; dopts <- getDOpts #ifdef DEBUG ; if n > 8 then dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) @@ -1722,34 +1931,37 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state reduce env wanted avails -- It's the same as an existing inst, or a superclass thereof | Just avail <- findAvail avails wanted - = returnM avails + = do { traceTc (text "reduce: found " <+> ppr wanted) + ; returnM avails + } | otherwise - = case red_try_me env wanted of { - ; Stop -> try_simple (addIrred NoSCs) -- See Note [No superclasses for Stop] - - ; ReduceMe want_scs -> -- It should be reduced - reduceInst env avails wanted `thenM` \ (avails, lookup_result) -> - case lookup_result of - NoInstance -> -- No such instance! + = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails) + ; case red_try_me env wanted of { + Stop -> try_simple (addIrred NoSCs); + -- See Note [No superclasses for Stop] + + ReduceMe want_scs -> do -- It should be reduced + { (avails, lookup_result) <- reduceInst env avails wanted + ; case lookup_result of + NoInstance -> addIrred want_scs avails wanted -- Add it and its superclasses - addIrred want_scs avails wanted + + GenInst [] rhs -> addWanted want_scs avails wanted rhs [] - GenInst [] rhs -> addWanted want_scs avails wanted rhs [] - - GenInst wanteds' rhs -> do { avails1 <- addIrred NoSCs avails wanted - ; avails2 <- reduceList env wanteds' avails1 - ; addWanted want_scs avails2 wanted rhs wanteds' } + GenInst wanteds' rhs + -> do { avails1 <- addIrred NoSCs avails wanted + ; avails2 <- reduceList env wanteds' avails1 + ; addWanted want_scs 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 -- needs. See note [RECURSIVE DICTIONARIES] -- NB: we must not do an addWanted before, because that adds the - -- superclasses too, and thaat can lead to a spurious loop; see + -- superclasses too, and that can lead to a spurious loop; see -- the examples in [SUPERCLASS-LOOP] -- So we do an addIrred before, and then overwrite it afterwards with addWanted - - } + } } where -- First, see if the inst can be reduced to a constant in one step -- Works well for literals (1::Int) and constant dictionaries (d::Num Int) @@ -1849,19 +2061,46 @@ contributing clauses. \begin{code} --------------------------------------------- reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult) -reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc, +reduceInst env avails (ImplicInst { tci_name = name, + tci_tyvars = tvs, tci_reft = reft, tci_loc = loc, tci_given = extra_givens, tci_wanted = wanteds }) - = reduceImplication env avails reft tvs extra_givens wanteds loc + = reduceImplication env avails name reft tvs extra_givens wanteds loc reduceInst env avails other_inst = do { result <- lookupSimpleInst other_inst ; return (avails, result) } \end{code} +Note [Equational Constraints in Implication Constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +An implication constraint is of the form + Given => Wanted +where Given and Wanted may contain both equational and dictionary +constraints. The delay and reduction of these two kinds of constraints +is distinct: + +-) In the generated code, wanted Dictionary constraints are wrapped up in an + implication constraint that is created at the code site where the wanted + dictionaries can be reduced via a let-binding. This let-bound implication + constraint is deconstructed at the use-site of the wanted dictionaries. + +-) While the reduction of equational constraints is also delayed, the delay + is not manifest in the generated code. The required evidence is generated + in the code directly at the use-site. There is no let-binding and deconstruction + necessary. The main disadvantage is that we cannot exploit sharing as the + same evidence may be generated at multiple use-sites. However, this disadvantage + is limited because it only concerns coercions which are erased. + +The different treatment is motivated by the different in representation. Dictionary +constraints require manifest runtime dictionaries, while equations require coercions +which are types. + \begin{code} --------------------------------------------- reduceImplication :: RedEnv -> Avails + -> Name -> Refinement -- May refine the givens; often empty -> [TcTyVar] -- Quantified type variables; all skolems -> [Inst] -- Extra givens; all rigid @@ -1892,61 +2131,130 @@ Note that \begin{code} -- ToDo: should we instantiate tvs? I think it's not necessary -- - -- ToDo: what about improvement? There may be some improvement - -- exposed as a result of the simplifications done by reduceList - -- which are discarded if we back off. - -- This is almost certainly Wrong, but we'll fix it when dealing - -- better with equality constraints -reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc + -- Note on coercion variables: + -- + -- The extra given coercion variables are bound at two different sites: + -- -) in the creation context of the implication constraint + -- the solved equational constraints use these binders + -- + -- -) at the solving site of the implication constraint + -- the solved dictionaries use these binders + -- these binders are generated by reduceImplication + -- +reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc = do { -- Add refined givens, and the extra givens - (refined_red_givens, avails) - <- if isEmptyRefinement reft then return (red_givens env, orig_avails) - else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env) - ; avails <- foldlM addGiven avails extra_givens + -- Todo fix this +-- (refined_red_givens,refined_avails) +-- <- if isEmptyRefinement reft then return (red_givens env,orig_avails) +-- else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env) +-- Commented out SLPJ Sept 07; see comment with extractLocalResults below + let refined_red_givens = [] -- Solve the sub-problem ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications] - env' = env { red_givens = refined_red_givens ++ extra_givens + env' = env { red_givens = extra_givens ++ availsInsts orig_avails + , red_reft = reft + , red_doc = sep [ptext SLIT("reduceImplication for") <+> ppr name, + nest 2 (parens $ ptext SLIT("within") <+> red_doc env)] , red_try_me = try_me } ; traceTc (text "reduceImplication" <+> vcat [ ppr orig_avails, ppr (red_givens env), ppr extra_givens, - ppr reft, ppr wanteds, ppr avails ]) - ; avails <- reduceList env' wanteds avails + ppr reft, ppr wanteds]) + ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds + ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens + -- SLPJ Sept 07: I think this is bogus; currently + -- there are no Eqinsts in extra_givens + dict_ids = map instToId extra_dict_givens + + -- needed_givens0 is the free vars of the bindings + -- Remove the ones we are going to lambda-bind + -- Use the actual dictionary identity *not* equality on Insts + -- (Mind you, it should make no difference here.) + ; let needed_givens = [ng | ng <- needed_givens0 + , instToVar ng `notElem` dict_ids] - -- Extract the results -- Note [Reducing implication constraints] - ; (binds, irreds) <- extractResults avails wanteds - ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds + -- Tom -- update note, put somewhere! ; traceTc (text "reduceImplication result" <+> vcat - [ ppr outer, ppr inner, ppr binds]) + [ppr irreds, ppr binds, ppr needed_givens]) + + ; -- extract superclass binds + -- (sc_binds,_) <- extractResults avails [] +-- ; traceTc (text "reduceImplication sc_binds" <+> vcat +-- [ppr sc_binds, ppr avails]) +-- -- We always discard the extra avails we've generated; -- but we remember if we have done any (global) improvement - ; let ret_avails = updateImprovement orig_avails avails +-- ; let ret_avails = avails + ; let ret_avails = orig_avails +-- ; let ret_avails = updateImprovement orig_avails avails + + -- SLPJ Sept 07: what if improvement happened inside the checkLoop? + -- Then we must iterate the outer loop too! - ; if isEmptyLHsBinds binds && null outer then -- No progress + ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds))) + +-- Progress is no longer measered by the number of bindings + ; if (isEmptyLHsBinds binds) && (not $ null irreds) then -- No progress + -- If there are any irreds, we back off and return NoInstance return (ret_avails, NoInstance) else do - { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner - - ; let dict_ids = map instToId extra_givens - co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) + { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds + -- This binding is useless if the recursive simplification + -- made no progress; but currently we don't try to optimise that + -- case. After all, we only try hard to reduce at top level, or + -- when inferring types. + + ; let dict_wanteds = filter (not . isEqInst) wanteds + -- TOMDO: given equational constraints bug! + -- we need a different evidence for given + -- equations depending on whether we solve + -- dictionary constraints or equational constraints + + eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens + -- SLPJ Sept07: this looks Utterly Wrong to me, but I think + -- that current extra_givens has no EqInsts, so + -- it makes no difference + co = wrap_inline -- Note [Always inline implication constraints] + <.> mkWpTyLams tvs + <.> mkWpTyLams eq_tyvars + <.> mkWpLams dict_ids + <.> WpLet (binds `unionBags` bind) + wrap_inline | null dict_ids = idHsWrapper + | otherwise = WpInline rhs = mkHsWrap co payload loc = instLocSpan inst_loc - payload | [wanted] <- wanteds = HsVar (instToId wanted) - | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed + payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted) + | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed - ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs)) - } } + + ; traceTc (vcat [text "reduceImplication" <+> ppr name, + ppr implic_insts, + text "->" <+> sep [ppr needed_givens, ppr rhs]]) + ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs)) + } + } \end{code} +Note [Always inline implication constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose an implication constraint floats out of an INLINE function. +Then although the implication has a single call site, it won't be +inlined. And that is bad because it means that even if there is really +*no* overloading (type signatures specify the exact types) there will +still be dictionary passing in the resulting code. To avert this, +we mark the implication constraints themselves as INLINE, at least when +there is no loss of sharing as a result. + Note [Reducing implication constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we are trying to simplify - (Ord a, forall b. C a b => (W [a] b, D c b)) + ( do: Ord a, + ic: (forall b. C a b => (W [a] b, D c b)) ) where instance (C a b, Ord a) => W [a] b When solving the implication constraint, we'll start with @@ -1954,16 +2262,26 @@ When solving the implication constraint, we'll start with in the Avails. Then we add (C a b -> Given) and solve. Extracting the results gives us a binding for the (W [a] b), with an Irred of (Ord a, D c b). Now, the (Ord a) comes from "outside" the implication, -but the (D d b) is from "inside". So we want to generate a Rhs binding +but the (D d b) is from "inside". So we want to generate a GenInst like this - ic = /\b \dc:C a b). (df a b dc do, ic' b dc) - depending on - do :: Ord a - ic' :: forall b. C a b => D c b + ic = GenInst + [ do :: Ord a, + ic' :: forall b. C a b => D c b] + (/\b \(dc:C a b). (df a b dc do, ic' b dc)) + +The first arg of GenInst gives the free dictionary variables of the +second argument -- the "needed givens". And that list in turn is +vital because it's used to determine what other dicts must be solved. +This very list ends up in the second field of the Rhs, and drives +extractResults. + +The need for this field is why we have to return "needed givens" +from extractResults, reduceContext, checkLoop, and so on. -The 'depending on' part of the Rhs is important, because it drives -the extractResults code. +NB: the "needed givens" in a GenInst or Rhs, may contain two dicts +with the same type but different Ids, e.g. [d12 :: Eq a, d81 :: Eq a] +That says we must generate a binding for both d12 and d81. The "inside" and "outside" distinction is what's going on with 'inner' and 'outer' in reduceImplication @@ -2027,7 +2345,7 @@ data AvailHow = IsIrred -- Used for irreducible dictionaries, -- which are going to be lambda bound - | Given TcId -- Used for dictionaries for which we have a binding + | Given Inst -- Used for dictionaries for which we have a binding -- e.g. those "given" in a signature | Rhs -- Used when there is a RHS @@ -2039,8 +2357,9 @@ instance Outputable Avails where pprAvails (Avails imp avails) = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty) - , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)] - | (inst,avail) <- fmToList avails ])] + , nest 2 $ braces $ + vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)] + | (inst,avail) <- fmToList avails ]] instance Outputable AvailHow where ppr = pprAvail @@ -2049,7 +2368,8 @@ instance Outputable AvailHow where pprAvail :: AvailHow -> SDoc pprAvail IsIrred = text "Irred" pprAvail (Given x) = text "Given" <+> ppr x -pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)] +pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs, + nest 2 (ppr rhs)] ------------------------- extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv @@ -2092,46 +2412,56 @@ We assume that they'll be wrapped in a big Rec, so that the dependency analyser can sort them out later \begin{code} +type DoneEnv = FiniteMap Inst [Id] +-- Tracks which things we have evidence for + extractResults :: Avails -> [Inst] -- Wanted - -> TcM ( TcDictBinds, -- Bindings - [Inst]) -- Irreducible ones + -> (TcDictBinds, -- Bindings + [Inst], -- Irreducible ones + [Inst]) -- Needed givens, i.e. ones used in the bindings + -- Postcondition: needed-givens = free vars( binds ) \ irreds + -- needed-gives is subset of Givens in incoming Avails + -- Note [Reducing implication constraints] extractResults (Avails _ avails) wanteds - = go avails emptyBag [] wanteds + = go emptyBag [] [] emptyFM wanteds where - go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] - -> TcM (TcDictBinds, [Inst]) - go avails binds irreds [] - = returnM (binds, irreds) - - go avails binds irreds (w:ws) + go :: TcDictBinds -- Bindings for dicts + -> [Inst] -- Irreds + -> [Inst] -- Needed givens + -> DoneEnv -- Has an entry for each inst in the above three sets + -> [Inst] -- Wanted + -> (TcDictBinds, [Inst], [Inst]) + go binds irreds givens done [] + = (binds, irreds, givens) + + go binds irreds givens done (w:ws) + | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w + = if w_id `elem` done_ids then + go binds irreds givens done ws + else + go (add_bind (nlHsVar done_id)) irreds givens + (addToFM done w (done_id : w_id : rest_done_ids)) ws + + | otherwise -- Not yet done = case findAvailEnv avails w of Nothing -> pprTrace "Urk: extractResults" (ppr w) $ - go avails binds irreds ws - - Just (Given id) - | id == w_id -> go avails binds irreds ws - | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws - -- The sought Id can be one of the givens, via a superclass chain - -- and then we definitely don't want to generate an x=x binding! - - Just IsIrred -> go (add_given avails w) binds (w:irreds) ws - -- The add_given handles the case where we want (Ord a, Eq a), and we - -- don't want to emit *two* Irreds for Ord a, one via the superclass chain - -- This showed up in a dupliated Ord constraint in the error message for - -- test tcfail043 - - Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws) - where - new_binds = addBind binds w_id rhs - where - w_id = instToId w + go binds irreds givens done ws + + Just IsIrred -> go binds (w:irreds) givens done' ws - add_given avails w = extendAvailEnv avails w (Given (instToId w)) - -- Don't add the same binding twice + Just (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws) -addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs)) + Just (Given g) -> go binds' irreds (g:givens) (addToFM done w [g_id]) ws + where + g_id = instToId g + binds' | w_id == g_id = binds + | otherwise = add_bind (nlHsVar g_id) + where + w_id = instToId w + done' = addToFM done w [w_id] + add_bind rhs = addInstToDictBind binds w rhs \end{code} @@ -2153,15 +2483,15 @@ addWanted want_scs avails wanted rhs_expr wanteds avail = Rhs rhs_expr wanteds addGiven :: Avails -> Inst -> TcM Avails -addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given)) +addGiven avails given = addAvailAndSCs AddSCs avails given (Given given) -- Always add superclasses for 'givens' -- -- 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', -- so the assert isn't true -addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails) -addRefinedGiven reft (refined_givens, avails) given +addRefinedGiven :: Refinement -> Avails -> Inst -> TcM Avails +addRefinedGiven reft avails given | isDict given -- We sometimes have 'given' methods, but they -- are always optional, so we can drop them , let pred = dictPred given @@ -2170,13 +2500,12 @@ addRefinedGiven reft (refined_givens, avails) given = do { new_given <- newDictBndr (instLoc given) pred ; let rhs = L (instSpan given) $ HsWrap (WpCo co) (HsVar (instToId given)) - ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given]) - ; return (new_given:refined_givens, avails) } + ; addAvailAndSCs AddSCs avails new_given (Rhs rhs [given]) } -- ToDo: the superclasses of the original given all exist in Avails -- so we could really just cast them, but it's more awkward to do, -- and hopefully the optimiser will spot the duplicated work | otherwise - = return (refined_givens, avails) + = return avails \end{code} Note [ImplicInst rigidity] @@ -2215,7 +2544,7 @@ addAvailAndSCs want_scs avails inst avail where is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys -- Note: this compares by *type*, not by Unique - deps = findAllDeps (unitVarSet (instToId inst)) avail + deps = findAllDeps (unitVarSet (instToVar inst)) avail dep_tys = map idType (varSetElems deps) findAllDeps :: IdSet -> AvailHow -> IdSet @@ -2228,6 +2557,7 @@ addAvailAndSCs want_scs avails inst avail find_all :: IdSet -> Inst -> IdSet find_all so_far kid + | isEqInst kid = so_far | kid_id `elemVarSet` so_far = so_far | Just avail <- findAvail avails kid = findAllDeps so_far' avail | otherwise = so_far' @@ -2237,7 +2567,7 @@ addAvailAndSCs want_scs avails inst avail addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails -- Add all the superclasses of the Inst to Avails - -- The first param says "dont do this because the original thing + -- The first param says "don't do this because the original thing -- depends on this one, so you'd build a loop" -- Invariant: the Inst is already in Avails. @@ -2248,7 +2578,8 @@ addSCs is_loop avails dict where (clas, tys) = getDictClassTys dict (tyvars, sc_theta, sc_sels, _) = classBigSig clas - sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta + sc_theta' = filter (not . isEqPred) $ + substTheta (zipTopTvSubst tyvars tys) sc_theta add_sc avails (sc_dict, sc_sel) | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2] @@ -2257,14 +2588,41 @@ addSCs is_loop avails dict ; addSCs is_loop avails' sc_dict } where sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel)) - co_fn = WpApp (instToId dict) <.> mkWpTyApps tys + co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys is_given :: Inst -> Bool is_given sc_dict = case findAvail avails sc_dict of Just (Given _) -> True -- Given is cheaper than superclass selection other -> False + +-- From the a set of insts obtain all equalities that (transitively) occur in +-- superclass contexts of class constraints (aka the ancestor equalities). +-- +ancestorEqualities :: [Inst] -> TcM [Inst] +ancestorEqualities + = mapM mkWantedEqInst -- turn only equality predicates.. + . filter isEqPred -- ..into wanted equality insts + . bagToList + . addAEsToBag emptyBag -- collect the superclass constraints.. + . map dictPred -- ..of all predicates in a bag + . filter isClassDict + where + addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType + addAEsToBag bag [] = bag + addAEsToBag bag (pred:preds) + | pred `elemBag` bag = addAEsToBag bag preds + | isEqPred pred = addAEsToBag bagWithPred preds + | isClassPred pred = addAEsToBag bagWithPred predsWithSCs + | otherwise = addAEsToBag bag preds + where + bagWithPred = bag `snocBag` pred + predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta + -- + (tyvars, sc_theta, _, _) = classBigSig clas + (clas, tys) = getClassPredTys pred \end{code} + %************************************************************************ %* * \section{tcSimplifyTop: defaulting} @@ -2301,11 +2659,15 @@ tcSimplifyInteractive wanteds -- error message generation for the monomorphism restriction tc_simplify_top doc interactive wanteds = do { dflags <- getDOpts - ; wanteds <- mapM zonkInst wanteds + ; wanteds <- zonkInsts wanteds ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds)) + ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds) ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds +-- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds + ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1) ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1 + ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2) -- Use the defaulting rules to do extra unification -- NB: irreds2 are already zonked @@ -2368,7 +2730,7 @@ disambiguate doc interactive dflags insts = return (insts, emptyBag) | null defaultable_groups - = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups]) + = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups]) ; return (insts, emptyBag) } | otherwise @@ -2431,7 +2793,7 @@ disambigGroup :: [Type] -- The default types disambigGroup default_tys dicts = try_default default_tys where - (_,_,tyvar) = head dicts -- Should be non-empty + (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty classes = [c | (_,c,_) <- dicts] try_default [] = return () @@ -2446,7 +2808,9 @@ disambigGroup default_tys dicts -- After this we can't fail ; warnDefault dicts default_ty - ; unifyType default_ty (mkTyVarTy tyvar) } + ; unifyType default_ty (mkTyVarTy tyvar) + ; return () -- TOMDO: do something with the coercion + } ----------------------- @@ -2522,7 +2886,6 @@ tcSimplifyDeriv :: InstOrigin -> TcM ThetaType -- Needed -- Given instance (wanted) => C inst_ty -- Simplify 'wanted' as much as possible --- The inst_ty is needed only for the termination check tcSimplifyDeriv orig tyvars theta = do { (tvs, _, tenv) <- tcInstTyVars tyvars @@ -2532,8 +2895,9 @@ tcSimplifyDeriv orig tyvars theta ; wanteds <- newDictBndrsO orig (substTheta tenv theta) ; (irreds, _) <- tryHardCheckLoop doc wanteds - ; let (tv_dicts, others) = partition isTyVarDict irreds + ; let (tv_dicts, others) = partition ok irreds ; addNoInstanceErrs others + -- See Note [Exotic derived instance contexts] in TcMType ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars) simpl_theta = substTheta rev_env (map dictPred tv_dicts) @@ -2543,49 +2907,10 @@ tcSimplifyDeriv orig tyvars theta ; return simpl_theta } where doc = ptext SLIT("deriving classes for a data type") -\end{code} - -Note [Exotic derived instance contexts] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data T a b c = MkT (Foo a b c) deriving( Eq ) - instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) - -Notice that this instance (just) satisfies the Paterson termination -conditions. Then we *could* derive an instance decl like this: - - instance (C Int a, Eq b, Eq c) => Eq (T a b c) -even though there is no instance for (C Int a), because there just -*might* be an instance for, say, (C Int Bool) at a site where we -need the equality instance for T's. - -However, this seems pretty exotic, and it's quite tricky to allow -this, and yet give sensible error messages in the (much more common) -case where we really want that instance decl for C. - -So for now we simply require that the derived instance context -should have only type-variable constraints. - -Here is another example: - data Fix f = In (f (Fix f)) deriving( Eq ) -Here, if we are prepared to allow -fallow-undecidable-instances we -could derive the instance - instance Eq (f (Fix f)) => Eq (Fix f) -but this is so delicate that I don't think it should happen inside -'deriving'. If you want this, write it yourself! - -NB: if you want to lift this condition, make sure you still meet the -termination conditions! If not, the deriving mechanism generates -larger and larger constraints. Example: - data Succ a = S a - data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show - -Note the lack of a Show instance for Succ. First we'll generate - instance (Show (Succ a), Show a) => Show (Seq a) -and then - instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) -and so on. Instead we want to complain of no instance for (Show (Succ a)). + ok dict | isDict dict = validDerivPred (dictPred dict) + | otherwise = False +\end{code} @tcSimplifyDefault@ just checks class-type constraints, essentially; @@ -2603,7 +2928,7 @@ tcSimplifyDefault theta if null irreds then returnM () else - failM + traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM where doc = ptext SLIT("default declaration") \end{code} @@ -2627,11 +2952,10 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group -- We want to report them together in error messages groupErrs report_err [] - = returnM () + = return () groupErrs report_err (inst:insts) - = do_one (inst:friends) `thenM_` - groupErrs report_err others - + = do { do_one (inst:friends) + ; groupErrs report_err others } where -- (It may seem a bit crude to compare the error messages, -- but it makes sure that we combine just what the user sees, @@ -2691,14 +3015,17 @@ reportNoInstances tidy_env mb_what insts = groupErrs (report_no_instances tidy_env mb_what) insts report_no_instances tidy_env mb_what insts - = do { inst_envs <- tcGetInstEnvs - ; let (implics, insts1) = partition isImplicInst insts - (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1 - ; traceTc (text "reportNoInstnces" <+> vcat - [ppr implics, ppr insts1, ppr insts2]) - ; mapM_ complain_implic implics - ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps - ; groupErrs complain_no_inst insts2 } + = do { inst_envs <- tcGetInstEnvs + ; let (implics, insts1) = partition isImplicInst insts + (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1 + (eqInsts, insts3) = partition isEqInst insts2 + ; traceTc (text "reportNoInstances" <+> vcat + [ppr insts, ppr implics, ppr insts1, ppr insts2]) + ; mapM_ complain_implic implics + ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps + ; groupErrs complain_no_inst insts3 + ; mapM_ (addErrTcM . mk_eq_err) eqInsts + } where complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts) @@ -2714,9 +3041,9 @@ report_no_instances tidy_env mb_what insts | not (isClassDict wanted) = Left wanted | otherwise = case lookupInstEnv inst_envs clas tys of - -- The case of exactly one match and no unifiers means - -- a successful lookup. That can't happen here, becuase - -- dicts only end up here if they didn't match in Inst.lookupInst + -- The case of exactly one match and no unifiers means a + -- successful lookup. That can't happen here, because dicts + -- only end up here if they didn't match in Inst.lookupInst #ifdef DEBUG ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted) #endif @@ -2739,10 +3066,13 @@ report_no_instances tidy_env mb_what insts parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+> quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))), ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"), - ptext SLIT("when compiling the other instances")])] + ptext SLIT("when compiling the other instance declarations")])] where ispecs = [ispec | (ispec, _) <- matches] + mk_eq_err :: Inst -> (TidyEnv, SDoc) + mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst) + mk_no_inst_err insts | null insts = empty @@ -2828,10 +3158,6 @@ mkMonomorphismMsg tidy_env inst_tvs nest 2 (vcat docs), monomorphism_fix dflags] -isRuntimeUnk :: TcTyVar -> Bool -isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True - | otherwise = False - monomorphism_fix :: DynFlags -> SDoc monomorphism_fix dflags = ptext SLIT("Probable fix:") <+> vcat