X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=aff019e851b649d76fe60fffdb9a09d77386d26d;hp=c0ae8ce45f08191421623979a3a4a21c153adab5;hb=aafdba3bce91afb003f5f50e001e141744837bae;hpb=a7ba22ff9bdc25d23af38ff1a2c9bbcc12dd45b8 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index c0ae8ce..aff019e 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -6,16 +6,25 @@ 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, tcSimplifyRuleLhs, tcSimplifyIPs, tcSimplifySuperClasses, tcSimplifyTop, tcSimplifyInteractive, - tcSimplifyBracket, + tcSimplifyBracket, tcSimplifyCheckPat, tcSimplifyDeriv, tcSimplifyDefault, - bindInstsOfLocalFuns + bindInstsOfLocalFuns, + + misMatchMsg ) where #include "HsVersions.h" @@ -27,12 +36,13 @@ import TcRnMonad import Inst import TcEnv import InstEnv -import TcMType +import TcGadt import TcType +import TcMType import TcIface -import Id +import TcTyFuns +import TypeRep import Var -import TyCon import Name import NameSet import Class @@ -45,11 +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 @@ -133,14 +146,9 @@ from. The Right Thing is to improve whenever the constraint set changes at all. Not hard in principle, but it'll take a bit of fiddling to do. - - - -------------------------------------- - Notes on quantification - -------------------------------------- - -Suppose we are about to do a generalisation step. -We have in our hand +Note [Choosing which variables to quantify] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are about to do a generalisation step. We have in our hand G the environment T the type of the RHS @@ -163,11 +171,12 @@ Here are the things that *must* be true: (A) Q intersect fv(G) = EMPTY limits how big Q can be (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be -(A) says we can't quantify over a variable that's free in the -environment. (B) says we must quantify over all the truly free -variables in T, else we won't get a sufficiently general type. We do -not *need* to quantify over any variable that is fixed by the free -vars of the environment G. + (A) says we can't quantify over a variable that's free in the environment. + (B) says we must quantify over all the truly free variables in T, else + we won't get a sufficiently general type. + +We do not *need* to quantify over any variable that is fixed by the +free vars of the environment G. BETWEEN THESE TWO BOUNDS, ANY Q WILL DO! @@ -181,38 +190,15 @@ Example: class H x y | x->y where ... So Q can be {c,d}, {b,c,d} +In particular, it's perfectly OK to quantify over more type variables +than strictly necessary; there is no need to quantify over 'b', since +it is determined by 'a' which is free in the envt, but it's perfectly +OK to do so. However we must not quantify over 'a' itself. + Other things being equal, however, we'd like to quantify over as few variables as possible: smaller types, fewer type applications, more -constraints can get into Ct instead of Cq. - - ------------------------------------------ -We will make use of - - fv(T) the free type vars of T - - oclose(vs,C) The result of extending the set of tyvars vs - using the functional dependencies from C - - grow(vs,C) The result of extend the set of tyvars vs - using all conceivable links from C. - - E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e} - Then grow(vs,C) = {a,b,c} - - Note that grow(vs,C) `superset` grow(vs,simplify(C)) - That is, simplfication can only shrink the result of grow. - -Notice that - oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs - grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C) - - ------------------------------------------ - -Choosing Q -~~~~~~~~~~ -Here's a good way to choose Q: +constraints can get into Ct instead of Cq. Here's a good way to +choose Q: Q = grow( fv(T), C ) \ oclose( fv(G), C ) @@ -246,9 +232,8 @@ all the functional dependencies yet: T = c->c C = (Eq (T c d)) - Now oclose(fv(T),C) = {c}, because the functional dependency isn't - apparent yet, and that's wrong. We must really quantify over d too. - +Now oclose(fv(T),C) = {c}, because the functional dependency isn't +apparent yet, and that's wrong. We must really quantify over d too. There really isn't any point in quantifying over any more than grow( fv(T), C ), because the call sites can't possibly influence @@ -398,8 +383,8 @@ When m is later unified with [], we can solve both constraints. Notes on implicit parameters -------------------------------------- -Question 1: can we "inherit" implicit parameters -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Inheriting implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y @@ -424,6 +409,26 @@ BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring. +Note [Implicit parameters and ambiguity] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +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'. + + Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ BUT WATCH OUT: When you supply a type signature, we can't force you @@ -642,82 +647,210 @@ tcSimplifyInfer :: SDoc -> TcTyVarSet -- fv(T); type vars -> [Inst] -- Wanted - -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) - TcDictBinds, -- Bindings - [TcId]) -- Dict Ids that must be bound here (zonked) + -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified) + [Inst], -- Dict Ids that must be bound here (zonked) + TcDictBinds) -- Bindings -- Any free (escaping) Insts are tossed into the environment \end{code} \begin{code} -tcSimplifyInfer doc tau_tvs wanted_lie - = inferLoop doc (varSetElems tau_tvs) - wanted_lie `thenM` \ (qtvs, frees, binds, irreds) -> - - extendLIEs frees `thenM_` - returnM (qtvs, binds, map instToId irreds) - -inferLoop doc tau_tvs wanteds - = -- Step 1 - zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' -> - mappM zonkInst wanteds `thenM` \ wanteds' -> - tcGetGlobalTyVars `thenM` \ gbl_tvs -> - let - preds = fdPredsOfInsts wanteds' - qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs - - try_me inst - | isFreeWhenInferring qtvs inst = Free - | isClassDict inst = DontReduceUnlessConstant -- Dicts - | otherwise = ReduceMe NoSCs -- Lits and Methods - in - traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, - ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_` - -- Step 2 - reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) -> - - -- Step 3 - if no_improvement then - returnM (varSetElems qtvs, frees, binds, irreds) - else - -- If improvement did some unification, we go round again. There - -- are two subtleties: - -- a) 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 example [LOOP] - -- - -- b) It's also essential to re-process frees, because unification - -- might mean that a type variable that looked free isn't now. - -- - -- Hence the (irreds ++ frees) - - -- However, NOTICE that when we are done, we might have some bindings, but - -- the final qtvs might be empty. See [NO TYVARS] below. - - inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) -> - returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1) +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 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 + -- constraints that don't mention qtvs at all + ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted' + ; extendLIEs free + + -- To make types simple, reduce as much as possible + ; 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] + ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs + ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1 + + -- Now work out all over again which type variables to quantify, + -- exactly in the same way as before, but starting from irreds2. Why? + -- a) By now improvment may have taken place, and we must *not* + -- quantify over any variable free in the environment + -- tc137 (function h inside g) is an example + -- + -- b) Do not quantify over constraints that *now* do not + -- mention quantified type variables, because they are + -- simply ambiguous (or might be bound further out). Example: + -- f :: Eq b => a -> (a, b) + -- g x = fst (f x) + -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta) + -- We decide to quantify over 'alpha' alone, but free1 does not include f77 + -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous) + -- constraint (Eq beta), which we dump back into the free set + -- See test tcfail181 + -- + -- c) irreds may contain type variables not previously mentioned, + -- e.g. instance D a x => Foo [a] + -- wanteds = Foo [a] + -- 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_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 + + -- Turn the quantified meta-type variables into real type variables + ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs) + + -- We can't abstract over any remaining unsolved + -- implications so instead just float them outwards. Ugh. + ; let (q_dicts0, implics) = partition isAbstractableInst irreds3 + ; loc <- getInstLoc (ImplicOrigin doc) + ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics + + -- 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. + +approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds) +-- Note [Inference and implication constraints] +-- Given a bunch of Dict and ImplicInsts, try to approximate the implications by +-- - fetching any dicts inside them that are free +-- - using those dicts as cruder constraints, to solve the implications +-- - returning the extra ones too + +approximateImplications doc want_dict irreds + | null extra_dicts + = return (irreds, emptyBag) + | otherwise + = do { extra_dicts' <- mapM cloneDict extra_dicts + ; tryHardCheckLoop doc (extra_dicts' ++ irreds) } + -- By adding extra_dicts', we make them + -- available to solve the implication constraints + where + extra_dicts = get_dicts (filter isImplicInst irreds) + + get_dicts :: [Inst] -> [Inst] -- Returns only Dicts + -- Find the wanted constraints in implication constraints that satisfy + -- want_dict, and are not bound by forall's in the constraint itself + get_dicts ds = concatMap get_dict ds + + get_dict d@(Dict {}) | want_dict d = [d] + | otherwise = [] + get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds}) + = [ 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} -Example [LOOP] +Note [Inference and implication constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have a wanted implication constraint (perhaps arising from +a nested pattern match) like + C a => D [a] +and we are now trying to quantify over 'a' when inferring the type for +a function. In principle it's possible that there might be an instance + instance (C a, E a) => D [a] +so the context (E a) would suffice. The Right Thing is to abstract over +the implication constraint, but we don't do that (a) because it'll be +surprising to programmers and (b) because we don't have the machinery to deal +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_dicts in approximateImplications. + +The common cases are more clear-cut, when we have things like + forall a. C a => C b +Here, abstracting over (C b) is not an approximation at all -- but see +Note [Freeness and implications]. + +See Trac #1430 and test tc228. - class If b t e r | b t e -> r - instance If T t e t - instance If F t e e - class Lte a b c | a b -> c where lte :: a -> b -> c - instance Lte Z b T - instance (Lte a b l,If l b a c) => Max a b c -Wanted: Max Z (S x) y +\begin{code} +----------------------------------------------------------- +-- tcSimplifyInferCheck is used when we know the constraints we are to simplify +-- against, but we don't know the type variables over which we are going to quantify. +-- This happens when we have a type signature for a mutually recursive group +tcSimplifyInferCheck + :: InstLoc + -> TcTyVarSet -- fv(T) + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM ([TyVar], -- Fully zonked, and quantified + TcDictBinds) -- Bindings -Then we'll reduce using the Max instance to: - (Lte Z (S x) l, If l (S x) Z y) -and improve by binding l->T, after which we can do some reduction -on both the Lte and If constraints. What we *can't* do is start again -with (Max Z (S x) y)! +tcSimplifyInferCheck loc tau_tvs 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, + -- but in bizarre cases you can get extra ones + -- f :: forall a. Num a => a -> a + -- f x = fst (g (x, head [])) + 1 + -- g a b = (b,a) + -- Here we infer g :: forall a b. a -> b -> (b,a) + -- We don't want g to be monomorphic in b just because + -- f isn't quantified over b. + ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) + ; all_tvs <- zonkTcTyVarsAndFV all_tvs + ; gbl_tvs <- tcGetGlobalTyVars + ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs) + -- We could close gbl_tvs, but its not necessary for + -- soundness, and it'll only affect which tyvars, not which + -- dictionaries, we quantify over + + ; qtvs' <- zonkQuantifiedTyVars qtvs -[NO TYVARS] + -- 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} +Note [Squashing methods] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Be careful if you want to float methods more: + truncate :: forall a. RealFrac a => forall b. Integral b => a -> b +From an application (truncate f i) we get + t1 = truncate at f + t2 = t1 at i +If we have also have a second occurrence of truncate, we get + t3 = truncate at f + t4 = t3 at i +When simplifying with i,f free, we might still notice that +t1=t3; but alas, the binding for t2 (which mentions t1) +may continue to float out! + + +Note [NO TYVARS] +~~~~~~~~~~~~~~~~~ class Y a b | a -> b where y :: a -> X b @@ -742,16 +875,18 @@ The net effect of [NO TYVARS] \begin{code} isFreeWhenInferring :: TyVarSet -> Inst -> Bool isFreeWhenInferring qtvs inst - = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars - && isInheritableInst inst -- And no implicit parameter involved - -- (see "Notes on implicit parameters") + = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars + && isInheritableInst inst -- and no implicit parameter involved + -- see Note [Inheriting implicit parameters] +{- No longer used (with implication constraints) isFreeWhenChecking :: TyVarSet -- Quantified tyvars -> NameSet -- Quantified implicit parameters -> Inst -> Bool isFreeWhenChecking qtvs ips inst = isFreeWrtTyVars qtvs inst && isFreeWrtIPs ips inst +-} isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst)) @@ -768,110 +903,280 @@ isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst)) we are going to quantify over. For example, a class or instance declaration. \begin{code} -tcSimplifyCheck - :: SDoc - -> [TcTyVar] -- Quantify over these - -> [Inst] -- Given - -> [Inst] -- Wanted - -> TcM TcDictBinds -- Bindings - +----------------------------------------------------------- -- tcSimplifyCheck is used when checking expression type signatures, -- class decls, instance decls etc. +tcSimplifyCheck :: InstLoc + -> [TcTyVar] -- Quantify over these + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM TcDictBinds -- Bindings +tcSimplifyCheck loc qtvs givens wanteds + = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) + do { traceTc (text "tcSimplifyCheck") + ; (irreds, binds) <- gentleCheckLoop loc givens wanteds + ; implic_bind <- bindIrreds loc qtvs givens irreds + ; return (binds `unionBags` implic_bind) } + +----------------------------------------------------------- +-- tcSimplifyCheckPat is used for existential pattern match +tcSimplifyCheckPat :: InstLoc + -> [CoVar] -> Refinement + -> [TcTyVar] -- Quantify over these + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM TcDictBinds -- Bindings +tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds + = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) + 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) } + +----------------------------------------------------------- +bindIrreds :: InstLoc -> [TcTyVar] + -> [Inst] -> [Inst] + -> TcM TcDictBinds +bindIrreds loc qtvs givens irreds + = bindIrredsR loc qtvs [] emptyRefinement givens irreds + +bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar] + -> Refinement -> [Inst] -> [Inst] + -> TcM TcDictBinds +-- Make a binding that binds 'irreds', by generating an implication +-- constraint for them, *and* throwing the constraint into the LIE +bindIrredsR loc qtvs co_vars reft givens irreds + | null irreds + = return emptyBag + | otherwise + = 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 + -- (the refinement is like more givens), then it's safe to + -- partition the 'wanteds' by their qtvs, thereby trimming irreds + -- See Note [Freeness and implications] + ; irreds' <- if null givens' && isEmptyRefinement reft + then do + { let qtv_set = mkVarSet qtvs + (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds + ; extendLIEs frees + ; return real_irreds } + else return irreds + + ; let all_tvs = qtvs ++ co_vars -- Abstract over all these + ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds' + -- This call does the real work + -- If irreds' is empty, it does something sensible + ; extendLIEs implics + ; return bind } + + +makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement + -> [Inst] -> [Inst] + -> TcM ([Inst], TcDictBinds) +-- Make a binding that binds 'irreds', by generating an implication +-- constraint for them, *and* throwing the constraint into the LIE +-- The binding looks like +-- (ir1, .., irn) = f qtvs givens +-- where f is (evidence for) the new implication constraint +-- f :: forall qtvs. {reft} givens => (ir1, .., irn) +-- qtvs includes coercion variables -- --- NB: tcSimplifyCheck does not consult the --- global type variables in the environment; so you don't --- need to worry about setting them before calling tcSimplifyCheck -tcSimplifyCheck doc qtvs givens wanted_lie - = ASSERT( all isSkolemTyVar qtvs ) - do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie - ; extendLIEs frees - ; return binds } +-- 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 = (eq_givens ++ dict_givens), + tci_wanted = irreds, tci_loc = loc } + ; 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 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 + -> [Inst] -- Wanted + -> TcM ([Inst], TcDictBinds) + +tryHardCheckLoop doc wanteds + = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds + ; return (irreds,binds) + } where --- get_qtvs = zonkTcTyVarsAndFV qtvs - get_qtvs = return (mkVarSet qtvs) -- All skolems - + try_me inst = ReduceMe AddSCs + -- Here's the try-hard bit --- tcSimplifyInferCheck is used when we know the constraints we are to simplify --- against, but we don't know the type variables over which we are going to quantify. --- This happens when we have a type signature for a mutually recursive group -tcSimplifyInferCheck - :: SDoc - -> TcTyVarSet -- fv(T) - -> [Inst] -- Given - -> [Inst] -- Wanted - -> TcM ([TcTyVar], -- Variables over which to quantify - TcDictBinds) -- Bindings +----------------------------------------------------------- +gentleCheckLoop :: InstLoc + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM ([Inst], TcDictBinds) -tcSimplifyInferCheck doc tau_tvs givens wanted_lie - = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie - ; extendLIEs frees - ; return (qtvs', binds) } +gentleCheckLoop inst_loc givens wanteds + = do { (irreds,binds,_) <- checkLoop env wanteds + ; return (irreds,binds) + } where - -- Figure out which type variables to quantify over - -- You might think it should just be the signature tyvars, - -- but in bizarre cases you can get extra ones - -- f :: forall a. Num a => a -> a - -- f x = fst (g (x, head [])) + 1 - -- g a b = (b,a) - -- Here we infer g :: forall a b. a -> b -> (b,a) - -- We don't want g to be monomorphic in b just because - -- f isn't quantified over b. - all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) - - get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' -> - tcGetGlobalTyVars `thenM` \ gbl_tvs -> - let - qtvs = all_tvs' `minusVarSet` gbl_tvs - -- We could close gbl_tvs, but its not necessary for - -- soundness, and it'll only affect which tyvars, not which - -- dictionaries, we quantify over - in - returnM qtvs + env = mkRedEnv (pprInstLoc inst_loc) try_me givens + + try_me inst | isMethodOrLit inst = ReduceMe AddSCs + | 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} -Here is the workhorse function for all three wrappers. +Note [Check gently] +~~~~~~~~~~~~~~~~~~~~ +We have to very careful about not simplifying too vigorously +Example: + data T a where + MkT :: a -> T [a] + + f :: Show b => T b -> b + f (MkT x) = show [x] + +Inside the pattern match, which binds (a:*, x:a), we know that + b ~ [a] +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 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 +and methods only, plus common up equal things), deferring the real +work until top level, when we solve the implication constraint +with tryHardCheckLooop. -\begin{code} -tcSimplCheck doc get_qtvs want_scs givens wanted_lie - = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie - -- Complain about any irreducible ones - ; if not (null irreds) - then do { givens' <- mappM zonkInst given_dicts_and_ips - ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds } - else return () +\begin{code} +----------------------------------------------------------- +checkLoop :: RedEnv + -> [Inst] -- Wanted + -> TcM ([Inst], TcDictBinds, + [Inst]) -- needed givens +-- Precondition: givens are completely rigid +-- Postcondition: returned Insts are zonked + +checkLoop env 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' - ; returnM (qtvs, frees, binds) } - where - given_dicts_and_ips = filter (not . isMethod) givens - -- For error reporting, filter out methods, which are - -- only added to the given set as an optimisation - - ip_set = mkNameSet (ipNamesOfInsts givens) - - check_loop givens wanteds - = -- Step 1 - mappM zonkInst givens `thenM` \ givens' -> - mappM zonkInst wanteds `thenM` \ wanteds' -> - get_qtvs `thenM` \ qtvs' -> - - -- Step 2 - let - -- When checking against a given signature we always reduce - -- until we find a match against something given, or can't reduce - try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free - | otherwise = ReduceMe want_scs - in - reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) -> - - -- Step 3 - if no_improvement then - returnM (varSetElems qtvs', frees, binds, irreds) - else - check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) -> - returnM (qtvs', frees1, binds `unionBags` binds1, irreds1) + ; 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} +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 + instance If T t e t + instance If F t e e + class Lte a b c | a b -> c where lte :: a -> b -> c + instance Lte Z b T + instance (Lte a b l,If l b a c) => Max a b c + +Wanted: Max Z (S x) y + +Then we'll reduce using the Max instance to: + (Lte Z (S x) l, If l (S x) Z y) +and improve by binding l->T, after which we can do some reduction +on both the Lte and If constraints. What we *can't* do is start again +with (Max Z (S x) y)! + + %************************************************************************ %* * @@ -918,15 +1223,21 @@ Two more nasty cases are in tcrun033 \begin{code} -tcSimplifySuperClasses qtvs givens sc_wanteds - = ASSERT( all isSkolemTyVar qtvs ) - do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds - ; ext_default <- doptM Opt_ExtendedDefaultRules - ; binds2 <- tc_simplify_top doc ext_default NoSCs frees - ; return (binds1 `unionBags` binds2) } +tcSimplifySuperClasses + :: InstLoc + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM TcDictBinds +tcSimplifySuperClasses loc givens sc_wanteds + = do { traceTc (text "tcSimplifySuperClasses") + ; (irreds,binds1,_) <- checkLoop env sc_wanteds + ; let (tidy_env, tidy_irreds) = tidyInsts irreds + ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds + ; return binds1 } where - get_qtvs = return (mkVarSet qtvs) - doc = ptext SLIT("instance declaration superclass context") + env = mkRedEnv (pprInstLoc loc) try_me givens + try_me inst = ReduceMe NoSCs + -- Like tryHardCheckLoop, but with NoSCs \end{code} @@ -1038,7 +1349,7 @@ tcSimplifyRestricted -- Used for restricted binding groups -> [Name] -- Things bound in this group -> TcTyVarSet -- Free in the type of the RHSs -> [Inst] -- Free in the RHSs - -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) + -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified) TcDictBinds) -- Bindings -- tcSimpifyRestricted returns no constraints to -- quantify over; by definition there are none. @@ -1046,9 +1357,10 @@ tcSimplifyRestricted -- Used for restricted binding groups tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- Zonk everything in sight - = mappM zonkInst wanteds `thenM` \ wanteds' -> + = do { traceTc (text "tcSimplifyRestricted") + ; wanteds' <- zonkInsts wanteds - -- 'reduceMe': Reduce as far as we can. Don't stop at + -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type -- variables as possible, and we don't want to stop -- at (say) Monad (ST s), because that reduces @@ -1057,28 +1369,40 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- BUT do no improvement! See Plan D above -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint - reduceContextWithoutImprovement - doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) -> + ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) + ; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds' -- Next, figure out the tyvars we will quantify over - zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' -> - tcGetGlobalTyVars `thenM` \ gbl_tvs' -> - mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' -> - let - constrained_tvs' = tyVarsOfInsts constrained_dicts' - qtvs' = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs') - `minusVarSet` constrained_tvs' - in - traceTc (text "tcSimplifyRestricted" <+> vcat [ - pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts', + ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + ; gbl_tvs' <- tcGetGlobalTyVars + ; constrained_dicts' <- zonkInsts constrained_dicts + + ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs' + -- As in tcSimplifyInfer + + -- Do not quantify over constrained type variables: + -- this is the monomorphism restriction + constrained_tvs' = tyVarsOfInsts constrained_dicts' + qtvs = qtvs1 `minusVarSet` constrained_tvs' + pp_bndrs = pprWithCommas (quotes . ppr) bndrs + + -- Warn in the mono + ; warn_mono <- doptM Opt_WarnMonomorphism + ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1)) + (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding") + <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs, + ptext SLIT("Consider giving a type signature for") <+> pp_bndrs]) + + ; traceTc (text "tcSimplifyRestricted" <+> vcat [ + pprInsts wanteds, pprInsts constrained_dicts', ppr _binds, - ppr constrained_tvs', ppr tau_tvs', ppr qtvs' ]) `thenM_` + ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) -- The first step may have squashed more methods than -- necessary, so try again, this time more gently, knowing the exact -- set of type variables to quantify over. -- - -- We quantify only over constraints that are captured by qtvs'; + -- We quantify only over constraints that are captured by qtvs; -- these will just be a subset of non-dicts. This in contrast -- to normal inference (using isFreeWhenInferring) in which we quantify over -- all *non-inheritable* constraints too. This implements choice @@ -1090,27 +1414,23 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- -- At top level, we *do* squash methods becuase we want to -- expose implicit parameters to the test that follows - let - is_nested_group = isNotTopLevel top_lvl - try_me inst | isFreeWrtTyVars qtvs' inst, - (is_nested_group || isDict inst) = Free - | otherwise = ReduceMe AddSCs - in - reduceContextWithoutImprovement - doc try_me wanteds' `thenM` \ (frees, binds, irreds) -> - ASSERT( null irreds ) + ; let is_nested_group = isNotTopLevel top_lvl + try_me inst | isFreeWrtTyVars qtvs inst, + (is_nested_group || isDict inst) = Stop + | otherwise = ReduceMe AddSCs + env = mkNoImproveRedEnv doc try_me + ; (_imp, binds, irreds, _) <- reduceContext env wanteds' -- See "Notes on implicit parameters, Question 4: top level" - if is_nested_group then - extendLIEs frees `thenM_` - returnM (varSetElems qtvs', binds) - else - let - (non_ips, bad_ips) = partition isClassDict frees - in - addTopIPErrs bndrs bad_ips `thenM_` - extendLIEs non_ips `thenM_` - returnM (varSetElems qtvs', binds) + ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured + if is_nested_group then + extendLIEs irreds + else do { let (bad_ips, non_ips) = partition isIPDict irreds + ; addTopIPErrs bndrs bad_ips + ; extendLIEs non_ips } + + ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs) + ; return (qtvs', binds) } \end{code} @@ -1187,10 +1507,10 @@ tcSimplifyRuleLhs wanteds | otherwise = do { w' <- zonkInst w -- So that (3::Int) does not generate a call -- to fromInteger; this looks fragile to me - ; lookup_result <- lookupInst w' + ; lookup_result <- lookupSimpleInst w' ; case lookup_result of - GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws) - SimpleInst rhs -> go dicts (addBind binds w rhs) ws + GenInst ws' rhs -> + go dicts (addInstToDictBind binds w rhs) (ws' ++ ws) NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) } \end{code} @@ -1205,8 +1525,8 @@ this bracket again at its usage site. \begin{code} tcSimplifyBracket :: [Inst] -> TcM () tcSimplifyBracket wanteds - = simpleReduceLoop doc reduceMe wanteds `thenM_` - returnM () + = do { tryHardCheckLoop doc wanteds + ; return () } where doc = text "tcSimplifyBracket" \end{code} @@ -1236,30 +1556,34 @@ force the binding for ?x to be of type Int. tcSimplifyIPs :: [Inst] -- The implicit parameters bound here -> [Inst] -- Wanted -> TcM TcDictBinds -tcSimplifyIPs given_ips wanteds - = simpl_loop given_ips wanteds `thenM` \ (frees, binds) -> - extendLIEs frees `thenM_` - returnM binds - where - doc = text "tcSimplifyIPs" <+> ppr given_ips - ip_set = mkNameSet (ipNamesOfInsts given_ips) + -- We need a loop so that we do improvement, and then + -- (next time round) generate a binding to connect the two + -- let ?x = e in ?x + -- Here the two ?x's have different types, and improvement + -- makes them the same. - -- Simplify any methods that mention the implicit parameter - try_me inst | isFreeWrtIPs ip_set inst = Free - | otherwise = ReduceMe NoSCs +tcSimplifyIPs given_ips wanteds + = do { wanteds' <- zonkInsts wanteds + ; given_ips' <- zonkInsts given_ips + -- Unusually for checking, we *must* zonk the given_ips - simpl_loop givens wanteds - = mappM zonkInst givens `thenM` \ givens' -> - mappM zonkInst wanteds `thenM` \ wanteds' -> + ; let env = mkRedEnv doc try_me given_ips' + ; (improved, binds, irreds, _) <- reduceContext env wanteds' - reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) -> + ; if not improved then + ASSERT( all is_free irreds ) + do { extendLIEs irreds + ; return binds } + else + tcSimplifyIPs given_ips wanteds } + where + doc = text "tcSimplifyIPs" <+> ppr given_ips + ip_set = mkNameSet (ipNamesOfInsts given_ips) + is_free inst = isFreeWrtIPs ip_set inst - if no_improvement then - ASSERT( null irreds ) - returnM (frees, binds) - else - simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) -> - returnM (frees1, binds `unionBags` binds1) + -- Simplify any methods that mention the implicit parameter + try_me inst | is_free inst = Stop + | otherwise = ReduceMe NoSCs \end{code} @@ -1304,11 +1628,10 @@ bindInstsOfLocalFuns wanteds local_ids returnM emptyLHsBinds | otherwise - = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) -> - ASSERT( null irreds ) - extendLIEs not_for_me `thenM_` - extendLIEs frees `thenM_` - returnM binds + = do { (irreds, binds) <- gentleInferLoop doc for_me + ; extendLIEs not_for_me + ; extendLIEs irreds + ; return binds } where doc = text "bindInsts" <+> ppr local_ids overloaded_ids = filter is_overloaded local_ids @@ -1318,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 = Free \end{code} @@ -1332,116 +1653,70 @@ bindInstsOfLocalFuns wanteds local_ids The main control over context reduction is here \begin{code} +data RedEnv + = RedEnv { red_doc :: SDoc -- The context + , red_try_me :: Inst -> WhatToDo + , red_improve :: Bool -- True <=> do improvement + , 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] + } + +-- Note [Rigidity] +-- The red_givens are rigid so far as cmpInst is concerned. +-- There is one case where they are not totally rigid, namely in tcSimplifyIPs +-- let ?x = e in ... +-- Here, the given is (?x::a), where 'a' is not necy a rigid type +-- But that doesn't affect the comparison, which is based only on mame. + +-- Note [RedStack] +-- The red_stack pair (n,insts) pair is just used for error reporting. +-- 'n' is always the depth of the stack. +-- The 'insts' is the stack of Insts being reduced: to produce X +-- I had to produce Y, to produce Y I had to produce Z, and so on. + + +mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv +mkRedEnv doc try_me givens + = RedEnv { red_doc = doc, red_try_me = try_me, + 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_reft = emptyRefinement, + red_stack = (0,[]), + red_improve = True } + data WhatToDo = ReduceMe WantSCs -- Try to reduce this - -- If there's no instance, behave exactly like - -- DontReduce: add the inst to the irreductible ones, - -- but don't produce an error message of any kind. + -- If there's no instance, add the inst to the + -- irreductible ones, but don't produce an error + -- message of any kind. -- It might be quite legitimate such as (Eq a)! - | DontReduceUnlessConstant -- Return as irreducible unless it can - -- be reduced to a constant in one step - - | Free -- Return as free - -reduceMe :: Inst -> WhatToDo -reduceMe inst = ReduceMe AddSCs + | Stop -- Return as irreducible unless it can + -- be reduced to a constant in one step + -- Do not add superclasses; see 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] -\end{code} - - - -\begin{code} -type Avails = FiniteMap Inst Avail -emptyAvails = emptyFM - -data Avail - = IsFree -- Used for free Insts - | Irred -- Used for irreducible dictionaries, - -- which are going to be lambda bound - - | Given TcId -- Used for dictionaries for which we have a binding - -- e.g. those "given" in a signature - - | Rhs -- Used when there is a RHS - (LHsExpr TcId) -- The RHS - [Inst] -- Insts free in the RHS; we need these too - -pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)] - | (inst,avail) <- fmToList avails ] - -instance Outputable Avail where - ppr = pprAvail - -pprAvail IsFree = text "Free" -pprAvail Irred = text "Irred" -pprAvail (Given x) = text "Given" <+> ppr x -pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs) -\end{code} - -Extracting the bindings from a bunch of Avails. -The bindings do *not* come back sorted in dependency order. -We assume that they'll be wrapped in a big Rec, so that the -dependency analyser can sort them out later - -The loop startes -\begin{code} -extractResults :: Avails - -> [Inst] -- Wanted - -> TcM (TcDictBinds, -- Bindings - [Inst], -- Irreducible ones - [Inst]) -- Free ones -extractResults avails wanteds - = go avails emptyBag [] [] wanteds - where - go avails binds irreds frees [] - = returnM (binds, irreds, frees) - - go avails binds irreds frees (w:ws) - = case lookupFM avails w of - Nothing -> pprTrace "Urk: extractResults" (ppr w) $ - go avails binds irreds frees ws - - Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws - Just Irred -> go (add_given avails w) binds (w:irreds) frees ws - - Just (Given id) -> go avails new_binds irreds frees ws - where - new_binds | id == instToId w = binds - | otherwise = addBind binds w (L (instSpan w) (HsVar id)) - -- 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 irreds frees (ws' ++ ws) - where - new_binds = addBind binds w rhs - - add_given avails w = addToFM avails w (Given (instToId w)) - - add_free avails w | isMethod w = avails - | otherwise = add_given avails w - -- NB: Hack alert! - -- Do *not* replace Free by Given if it's a method. - -- The following situation shows why this is bad: - -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b - -- From an application (truncate f i) we get - -- t1 = truncate at f - -- t2 = t1 at i - -- If we have also have a second occurrence of truncate, we get - -- t3 = truncate at f - -- t4 = t3 at i - -- When simplifying with i,f free, we might still notice that - -- t1=t3; but alas, the binding for t2 (which mentions t1) - -- will continue to float out! - -addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst)) - (VarBind (instToId inst) rhs)) -instSpan wanted = instLocSrcSpan (instLoc wanted) +zonkRedEnv :: RedEnv -> TcM RedEnv +zonkRedEnv env + = do { givens' <- mappM zonkInst (red_givens env) + ; return $ env {red_givens = givens'} + } \end{code} @@ -1451,139 +1726,167 @@ instSpan wanted = instLocSrcSpan (instLoc wanted) %* * %************************************************************************ -When the "what to do" predicate doesn't depend on the quantified type variables, -matters are easier. We don't need to do any zonking, unless the improvement step -does something, in which case we zonk before iterating. - -The "given" set is always empty. - -\begin{code} -simpleReduceLoop :: SDoc - -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables - -> [Inst] -- Wanted - -> TcM ([Inst], -- Free - TcDictBinds, - [Inst]) -- Irreducible - -simpleReduceLoop doc try_me wanteds - = mappM zonkInst wanteds `thenM` \ wanteds' -> - reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) -> - if no_improvement then - returnM (frees, binds, irreds) - else - simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) -> - returnM (frees1, binds `unionBags` binds1, irreds1) -\end{code} +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 :: SDoc - -> (Inst -> WhatToDo) - -> [Inst] -- Given +reduceContext :: RedEnv -> [Inst] -- Wanted - -> TcM (Bool, -- True <=> improve step did no unification - [Inst], -- Free - TcDictBinds, -- Dictionary bindings - [Inst]) -- Irreducible - -reduceContext doc try_me givens wanteds - = - traceTc (text "reduceContext" <+> (vcat [ - text "----------------------", - doc, - text "given" <+> ppr givens, - text "wanted" <+> ppr wanteds, - text "----------------------" - ])) `thenM_` - - -- Build the Avail mapping from "givens" - foldlM addGiven emptyAvails givens `thenM` \ init_state -> - - -- Do the real work - reduceList (0,[]) try_me wanteds init_state `thenM` \ avails -> + -> TcM (ImprovementDone, + TcDictBinds, -- Dictionary bindings + [Inst], -- Irreducible + [Inst]) -- Needed givens - -- Do improvement, using everything in avails - -- In particular, avails includes all superclasses of everything - tcImprove avails `thenM` \ no_improvement -> - - extractResults avails wanteds `thenM` \ (binds, irreds, frees) -> - - traceTc (text "reduceContext end" <+> (vcat [ +reduceContext env wanteds + = do { traceTc (text "reduceContext" <+> (vcat [ text "----------------------", - doc, - text "given" <+> ppr givens, + red_doc env, + text "given" <+> ppr (red_givens env), text "wanted" <+> ppr wanteds, - text "----", - text "avails" <+> pprAvails avails, - text "frees" <+> ppr frees, - text "no_improvement =" <+> ppr no_improvement, text "----------------------" - ])) `thenM_` - - returnM (no_improvement, frees, binds, irreds) - --- reduceContextWithoutImprovement differs from reduceContext --- (a) no improvement --- (b) 'givens' is assumed empty -reduceContextWithoutImprovement doc try_me wanteds - = - traceTc (text "reduceContextWithoutImprovement" <+> (vcat [ - text "----------------------", - doc, - text "wanted" <+> ppr wanteds, - text "----------------------" - ])) `thenM_` - - -- Do the real work - reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails -> - extractResults avails wanteds `thenM` \ (binds, irreds, frees) -> - - traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [ + ])) + + + ; 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 "----------------------", - doc, + red_doc 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 "frees" <+> ppr frees, + text "improved =" <+> ppr improved, + text "(all) irreds = " <+> ppr all_irreds, + text "binds = " <+> ppr binds, + text "needed givens = " <+> ppr needed_givens, text "----------------------" - ])) `thenM_` - - returnM (frees, binds, irreds) - -tcImprove :: Avails -> TcM Bool -- False <=> no change --- Perform improvement using all the predicates in Avails -tcImprove avails - = tcGetInstEnvs `thenM` \ inst_envs -> - let - preds = [ (pred, pp_loc) - | (inst, avail) <- fmToList avails, - pred <- get_preds inst avail, - let pp_loc = pprInstLoc (instLoc inst) - ] + ])) + + ; return (improved, + given_binds `unionBags` normalise_binds1 + `unionBags` normalise_binds2 + `unionBags` binds, + all_irreds, + needed_givens) + } + +tcImproveOne :: Avails -> Inst -> TcM ImprovementDone +tcImproveOne avails inst + | not (isDict inst) = return False + | otherwise + = do { inst_envs <- tcGetInstEnvs + ; let eqns = improveOne (classInstances inst_envs) + (dictPred inst, pprInstArising inst) + [ (dictPred p, pprInstArising p) + | p <- availsInsts avails, isDict p ] -- 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 - - -- For free Methods, we want to take predicates from their context, - -- but for Methods that have been squished their context will already - -- be in Avails, and we don't want duplicates. Hence this rather - -- horrid get_preds function - get_preds inst IsFree = fdPredsOfInst inst - get_preds inst other | isDict inst = [dictPred inst] - | otherwise = [] - - eqns = improve get_insts preds - get_insts clas = classInstances inst_envs clas - in - if null eqns then - returnM True - else - traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_` - mappM_ unify eqns `thenM_` - returnM False + ; traceTc (text "improveOne" <+> ppr inst) + ; unifyEqns eqns } + +unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] + -> TcM ImprovementDone +unifyEqns [] = return False +unifyEqns eqns + = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) + ; mappM_ unify eqns + ; return True } where unify ((qtvs, pairs), what1, what2) = addErrCtxtM (mkEqnMsg what1 what2) $ @@ -1605,198 +1908,72 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env The main context-reduction function is @reduce@. Here's its game plan. \begin{code} -reduceList :: (Int,[Inst]) -- Stack (for err msgs) - -- along with its depth - -> (Inst -> WhatToDo) - -> [Inst] - -> Avails - -> TcM Avails -\end{code} - -@reduce@ is passed - try_me: given an inst, this function returns - Reduce reduce this - DontReduce return this in "irreds" - Free return this in "frees" - - wanteds: The list of insts to reduce - state: An accumulating parameter of type Avails - that contains the state of the algorithm - - It returns a Avails. - -The (n,stack) pair is just used for error reporting. -n is always the depth of the stack. -The stack is the stack of Insts being reduced: to produce X -I had to produce Y, to produce Y I had to produce Z, and so on. - -\begin{code} -reduceList (n,stack) try_me wanteds state - = do { dopts <- getDOpts +reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails +reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state + = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state)) + ; dopts <- getDOpts #ifdef DEBUG ; if n > 8 then - dumpTcRn (text "Interesting! Context reduction stack deeper than 8:" - <+> (int n $$ ifPprDebug (nest 2 (pprStack stack)))) + dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) + 2 (ifPprDebug (nest 2 (pprStack stk)))) else return () #endif ; if n >= ctxtStkDepth dopts then - failWithTc (reduceDepthErr n stack) + failWithTc (reduceDepthErr n stk) else go wanteds state } where go [] state = return state - go (w:ws) state = do { state' <- reduce (n+1, w:stack) try_me 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! -reduce stack try_me wanted avails +reduce env wanted avails -- It's the same as an existing inst, or a superclass thereof - | Just avail <- isAvailable avails wanted - = returnM avails + | Just avail <- findAvail avails wanted + = do { traceTc (text "reduce: found " <+> ppr wanted) + ; returnM avails + } | otherwise - = case try_me wanted of { - - ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced) - -- First, see if the inst can be reduced to a constant in one step - try_simple (addIrred AddSCs) -- Assume want superclasses - - ; Free -> -- It's free so just chuck it upstairs - -- First, see if the inst can be reduced to a constant in one step - try_simple addFree - - ; ReduceMe want_scs -> -- It should be reduced - lookupInst wanted `thenM` \ lookup_result -> - case lookup_result of - GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 -> - reduceList stack try_me wanteds' avails1 `thenM` \ avails2 -> - addWanted want_scs avails2 wanted rhs wanteds' - -- Experiment with temporarily doing addIrred *before* the reduceList, + = 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 + + 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' } } + -- 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 - - SimpleInst rhs -> addWanted want_scs avails wanted rhs [] - - NoInstance -> -- No such instance! - -- Add it and its superclasses - addIrred want_scs avails wanted - } + } } 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) + -- Don't bother for implication constraints, which take real work try_simple do_this_otherwise - = lookupInst wanted `thenM` \ lookup_result -> - case lookup_result of - SimpleInst rhs -> addWanted AddSCs avails wanted rhs [] - other -> do_this_otherwise avails wanted + = do { res <- lookupSimpleInst wanted + ; case res of + GenInst [] rhs -> addWanted AddSCs avails wanted rhs [] + other -> do_this_otherwise avails wanted } \end{code} -\begin{code} -------------------------- -isAvailable :: Avails -> Inst -> Maybe Avail -isAvailable avails wanted = lookupFM avails wanted - -- NB 1: the Ord instance of Inst compares by the class/type info - -- *not* by unique. So - -- d1::C Int == d2::C Int - -------------------------- -addFree :: Avails -> Inst -> TcM Avails - -- When an Inst is tossed upstairs as 'free' we nevertheless add it - -- to avails, so that any other equal Insts will be commoned up right - -- here rather than also being tossed upstairs. This is really just - -- an optimisation, and perhaps it is more trouble that it is worth, - -- as the following comments show! - -- - -- NB: do *not* add superclasses. If we have - -- df::Floating a - -- dn::Num a - -- but a is not bound here, then we *don't* want to derive - -- dn from df here lest we lose sharing. - -- -addFree avails free = returnM (addToFM avails free IsFree) - -addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails -addWanted want_scs avails wanted rhs_expr wanteds - = addAvailAndSCs want_scs avails wanted avail - where - avail = Rhs rhs_expr wanteds - -addGiven :: Avails -> Inst -> TcM Avails -addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given)) - -- Always add superclasses for 'givens' - -- - -- No ASSERT( not (given `elemFM` 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 - -addIrred :: WantSCs -> Avails -> Inst -> TcM Avails -addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails ) - addAvailAndSCs want_scs avails irred Irred - -addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails -addAvailAndSCs want_scs avails inst avail - | not (isClassDict inst) = return avails_with_inst - | NoSCs <- want_scs = return avails_with_inst - | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) - ; addSCs is_loop avails_with_inst inst } - where - avails_with_inst = addToFM avails inst avail - - is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys - -- Note: this compares by *type*, not by Unique - deps = findAllDeps (unitVarSet (instToId inst)) avail - dep_tys = map idType (varSetElems deps) - - findAllDeps :: IdSet -> Avail -> IdSet - -- Find all the Insts that this one depends on - -- See Note [SUPERCLASS-LOOP 2] - -- Watch out, though. Since the avails may contain loops - -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far - findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids - findAllDeps so_far other = so_far - - find_all :: IdSet -> Inst -> IdSet - find_all so_far kid - | kid_id `elemVarSet` so_far = so_far - | Just avail <- lookupFM avails kid = findAllDeps so_far' avail - | otherwise = so_far' - where - so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far - kid_id = instToId kid - -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 - -- depends on this one, so you'd build a loop" - -- Invariant: the Inst is already in Avails. - -addSCs is_loop avails dict - = do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta' - ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) } - where - (clas, tys) = getDictClassTys dict - (tyvars, sc_theta, sc_sels, _) = classBigSig clas - sc_theta' = 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] - | is_given sc_dict = return avails - | otherwise = 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 - avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict]) - - is_given :: Inst -> Bool - is_given sc_dict = case lookupFM avails sc_dict of - Just (Given _) -> True -- Given is cheaper than superclass selection - other -> False -\end{code} - Note [SUPERCLASS-LOOP 2] ~~~~~~~~~~~~~~~~~~~~~~~~ But the above isn't enough. Suppose we are *given* d1:Ord a, @@ -1831,7 +2008,7 @@ At first I had a gross hack, whereby I simply did not add superclass constraints in addWanted, though I did for addGiven and addIrred. This was sub-optimal, becuase it lost legitimate superclass sharing, and it still didn't do the job: I found a very obscure program (now tcrun021) in which improvement meant the -simplifier got two bites a the cherry... so something seemed to be an Irred +simplifier got two bites a the cherry... so something seemed to be an Stop first time, but reducible next time. Now we implement the Right Solution, which is to check for loops directly @@ -1877,6 +2054,577 @@ contributing clauses. %************************************************************************ %* * + Reducing a single constraint +%* * +%************************************************************************ + +\begin{code} +--------------------------------------------- +reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult) +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 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 + -> [Inst] -- Wanted + -> InstLoc + -> TcM (Avails, LookupInstResult) +\end{code} + +Suppose we are simplifying the constraint + forall bs. extras => wanted +in the context of an overall simplification problem with givens 'givens', +and refinment 'reft'. + +Note that + * The refinement is often empty + + * The 'extra givens' need not mention any of the quantified type variables + e.g. forall {}. Eq a => Eq [a] + forall {}. C Int => D (Tree Int) + + This happens when you have something like + data T a where + T1 :: Eq a => a -> T a + + f :: T a -> Int + f x = ...(case x of { T1 v -> v==v })... + +\begin{code} + -- ToDo: should we instantiate tvs? I think it's not necessary + -- + -- 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 + -- 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 = 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]) + ; (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] + + -- Note [Reducing implication constraints] + -- Tom -- update note, put somewhere! + + ; traceTc (text "reduceImplication result" <+> vcat + [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 = 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! + + ; 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 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 | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted) + | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed + + + ; 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 + ( 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 + Ord a -> Irred +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 GenInst +like this + + 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. + +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 + + +Note [Freeness and implications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It's hard to say when an implication constraint can be floated out. Consider + forall {} Eq a => Foo [a] +The (Foo [a]) doesn't mention any of the quantified variables, but it +still might be partially satisfied by the (Eq a). + +There is a useful special case when it *is* easy to partition the +constraints, namely when there are no 'givens'. Consider + forall {a}. () => Bar b +There are no 'givens', and so there is no reason to capture (Bar b). +We can let it float out. But if there is even one constraint we +must be much more careful: + forall {a}. C a b => Bar (m b) +because (C a b) might have a superclass (D b), from which we might +deduce (Bar [b]) when m later gets instantiated to []. Ha! + +Here is an even more exotic example + class C a => D a b +Now consider the constraint + forall b. D Int b => C Int +We can satisfy the (C Int) from the superclass of D, so we don't want +to float the (C Int) out, even though it mentions no type variable in +the constraints! + +Note [Pruning the givens in an implication constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are about to form the implication constraint + forall tvs. Eq a => Ord b +The (Eq a) cannot contribute to the (Ord b), because it has no access to +the type variable 'b'. So we could filter out the (Eq a) from the givens. + +Doing so would be a bit tidier, but all the implication constraints get +simplified away by the optimiser, so it's no great win. So I don't take +advantage of that at the moment. + +If you do, BE CAREFUL of wobbly type variables. + + +%************************************************************************ +%* * + Avails and AvailHow: the pool of evidence +%* * +%************************************************************************ + + +\begin{code} +data Avails = Avails !ImprovementDone !AvailEnv + +type ImprovementDone = Bool -- True <=> some unification has happened + -- so some Irreds might now be reducible + -- keys that are now + +type AvailEnv = FiniteMap Inst AvailHow +data AvailHow + = IsIrred -- Used for irreducible dictionaries, + -- which are going to be lambda bound + + | 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 + (LHsExpr TcId) -- The RHS + [Inst] -- Insts free in the RHS; we need these too + +instance Outputable Avails where + ppr = pprAvails + +pprAvails (Avails imp avails) + = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty) + , nest 2 $ braces $ + vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)] + | (inst,avail) <- fmToList avails ]] + +instance Outputable AvailHow where + ppr = pprAvail + +------------------------- +pprAvail :: AvailHow -> SDoc +pprAvail IsIrred = text "Irred" +pprAvail (Given x) = text "Given" <+> ppr x +pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs, + nest 2 (ppr rhs)] + +------------------------- +extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv +extendAvailEnv env inst avail = addToFM env inst avail + +findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow +findAvailEnv env wanted = lookupFM env wanted + -- NB 1: the Ord instance of Inst compares by the class/type info + -- *not* by unique. So + -- d1::C Int == d2::C Int + +emptyAvails :: Avails +emptyAvails = Avails False emptyFM + +findAvail :: Avails -> Inst -> Maybe AvailHow +findAvail (Avails _ avails) wanted = findAvailEnv avails wanted + +elemAvails :: Inst -> Avails -> Bool +elemAvails wanted (Avails _ avails) = wanted `elemFM` avails + +extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails +-- Does improvement +extendAvails avails@(Avails imp env) inst avail + = do { imp1 <- tcImproveOne avails inst -- Do any improvement + ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) } + +availsInsts :: Avails -> [Inst] +availsInsts (Avails _ avails) = keysFM avails + +availsImproved (Avails imp _) = imp + +updateImprovement :: Avails -> Avails -> Avails +-- (updateImprovement a1 a2) sets a1's improvement flag from a2 +updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1 +\end{code} + +Extracting the bindings from a bunch of Avails. +The bindings do *not* come back sorted in dependency order. +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 + -> (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 emptyBag [] [] emptyFM wanteds + where + 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 binds irreds givens done ws + + Just IsIrred -> go binds (w:irreds) givens done' ws + + Just (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws) + + 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} + + +Note [No superclasses for Stop] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we decide not to reduce an Inst -- the 'WhatToDo' --- we still +add it to avails, so that any other equal Insts will be commoned up +right here. However, we do *not* add superclasses. If we have + df::Floating a + dn::Num a +but a is not bound here, then we *don't* want to derive dn from df +here lest we lose sharing. + +\begin{code} +addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails +addWanted want_scs avails wanted rhs_expr wanteds + = addAvailAndSCs want_scs avails wanted avail + where + avail = Rhs rhs_expr wanteds + +addGiven :: Avails -> Inst -> TcM Avails +addGiven avails given = addAvailAndSCs AddSCs avails given (Given given) + -- Always add superclasses for 'givens' + -- + -- 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 -> 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 + , isRefineablePred pred -- See Note [ImplicInst rigidity] + , Just (co, pred) <- refinePred reft pred + = do { new_given <- newDictBndr (instLoc given) pred + ; let rhs = L (instSpan given) $ + HsWrap (WpCo co) (HsVar (instToId given)) + ; 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 avails +\end{code} + +Note [ImplicInst rigidity] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + C :: forall ab. (Eq a, Ord b) => b -> T a + + ...(case x of C v -> )... + +From the case (where x::T ty) we'll get an implication constraint + forall b. (Eq ty, Ord b) => +Now suppose itself has an implication constraint +of form + forall c. => +Then, we can certainly apply the refinement to the Ord b, becuase it is +existential, but we probably should not apply it to the (Eq ty) because it may +be wobbly. Hence the isRigidInst + +@Insts@ are ordered by their class/type info, rather than by their +unique. This allows the context-reduction mechanism to use standard finite +maps to do their stuff. It's horrible that this code is here, rather +than with the Avails handling stuff in TcSimplify + +\begin{code} +addIrred :: WantSCs -> Avails -> Inst -> TcM Avails +addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails ) + addAvailAndSCs want_scs avails irred IsIrred + +addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails +addAvailAndSCs want_scs avails inst avail + | not (isClassDict inst) = extendAvails avails inst avail + | NoSCs <- want_scs = extendAvails avails inst avail + | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) + ; avails' <- extendAvails avails inst avail + ; addSCs is_loop avails' inst } + where + is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys + -- Note: this compares by *type*, not by Unique + deps = findAllDeps (unitVarSet (instToVar inst)) avail + dep_tys = map idType (varSetElems deps) + + findAllDeps :: IdSet -> AvailHow -> IdSet + -- Find all the Insts that this one depends on + -- See Note [SUPERCLASS-LOOP 2] + -- Watch out, though. Since the avails may contain loops + -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far + findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids + findAllDeps so_far other = so_far + + 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' + where + so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far + kid_id = instToId kid + +addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails + -- Add all the superclasses of the Inst to Avails + -- 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. + +addSCs is_loop avails dict + = ASSERT( isDict dict ) + do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta' + ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) } + where + (clas, tys) = getDictClassTys dict + (tyvars, sc_theta, sc_sels, _) = classBigSig clas + 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] + | is_given sc_dict = return avails + | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict]) + ; addSCs is_loop avails' sc_dict } + where + sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel)) + 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} %* * %************************************************************************ @@ -1898,104 +2646,47 @@ It's OK: the final zonking stage should zap y to (), which is fine. \begin{code} tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds tcSimplifyTop wanteds - = do { ext_default <- doptM Opt_ExtendedDefaultRules - ; tc_simplify_top doc ext_default AddSCs wanteds } + = tc_simplify_top doc False wanteds where doc = text "tcSimplifyTop" tcSimplifyInteractive wanteds - = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds + = tc_simplify_top doc True wanteds where - doc = text "tcSimplifyTop" + doc = text "tcSimplifyInteractive" -- The TcLclEnv should be valid here, solely to improve -- error message generation for the monomorphism restriction -tc_simplify_top doc use_extended_defaulting want_scs wanteds - = do { lcl_env <- getLclEnv - ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env)) - - ; let try_me inst = ReduceMe want_scs - ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds - - ; let - -- First get rid of implicit parameters - (non_ips, bad_ips) = partition isClassDict irreds - - -- All the non-tv or multi-param ones are definite errors - (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips - bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs) - - -- Group by type variable - tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts - - -- Pick the ones which its worth trying to disambiguate - -- namely, the ones whose type variable isn't bound - -- up with one of the non-tyvar classes - (default_gps, non_default_gps) = partition defaultable_group tv_groups - defaultable_group ds - = (bad_tyvars `disjointVarSet` tyVarsOfInst (head ds)) - && defaultable_classes (map get_clas ds) - defaultable_classes clss - | use_extended_defaulting = any isInteractiveClass clss - | otherwise = all isStandardClass clss && any isNumericClass clss - - isInteractiveClass cls = isNumericClass cls - || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey]) - -- In interactive mode, or with -fextended-default-rules, - -- we default Show a to Show () to avoid graututious errors on "show []" - - - -- Collect together all the bad guys - bad_guys = non_tvs ++ concat non_default_gps - (ambigs, no_insts) = partition isTyVarDict bad_guys - -- If the dict has no type constructors involved, it must be ambiguous, - -- except I suppose that another error with fundeps maybe should have - -- constrained those type variables - - -- Report definite errors - ; ASSERT( null frees ) - groupErrs (addNoInstanceErrs Nothing []) no_insts - ; strangeTopIPErrs bad_ips - - -- Deal with ambiguity errors, but only if - -- if there has not been an error so far: - -- errors often give rise to spurious ambiguous Insts. - -- For example: - -- f = (*) -- Monomorphic - -- g :: Num a => a -> a - -- g x = f x x - -- Here, we get a complaint when checking the type signature for g, - -- that g isn't polymorphic enough; but then we get another one when - -- dealing with the (Num a) context arising from f's definition; - -- we try to unify a with Int (to default it), but find that it's - -- already been unified with the rigid variable from g's type sig - ; binds_ambig <- ifErrsM (returnM []) $ - do { -- Complain about the ones that don't fall under - -- the Haskell rules for disambiguation - -- This group includes both non-existent instances - -- e.g. Num (IO a) and Eq (Int -> Int) - -- and ambiguous dictionaries - -- e.g. Num a - addTopAmbigErrs ambigs - - -- Disambiguate the ones that look feasible - ; mappM disambigGroup default_gps } - - ; return (binds `unionBags` unionManyBags binds_ambig) } - ----------------------------------- -d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2 - -is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a) - -- Invariant: argument is a ClassDict, not IP or method -is_unary_tyvar_dict d = case getDictClassTys d of - (_, [ty]) -> tcIsTyVarTy ty - other -> False - -get_tv d = case getDictClassTys d of - (clas, [ty]) -> tcGetTyVar "tcSimplify" ty -get_clas d = case getDictClassTys d of - (clas, _) -> clas +tc_simplify_top doc interactive wanteds + = do { dflags <- getDOpts + ; 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 + ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2 + + -- Deal with implicit parameters + ; let (bad_ips, non_ips) = partition isIPDict irreds3 + (ambigs, others) = partition isTyVarDict non_ips + + ; topIPErrs bad_ips -- Can arise from f :: Int -> Int + -- f x = x + ?y + ; addNoInstanceErrs others + ; addTopAmbigErrs ambigs + + ; return (binds1 `unionBags` binds2 `unionBags` binds3) } + where + doc1 = doc <+> ptext SLIT("(first round)") + doc2 = doc <+> ptext SLIT("(approximate)") + doc3 = doc <+> ptext SLIT("(disambiguate)") \end{code} If a dictionary constrains a type variable which is @@ -2031,88 +2722,145 @@ Since we're not using the result of @foo@, the result if (presumably) @void@. \begin{code} -disambigGroup :: [Inst] -- All standard classes of form (C a) - -> TcM TcDictBinds +disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds) + -- Just does unification to fix the default types + -- The Insts are assumed to be pre-zonked +disambiguate doc interactive dflags insts + | null insts + = return (insts, emptyBag) -disambigGroup dicts - = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT - -- SO, TRY DEFAULT TYPES IN ORDER - - -- Failure here is caused by there being no type in the - -- default list which can satisfy all the ambiguous classes. - -- For example, if Real a is reqd, but the only type in the - -- default list is Int. - get_default_tys `thenM` \ default_tys -> - let - try_default [] -- No defaults work, so fail - = failM - - try_default (default_ty : default_tys) - = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try - -- default_tys instead - tcSimplifyDefault theta `thenM` \ _ -> - returnM default_ty - where - theta = [mkClassPred clas [default_ty] | clas <- classes] - in - -- See if any default works - tryM (try_default default_tys) `thenM` \ mb_ty -> - case mb_ty of - Left _ -> bomb_out - Right chosen_default_ty -> choose_default chosen_default_ty - where - tyvar = get_tv (head dicts) -- Should be non-empty - classes = map get_clas dicts - - choose_default default_ty -- Commit to tyvar = default_ty - = -- Bind the type variable - unifyType default_ty (mkTyVarTy tyvar) `thenM_` - -- and reduce the context, for real this time - simpleReduceLoop (text "disambig" <+> ppr dicts) - reduceMe dicts `thenM` \ (frees, binds, ambigs) -> - WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs ) - warnDefault dicts default_ty `thenM_` - returnM binds - - bomb_out = addTopAmbigErrs dicts `thenM_` - returnM emptyBag - -get_default_tys - = do { mb_defaults <- getDefaultTys - ; case mb_defaults of - Just tys -> return tys - Nothing -> -- No use-supplied default; - -- use [Integer, Double] - do { integer_ty <- tcMetaTy integerTyConName - ; checkWiredInTyCon doubleTyCon - ; return [integer_ty, doubleTy] } } -\end{code} + | null defaultable_groups + = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups]) + ; return (insts, emptyBag) } -[Aside - why the defaulting mechanism is turned off when - dealing with arguments and results to ccalls. + | otherwise + = do { -- Figure out what default types to use + default_tys <- getDefaultTys extended_defaulting ovl_strings + + ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups]) + ; mapM_ (disambigGroup default_tys) defaultable_groups -When typechecking _ccall_s, TcExpr ensures that the external -function is only passed arguments (and in the other direction, -results) of a restricted set of 'native' types. + -- disambigGroup does unification, hence try again + ; tryHardCheckLoop doc insts } -The interaction between the defaulting mechanism for numeric -values and CC & CR can be a bit puzzling to the user at times. -For example, + where + extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags + ovl_strings = dopt Opt_OverloadedStrings dflags - x <- _ccall_ f - if (x /= 0) then - _ccall_ g x - else - return () + unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints + bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints + (unaries, bad_tvs_s) = partitionWith find_unary insts + bad_tvs = unionVarSets bad_tvs_s -What type has 'x' got here? That depends on the default list -in operation, if it is equal to Haskell 98's default-default -of (Integer, Double), 'x' has type Double, since Integer -is not an instance of CR. If the default list is equal to -Haskell 1.4's default-default of (Int, Double), 'x' has type -Int. + -- Finds unary type-class constraints + find_unary d@(Dict {tci_pred = ClassP cls [ty]}) + | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv) + find_unary inst = Right (tyVarsOfInst inst) -End of aside] + -- Group by type variable + defaultable_groups :: [[(Inst,Class,TcTyVar)]] + defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries) + cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2 + + defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool + defaultable_group ds@((_,_,tv):_) + = isTyConableTyVar tv -- Note [Avoiding spurious errors] + && not (tv `elemVarSet` bad_tvs) + && defaultable_classes [c | (_,c,_) <- ds] + defaultable_group [] = panic "defaultable_group" + + defaultable_classes clss + | extended_defaulting = any isInteractiveClass clss + | otherwise = all is_std_class clss && (any is_num_class clss) + + -- In interactive mode, or with -fextended-default-rules, + -- we default Show a to Show () to avoid graututious errors on "show []" + isInteractiveClass cls + = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey]) + + is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey)) + -- is_num_class adds IsString to the standard numeric classes, + -- when -foverloaded-strings is enabled + + is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey)) + -- Similarly is_std_class + +----------------------- +disambigGroup :: [Type] -- The default types + -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a) + -> TcM () -- Just does unification, to fix the default types + +disambigGroup default_tys dicts + = try_default default_tys + where + (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty + classes = [c | (_,c,_) <- dicts] + + try_default [] = return () + try_default (default_ty : default_tys) + = tryTcLIE_ (try_default default_tys) $ + do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes] + -- This may fail; then the tryTcLIE_ kicks in + -- Failure here is caused by there being no type in the + -- default list which can satisfy all the ambiguous classes. + -- For example, if Real a is reqd, but the only type in the + -- default list is Int. + + -- After this we can't fail + ; warnDefault dicts default_ty + ; unifyType default_ty (mkTyVarTy tyvar) + ; return () -- TOMDO: do something with the coercion + } + + +----------------------- +getDefaultTys :: Bool -> Bool -> TcM [Type] +getDefaultTys extended_deflts ovl_strings + = do { mb_defaults <- getDeclaredDefaultTys + ; case mb_defaults of { + Just tys -> return tys ; -- User-supplied defaults + Nothing -> do + + -- No use-supplied default + -- Use [Integer, Double], plus modifications + { integer_ty <- tcMetaTy integerTyConName + ; checkWiredInTyCon doubleTyCon + ; string_ty <- tcMetaTy stringTyConName + ; return (opt_deflt extended_deflts unitTy + -- Note [Default unitTy] + ++ + [integer_ty,doubleTy] + ++ + opt_deflt ovl_strings string_ty) } } } + where + opt_deflt True ty = [ty] + opt_deflt False ty = [] +\end{code} + +Note [Default unitTy] +~~~~~~~~~~~~~~~~~~~~~ +In interative mode (or with -fextended-default-rules) 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" +This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't +want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to +default the 'a' to (), rather than to Integer (which is what would otherwise happen; +and then GHCi doesn't attempt to print the (). So in interactive mode, we add +() to the list of defaulting types. See Trac #1200. + +Note [Avoiding spurious errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When doing the unification for defaulting, we check for skolem +type variables, and simply don't default them. For example: + f = (*) -- Monomorphic + g :: Num a => a -> a + g x = f x x +Here, we get a complaint when checking the type signature for g, +that g isn't polymorphic enough; but then we get another one when +dealing with the (Num a) context arising from f's definition; +we try to unify a with Int (to default it), but find that it's +already been unified with the rigid variable from g's type sig %************************************************************************ @@ -2133,78 +2881,36 @@ instance declarations. \begin{code} tcSimplifyDeriv :: InstOrigin - -> TyCon -> [TyVar] -> ThetaType -- Wanted -> TcM ThetaType -- Needed +-- Given instance (wanted) => C inst_ty +-- Simplify 'wanted' as much as possible -tcSimplifyDeriv orig tc tyvars theta - = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) -> +tcSimplifyDeriv orig tyvars theta + = do { (tvs, _, tenv) <- tcInstTyVars tyvars -- The main loop may do unification, and that may crash if -- it doesn't see a TcTyVar, so we have to instantiate. Sigh -- ToDo: what if two of them do get unified? - newDictBndrsO orig (substTheta tenv theta) `thenM` \ wanteds -> - simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) -> - ASSERT( null frees ) -- reduceMe never returns Free - - doptM Opt_GlasgowExts `thenM` \ gla_exts -> - doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok -> - let - inst_ty = mkTyConApp tc (mkTyVarTys tvs) - (ok_insts, bad_insts) = partition is_ok_inst irreds - is_ok_inst dict - = isTyVarClassPred pred || (gla_exts && ok_gla_pred pred) - where - pred = dictPred dict -- reduceMe squashes all non-dicts - - ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred]) - -- See Note [Deriving context] - - tv_set = mkVarSet tvs - simpl_theta = map dictPred ok_insts - weird_preds = [pred | pred <- simpl_theta - , not (tyVarsOfPred pred `subVarSet` tv_set)] - - -- Check for a bizarre corner case, when the derived instance decl should - -- have form instance C a b => D (T a) where ... - -- Note that 'b' isn't a parameter of T. This gives rise to all sorts - -- of problems; in particular, it's hard to compare solutions for - -- equality when finding the fixpoint. So I just rule it out for now. - - rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars) - -- This reverse-mapping is a Royal Pain, - -- but the result should mention TyVars not TcTyVars - in - -- In effect, the bad and wierd insts cover all of the cases that - -- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv - -- * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance) - -- * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance) - addNoInstanceErrs Nothing [] bad_insts `thenM_` - mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_` - returnM (substTheta rev_env simpl_theta) + ; wanteds <- newDictBndrsO orig (substTheta tenv theta) + ; (irreds, _) <- tryHardCheckLoop doc wanteds + + ; 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) + -- This reverse-mapping is a pain, but the result + -- should mention the original TyVars not TcTyVars + + ; return simpl_theta } where - doc = ptext SLIT("deriving classes for a data type") -\end{code} + doc = ptext SLIT("deriving classes for a data type") -Note [Deriving context] -~~~~~~~~~~~~~~~~~~~~~~~ -With -fglasgow-exts, we allow things like (C Int a) in the simplified -context for a derived instance declaration, because at a use of this -instance, we might know that a=Bool, and have an instance for (C Int -Bool) - -We nevertheless insist that each predicate meets 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; @@ -2216,14 +2922,13 @@ tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it -> TcM () tcSimplifyDefault theta - = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds -> - simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) -> - ASSERT( null frees ) -- try_me never returns Free - addNoInstanceErrs Nothing [] irreds `thenM_` + = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds -> + tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) -> + addNoInstanceErrs irreds `thenM_` if null irreds then returnM () else - failM + traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM where doc = ptext SLIT("default declaration") \end{code} @@ -2247,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, @@ -2264,24 +2968,27 @@ groupErrs report_err (inst:insts) -- Add the "arising from..." part to a message about bunch of dicts addInstLoc :: [Inst] -> Message -> Message -addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts))) +addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts)) addTopIPErrs :: [Name] -> [Inst] -> TcM () addTopIPErrs bndrs [] = return () addTopIPErrs bndrs ips - = addErrTcM (tidy_env, mk_msg tidy_ips) + = do { dflags <- getDOpts + ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) } where (tidy_env, tidy_ips) = tidyInsts ips - mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"), - nest 2 (ptext SLIT("the monomorphic top-level binding(s) of") + mk_msg dflags ips + = vcat [sep [ptext SLIT("Implicit parameters escape from"), + nest 2 (ptext SLIT("the monomorphic top-level binding") + <> plural bndrs <+> ptext SLIT("of") <+> pprBinders bndrs <> colon)], - nest 2 (vcat (map ppr_ip ips)), - monomorphism_fix] - ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip) + nest 2 (vcat (map ppr_ip ips)), + monomorphism_fix dflags] + ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip -strangeTopIPErrs :: [Inst] -> TcM () -strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all +topIPErrs :: [Inst] -> TcM () +topIPErrs dicts = groupErrs report tidy_dicts where (tidy_env, tidy_dicts) = tidyInsts dicts @@ -2289,60 +2996,68 @@ strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprDictsTheta tidy_dicts) -addNoInstanceErrs :: Maybe SDoc -- Nothing => top level - -- Just d => d describes the construct - -> [Inst] -- What is given by the context or type sig - -> [Inst] -- What is wanted +addNoInstanceErrs :: [Inst] -- Wanted (can include implications) -> TcM () -addNoInstanceErrs mb_what givens [] - = returnM () -addNoInstanceErrs mb_what givens dicts - = -- Some of the dicts are here because there is no instances - -- and some because there are too many instances (overlap) - tcGetInstEnvs `thenM` \ inst_envs -> - let - (tidy_env1, tidy_givens) = tidyInsts givens - (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts - - -- Run through the dicts, generating a message for each - -- overlapping one, but simply accumulating all the - -- no-instance ones so they can be reported as a group - (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts - check_overlap (overlap_doc, no_inst_dicts) dict - | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts) - | 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 +addNoInstanceErrs insts + = do { let (tidy_env, tidy_insts) = tidyInsts insts + ; reportNoInstances tidy_env Nothing tidy_insts } + +reportNoInstances + :: TidyEnv + -> Maybe (InstLoc, [Inst]) -- Context + -- Nothing => top level + -- Just (d,g) => d describes the construct + -- with givens g + -> [Inst] -- What is wanted (can include implications) + -> TcM () + +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 + (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) + + complain_implic inst -- Recurse! + = reportNoInstances tidy_env + (Just (tci_loc inst, tci_given inst)) + (tci_wanted inst) + + check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc + -- Right msg => overlap message + -- Left inst => no instance + check_overlap inst_envs wanted + | 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, because dicts + -- only end up here if they didn't match in Inst.lookupInst #ifdef DEBUG - ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict) + ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted) #endif - ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match - res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts) + ([], _) -> Left wanted -- No match + res -> Right (mk_overlap_msg wanted res) where - (clas,tys) = getDictClassTys dict - in - - -- Now generate a good message for the no-instance bunch - mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) -> - let - no_inst_doc | null no_inst_dicts = empty - | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix] - heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+> - ptext SLIT("for") <+> pprDictsTheta no_inst_dicts - | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts, - nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens] - in - -- And emit both the non-instance and overlap messages - addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc) - where + (clas,tys) = getDictClassTys wanted + mk_overlap_msg dict (matches, unifiers) - = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") + = ASSERT( not (null matches) ) + vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") <+> pprPred (dictPred dict))), sep [ptext SLIT("Matching instances") <> colon, nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])], - ASSERT( not (null matches) ) if not (isSingleton matches) then -- Two or more matches empty @@ -2350,35 +3065,54 @@ addNoInstanceErrs mb_what givens dicts ASSERT( not (null unifiers) ) parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+> quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))), - ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])] + ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"), + ptext SLIT("when compiling the other instance declarations")])] where - ispecs = [ispec | (_, ispec) <- matches] + 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 + + | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls) + not (isEmptyVarSet (tyVarsOfInsts insts)) + = vcat [ addInstLoc insts $ + sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts + , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens] + , show_fixes (fix1 loc : fixes2) ] + + | otherwise -- Top level + = vcat [ addInstLoc insts $ + ptext SLIT("No instance") <> plural insts + <+> ptext SLIT("for") <+> pprDictsTheta insts + , show_fixes fixes2 ] - mk_probable_fix tidy_env dicts - = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)]) where - fixes = add_ors (fix1 ++ fix2) - - fix1 = case mb_what of - Nothing -> [] -- Top level - Just what -> -- Nested (type signatures, instance decls) - [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts, - ptext SLIT("to the") <+> what] ] - - fix2 | null instance_dicts = [] - | otherwise = [ sep [ptext SLIT("add an instance declaration for"), - pprDictsTheta instance_dicts] ] - instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)] + fix1 loc = sep [ ptext SLIT("add") <+> pprDictsTheta insts + <+> ptext SLIT("to the context of"), + nest 2 (ppr (instLocOrigin loc)) ] + -- I'm not sure it helps to add the location + -- nest 2 (ptext SLIT("at") <+> ppr (instLocSpan loc)) ] + + fixes2 | null instance_dicts = [] + | otherwise = [sep [ptext SLIT("add an instance declaration for"), + pprDictsTheta instance_dicts]] + instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)] -- Insts for which it is worth suggesting an adding an instance declaration -- Exclude implicit parameters, and tyvar dicts - add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen - add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange - add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs + show_fixes :: [SDoc] -> SDoc + show_fixes [] = empty + show_fixes (f:fs) = sep [ptext SLIT("Possible fix:"), + nest 2 (vcat (f : map (ptext SLIT("or") <+>) fs))] addTopAmbigErrs dicts -- Divide into groups that share a common set of ambiguous tyvars - = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts]) + = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened + -- See Note [Avoiding spurious errors] + mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts]) where (tidy_env, tidy_dicts) = tidyInsts dicts @@ -2389,7 +3123,7 @@ addTopAmbigErrs dicts report :: [(Inst,[TcTyVar])] -> TcM () report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) -> - setSrcSpan (instLocSrcSpan (instLoc inst)) $ + setSrcSpan (instSpan inst) $ -- the location of the first one will do for the err message addErrTcM (tidy_env, msg $$ mono_msg) where @@ -2398,6 +3132,7 @@ addTopAmbigErrs dicts pprQuotedList tvs <+> in_msg, nest 2 (pprDictsInFull dicts)] in_msg = text "in the constraint" <> plural dicts <> colon + report [] = panic "addTopAmbigErrs" mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message) @@ -2406,38 +3141,44 @@ mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message) -- Try to identify the offending variable -- ASSUMPTION: the Insts are fully zonked mkMonomorphismMsg tidy_env inst_tvs - = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) -> - returnM (tidy_env, mk_msg docs) + = do { dflags <- getDOpts + ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env + ; return (tidy_env, mk_msg dflags docs) } where - mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)") + mk_msg _ _ | any isRuntimeUnk inst_tvs + = vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+> + (pprWithCommas ppr inst_tvs), + ptext SLIT("Use :print or :force to determine these types")] + mk_msg _ [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)") -- This happens in things like -- f x = show (read "foo") - -- whre monomorphism doesn't play any role - mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"), - nest 2 (vcat docs), - monomorphism_fix - ] -monomorphism_fix :: SDoc -monomorphism_fix = ptext SLIT("Probable fix:") <+> - (ptext SLIT("give these definition(s) an explicit type signature") - $$ ptext SLIT("or use -fno-monomorphism-restriction")) + -- where monomorphism doesn't play any role + mk_msg dflags docs + = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"), + nest 2 (vcat docs), + monomorphism_fix dflags] + +monomorphism_fix :: DynFlags -> SDoc +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" + -- if it is not already set! -warnDefault dicts default_ty +warnDefault ups default_ty = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag -> addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg) where + dicts = [d | (d,_,_) <- ups] + -- Tidy them first (_, tidy_dicts) = tidyInsts dicts warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty), pprDictsInFull tidy_dicts] --- Used for the ...Thetas variants; all top level -badDerivedPred pred - = vcat [ptext SLIT("Can't derive instances where the instance context mentions"), - ptext SLIT("type variables that are not data type parameters"), - nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)] - reduceDepthErr n stack = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n, ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),