X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=bed09325acde46c7fa3d695f4a4bfb732ca49a07;hp=737999308f87e41b36a6984f93dfc7bf40557bf0;hb=HEAD;hpb=e6d057711f4d6d6ff6342c39fa2b9e44d25447f1 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 7379993..bed0932 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -1,425 +1,455 @@ -% -% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 -% -\section[TcSimplify]{TcSimplify} - - - \begin{code} -module TcSimplify ( - tcSimplifyInfer, tcSimplifyInferCheck, - tcSimplifyCheck, tcSimplifyRestricted, - tcSimplifyRuleLhs, tcSimplifyIPs, - tcSimplifySuperClasses, - tcSimplifyTop, tcSimplifyInteractive, - tcSimplifyBracket, - - tcSimplifyDeriv, tcSimplifyDefault, - bindInstsOfLocalFuns - ) where +module TcSimplify( + simplifyInfer, + simplifyDefault, simplifyDeriv, + simplifyRule, simplifyTop, simplifyInteractive + ) where #include "HsVersions.h" -import {-# SOURCE #-} TcUnify( unifyType ) -import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, mkWpTyApps, - HsWrapper(..), (<.>), nlHsTyApp, emptyLHsBinds ) -import TcHsSyn ( mkHsApp ) - +import HsSyn import TcRnMonad -import Inst ( lookupInst, LookupInstResult(..), - tyVarsOfInst, fdPredsOfInsts, - isDict, isClassDict, isLinearInst, linearInstType, - isMethodFor, isMethod, - instToId, tyVarsOfInsts, cloneDict, - ipNamesOfInsts, ipNamesOfInst, dictPred, - fdPredsOfInst, - newDictBndrs, newDictBndrsO, tcInstClassOp, - getDictClassTys, isTyVarDict, instLoc, - zonkInst, tidyInsts, tidyMoreInsts, - pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs, - isInheritableInst, pprDictsTheta - ) -import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders, - lclEnvElts, tcMetaTy ) -import InstEnv ( lookupInstEnv, classInstances, pprInstances ) -import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType ) -import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred, - mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar, - mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys, - tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy ) -import TcIface ( checkWiredInTyCon ) -import Id ( idType, mkUserLocal ) -import Var ( TyVar ) -import TyCon ( TyCon ) -import Name ( Name, getOccName, getSrcLoc ) -import NameSet ( NameSet, mkNameSet, elemNameSet ) -import Class ( classBigSig, classKey ) -import FunDeps ( oclose, grow, improve, pprEquation ) -import PrelInfo ( isNumericClass, isStandardClass ) -import PrelNames ( splitName, fstName, sndName, integerTyConName, - showClassKey, eqClassKey, ordClassKey ) -import Type ( zipTopTvSubst, substTheta, substTy ) -import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon ) -import ErrUtils ( Message ) -import BasicTypes ( TopLevelFlag, isNotTopLevel ) +import TcErrors +import TcMType +import TcType +import TcSMonad +import TcInteract +import Inst +import Id ( evVarPred ) +import Unify ( niFixTvSubst, niSubstTvSet ) +import Var import VarSet -import VarEnv ( TidyEnv ) -import FiniteMap +import VarEnv +import Coercion +import TypeRep + +import Name +import NameEnv ( emptyNameEnv ) import Bag +import ListSetOps +import Util +import PrelInfo +import PrelNames +import Class ( classKey ) +import BasicTypes ( RuleName, TopLevelFlag, isTopLevel ) +import Control.Monad ( when ) import Outputable -import ListSetOps ( equivClasses ) -import Util ( zipEqual, isSingleton ) -import List ( partition ) -import SrcLoc ( Located(..) ) -import DynFlags ( DynFlags(ctxtStkDepth), - DynFlag( Opt_GlasgowExts, Opt_AllowUndecidableInstances, - Opt_WarnTypeDefaults, Opt_ExtendedDefaultRules ) ) +import FastString \end{code} -%************************************************************************ -%* * -\subsection{NOTES} -%* * -%************************************************************************ - - -------------------------------------- - Notes on functional dependencies (a bug) - -------------------------------------- - -Consider this: - - class C a b | a -> b - class D a b | a -> b - - instance D a b => C a b -- Undecidable - -- (Not sure if it's crucial to this eg) - f :: C a b => a -> Bool - f _ = True - - g :: C a b => a -> Bool - g = f - -Here f typechecks, but g does not!! Reason: before doing improvement, -we reduce the (C a b1) constraint from the call of f to (D a b1). - -Here is a more complicated example: - -| > class Foo a b | a->b -| > -| > class Bar a b | a->b -| > -| > data Obj = Obj -| > -| > instance Bar Obj Obj -| > -| > instance (Bar a b) => Foo a b -| > -| > foo:: (Foo a b) => a -> String -| > foo _ = "works" -| > -| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w -| > runFoo f = f Obj -| -| *Test> runFoo foo -| -| :1: -| Could not deduce (Bar a b) from the context (Foo a b) -| arising from use of `foo' at :1 -| Probable fix: -| Add (Bar a b) to the expected type of an expression -| In the first argument of `runFoo', namely `foo' -| In the definition of `it': it = runFoo foo -| -| Why all of the sudden does GHC need the constraint Bar a b? The -| function foo didn't ask for that... - -The trouble is that to type (runFoo foo), GHC has to solve the problem: - - Given constraint Foo a b - Solve constraint Foo a b' - -Notice that b and b' aren't the same. To solve this, just do -improvement and then they are the same. But GHC currently does - simplify constraints - apply improvement - and loop - -That is usually fine, but it isn't here, because it sees that Foo a b is -not the same as Foo a b', and so instead applies the instance decl for -instance Bar a b => Foo a b. And that's where the Bar constraint comes -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 - - G the environment - T the type of the RHS - C the constraints from that RHS - -The game is to figure out - - Q the set of type variables over which to quantify - Ct the constraints we will *not* quantify over - Cq the constraints we will quantify over - -So we're going to infer the type - - forall Q. Cq => T - -and float the constraints Ct further outwards. - -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. - - BETWEEN THESE TWO BOUNDS, ANY Q WILL DO! - -Example: class H x y | x->y where ... - - fv(G) = {a} C = {H a b, H c d} - T = c -> b - - (A) Q intersect {a} is empty - (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d} - - So Q can be {c,d}, {b,c,d} - -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: - - Q = grow( fv(T), C ) \ oclose( fv(G), C ) - -That is, quantify over all variable that that MIGHT be fixed by the -call site (which influences T), but which aren't DEFINITELY fixed by -G. This choice definitely quantifies over enough type variables, -albeit perhaps too many. - -Why grow( fv(T), C ) rather than fv(T)? Consider +********************************************************************************* +* * +* External interface * +* * +********************************************************************************* - class H x y | x->y where ... - - T = c->c - C = (H c d) - - If we used fv(T) = {c} we'd get the type - - forall c. H c d => c -> b - - And then if the fn was called at several different c's, each of - which fixed d differently, we'd get a unification error, because - d isn't quantified. Solution: quantify d. So we must quantify - everything that might be influenced by c. - -Why not oclose( fv(T), C )? Because we might not be able to see -all the functional dependencies yet: - - class H x y | x->y where ... - instance H x y => Eq (T x y) where ... - - 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. - - -There really isn't any point in quantifying over any more than -grow( fv(T), C ), because the call sites can't possibly influence -any other type variables. - - - -------------------------------------- - Note [Ambiguity] -------------------------------------- - -It's very hard to be certain when a type is ambiguous. Consider - - class K x - class H x y | x -> y - instance H x y => K (x,y) - -Is this type ambiguous? - forall a b. (K (a,b), Eq b) => a -> a - -Looks like it! But if we simplify (K (a,b)) we get (H a b) and -now we see that a fixes b. So we can't tell about ambiguity for sure -without doing a full simplification. And even that isn't possible if -the context has some free vars that may get unified. Urgle! - -Here's another example: is this ambiguous? - forall a b. Eq (T b) => a -> a -Not if there's an insance decl (with no context) - instance Eq (T b) where ... - -You may say of this example that we should use the instance decl right -away, but you can't always do that: - - class J a b where ... - instance J Int b where ... - - f :: forall a b. J a b => a -> a - -(Notice: no functional dependency in J's class decl.) -Here f's type is perfectly fine, provided f is only called at Int. -It's premature to complain when meeting f's signature, or even -when inferring a type for f. - - - -However, we don't *need* to report ambiguity right away. It'll always -show up at the call site.... and eventually at main, which needs special -treatment. Nevertheless, reporting ambiguity promptly is an excellent thing. - -So here's the plan. We WARN about probable ambiguity if - - fv(Cq) is not a subset of oclose(fv(T) union fv(G), C) - -(all tested before quantification). -That is, all the type variables in Cq must be fixed by the the variables -in the environment, or by the variables in the type. - -Notice that we union before calling oclose. Here's an example: - - class J a b c | a b -> c - fv(G) = {a} - -Is this ambiguous? - forall b c. (J a b c) => b -> b - -Only if we union {a} from G with {b} from T before using oclose, -do we see that c is fixed. - -It's a bit vague exactly which C we should use for this oclose call. If we -don't fix enough variables we might complain when we shouldn't (see -the above nasty example). Nothing will be perfect. That's why we can -only issue a warning. - - -Can we ever be *certain* about ambiguity? Yes: if there's a constraint - - c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY - -then c is a "bubble"; there's no way it can ever improve, and it's -certainly ambiguous. UNLESS it is a constant (sigh). And what about -the nasty example? +\begin{code} +simplifyTop :: WantedConstraints -> TcM (Bag EvBind) +-- Simplify top-level constraints +-- Usually these will be implications, +-- but when there is nothing to quantify we don't wrap +-- in a degenerate implication, so we do that here instead +simplifyTop wanteds + = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds + +------------------ +simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind) +simplifyInteractive wanteds + = simplifyCheck SimplInteractive wanteds + +------------------ +simplifyDefault :: ThetaType -- Wanted; has no type variables in it + -> TcM () -- Succeeds iff the constraint is soluble +simplifyDefault theta + = do { wanted <- newFlatWanteds DefaultOrigin theta + ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults"))) + (mkFlatWC wanted) + ; return () } +\end{code} - class K x - class H x y | x -> y - instance H x y => K (x,y) -Is this type ambiguous? - forall a b. (K (a,b), Eq b) => a -> a -Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after -is a "bubble" that's a set of constraints +********************************************************************************* +* * +* Deriving +* * +*********************************************************************************** - Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY +\begin{code} +simplifyDeriv :: CtOrigin + -> PredType + -> [TyVar] + -> ThetaType -- Wanted + -> TcM ThetaType -- Needed +-- Given instance (wanted) => C inst_ty +-- Simplify 'wanted' as much as possibles +-- Fail if not possible +simplifyDeriv orig pred tvs theta + = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize + -- The constraint solving machinery + -- expects *TcTyVars* not TyVars. + -- We use *non-overlappable* (vanilla) skolems + -- See Note [Overlap and deriving] + + ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols + subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs + doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred) + + ; wanted <- newFlatWanteds orig (substTheta skol_subst theta) + + ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted) + ; (residual_wanted, _binds) + <- runTcS (SimplInfer doc) NoUntouchables $ + solveWanteds emptyInert (mkFlatWC wanted) + + ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted) + -- See Note [Exotic derived instance contexts] + get_good :: WantedEvVar -> Either PredType WantedEvVar + get_good wev | validDerivPred p = Left p + | otherwise = Right wev + where p = evVarOfPred wev + + ; reportUnsolved (residual_wanted { wc_flat = bad }) + + ; let min_theta = mkMinimalBySCs (bagToList good) + ; return (substTheta subst_skol min_theta) } +\end{code} -Hence another idea. To decide Q start with fv(T) and grow it -by transitive closure in Cq (no functional dependencies involved). -Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok. -The definitely-ambiguous can then float out, and get smashed at top level -(which squashes out the constants, like Eq (T a) above) +Note [Overlap and deriving] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider some overlapping instances: + data Show a => Show [a] where .. + data Show [Char] where ... + +Now a data type with deriving: + data T a = MkT [a] deriving( Show ) + +We want to get the derived instance + instance Show [a] => Show (T a) where... +and NOT + instance Show a => Show (T a) where... +so that the (Show (T Char)) instance does the Right Thing + +It's very like the situation when we're inferring the type +of a function + f x = show [x] +and we want to infer + f :: Show [a] => a -> String + +BOTTOM LINE: use vanilla, non-overlappable skolems when inferring + the context for the derived instance. + Hence tcInstSkolTyVars not tcInstSuperSkolTyVars + +Note [Exotic derived instance contexts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In a 'derived' instance declaration, we *infer* the context. It's a +bit unclear what rules we should apply for this; the Haskell report is +silent. Obviously, constraints like (Eq a) are fine, but what about + data T f a = MkT (f a) deriving( Eq ) +where we'd get an Eq (f a) constraint. That's probably fine too. + +One could go further: consider + data T a b c = MkT (Foo a b c) deriving( Eq ) + instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) + +Notice that this instance (just) satisfies the Paterson termination +conditions. Then we *could* derive an instance decl like this: + + instance (C Int a, Eq b, Eq c) => Eq (T a b c) +even though there is no instance for (C Int a), because there just +*might* be an instance for, say, (C Int Bool) at a site where we +need the equality instance for T's. + +However, this seems pretty exotic, and it's quite tricky to allow +this, and yet give sensible error messages in the (much more common) +case where we really want that instance decl for C. + +So for now we simply require that the derived instance context +should have only type-variable constraints. +Here is another example: + data Fix f = In (f (Fix f)) deriving( Eq ) +Here, if we are prepared to allow -XUndecidableInstances we +could derive the instance + instance Eq (f (Fix f)) => Eq (Fix f) +but this is so delicate that I don't think it should happen inside +'deriving'. If you want this, write it yourself! + +NB: if you want to lift this condition, make sure you still meet the +termination conditions! If not, the deriving mechanism generates +larger and larger constraints. Example: + data Succ a = S a + data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show + +Note the lack of a Show instance for Succ. First we'll generate + instance (Show (Succ a), Show a) => Show (Seq a) +and then + instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) +and so on. Instead we want to complain of no instance for (Show (Succ a)). + +The bottom line +~~~~~~~~~~~~~~~ +Allow constraints which consist only of type variables, with no repeats. + +********************************************************************************* +* * +* Inference +* * +*********************************************************************************** - -------------------------------------- - Notes on principal types - -------------------------------------- +\begin{code} +simplifyInfer :: TopLevelFlag + -> Bool -- Apply monomorphism restriction + -> [(Name, TcTauType)] -- Variables to be generalised, + -- and their tau-types + -> WantedConstraints + -> TcM ([TcTyVar], -- Quantify over these type variables + [EvVar], -- ... and these constraints + TcEvBinds) -- ... binding these evidence variables +simplifyInfer top_lvl apply_mr name_taus wanteds + | isEmptyWC wanteds + = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked + ; zonked_taus <- zonkTcTypes (map snd name_taus) + ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs + ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify) + ; return (qtvs, [], emptyTcEvBinds) } - class C a where - op :: a -> a + | otherwise + = do { zonked_wanteds <- zonkWC wanteds + ; zonked_taus <- zonkTcTypes (map snd name_taus) + ; gbl_tvs <- tcGetGlobalTyVars + + ; traceTc "simplifyInfer {" $ vcat + [ ptext (sLit "apply_mr =") <+> ppr apply_mr + , ptext (sLit "zonked_taus =") <+> ppr zonked_taus + , ptext (sLit "wanted =") <+> ppr zonked_wanteds + ] + + -- Step 1 + -- Make a guess at the quantified type variables + -- Then split the constraints on the baisis of those tyvars + -- to avoid unnecessarily simplifying a class constraint + -- See Note [Avoid unecessary constraint simplification] + ; let zonked_tau_tvs = get_tau_tvs zonked_taus + proto_qtvs = growWanteds gbl_tvs zonked_wanteds $ + zonked_tau_tvs `minusVarSet` gbl_tvs + (perhaps_bound, surely_free) + = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds) + + ; traceTc "simplifyInfer proto" $ vcat + [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs + , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs + , ptext (sLit "surely_fref =") <+> ppr surely_free + ] + + ; emitFlats surely_free + ; traceTc "sinf" $ vcat + [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound + , ptext (sLit "surely_free =") <+> ppr surely_free + ] + + -- Step 2 + -- Now simplify the possibly-bound constraints + ; (simpl_results, tc_binds0) + <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $ + simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound }) + + ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint + (do { reportUnsolved simpl_results; failM }) + + -- Step 3 + -- Split again simplified_perhaps_bound, because some unifications + -- may have happened, and emit the free constraints. + ; gbl_tvs <- tcGetGlobalTyVars + ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs + ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results) + ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs + mr_qtvs = init_tvs `minusVarSet` constrained_tvs + constrained_tvs = tyVarsOfEvVarXs zonked_simples + qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs + (final_qtvs, (bound, free)) + | apply_mr = (mr_qtvs, (emptyBag, zonked_simples)) + | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples) + ; emitFlats free + + ; if isEmptyVarSet final_qtvs && isEmptyBag bound + then ASSERT( isEmptyBag (wc_insol simpl_results) ) + do { traceTc "} simplifyInfer/no quantification" empty + ; emitImplications (wc_impl simpl_results) + ; return ([], [], EvBinds tc_binds0) } + else do + + -- Step 4, zonk quantified variables + { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound + ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty) + | (name, ty) <- name_taus ] + -- Don't add the quantified variables here, because + -- they are also bound in ic_skols and we want them to be + -- tidied uniformly + skol_info = InferSkol poly_ids + + ; gloc <- getCtLoc skol_info + ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) + + -- Step 5 + -- Minimize `bound' and emit an implication + ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds + ; ev_binds_var <- newTcEvBinds + ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0 + ; lcl_env <- getLclTypeEnv + ; let implic = Implic { ic_untch = NoUntouchables + , ic_env = lcl_env + , ic_skols = mkVarSet qtvs_to_return + , ic_given = minimal_bound_ev_vars + , ic_wanted = simpl_results { wc_flat = bound } + , ic_insol = False + , ic_binds = ev_binds_var + , ic_loc = gloc } + ; emitImplication implic + ; traceTc "} simplifyInfer/produced residual implication for quantification" $ + vcat [ ptext (sLit "implic =") <+> ppr implic + -- ic_skols, ic_given give rest of result + , ptext (sLit "qtvs =") <+> ppr final_qtvs + , ptext (sLit "spb =") <+> ppr zonked_simples + , ptext (sLit "bound =") <+> ppr bound ] + + + + ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } } + where + get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes + | otherwise = exactTyVarsOfTypes + -- See Note [Silly type synonym] in TcType +\end{code} - f x = let g y = op (y::Int) in True -Here the principal type of f is (forall a. a->a) -but we'll produce the non-principal type - f :: forall a. C Int => a -> a +Note [Minimize by Superclasses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we quantify over a constraint, in simplifyInfer we need to +quantify over a constraint that is minimal in some sense: For +instance, if the final wanted constraint is (Eq alpha, Ord alpha), +we'd like to quantify over Ord alpha, because we can just get Eq alpha +from superclass selection from Ord alpha. This minimization is what +mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint +to check the original wanted. - -------------------------------------- - The need for forall's in constraints - -------------------------------------- +\begin{code} +simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints +simplifyWithApprox wanted + = do { traceTcS "simplifyApproxLoop" (ppr wanted) -[Exchange on Haskell Cafe 5/6 Dec 2000] + ; results <- solveWanteds emptyInert wanted - class C t where op :: t -> Bool - instance C [t] where op x = True + ; let (residual_implics, floats) = approximateImplications (wc_impl results) - p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ []) - q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f) + -- If no new work was produced then we are done with simplifyApproxLoop + ; if insolubleWC results || isEmptyBag floats + then return results -The definitions of p and q differ only in the order of the components in -the pair on their right-hand sides. And yet: + else solveWanteds emptyInert + (WC { wc_flat = floats `unionBags` wc_flat results + , wc_impl = residual_implics + , wc_insol = emptyBag }) } - ghc and "Typing Haskell in Haskell" reject p, but accept q; - Hugs rejects q, but accepts p; - hbc rejects both p and q; - nhc98 ... (Malcolm, can you fill in the blank for us!). +approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar) +-- Extracts any nested constraints that don't mention the skolems +approximateImplications impls + = do_bag (float_implic emptyVarSet) impls + where + do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c) + do_bag f = foldrBag (plus . f) (emptyBag, emptyBag) + plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c) + plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2) + + float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar) + float_implic skols imp + = (unitBag (imp { ic_wanted = wanted' }), floats) + where + (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp) -The type signature for f forces context reduction to take place, and -the results of this depend on whether or not the type of y is known, -which in turn depends on which component of the pair the type checker -analyzes first. + float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic }) + = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2) + where + (flat', floats1) = do_bag (float_flat skols) flat + (implic', floats2) = do_bag (float_implic skols) implic -Solution: if y::m a, float out the constraints - Monad m, forall c. C (m c) -When m is later unified with [], we can solve both constraints. + float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar) + float_flat skols wev + | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev) + | otherwise = (unitBag wev, emptyBag) +\end{code} +\begin{code} +-- (growX gbls wanted tvs) grows a seed 'tvs' against the +-- X-constraint 'wanted', nuking the 'gbls' at each stage +-- It's conservative in that if the seed could *possibly* +-- grow to include a type variable, then it does + +growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet +growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc) + +growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet +growWantedEVs gbl_tvs ws tvs + | isEmptyBag ws = tvs + | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs + +-------- Helper functions, do not do fixpoint ------------------------ +growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet +growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) . + growPreds gbl_tvs evVarOfPred (wc_flat wc) . + growPreds gbl_tvs evVarOfPred (wc_insol wc) + +growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet +growImplics gbl_tvs implics tvs + = foldrBag grow_implic tvs implics + where + grow_implic implic tvs + = grow tvs `minusVarSet` ic_skols implic + where + grow = growWC gbl_tvs (ic_wanted implic) . + growPreds gbl_tvs evVarPred (listToBag (ic_given implic)) + -- We must grow from givens too; see test IPRun - -------------------------------------- - Notes on implicit parameters - -------------------------------------- +growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet +growPreds gbl_tvs get_pred items tvs + = foldrBag extend tvs items + where + extend item tvs = tvs `unionVarSet` + (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs) + +-------------------- +quantifyMe :: TyVarSet -- Quantifying over these + -> WantedEvVar + -> Bool -- True <=> quantify over this wanted +quantifyMe qtvs wev + | isIPPred pred = True -- Note [Inheriting implicit parameters] + | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs + where + pred = evVarOfPred wev +\end{code} -Question 1: can we "inherit" implicit parameters -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Avoid unecessary constraint simplification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When inferring the type of a let-binding, with simplifyInfer, +try to avoid unnecessariliy simplifying class constraints. +Doing so aids sharing, but it also helps with delicate +situations like + instance C t => C [t] where .. + f :: C [t] => .... + f x = let g y = ...(constraint C [t])... + in ... +When inferring a type for 'g', we don't want to apply the +instance decl, because then we can't satisfy (C t). So we +just notice that g isn't quantified over 't' and partition +the contraints before simplifying. + +This only half-works, but then let-generalisation only half-works. + + +Note [Inheriting implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y @@ -444,2113 +474,843 @@ BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring. -Question 2: type signatures -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -BUT WATCH OUT: When you supply a type signature, we can't force you -to quantify over implicit parameters. For example: - - (?x + 1) :: Int - -This is perfectly reasonable. We do not want to insist on - - (?x + 1) :: (?x::Int => Int) - -That would be silly. Here, the definition site *is* the occurrence site, -so the above strictures don't apply. Hence the difference between -tcSimplifyCheck (which *does* allow implicit paramters to be inherited) -and tcSimplifyCheckBind (which does not). - -What about when you supply a type signature for a binding? -Is it legal to give the following explicit, user type -signature to f, thus: - - f :: Int -> Int - f x = (x::Int) + ?y - -At first sight this seems reasonable, but it has the nasty property -that adding a type signature changes the dynamic semantics. -Consider this: - - (let f x = (x::Int) + ?y - in (f 3, f 3 with ?y=5)) with ?y = 6 - - returns (3+6, 3+5) -vs - (let f :: Int -> Int - f x = x + ?y - in (f 3, f 3 with ?y=5)) with ?y = 6 - - returns (3+6, 3+6) - -Indeed, simply inlining f (at the Haskell source level) would change the -dynamic semantics. - -Nevertheless, as Launchbury says (email Oct 01) we can't really give the -semantics for a Haskell program without knowing its typing, so if you -change the typing you may change the semantics. - -To make things consistent in all cases where we are *checking* against -a supplied signature (as opposed to inferring a type), we adopt the -rule: - - a signature does not need to quantify over implicit params. - -[This represents a (rather marginal) change of policy since GHC 5.02, -which *required* an explicit signature to quantify over all implicit -params for the reasons mentioned above.] - -But that raises a new question. Consider - - Given (signature) ?x::Int - Wanted (inferred) ?x::Int, ?y::Bool - -Clearly we want to discharge the ?x and float the ?y out. But -what is the criterion that distinguishes them? Clearly it isn't -what free type variables they have. The Right Thing seems to be -to float a constraint that - neither mentions any of the quantified type variables - nor any of the quantified implicit parameters - -See the predicate isFreeWhenChecking. - - -Question 3: monomorphism -~~~~~~~~~~~~~~~~~~~~~~~~ -There's a nasty corner case when the monomorphism restriction bites: - - z = (x::Int) + ?y - -The argument above suggests that we *must* generalise -over the ?y parameter, to get - z :: (?y::Int) => Int, -but the monomorphism restriction says that we *must not*, giving - z :: Int. -Why does the momomorphism restriction say this? Because if you have - - let z = x + ?y in z+z - -you might not expect the addition to be done twice --- but it will if -we follow the argument of Question 2 and generalise over ?y. - - -Question 4: top level -~~~~~~~~~~~~~~~~~~~~~ -At the top level, monomorhism makes no sense at all. - - module Main where - main = let ?x = 5 in print foo - - foo = woggle 3 - - woggle :: (?x :: Int) => Int -> Int - woggle y = ?x + y - -We definitely don't want (foo :: Int) with a top-level implicit parameter -(?x::Int) becuase there is no way to bind it. - - -Possible choices -~~~~~~~~~~~~~~~~ -(A) Always generalise over implicit parameters - Bindings that fall under the monomorphism restriction can't - be generalised - - Consequences: - * Inlining remains valid - * No unexpected loss of sharing - * But simple bindings like - z = ?y + 1 - will be rejected, unless you add an explicit type signature - (to avoid the monomorphism restriction) - z :: (?y::Int) => Int - z = ?y + 1 - This seems unacceptable - -(B) Monomorphism restriction "wins" - Bindings that fall under the monomorphism restriction can't - be generalised - Always generalise over implicit parameters *except* for bindings - that fall under the monomorphism restriction - - Consequences - * Inlining isn't valid in general - * No unexpected loss of sharing - * Simple bindings like - z = ?y + 1 - accepted (get value of ?y from binding site) - -(C) Always generalise over implicit parameters - Bindings that fall under the monomorphism restriction can't - be generalised, EXCEPT for implicit parameters - Consequences - * Inlining remains valid - * Unexpected loss of sharing (from the extra generalisation) - * Simple bindings like - z = ?y + 1 - accepted (get value of ?y from occurrence sites) - - -Discussion -~~~~~~~~~~ -None of these choices seems very satisfactory. But at least we should -decide which we want to do. - -It's really not clear what is the Right Thing To Do. If you see - - z = (x::Int) + ?y - -would you expect the value of ?y to be got from the *occurrence sites* -of 'z', or from the valuue of ?y at the *definition* of 'z'? In the -case of function definitions, the answer is clearly the former, but -less so in the case of non-fucntion definitions. On the other hand, -if we say that we get the value of ?y from the definition site of 'z', -then inlining 'z' might change the semantics of the program. - -Choice (C) really says "the monomorphism restriction doesn't apply -to implicit parameters". Which is fine, but remember that every -innocent binding 'x = ...' that mentions an implicit parameter in -the RHS becomes a *function* of that parameter, called at each -use of 'x'. Now, the chances are that there are no intervening 'with' -clauses that bind ?y, so a decent compiler should common up all -those function calls. So I think I strongly favour (C). Indeed, -one could make a similar argument for abolishing the monomorphism -restriction altogether. - -BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted - - - -%************************************************************************ -%* * -\subsection{tcSimplifyInfer} -%* * -%************************************************************************ - -tcSimplify is called when we *inferring* a type. Here's the overall game plan: - - 1. Compute Q = grow( fvs(T), C ) - - 2. Partition C based on Q into Ct and Cq. Notice that ambiguous - predicates will end up in Ct; we deal with them at the top level - - 3. Try improvement, using functional dependencies - - 4. If Step 3 did any unification, repeat from step 1 - (Unification can change the result of 'grow'.) - -Note: we don't reduce dictionaries in step 2. For example, if we have -Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different -after step 2. However note that we may therefore quantify over more -type variables than we absolutely have to. - -For the guts, we need a loop, that alternates context reduction and -improvement with unification. E.g. Suppose we have - - class C x y | x->y where ... - -and tcSimplify is called with: - (C Int a, C Int b) -Then improvement unifies a with b, giving - (C Int a, C Int a) - -If we need to unify anything, we rattle round the whole thing all over -again. - - -\begin{code} -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) - -- 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) -\end{code} - -Example [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)! - -[NO TYVARS] - - class Y a b | a -> b where - y :: a -> X b - - instance Y [[a]] a where - y ((x:_):_) = X x - - k :: X a -> X a -> X a - - g :: Num a => [X a] -> [X a] - g xs = h xs - where - h ys = ys ++ map (k (y [[0]])) xs - -The excitement comes when simplifying the bindings for h. Initially -try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}. -From this we get t1:=:t2, but also various bindings. We can't forget -the bindings (because of [LOOP]), but in fact t1 is what g is -polymorphic in. - -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") - -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)) -\end{code} - - -%************************************************************************ -%* * -\subsection{tcSimplifyCheck} -%* * -%************************************************************************ - -@tcSimplifyCheck@ is used when we know exactly the set of variables -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. --- --- 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 } - where --- get_qtvs = zonkTcTyVarsAndFV qtvs - get_qtvs = return (mkVarSet qtvs) -- All skolems - - --- 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 - -tcSimplifyInferCheck doc tau_tvs givens wanted_lie - = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie - ; extendLIEs frees - ; return (qtvs', 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 -\end{code} - -Here is the workhorse function for all three wrappers. - -\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 () - - ; 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) -\end{code} - - -%************************************************************************ -%* * - tcSimplifySuperClasses -%* * -%************************************************************************ - -Note [SUPERCLASS-LOOP 1] -~~~~~~~~~~~~~~~~~~~~~~~~ -We have to be very, very careful when generating superclasses, lest we -accidentally build a loop. Here's an example: - - class S a - - class S a => C a where { opc :: a -> a } - class S b => D b where { opd :: b -> b } - - instance C Int where - opc = opd - - instance D Int where - opd = opc - -From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int} -Simplifying, we may well get: - $dfCInt = :C ds1 (opd dd) - dd = $dfDInt - ds1 = $p1 dd -Notice that we spot that we can extract ds1 from dd. - -Alas! Alack! We can do the same for (instance D Int): - - $dfDInt = :D ds2 (opc dc) - dc = $dfCInt - ds2 = $p1 dc - -And now we've defined the superclass in terms of itself. - -Solution: never generate a superclass selectors at all when -satisfying the superclass context of an instance declaration. - -Two more nasty cases are in - tcrun021 - tcrun033 - -\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) } - where - get_qtvs = return (mkVarSet qtvs) - doc = ptext SLIT("instance declaration superclass context") -\end{code} - - -%************************************************************************ -%* * -\subsection{tcSimplifyRestricted} -%* * -%************************************************************************ - -tcSimplifyRestricted infers which type variables to quantify for a -group of restricted bindings. This isn't trivial. - -Eg1: id = \x -> x - We want to quantify over a to get id :: forall a. a->a - -Eg2: eq = (==) - We do not want to quantify over a, because there's an Eq a - constraint, so we get eq :: a->a->Bool (notice no forall) - -So, assume: - RHS has type 'tau', whose free tyvars are tau_tvs - RHS has constraints 'wanteds' - -Plan A (simple) - Quantify over (tau_tvs \ ftvs(wanteds)) - This is bad. The constraints may contain (Monad (ST s)) - where we have instance Monad (ST s) where... - so there's no need to be monomorphic in s! - - Also the constraint might be a method constraint, - whose type mentions a perfectly innocent tyvar: - op :: Num a => a -> b -> a - Here, b is unconstrained. A good example would be - foo = op (3::Int) - We want to infer the polymorphic type - foo :: forall b. b -> b - - -Plan B (cunning, used for a long time up to and including GHC 6.2) - Step 1: Simplify the constraints as much as possible (to deal - with Plan A's problem). Then set - qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) - - Step 2: Now simplify again, treating the constraint as 'free' if - it does not mention qtvs, and trying to reduce it otherwise. - The reasons for this is to maximise sharing. - - This fails for a very subtle reason. Suppose that in the Step 2 - a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'. - In the Step 1 this constraint might have been simplified, perhaps to - (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'. - This won't happen in Step 2... but that in turn might prevent some other - constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) - and that in turn breaks the invariant that no constraints are quantified over. - - Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates - the problem. - - -Plan C (brutal) - Step 1: Simplify the constraints as much as possible (to deal - with Plan A's problem). Then set - qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) - Return the bindings from Step 1. - - -A note about Plan C (arising from "bug" reported by George Russel March 2004) -Consider this: - - instance (HasBinary ty IO) => HasCodedValue ty - - foo :: HasCodedValue a => String -> IO a - - doDecodeIO :: HasCodedValue a => () -> () -> IO a - doDecodeIO codedValue view - = let { act = foo "foo" } in act - -You might think this should work becuase the call to foo gives rise to a constraint -(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the -restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the -constraint using the (rather bogus) instance declaration, and now we are stuffed. - -I claim this is not really a bug -- but it bit Sergey as well as George. So here's -plan D - - -Plan D (a variant of plan B) - Step 1: Simplify the constraints as much as possible (to deal - with Plan A's problem), BUT DO NO IMPROVEMENT. Then set - qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) - - Step 2: Now simplify again, treating the constraint as 'free' if - it does not mention qtvs, and trying to reduce it otherwise. - - The point here is that it's generally OK to have too few qtvs; that is, - to make the thing more monomorphic than it could be. We don't want to - do that in the common cases, but in wierd cases it's ok: the programmer - can always add a signature. +********************************************************************************* +* * +* RULES * +* * +*********************************************************************************** - Too few qtvs => too many wanteds, which is what happens if you do less - improvement. +Note [Simplifying RULE lhs constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +On the LHS of transformation rules we only simplify only equalities, +but not dictionaries. We want to keep dictionaries unsimplified, to +serve as the available stuff for the RHS of the rule. We *do* want to +simplify equalities, however, to detect ill-typed rules that cannot be +applied. - -\begin{code} -tcSimplifyRestricted -- Used for restricted binding groups - -- i.e. ones subject to the monomorphism restriction - :: SDoc - -> TopLevelFlag - -> [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) - TcDictBinds) -- Bindings - -- tcSimpifyRestricted returns no constraints to - -- quantify over; by definition there are none. - -- They are all thrown back in the LIE - -tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds - -- Zonk everything in sight - = mappM zonkInst wanteds `thenM` \ wanteds' -> - - -- '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 - -- immediately, with no constraint on s. - -- - -- 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) -> - - -- 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', - ppr _binds, - ppr constrained_tvs', ppr tau_tvs', ppr qtvs' ]) `thenM_` - - -- 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'; - -- 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 - -- (B) under "implicit parameter and monomorphism" above. - -- - -- Remember that we may need to do *some* simplification, to - -- (for example) squash {Monad (ST s)} into {}. It's not enough - -- just to float all constraints - -- - -- 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 ) - - -- 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) -\end{code} - - -%************************************************************************ -%* * - tcSimplifyRuleLhs -%* * -%************************************************************************ - -On the LHS of transformation rules we only simplify methods and constants, -getting dictionaries. We want to keep all of them unsimplified, to serve -as the available stuff for the RHS of the rule. +Implementation: the TcSFlags carried by the TcSMonad controls the +amount of simplification, so simplifyRuleLhs just sets the flag +appropriately. Example. Consider the following left-hand side of a rule - f (x == y) (y > z) = ... - If we typecheck this expression we get constraints - d1 :: Ord a, d2 :: Eq a - We do NOT want to "simplify" to the LHS - forall x::a, y::a, z::a, d1::Ord a. f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ... - Instead we want - forall x::a, y::a, z::a, d1::Ord a, d2::Eq a. f ((==) d2 x y) ((>) d1 y z) = ... Here is another example: - fromIntegral :: (Integral a, Num b) => a -> b {-# RULES "foo" fromIntegral = id :: Int -> Int #-} - In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont* want to get - forall dIntegralInt. fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int - because the scsel will mess up RULE matching. Instead we want - forall dIntegralInt, dNumInt. fromIntegral Int Int dIntegralInt dNumInt = id Int Even if we have - g (x == y) (y == z) = .. - where the two dictionaries are *identical*, we do NOT WANT - forall x::a, y::a, z::a, d1::Eq a f ((==) d1 x y) ((>) d1 y z) = ... - because that will only match if the dict args are (visibly) equal. Instead we want to quantify over the dictionaries separately. -In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving -all dicts unchanged, with absolutely no sharing. It's simpler to do this -from scratch, rather than further parameterise simpleReduceLoop etc - -\begin{code} -tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds) -tcSimplifyRuleLhs wanteds - = go [] emptyBag wanteds - where - go dicts binds [] - = return (dicts, binds) - go dicts binds (w:ws) - | isDict w - = go (w:dicts) binds ws - | 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' - ; case lookup_result of - GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws) - SimpleInst rhs -> go dicts (addBind binds w rhs) ws - NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) - } -\end{code} +In short, simplifyRuleLhs must *only* squash equalities, leaving +all dicts unchanged, with absolutely no sharing. -tcSimplifyBracket is used when simplifying the constraints arising from -a Template Haskell bracket [| ... |]. We want to check that there aren't -any constraints that can't be satisfied (e.g. Show Foo, where Foo has no -Show instance), but we aren't otherwise interested in the results. -Nor do we care about ambiguous dictionaries etc. We will type check -this bracket again at its usage site. +HOWEVER, under a nested implication things are different +Consider + f :: (forall a. Eq a => a->a) -> Bool -> ... + {-# RULES "foo" forall (v::forall b. Eq b => b->b). + f b True = ... + #=} +Here we *must* solve the wanted (Eq a) from the given (Eq a) +resulting from skolemising the agument type of g. So we +revert to SimplCheck when going under an implication. \begin{code} -tcSimplifyBracket :: [Inst] -> TcM () -tcSimplifyBracket wanteds - = simpleReduceLoop doc reduceMe wanteds `thenM_` - returnM () - where - doc = text "tcSimplifyBracket" +simplifyRule :: RuleName + -> [TcTyVar] -- Explicit skolems + -> WantedConstraints -- Constraints from LHS + -> WantedConstraints -- Constraints from RHS + -> TcM ([EvVar], -- LHS dicts + TcEvBinds, -- Evidence for LHS + TcEvBinds) -- Evidence for RHS +-- See Note [Simplifying RULE lhs constraints] +simplifyRule name tv_bndrs lhs_wanted rhs_wanted + = do { loc <- getCtLoc (RuleSkol name) + ; zonked_lhs <- zonkWC lhs_wanted + ; let untch = NoUntouchables + -- We allow ourselves to unify environment + -- variables; hence *no untouchables* + + ; (lhs_results, lhs_binds) + <- runTcS (SimplRuleLhs name) untch $ + solveWanteds emptyInert zonked_lhs + + ; traceTc "simplifyRule" $ + vcat [ text "zonked_lhs" <+> ppr zonked_lhs + , text "lhs_results" <+> ppr lhs_results + , text "lhs_binds" <+> ppr lhs_binds + , text "rhs_wanted" <+> ppr rhs_wanted ] + + + -- Don't quantify over equalities (judgement call here) + ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred) + (wc_flat lhs_results) + lhs_dicts = map evVarOf (bagToList dicts) + -- Dicts and implicit parameters + + -- Fail if we have not got down to unsolved flats + ; ev_binds_var <- newTcEvBinds + ; emitImplication $ Implic { ic_untch = untch + , ic_env = emptyNameEnv + , ic_skols = mkVarSet tv_bndrs + , ic_given = lhs_dicts + , ic_wanted = lhs_results { wc_flat = eqs } + , ic_insol = insolubleWC lhs_results + , ic_binds = ev_binds_var + , ic_loc = loc } + + -- Notice that we simplify the RHS with only the explicitly + -- introduced skolems, allowing the RHS to constrain any + -- unification variables. + -- Then, and only then, we call zonkQuantifiedTypeVariables + -- Example foo :: Ord a => a -> a + -- foo_spec :: Int -> Int + -- {-# RULE "foo" foo = foo_spec #-} + -- Here, it's the RHS that fixes the type variable + + -- So we don't want to make untouchable the type + -- variables in the envt of the RHS, because they include + -- the template variables of the RULE + + -- Hence the rather painful ad-hoc treatement here + ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds + ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name) + ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $ + WC { wc_flat = emptyBag + , wc_insol = emptyBag + , wc_impl = unitBag $ + Implic { ic_untch = NoUntouchables + , ic_env = emptyNameEnv + , ic_skols = mkVarSet tv_bndrs + , ic_given = lhs_dicts + , ic_wanted = rhs_wanted + , ic_insol = insolubleWC rhs_wanted + , ic_binds = rhs_binds_var + , ic_loc = loc } } + ; rhs_binds2 <- readTcRef evb_ref + + ; return ( lhs_dicts + , EvBinds lhs_binds + , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) } \end{code} -%************************************************************************ -%* * -\subsection{Filtering at a dynamic binding} -%* * -%************************************************************************ - -When we have - let ?x = R in B - -we must discharge all the ?x constraints from B. We also do an improvement -step; if we have ?x::t1 and ?x::t2 we must unify t1, t2. - -Actually, the constraints from B might improve the types in ?x. For example - - f :: (?x::Int) => Char -> Char - let ?x = 3 in f 'c' - -then the constraint (?x::Int) arising from the call to f will -force the binding for ?x to be of type Int. - -\begin{code} -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) - - -- Simplify any methods that mention the implicit parameter - try_me inst | isFreeWrtIPs ip_set inst = Free - | otherwise = ReduceMe NoSCs - - simpl_loop givens wanteds - = mappM zonkInst givens `thenM` \ givens' -> - mappM zonkInst wanteds `thenM` \ wanteds' -> - - reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) -> - - if no_improvement then - ASSERT( null irreds ) - returnM (frees, binds) - else - simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) -> - returnM (frees1, binds `unionBags` binds1) -\end{code} - - -%************************************************************************ -%* * -\subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@} -%* * -%************************************************************************ - -When doing a binding group, we may have @Insts@ of local functions. -For example, we might have... -\begin{verbatim} -let f x = x + 1 -- orig local function (overloaded) - f.1 = f Int -- two instances of f - f.2 = f Float - in - (f.1 5, f.2 6.7) -\end{verbatim} -The point is: we must drop the bindings for @f.1@ and @f.2@ here, -where @f@ is in scope; those @Insts@ must certainly not be passed -upwards towards the top-level. If the @Insts@ were binding-ified up -there, they would have unresolvable references to @f@. - -We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@. -For each method @Inst@ in the @init_lie@ that mentions one of the -@Ids@, we create a binding. We return the remaining @Insts@ (in an -@LIE@), as well as the @HsBinds@ generated. - -\begin{code} -bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds --- Simlifies only MethodInsts, and generate only bindings of form --- fm = f tys dicts --- We're careful not to even generate bindings of the form --- d1 = d2 --- You'd think that'd be fine, but it interacts with what is --- arguably a bug in Match.tidyEqnInfo (see notes there) - -bindInstsOfLocalFuns wanteds local_ids - | null overloaded_ids - -- Common case - = extendLIEs wanteds `thenM_` - 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 - where - doc = text "bindInsts" <+> ppr local_ids - overloaded_ids = filter is_overloaded local_ids - is_overloaded id = isOverloadedTy (idType id) - (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds - - 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} - - -%************************************************************************ -%* * -\subsection{Data types for the reduction mechanism} -%* * -%************************************************************************ - -The main control over context reduction is here - -\begin{code} -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. - -- 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 - -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 - Bool -- True <=> actually consumed (splittable IPs only) - - | Rhs -- Used when there is a RHS - (LHsExpr TcId) -- The RHS - [Inst] -- Insts free in the RHS; we need these too - - | Linear -- Splittable Insts only. - Int -- The Int is always 2 or more; indicates how - -- many copies are required - Inst -- The splitter - Avail -- Where the "master copy" is - - | LinRhss -- Splittable Insts only; this is used only internally - -- by extractResults, where a Linear - -- is turned into an LinRhss - [LHsExpr TcId] -- A supply of suitable RHSs - -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 b) = text "Given" <+> ppr x <+> - if b then text "(used)" else empty -pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs) -pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a -pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss -\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 +********************************************************************************* +* * +* Main Simplifier * +* * +*********************************************************************************** -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 - - Just (Linear n split_inst avail) -- Transform Linear --> LinRhss - -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) -> - split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) -> - go (addToFM avails w (LinRhss rhss)) - (binds `unionBags` binds') - irreds' frees' (split_inst : w : ws) - - Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss - -> go new_avails new_binds irreds frees ws - where - new_binds = addBind binds w rhs - new_avails = addToFM avails w (LinRhss rhss) - - -- get_root is just used for Linear - get_root irreds frees (Given id _) w = returnM (irreds, frees, id) - get_root irreds frees Irred w = cloneDict w `thenM` \ w' -> - returnM (w':irreds, frees, instToId w') - get_root irreds frees IsFree w = cloneDict w `thenM` \ w' -> - returnM (irreds, w':frees, instToId w') - - add_given avails w = addToFM avails w (Given (instToId w) True) - - 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! - -split :: Int -> TcId -> TcId -> Inst - -> TcM (TcDictBinds, [LHsExpr TcId]) --- (split n split_id root_id wanted) returns --- * a list of 'n' expressions, all of which witness 'avail' --- * a bunch of auxiliary bindings to support these expressions --- * one or zero insts needed to witness the whole lot --- (maybe be zero if the initial Inst is a Given) +simplifyCheck :: SimplContext + -> WantedConstraints -- Wanted + -> TcM (Bag EvBind) +-- Solve a single, top-level implication constraint +-- e.g. typically one created from a top-level type signature +-- f :: forall a. [a] -> [a] +-- f x = rhs +-- We do this even if the function has no polymorphism: +-- g :: Int -> Int + +-- g y = rhs +-- (whereas for *nested* bindings we would not create +-- an implication constraint for g at all.) -- --- NB: 'wanted' is just a template +-- Fails if can't solve something in the input wanteds +simplifyCheck ctxt wanteds + = do { wanteds <- zonkWC wanteds + + ; traceTc "simplifyCheck {" (vcat + [ ptext (sLit "wanted =") <+> ppr wanteds ]) + + ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $ + solveWanteds emptyInert wanteds + + ; traceTc "simplifyCheck }" $ + ptext (sLit "unsolved =") <+> ppr unsolved + + ; reportUnsolved unsolved + + ; return ev_binds } + +---------------- +solveWanteds :: InertSet -- Given + -> WantedConstraints + -> TcS WantedConstraints +solveWanteds inert wanted + = do { (unsolved_flats, unsolved_implics, insols) + <- solve_wanteds inert wanted + ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived + , wc_impl = unsolved_implics + , wc_insol = insols }) } + +solve_wanteds :: InertSet -- Given + -> WantedConstraints + -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar) +-- solve_wanteds iterates when it is able to float equalities +-- out of one or more of the implications +solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols }) + = do { traceTcS "solveWanteds {" (ppr wanted) + + -- Try the flat bit + -- Discard from insols all the derived/given constraints + -- because they will show up again when we try to solve + -- everything else. Solving them a second time is a bit + -- of a waste, but the code is simple, and the program is + -- wrong anyway! + ; let all_flats = flats `unionBags` keepWanted insols + ; inert1 <- solveInteractWanted inert (bagToList all_flats) + + ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics + + ; bb <- getTcEvBindsBag + ; tb <- getTcSTyBindsMap + ; traceTcS "solveWanteds }" $ + vcat [ text "unsolved_flats =" <+> ppr unsolved_flats + , text "unsolved_implics =" <+> ppr unsolved_implics + , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) + , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb)) + ] + + ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats + -- See Note [Solving Family Equations] + -- NB: remaining_flats has already had subst applied + + ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats + + ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats + , mapBag (substImplication subst) unsolved_implics + , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) } -split n split_id root_id wanted - = go n where - ty = linearInstType wanted - pair_ty = mkTyConApp pairTyCon [ty,ty] - id = instToId wanted - occ = getOccName id - loc = getSrcLoc id - span = instSpan wanted - - go 1 = returnM (emptyBag, [L span $ HsVar root_id]) - - go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) -> - expand n rhss `thenM` \ (binds2, rhss') -> - returnM (binds1 `unionBags` binds2, rhss') - - -- (expand n rhss) - -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings - -- e.g. expand 3 [rhs1, rhs2] - -- = ( { x = split rhs1 }, - -- [fst x, snd x, rhs2] ) - expand n rhss - | n `rem` 2 == 0 = go rhss -- n is even - | otherwise = go (tail rhss) `thenM` \ (binds', rhss') -> - returnM (binds', head rhss : rhss') - where - go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') -> - returnM (listToBag binds', concat rhss') - - do_one rhs = newUnique `thenM` \ uniq -> - tcLookupId fstName `thenM` \ fst_id -> - tcLookupId sndName `thenM` \ snd_id -> - let - x = mkUserLocal occ uniq pair_ty loc - in - returnM (L span (VarBind x (mk_app span split_id rhs)), - [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x]) - -mk_fs_app span id ty var = nlHsTyApp id [ty,ty] `mkHsApp` (L span (HsVar var)) - -mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs) - -addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst)) - (VarBind (instToId inst) rhs)) -instSpan wanted = instLocSrcSpan (instLoc wanted) -\end{code} - - -%************************************************************************ -%* * -\subsection[reduce]{@reduce@} -%* * -%************************************************************************ - -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} - - - -\begin{code} -reduceContext :: SDoc - -> (Inst -> WhatToDo) - -> [Inst] -- Given - -> [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 -> - - -- 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 [ - text "----------------------", - doc, - text "given" <+> ppr givens, - 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 [ - text "----------------------", - doc, - text "wanted" <+> ppr wanteds, - text "----", - text "avails" <+> pprAvails avails, - text "frees" <+> ppr frees, - 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) - ] - -- 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 + simpl_loop :: Int + -> InertSet + -> Bag Implication + -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived + simpl_loop n inert implics + | n>10 + = trace "solveWanteds: loop" $ -- Always bleat + do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively + ; let (_, unsolved_cans) = extractUnsolved inert + ; return (unsolved_cans, implics) } + + | otherwise + = do { traceTcS "solveWanteds: simpl_loop start {" $ + vcat [ text "n =" <+> ppr n + , text "implics =" <+> ppr implics + , text "inert =" <+> ppr inert ] + + ; let (just_given_inert, unsolved_cans) = extractUnsolved inert + -- unsolved_cans contains either Wanted or Derived! + + ; (implic_eqs, unsolved_implics) + <- solveNestedImplications just_given_inert unsolved_cans implics + + -- Apply defaulting rules if and only if there + -- no floated equalities. If there are, they may + -- solve the remaining wanteds, so don't do defaulting. + ; improve_eqs <- if not (isEmptyBag implic_eqs) + then return implic_eqs + else applyDefaultingRules just_given_inert unsolved_cans + + ; traceTcS "solveWanteds: simpl_loop end }" $ + vcat [ text "improve_eqs =" <+> ppr improve_eqs + , text "unsolved_flats =" <+> ppr unsolved_cans + , text "unsolved_implics =" <+> ppr unsolved_implics ] + + ; (improve_eqs_already_in_inert, inert_with_improvement) + <- solveInteract inert improve_eqs + + ; if improve_eqs_already_in_inert then + return (unsolved_cans, unsolved_implics) + else + simpl_loop (n+1) inert_with_improvement + -- Contain unsolved_cans and the improve_eqs + unsolved_implics + } + +givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar +-- Extract the Wanted ones from CanonicalCts and conver to +-- Givens; not Given/Solved, see Note [Preparing inert set for implications] +givensFromWanteds _ctxt = foldrBag getWanted emptyBag where - unify ((qtvs, pairs), what1, what2) - = addErrCtxtM (mkEqnMsg what1 what2) $ - tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) -> - mapM_ (unif_pr tenv) pairs - unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2) - -pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] - -mkEqnMsg (pred1,from1) (pred2,from2) tidy_env - = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2 - ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' } - ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"), - nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), - nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])] - ; return (tidy_env, msg) } -\end{code} - -The main context-reduction function is @reduce@. Here's its game plan. + getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar + getWanted cc givens + | pushable_wanted cc + = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol) + in given `consBag` givens -- and not mkSolvedFlavor, + -- see Note [Preparing inert set for implications] + | otherwise = givens + + pushable_wanted :: CanonicalCt -> Bool + pushable_wanted cc + | not (isCFrozenErr cc) + , isWantedCt cc + = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications] + | otherwise = False + +solveNestedImplications :: InertSet -> CanonicalCts + -> Bag Implication + -> TcS (Bag FlavoredEvVar, Bag Implication) +solveNestedImplications just_given_inert unsolved_cans implics + | isEmptyBag implics + = return (emptyBag, emptyBag) + | otherwise + = do { -- See Note [Preparing inert set for implications] + -- Push the unsolved wanteds inwards, but as givens + + ; simpl_ctx <- getTcSContext + + ; let pushed_givens = givensFromWanteds simpl_ctx unsolved_cans + tcs_untouchables = filterVarSet isFlexiTcsTv $ + tyVarsOfEvVarXs pushed_givens + -- See Note [Extra TcsTv untouchables] + + ; traceTcS "solveWanteds: preparing inerts for implications {" + (vcat [ppr tcs_untouchables, ppr pushed_givens]) + + ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens + + ; traceTcS "solveWanteds: } now doing nested implications {" $ + vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics + , text "implics =" <+> ppr implics ] + + ; (implic_eqs, unsolved_implics) + <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics + + ; traceTcS "solveWanteds: done nested implications }" $ + vcat [ text "implic_eqs =" <+> ppr implic_eqs + , text "unsolved_implics =" <+> ppr unsolved_implics ] + + ; return (implic_eqs, unsolved_implics) } + +solveImplication :: TcTyVarSet -- Untouchable TcS unification variables + -> InertSet -- Given + -> Implication -- Wanted + -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type + Bag Implication) -- Unsolved rest (always empty or singleton) +-- Returns: +-- 1. A bag of floatable wanted constraints, not mentioning any skolems, +-- that are of the form unification var = type +-- +-- 2. Maybe a unsolved implication, empty if entirely solved! +-- +-- Precondition: everything is zonked by now +solveImplication tcs_untouchables inert + imp@(Implic { ic_untch = untch + , ic_binds = ev_binds + , ic_skols = skols + , ic_given = givens + , ic_wanted = wanteds + , ic_loc = loc }) + = nestImplicTcS ev_binds (untch, tcs_untouchables) $ + recoverTcS (return (emptyBag, emptyBag)) $ + -- Recover from nested failures. Even the top level is + -- just a bunch of implications, so failing at the first + -- one is bad + do { traceTcS "solveImplication {" (ppr imp) + + -- Solve flat givens + ; given_inert <- solveInteractGiven inert loc givens + + -- Simplify the wanteds + ; (unsolved_flats, unsolved_implics, insols) + <- solve_wanteds given_inert wanteds + + ; let (res_flat_free, res_flat_bound) + = floatEqualities skols givens unsolved_flats + final_flat = keepWanted res_flat_bound + + ; let res_wanted = WC { wc_flat = final_flat + , wc_impl = unsolved_implics + , wc_insol = insols } + res_implic = unitImplication $ + imp { ic_wanted = res_wanted + , ic_insol = insolubleWC res_wanted } + + ; traceTcS "solveImplication end }" $ vcat + [ text "res_flat_free =" <+> ppr res_flat_free + , text "res_implic =" <+> ppr res_implic ] + + ; return (res_flat_free, res_implic) } + + +floatEqualities :: TcTyVarSet -> [EvVar] + -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar) +-- Post: The returned FlavoredEvVar's are only Wanted or Derived +-- and come from the input wanted ev vars or deriveds +floatEqualities skols can_given wantders + | hasEqualities can_given = (emptyBag, wantders) + -- Note [Float Equalities out of Implications] + | otherwise = partitionBag is_floatable wantders + -\begin{code} -reduceList :: (Int,[Inst]) -- Stack (for err msgs) - -- along with its depth - -> (Inst -> WhatToDo) - -> [Inst] - -> Avails - -> TcM Avails + where is_floatable :: FlavoredEvVar -> Bool + is_floatable (EvVarX cv _fl) + | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv) + is_floatable _flev = False + + tvs_under_fsks :: Type -> TyVarSet + -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym + tvs_under_fsks (TyVarTy tv) + | not (isTcTyVar tv) = unitVarSet tv + | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty + | otherwise = unitVarSet tv + tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys) + tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty + tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res + tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg + tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder + -- can mention type variables! + | isTyVar tv = inner_tvs `delVarSet` tv + | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) ) + inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv) + where + inner_tvs = tvs_under_fsks ty + + predTvs_under_fsks :: PredType -> TyVarSet + predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty + predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys) + predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2 \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 -#ifdef DEBUG - ; if n > 8 then - dumpTcRn (text "Interesting! Context reduction stack deeper than 8:" - <+> (int n $$ ifPprDebug (nest 2 (pprStack stack)))) - else return () -#endif - ; if n >= ctxtStkDepth dopts then - failWithTc (reduceDepthErr n stack) - 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 ws state' } - - -- Base case: we're done! -reduce stack try_me wanted avails - -- It's the same as an existing inst, or a superclass thereof - | Just avail <- isAvailable avails wanted - = if isLinearInst wanted then - addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') -> - reduceList stack try_me wanteds' avails' - else - returnM avails -- No op for non-linear things - - | 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, - -- 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 - -- 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 - 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 -\end{code} +Note [Preparing inert set for implications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Before solving the nested implications, we convert any unsolved flat wanteds +to givens, and add them to the inert set. Reasons: + + a) In checking mode, suppresses unnecessary errors. We already have + on unsolved-wanted error; adding it to the givens prevents any + consequential errors from showing up + + b) More importantly, in inference mode, we are going to quantify over this + constraint, and we *don't* want to quantify over any constraints that + are deducible from it. + + c) Flattened type-family equalities must be exposed to the nested + constraints. Consider + F b ~ alpha, (forall c. F b ~ alpha) + Obviously this is soluble with [alpha := F b]. But the + unification is only done by solveCTyFunEqs, right at the end of + solveWanteds, and if we aren't careful we'll end up with an + unsolved goal inside the implication. We need to "push" the + as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it + can be used to solve the inner (F b + ~ alpha). See Trac #4935. + + d) There are other cases where interactions between wanteds that can help + to solve a constraint. For example + + class C a b | a -> b + + (C Int alpha), (forall d. C d blah => C Int a) + + If we push the (C Int alpha) inwards, as a given, it can produce + a fundep (alpha~a) and this can float out again and be used to + fix alpha. (In general we can't float class constraints out just + in case (C d blah) might help to solve (C Int a).) + +The unsolved wanteds are *canonical* but they may not be *inert*, +because when made into a given they might interact with other givens. +Hence the call to solveInteract. Example: + + Original inert set = (d :_g D a) /\ (co :_w a ~ [beta]) + +We were not able to solve (a ~w [beta]) but we can't just assume it as +given because the resulting set is not inert. Hence we have to do a +'solveInteract' step first. + +Finally, note that we convert them to [Given] and NOT [Given/Solved]. +The reason is that Given/Solved are weaker than Givens and may be discarded. +As an example consider the inference case, where we may have, the following +original constraints: + [Wanted] F Int ~ Int + (F Int ~ a => F Int ~ a) +If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next +given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting +the (F Int ~ a) insoluble. Hence we should really convert the residual +wanteds to plain old Given. + +We need only push in unsolved equalities both in checking mode and inference mode: + + (1) In checking mode we should not push given dictionaries in because of +example LongWayOverlapping.hs, where we might get strange overlap +errors between far-away constraints in the program. But even in +checking mode, we must still push type family equations. Consider: + + type instance F True a b = a + type instance F False a b = b + + [w] F c a b ~ gamma + (c ~ True) => a ~ gamma + (c ~ False) => b ~ gamma + +Since solveCTyFunEqs happens at the very end of solving, the only way to solve +the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not +merely Given/Solved because it has to interact with the top-level instance +environment) and push it inside the implications. Now, when we come out again at +the end, having solved the implications solveCTyFunEqs will solve this equality. + + (2) In inference mode, we recheck the final constraint in checking mode and +hence we will be able to solve inner implications from top-level quantified +constraints nonetheless. + + +Note [Extra TcsTv untouchables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Furthemore, we record the inert set simplifier-generated unification +variables of the TcsTv kind (such as variables from instance that have +been applied, or unification flattens). These variables must be passed +to the implications as extra untouchable variables. Otherwise we have +the danger of double unifications. Example (from trac ticket #4494): + + (F Int ~ uf) /\ (forall a. C a => F Int ~ beta) + +In this example, beta is touchable inside the implication. The first +solveInteract step leaves 'uf' ununified. Then we move inside the +implication where a new constraint + uf ~ beta +emerges. We may spontaneously solve it to get uf := beta, so the whole +implication disappears but when we pop out again we are left with (F +Int ~ uf) which will be unified by our final solveCTyFunEqs stage and +uf will get unified *once more* to (F Int). + +The solution is to record the TcsTvs (i.e. the simplifier-generated +unification variables) that are generated when solving the flats, and +make them untouchables for the nested implication. In the example +above uf would become untouchable, so beta would be forced to be +unified as beta := uf. + +NB: A consequence is that every simplifier-generated TcsTv variable + that gets floated out of an implication becomes now untouchable + next time we go inside that implication to solve any residual + constraints. In effect, by floating an equality out of the + implication we are committing to have it solved in the outside. + +Note [Float Equalities out of Implications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We want to float equalities out of vanilla existentials, but *not* out +of GADT pattern matches. \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 -addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst]) -addLinearAvailable avails avail wanted - -- avails currently maps [wanted -> avail] - -- Extend avails to reflect a neeed for an extra copy of avail - - | Just avail' <- split_avail avail - = returnM (addToFM avails wanted avail', []) - - | otherwise - = tcLookupId splitName `thenM` \ split_id -> - tcInstClassOp (instLoc wanted) split_id - [linearInstType wanted] `thenM` \ split_inst -> - returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst]) - - where - split_avail :: Avail -> Maybe Avail - -- (Just av) if there's a modified version of avail that - -- we can use to replace avail in avails - -- Nothing if there isn't, so we need to create a Linear - split_avail (Linear n i a) = Just (Linear (n+1) i a) - split_avail (Given id used) | not used = Just (Given id True) - | otherwise = Nothing - split_avail Irred = Nothing - split_avail IsFree = Nothing - split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails) - -------------------------- -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) False) - -- 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 } +solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts) +-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible +-- See Note [Solving Family Equations] +-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications +-- where the newly generated equalities (alpha := F xi) have been substituted through. +solveCTyFunEqs cts + = do { untch <- getUntouchables + ; let (unsolved_can_cts, (ni_subst, cv_binds)) + = getSolvableCTyFunEqs untch cts + ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:" + , ppr ni_subst, ppr cv_binds + ]) + ; mapM_ solve_one cv_binds + + ; return (niFixTvSubst ni_subst, unsolved_can_cts) } 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) } + solve_one (cv,tv,ty) = do { setWantedTyBind tv ty + ; setCoBind cv (mkReflCo ty) } + +------------ +type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)]) + -- The TvSubstEnv is not idempotent, but is loop-free + -- See Note [Non-idempotent substitution] in Unify +emptyFunEqBinds :: FunEqBinds +emptyFunEqBinds = (emptyVarEnv, []) + +extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds +extendFunEqBinds (tv_subst, cv_binds) cv tv ty + = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds) + +------------ +getSolvableCTyFunEqs :: TcsUntouchables + -> CanonicalCts -- Precondition: all Wanteds or Derived! + -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables +getSolvableCTyFunEqs untch cts + = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts 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 + dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt + -> (CanonicalCts, FunEqBinds) + dflt_funeq (cts_in, feb@(tv_subst, _)) + (CFunEqCan { cc_id = cv + , cc_flavor = fl + , cc_fun = tc + , cc_tyargs = xis + , cc_rhs = xi }) + | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable + + , isTouchableMetaTyVar_InRange untch tv + -- And it's a *touchable* unification variable + + , typeKind xi `isSubKind` tyVarKind tv + -- Must do a small kind check since TcCanonical invariants + -- on family equations only impose compatibility, not subkinding + + , not (tv `elemVarEnv` tv_subst) + -- Check not in extra_binds + -- See Note [Solving Family Equations], Point 1 + + , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis)) + -- Occurs check: see Note [Solving Family Equations], Point 2 + = ASSERT ( not (isGivenOrSolved fl) ) + (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis)) + + dflt_funeq (cts_in, fun_eq_binds) ct + = (cts_in `extendCCans` ct, fun_eq_binds) \end{code} -Note [SUPERCLASS-LOOP 2] -~~~~~~~~~~~~~~~~~~~~~~~~ -But the above isn't enough. Suppose we are *given* d1:Ord a, -and want to deduce (d2:C [a]) where - - class Ord a => C a where - instance Ord [a] => C [a] where ... - -Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the -superclasses of C [a] to avails. But we must not overwrite the binding -for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just -build a loop! - -Here's another variant, immortalised in tcrun020 - class Monad m => C1 m - class C1 m => C2 m x - instance C2 Maybe Bool -For the instance decl we need to build (C1 Maybe), and it's no good if -we run around and add (C2 Maybe Bool) and its superclasses to the avails -before we search for C1 Maybe. - -Here's another example - class Eq b => Foo a b - instance Eq a => Foo [a] a -If we are reducing - (Foo [t] t) - -we'll first deduce that it holds (via the instance decl). We must not -then overwrite the Eq t constraint with a superclass selection! - -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 -first time, but reducible next time. - -Now we implement the Right Solution, which is to check for loops directly -when adding superclasses. It's a bit like the occurs check in unification. - - -Note [RECURSIVE DICTIONARIES] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data D r = ZeroD | SuccD (r (D r)); - - instance (Eq (r (D r))) => Eq (D r) where - ZeroD == ZeroD = True - (SuccD a) == (SuccD b) = a == b - _ == _ = False; - - equalDC :: D [] -> D [] -> Bool; - equalDC = (==); - -We need to prove (Eq (D [])). Here's how we go: - - d1 : Eq (D []) - -by instance decl, holds if - d2 : Eq [D []] - where d1 = dfEqD d2 - -by instance decl of Eq, holds if - d3 : D [] - where d2 = dfEqList d3 - d1 = dfEqD d2 - -But now we can "tie the knot" to give - - d3 = d1 - d2 = dfEqList d3 - d1 = dfEqD d2 - -and it'll even run! The trick is to put the thing we are trying to prove -(in this case Eq (D []) into the database before trying to prove its -contributing clauses. - - -%************************************************************************ -%* * -\section{tcSimplifyTop: defaulting} -%* * -%************************************************************************ - - -@tcSimplifyTop@ is called once per module to simplify all the constant -and ambiguous Insts. - -We need to be careful of one case. Suppose we have - - instance Num a => Num (Foo a b) where ... - -and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify -to (Num x), and default x to Int. But what about y?? - -It's OK: the final zonking stage should zap y to (), which is fine. +Note [Solving Family Equations] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +After we are done with simplification we may be left with constraints of the form: + [Wanted] F xis ~ beta +If 'beta' is a touchable unification variable not already bound in the TyBinds +then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'. + +When is it ok to do so? + 1) 'beta' must not already be defaulted to something. Example: + + [Wanted] F Int ~ beta <~ Will default [beta := F Int] + [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We + have to report this as unsolved. + + 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to + set [beta := F xis] only if beta is not among the free variables of xis. + + 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS + of type family equations. See Inert Set invariants in TcInteract. + + +********************************************************************************* +* * +* Defaulting and disamgiguation * +* * +********************************************************************************* + +Basic plan behind applyDefaulting rules: + + Step 1: + Split wanteds into defaultable groups, `groups' and the rest `rest_wanted' + For each defaultable group, do: + For each possible substitution for [alpha |-> tau] where `alpha' is the + group's variable, do: + 1) Make up new TcEvBinds + 2) Extend TcS with (groupVariable + 3) given_inert <- solveOne inert (given : a ~ tau) + 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints) + 5) if unsolved == empty then + sneakyUnify a |-> tau + write the evidence bins + return (final_inert ++ group_constraints,[]) + -- will contain the info (alpha |-> tau)!! + goto next defaultable group + if unsolved <> empty then + throw away evidence binds + try next substitution + If you've run out of substitutions for this group, too bad, you failed + return (inert,group) + goto next defaultable group + + Step 2: + Collect all the (canonical-cts, wanteds) gathered this way. + - Do a solveGiven over the canonical-cts to make sure they are inert +------------------------------------------------------------------------------------------ \begin{code} -tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds -tcSimplifyTop wanteds - = do { ext_default <- doptM Opt_ExtendedDefaultRules - ; tc_simplify_top doc ext_default AddSCs wanteds } - where - doc = text "tcSimplifyTop" - -tcSimplifyInteractive wanteds - = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds +applyDefaultingRules :: InertSet + -> CanonicalCts -- All wanteds + -> TcS (Bag FlavoredEvVar) -- All wanteds again! +-- Return some *extra* givens, which express the +-- type-class-default choice + +applyDefaultingRules inert wanteds + | isEmptyBag wanteds + = return emptyBag + | otherwise + = do { untch <- getUntouchables + ; tv_cts <- mapM (defaultTyVar untch) $ + varSetElems (tyVarsOfCDicts wanteds) + + ; info@(_, default_tys, _) <- getDefaultInfo + ; let groups = findDefaultableGroups info untch wanteds + ; deflt_cts <- mapM (disambigGroup default_tys inert) groups + + ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts + , text "Type defaults =" <+> ppr deflt_cts]) + + ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) } + +------------------ +defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar) +-- defaultTyVar is used on any un-instantiated meta type variables to +-- default the kind of ? and ?? etc to *. This is important to ensure +-- that instance declarations match. For example consider +-- instance Show (a->b) +-- foo x = show (\_ -> True) +-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), +-- and that won't match the typeKind (*) in the instance decl. +-- See test tc217. +-- +-- We look only at touchable type variables. No further constraints +-- are going to affect these type variables, so it's time to do it by +-- hand. However we aren't ready to default them fully to () or +-- whatever, because the type-class defaulting rules have yet to run. + +defaultTyVar untch the_tv + | isTouchableMetaTyVar_InRange untch the_tv + , not (k `eqKind` default_k) + = do { ev <- TcSMonad.newKindConstraint the_tv default_k + ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk + ; return (unitBag (mkEvVarX ev (Wanted loc))) } + | otherwise + = return emptyBag -- The common case + where + k = tyVarKind the_tv + default_k = defaultKind k + + +---------------- +findDefaultableGroups + :: ( SimplContext + , [Type] + , (Bool,Bool) ) -- (Overloaded strings, extended default rules) + -> TcsUntouchables -- Untouchable + -> CanonicalCts -- Unsolved + -> [[(CanonicalCt,TcTyVar)]] +findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) + untch wanteds + | not (performDefaulting ctxt) = [] + | null default_tys = [] + | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries) where - doc = text "tcSimplifyTop" - --- 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 []" - + unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints + non_unaries :: [CanonicalCt] -- and *other* constraints - -- 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 -\end{code} - -If a dictionary constrains a type variable which is - * not mentioned in the environment - * and not mentioned in the type of the expression -then it is ambiguous. No further information will arise to instantiate -the type variable; nor will it be generalised and turned into an extra -parameter to a function. - -It is an error for this to occur, except that Haskell provided for -certain rules to be applied in the special case of numeric types. -Specifically, if - * at least one of its classes is a numeric class, and - * all of its classes are numeric or standard -then the type variable can be defaulted to the first type in the -default-type list which is an instance of all the offending classes. - -So here is the function which does the work. It takes the ambiguous -dictionaries and either resolves them (producing bindings) or -complains. It works by splitting the dictionary list by type -variable, and using @disambigOne@ to do the real business. - -@disambigOne@ assumes that its arguments dictionaries constrain all -the same type variable. - -ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to -@()@ instead of @Int@. I reckon this is the Right Thing to do since -the most common use of defaulting is code like: -\begin{verbatim} - _ccall_ foo `seqPrimIO` bar -\end{verbatim} -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 - -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 + (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds) + -- Finds unary type-class constraints + find_unary cc@(CDictCan { cc_tyargs = [ty] }) + | Just tv <- tcGetTyVar_maybe ty + = Left (cc, tv) + find_unary cc = Right cc -- Non unary or non dictionary + + bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries + bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries + + cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2 + + is_defaultable_group ds@((_,tv):_) + = isTyConableTyVar tv -- Note [Avoiding spurious errors] + && not (tv `elemVarSet` bad_tvs) + && isTouchableMetaTyVar_InRange untch tv + && defaultable_classes [cc_class cc | (cc,_) <- ds] + is_defaultable_group [] = panic "defaultable_group" + + defaultable_classes clss + | extended_defaults = any isInteractiveClass clss + | otherwise = all is_std_class clss && (any is_num_class clss) + + -- In interactive mode, or with -XExtendedDefaultRules, + -- we default Show a to Show () to avoid graututious errors on "show []" + isInteractiveClass cls + = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey]) + + 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 + -> InertSet -- Given inert + -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) + -- sharing same type variable + -> TcS (Bag FlavoredEvVar) + +disambigGroup [] _inert _grp + = return emptyBag +disambigGroup (default_ty:default_tys) inert group + = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty) + ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty + ; let der_flav = mk_derived_flavor (cc_flavor the_ct) + derived_eq = mkEvVarX ev der_flav + + ; success <- tryTcS $ + do { (_,final_inert) <- solveInteract inert $ listToBag $ + derived_eq : wanted_ev_vars + ; let (_, unsolved) = extractUnsolved final_inert + ; let wanted_unsolved = filterBag isWantedCt unsolved + -- Don't care about Derived's + ; return (isEmptyBag wanted_unsolved) } + ; case success of + True -> -- Success: record the type variable binding, and return + do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty + ; traceTcS "disambigGroup succeeded" (ppr default_ty) + ; return (unitBag derived_eq) } + False -> -- Failure: try with the next type + do { traceTcS "disambigGroup failed, will try other default types" + (ppr default_ty) + ; disambigGroup default_tys inert group } } 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] } } + ((the_ct,the_tv):_) = group + wanteds = map fst group + wanted_ev_vars :: [FlavoredEvVar] + wanted_ev_vars = map deCanonicalise wanteds + + mk_derived_flavor :: CtFlavor -> CtFlavor + mk_derived_flavor (Wanted loc) = Derived loc + mk_derived_flavor _ = panic "Asked to disambiguate given or derived!" \end{code} -[Aside - why the defaulting mechanism is turned off when - dealing with arguments and results to ccalls. +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 -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. -The interaction between the defaulting mechanism for numeric -values and CC & CR can be a bit puzzling to the user at times. -For example, - x <- _ccall_ f - if (x /= 0) then - _ccall_ g x - else - return () - -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. - -End of aside] - - -%************************************************************************ -%* * -\subsection[simple]{@Simple@ versions} -%* * -%************************************************************************ - -Much simpler versions when there are no bindings to make! - -@tcSimplifyThetas@ simplifies class-type constraints formed by -@deriving@ declarations and when specialising instances. We are -only interested in the simplified bunch of class/type constraints. - -It simplifies to constraints of the form (C a b c) where -a,b,c are type variables. This is required for the context of -instance declarations. +********************************************************************************* +* * +* Utility functions +* * +********************************************************************************* \begin{code} -tcSimplifyDeriv :: TyCon - -> [TyVar] - -> ThetaType -- Wanted - -> TcM ThetaType -- Needed - -tcSimplifyDeriv tc tyvars theta - = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) -> - -- 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 DerivOrigin (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 - tv_set = mkVarSet tvs - - (bad_insts, ok_insts) = partition is_bad_inst irreds - is_bad_inst dict - = let pred = dictPred dict -- reduceMe squashes all non-dicts - in isEmptyVarSet (tyVarsOfPred pred) - -- Things like (Eq T) are bad - || (not gla_exts && not (isTyVarClassPred pred)) - - 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 - - addNoInstanceErrs Nothing [] bad_insts `thenM_` - mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_` - returnM (substTheta rev_env simpl_theta) - where - doc = ptext SLIT("deriving classes for a data type") -\end{code} - -@tcSimplifyDefault@ just checks class-type constraints, essentially; -used with \tr{default} declarations. We are only interested in -whether it worked or not. - -\begin{code} -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_` - if null irreds then - returnM () - else - failM - where - doc = ptext SLIT("default declaration") -\end{code} - - -%************************************************************************ -%* * -\section{Errors and contexts} -%* * -%************************************************************************ - -ToDo: for these error messages, should we note the location as coming -from the insts, or just whatever seems to be around in the monad just -now? - -\begin{code} -groupErrs :: ([Inst] -> TcM ()) -- Deal with one group - -> [Inst] -- The offending Insts - -> TcM () --- Group together insts with the same origin --- We want to report them together in error messages - -groupErrs report_err [] - = returnM () -groupErrs report_err (inst:insts) - = do_one (inst:friends) `thenM_` - 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, - -- and it avoids need equality on InstLocs.) - (friends, others) = partition is_friend insts - loc_msg = showSDoc (pprInstLoc (instLoc inst)) - is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg - do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts) - -- Add location and context information derived from the 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))) - -addTopIPErrs :: [Name] -> [Inst] -> TcM () -addTopIPErrs bndrs [] - = return () -addTopIPErrs bndrs ips - = addErrTcM (tidy_env, mk_msg 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") - <+> pprBinders bndrs <> colon)], - nest 2 (vcat (map ppr_ip ips)), - monomorphism_fix] - ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip) - -strangeTopIPErrs :: [Inst] -> TcM () -strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all - = groupErrs report tidy_dicts - where - (tidy_env, tidy_dicts) = tidyInsts dicts - report dicts = addErrTcM (tidy_env, mk_msg dicts) - 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 - -> 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 -#ifdef DEBUG - ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict) -#endif - ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match - res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts) - 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 - mk_overlap_msg dict (matches, unifiers) - = 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 - else -- One match, plus some unifiers - 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")])] - where - ispecs = [ispec | (_, ispec) <- matches] - - 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)] - -- 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 - -addTopAmbigErrs dicts --- Divide into groups that share a common set of ambiguous tyvars - = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts]) - where - (tidy_env, tidy_dicts) = tidyInsts dicts - - tvs_of :: Inst -> [TcTyVar] - tvs_of d = varSetElems (tyVarsOfInst d) - cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2 - - 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)) $ - -- the location of the first one will do for the err message - addErrTcM (tidy_env, msg $$ mono_msg) - where - dicts = map fst pairs - msg = sep [text "Ambiguous type variable" <> plural tvs <+> - pprQuotedList tvs <+> in_msg, - nest 2 (pprDictsInFull dicts)] - in_msg = text "in the constraint" <> plural dicts <> colon - - -mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message) --- There's an error with these Insts; if they have free type variables --- it's probably caused by the monomorphism restriction. --- 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) - where - 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")) - -warnDefault dicts default_ty - = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag -> - addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg) - where - -- 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"), - nest 4 (pprStack stack)] - -pprStack stack = vcat (map pprInstInFull stack) -\end{code} +newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar) +newFlatWanteds orig theta + = do { loc <- getCtLoc orig + ; evs <- newWantedEvVars theta + ; return (listToBag [EvVarX w loc | w <- evs]) } +\end{code} \ No newline at end of file