X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=3c7df83c07777fcf3a29d1888e4dddb47b47b9ae;hb=488da9e2096994a3a8dd6d559785c792a4527f73;hp=fbd676f0a6de4b4e12510ad504a6c2fbe4b7f3e9;hpb=3239b75871f923899079e5a3fba6f356bfd15668;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index fbd676f..3c7df83 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -36,6 +36,7 @@ import TcIface import TcTyFuns import DsUtils -- Big-tuple functions import Var +import Id import Name import NameSet import Class @@ -57,7 +58,6 @@ import Util import SrcLoc import DynFlags import FastString - import Control.Monad import Data.List \end{code} @@ -91,34 +91,36 @@ we reduce the (C a b1) constraint from the call of f to (D a b1). Here is a more complicated example: -| > class Foo a b | a->b -| > -| > class Bar a b | a->b -| > -| > data Obj = Obj -| > -| > instance Bar Obj Obj -| > -| > instance (Bar a b) => Foo a b -| > -| > foo:: (Foo a b) => a -> String -| > foo _ = "works" -| > -| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w -| > runFoo f = f Obj -| -| *Test> runFoo foo -| -| :1: -| Could not deduce (Bar a b) from the context (Foo a b) -| arising from use of `foo' at :1 -| Probable fix: -| Add (Bar a b) to the expected type of an expression -| In the first argument of `runFoo', namely `foo' -| In the definition of `it': it = runFoo foo -| -| Why all of the sudden does GHC need the constraint Bar a b? The -| function foo didn't ask for that... +@ + > class Foo a b | a->b + > + > class Bar a b | a->b + > + > data Obj = Obj + > + > instance Bar Obj Obj + > + > instance (Bar a b) => Foo a b + > + > foo:: (Foo a b) => a -> String + > foo _ = "works" + > + > runFoo:: (forall a b. (Foo a b) => a -> w) -> w + > runFoo f = f Obj + + *Test> runFoo foo + + :1: + Could not deduce (Bar a b) from the context (Foo a b) + arising from use of `foo' at :1 + Probable fix: + Add (Bar a b) to the expected type of an expression + In the first argument of `runFoo', namely `foo' + In the definition of `it': it = runFoo foo + + Why all of the sudden does GHC need the constraint Bar a b? The + function foo didn't ask for that... +@ The trouble is that to type (runFoo foo), GHC has to solve the problem: @@ -1088,18 +1090,16 @@ checkLoop :: RedEnv -- Postcondition: returned Insts are zonked checkLoop env wanteds - = go env wanteds (return ()) - where go env wanteds elim_skolems + = go env wanteds + where go env wanteds = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv] ; env' <- zonkRedEnv env ; wanteds' <- zonkInsts wanteds - ; (improved, binds, irreds, elim_more_skolems) - <- reduceContext env' wanteds' - ; let elim_skolems' = elim_skolems >> elim_more_skolems + ; (improved, binds, irreds) <- reduceContext env' wanteds' - ; if not improved then - elim_skolems' >> return (irreds, binds) + ; if null irreds || not improved then + return (irreds, binds) else do -- If improvement did some unification, we go round again. @@ -1108,7 +1108,7 @@ checkLoop env wanteds -- variable which might have been unified, so we'd get an -- infinite loop if we started again with wanteds! -- See Note [LOOP] - { (irreds1, binds1) <- go env' irreds elim_skolems' + { (irreds1, binds1) <- go env' irreds ; return (irreds1, binds `unionBags` binds1) } } \end{code} @@ -1357,9 +1357,7 @@ 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 (\_ -> ReduceMe AddSCs) - ; (_imp, _binds, constrained_dicts, elim_skolems) - <- reduceContext env wanteds' - ; elim_skolems + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) @@ -1408,8 +1406,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, elim_skolems) <- reduceContext env wanteds' - ; elim_skolems + ; (_imp, binds, irreds) <- reduceContext env wanteds' -- See "Notes on implicit parameters, Question 4: top level" ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured @@ -1482,27 +1479,55 @@ Instead we want to quantify over the dictionaries separately. In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving all dicts unchanged, with absolutely no sharing. It's simpler to do this -from scratch, rather than further parameterise simpleReduceLoop etc +from scratch, rather than further parameterise simpleReduceLoop etc. +Simpler, maybe, but alas not simple (see Trac #2494) + +* Type errors may give rise to an (unsatisfiable) equality constraint + +* Applications of a higher-rank function on the LHS may give + rise to an implication constraint, esp if there are unsatisfiable + equality constraints inside. \begin{code} tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds) tcSimplifyRuleLhs wanteds - = go [] emptyBag wanteds + = do { wanteds' <- zonkInsts wanteds + ; (irreds, binds) <- go [] emptyBag wanteds' + ; let (dicts, bad_irreds) = partition isDict irreds + ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds) + ; addNoInstanceErrs (nub bad_irreds) + -- The nub removes duplicates, which has + -- not happened otherwise (see notes above) + ; return (dicts, binds) } where - go dicts binds [] - = return (dicts, binds) - go dicts binds (w:ws) + go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds) + go irreds binds [] + = return (irreds, binds) + go irreds binds (w:ws) | isDict w - = go (w:dicts) binds ws + = go (w:irreds) binds ws + | isImplicInst w -- Have a go at reducing the implication + = do { (binds1, irreds1) <- reduceImplication red_env w + ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1 + ; go (bad_irreds ++ irreds) + (binds `unionBags` binds1) + (ok_irreds ++ ws)} | otherwise = do { w' <- zonkInst w -- So that (3::Int) does not generate a call -- to fromInteger; this looks fragile to me ; lookup_result <- lookupSimpleInst w' ; case lookup_result of - GenInst ws' rhs -> - go dicts (addInstToDictBind binds w rhs) (ws' ++ ws) - NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) + NoInstance -> go (w:irreds) binds ws + GenInst ws' rhs -> go irreds binds' (ws' ++ ws) + where + binds' = addInstToDictBind binds w rhs } + + -- Sigh: we need to reduce inside implications + red_env = mkRedEnv doc try_me [] + doc = ptext (sLit "Implication constraint in RULE lhs") + try_me inst | isMethodOrLit inst = ReduceMe AddSCs + | otherwise = Stop -- Be gentle \end{code} tcSimplifyBracket is used when simplifying the constraints arising from @@ -1558,8 +1583,7 @@ tcSimplifyIPs given_ips wanteds -- Unusually for checking, we *must* zonk the given_ips ; let env = mkRedEnv doc try_me given_ips' - ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds' - ; elim_skolems + ; (improved, binds, irreds) <- reduceContext env wanteds' ; if not improved then ASSERT( all is_free irreds ) @@ -1732,110 +1756,88 @@ reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, TcDictBinds, -- Dictionary bindings - [Inst], -- Irreducible - TcM ()) -- Undo skolems from SkolemOccurs + [Inst]) -- Irreducible -reduceContext env wanteds +reduceContext env wanteds0 = do { traceTc (text "reduceContext" <+> (vcat [ text "----------------------", red_doc env, text "given" <+> ppr (red_givens env), - text "wanted" <+> ppr wanteds, + text "wanted" <+> ppr wanteds0, text "----------------------" ])) - - ; let givens = red_givens env - (given_eqs0, given_dicts0) = partition isEqInst givens - (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds - (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs - -- 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 + ; ancestor_eqs <- ancestorEqualities wanteds0 ; 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" + -- Normalise and solve all equality constraints as far as possible + -- and normalise all dictionary constraints wrt to the reduced + -- equalities. The returned wanted constraints include the + -- irreducible wanted equalities. + ; let wanteds = wanteds0 ++ ancestor_eqs + givens = red_givens env + ; (givens', + wanteds', + normalise_binds, + eq_improved) <- tcReduceEqs givens wanteds + ; traceTc $ text "reduceContext: tcReduceEqs" <+> vcat + [ppr givens', ppr wanteds', ppr normalise_binds] + + -- Build the Avail mapping from "given_dicts" ; (init_state, _) <- getLIE $ do - { init_state <- foldlM addGiven emptyAvails given_dicts + { init_state <- foldlM addGiven emptyAvails givens' ; return init_state } - -- *** ToDo: what to do with the "extra_givens"? For the - -- moment I'm simply discarding them, which is probably wrong - - -- 6. Solve the *wanted* *dictionary* constraints (not implications) - -- This may expose some further equational constraints... + -- Solve the *wanted* *dictionary* constraints (not implications) + -- This may expose some further equational constraints... + ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds' ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state) - ; (dict_binds, bound_dicts, dict_irreds) - <- extractResults avails wanted_dicts - ; traceTc $ text "reduceContext extractresults" <+> vcat + ; (dict_binds, + bound_dicts, + dict_irreds) <- extractResults avails wanted_dicts + ; traceTc $ text "reduceContext: extractResults" <+> vcat [ppr avails, ppr wanted_dicts, ppr dict_binds] -- Solve the wanted *implications*. In doing so, we can provide -- as "given" all the dicts that were originally given, -- *or* for which we now have bindings, -- *or* which are now irreds - ; let implic_env = env { red_givens = givens ++ bound_dicts - ++ dict_irreds } + ; let implic_env = env { red_givens = givens ++ bound_dicts ++ + dict_irreds } ; (implic_binds_s, implic_irreds_s) - <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0 + <- mapAndUnzipM (reduceImplication implic_env) wanted_implics ; let implic_binds = unionManyBags implic_binds_s implic_irreds = concat implic_irreds_s - -- Normalise the wanted equality constraints - ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs) - - -- Normalise the wanted dictionaries - ; let irreds = dict_irreds ++ implic_irreds - eqs = eq_irreds ++ given_eqs - ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds - - -- Figure out whether we should go round again. We do so in either - -- two cases: - -- (1) If any of the mutable tyvars in givens or irreds has been - -- filled in by improvement, there is merit in going around - -- again, because we may make further progress. - -- (2) If we managed to normalise any dicts, there is merit in going - -- around gain, because reduceList may be able to get further. - -- - -- ToDo: 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 = norm_irreds ++ eq_irreds - ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $ - tyVarsOfInsts (givens ++ all_irreds) - ; let improvedDicts = not $ isEmptyBag normalise_binds - improved = improvedMetaTy || improvedDicts - - -- The old plan (fragile) - -- improveed = availsImproved avails - -- || (not $ isEmptyBag normalise_binds1) - -- || (not $ isEmptyBag normalise_binds2) - -- || (any isEqInst irreds) + -- Collect all irreducible instances, and determine whether we should + -- go round again. We do so in either of two cases: + -- (1) If dictionary reduction or equality solving led to + -- improvement (i.e., instantiated type variables). + -- (2) If we uncovered extra equalities. We will try to solve them + -- in the next iteration. + + ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs + avails_improved = availsImproved avails + improvedFlexible = avails_improved || eq_improved + extraEqs = (not . null) extra_eqs + improved = improvedFlexible || extraEqs + -- + improvedHint = (if avails_improved then " [AVAILS]" else "") ++ + (if eq_improved then " [EQ]" else "") ++ + (if extraEqs then " [EXTRA EQS]" else "") ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", red_doc env, text "given" <+> ppr givens, - text "given_eqs" <+> ppr given_eqs, - text "wanted" <+> ppr wanteds, - text "wanted_dicts" <+> ppr wanted_dicts, + text "wanted" <+> ppr wanteds0, text "----", text "avails" <+> pprAvails avails, - text "improved =" <+> ppr improved, + text "improved =" <+> ppr improved <+> text improvedHint, text "(all) irreds = " <+> ppr all_irreds, text "dict-binds = " <+> ppr dict_binds, text "implic-binds = " <+> ppr implic_binds, @@ -1843,11 +1845,9 @@ reduceContext env wanteds ])) ; return (improved, - given_binds `unionBags` normalise_binds - `unionBags` dict_binds - `unionBags` implic_binds, - all_irreds, - eliminate_skolems) + normalise_binds `unionBags` dict_binds + `unionBags` implic_binds, + all_irreds) } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone @@ -1862,33 +1862,44 @@ tcImproveOne avails inst -- Avails has all the superclasses etc (good) -- It also has all the intermediates of the deduction (good) -- It does not have duplicates (good) - -- NB that (?x::t1) and (?x::t2) will be held separately in avails - -- so that improve will see them separate + -- NB that (?x::t1) and (?x::t2) will be held separately in + -- avails so that improve will see them separate ; traceTc (text "improveOne" <+> ppr inst) ; unifyEqns eqns } -unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] +unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))] -> TcM ImprovementDone unifyEqns [] = return False unifyEqns eqns = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns)) - ; mapM_ unify eqns - ; return True } + ; improved <- mapM unify eqns + ; return $ or improved + } where unify ((qtvs, pairs), what1, what2) - = addErrCtxtM (mkEqnMsg what1 what2) $ do - (_, _, tenv) <- tcInstTyVars (varSetElems qtvs) - mapM_ (unif_pr tenv) pairs - unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2) + = addErrCtxtM (mkEqnMsg what1 what2) $ + do { let freeTyVars = unionVarSets (map tvs_pr pairs) + `minusVarSet` qtvs + ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs) + ; mapM_ (unif_pr tenv) pairs + ; anyM isFilledMetaTyVar $ varSetElems freeTyVars + } + + unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2) + + tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc -pprEquationDoc (eqn, (p1, _), (p2, _)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] +pprEquationDoc (eqn, (p1, _), (p2, _)) + = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc) mkEqnMsg (pred1,from1) (pred2,from2) tidy_env - = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2 - ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' } + = do { pred1' <- zonkTcPredType pred1 + ; pred2' <- zonkTcPredType pred2 + ; let { pred1'' = tidyPred tidy_env pred1' + ; pred2'' = tidyPred tidy_env pred2' } ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])] @@ -2338,8 +2349,8 @@ extendAvails avails@(Avails imp env) inst avail availsInsts :: Avails -> [Inst] availsInsts (Avails _ avails) = keysFM avails -_availsImproved :: Avails -> ImprovementDone -_availsImproved (Avails imp _) = imp +availsImproved :: Avails -> ImprovementDone +availsImproved (Avails imp _) = imp \end{code} Extracting the bindings from a bunch of Avails. @@ -2670,7 +2681,7 @@ disambiguate doc interactive dflags insts | extended_defaulting = any isInteractiveClass clss | otherwise = all is_std_class clss && (any is_num_class clss) - -- In interactive mode, or with -fextended-default-rules, + -- In interactive mode, or with -XExtendedDefaultRules, -- we default Show a to Show () to avoid graututious errors on "show []" isInteractiveClass cls = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey]) @@ -2736,7 +2747,7 @@ getDefaultTys extended_deflts ovl_strings Note [Default unitTy] ~~~~~~~~~~~~~~~~~~~~~ -In interative mode (or with -fextended-default-rules) we add () as the first type we +In interative mode (or with -XExtendedDefaultRules) we add () as the first type we try when defaulting. This has very little real impact, except in the following case. Consider: Text.Printf.printf "hello" @@ -2962,7 +2973,7 @@ report_no_instances tidy_env mb_what insts ASSERT( not (null unifiers) ) 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 "To pick the first instance above, use -XIncoherentInstances"), ptext (sLit "when compiling the other instance declarations")])] where ispecs = [ispec | (ispec, _) <- matches] @@ -3061,8 +3072,8 @@ monomorphism_fix dflags = ptext (sLit "Probable fix:") <+> vcat [ptext (sLit "give these definition(s) an explicit type signature"), if dopt Opt_MonomorphismRestriction dflags - then ptext (sLit "or use -fno-monomorphism-restriction") - else empty] -- Only suggest adding "-fno-monomorphism-restriction" + then ptext (sLit "or use -XNoMonomorphismRestriction") + else empty] -- Only suggest adding "-XNoMonomorphismRestriction" -- if it is not already set! warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()