%
\section[TcSimplify]{TcSimplify}
-Notes:
-Inference (local definitions)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the inst constrains a local type variable, then
- [ReduceMe] if it's a literal or method inst, reduce it
- [DontReduce] otherwise see whether the inst is just a constant
- if succeed, use it
- if not, add original to context
- This check gets rid of constant dictionaries without
- losing sharing.
+\begin{code}
+module TcSimplify (
+ tcSimplifyInfer, tcSimplifyInferCheck,
+ tcSimplifyCheck, tcSimplifyRestricted,
+ tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
+
+ tcSimplifyThetas, tcSimplifyCheckThetas,
+ bindInstsOfLocalFuns
+ ) where
+
+#include "HsVersions.h"
+
+import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
+import TcHsSyn ( TcExpr, TcId,
+ TcMonoBinds, TcDictBinds
+ )
+
+import TcMonad
+import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
+ tyVarsOfInst, predsOfInsts, predsOfInst,
+ isDict, isClassDict, instName,
+ isStdClassTyVarDict, isMethodFor,
+ instToId, tyVarsOfInsts,
+ instBindingRequired, instCanBeGeneralised,
+ newDictsFromOld, instMentionsIPs,
+ getDictClassTys, isTyVarDict,
+ instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
+ Inst, LIE, pprInsts, pprInstsInFull,
+ mkLIE, lieToList
+ )
+import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
+import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
+
+import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
+import TcType ( ThetaType, PredType, mkClassPred, isOverloadedTy,
+ mkTyVarTy, tcGetTyVar, isTyVarClassPred,
+ tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
+ inheritablePred, predHasFDs )
+import Id ( idType )
+import NameSet ( mkNameSet )
+import Class ( classBigSig )
+import FunDeps ( oclose, grow, improve )
+import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
+
+import Subst ( mkTopTyVarSubst, substTheta, substTy )
+import TysWiredIn ( unitTy )
+import VarSet
+import FiniteMap
+import Outputable
+import ListSetOps ( equivClasses )
+import Util ( zipEqual )
+import List ( partition )
+import CmdLineOpts
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{NOTES}
+%* *
+%************************************************************************
+
+ --------------------------------------
+ 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
+
+ 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.
+
+
+
+ --------------------------------------
+ Notes on ambiguity
+ --------------------------------------
+
+It's very hard to be certain when a type is ambiguous. Consider
-If the inst does not constrain a local type variable then
- [Free] then throw it out as free.
+ class K x
+ class H x y | x -> y
+ instance H x y => K (x,y)
-Inference (top level definitions)
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If the inst does not constrain a local type variable, then
- [FreeIfTautological] try for tautology;
- if so, throw it out as free
- (discarding result of tautology check)
- if not, make original inst part of the context
- (eliminating superclasses as usual)
+Is this type ambiguous?
+ forall a b. (K (a,b), Eq b) => a -> a
-If the inst constrains a local type variable, then
- as for inference (local defns)
+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 ...
-Checking (local defns)
-~~~~~~~~
-If the inst constrains a local type variable then
- [ReduceMe] reduce (signal error on failure)
+You may say of this example that we should use the instance decl right
+away, but you can't always do that:
-If the inst does not constrain a local type variable then
- [Free] throw it out as free.
+ class J a b where ...
+ instance J Int b where ...
-Checking (top level)
-~~~~~~~~~~~~~~~~~~~~
-If the inst constrains a local type variable then
- as for checking (local defns)
+ f :: forall a b. J a b => a -> a
-If the inst does not constrain a local type variable then
- as for checking (local defns)
+(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.
-Checking once per module
-~~~~~~~~~~~~~~~~~~~~~~~~~
-For dicts of the form (C a), where C is a std class
- and "a" is a type variable,
- [DontReduce] add to context
+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.
-otherwise [ReduceMe] always reduce
+So here's the plan. We WARN about probable ambiguity if
-[NB: we may generate one Tree [Int] dict per module, so
- sharing is not complete.]
+ fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
-Sort out ambiguity at the end.
+(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.
-Principal types
-~~~~~~~~~~~~~~~
-class C a where
- op :: a -> a
+Notice that we union before calling oclose. Here's an example:
-f x = let g y = op (y::Int) in True
+ 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?
+
+ 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
+
+ Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
+
+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)
+
+
+ --------------------------------------
+ Notes on principal types
+ --------------------------------------
+
+ class C a where
+ op :: a -> a
+
+ 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
-Ambiguity
-~~~~~~~~~
+ --------------------------------------
+ Notes on implicit parameters
+ --------------------------------------
+
+Question 1: can we "inherit" implicit parameters
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
- instance C (T a) Int where ...
- instance C (T a) Bool where ...
+ f x = (x::Int) + ?y
+
+where f is *not* a top-level binding.
+From the RHS of f we'll get the constraint (?y::Int).
+There are two types we might infer for f:
+
+ f :: Int -> Int
+
+(so we get ?y from the context of f's definition), or
+
+ f :: (?y::Int) => Int -> Int
+
+At first you might think the first was better, becuase then
+?y behaves like a free variable of the definition, rather than
+having to be passed at each call site. But of course, the WHOLE
+IDEA is that ?y should be passed at each call site (that's what
+dynamic binding means) so we'd better infer the second.
+
+BOTTOM LINE: you *must* quantify over implicit parameters. See
+isFreeAndInheritable.
+
+BUT WATCH OUT: for *expressions*, this isn't right. Consider:
+
+ (?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).
+
+
+Question 2: type signatures
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+OK, so is it legal to give an 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.
+
+Conclusion: the above type signature is illegal. You'll get a message
+of the form "could not deduce (?y::Int) from ()".
-and suppose we infer a context
- C (T x) y
+Question 3: monomorphism
+~~~~~~~~~~~~~~~~~~~~~~~~
+There's a nasty corner case when the monomorphism restriction bites:
-from some expression, where x and y are type varibles,
-and x is ambiguous, and y is being quantified over.
-Should we complain, or should we generate the type
+ z = (x::Int) + ?y
- forall x y. C (T x) y => <type not involving x>
+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
-The idea is that at the call of the function we might
-know that y is Int (say), so the "x" isn't really ambiguous.
-Notice that we have to add "x" to the type variables over
-which we generalise.
+ let z = x + ?y in z+z
-Something similar can happen even if C constrains only ambiguous
-variables. Suppose we infer the context
+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.
- C [x]
-where x is ambiguous. Then we could infer the type
- forall x. C [x] => <type not involving x>
+Possible choices
+~~~~~~~~~~~~~~~~
+(A) Always generalise over implicit parameters
+ Bindings that fall under the monomorphism restriction can't
+ be generalised
-in the hope that at the call site there was an instance
-decl such as
+ 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
- instance Num a => C [a] where ...
+(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
-and hence the default mechanism would resolve the "a".
+ 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}
-module TcSimplify (
- tcSimplify, tcSimplifyAndCheck,
- tcSimplifyTop, tcSimplifyThetas, tcSimplifyCheckThetas,
- bindInstsOfLocalFuns
- ) where
+tcSimplifyInfer
+ :: SDoc
+ -> TcTyVarSet -- fv(T); type vars
+ -> LIE -- Wanted
+ -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
+ LIE, -- Free
+ TcDictBinds, -- Bindings
+ [TcId]) -- Dict Ids that must be bound here (zonked)
+\end{code}
-#include "HsVersions.h"
-import CmdLineOpts ( opt_MaxContextReductionDepth )
-import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
-import TcHsSyn ( TcExpr, TcIdOcc(..), TcIdBndr,
- TcMonoBinds, TcDictBinds
- )
+\begin{code}
+tcSimplifyInfer doc tau_tvs wanted_lie
+ = inferLoop doc (varSetElems tau_tvs)
+ (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
-import TcMonad
-import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
- tyVarsOfInst,
- isDict, isStdClassTyVarDict, isMethodFor,
- instToId, instBindingRequired, instCanBeGeneralised,
- newDictFromOld,
- instLoc, getDictClassTys,
- pprInst, zonkInst, tidyInst, tidyInsts,
- Inst, LIE, pprInsts, pprInstsInFull, mkLIE, emptyLIE,
- plusLIE, pprOrigin
- )
-import TcEnv ( TcIdOcc(..), tcGetGlobalTyVars )
-import TcType ( TcType, TcTyVarSet, typeToTcType )
-import TcUnify ( unifyTauTy )
-import Id ( idType )
-import VarSet ( mkVarSet )
+ -- Check for non-generalisable insts
+ mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
-import Bag ( bagToList )
-import Class ( Class, ClassInstEnv, classBigSig, classInstEnv )
-import PrelInfo ( isNumericClass, isCreturnableClass )
+ returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
-import Type ( Type, ThetaType, TauType, mkTyVarTy, getTyVar,
- isTyVarTy, substFlexiTheta, splitSigmaTy,
- tyVarsOfTypes
- )
-import PprType ( pprConstraint )
-import TysWiredIn ( unitTy )
-import VarSet
-import VarEnv ( zipVarEnv )
-import FiniteMap
-import BasicTypes ( TopLevelFlag(..) )
-import CmdLineOpts ( opt_GlasgowExts )
-import Outputable
-import Util
-import List ( partition )
+inferLoop doc tau_tvs wanteds
+ = -- Step 1
+ zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
+ mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
+ let
+ preds = predsOfInsts wanteds'
+ qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+
+ try_me inst
+ | isFreeAndInheritable qtvs inst = Free
+ | isClassDict inst = DontReduceUnlessConstant -- Dicts
+ | otherwise = ReduceMe -- Lits and Methods
+ in
+ -- Step 2
+ reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+ -- Step 3
+ if no_improvement then
+ returnTc (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)
+
+ inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
+ returnTc (qtvs1, frees1, binds `AndMonoBinds` 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)!
+
+\begin{code}
+isFreeAndInheritable qtvs inst
+ = isFree qtvs inst -- Constrains no quantified vars
+ && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
+ -- (see "Notes on implicit parameters")
+
+isFree qtvs inst
+ = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
\end{code}
%************************************************************************
%* *
-\subsection[tcSimplify-main]{Main entry function}
+\subsection{tcSimplifyCheck}
%* *
%************************************************************************
-The main wrapper is @tcSimplify@. It just calls @tcSimpl@, but with
-the ``don't-squash-consts'' flag set depending on top-level ness. For
-top level defns we *do* squash constants, so that they stay local to a
-single defn. This makes things which are inlined more likely to be
-exportable, because their constants are "inside". Later passes will
-float them out if poss, after inlinings are sorted out.
+@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}
-tcSimplify
- :: SDoc
- -> TopLevelFlag
- -> TcTyVarSet s -- ``Local'' type variables
- -- ASSERT: this tyvar set is already zonked
- -> LIE s -- Wanted
- -> TcM s (LIE s, -- Free
- TcDictBinds s, -- Bindings
- LIE s) -- Remaining wanteds; no dups
-
-tcSimplify str top_lvl local_tvs wanted_lie
- | isEmptyVarSet local_tvs
- = returnTc (wanted_lie, EmptyMonoBinds, emptyLIE)
+tcSimplifyCheck
+ :: SDoc
+ -> [TcTyVar] -- Quantify over these
+ -> [Inst] -- Given
+ -> LIE -- Wanted
+ -> TcM (LIE, -- Free
+ TcDictBinds) -- Bindings
+
+-- tcSimplifyCheck is used when checking exprssion type signatures,
+-- class decls, instance decls etc.
+-- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
+-- It's important that we can float out non-inheritable predicates
+-- Example: (?x :: Int) is ok!
+tcSimplifyCheck doc qtvs givens wanted_lie
+ = tcSimplCheck doc isFree get_qtvs
+ givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
+ returnTc (frees, binds)
+ where
+ get_qtvs = zonkTcTyVarsAndFV qtvs
+
+
+-- 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
+ -> LIE -- Wanted
+ -> TcM ([TcTyVar], -- Variables over which to quantify
+ LIE, -- Free
+ TcDictBinds) -- Bindings
+
+tcSimplifyInferCheck doc tau_tvs givens wanted_lie
+ = tcSimplCheck doc isFreeAndInheritable get_qtvs givens wanted_lie
+ 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 `thenNF_Tc` \ all_tvs' ->
+ tcGetGlobalTyVars `thenNF_Tc` \ 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
+ returnNF_Tc qtvs
+\end{code}
- | otherwise
- = reduceContext str try_me [] wanteds `thenTc` \ (binds, frees, irreds) ->
+Here is the workhorse function for all three wrappers.
- -- Check for non-generalisable insts
+\begin{code}
+tcSimplCheck doc is_free get_qtvs givens wanted_lie
+ = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
+
+ -- Complain about any irreducible ones
+ complainCheck doc givens irreds `thenNF_Tc_`
+
+ -- Done
+ returnTc (qtvs, mkLIE frees, binds)
+
+ where
+ check_loop givens wanteds
+ = -- Step 1
+ mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
+ mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ get_qtvs `thenNF_Tc` \ 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 | is_free qtvs' inst = Free
+ | otherwise = ReduceMe
+ in
+ reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+ -- Step 3
+ if no_improvement then
+ returnTc (varSetElems qtvs', frees, binds, irreds)
+ else
+ check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
+ returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{tcSimplifyRestricted}
+%* *
+%************************************************************************
+
+\begin{code}
+tcSimplifyRestricted -- Used for restricted binding groups
+ -- i.e. ones subject to the monomorphism restriction
+ :: SDoc
+ -> TcTyVarSet -- Free in the type of the RHSs
+ -> LIE -- Free in the RHSs
+ -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
+ LIE, -- Free
+ TcDictBinds) -- Bindings
+
+tcSimplifyRestricted doc tau_tvs wanted_lie
+ = -- First squash out all methods, to find the constrained tyvars
+ -- We can't just take the free vars of wanted_lie because that'll
+ -- have methods that may incidentally mention entirely unconstrained variables
+ -- e.g. a call to f :: Eq a => a -> b -> b
+ -- Here, b is unconstrained. A good example would be
+ -- foo = f (3::Int)
+ -- We want to infer the polymorphic type
+ -- foo :: forall b. b -> b
let
- cant_generalise = filter (not . instCanBeGeneralised) irreds
+ wanteds = lieToList wanted_lie
+ try_me inst = 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.
in
- checkTc (null cant_generalise)
- (genCantGenErr cant_generalise) `thenTc_`
-
- -- Check for ambiguous insts.
- -- You might think these can't happen (I did) because an ambiguous
- -- inst like (Eq a) will get tossed out with "frees", and eventually
- -- dealt with by tcSimplifyTop.
- -- But we can get stuck with
- -- C a b
- -- where "a" is one of the local_tvs, but "b" is unconstrained.
- -- Then we must yell about the ambiguous b
- -- But we must only do so if "b" really is unconstrained; so
- -- we must grab the global tyvars to answer that question
- tcGetGlobalTyVars `thenNF_Tc` \ global_tvs ->
+ simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
+
+ -- Next, figure out the tyvars we will quantify over
+ zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
+ tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
let
- avail_tvs = local_tvs `unionVarSet` global_tvs
- (irreds', bad_guys) = partition (isEmptyVarSet . ambig_tv_fn) irreds
- ambig_tv_fn dict = tyVarsOfInst dict `minusVarSet` avail_tvs
+ constrained_tvs = tyVarsOfInsts constrained_dicts
+ qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
+ `minusVarSet` constrained_tvs
in
- addAmbigErrs ambig_tv_fn bad_guys `thenNF_Tc_`
+ -- The first step may have squashed more methods than
+ -- necessary, so try again, this time 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 isFreeAndInheritable) in which we quantify over
+ -- all *non-inheritable* constraints too. This implements choice
+ -- (B) under "implicit parameter and monomorphism" above.
+ mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
+ let
+ try_me inst | isFree qtvs inst = Free
+ | otherwise = ReduceMe
+ in
+ reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ ASSERT( no_improvement )
+ ASSERT( null irreds )
+ -- No need to loop because simpleReduceLoop will have
+ -- already done any improvement necessary
- -- Finished
- returnTc (mkLIE frees, binds, mkLIE irreds')
- where
- wanteds = bagToList wanted_lie
-
- try_me inst
- -- Does not constrain a local tyvar
- | isEmptyVarSet (tyVarsOfInst inst `intersectVarSet` local_tvs)
- = -- if is_top_level then
- -- FreeIfTautological -- Special case for inference on
- -- -- top-level defns
- -- else
- Free
-
- -- We're infering (not checking) the type, and
- -- the inst constrains a local type variable
- | isDict inst = DontReduce -- Dicts
- | otherwise = ReduceMe AddToIrreds -- Lits and Methods
+ returnTc (varSetElems qtvs, mkLIE frees, binds)
\end{code}
-@tcSimplifyAndCheck@ is similar to the above, except that it checks
-that there is an empty wanted-set at the end. It may still return
-some of constant insts, which have to be resolved finally at the end.
+
+%************************************************************************
+%* *
+\subsection{tcSimplifyToDicts}
+%* *
+%************************************************************************
+
+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.
+
+The same thing is used for specialise pragmas. Consider
+
+ f :: Num a => a -> a
+ {-# SPECIALISE f :: Int -> Int #-}
+ f = ...
+
+The type checker generates a binding like:
+
+ f_spec = (f :: Int -> Int)
+
+and we want to end up with
+
+ f_spec = _inline_me_ (f Int dNumInt)
+
+But that means that we must simplify the Method for f to (f Int dNumInt)!
+So tcSimplifyToDicts squeezes out all Methods.
+
+IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
+
+ fromIntegral :: (Integral a, Num b) => a -> b
+ {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
+
+Here, 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 matching. Instead we want
+
+ forall dIntegralInt, dNumInt.
+ fromIntegral Int Int dIntegralInt dNumInt = id Int
+
+Hence "DontReduce NoSCs"
\begin{code}
-tcSimplifyAndCheck
- :: SDoc
- -> TcTyVarSet s -- ``Local'' type variables
- -- ASSERT: this tyvar set is already zonked
- -> LIE s -- Given; constrain only local tyvars
- -> LIE s -- Wanted
- -> TcM s (LIE s, -- Free
- TcDictBinds s) -- Bindings
-
-tcSimplifyAndCheck str local_tvs given_lie wanted_lie
- | isEmptyVarSet local_tvs
- -- This can happen quite legitimately; for example in
- -- instance Num Int where ...
- = returnTc (wanted_lie, EmptyMonoBinds)
+tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
+tcSimplifyToDicts wanted_lie
+ = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ -- Since try_me doesn't look at types, we don't need to
+ -- do any zonking, so it's safe to call reduceContext directly
+ ASSERT( null frees )
+ returnTc (irreds, binds)
- | otherwise
- = reduceContext str try_me givens wanteds `thenTc` \ (binds, frees, irreds) ->
+ where
+ doc = text "tcSimplifyToDicts"
+ wanteds = lieToList wanted_lie
- -- Complain about any irreducible ones
- mapNF_Tc complain irreds `thenNF_Tc_`
+ -- Reduce methods and lits only; stop as soon as we get a dictionary
+ try_me inst | isDict inst = DontReduce NoSCs
+ | otherwise = ReduceMe
+\end{code}
- -- Done
+
+%************************************************************************
+%* *
+\subsection{Filtering at a dynamic binding}
+%* *
+%************************************************************************
+
+When we have
+ let ?x = R in B
+
+we must discharge all the ?x constraints from B. We also do an improvement
+step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
+
+Actually, the constraints from B might improve the types in ?x. For example
+
+ f :: (?x::Int) => Char -> Char
+ let ?x = 3 in f 'c'
+
+then the constraint (?x::Int) arising from the call to f will
+force the binding for ?x to be of type Int.
+
+\begin{code}
+tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
+ -> LIE
+ -> TcM (LIE, TcDictBinds)
+tcSimplifyIPs given_ips wanted_lie
+ = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
returnTc (mkLIE frees, binds)
where
- givens = bagToList given_lie
- wanteds = bagToList wanted_lie
+ doc = text "tcSimplifyIPs" <+> ppr ip_names
+ wanteds = lieToList wanted_lie
+ ip_names = map instName given_ips
+ ip_set = mkNameSet ip_names
+
+ -- Simplify any methods that mention the implicit parameter
+ try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
+ | otherwise = Free
+
+ simpl_loop givens wanteds
+ = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
+ mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+
+ reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+
+ if no_improvement then
+ ASSERT( null irreds )
+ returnTc (frees, binds)
+ else
+ simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
+ returnTc (frees1, binds `AndMonoBinds` 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 :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
- try_me inst
- -- Does not constrain a local tyvar
- | isEmptyVarSet (tyVarsOfInst inst `intersectVarSet` local_tvs)
- = Free
+bindInstsOfLocalFuns init_lie local_ids
+ | null overloaded_ids
+ -- Common case
+ = returnTc (init_lie, EmptyMonoBinds)
- -- When checking against a given signature we always reduce
- -- until we find a match against something given, or can't reduce
- | otherwise
- = ReduceMe AddToIrreds
+ | otherwise
+ = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
+ ASSERT( null irreds )
+ returnTc (mkLIE frees, binds)
+ where
+ doc = text "bindInsts" <+> ppr local_ids
+ wanteds = lieToList init_lie
+ overloaded_ids = filter is_overloaded local_ids
+ is_overloaded id = isOverloadedTy (idType id)
- complain dict = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens ->
- addNoInstanceErr str givens dict
+ 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 | isMethodFor overloaded_set inst = ReduceMe
+ | otherwise = Free
\end{code}
The main control over context reduction is here
\begin{code}
-data WhatToDo
- = ReduceMe -- Try to reduce this
- NoInstanceAction -- What to do if there's no such instance
+data WhatToDo
+ = ReduceMe -- 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)!
+
+ | DontReduce WantSCs -- Return as irreducible
- | DontReduce -- Return as irreducible
+ | DontReduceUnlessConstant -- Return as irreducible unless it can
+ -- be reduced to a constant in one step
| Free -- Return as free
- | FreeIfTautological -- Return as free iff it's tautological;
- -- if not, return as irreducible
+data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
+ -- of a predicate when adding it to the avails
+\end{code}
-data NoInstanceAction
- = Stop -- Fail; no error message
- -- (Only used when tautology checking.)
- | AddToIrreds -- Just add the inst to the irreductible ones; don't
- -- produce an error message of any kind.
- -- It might be quite legitimate such as (Eq a)!
+
+\begin{code}
+type RedState = (Avails, -- What's available
+ [Inst]) -- Insts for which try_me returned Free
+
+type Avails = FiniteMap Inst Avail
+
+data Avail
+ = Irred -- Used for irreducible dictionaries,
+ -- which are going to be lambda bound
+
+ | BoundTo TcId -- Used for dictionaries for which we have a binding
+ -- e.g. those "given" in a signature
+
+ | NoRhs -- Used for Insts like (CCallable f)
+ -- where no witness is required.
+
+ | Rhs -- Used when there is a RHS
+ TcExpr -- The RHS
+ [Inst] -- Insts free in the RHS; we need these too
+
+pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
+ | (inst,avail) <- fmToList avails ]
+
+instance Outputable Avail where
+ ppr = pprAvail
+
+pprAvail NoRhs = text "<no rhs>"
+pprAvail Irred = text "Irred"
+pprAvail (BoundTo x) = text "Bound to" <+> ppr x
+pprAvail (Rhs rhs bs) = 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}
+bindsAndIrreds :: Avails
+ -> [Inst] -- Wanted
+ -> (TcDictBinds, -- Bindings
+ [Inst]) -- Irreducible ones
+
+bindsAndIrreds avails wanteds
+ = go avails EmptyMonoBinds [] wanteds
+ where
+ go avails binds irreds [] = (binds, irreds)
+
+ go avails binds irreds (w:ws)
+ = case lookupFM avails w of
+ Nothing -> -- Free guys come out here
+ -- (If we didn't do addFree we could use this as the
+ -- criterion for free-ness, and pick up the free ones here too)
+ go avails binds irreds ws
+
+ Just NoRhs -> go avails binds irreds ws
+ Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
-\begin{code}
-type RedState s
- = (Avails s, -- What's available
- [Inst s], -- Insts for which try_me returned Free
- [Inst s] -- Insts for which try_me returned DontReduce
- )
-
-type Avails s = FiniteMap (Inst s) (Avail s)
-
-data Avail s
- = Avail
- (TcIdOcc s) -- The "main Id"; that is, the Id for the Inst that
- -- caused this avail to be put into the finite map in the first place
- -- It is this Id that is bound to the RHS.
-
- (RHS s) -- The RHS: an expression whose value is that Inst.
- -- The main Id should be bound to this RHS
-
- [TcIdOcc s] -- Extra Ids that must all be bound to the main Id.
- -- At the end we generate a list of bindings
- -- { i1 = main_id; i2 = main_id; i3 = main_id; ... }
-
-data RHS s
- = NoRhs -- Used for irreducible dictionaries,
- -- which are going to be lambda bound, or for those that are
- -- suppplied as "given" when checking againgst a signature.
- --
- -- NoRhs is also used for Insts like (CCallable f)
- -- where no witness is required.
+ Just (BoundTo id) -> go avails new_binds irreds ws
+ where
+ -- For implicit parameters, all occurrences share the same
+ -- Id, so there is no need for synonym bindings
+ new_binds | new_id == id = binds
+ | otherwise = addBind binds new_id (HsVar id)
+ new_id = instToId w
- | Rhs -- Used when there is a RHS
- (TcExpr s)
- Bool -- True => the RHS simply selects a superclass dictionary
- -- from a subclass dictionary.
- -- False => not so.
- -- This is useful info, because superclass selection
- -- is cheaper than building the dictionary using its dfun,
- -- and we can sometimes replace the latter with the former
-
- | PassiveScSel -- Used for as-yet-unactivated RHSs. For example suppose we have
- -- an (Ord t) dictionary; then we put an (Eq t) entry in
- -- the finite map, with an PassiveScSel. Then if the
- -- the (Eq t) binding is ever *needed* we make it an Rhs
- (TcExpr s)
- [Inst s] -- List of Insts that are free in the RHS.
- -- If the main Id is subsequently needed, we toss this list into
- -- the needed-inst pool so that we make sure their bindings
- -- will actually be produced.
- --
- -- Invariant: these Insts are already in the finite mapping
-
-
-pprAvails avails = vcat (map pp (eltsFM avails))
- where
- pp (Avail main_id rhs ids)
- = ppr main_id <> colon <+> brackets (ppr ids) <+> pprRhs rhs
+ Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
+ where
+ id = instToId w
+ avails' = addToFM avails w (BoundTo id)
-pprRhs NoRhs = text "<no rhs>"
-pprRhs (Rhs rhs b) = ppr rhs
-pprRhs (PassiveScSel rhs is) = text "passive" <+> ppr rhs
+addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
\end{code}
%* *
%************************************************************************
-The main entry point for context reduction is @reduceContext@:
+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
+ = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
+ reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
+ if no_improvement then
+ returnTc (frees, binds, irreds)
+ else
+ simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
+ returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
+\end{code}
+
+
\begin{code}
-reduceContext :: SDoc -> (Inst s -> WhatToDo)
- -> [Inst s] -- Given
- -> [Inst s] -- Wanted
- -> TcM s (TcDictBinds s,
- [Inst s], -- Free
- [Inst s]) -- Irreducible
-
-reduceContext str try_me givens wanteds
- = -- Zonking first
- mapNF_Tc zonkInst givens `thenNF_Tc` \ givens ->
- mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds ->
-
-{-
- pprTrace "reduceContext" (vcat [
+reduceContext :: SDoc
+ -> (Inst -> WhatToDo)
+ -> [Inst] -- Given
+ -> [Inst] -- Wanted
+ -> NF_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 "----------------------",
- str,
+ doc,
text "given" <+> ppr givens,
text "wanted" <+> ppr wanteds,
text "----------------------"
- ]) $
--}
+ ])) `thenNF_Tc_`
+
-- Build the Avail mapping from "givens"
- foldlNF_Tc addGiven emptyFM givens `thenNF_Tc` \ avails ->
+ foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
-- Do the real work
- reduceList (0,[]) try_me wanteds (avails, [], []) `thenTc` \ (avails, frees, irreds) ->
+ reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
- -- Extract the bindings from avails
- let
- binds = foldFM add_bind EmptyMonoBinds avails
-
- add_bind _ (Avail main_id rhs ids) binds
- = foldr add_synonym (add_rhs_bind rhs binds) ids
- where
- add_rhs_bind (Rhs rhs _) binds = binds `AndMonoBinds` VarMonoBind main_id rhs
- add_rhs_bind other binds = binds
-
- -- Add the trivial {x = y} bindings
- -- The main Id can end up in the list when it's first added passively
- -- and then activated, so we have to filter it out. A bit of a hack.
- add_synonym id binds
- | id /= main_id = binds `AndMonoBinds` VarMonoBind id (HsVar main_id)
- | otherwise = binds
- in
-{-
- pprTrace ("reduceContext end") (vcat [
+ -- Do improvement, using everything in avails
+ -- In particular, avails includes all superclasses of everything
+ tcImprove avails `thenTc` \ no_improvement ->
+
+ traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
- str,
+ doc,
text "given" <+> ppr givens,
text "wanted" <+> ppr wanteds,
- text "----",
+ text "----",
text "avails" <+> pprAvails avails,
- text "irreds" <+> ppr irreds,
+ text "frees" <+> ppr frees,
+ text "no_improvement =" <+> ppr no_improvement,
text "----------------------"
- ]) $
--}
- returnTc (binds, frees, irreds)
+ ])) `thenNF_Tc_`
+ let
+ (binds, irreds) = bindsAndIrreds avails wanteds
+ in
+ returnTc (no_improvement, frees, binds, irreds)
+
+tcImprove avails
+ = tcGetInstEnv `thenTc` \ inst_env ->
+ let
+ preds = [ (pred, pp_loc)
+ | inst <- keysFM avails,
+ let pp_loc = pprInstLoc (instLoc inst),
+ pred <- predsOfInst inst,
+ predHasFDs pred
+ ]
+ -- 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
+ eqns = improve (classInstEnv inst_env) preds
+ in
+ if null eqns then
+ returnTc True
+ else
+ traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns)) `thenNF_Tc_`
+ mapTc_ unify eqns `thenTc_`
+ returnTc False
+ where
+ unify ((qtvs, t1, t2), doc)
+ = tcAddErrCtxt doc $
+ tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
+ unifyTauTy (substTy tenv t1) (substTy tenv t2)
+ ppr_eqn ((qtvs, t1, t2), doc)
+ = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
+ <+> ppr t1 <+> ptext SLIT(":=:") <+> ppr t2,
+ nest 2 doc]
\end{code}
The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
-reduceList :: (Int,[Inst s])
- -> (Inst s -> WhatToDo)
- -> [Inst s]
- -> RedState s
- -> TcM s (RedState s)
+reduceList :: (Int,[Inst]) -- Stack (for err msgs)
+ -- along with its depth
+ -> (Inst -> WhatToDo)
+ -> [Inst]
+ -> RedState
+ -> TcM RedState
\end{code}
@reduce@ is passed
Free return this in "frees"
wanteds: The list of insts to reduce
- state: An accumulating parameter of type RedState
+ state: An accumulating parameter of type RedState
that contains the state of the algorithm
-
+
It returns a RedState.
+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
| otherwise
=
#ifdef DEBUG
- (if n > 4 then
+ (if n > 8 then
pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
else (\x->x))
#endif
go ws state'
-- Base case: we're done!
-reduce stack try_me wanted state@(avails, frees, irreds)
-
+reduce stack try_me wanted state
-- It's the same as an existing inst, or a superclass thereof
- | wanted `elemFM` avails
- = returnTc (activate avails wanted, frees, irreds)
-
- -- It should be reduced
- | case try_me_result of { ReduceMe _ -> True; _ -> False }
- = lookupInst wanted `thenNF_Tc` \ lookup_result ->
-
- case lookup_result of
- GenInst wanteds' rhs -> use_instance wanteds' rhs
- SimpleInst rhs -> use_instance [] rhs
-
- NoInstance -> -- No such instance!
- -- Decide what to do based on the no_instance_action requested
- case no_instance_action of
- Stop -> failTc -- Fail
- AddToIrreds -> add_to_irreds -- Add the offending insts to the irreds
-
- -- It's free and this isn't a top-level binding, so just chuck it upstairs
- | case try_me_result of { Free -> True; _ -> False }
- = -- First, see if the inst can be reduced to a constant in one step
- lookupInst wanted `thenNF_Tc` \ lookup_result ->
- case lookup_result of
- SimpleInst rhs -> use_instance [] rhs
- other -> add_to_frees
-
- -- It's free and this is a top level binding, so
- -- check whether it's a tautology or not
- | case try_me_result of { FreeIfTautological -> True; _ -> False }
- = -- Try for tautology
- tryTc
- -- If tautology trial fails, add to irreds
- (addGiven avails wanted `thenNF_Tc` \ avails' ->
- returnTc (avails', frees, wanted:irreds))
-
- -- If tautology succeeds, just add to frees
- (reduce stack try_me_taut wanted (avails, [], []) `thenTc_`
- returnTc (avails, wanted:frees, irreds))
-
-
- -- It's irreducible (or at least should not be reduced)
- | otherwise
- = ASSERT( case try_me_result of { DontReduce -> True; other -> False } )
- -- See if the inst can be reduced to a constant in one step
- lookupInst wanted `thenNF_Tc` \ lookup_result ->
- case lookup_result of
- SimpleInst rhs -> use_instance [] rhs
- other -> add_to_irreds
-
- where
- -- The three main actions
- add_to_frees = let
- avails' = addFree avails wanted
- -- Add the thing to the avails set so any identical Insts
- -- will be commoned up with it right here
- in
- returnTc (avails', wanted:frees, irreds)
-
- add_to_irreds = addGiven avails wanted `thenNF_Tc` \ avails' ->
- returnTc (avails', frees, wanted:irreds)
-
- use_instance wanteds' rhs = addWanted avails wanted rhs `thenNF_Tc` \ avails' ->
- reduceList stack try_me wanteds' (avails', frees, irreds)
-
- try_me_result = try_me wanted
- ReduceMe no_instance_action = try_me_result
-
- -- The try-me to use when trying to identify tautologies
- -- It blunders on reducing as much as possible
- try_me_taut inst = ReduceMe Stop -- No error recovery
-\end{code}
-
-
-\begin{code}
-activate :: Avails s -> Inst s -> Avails s
- -- Activate the binding for Inst, ensuring that a binding for the
- -- wanted Inst will be generated.
- -- (Activate its parent if necessary, recursively).
- -- Precondition: the Inst is in Avails already
-
-activate avails wanted
- | not (instBindingRequired wanted)
- = avails
+ | isAvailable state wanted
+ = returnTc state
| otherwise
- = case lookupFM avails wanted of
-
- Just (Avail main_id (PassiveScSel rhs insts) ids) ->
- foldl activate avails' insts -- Activate anything it needs
- where
- avails' = addToFM avails wanted avail'
- avail' = Avail main_id (Rhs rhs True) (wanted_id : ids) -- Activate it
-
- Just (Avail main_id other_rhs ids) -> -- Just add to the synonyms list
- addToFM avails wanted (Avail main_id other_rhs (wanted_id : ids))
-
- Nothing -> panic "activate"
- where
- wanted_id = instToId wanted
-
-addWanted avails wanted rhs_expr
- = ASSERT( not (wanted `elemFM` avails) )
- returnNF_Tc (addToFM avails wanted avail)
- -- NB: we don't add the thing's superclasses too!
- -- Why not? Because addWanted is used when we've successfully used an
- -- instance decl to reduce something; e.g.
- -- d:Ord [a] = dfunOrd (d1:Eq [a]) (d2:Ord a)
- -- Note that we pass the superclasses to the dfun, so they will be "wanted".
- -- If we put the superclasses of "d" in avails, then we might end up
- -- expressing "d1" in terms of "d", which would be a disaster.
- where
- avail = Avail (instToId wanted) rhs []
+ = case try_me wanted of {
- rhs | instBindingRequired wanted = Rhs rhs_expr False -- Not superclass selection
- | otherwise = NoRhs
+ DontReduce want_scs -> addIrred want_scs state wanted
-addFree :: Avails s -> Inst s -> (Avails s)
- -- 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.
-addFree avails free
- | isDict free = addToFM avails free (Avail (instToId free) NoRhs [])
- | otherwise = avails
-
-addGiven :: Avails s -> Inst s -> NF_TcM s (Avails s)
-addGiven avails given
- = -- ASSERT( not (given `elemFM` avails) )
- -- This assertion isn't necessarily true. It's permitted
- -- to given a redundant context in a type signature (eg (Ord a, Eq a) => ...)
- -- and when typechecking instance decls we generate redundant "givens" too.
- addAvail avails given avail
- where
- avail = Avail (instToId given) NoRhs []
+ ; 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
-addAvail avails wanted avail
- = addSuperClasses (addToFM avails wanted avail) wanted
+ ; 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
-addSuperClasses :: Avails s -> Inst s -> NF_TcM s (Avails s)
- -- Add all the superclasses of the Inst to Avails
- -- Invariant: the Inst is already in Avails.
+ ; ReduceMe -> -- It should be reduced
+ lookupInst wanted `thenNF_Tc` \ lookup_result ->
+ case lookup_result of
+ GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
+ addWanted state' wanted rhs wanteds'
+ SimpleInst rhs -> addWanted state wanted rhs []
-addSuperClasses avails dict
- | not (isDict dict)
- = returnNF_Tc avails
+ NoInstance -> -- No such instance!
+ -- Add it and its superclasses
+ addIrred AddSCs state wanted
- | otherwise -- It is a dictionary
- = foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_theta' sc_sels)
+ }
where
- (clas, tys) = getDictClassTys dict
-
- (tyvars, sc_theta, sc_sels, _, _) = classBigSig clas
- sc_theta' = substFlexiTheta (zipVarEnv tyvars tys) sc_theta
-
- add_sc avails ((super_clas, super_tys), sc_sel)
- = newDictFromOld dict super_clas super_tys `thenNF_Tc` \ super_dict ->
- let
- sc_sel_rhs = DictApp (TyApp (HsVar (RealId sc_sel))
- tys)
- [instToId dict]
- in
- case lookupFM avails super_dict of
-
- Just (Avail main_id (Rhs rhs False {- not sc selection -}) ids) ->
- -- Already there, but not as a superclass selector
- -- No need to look at its superclasses; since it's there
- -- already they must be already in avails
- -- However, we must remember to activate the dictionary
- -- from which it is (now) generated
- returnNF_Tc (activate avails' dict)
- where
- avails' = addToFM avails super_dict avail
- avail = Avail main_id (Rhs sc_sel_rhs True) ids -- Superclass selection
-
- Just (Avail _ _ _) -> returnNF_Tc avails
- -- Already there; no need to do anything
-
- Nothing ->
- -- Not there at all, so add it, and its superclasses
- addAvail avails super_dict avail
- where
- avail = Avail (instToId super_dict)
- (PassiveScSel sc_sel_rhs [dict])
- []
-\end{code}
-
-%************************************************************************
-%* *
-\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.
-
-\begin{code}
-tcSimplifyThetas :: (Class -> ClassInstEnv) -- How to find the ClassInstEnv
- -> ThetaType -- Wanted
- -> TcM s ThetaType -- Needed; of the form C a b c
- -- where a,b,c are type variables
-
-tcSimplifyThetas inst_mapper wanteds
- = reduceSimple inst_mapper [] wanteds `thenNF_Tc` \ irreds ->
- let
- -- Check that the returned dictionaries are of the form (C a b c)
- bad_guys | opt_GlasgowExts = [ct | ct@(clas,tys) <- irreds,
- isEmptyVarSet (tyVarsOfTypes tys)]
- | otherwise = [ct | ct@(clas,tys) <- irreds,
- not (all isTyVarTy tys)]
-
- in
- if null bad_guys then
- returnTc irreds
- else
- mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
- failTc
-\end{code}
-
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
-used with \tr{default} declarations. We are only interested in
-whether it worked or not.
-
-\begin{code}
-tcSimplifyCheckThetas :: ThetaType -- Given
- -> ThetaType -- Wanted
- -> TcM s ()
-
-tcSimplifyCheckThetas givens wanteds
- = reduceSimple classInstEnv givens wanteds `thenNF_Tc` \ irreds ->
- if null irreds then
- returnTc ()
- else
- mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
- failTc
+ try_simple do_this_otherwise
+ = lookupInst wanted `thenNF_Tc` \ lookup_result ->
+ case lookup_result of
+ SimpleInst rhs -> addWanted state wanted rhs []
+ other -> do_this_otherwise state wanted
\end{code}
\begin{code}
-type AvailsSimple = FiniteMap (Class, [TauType]) Bool
- -- True => irreducible
- -- False => given, or can be derived from a given or from an irreducible
-
-reduceSimple :: (Class -> ClassInstEnv)
- -> ThetaType -- Given
- -> ThetaType -- Wanted
- -> NF_TcM s ThetaType -- Irreducible
-
-reduceSimple inst_mapper givens wanteds
- = reduce_simple (0,[]) inst_mapper givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
- returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
+isAvailable :: RedState -> Inst -> Bool
+isAvailable (avails, _) wanted = wanted `elemFM` avails
+ -- NB: the Ord instance of Inst compares by the class/type info
+ -- *not* by unique. So
+ -- d1::C Int == d2::C Int
+
+-------------------------
+addFree :: RedState -> Inst -> NF_TcM RedState
+ -- 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!
+ --
+ -- NB1: 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.
+ --
+ -- NB2: do *not* add the Inst to avails at all 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!
+ -- Solution: never put methods in avail till they are captured
+ -- in which case addFree isn't used
+ --
+ -- NB3: make sure that CCallable/CReturnable use NoRhs rather
+ -- than BoundTo, else we end up with bogus bindings.
+ -- c.f. instBindingRequired in addWanted
+addFree (avails, frees) free
+ | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
+ | otherwise = returnNF_Tc (avails, free:frees)
where
- givens_fm = foldl addNonIrred emptyFM givens
-
-reduce_simple :: (Int,ThetaType) -- Stack
- -> (Class -> ClassInstEnv)
- -> AvailsSimple
- -> ThetaType
- -> NF_TcM s AvailsSimple
-
-reduce_simple (n,stack) inst_mapper avails wanteds
- = go avails wanteds
+ avail | instBindingRequired free = BoundTo (instToId free)
+ | otherwise = NoRhs
+
+addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
+addWanted state@(avails, frees) wanted rhs_expr wanteds
+-- Do *not* add superclasses as well. Here's an example of why not
+-- class Eq a => 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!
+-- ToDo: this isn't entirely unsatisfactory, because
+-- we may also lose some entirely-legitimate sharing this way
+
+ = ASSERT( not (isAvailable state wanted) )
+ returnNF_Tc (addToFM avails wanted avail, frees)
where
- go avails [] = returnNF_Tc avails
- go avails (w:ws) = reduce_simple_help (n+1,w:stack) inst_mapper avails w `thenNF_Tc` \ avails' ->
- go avails' ws
-
-reduce_simple_help stack inst_mapper givens wanted@(clas,tys)
- | wanted `elemFM` givens
- = returnNF_Tc givens
+ avail | instBindingRequired wanted = Rhs rhs_expr wanteds
+ | otherwise = ASSERT( null wanteds ) NoRhs
- | otherwise
- = lookupSimpleInst (inst_mapper clas) clas tys `thenNF_Tc` \ maybe_theta ->
-
- case maybe_theta of
- Nothing -> returnNF_Tc (addIrred givens wanted)
- Just theta -> reduce_simple stack inst_mapper (addNonIrred givens wanted) theta
+addGiven :: RedState -> Inst -> NF_TcM RedState
+addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
-addIrred :: AvailsSimple -> (Class, [TauType]) -> AvailsSimple
-addIrred givens ct
- = addSCs (addToFM givens ct True) ct
+addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
+addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
+addIrred AddSCs state irred = addAvailAndSCs state irred Irred
-addNonIrred :: AvailsSimple -> (Class, [TauType]) -> AvailsSimple
-addNonIrred givens ct
- = addSCs (addToFM givens ct False) ct
+addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
+addAvailAndSCs (avails, frees) wanted avail
+ = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
+ returnNF_Tc (avails', frees)
-addSCs givens ct@(clas,tys)
- = foldl add givens sc_theta
- where
- (tyvars, sc_theta_tmpl, _, _, _) = classBigSig clas
- sc_theta = substFlexiTheta (zipVarEnv tyvars tys) sc_theta_tmpl
+---------------------
+add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
+add_avail_and_scs avails wanted avail
+ = add_scs (addToFM avails wanted avail) wanted
- add givens ct = case lookupFM givens ct of
- Nothing -> -- Add it and its superclasses
- addSCs (addToFM givens ct False) ct
+add_scs :: Avails -> Inst -> NF_TcM Avails
+ -- Add all the superclasses of the Inst to Avails
+ -- Invariant: the Inst is already in Avails.
- Just True -> -- Set its flag to False; superclasses already done
- addToFM givens ct False
+add_scs avails dict
+ | not (isClassDict dict)
+ = returnNF_Tc avails
- Just False -> -- Already done
- givens
-
+ | otherwise -- It is a dictionary
+ = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
+ foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
+ where
+ (clas, tys) = getDictClassTys dict
+ (tyvars, sc_theta, sc_sels, _) = classBigSig clas
+ sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
+
+ add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
+ = case lookupFM avails sc_dict of
+ Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
+ other -> add_avail_and_scs avails sc_dict avail
+ where
+ sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
+ avail = Rhs sc_sel_rhs [dict]
\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 :: LIE s -> [TcIdBndr s] -> TcM s (LIE s, TcMonoBinds s)
-
-bindInstsOfLocalFuns init_lie local_ids
- | null overloaded_ids || null lie_for_here
- -- Common case
- = returnTc (init_lie, EmptyMonoBinds)
-
- | otherwise
- = reduceContext (text "bindInsts" <+> ppr local_ids)
- try_me [] lie_for_here `thenTc` \ (binds, frees, irreds) ->
- ASSERT( null irreds )
- returnTc (mkLIE frees `plusLIE` mkLIE lie_not_for_here, binds)
- where
- overloaded_ids = filter is_overloaded local_ids
- is_overloaded id = case splitSigmaTy (idType id) of
- (_, theta, _) -> not (null theta)
+Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
+and want to deduce (d2:C [a]) where
- 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
+ class Ord a => C a where
+ instance Ord a => C [a] where ...
- -- No sense in repeatedly zonking lots of
- -- constant constraints so filter them out here
- (lie_for_here, lie_not_for_here) = partition (isMethodFor overloaded_set)
- (bagToList init_lie)
- try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
- | otherwise = Free
-\end{code}
+Then we'll use the instance decl to deduce C [a] and then add the
+superclasses of C [a] to avails. But we must not overwrite the binding
+for d1:Ord a (which is given) with a superclass selection or we'll just
+build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
+than a selection.
%************************************************************************
%* *
-\section[Disambig]{Disambiguation of overloading}
+\section{tcSimplifyTop: defaulting}
%* *
%************************************************************************
If a dictionary constrains a type variable which is
-\begin{itemize}
-\item
-not mentioned in the environment
-\item
-and not mentioned in the type of the expression
-\end{itemize}
+ * 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
-\begin{itemize}
-\item
-at least one of its classes is a numeric class, and
-\item
-all of its classes are numeric or standard
-\end{itemize}
+ * 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.
complains. It works by splitting the dictionary list by type
variable, and using @disambigOne@ to do the real business.
+@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.
-@tcSimplifyTop@ is called once per module to simplify
-all the constant and ambiguous Insts.
\begin{code}
-tcSimplifyTop :: LIE s -> TcM s (TcDictBinds s)
+tcSimplifyTop :: LIE -> TcM TcDictBinds
tcSimplifyTop wanted_lie
- = reduceContext (text "tcSimplTop") try_me [] wanteds `thenTc` \ (binds1, frees, irreds) ->
+ = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
ASSERT( null frees )
let
-- All the non-std ones are definite errors
(stds, non_stds) = partition isStdClassTyVarDict irreds
-
-- Group by type variable
std_groups = equivClasses cmp_by_tyvar stds
-- Pick the ones which its worth trying to disambiguate
(std_oks, std_bads) = partition worth_a_try std_groups
- -- Have a try at disambiguation
+
+ -- Have a try at disambiguation
-- if the type variable isn't bound
-- up with one of the non-standard classes
- worth_a_try group@(d:_) = isEmptyVarSet (tyVarsOfInst d `intersectVarSet` non_std_tyvars)
+ worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
-- Collect together all the bad guys
bad_guys = non_stds ++ concat std_bads
in
-
-- Disambiguate the ones that look feasible
mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
-- And complain about the ones that don't
- mapNF_Tc complain bad_guys `thenNF_Tc_`
+ -- This group includes both non-existent instances
+ -- e.g. Num (IO a) and Eq (Int -> Int)
+ -- and ambiguous dictionaries
+ -- e.g. Num a
+ addTopAmbigErrs bad_guys `thenNF_Tc_`
- returnTc (binds1 `andMonoBinds` andMonoBindList binds_ambig)
+ returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
where
- wanteds = bagToList wanted_lie
- try_me inst = ReduceMe AddToIrreds
+ wanteds = lieToList wanted_lie
+ try_me inst = ReduceMe
d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
- complain d | isEmptyVarSet (tyVarsOfInst d) = addTopInstanceErr d
- | otherwise = addAmbigErr tyVarsOfInst d
-
get_tv d = case getDictClassTys d of
- (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
+ (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
get_clas d = case getDictClassTys d of
(clas, [ty]) -> clas
\end{code}
@void@.
\begin{code}
-disambigGroup :: [Inst s] -- All standard classes of form (C a)
- -> TcM s (TcDictBinds s)
+disambigGroup :: [Inst] -- All standard classes of form (C a)
+ -> TcM TcDictBinds
disambigGroup dicts
- | any isNumericClass classes -- Guaranteed all standard classes
+ | any isNumericClass classes -- Guaranteed all standard classes
+ -- see comment at the end of function for reasons as to
+ -- why the defaulting mechanism doesn't apply to groups that
+ -- include CCallable or CReturnable dicts.
+ && not (any isCcallishClass classes)
= -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
-- SO, TRY DEFAULT TYPES IN ORDER
= failTc
try_default (default_ty : default_tys)
- = tryTc (try_default default_tys) $ -- If default_ty fails, we try
+ = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
-- default_tys instead
- tcSimplifyCheckThetas [] thetas `thenTc` \ _ ->
+ tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
returnTc default_ty
where
- thetas = classes `zip` repeat [default_ty]
+ theta = [mkClassPred clas [default_ty] | clas <- classes]
in
-- See if any default works, and if so bind the type variable to it
-- If not, add an AmbigErr
- recoverTc (complain dicts `thenNF_Tc_` returnTc EmptyMonoBinds) $
+ recoverTc (addAmbigErrs dicts `thenNF_Tc_`
+ returnTc EmptyMonoBinds) $
try_default default_tys `thenTc` \ chosen_default_ty ->
-- Bind the type variable and reduce the context, for real this time
- let
- chosen_default_tc_ty = typeToTcType chosen_default_ty -- Tiresome!
- in
- unifyTauTy chosen_default_tc_ty (mkTyVarTy tyvar) `thenTc_`
- reduceContext (text "disambig" <+> ppr dicts)
- try_me [] dicts `thenTc` \ (binds, frees, ambigs) ->
- ASSERT( null frees && null ambigs )
+ unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
+ simpleReduceLoop (text "disambig" <+> ppr dicts)
+ try_me dicts `thenTc` \ (frees, binds, ambigs) ->
+ WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
+ warnDefault dicts chosen_default_ty `thenTc_`
returnTc binds
| all isCreturnableClass classes
- = -- Default CCall stuff to (); we don't even both to check that () is an
+ = -- Default CCall stuff to (); we don't even both to check that () is an
-- instance of CReturnable, because we know it is.
unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
returnTc EmptyMonoBinds
-
+
| otherwise -- No defaults
- = complain dicts `thenNF_Tc_`
+ = addAmbigErrs dicts `thenNF_Tc_`
returnTc EmptyMonoBinds
where
- complain = addAmbigErrs tyVarsOfInst
- try_me inst = ReduceMe AddToIrreds -- This reduce should not fail
+ try_me inst = ReduceMe -- This reduce should not fail
tyvar = get_tv (head dicts) -- Should be non-empty
classes = map get_clas dicts
\end{code}
+[Aside - why the defaulting mechanism is turned off when
+ dealing with arguments and results to ccalls.
+
+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. This is
+implemented via the help of the pseudo-type classes,
+@CReturnable@ (CR) and @CCallable@ (CC.)
+
+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.
+
+To try to minimise the potential for surprises here, the
+defaulting mechanism is turned off in the presence of
+CCallable and CReturnable.
+
+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.
+
+\begin{code}
+tcSimplifyThetas :: ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
+
+tcSimplifyThetas wanteds
+ = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
+ reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
+ let
+ -- For multi-param Haskell, check that the returned dictionaries
+ -- don't have any of the form (C Int Bool) for which
+ -- we expect an instance here
+ -- For Haskell 98, check that all the constraints are of the form C a,
+ -- where a is a type variable
+ bad_guys | glaExts = [pred | pred <- irreds,
+ isEmptyVarSet (tyVarsOfPred pred)]
+ | otherwise = [pred | pred <- irreds,
+ not (isTyVarClassPred pred)]
+ in
+ if null bad_guys then
+ returnTc irreds
+ else
+ mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
+ failTc
+\end{code}
+
+@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+used with \tr{default} declarations. We are only interested in
+whether it worked or not.
+
+\begin{code}
+tcSimplifyCheckThetas :: ThetaType -- Given
+ -> ThetaType -- Wanted
+ -> TcM ()
+
+tcSimplifyCheckThetas givens wanteds
+ = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
+ if null irreds then
+ returnTc ()
+ else
+ mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
+ failTc
+\end{code}
+
+
+\begin{code}
+type AvailsSimple = FiniteMap PredType Bool
+ -- True => irreducible
+ -- False => given, or can be derived from a given or from an irreducible
+
+reduceSimple :: ThetaType -- Given
+ -> ThetaType -- Wanted
+ -> NF_TcM ThetaType -- Irreducible
+
+reduceSimple givens wanteds
+ = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
+ returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
+ where
+ givens_fm = foldl addNonIrred emptyFM givens
+
+reduce_simple :: (Int,ThetaType) -- Stack
+ -> AvailsSimple
+ -> ThetaType
+ -> NF_TcM AvailsSimple
+
+reduce_simple (n,stack) avails wanteds
+ = go avails wanteds
+ where
+ go avails [] = returnNF_Tc avails
+ go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
+ go avails' ws
+
+reduce_simple_help stack givens wanted
+ | wanted `elemFM` givens
+ = returnNF_Tc givens
+
+ | Just (clas, tys) <- getClassPredTys_maybe wanted
+ = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
+ case maybe_theta of
+ Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
+ Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
+
+ | otherwise
+ = returnNF_Tc (addSimpleIrred givens wanted)
+
+addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
+addSimpleIrred givens pred
+ = addSCs (addToFM givens pred True) pred
+
+addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
+addNonIrred givens pred
+ = addSCs (addToFM givens pred False) pred
+
+addSCs givens pred
+ | not (isClassPred pred) = givens
+ | otherwise = foldl add givens sc_theta
+ where
+ Just (clas,tys) = getClassPredTys_maybe pred
+ (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
+ sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
+
+ add givens ct
+ = case lookupFM givens ct of
+ Nothing -> -- Add it and its superclasses
+ addSCs (addToFM givens ct False) ct
+
+ Just True -> -- Set its flag to False; superclasses already done
+ addToFM givens ct False
+
+ Just False -> -- Already done
+ givens
+
+\end{code}
-Errors and contexts
-~~~~~~~~~~~~~~~~~~~
+%************************************************************************
+%* *
+\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}
-genCantGenErr insts -- Can't generalise these Insts
- = sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
- nest 4 (pprInstsInFull insts)
- ]
-
-addAmbigErrs ambig_tv_fn dicts = mapNF_Tc (addAmbigErr ambig_tv_fn) dicts
-
-addAmbigErr ambig_tv_fn dict
- = tcAddSrcLoc (instLoc dict) $
- addErrTcM (tidy_env,
- sep [text "Ambiguous type variable(s)" <+>
- hsep (punctuate comma (map (quotes . ppr) ambig_tvs)),
- nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict)),
- nest 4 (pprOrigin dict)])
+groupInsts :: [Inst] -> [[Inst]]
+-- Group together insts with the same origin
+-- We want to report them together in error messages
+groupInsts [] = []
+groupInsts (inst:insts) = (inst:friends) : groupInsts 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
+
+
+addTopAmbigErrs dicts
+ = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
+ mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
+ mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
+ returnNF_Tc ()
where
- ambig_tvs = varSetElems (ambig_tv_fn tidy_dict)
- (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
+ fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
+ (tidy_env, tidy_dicts) = tidyInsts dicts
+ (bad_ips, non_ips) = partition is_ip tidy_dicts
+ (no_insts, ambigs) = partition no_inst non_ips
+ is_ip d = any isIPPred (predsOfInst d)
+ no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
+
+plural [x] = empty
+plural xs = char 's'
+
+addTopIPErrs tidy_env tidy_dicts
+ = addInstErrTcM (instLoc (head tidy_dicts))
+ (tidy_env,
+ ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
-- Used for top-level irreducibles
-addTopInstanceErr dict
- = tcAddSrcLoc (instLoc dict) $
- addErrTcM (tidy_env,
- sep [ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict),
- nest 4 $ pprOrigin dict])
+addTopInstanceErrs tidy_env tidy_dicts
+ = addInstErrTcM (instLoc (head tidy_dicts))
+ (tidy_env,
+ ptext SLIT("No instance") <> plural tidy_dicts <+>
+ ptext SLIT("for") <+> pprInsts tidy_dicts)
+
+addAmbigErrs dicts
+ = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
+ where
+ (tidy_env, tidy_dicts) = tidyInsts dicts
+
+addAmbigErr tidy_env tidy_dict
+ = addInstErrTcM (instLoc tidy_dict)
+ (tidy_env,
+ sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
+ nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
+ where
+ ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
+
+warnDefault dicts default_ty
+ = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
+ tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
where
- (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
-
-addNoInstanceErr str givens dict
- = tcAddSrcLoc (instLoc dict) $
- addErrTcM (tidy_env,
- sep [sep [ptext SLIT("Could not deduce") <+> quotes (pprInst tidy_dict),
- nest 4 $ parens $ pprOrigin dict],
- nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens]
- $$
- ptext SLIT("Probable cause:") <+>
- vcat [ptext SLIT("missing") <+> quotes (pprInst tidy_dict) <+> ptext SLIT("in") <+> str,
- if all_tyvars then empty else
- ptext SLIT("or missing instance declaration for") <+> quotes (pprInst tidy_dict)]
- )
+ -- Tidy them first
+ (_, tidy_dicts) = tidyInsts dicts
+ get_loc i = case instLoc i of { (_,loc,_) -> loc }
+ warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
+ quotes (ppr default_ty),
+ pprInstsInFull tidy_dicts]
+
+complainCheck doc givens irreds
+ = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
+ mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
+ returnNF_Tc ()
where
- all_tyvars = all isTyVarTy tys
- (_, tys) = getDictClassTys dict
- (tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
+ given_dicts = filter isDict givens
+ -- Filter out methods, which are only added to
+ -- the given set as an optimisation
+
+addNoInstanceErrs what_doc givens dicts
+ = tcGetInstEnv `thenNF_Tc` \ inst_env ->
+ let
+ (tidy_env1, tidy_givens) = tidyInsts givens
+ (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
+
+ doc = vcat [sep [herald <+> pprInsts tidy_dicts,
+ nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
+ ambig_doc,
+ ptext SLIT("Probable fix:"),
+ nest 4 fix1,
+ nest 4 fix2]
+
+ herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
+ unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
+ | otherwise = empty
+
+ -- The error message when we don't find a suitable instance
+ -- is complicated by the fact that sometimes this is because
+ -- there is no instance, and sometimes it's because there are
+ -- too many instances (overlap). See the comments in TcEnv.lhs
+ -- with the InstEnv stuff.
+
+ ambig_doc
+ | not ambig_overlap = empty
+ | otherwise
+ = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
+ nest 4 (ptext SLIT("depends on the instantiation of") <+>
+ quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
+
+ fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
+ ptext SLIT("to the") <+> what_doc]
+
+ fix2 | null instance_dicts
+ = empty
+ | otherwise
+ = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
+
+ instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
+ -- Insts for which it is worth suggesting an adding an instance declaration
+ -- Exclude implicit parameters, and tyvar dicts
+
+ -- Checks for the ambiguous case when we have overlapping instances
+ ambig_overlap = any ambig_overlap1 dicts
+ ambig_overlap1 dict
+ | isClassDict dict
+ = case lookupInstEnv inst_env clas tys of
+ NoMatch ambig -> ambig
+ other -> False
+ | otherwise = False
+ where
+ (clas,tys) = getDictClassTys dict
+ in
+ addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
-- Used for the ...Thetas variants; all top level
-addNoInstErr (c,ts)
- = addErrTc (ptext SLIT("No instance for") <+> quotes (pprConstraint c ts))
+addNoInstErr pred
+ = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
reduceDepthErr n stack
= vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
nest 4 (pprInstsInFull stack)]
reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+
+-----------------------------------------------
+addCantGenErr inst
+ = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
+ nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
\end{code}