X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=0516308c5d91ba05a0c3e5134e1b810edac24f29;hb=6bb651084a0ebd572739ab9319c800c6ad83eb56;hp=62a71515ab60ac7c8b18660c98cc0b797bdeb949;hpb=25f84fa7e4b84c3db5ba745a7881c009b778e0b1;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 62a7151..0516308 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -411,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'. @@ -776,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 @@ -945,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 @@ -982,24 +989,23 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs reft - givens -- Guaranteed all Dicts (TOMDO: true?) + 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) = partitionGivenEqInsts givens + ; let (eq_givens, dict_givens) = partition isEqInst givens eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens ; let name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_reft = reft, tci_tyvars = all_tvs, tci_given = (eq_givens ++ dict_givens), tci_wanted = irreds, tci_loc = loc } - ; let - -- only create binder for dict_irreds - -- we - (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds + ; 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) @@ -1044,6 +1050,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] @@ -1061,7 +1077,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 @@ -1082,10 +1098,11 @@ checkLoop :: RedEnv checkLoop env wanteds = go env wanteds [] where go env wanteds needed_givens - = do { -- Givens are skolems, so no need to zonk them - wanteds' <- zonkInsts wanteds + = 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, more_needed_givens) <- reduceContext env' wanteds' ; let all_needed_givens = needed_givens ++ more_needed_givens @@ -1098,10 +1115,44 @@ checkLoop env 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 + { (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } } \end{code} +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. + + Note [LOOP] ~~~~~~~~~~~ class If b t e r | b t e -> r @@ -1452,7 +1503,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 w rhs) (ws' ++ ws) + GenInst ws' rhs -> + go dicts (addInstToDictBind binds w rhs) (ws' ++ ws) NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) } \end{code} @@ -1570,12 +1622,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) @@ -1584,8 +1635,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} @@ -1605,6 +1654,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] } @@ -1626,14 +1677,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 @@ -1651,14 +1705,33 @@ 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 @@ -1678,54 +1751,57 @@ reduceContext env wanteds ])) - ; let givens = red_givens env - (given_eqs0,given_dicts0) = partitionGivenEqInsts givens - (wanted_eqs0,wanted_dicts) = partitionWantedEqInsts wanteds + ; let givens = red_givens env + (given_eqs0, given_dicts0) = partition isEqInst givens + (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds - ; wanted_ancestor_eqs <- (mapM wantedAncestorEqualities wanted_dicts >>= \ls -> return (concat ls)) - ; traceTc (text "test wanted SCs" <+> ppr wanted_ancestor_eqs) - ; let wanted_eqs = wanted_ancestor_eqs ++ wanted_eqs0 + -- 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_dicts + ; 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) <- normaliseGivens given_eqs0 + -- 1. Normalise the *given* *equality* constraints + ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0 - ; -- 2. Normalise the *given* *dictionary* constraints + -- 2. Normalise the *given* *dictionary* constraints -- wrt. the toplevel and given equations - (given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0 + ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs + given_dicts0 - ; -- 3. Solve the *wanted* *equation* constraints - eq_irreds0 <- solveWanteds given_eqs wanted_eqs + -- 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 <- normaliseWanteds eq_irreds0 - --- -- 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 + -- 4. Normalise the *wanted* equality constraints with respect to + -- each other + ; eq_irreds <- normaliseWantedEqs eq_irreds0 -- 5. Build the Avail mapping from "given_dicts" + -- Add dicts refined by the current type refinement ; init_state <- foldlM addGiven emptyAvails given_dicts + ; let reft = red_reft env + ; init_state <- if isEmptyRefinement reft then return init_state + else foldlM (addRefinedGiven reft) + init_state given_dicts -- 6. Solve the *wanted* *dictionary* constraints -- This may expose some further equational constraints... ; wanted_dicts' <- zonkInsts wanted_dicts ; avails <- reduceList env wanted_dicts' init_state - ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts' - ; traceTc (text "reduceContext extractresults" <+> vcat - [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]) + ; let (binds, irreds0, needed_givens) = extractResults avails wanted_dicts' + ; traceTc $ text "reduceContext extractresults" <+> vcat + [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens] - ; -- 7. Normalise the *wanted* *dictionary* constraints + -- 7. Normalise the *wanted* *dictionary* constraints -- wrt. the toplevel and given equations - (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0 + ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0 - ; -- 8. Substitute the wanted *equations* in the wanted *dictionaries* - (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1 + -- 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 + -- 9. eliminate the artificial skolem constants introduced in 1. + ; eliminate_skolems -- If there was some FD improvement, -- or new wanted equations have been exposed, @@ -1733,7 +1809,7 @@ reduceContext env wanteds ; let improved = availsImproved avails || (not $ isEmptyBag normalise_binds1) || (not $ isEmptyBag normalise_binds2) - || (not $ null $ fst $ partitionGivenEqInsts irreds) + || (any isEqInst irreds) ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", @@ -1749,7 +1825,13 @@ reduceContext env wanteds text "----------------------" ])) - ; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) } + ; return (improved, + given_binds `unionBags` normalise_binds1 + `unionBags` normalise_binds2 + `unionBags` binds, + irreds ++ eq_irreds, + needed_givens) + } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone tcImproveOne avails inst @@ -1798,7 +1880,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) @@ -1811,8 +1894,7 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state go wanteds state } where go [] state = return state - go (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state) - ; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state + go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state ; go ws state' } -- Base case: we're done! @@ -1824,7 +1906,7 @@ reduce env wanted avails } | otherwise - = do { traceTc (text "reduce" <+> ppr avails <+> ppr wanted) + = 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] @@ -1949,9 +2031,10 @@ 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 @@ -1961,7 +2044,7 @@ reduceInst env avails other_inst Note [Equational Constraints in Implication Constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -An equational constraint is of the form +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 @@ -1987,6 +2070,7 @@ which are types. --------------------------------------------- reduceImplication :: RedEnv -> Avails + -> Name -> Refinement -- May refine the givens; often empty -> [TcTyVar] -- Quantified type variables; all skolems -> [Inst] -- Extra givens; all rigid @@ -2027,16 +2111,21 @@ Note that -- the solved dictionaries use these binders -- these binders are generated by reduceImplication -- -reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc +reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc = do { -- Add refined givens, and the 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) +-- (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 ++ availsInsts orig_avails + 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 @@ -2044,20 +2133,23 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds]) ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds - ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_givens] + ; 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] -- Note [Reducing implication constraints] -- Tom -- update note, put somewhere! ; traceTc (text "reduceImplication result" <+> vcat - [ppr irreds, ppr binds, ppr needed_givens1]) --- ; avails <- reduceList env' wanteds avails --- --- -- Extract the binding --- ; (binds, irreds) <- extractResults avails wanteds - ; (refinement_binds,needed_givens) <- extractLocalResults refined_avails needed_givens1 - ; traceTc (text "reduceImplication local results" <+> vcat - [ppr refinement_binds, ppr needed_givens]) + [ppr irreds, ppr binds, ppr needed_givens]) ; -- extract superclass binds -- (sc_binds,_) <- extractResults avails [] @@ -2071,9 +2163,12 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc ; 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! + ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds))) --- Porgress is no longer measered by the number of bindings +-- Progress is no longer measered by the number of bindings -- ; if isEmptyLHsBinds binds then -- No progress ; if (isEmptyLHsBinds binds) && (not $ null irreds) then return (ret_avails, NoInstance) @@ -2086,24 +2181,26 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc -- when inferring types. ; let dict_wanteds = filter (not . isEqInst) wanteds - (extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens - dict_ids = map instToId extra_dict_givens -- 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 = uniqSetToList $ 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 -- dict_ids = map instToId extra_givens - co = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` refinement_binds `unionBags` bind) + co = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind) rhs = mkHsWrap co payload loc = instLocSpan inst_loc payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted) | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed - ; traceTc (text "reduceImplication ->" <+> vcat - [ ppr ret_avails, - ppr implic_insts]) + ; traceTc (vcat [text "reduceImplication" <+> ppr name, + ppr implic_insts, + text "->" <+> sep [ppr needed_givens, ppr rhs]]) -- If there are any irreds, we back off and return NoInstance ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs)) } @@ -2113,7 +2210,8 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc 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 @@ -2121,16 +2219,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 'depending on' part of the Rhs is important, because it drives -the extractResults code. +The need for this field is why we have to return "needed givens" +from extractResults, reduceContext, checkLoop, and so on. + +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 @@ -2194,7 +2302,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 @@ -2206,8 +2314,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 @@ -2216,7 +2325,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 @@ -2259,81 +2369,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 - [Inst]) -- Needed givens, i.e. ones used in the bindings + -> (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] -> [Inst] - -> TcM (TcDictBinds, [Inst], [Inst]) - go avails binds irreds givens [] - = returnM (binds, irreds, givens) - - go avails binds irreds givens (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 givens ws - - Just (Given id) - | id == w_id -> go avails binds irreds (w:givens) ws - | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w id:givens) 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) givens 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 givens (ws' ++ ws) - where - new_binds = addBind binds w rhs - where - w_id = instToId w - update_id m@(Method{}) id = m {tci_id = id} - update_id w id = w {tci_name = idName id} - - add_given avails w = extendAvailEnv avails w (Given (instToId w)) + go binds irreds givens done ws -extractLocalResults :: Avails - -> [Inst] -- Wanted - -> TcM ( TcDictBinds, -- Bindings - [Inst]) -- Needed givens, i.e. ones used in the bindings - -extractLocalResults (Avails _ avails) wanteds - = go avails emptyBag [] wanteds - where - go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] - -> TcM (TcDictBinds, [Inst]) - go avails binds givens [] - = returnM (binds, givens) - - go avails binds givens (w:ws) - = case findAvailEnv avails w of - Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $ - go avails binds givens ws + Just IsIrred -> go binds (w:irreds) givens done' ws - Just IsIrred -> - go avails binds givens ws + Just (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws) - Just (Given id) - | id == w_id -> go avails binds (w:givens) ws - | otherwise -> go avails binds (w{tci_name=idName id}:givens) 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 (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws) - where - new_binds = addBind binds w 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 - - add_given avails w = extendAvailEnv avails w (Given (instToId w)) + w_id = instToId w + done' = addToFM done w [w_id] + add_bind rhs = addInstToDictBind binds w rhs \end{code} @@ -2355,15 +2440,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 @@ -2372,28 +2457,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) } - -- 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) - -addRefinedGiven' :: Refinement -> [Inst] -> Inst -> TcM [Inst] -addRefinedGiven' reft refined_givens given - | isDict given -- We sometimes have 'given' methods, but they - -- are always optional, so we can drop them - , let pred = dictPred given - , isRefineablePred pred -- See Note [ImplicInst rigidity] - , Just (co, pred) <- refinePred reft pred - = do { new_given <- newDictBndr (instLoc given) pred - ; return (new_given:refined_givens) } + ; 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 + = return avails \end{code} Note [ImplicInst rigidity] @@ -2432,7 +2501,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 @@ -2445,6 +2514,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' @@ -2454,7 +2524,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. @@ -2465,7 +2535,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] @@ -2474,39 +2545,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 - -wantedAncestorEqualities :: Inst -> TcM [Inst] -wantedAncestorEqualities dict - | isClassDict dict - = mapM mkWantedEqInst $ filter isEqPred $ bagToList $ wantedAncestorEqualities' (dictPred dict) emptyBag - | otherwise - = return [] - -wantedAncestorEqualities' :: PredType -> Bag PredType -> Bag PredType -wantedAncestorEqualities' pred bag - = ASSERT( isClassPred pred ) - let (clas, tys) = getClassPredTys pred +-- 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 - sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta - add_sc bag sc_pred - | elemBag sc_pred bag = bag - | not (isEqPred sc_pred) - && not (isClassPred sc_pred) - = bag - | isEqPred sc_pred = consBag sc_pred bag - | otherwise = let bag' = consBag sc_pred bag - in wantedAncestorEqualities' sc_pred bag' - in foldl add_sc bag sc_theta' - + (clas, tys) = getClassPredTys pred \end{code} + %************************************************************************ %* * \section{tcSimplifyTop: defaulting} @@ -2548,6 +2621,7 @@ tc_simplify_top doc interactive 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) @@ -2811,7 +2885,7 @@ tcSimplifyDefault theta if null irreds then returnM () else - failM + traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM where doc = ptext SLIT("default declaration") \end{code} @@ -2908,7 +2982,7 @@ report_no_instances tidy_env mb_what insts ; mapM_ complain_implic implics ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps ; groupErrs complain_no_inst insts3 - ; mapM_ complain_eq eqInsts + ; mapM_ eqInstMisMatch eqInsts } where complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts) @@ -2918,13 +2992,6 @@ report_no_instances tidy_env mb_what insts (Just (tci_loc inst, tci_given inst)) (tci_wanted inst) - complain_eq EqInst {tci_left = lty, tci_right = rty, - tci_loc = InstLoc _ _ ctxt} - = do { (env, msg) <- misMatchMsg lty rty - ; setErrCtxt ctxt $ - failWithTcM (env, msg) - } - check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc -- Right msg => overlap message -- Left inst => no instance @@ -3046,10 +3113,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 @@ -3077,59 +3140,4 @@ reduceDepthErr n stack nest 4 (pprStack stack)] pprStack stack = vcat (map pprInstInFull stack) - ------------------------ -misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc) --- Generate the message when two types fail to match, --- going to some trouble to make it helpful. --- The argument order is: actual type, expected type -misMatchMsg ty_act ty_exp - = do { env0 <- tcInitTidyEnv - ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp ty_act - ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ty_exp - ; return (env2, - sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, - nest 7 $ - ptext SLIT("against inferred type") <+> pp_act], - nest 2 (extra_exp $$ extra_act)]) } - -ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc) -ppr_ty env ty other_ty - = do { ty' <- zonkTcType ty - ; let (env1, tidy_ty) = tidyOpenType env ty' - ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty - ; return (env2, quotes (ppr tidy_ty), extra) } - --- (ppr_extra env ty other_ty) shows extra info about 'ty' -ppr_extra env (TyVarTy tv) other_ty - | isSkolemTyVar tv || isSigTyVar tv - = return (env1, pprSkolTvBinding tv1) - where - (env1, tv1) = tidySkolemTyVar env tv - -ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _) - | getOccName tc1 == getOccName tc2 - = -- This case helps with messages that would otherwise say - -- Could not match 'T' does not match 'M.T' - -- which is not helpful - do { this_mod <- getModule - ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) } - where - tc_mod = nameModule (getName tc1) - tc_pkg = modulePackageId tc_mod - tc2_pkg = modulePackageId (nameModule (getName tc2)) - mk_mod this_mod - | tc_mod == this_mod = ptext SLIT("in this module") - - | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg - -- Suppress the module name if (a) it's from another package - -- (b) other_ty isn't from that same package - - | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg - where - home_pkg = tc_pkg == modulePackageId this_mod - pp_pkg | home_pkg = empty - | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg) - -ppr_extra env ty other_ty = return (env, empty) -- Normal case \end{code}