-%
-% (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(..), (<.>), emptyLHsBinds )
-
+import HsSyn
import TcRnMonad
-import Inst ( lookupInst, LookupInstResult(..),
- tyVarsOfInst, fdPredsOfInsts,
- isDict, isClassDict,
- isMethodFor, isMethod,
- instToId, tyVarsOfInsts,
- ipNamesOfInsts, ipNamesOfInst, dictPred,
- fdPredsOfInst,
- newDictBndrs, newDictBndrsO,
- getDictClassTys, isTyVarDict, instLoc,
- zonkInst, tidyInsts, tidyMoreInsts,
- pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
- isInheritableInst, pprDictsTheta
- )
-import TcEnv ( tcGetGlobalTyVars, findGlobals, pprBinders,
- lclEnvElts, tcMetaTy )
-import InstEnv ( lookupInstEnv, classInstances, pprInstances )
-import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType )
-import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
- mkClassPred, isOverloadedTy, isSkolemTyVar,
- mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
- tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
-import TcIface ( checkWiredInTyCon )
-import Id ( idType )
-import Var ( TyVar )
-import TyCon ( TyCon )
-import Name ( Name )
-import NameSet ( NameSet, mkNameSet, elemNameSet )
-import Class ( classBigSig, classKey )
-import FunDeps ( oclose, grow, improve, pprEquation )
-import PrelInfo ( isNumericClass, isStandardClass )
-import PrelNames ( integerTyConName,
- showClassKey, eqClassKey, ordClassKey )
-import Type ( zipTopTvSubst, substTheta, substTy )
-import TysWiredIn ( 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
-|
-| <interactive>:1:
-| Could not deduce (Bar a b) from the context (Foo a b)
-| arising from use of `foo' at <interactive>: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
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.
+*********************************************************************************
+* *
+* RULES *
+* *
+***********************************************************************************
- 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.
+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.
- Too few qtvs => too many wanteds, which is what happens if you do less
- improvement.
-
-
-\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
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.
-\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}
-
-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.
+*********************************************************************************
+* *
+* Main Simplifier *
+* *
+***********************************************************************************
\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
+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.)
+--
+-- 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 ) }
- | 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
+ 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
+ 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
+
-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]
+ 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}
+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}
-type Avails = FiniteMap Inst Avail
-emptyAvails = emptyFM
-data Avail
- = IsFree -- Used for free Insts
- | Irred -- Used for irreducible dictionaries,
- -- which are going to be lambda bound
-
- | Given TcId -- Used for dictionaries for which we have a binding
- -- e.g. those "given" in a signature
-
- | Rhs -- Used when there is a RHS
- (LHsExpr TcId) -- The RHS
- [Inst] -- Insts free in the RHS; we need these too
-
-pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
- | (inst,avail) <- fmToList avails ]
-
-instance Outputable Avail where
- ppr = pprAvail
-
-pprAvail IsFree = text "Free"
-pprAvail Irred = text "Irred"
-pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
-\end{code}
-
-Extracting the bindings from a bunch of Avails.
-The bindings do *not* come back sorted in dependency order.
-We assume that they'll be wrapped in a big Rec, so that the
-dependency analyser can sort them out later
-
-The loop startes
-\begin{code}
-extractResults :: Avails
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds, -- Bindings
- [Inst], -- Irreducible ones
- [Inst]) -- Free ones
-
-extractResults avails wanteds
- = go avails emptyBag [] [] wanteds
+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
- go avails binds irreds frees []
- = returnM (binds, irreds, frees)
-
- go avails binds irreds frees (w:ws)
- = case lookupFM avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds frees ws
-
- Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
- Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
-
- Just (Given id) -> go avails new_binds irreds frees ws
- where
- new_binds | id == instToId w = binds
- | otherwise = addBind binds w (L (instSpan w) (HsVar id))
- -- The sought Id can be one of the givens, via a superclass chain
- -- and then we definitely don't want to generate an x=x binding!
-
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
-
- add_given avails w = addToFM avails w (Given (instToId w))
-
- add_free avails w | isMethod w = avails
- | otherwise = add_given avails w
- -- NB: Hack alert!
- -- Do *not* replace Free by Given if it's a method.
- -- The following situation shows why this is bad:
- -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
- -- From an application (truncate f i) we get
- -- t1 = truncate at f
- -- t2 = t1 at i
- -- If we have also have a second occurrence of truncate, we get
- -- t3 = truncate at f
- -- t4 = t3 at i
- -- When simplifying with i,f free, we might still notice that
- -- t1=t3; but alas, the binding for t2 (which mentions t1)
- -- will continue to float out!
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
- (VarBind (instToId inst) rhs))
-instSpan wanted = instLocSrcSpan (instLoc wanted)
-\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
+ 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
- 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.
-
-\begin{code}
-reduceList :: (Int,[Inst]) -- Stack (for err msgs)
- -- along with its depth
- -> (Inst -> WhatToDo)
- -> [Inst]
- -> Avails
- -> TcM Avails
+ 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}
-@reduce@ is passed
- try_me: given an inst, this function returns
- Reduce reduce this
- DontReduce return this in "irreds"
- Free return this in "frees"
+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
+------------------------------------------------------------------------------------------
- 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
- = returnM avails
-
+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
- = 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}
-
-
-\begin{code}
--------------------------
-isAvailable :: Avails -> Inst -> Maybe Avail
-isAvailable avails wanted = lookupFM avails wanted
- -- NB 1: the Ord instance of Inst compares by the class/type info
- -- *not* by unique. So
- -- d1::C Int == d2::C Int
-
--------------------------
-addFree :: Avails -> Inst -> TcM Avails
- -- When an Inst is tossed upstairs as 'free' we nevertheless add it
- -- to avails, so that any other equal Insts will be commoned up right
- -- here rather than also being tossed upstairs. This is really just
- -- an optimisation, and perhaps it is more trouble that it is worth,
- -- as the following comments show!
- --
- -- NB: do *not* add superclasses. If we have
- -- df::Floating a
- -- dn::Num a
- -- but a is not bound here, then we *don't* want to derive
- -- dn from df here lest we lose sharing.
- --
-addFree avails free = returnM (addToFM avails free IsFree)
-
-addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted want_scs avails wanted rhs_expr wanteds
- = addAvailAndSCs want_scs avails wanted avail
- where
- avail = Rhs rhs_expr wanteds
-
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
- -- Always add superclasses for 'givens'
- --
- -- No ASSERT( not (given `elemFM` avails) ) because in an instance
- -- decl for Ord t we can add both Ord t and Eq t as 'givens',
- -- so the assert isn't true
-
-addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
-addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
- addAvailAndSCs want_scs avails irred Irred
-
-addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
-addAvailAndSCs want_scs avails inst avail
- | not (isClassDict inst) = return avails_with_inst
- | NoSCs <- want_scs = return avails_with_inst
- | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
- ; addSCs is_loop avails_with_inst inst }
- where
- avails_with_inst = addToFM avails inst avail
-
- is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
- -- Note: this compares by *type*, not by Unique
- deps = findAllDeps (unitVarSet (instToId inst)) avail
- dep_tys = map idType (varSetElems deps)
-
- findAllDeps :: IdSet -> Avail -> IdSet
- -- Find all the Insts that this one depends on
- -- See Note [SUPERCLASS-LOOP 2]
- -- Watch out, though. Since the avails may contain loops
- -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
- findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
- findAllDeps so_far other = so_far
-
- find_all :: IdSet -> Inst -> IdSet
- find_all so_far kid
- | kid_id `elemVarSet` so_far = so_far
- | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
- | otherwise = so_far'
- where
- so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
- kid_id = instToId kid
-
-addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
- -- Add all the superclasses of the Inst to Avails
- -- The first param says "dont do this because the original thing
- -- depends on this one, so you'd build a loop"
- -- Invariant: the Inst is already in Avails.
-
-addSCs is_loop avails dict
- = do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
- ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
+ = 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
- (clas, tys) = getDictClassTys dict
- (tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
-
- add_sc avails (sc_dict, sc_sel)
- | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
- | is_given sc_dict = return avails
- | otherwise = addSCs is_loop avails' sc_dict
- where
- sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
- co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
- avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
-
- is_given :: Inst -> Bool
- is_given sc_dict = case lookupFM avails sc_dict of
- Just (Given _) -> True -- Given is cheaper than superclass selection
- other -> False
-\end{code}
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough. Suppose we are *given* d1:Ord a,
-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.
-
-
-\begin{code}
-tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
-tcSimplifyTop wanteds
- = do { ext_default <- doptM Opt_ExtendedDefaultRules
- ; tc_simplify_top doc ext_default AddSCs wanteds }
+ 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"
-
-tcSimplifyInteractive wanteds
- = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
- 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 :: InstOrigin
- -> TyCon
- -> [TyVar]
- -> ThetaType -- Wanted
- -> TcM ThetaType -- Needed
-
-tcSimplifyDeriv orig 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 orig (substTheta tenv theta) `thenM` \ wanteds ->
- simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
- ASSERT( null frees ) -- reduceMe never returns Free
-
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
- let
- 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
projects / ghc-hetmet.git / blobdiff