-%
-% (c) The University of Glasgow 2006
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-%
-
-TcSimplify
-
\begin{code}
-module TcSimplify (
- tcSimplifyInfer, tcSimplifyInferCheck,
- tcSimplifyCheck, tcSimplifyRestricted,
- tcSimplifyRuleLhs, tcSimplifyIPs,
- tcSimplifySuperClasses,
- tcSimplifyTop, tcSimplifyInteractive,
- tcSimplifyBracket, tcSimplifyCheckPat,
-
- tcSimplifyDeriv, tcSimplifyDefault,
- bindInstsOfLocalFuns,
-
- tcSimplifyStagedExpr,
-
- misMatchMsg
- ) where
+module TcSimplify(
+ simplifyInfer, simplifySuperClass,
+ simplifyDefault, simplifyDeriv, simplifyBracket,
+ simplifyRule, simplifyTop, simplifyInteractive
+ ) where
#include "HsVersions.h"
-import {-# SOURCE #-} TcUnify( unifyType )
-import HsSyn
-
+import HsSyn
import TcRnMonad
-import TcHsSyn ( hsLPatType )
-import Inst
-import TcEnv
-import InstEnv
-import TcType
+import TcErrors
+import TcCanonical
import TcMType
-import TcIface
-import TcTyFuns
-import DsUtils -- Big-tuple functions
+import TcType
+import TcSMonad
+import TcInteract
+import Inst
import Var
-import Id
-import Name
-import NameSet
-import Class
-import FunDeps
-import PrelInfo
-import PrelNames
-import TysWiredIn
-import ErrUtils
-import BasicTypes
import VarSet
-import VarEnv
-import FiniteMap
+import Name
+import NameEnv ( emptyNameEnv )
import Bag
-import Outputable
import ListSetOps
import Util
-import SrcLoc
-import DynFlags
+import PrelInfo
+import PrelNames
+import Class ( classKey )
+import BasicTypes ( RuleName )
+import Data.List ( partition )
+import Outputable
import FastString
-
-import Control.Monad
-import Data.List
\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.
-
-Note [Choosing which variables to quantify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are about to do a generalisation step. We have in our hand
-
- G the environment
- T the type of the RHS
- 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}
-
-In particular, it's perfectly OK to quantify over more type variables
-than strictly necessary; there is no need to quantify over 'b', since
-it is determined by 'a' which is free in the envt, but it's perfectly
-OK to do so. However we must not quantify over 'a' itself.
-
-Other things being equal, however, we'd like to quantify over as few
-variables as possible: smaller types, fewer type applications, more
-constraints can get into Ct instead of Cq. 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 ...
+*********************************************************************************
+* *
+* External interface *
+* *
+*********************************************************************************
- 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?
-
- 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)
+\begin{code}
+simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
+-- Simplify top-level constraints
+-- Usually these will be implications, when there is
+-- nothing to quanitfy we don't wrap in a degenerate implication,
+-- so we do that here instead
+simplifyTop wanteds
+ = simplifyCheck SimplCheck 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 { loc <- getCtLoc DefaultOrigin
+ ; wanted <- newWantedEvVars theta
+ ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
+ ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
+ ; return () }
+\end{code}
+simplifyBracket 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.
- --------------------------------------
- Notes on principal types
- --------------------------------------
+\begin{code}
+simplifyBracket :: WantedConstraints -> TcM ()
+simplifyBracket wanteds
+ = do { zonked_wanteds <- mapBagM zonkWanted wanteds
+ ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
+ ; return () }
+\end{code}
- class C a where
- op :: a -> a
- f x = let g y = op (y::Int) in True
+*********************************************************************************
+* *
+* Deriving
+* *
+***********************************************************************************
-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
+\begin{code}
+simplifyDeriv :: CtOrigin
+ -> [TyVar]
+ -> ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
+-- Given instance (wanted) => C inst_ty
+-- Simplify 'wanted' as much as possibles
+simplifyDeriv orig tvs theta
+ = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
+ -- One reason is that the constraint solving machinery
+ -- expects *TcTyVars* not TyVars. Another is that
+ -- when looking up instances we don't want overlap
+ -- of type variables
+
+ ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
+
+ ; loc <- getCtLoc orig
+ ; wanted <- newWantedEvVars (substTheta skol_subst theta)
+ ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
+
+ ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
+ ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
+
+ ; let (good, bad) = partition validDerivPred $
+ foldrBag ((:) . wantedEvVarPred) [] unsolved
+ -- See Note [Exotic derived instance contexts]
+ subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+
+ ; reportUnsolvedDeriv bad loc
+ ; return $ substTheta subst_skol good }
+\end{code}
+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.
- --------------------------------------
- The need for forall's in constraints
- --------------------------------------
+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)
-[Exchange on Haskell Cafe 5/6 Dec 2000]
+Notice that this instance (just) satisfies the Paterson termination
+conditions. Then we *could* derive an instance decl like this:
- class C t where op :: t -> Bool
- instance C [t] where op x = True
+ 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.
- 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)
+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.
-The definitions of p and q differ only in the order of the components in
-the pair on their right-hand sides. And yet:
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
- 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!).
+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
+* *
+***********************************************************************************
-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.
+\begin{code}
+simplifyInfer :: Bool -- Apply monomorphism restriction
+ -> TcTyVarSet -- These type variables are free in the
+ -- types to be generalised
+ -> WantedConstraints
+ -> TcM ([TcTyVar], -- Quantify over these type variables
+ [EvVar], -- ... and these constraints
+ TcEvBinds) -- ... binding these evidence variables
+simplifyInfer apply_mr tau_tvs wanted
+ | isEmptyBag wanted -- Trivial case is quite common
+ = do { zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
+ ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
+ ; return (qtvs, [], emptyTcEvBinds) }
-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.
+ | otherwise
+ = do { zonked_wanted <- mapBagM zonkWanted wanted
+ ; traceTc "simplifyInfer {" $ vcat
+ [ ptext (sLit "apply_mr =") <+> ppr apply_mr
+ , ptext (sLit "wanted =") <+> ppr zonked_wanted
+ , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
+ ]
+
+ ; (simple_wanted, tc_binds)
+ <- simplifyAsMuchAsPossible SimplInfer zonked_wanted
+
+ ; gbl_tvs <- tcGetGlobalTyVars
+ ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+ ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted
+ ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
+ (bound, free) | apply_mr = (emptyBag, zonked_simples)
+ | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
+
+ ; traceTc "end simplifyInfer }" $
+ vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
+ , text "wanted = " <+> ppr zonked_wanted
+ , text "qtvs = " <+> ppr qtvs
+ , text "free = " <+> ppr free
+ , text "bound = " <+> ppr bound ]
+
+ -- Turn the quantified meta-type variables into real type variables
+ ; emitConstraints (mapBag WcEvVar free)
+ ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
+ ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
+ ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
+
+------------------------
+simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
+ -> TcM (Bag WantedEvVar, Bag EvBind)
+-- We use this function when inferring the type of a function
+-- The wanted constraints are already zonked
+simplifyAsMuchAsPossible ctxt wanteds
+ = do { let untch = emptyVarSet
+ -- We allow ourselves to unify environment
+ -- variables; hence *no untouchables*
+
+ ; ((unsolved_flats, unsolved_implics), ev_binds)
+ <- runTcS ctxt untch $
+ simplifyApproxLoop 0 wanteds
+
+ -- Report any errors
+ ; mapBagM_ reportUnsolvedImplication unsolved_implics
+
+ ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
+ ; return (final_wanted_evvars, ev_binds) }
+ where
+ simplifyApproxLoop :: Int -> WantedConstraints
+ -> TcS (CanonicalCts, Bag Implication)
+ simplifyApproxLoop n wanteds
+ | n > 10
+ = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
+ | otherwise
+ = do { traceTcS "simplifyApproxLoop" (vcat
+ [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
+ ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
+
+ ; let (extra_flats, thiner_unsolved_implics)
+ = approximateImplications unsolved_implics
+ unsolved
+ = mkWantedConstraints unsolved_flats thiner_unsolved_implics
+
+ ;-- If no new work was produced then we are done with simplifyApproxLoop
+ if isEmptyBag extra_flats
+ then do { traceTcS "simplifyApproxLoopRes" (vcat
+ [ ptext (sLit "Wanted = ") <+> ppr wanteds
+ , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
+ ; return (unsolved_flats, unsolved_implics) }
+
+ else -- Produced new flat work wanteds, go round the loop
+ simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
+ }
+
+approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
+-- (wc1, impls2) <- approximateImplications impls
+-- splits 'impls' into two parts
+-- wc1: a bag of constraints that do not mention any skolems
+-- impls2: a bag of *thiner* implication constraints
+approximateImplications impls
+ = splitBag (do_implic emptyVarSet) impls
+ where
+ ------------------
+ do_wanted :: TcTyVarSet -> WantedConstraint
+ -> (WantedConstraints, WantedConstraints)
+ do_wanted skols (WcImplic impl)
+ = let (fl_w, mb_impl) = do_implic skols impl
+ in (fl_w, mapBag WcImplic mb_impl)
+ do_wanted skols wc@(WcEvVar wev)
+ | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
+ | otherwise = (emptyBag, unitBag wc)
+
+ ------------------
+ do_implic :: TcTyVarSet -> Implication
+ -> (WantedConstraints, Bag Implication)
+ do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
+ = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
+ else unitBag impl{ ic_wanted = rest_wanted } )
+ where
+ (floatable_wanted, rest_wanted)
+ = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
+
+ ------------------
+ splitBag :: (a -> (WantedConstraints, Bag a))
+ -> Bag a -> (WantedConstraints, Bag a)
+ splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
+ where
+ do_one x (b1,b2)
+ = (wcs `unionBags` b1, imps `unionBags` b2)
+ where
+ (wcs, imps) = f x
+\end{code}
- --------------------------------------
- Notes on implicit parameters
- --------------------------------------
+\begin{code}
+findQuantifiedTyVars :: Bool -- Apply the MR
+ -> Bag WantedEvVar -- Simplified constraints from RHS
+ -> TyVarSet -- Free in tau-type of definition
+ -> TyVarSet -- Free in the envt
+ -> TyVarSet -- Quantify over these
+
+findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
+ | isEmptyBag wanteds = init_tvs
+ | apply_mr = init_tvs `minusVarSet` constrained_tvs
+ | otherwise = fixVarSet mk_next init_tvs
+ where
+ init_tvs = tau_tvs `minusVarSet` gbl_tvs
+ mk_next tvs = foldrBag grow_one tvs wanteds
+
+ grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
+ where
+ extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
+
+ constrained_tvs = tyVarsOfWantedEvVars wanteds
+
+--------------------
+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 = wantedEvVarPred wev
+\end{code}
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
over implicit parameters. See the predicate isFreeWhenInferring.
-Note [Implicit parameters and ambiguity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Only a *class* predicate can give rise to ambiguity
-An *implicit parameter* cannot. For example:
- foo :: (?x :: [a]) => Int
- foo = length ?x
-is fine. The call site will suppply a particular 'x'
-
-Furthermore, the type variables fixed by an implicit parameter
-propagate to the others. E.g.
- foo :: (Show a, ?x::[a]) => Int
- foo = show (?x++?x)
-The type of foo looks ambiguous. But it isn't, because at a call site
-we might have
- let ?x = 5::Int in foo
-and all is well. In effect, implicit parameters are, well, parameters,
-so we can take their type variables into account as part of the
-"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
-
-
-Question 2: type signatures
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-BUT WATCH OUT: When you supply a type signature, we can't force you
-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.
-
+*********************************************************************************
+* *
+* Superclasses *
+* *
+***********************************************************************************
+
+When constructing evidence for superclasses in an instance declaration,
+ * we MUST have the "self" dictionary available, but
+ * we must NOT have its superclasses derived from "self"
+
+Moreover, we must *completely* solve the constraints right now,
+not wrap them in an implication constraint to solve later. Why?
+Because when that implication constraint is solved there may
+be some unrelated other solved top-level constraints that
+recursively depend on the superclass we are building. Consider
+ class Ord a => C a where
+ instance C [Int] where ...
+Then we get
+ dCListInt :: C [Int]
+ dCListInt = MkC $cNum ...
+
+ $cNum :: Ord [Int] -- The superclass
+ $cNum = let self = dCListInt in <solve Ord [Int]>
+
+Now, if there is some *other* top-level constraint solved
+looking like
+ foo :: Ord [Int]
+ foo = scsel dCInt
+we must not solve the (Ord [Int]) wanted from foo!!
\begin{code}
-tcSimplifyInfer
- :: SDoc
- -> TcTyVarSet -- fv(T); type vars
- -> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)
- [Inst], -- Dict Ids that must be bound here (zonked)
- TcDictBinds) -- Bindings
- -- Any free (escaping) Insts are tossed into the environment
+simplifySuperClass :: EvVar -- The "self" dictionary
+ -> WantedConstraints
+ -> TcM ()
+simplifySuperClass self wanteds
+ = do { wanteds <- mapBagM zonkWanted wanteds
+ ; loc <- getCtLoc NoScSkol
+ ; (unsolved, ev_binds)
+ <- runTcS SimplCheck emptyVarSet $
+ do { can_self <- canGivens loc [self]
+ ; let inert = foldlBag extendInertSet emptyInert can_self
+ -- No need for solveInteract; we know it's inert
+
+ ; solveWanteds inert wanteds }
+
+ ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
+ reportUnsolved unsolved }
\end{code}
-\begin{code}
-tcSimplifyInfer doc tau_tvs wanted
- = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; wanted' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let preds1 = fdPredsOfInsts wanted'
- gbl_tvs1 = oclose preds1 gbl_tvs
- qtvs = growInstsTyVars wanted' tau_tvs1 `minusVarSet` gbl_tvs1
- -- See Note [Choosing which variables to quantify]
-
- -- To maximise sharing, remove from consideration any
- -- constraints that don't mention qtvs at all
- ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; extendLIEs free
-
- -- To make types simple, reduce as much as possible
- ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (growInstsTyVars wanted' tau_tvs1) $$ ppr gbl_tvs $$
- ppr gbl_tvs1 $$ ppr free $$ ppr bound))
- ; (irreds1, binds1) <- tryHardCheckLoop doc bound
-
- -- Note [Inference and implication constraints]
- ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
- ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
-
- -- Now work out all over again which type variables to quantify,
- -- exactly in the same way as before, but starting from irreds2. Why?
- -- a) By now improvment may have taken place, and we must *not*
- -- quantify over any variable free in the environment
- -- tc137 (function h inside g) is an example
- --
- -- b) Do not quantify over constraints that *now* do not
- -- mention quantified type variables, because they are
- -- simply ambiguous (or might be bound further out). Example:
- -- f :: Eq b => a -> (a, b)
- -- g x = fst (f x)
- -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
- -- We decide to quantify over 'alpha' alone, but free1 does not include f77
- -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
- -- constraint (Eq beta), which we dump back into the free set
- -- See test tcfail181
- --
- -- c) irreds may contain type variables not previously mentioned,
- -- e.g. instance D a x => Foo [a]
- -- wanteds = Foo [a]
- -- Then after simplifying we'll get (D a x), and x is fresh
- -- We must quantify over x else it'll be totally unbound
- ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
- ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
- -- Note that we start from gbl_tvs1
- -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
- -- we've already put some of the original preds1 into frees
- -- E.g. wanteds = C a b (where a->b)
- -- gbl_tvs = {a}
- -- tau_tvs = {b}
- -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
- -- irreds2 will be empty. But we don't want to generalise over b!
- ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
- qtvs = growInstsTyVars irreds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
- ---------------------------------------------------
- -- BUG WARNING: there's a nasty bug lurking here
- -- fdPredsOfInsts may return preds that mention variables quantified in
- -- one of the implication constraints in irreds2; and that is clearly wrong:
- -- we might quantify over too many variables through accidental capture
- ---------------------------------------------------
- ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
- ; extendLIEs free
-
- -- Turn the quantified meta-type variables into real type variables
- ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
-
- -- We can't abstract over any remaining unsolved
- -- implications so instead just float them outwards. Ugh.
- ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
- ; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
-
- -- Prepare equality instances for quantification
- ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
- ; q_eqs <- mapM finalizeEqInst q_eqs0
-
- ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
- -- NB: when we are done, we might have some bindings, but
- -- the final qtvs might be empty. See Note [NO TYVARS] below.
-
-approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
--- Note [Inference and implication constraints]
--- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
--- - fetching any dicts inside them that are free
--- - using those dicts as cruder constraints, to solve the implications
--- - returning the extra ones too
-
-approximateImplications doc want_dict irreds
- | null extra_dicts
- = return (irreds, emptyBag)
- | otherwise
- = do { extra_dicts' <- mapM cloneDict extra_dicts
- ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
- -- By adding extra_dicts', we make them
- -- available to solve the implication constraints
- where
- extra_dicts = get_dicts (filter isImplicInst irreds)
-
- get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
- -- Find the wanted constraints in implication constraints that satisfy
- -- want_dict, and are not bound by forall's in the constraint itself
- get_dicts ds = concatMap get_dict ds
-
- get_dict d@(Dict {}) | want_dict d = [d]
- | otherwise = []
- get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
- = [ d | let tv_set = mkVarSet tvs
- , d <- get_dicts wanteds
- , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
- get_dict i@(EqInst {}) | want_dict i = [i]
- | otherwise = []
- get_dict other = pprPanic "approximateImplications" (ppr other)
-\end{code}
+*********************************************************************************
+* *
+* RULES *
+* *
+***********************************************************************************
-Note [Inference and implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have a wanted implication constraint (perhaps arising from
-a nested pattern match) like
- C a => D [a]
-and we are now trying to quantify over 'a' when inferring the type for
-a function. In principle it's possible that there might be an instance
- instance (C a, E a) => D [a]
-so the context (E a) would suffice. The Right Thing is to abstract over
-the implication constraint, but we don't do that (a) because it'll be
-surprising to programmers and (b) because we don't have the machinery to deal
-with 'given' implications.
-
-So our best approximation is to make (D [a]) part of the inferred
-context, so we can use that to discharge the implication. Hence
-the strange function get_dicts in approximateImplications.
-
-The common cases are more clear-cut, when we have things like
- forall a. C a => C b
-Here, abstracting over (C b) is not an approximation at all -- but see
-Note [Freeness and implications].
-
-See Trac #1430 and test tc228.
-
-
-\begin{code}
------------------------------------------------------------
--- tcSimplifyInferCheck is used when we know the constraints we are to simplify
--- against, but we don't know the type variables over which we are going to quantify.
--- This happens when we have a type signature for a mutually recursive group
-tcSimplifyInferCheck
- :: InstLoc
- -> TcTyVarSet -- fv(T)
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([TyVar], -- Fully zonked, and quantified
- TcDictBinds) -- Bindings
-
-tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
- ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-
- -- Figure out which type variables to quantify over
- -- You might think it should just be the signature tyvars,
- -- but in bizarre cases you can get extra ones
- -- f :: forall a. Num a => a -> a
- -- f x = fst (g (x, head [])) + 1
- -- g a b = (b,a)
- -- Here we infer g :: forall a b. a -> b -> (b,a)
- -- We don't want g to be monomorphic in b just because
- -- f isn't quantified over b.
- ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
- ; all_tvs <- zonkTcTyVarsAndFV all_tvs
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
- -- We could close gbl_tvs, but its not necessary for
- -- soundness, and it'll only affect which tyvars, not which
- -- dictionaries, we quantify over
-
- ; qtvs' <- zonkQuantifiedTyVars qtvs
-
- -- Now we are back to normal (c.f. tcSimplCheck)
- ; implic_bind <- bindIrreds loc qtvs' givens irreds
-
- ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
- ; return (qtvs', binds `unionBags` implic_bind) }
-\end{code}
-
-Note [Squashing methods]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Be careful if you want to float methods more:
- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
-From an application (truncate f i) we get
- t1 = truncate at f
- t2 = t1 at i
-If we have also have a second occurrence of truncate, we get
- t3 = truncate at f
- t4 = t3 at i
-When simplifying with i,f free, we might still notice that
-t1=t3; but alas, the binding for t2 (which mentions t1)
-may continue to float out!
-
-
-Note [NO TYVARS]
-~~~~~~~~~~~~~~~~~
- class Y a b | a -> b where
- y :: a -> X b
-
- 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 Note [Inheriting implicit parameters]
-
-{- No longer used (with implication constraints)
-isFreeWhenChecking :: TyVarSet -- Quantified tyvars
- -> NameSet -- Quantified implicit parameters
- -> Inst -> Bool
-isFreeWhenChecking qtvs ips inst
- = isFreeWrtTyVars qtvs inst
- && isFreeWrtIPs ips inst
--}
-
-isFreeWrtTyVars :: VarSet -> Inst -> Bool
-isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
-isFreeWrtIPs :: NameSet -> Inst -> Bool
-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 is used when checking expression type signatures,
--- class decls, instance decls etc.
-tcSimplifyCheck :: InstLoc
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheck loc qtvs givens wanteds
- = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { traceTc (text "tcSimplifyCheck")
- ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc qtvs givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
--- tcSimplifyCheckPat is used for existential pattern match
-tcSimplifyCheckPat :: InstLoc
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc qtvs givens wanteds
- = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { traceTc (text "tcSimplifyCheckPat")
- ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrredsR loc qtvs givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
-bindIrreds :: InstLoc -> [TcTyVar]
- -> [Inst] -> [Inst]
- -> TcM TcDictBinds
-bindIrreds loc qtvs givens irreds
- = bindIrredsR loc qtvs givens irreds
-
-bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
-bindIrredsR loc qtvs givens irreds
- | null irreds
- = return emptyBag
- | otherwise
- = do { let givens' = filter isAbstractableInst givens
- -- The givens can (redundantly) include methods
- -- We want to retain both EqInsts and Dicts
- -- There should be no implicadtion constraints
- -- See Note [Pruning the givens in an implication constraint]
-
- -- If there are no 'givens', then it's safe to
- -- partition the 'wanteds' by their qtvs, thereby trimming irreds
- -- See Note [Freeness and implications]
- ; irreds' <- if null givens'
- then do
- { let qtv_set = mkVarSet qtvs
- (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
- ; extendLIEs frees
- ; return real_irreds }
- else return irreds
-
- ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
- -- This call does the real work
- -- If irreds' is empty, it does something sensible
- ; extendLIEs implics
- ; return bind }
-
-
-makeImplicationBind :: InstLoc -> [TcTyVar]
- -> [Inst] -> [Inst]
- -> TcM ([Inst], TcDictBinds)
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them.
---
--- The binding looks like
--- (ir1, .., irn) = f qtvs givens
--- where f is (evidence for) the new implication constraint
--- f :: forall qtvs. givens => (ir1, .., irn)
--- qtvs includes coercion variables
---
--- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs
- givens -- Guaranteed all Dicts or EqInsts
- irreds
- | null irreds -- If there are no irreds, we are done
- = return ([], emptyBag)
- | otherwise -- Otherwise we must generate a binding
- = do { uniq <- newUnique
- ; span <- getSrcSpanM
- ; let (eq_givens, dict_givens) = partition isEqInst givens
-
- -- extract equality binders
- eq_cotvs = map eqInstType eq_givens
-
- -- make the implication constraint instance
- name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name,
- tci_tyvars = all_tvs,
- tci_given = eq_givens ++ dict_givens,
- -- same order as binders
- tci_wanted = irreds,
- tci_loc = loc }
-
- -- create binders for the irreducible dictionaries
- dict_irreds = filter (not . isEqInst) irreds
- dict_irred_ids = map instToId dict_irreds
- lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
-
- -- create the binding
- rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId dict_givens)
- <.> mkWpTyApps eq_cotvs
- <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | [dict_irred_id] <- dict_irred_ids
- = VarBind dict_irred_id rhs
- | otherwise
- = PatBind { pat_lhs = lpat
- , pat_rhs = unguardedGRHSs rhs
- , pat_rhs_ty = hsLPatType lpat
- , bind_fvs = placeHolderNames
- }
-
- ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
- ; return ([implic_inst], unitBag (L span bind))
- }
-
------------------------------------------------------------
-tryHardCheckLoop :: SDoc
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-tryHardCheckLoop doc wanteds
- = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
- ; return (irreds,binds)
- }
- where
- try_me _ = ReduceMe
- -- Here's the try-hard bit
-
------------------------------------------------------------
-gentleCheckLoop :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-gentleCheckLoop inst_loc givens wanteds
- = do { (irreds,binds) <- checkLoop env wanteds
- ; return (irreds,binds)
- }
- where
- env = mkRedEnv (pprInstLoc inst_loc) try_me givens
-
- try_me inst | isMethodOrLit inst = ReduceMe
- | otherwise = Stop
- -- When checking against a given signature
- -- we MUST be very gentle: Note [Check gently]
-
-gentleInferLoop :: SDoc -> [Inst]
- -> TcM ([Inst], TcDictBinds)
-gentleInferLoop doc wanteds
- = do { (irreds, binds) <- checkLoop env wanteds
- ; return (irreds, binds) }
- where
- env = mkInferRedEnv doc try_me
- try_me inst | isMethodOrLit inst = ReduceMe
- | otherwise = Stop
-\end{code}
-
-Note [Check gently]
-~~~~~~~~~~~~~~~~~~~~
-We have to very careful about not simplifying too vigorously
-Example:
- data T a where
- MkT :: a -> T [a]
-
- f :: Show b => T b -> b
- f (MkT x) = show [x]
-
-Inside the pattern match, which binds (a:*, x:a), we know that
- b ~ [a]
-Hence we have a dictionary for Show [a] available; and indeed we
-need it. We are going to build an implication contraint
- forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledge (Show b)
-
-But we MUST NOT reduce (Show [a]) to (Show a), else the whole
-thing becomes insoluble. So we simplify gently (get rid of literals
-and methods only, plus common up equal things), deferring the real
-work until top level, when we solve the implication constraint
-with tryHardCheckLooop.
-
-
-\begin{code}
------------------------------------------------------------
-checkLoop :: RedEnv
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
--- Precondition: givens are completely rigid
--- Postcondition: returned Insts are zonked
-
-checkLoop env wanteds
- = go env wanteds
- where go env wanteds
- = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
- ; env' <- zonkRedEnv env
- ; wanteds' <- zonkInsts wanteds
-
- ; (improved, tybinds, binds, irreds)
- <- reduceContext env' wanteds'
- ; execTcTyVarBinds tybinds
-
- ; if null irreds || not improved then
- return (irreds, binds)
- else do
-
- -- If improvement did some unification, we go round again.
- -- We start again with irreds, not wanteds
- -- Using an instance decl might have introduced a fresh type
- -- variable which might have been unified, so we'd get an
- -- infinite loop if we started again with wanteds!
- -- See Note [LOOP]
- { (irreds1, binds1) <- go env' irreds
- ; return (irreds1, binds `unionBags` binds1) } }
-\end{code}
-
-Note [Zonking RedEnv]
-~~~~~~~~~~~~~~~~~~~~~
-It might appear as if the givens in RedEnv are always rigid, but that is not
-necessarily the case for programs involving higher-rank types that have class
-contexts constraining the higher-rank variables. An example from tc237 in the
-testsuite is
-
- class Modular s a | s -> a
-
- wim :: forall a w. Integral a
- => a -> (forall s. Modular s a => M s w) -> w
- wim i k = error "urk"
-
- test5 :: (Modular s a, Integral a) => M s a
- test5 = error "urk"
-
- test4 = wim 4 test4'
-
-Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
-quantified further outside. When type checking test4, we have to check
-whether the signature of test5 is an instance of
-
- (forall s. Modular s a => M s w)
-
-Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
-givens.
-
-Given the FD of Modular in this example, class improvement will instantiate
-t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
-Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
-the givens, we will get into a loop as improveOne uses the unification engine
-Unify.tcUnifyTys, which doesn't know about mutable type variables.
-
-
-Note [LOOP]
-~~~~~~~~~~~
- class If b t e r | b t e -> r
- instance If T t e t
- instance If F t e e
- class Lte a b c | a b -> c where lte :: a -> b -> c
- instance Lte Z b T
- instance (Lte a b l,If l b a c) => Max a b c
-
-Wanted: Max Z (S x) y
-
-Then we'll reduce using the Max instance to:
- (Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints. What we *can't* do is start again
-with (Max Z (S x) y)!
-
-
-
-%************************************************************************
-%* *
- 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.
-Two more nasty cases are in
- tcrun021
- tcrun033
-
-Solution:
- - Satisfy the superclass context *all by itself*
- (tcSimplifySuperClasses)
- - And do so completely; i.e. no left-over constraints
- to mix with the constraints arising from method declarations
-
-
-Note [Recursive instances and superclases]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this code, which arises in the context of "Scrap Your
-Boilerplate with Class".
-
- class Sat a
- class Data ctx a
- instance Sat (ctx Char) => Data ctx Char
- instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
-
- class Data Maybe a => Foo a
-
- instance Foo t => Sat (Maybe t)
-
- instance Data Maybe a => Foo a
- instance Foo a => Foo [a]
- instance Foo [Char]
-
-In the instance for Foo [a], when generating evidence for the superclasses
-(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
-Using the instance for Data, we therefore need
- (Sat (Maybe [a], Data Maybe a)
-But we are given (Foo a), and hence its superclass (Data Maybe a).
-So that leaves (Sat (Maybe [a])). Using the instance for Sat means
-we need (Foo [a]). And that is the very dictionary we are bulding
-an instance for! So we must put that in the "givens". So in this
-case we have
- Given: Foo a, Foo [a]
- Watend: Data Maybe [a]
-
-BUT we must *not not not* put the *superclasses* of (Foo [a]) in
-the givens, which is what 'addGiven' would normally do. Why? Because
-(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
-by selecting a superclass from Foo [a], which simply makes a loop.
-
-On the other hand we *must* put the superclasses of (Foo a) in
-the givens, as you can see from the derivation described above.
-
-Conclusion: in the very special case of tcSimplifySuperClasses
-we have one 'given' (namely the "this" dictionary) whose superclasses
-must not be added to 'givens' by addGiven.
-
-There is a complication though. Suppose there are equalities
- instance (Eq a, a~b) => Num (a,b)
-Then we normalise the 'givens' wrt the equalities, so the original
-given "this" dictionary is cast to one of a different type. So it's a
-bit trickier than before to identify the "special" dictionary whose
-superclasses must not be added. See test
- indexed-types/should_run/EqInInstance
-
-We need a persistent property of the dictionary to record this
-special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
-but cool), which is maintained by dictionary normalisation.
-Specifically, the InstLocOrigin is
- NoScOrigin
-then the no-superclass thing kicks in. WATCH OUT if you fiddle
-with InstLocOrigin!
-
-\begin{code}
-tcSimplifySuperClasses
- :: InstLoc
- -> Inst -- The dict whose superclasses
- -- are being figured out
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds
-tcSimplifySuperClasses loc this givens sc_wanteds
- = do { traceTc (text "tcSimplifySuperClasses")
-
- -- Note [Recursive instances and superclases]
- ; no_sc_loc <- getInstLoc NoScOrigin
- ; let no_sc_this = setInstLoc this no_sc_loc
-
- ; let env = RedEnv { red_doc = pprInstLoc loc,
- red_try_me = try_me,
- red_givens = no_sc_this : givens,
- red_stack = (0,[]),
- red_improve = False } -- No unification vars
-
-
- ; (irreds,binds1) <- checkLoop env sc_wanteds
- ; let (tidy_env, tidy_irreds) = tidyInsts irreds
- ; reportNoInstances tidy_env (Just (loc, givens)) [] tidy_irreds
- ; return binds1 }
- where
- try_me _ = ReduceMe -- Try hard, so we completely solve the superclass
- -- constraints right here. See Note [SUPERCLASS-LOOP 1]
-\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:
+Note [Simplifying RULE lhs constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+On the LHS of transformation rules we only simplify only equalitis,
+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.
- instance (HasBinary ty IO) => HasCodedValue ty
-
- foo :: HasCodedValue a => String -> IO a
-
- doDecodeIO :: HasCodedValue a => () -> () -> IO a
- doDecodeIO codedValue view
- = let { act = foo "foo" } in act
-
-You might think this should work becuase the call to foo gives rise to a constraint
-(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
-restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
-constraint using the (rather bogus) instance declaration, and now we are stuffed.
-
-I claim this is not really a bug -- but it bit Sergey as well as George. So here's
-plan D
-
-
-Plan D (a variant of plan B)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
-
- The point here is that it's generally OK to have too few qtvs; that is,
- to make the thing more monomorphic than it could be. We don't want to
- do that in the common cases, but in wierd cases it's ok: the programmer
- can always add a signature.
-
- 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 ([TyVar], -- Tyvars to quantify (zonked and quantified)
- 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
- = do { traceTc (text "tcSimplifyRestricted")
- ; wanteds_z <- zonkInsts 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
- ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
- ; (_imp, _tybinds, _binds, constrained_dicts)
- <- reduceContext env wanteds_z
-
- -- Next, figure out the tyvars we will quantify over
- ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; gbl_tvs' <- tcGetGlobalTyVars
- ; constrained_dicts' <- zonkInsts constrained_dicts
-
- ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
- -- As in tcSimplifyInfer
-
- -- Do not quantify over constrained type variables:
- -- this is the monomorphism restriction
- constrained_tvs' = tyVarsOfInsts constrained_dicts'
- qtvs = qtvs1 `minusVarSet` constrained_tvs'
- pp_bndrs = pprWithCommas (quotes . ppr) bndrs
-
- -- Warn in the mono
- ; warn_mono <- doptM Opt_WarnMonomorphism
- ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
- (vcat[ ptext (sLit "the Monomorphism Restriction applies to the binding")
- <> plural bndrs <+> ptext (sLit "for") <+> pp_bndrs,
- ptext (sLit "Consider giving a type signature for") <+> pp_bndrs])
-
- ; traceTc (text "tcSimplifyRestricted" <+> vcat [
- pprInsts wanteds, pprInsts constrained_dicts',
- ppr _binds,
- ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
-
- -- 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) = Stop
- | otherwise = ReduceMe
- env = mkNoImproveRedEnv doc try_me
- ; (_imp, tybinds, binds, irreds) <- reduceContext env wanteds_z
- ; execTcTyVarBinds tybinds
-
- -- See "Notes on implicit parameters, Question 4: top level"
- ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
- if is_nested_group then
- extendLIEs irreds
- else do { let (bad_ips, non_ips) = partition isIPDict irreds
- ; addTopIPErrs bndrs bad_ips
- ; extendLIEs non_ips }
-
- ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
- ; return (qtvs', binds) }
-\end{code}
-
-
-%************************************************************************
-%* *
- 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.
-Simpler, maybe, but alas not simple (see Trac #2494)
-
-* Type errors may give rise to an (unsatisfiable) equality constraint
-
-* Applications of a higher-rank function on the LHS may give
- rise to an implication constraint, esp if there are unsatisfiable
- equality constraints inside.
-
-\begin{code}
-tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
-tcSimplifyRuleLhs wanteds
- = do { wanteds' <- zonkInsts wanteds
- ; (irreds, binds) <- go [] emptyBag wanteds'
- ; let (dicts, bad_irreds) = partition isDict irreds
- ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
- ; addNoInstanceErrs (nub bad_irreds)
- -- The nub removes duplicates, which has
- -- not happened otherwise (see notes above)
- ; return (dicts, binds) }
- where
- go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
- go irreds binds []
- = return (irreds, binds)
- go irreds binds (w:ws)
- | isDict w
- = go (w:irreds) binds ws
- | isImplicInst w -- Have a go at reducing the implication
- = do { (binds1, irreds1) <- reduceImplication red_env w
- ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
- ; go (bad_irreds ++ irreds)
- (binds `unionBags` binds1)
- (ok_irreds ++ ws)}
- | otherwise
- = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
- -- to fromInteger; this looks fragile to me
- ; lookup_result <- lookupSimpleInst w'
- ; case lookup_result of
- NoInstance -> go (w:irreds) binds ws
- GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
- where
- binds' = addInstToDictBind binds w rhs
- }
-
- -- Sigh: we need to reduce inside implications
- red_env = mkInferRedEnv doc try_me
- doc = ptext (sLit "Implication constraint in RULE lhs")
- try_me inst | isMethodOrLit inst = ReduceMe
- | otherwise = Stop -- Be gentle
-\end{code}
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.
-tcSimplifyBracket is used when simplifying the constraints arising from
-a Template Haskell bracket [| ... |]. We want to check that there aren't
-any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
-Show instance), but we aren't otherwise interested in the results.
-Nor do we care about ambiguous dictionaries etc. We will type check
-this bracket again at its usage site.
+HOWEVER, under a nested implication things are different
+Consider
+ f :: (forall a. Eq a => a->a) -> Bool -> ...
+ {-# RULES "foo" forall (v::forall b. Eq b => b->b).
+ f b True = ...
+ #=}
+Here we *must* solve the wanted (Eq a) from the given (Eq a)
+resulting from skolemising the agument type of g. So we
+revert to SimplCheck when going under an implication.
\begin{code}
-tcSimplifyBracket :: [Inst] -> TcM ()
-tcSimplifyBracket wanteds
- = do { _ <- tryHardCheckLoop doc wanteds
- ; return () }
- 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 { zonked_lhs <- mapBagM zonkWanted lhs_wanted
+ ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
+
+ -- Don't quantify over equalities (judgement call here)
+ ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
+ lhs_dicts = map wantedEvVarToVar (bagToList dicts)
+ -- Dicts and implicit parameters
+ ; reportUnsolvedWantedEvVars eqs
+
+ -- 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
+ ; loc <- getCtLoc (RuleSkol name)
+ ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
+ Implic { ic_env_tvs = emptyVarSet -- No untouchables
+ , ic_env = emptyNameEnv
+ , ic_skols = mkVarSet tv_bndrs
+ , ic_scoped = panic "emitImplication"
+ , ic_given = lhs_dicts
+ , ic_wanted = 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
- -- We need a loop so that we do improvement, and then
- -- (next time round) generate a binding to connect the two
- -- let ?x = e in ?x
- -- Here the two ?x's have different types, and improvement
- -- makes them the same.
-
-tcSimplifyIPs given_ips wanteds
- = do { wanteds' <- zonkInsts wanteds
- ; given_ips' <- zonkInsts given_ips
- -- Unusually for checking, we *must* zonk the given_ips
-
- ; let env = mkRedEnv doc try_me given_ips'
- ; (improved, tybinds, binds, irreds) <- reduceContext env wanteds'
- ; execTcTyVarBinds tybinds
-
- ; if null irreds || not improved then
- ASSERT( all is_free irreds )
- do { extendLIEs irreds
- ; return binds }
- else do
- -- If improvement did some unification, we go round again.
- -- We start again with irreds, not wanteds
- -- Using an instance decl might have introduced a fresh type
- -- variable which might have been unified, so we'd get an
- -- infinite loop if we started again with wanteds!
- -- See Note [LOOP]
- { binds1 <- tcSimplifyIPs given_ips' irreds
- ; return $ binds `unionBags` binds1
- } }
+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 <- mapBagM zonkWanted wanteds
+
+ ; traceTc "simplifyCheck {" (vcat
+ [ ptext (sLit "wanted =") <+> ppr wanteds ])
+
+ ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
+ solveWanteds emptyInert wanteds
+
+ ; traceTc "simplifyCheck }" $
+ ptext (sLit "unsolved =") <+> ppr unsolved
+
+ ; reportUnsolved unsolved
+
+ ; return ev_binds }
+
+----------------
+solveWanteds :: InertSet -- Given
+ -> WantedConstraints -- Wanted
+ -> TcS (CanonicalCts, -- Unsolved flats
+ Bag Implication) -- Unsolved implications
+-- solveWanteds iterates when it is able to float equalities
+-- out of one or more of the implications
+solveWanteds inert wanteds
+ = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
+ ; can_flats <- canWanteds $ bagToList flat_wanteds
+ ; traceTcS "solveWanteds {" $
+ vcat [ text "wanteds =" <+> ppr wanteds
+ , text "inert =" <+> ppr inert ]
+ ; (unsolved_flats, unsolved_implics)
+ <- simpl_loop 1 can_flats implic_wanteds
+ ; traceTcS "solveWanteds }" $
+ vcat [ text "wanteds =" <+> ppr wanteds
+ , text "unsolved_flats =" <+> ppr unsolved_flats
+ , text "unsolved_implics =" <+> ppr unsolved_implics ]
+ ; return (unsolved_flats, unsolved_implics) }
where
- doc = text "tcSimplifyIPs" <+> ppr given_ips
- ip_set = mkNameSet (ipNamesOfInsts given_ips)
- is_free inst = isFreeWrtIPs ip_set inst
-
- -- Simplify any methods that mention the implicit parameter
- try_me inst | is_free inst = Stop
- | otherwise = ReduceMe
-\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 = do
- -- Common case
- extendLIEs wanteds
- return emptyLHsBinds
-
- | otherwise
- = do { (irreds, binds) <- gentleInferLoop doc for_me
- ; extendLIEs not_for_me
- ; extendLIEs irreds
- ; return binds }
+ simpl_loop :: Int
+ -> CanonicalCts -- May inlude givens (in the recursive call)
+ -> Bag Implication
+ -> TcS (CanonicalCts, Bag Implication)
+ simpl_loop n can_ws implics
+ | n>10
+ = trace "solveWanteds: loop" $ -- Always bleat
+ do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
+ ; return (can_ws, implics) }
+
+ | otherwise
+ = do { inert1 <- solveInteract inert can_ws
+ ; let (inert2, unsolved_flats) = extractUnsolved inert1
+
+ ; traceTcS "solveWanteds/done flats" $
+ vcat [ text "inerts =" <+> ppr inert2
+ , text "unsolved =" <+> ppr unsolved_flats ]
+
+ -- See Note [Preparing inert set for implications]
+ ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
+ ; (implic_eqs, unsolved_implics)
+ <- flatMapBagPairM (solveImplication inert_for_implics) 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.
+ ; final_eqs <- if not (isEmptyBag implic_eqs)
+ then return implic_eqs
+ else applyDefaultingRules inert2 unsolved_flats
+ -- default_eqs are *givens*, so simpl_loop may
+ -- recurse with givens in the argument
+
+ ; if isEmptyBag final_eqs then
+ return (unsolved_flats, unsolved_implics)
+ else
+ do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
+ [ text "floated_unsolved_eqs =" <+> ppr final_eqs
+ , text "unsolved_implics = " <+> ppr unsolved_implics ]
+ ; simpl_loop (n+1)
+ (unsolved_flats `unionBags` final_eqs)
+ unsolved_implics
+ } }
+
+solveImplication :: InertSet -- Given
+ -> Implication -- Wanted
+ -> TcS (CanonicalCts, -- Unsolved unification 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 inert
+ imp@(Implic { ic_env_tvs = untch
+ , ic_binds = ev_binds
+ , ic_skols = skols
+ , ic_given = givens
+ , ic_wanted = wanteds
+ , ic_loc = loc })
+ = nestImplicTcS ev_binds untch $
+ do { traceTcS "solveImplication {" (ppr imp)
+
+ -- Solve flat givens
+ ; can_givens <- canGivens loc givens
+ ; given_inert <- solveInteract inert can_givens
+
+ -- Simplify the wanteds
+ ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
+
+ ; let (res_flat_free, res_flat_bound)
+ = floatEqualities skols givens unsolved_flats
+ unsolved = mkWantedConstraints res_flat_bound unsolved_implics
+
+ ; traceTcS "solveImplication end }" $ vcat
+ [ text "res_flat_free =" <+> ppr res_flat_free
+ , text "res_flat_bound =" <+> ppr res_flat_bound
+ , text "unsolved_implics =" <+> ppr unsolved_implics ]
+
+ ; let res_bag | isEmptyBag unsolved = emptyBag
+ | otherwise = unitBag (imp { ic_wanted = unsolved })
+
+ ; return (res_flat_free, res_bag) }
+
+floatEqualities :: TcTyVarSet -> [EvVar]
+ -> CanonicalCts -> (CanonicalCts, CanonicalCts)
+floatEqualities skols can_given wanteds
+ | hasEqualities can_given = (emptyBag, wanteds)
+ | otherwise = partitionBag is_floatable wanteds
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
+ is_floatable :: CanonicalCt -> Bool
+ is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
+ | isMetaTyVar tv || isMetaTyVarTy ty
+ = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
+ is_floatable _ = False
\end{code}
-
-%************************************************************************
-%* *
-\subsection{Data types for the reduction mechanism}
-%* *
-%************************************************************************
-
-The main control over context reduction is here
-
-\begin{code}
-data RedEnv
- = RedEnv { red_doc :: SDoc -- The context
- , red_try_me :: Inst -> WhatToDo
- , red_improve :: Bool -- True <=> do improvement
- , red_givens :: [Inst] -- All guaranteed rigid
- -- Always dicts & equalities
- -- but see Note [Rigidity]
+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 uop
+ 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.
+
+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
+
+*********************************************************************************
+* *
+* Defaulting and disamgiguation *
+* *
+*********************************************************************************
+
+Basic plan behind applyDefaulting rules:
- , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
- -- See Note [RedStack]
- }
-
--- Note [Rigidity]
--- The red_givens are rigid so far as cmpInst is concerned.
--- There is one case where they are not totally rigid, namely in tcSimplifyIPs
--- let ?x = e in ...
--- Here, the given is (?x::a), where 'a' is not necy a rigid type
--- But that doesn't affect the comparison, which is based only on mame.
-
--- Note [RedStack]
--- The red_stack pair (n,insts) pair is just used for error reporting.
--- 'n' is always the depth of the stack.
--- The 'insts' is the stack of Insts being reduced: to produce X
--- I had to produce Y, to produce Y I had to produce Z, and so on.
-
-
-mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
-mkRedEnv doc try_me givens
- = RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = givens,
- red_stack = (0,[]),
- red_improve = True }
-
-mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
--- No givens at all
-mkInferRedEnv doc try_me
- = RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = [],
- red_stack = (0,[]),
- red_improve = True }
-
-mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
--- Do not do improvement; no givens
-mkNoImproveRedEnv doc try_me
- = RedEnv { red_doc = doc, red_try_me = try_me,
- red_givens = [],
- red_stack = (0,[]),
- red_improve = True }
-
-data WhatToDo
- = ReduceMe -- Try to reduce this
- -- If there's no instance, add the inst to the
- -- irreductible ones, but don't produce an error
- -- message of any kind.
- -- It might be quite legitimate such as (Eq a)!
-
- | Stop -- Return as irreducible unless it can
- -- be reduced to a constant in one step
- -- Do not add superclasses; see
-
-data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
- -- of a predicate when adding it to the avails
- -- The reason for this flag is entirely the super-class loop problem
- -- Note [SUPER-CLASS LOOP 1]
-
-zonkRedEnv :: RedEnv -> TcM RedEnv
-zonkRedEnv env
- = do { givens' <- mapM zonkInst (red_givens env)
- ; return $ env {red_givens = givens'}
- }
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection[reduce]{@reduce@}
-%* *
-%************************************************************************
-
-Note [Ancestor Equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-During context reduction, we add to the wanted equalities also those
-equalities that (transitively) occur in superclass contexts of wanted
-class constraints. Consider the following code
-
- class a ~ Int => C a
- instance C Int
-
-If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
-substituting Int for a. Hence, we ultimately want (C Int), which we
-discharge with the explicit instance.
-
-\begin{code}
-reduceContext :: RedEnv
- -> [Inst] -- Wanted
- -> TcM (ImprovementDone,
- TcTyVarBinds, -- Type variable bindings
- TcDictBinds, -- Dictionary bindings
- [Inst]) -- Irreducible
-
-reduceContext env wanteds0
- = do { traceTc (text "reduceContext" <+> (vcat [
- text "----------------------",
- red_doc env,
- text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds0,
- text "----------------------"
- ]))
-
- -- We want to add as wanted equalities those that (transitively)
- -- occur in superclass contexts of wanted class constraints.
- -- See Note [Ancestor Equalities]
- ; ancestor_eqs <- ancestorEqualities wanteds0
- ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
-
- -- Normalise and solve all equality constraints as far as possible
- -- and normalise all dictionary constraints wrt to the reduced
- -- equalities. The returned wanted constraints include the
- -- irreducible wanted equalities.
- ; let wanteds = wanteds0 ++ ancestor_eqs
- givens = red_givens env
- ; (givens',
- wanteds',
- tybinds,
- normalise_binds) <- tcReduceEqs givens wanteds
- ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
- [ppr givens', ppr wanteds', ppr tybinds,
- ppr normalise_binds]
-
- -- Build the Avail mapping from "given_dicts"
- ; (init_state, _) <- getLIE $ do
- { init_state <- foldlM addGiven emptyAvails givens'
- ; return init_state
- }
-
- -- Solve the *wanted* *dictionary* constraints (not implications)
- -- This may expose some further equational constraints in the course
- -- of improvement due to functional dependencies if any of the
- -- involved unifications gets deferred.
- ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
- ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
- -- The getLIE is reqd because reduceList does improvement
- -- (via extendAvails) which may in turn do unification
- ; (dict_binds,
- bound_dicts,
- dict_irreds) <- extractResults avails wanted_dicts
- ; traceTc $ text "reduceContext: extractResults" <+> vcat
- [ppr avails, ppr wanted_dicts, ppr dict_binds]
-
- -- Solve the wanted *implications*. In doing so, we can provide
- -- as "given" all the dicts that were originally given,
- -- *or* for which we now have bindings,
- -- *or* which are now irreds
- -- NB: Equality irreds need to be converted, as the recursive
- -- invocation of the solver will still treat them as wanteds
- -- otherwise.
- ; let implic_env = env { red_givens
- = givens ++ bound_dicts ++
- map wantedToLocalEqInst dict_irreds }
- ; (implic_binds_s, implic_irreds_s)
- <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
- ; let implic_binds = unionManyBags implic_binds_s
- implic_irreds = concat implic_irreds_s
-
- -- Collect all irreducible instances, and determine whether we should
- -- go round again. We do so in either of two cases:
- -- (1) If dictionary reduction or equality solving led to
- -- improvement (i.e., bindings for type variables).
- -- (2) If we reduced dictionaries (i.e., got dictionary bindings),
- -- they may have exposed further opportunities to normalise
- -- family applications. See Note [Dictionary Improvement]
- --
- -- NB: We do *not* go around for new extra_eqs. Morally, we should,
- -- but we can't without risking non-termination (see #2688). By
- -- not going around, we miss some legal programs mixing FDs and
- -- TFs, but we never claimed to support such programs in the
- -- current implementation anyway.
-
- ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
- avails_improved = availsImproved avails
- eq_improved = anyBag (not . isCoVarBind) tybinds
- improvedFlexible = avails_improved || eq_improved
- reduced_dicts = not (isEmptyBag dict_binds)
- improved = improvedFlexible || reduced_dicts
- --
- improvedHint = (if avails_improved then " [AVAILS]" else "") ++
- (if eq_improved then " [EQ]" else "")
-
- ; traceTc (text "reduceContext end" <+> (vcat [
- text "----------------------",
- red_doc env,
- text "given" <+> ppr givens,
- text "wanted" <+> ppr wanteds0,
- text "----",
- text "tybinds" <+> ppr tybinds,
- text "avails" <+> pprAvails avails,
- text "improved =" <+> ppr improved <+> text improvedHint,
- text "(all) irreds = " <+> ppr all_irreds,
- text "dict-binds = " <+> ppr dict_binds,
- text "implic-binds = " <+> ppr implic_binds,
- text "----------------------"
- ]))
-
- ; return (improved,
- tybinds,
- normalise_binds `unionBags` dict_binds
- `unionBags` implic_binds,
- all_irreds)
- }
- where
- isCoVarBind (TcTyVarBind tv _) = isCoVar tv
-
-tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
-tcImproveOne avails inst
- | not (isDict inst) = return False
- | otherwise
- = do { inst_envs <- tcGetInstEnvs
- ; let eqns = improveOne (classInstances inst_envs)
- (dictPred inst, pprInstArising inst)
- [ (dictPred p, pprInstArising p)
- | p <- availsInsts avails, isDict p ]
- -- Avails has all the superclasses etc (good)
- -- It also has all the intermediates of the deduction (good)
- -- It does not have duplicates (good)
- -- NB that (?x::t1) and (?x::t2) will be held separately in
- -- avails so that improve will see them separate
- ; traceTc (text "improveOne" <+> ppr inst)
- ; unifyEqns eqns }
-
-unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))]
- -> TcM ImprovementDone
-unifyEqns [] = return False
-unifyEqns eqns
- = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
- ; improved <- mapM unify eqns
- ; return $ or improved
- }
- where
- unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $
- do { let freeTyVars = unionVarSets (map tvs_pr pairs)
- `minusVarSet` qtvs
- ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
- ; mapM_ (unif_pr tenv) pairs
- ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
- }
-
- unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
-
- tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
-
-pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
-pprEquationDoc (eqn, (p1, _), (p2, _))
- = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
-
-mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
- -> TcM (TidyEnv, SDoc)
-mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
- = do { pred1' <- zonkTcPredType pred1
- ; pred2' <- zonkTcPredType pred2
- ; let { pred1'' = tidyPred tidy_env pred1'
- ; pred2'' = tidyPred tidy_env pred2' }
- ; 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}
-
-Note [Dictionary Improvement]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In reduceContext, we first reduce equalities and then class constraints.
-However, the letter may expose further opportunities for the former. Hence,
-we need to go around again if dictionary reduction produced any dictionary
-bindings. The following example demonstrated the point:
-
- data EX _x _y (p :: * -> *)
- data ANY
-
- class Base p
-
- class Base (Def p) => Prop p where
- type Def p
-
- instance Base ()
- instance Prop () where
- type Def () = ()
-
- instance (Base (Def (p ANY))) => Base (EX _x _y p)
- instance (Prop (p ANY)) => Prop (EX _x _y p) where
- type Def (EX _x _y p) = EX _x _y p
-
- data FOO x
- instance Prop (FOO x) where
- type Def (FOO x) = ()
-
- data BAR
- instance Prop BAR where
- type Def BAR = EX () () FOO
-
-During checking the last instance declaration, we need to check the superclass
-cosntraint Base (Def BAR), which family normalisation reduced to
-Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us
-Base (Def (FOO ANY)), which again requires family normalisation of Def to
-Base () before we can finish.
-
+ 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
+------------------------------------------------------------------------------------------
-The main context-reduction function is @reduce@. Here's its game plan.
\begin{code}
-reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
-reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
- = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
- ; dopts <- getDOpts
- ; when (debugIsOn && (n > 8)) $ do
- debugDumpTcRn (hang (ptext (sLit "Interesting! Context reduction stack depth") <+> int n)
- 2 (ifPprDebug (nest 2 (pprStack stk))))
- ; if n >= ctxtStkDepth dopts then
- failWithTc (reduceDepthErr n stk)
- else
- go wanteds state }
- where
- go [] state = return state
- go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
- ; go ws state' }
-
- -- Base case: we're done!
-reduce :: RedEnv -> Inst -> Avails -> TcM Avails
-reduce env wanted avails
-
- -- We don't reduce equalities here (and they must not end up as irreds
- -- in the Avails!)
- | isEqInst wanted
- = return avails
-
- -- It's the same as an existing inst, or a superclass thereof
- | Just _ <- findAvail avails wanted
- = do { traceTc (text "reduce: found " <+> ppr wanted)
- ; return avails
- }
-
+applyDefaultingRules :: InertSet
+ -> CanonicalCts -- All wanteds
+ -> TcS CanonicalCts
+-- Return some *extra* givens, which express the
+-- type-class-default choice
+
+applyDefaultingRules inert wanteds
+ | isEmptyBag wanteds
+ = return emptyBag
| otherwise
- = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
- ; case red_try_me env wanted of {
- Stop -> try_simple (addIrred NoSCs);
- -- See Note [No superclasses for Stop]
-
- ReduceMe -> do -- It should be reduced
- { (avails, lookup_result) <- reduceInst env avails wanted
- ; case lookup_result of
- NoInstance -> addIrred AddSCs avails wanted
- -- Add it and its superclasses
-
- GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
-
- GenInst wanteds' rhs
- -> do { avails1 <- addIrred NoSCs avails wanted
- ; avails2 <- reduceList env wanteds' avails1
- ; addWanted AddSCs avails2 wanted rhs wanteds' } }
- -- Temporarily do addIrred *before* the reduceList,
- -- which has the effect of adding the thing we are trying
- -- to prove to the database before trying to prove the things it
- -- needs. See note [RECURSIVE DICTIONARIES]
- -- NB: we must not do an addWanted before, because that adds the
- -- superclasses too, and that can lead to a spurious loop; see
- -- the examples in [SUPERCLASS-LOOP]
- -- So we do an addIrred before, and then overwrite it afterwards with addWanted
- } }
- where
- -- First, see if the inst can be reduced to a constant in one step
- -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
- -- Don't bother for implication constraints, which take real work
- try_simple do_this_otherwise
- = do { res <- lookupSimpleInst wanted
- ; case res of
- GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
- _ -> do_this_otherwise avails wanted }
-\end{code}
-
-
-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.
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We need to be careful when adding "the constaint we are trying to prove".
-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 Stop
-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.
-
-
-
-%************************************************************************
-%* *
- Reducing a single constraint
-%* *
-%************************************************************************
-
-\begin{code}
----------------------------------------------
-reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst _ avails other_inst
- = do { result <- lookupSimpleInst other_inst
- ; return (avails, result) }
-\end{code}
-
-Note [Equational Constraints in Implication Constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-An implication constraint is of the form
- Given => Wanted
-where Given and Wanted may contain both equational and dictionary
-constraints. The delay and reduction of these two kinds of constraints
-is distinct:
-
--) In the generated code, wanted Dictionary constraints are wrapped up in an
- implication constraint that is created at the code site where the wanted
- dictionaries can be reduced via a let-binding. This let-bound implication
- constraint is deconstructed at the use-site of the wanted dictionaries.
-
--) While the reduction of equational constraints is also delayed, the delay
- is not manifest in the generated code. The required evidence is generated
- in the code directly at the use-site. There is no let-binding and deconstruction
- necessary. The main disadvantage is that we cannot exploit sharing as the
- same evidence may be generated at multiple use-sites. However, this disadvantage
- is limited because it only concerns coercions which are erased.
-
-The different treatment is motivated by the different in representation. Dictionary
-constraints require manifest runtime dictionaries, while equations require coercions
-which are types.
-
-\begin{code}
----------------------------------------------
-reduceImplication :: RedEnv
- -> Inst
- -> TcM (TcDictBinds, [Inst])
-\end{code}
-
-Suppose we are simplifying the constraint
- forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens'.
-
-Note that
- * The 'givens' need not mention any of the quantified type variables
- e.g. forall {}. Eq a => Eq [a]
- forall {}. C Int => D (Tree Int)
-
- This happens when you have something like
- data T a where
- T1 :: Eq a => a -> T a
-
- f :: T a -> Int
- f x = ...(case x of { T1 v -> v==v })...
-
-\begin{code}
- -- ToDo: should we instantiate tvs? I think it's not necessary
- --
- -- Note on coercion variables:
- --
- -- The extra given coercion variables are bound at two different
- -- sites:
- --
- -- -) in the creation context of the implication constraint
- -- the solved equational constraints use these binders
- --
- -- -) at the solving site of the implication constraint
- -- the solved dictionaries use these binders;
- -- these binders are generated by reduceImplication
- --
- -- Note [Binders for equalities]
- -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- -- To reuse the binders of local/given equalities in the binders of
- -- implication constraints, it is crucial that these given equalities
- -- always have the form
- -- cotv :: t1 ~ t2
- -- where cotv is a simple coercion type variable (and not a more
- -- complex coercion term). We require that the extra_givens always
- -- have this form and exploit the special form when generating binders.
-reduceImplication env
- orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
- tci_tyvars = tvs,
- tci_given = extra_givens, tci_wanted = wanteds
- })
- = do { -- Solve the sub-problem
- ; let try_me _ = ReduceMe -- Note [Freeness and implications]
- env' = env { red_givens = extra_givens ++ red_givens env
- , red_doc = sep [ptext (sLit "reduceImplication for")
- <+> ppr name,
- nest 2 (parens $ ptext (sLit "within")
- <+> red_doc env)]
- , red_try_me = try_me }
-
- ; traceTc (text "reduceImplication" <+> vcat
- [ ppr (red_givens env), ppr extra_givens,
- ppr wanteds])
- ; (irreds, binds) <- checkLoop env' wanteds
-
- ; traceTc (text "reduceImplication result" <+> vcat
- [ppr irreds, ppr binds])
-
- ; -- extract superclass binds
- -- (sc_binds,_) <- extractResults avails []
--- ; traceTc (text "reduceImplication sc_binds" <+> vcat
--- [ppr sc_binds, ppr avails])
---
-
- -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
- -- Then we must iterate the outer loop too!
-
- ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
- -- we solve wanted eqs by side effect!
-
- -- Progress is no longer measered by the number of bindings
- -- If there are any irreds, but no bindings and no solved
- -- equalities, we back off and do nothing
- ; let backOff = isEmptyLHsBinds binds && -- no new bindings
- (not $ null irreds) && -- but still some irreds
- didntSolveWantedEqs -- no instantiated cotv
-
- ; if backOff then -- No progress
- return (emptyBag, [orig_implic])
- else do
- { (simpler_implic_insts, bind)
- <- makeImplicationBind inst_loc tvs extra_givens irreds
- -- This binding is useless if the recursive simplification
- -- made no progress; but currently we don't try to optimise that
- -- case. After all, we only try hard to reduce at top level, or
- -- when inferring types.
-
- ; let -- extract Id binders for dicts and CoTyVar binders for eqs;
- -- see Note [Binders for equalities]
- (extra_eq_givens, extra_dict_givens) = partition isEqInst
- extra_givens
- eq_cotvs = map instToVar extra_eq_givens
- dict_ids = map instToId extra_dict_givens
-
- -- Note [Always inline implication constraints]
- wrap_inline | null dict_ids = idHsWrapper
- | otherwise = WpInline
- co = wrap_inline
- <.> mkWpTyLams tvs
- <.> mkWpTyLams eq_cotvs
- <.> mkWpLams dict_ids
- <.> WpLet (binds `unionBags` bind)
- rhs = mkLHsWrap co payload
- loc = instLocSpan inst_loc
- -- wanted equalities are solved by updating their
- -- cotv; we don't generate bindings for them
- dict_bndrs = map (L loc . HsVar . instToId)
- . filter (not . isEqInst)
- $ wanteds
- payload = mkBigLHsTup dict_bndrs
-
-
- ; traceTc (vcat [text "reduceImplication" <+> ppr name,
- ppr simpler_implic_insts,
- text "->" <+> ppr rhs])
- ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),
- simpler_implic_insts)
- }
- }
-reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
-\end{code}
-
-Note [Always inline implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose an implication constraint floats out of an INLINE function.
-Then although the implication has a single call site, it won't be
-inlined. And that is bad because it means that even if there is really
-*no* overloading (type signatures specify the exact types) there will
-still be dictionary passing in the resulting code. To avert this,
-we mark the implication constraints themselves as INLINE, at least when
-there is no loss of sharing as a result.
-
-Note [Freeness and implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's hard to say when an implication constraint can be floated out. Consider
- forall {} Eq a => Foo [a]
-The (Foo [a]) doesn't mention any of the quantified variables, but it
-still might be partially satisfied by the (Eq a).
-
-There is a useful special case when it *is* easy to partition the
-constraints, namely when there are no 'givens'. Consider
- forall {a}. () => Bar b
-There are no 'givens', and so there is no reason to capture (Bar b).
-We can let it float out. But if there is even one constraint we
-must be much more careful:
- forall {a}. C a b => Bar (m b)
-because (C a b) might have a superclass (D b), from which we might
-deduce (Bar [b]) when m later gets instantiated to []. Ha!
-
-Here is an even more exotic example
- class C a => D a b
-Now consider the constraint
- forall b. D Int b => C Int
-We can satisfy the (C Int) from the superclass of D, so we don't want
-to float the (C Int) out, even though it mentions no type variable in
-the constraints!
-
-One more example: the constraint
- class C a => D a b
- instance (C a, E c) => E (a,c)
-
- constraint: forall b. D Int b => E (Int,c)
-
-You might think that the (D Int b) can't possibly contribute
-to solving (E (Int,c)), since the latter mentions 'c'. But
-in fact it can, because solving the (E (Int,c)) constraint needs
-dictionaries
- C Int, E c
-and the (C Int) can be satisfied from the superclass of (D Int b).
-So we must still not float (E (Int,c)) out.
-
-To think about: special cases for unary type classes?
-
-Note [Pruning the givens in an implication constraint]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are about to form the implication constraint
- forall tvs. Eq a => Ord b
-The (Eq a) cannot contribute to the (Ord b), because it has no access to
-the type variable 'b'. So we could filter out the (Eq a) from the givens.
-But BE CAREFUL of the examples above in [Freeness and implications].
-
-Doing so would be a bit tidier, but all the implication constraints get
-simplified away by the optimiser, so it's no great win. So I don't take
-advantage of that at the moment.
-
-If you do, BE CAREFUL of wobbly type variables.
-
-
-%************************************************************************
-%* *
- Avails and AvailHow: the pool of evidence
-%* *
-%************************************************************************
-
-
-\begin{code}
-data Avails = Avails !ImprovementDone !AvailEnv
-
-type ImprovementDone = Bool -- True <=> some unification has happened
- -- so some Irreds might now be reducible
- -- keys that are now
-
-type AvailEnv = FiniteMap Inst AvailHow
-data AvailHow
- = IsIrred -- Used for irreducible dictionaries,
- -- which are going to be lambda bound
-
- | Given Inst -- Used for dictionaries for which we have a binding
- -- e.g. those "given" in a signature
-
- | Rhs -- Used when there is a RHS
- (LHsExpr TcId) -- The RHS
- [Inst] -- Insts free in the RHS; we need these too
-
-instance Outputable Avails where
- ppr = pprAvails
-
-pprAvails :: Avails -> SDoc
-pprAvails (Avails imp avails)
- = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
- , nest 2 $ braces $
- vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
- | (inst,avail) <- fmToList avails ]]
-
-instance Outputable AvailHow where
- ppr = pprAvail
-
--------------------------
-pprAvail :: AvailHow -> SDoc
-pprAvail IsIrred = text "Irred"
-pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
- nest 2 (ppr rhs)]
-
--------------------------
-extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
-extendAvailEnv env inst avail = addToFM env inst avail
-
-findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
-findAvailEnv env wanted = lookupFM env wanted
- -- NB 1: the Ord instance of Inst compares by the class/type info
- -- *not* by unique. So
- -- d1::C Int == d2::C Int
-
-emptyAvails :: Avails
-emptyAvails = Avails False emptyFM
-
-findAvail :: Avails -> Inst -> Maybe AvailHow
-findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
-
-elemAvails :: Inst -> Avails -> Bool
-elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
-
-extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
--- Does improvement
-extendAvails avails@(Avails imp env) inst avail
- = do { imp1 <- tcImproveOne avails inst -- Do any improvement
- ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
-
-availsInsts :: Avails -> [Inst]
-availsInsts (Avails _ avails) = keysFM avails
-
-availsImproved :: Avails -> ImprovementDone
-availsImproved (Avails imp _) = imp
-\end{code}
-
-Extracting the bindings from a bunch of Avails.
-The bindings do *not* come back sorted in dependency order.
-We assume that they'll be wrapped in a big Rec, so that the
-dependency analyser can sort them out later
-
-\begin{code}
-type DoneEnv = FiniteMap Inst [Id]
--- Tracks which things we have evidence for
-
-extractResults :: Avails
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds, -- Bindings
- [Inst], -- The insts bound by the bindings
- [Inst]) -- Irreducible ones
- -- Note [Reducing implication constraints]
-
-extractResults (Avails _ avails) wanteds
- = go emptyBag [] [] emptyFM wanteds
- where
- go :: TcDictBinds -- Bindings for dicts
- -> [Inst] -- Bound by the bindings
- -> [Inst] -- Irreds
- -> DoneEnv -- Has an entry for each inst in the above three sets
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds, [Inst], [Inst])
- go binds bound_dicts irreds _ []
- = return (binds, bound_dicts, irreds)
-
- go binds bound_dicts irreds done (w:ws)
- | isEqInst w
- = go binds bound_dicts (w:irreds) done' ws
-
- | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
- = if w_id `elem` done_ids then
- go binds bound_dicts irreds done ws
- else
- go (add_bind (nlHsVar done_id)) bound_dicts irreds
- (addToFM done w (done_id : w_id : rest_done_ids)) ws
-
- | otherwise -- Not yet done
- = case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go binds bound_dicts irreds done ws
-
- Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
-
- Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
-
- Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws
- where
- g_id = instToId g
- binds' | w_id == g_id = binds
- | otherwise = add_bind (nlHsVar g_id)
- where
- w_id = instToId w
- done' = addToFM done w [w_id]
- add_bind rhs = addInstToDictBind binds w rhs
-\end{code}
-
-
-Note [No superclasses for Stop]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
-add it to avails, so that any other equal Insts will be commoned up
-right here. However, we do *not* add superclasses. If we have
- df::Floating a
- dn::Num a
-but a is not bound here, then we *don't* want to derive dn from df
-here lest we lose sharing.
-
-\begin{code}
-addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted want_scs avails wanted rhs_expr wanteds
- = addAvailAndSCs want_scs avails wanted avail
- where
- avail = Rhs rhs_expr wanteds
-
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given
- = addAvailAndSCs want_scs avails given (Given given)
- where
- want_scs = case instLocOrigin (instLoc given) of
- NoScOrigin -> NoSCs
- _other -> AddSCs
- -- Conditionally add superclasses for 'given'
- -- See Note [Recursive instances and superclases]
-
- -- No ASSERT( not (given `elemAvails` avails) ) because in an
- -- instance decl for Ord t we can add both Ord t and Eq t as
- -- 'givens', so the assert isn't true
-\end{code}
-
-\begin{code}
-addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
-addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
- addAvailAndSCs want_scs avails irred IsIrred
-
-addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
-addAvailAndSCs want_scs avails inst avail
- | not (isClassDict inst) = extendAvails avails inst avail
- | NoSCs <- want_scs = extendAvails avails inst avail
- | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
- ; avails' <- extendAvails avails inst avail
- ; addSCs is_loop avails' inst }
- where
- is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
- -- Note: this compares by *type*, not by Unique
- deps = findAllDeps (unitVarSet (instToVar inst)) avail
- dep_tys = map idType (varSetElems deps)
-
- findAllDeps :: IdSet -> AvailHow -> IdSet
- -- Find all the Insts that this one depends on
- -- See Note [SUPERCLASS-LOOP 2]
- -- Watch out, though. Since the avails may contain loops
- -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
- findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
- findAllDeps so_far _ = so_far
-
- find_all :: IdSet -> Inst -> IdSet
- find_all so_far kid
- | isEqInst kid = so_far
- | kid_id `elemVarSet` so_far = so_far
- | Just avail <- findAvail avails kid = findAllDeps so_far' avail
- | otherwise = so_far'
- where
- so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
- kid_id = instToId kid
-
-addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
- -- Add all the superclasses of the Inst to Avails
- -- The first param says "don't do this because the original thing
- -- depends on this one, so you'd build a loop"
- -- Invariant: the Inst is already in Avails.
-
-addSCs is_loop avails dict
- = ASSERT( isDict dict )
- do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
- ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
- where
- (clas, tys) = getDictClassTys dict
- (tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = filter (not . isEqPred) $
- substTheta (zipTopTvSubst tyvars tys) sc_theta
-
- add_sc avails (sc_dict, sc_sel)
- | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
- | is_given sc_dict = return avails
- | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
- ; addSCs is_loop avails' sc_dict }
- where
- sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
- co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys
-
- is_given :: Inst -> Bool
- is_given sc_dict = case findAvail avails sc_dict of
- Just (Given _) -> True -- Given is cheaper than superclass selection
- _ -> False
-
--- From the a set of insts obtain all equalities that (transitively) occur in
--- superclass contexts of class constraints (aka the ancestor equalities).
+ = do { untch <- getUntouchablesTcS
+ ; tv_cts <- mapM (defaultTyVar untch) $
+ varSetElems (tyVarsOfCanonicals wanteds)
+
+ ; info@(_, default_tys, _) <- getDefaultInfo
+ ; let groups = findDefaultableGroups info untch wanteds
+ ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
+
+ ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
+ , text "Type defaults =" <+> ppr deflt_cts])
+
+ ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
+
+------------------
+defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
+-- 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.
--
-ancestorEqualities :: [Inst] -> TcM [Inst]
-ancestorEqualities
- = mapM mkWantedEqInst -- turn only equality predicates..
- . filter isEqPred -- ..into wanted equality insts
- . bagToList
- . addAEsToBag emptyBag -- collect the superclass constraints..
- . map dictPred -- ..of all predicates in a bag
- . filter isClassDict
+-- 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
+ | isMetaTyVar the_tv
+ , not (the_tv `elemVarSet` untch)
+ , not (k `eqKind` default_k)
+ = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
+ ; let loc = CtLoc TypeEqOrigin (getSrcSpan the_tv) [] -- Yuk
+ wanted_eq = CTyEqCan { cc_id = ev
+ , cc_flavor = Wanted loc
+ , cc_tyvar = the_tv
+ , cc_rhs = better_ty }
+ ; return (unitBag wanted_eq) }
+
+ | otherwise
+ = return emptyCCan -- The common case
where
- addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
- addAEsToBag bag [] = bag
- addAEsToBag bag (pred:preds)
- | pred `elemBag` bag = addAEsToBag bag preds
- | isEqPred pred = addAEsToBag bagWithPred preds
- | isClassPred pred = addAEsToBag bagWithPred predsWithSCs
- | otherwise = addAEsToBag bag preds
- where
- bagWithPred = bag `snocBag` pred
- predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
- --
- (tyvars, sc_theta, _, _) = classBigSig clas
- (clas, tys) = getClassPredTys pred
-\end{code}
-
-
-%************************************************************************
-%* *
-\section{tcSimplifyTop: defaulting}
-%* *
-%************************************************************************
-
-
-@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
- = tc_simplify_top doc False wanteds
- where
- doc = text "tcSimplifyTop"
-
-tcSimplifyInteractive wanteds
- = tc_simplify_top doc True wanteds
+ k = tyVarKind the_tv
+ default_k = defaultKind k
+
+
+----------------
+findDefaultableGroups
+ :: ( SimplContext
+ , [Type]
+ , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
+ -> TcTyVarSet -- 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 "tcSimplifyInteractive"
-
--- The TcLclEnv should be valid here, solely to improve
--- error message generation for the monomorphism restriction
-tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))
-tc_simplify_top doc interactive wanteds
- = do { dflags <- getDOpts
- ; wanteds <- zonkInsts wanteds
- ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
-
- ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
- ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
--- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
- ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
- ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
- ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
-
- -- Use the defaulting rules to do extra unification
- -- NB: irreds2 are already zonked
- ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
-
- -- Deal with implicit parameters
- ; let (bad_ips, non_ips) = partition isIPDict irreds3
- (ambigs, others) = partition isTyVarDict non_ips
-
- ; topIPErrs bad_ips -- Can arise from f :: Int -> Int
- -- f x = x + ?y
- ; addNoInstanceErrs others
- ; addTopAmbigErrs ambigs
-
- ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
- where
- doc1 = doc <+> ptext (sLit "(first round)")
- doc2 = doc <+> ptext (sLit "(approximate)")
- doc3 = doc <+> ptext (sLit "(disambiguate)")
-\end{code}
-
-If a dictionary constrains a type variable which is
- * 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}
-disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
- -- Just does unification to fix the default types
- -- The Insts are assumed to be pre-zonked
-disambiguate doc interactive dflags insts
- | null insts
- = return (insts, emptyBag)
-
- | null defaultable_groups
- = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
- ; return (insts, emptyBag) }
-
- | otherwise
- = do { -- Figure out what default types to use
- default_tys <- getDefaultTys extended_defaulting ovl_strings
-
- ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
- ; mapM_ (disambigGroup default_tys) defaultable_groups
-
- -- disambigGroup does unification, hence try again
- ; tryHardCheckLoop doc insts }
-
- where
- extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
- -- See also Trac #1974
- ovl_strings = dopt Opt_OverloadedStrings dflags
-
- unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
- bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
- (unaries, bad_tvs_s) = partitionWith find_unary insts
- bad_tvs = unionVarSets bad_tvs_s
-
- -- Finds unary type-class constraints
- find_unary d@(Dict {tci_pred = ClassP cls [ty]})
- | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
- find_unary inst = Right (tyVarsOfInst inst)
-
- -- Group by type variable
- defaultable_groups :: [[(Inst,Class,TcTyVar)]]
- defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
- cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
-
- defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
- defaultable_group ds@((_,_,tv):_)
- = isTyConableTyVar tv -- Note [Avoiding spurious errors]
- && not (tv `elemVarSet` bad_tvs)
- && defaultable_classes [c | (_,c,_) <- ds]
- defaultable_group [] = panic "defaultable_group"
-
- defaultable_classes clss
- | extended_defaulting = any isInteractiveClass clss
- | otherwise = all is_std_class clss && (any is_num_class clss)
-
- -- In interactive mode, or with -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
- -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
- -> TcM () -- Just does unification, to fix the default types
-
-disambigGroup default_tys dicts
- = do { mb_chosen_ty <- try_default default_tys
- ; case mb_chosen_ty of
- Nothing -> return ()
- Just chosen_ty -> do { _ <- unifyType chosen_ty (mkTyVarTy tyvar)
- ; warnDefault dicts chosen_ty } }
- where
- (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty
- classes = [c | (_,c,_) <- dicts]
-
- try_default [] = return Nothing
- try_default (default_ty : default_tys)
- = tryTcLIE_ (try_default default_tys) $
- do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
- -- This may fail; then the tryTcLIE_ kicks in
- -- Failure here is caused by there being no type in the
- -- default list which can satisfy all the ambiguous classes.
- -- For example, if Real a is reqd, but the only type in the
- -- default list is Int.
-
- ; return (Just default_ty) -- TOMDO: do something with the coercion
- }
-
-
------------------------
-getDefaultTys :: Bool -> Bool -> TcM [Type]
-getDefaultTys extended_deflts ovl_strings
- = do { mb_defaults <- getDeclaredDefaultTys
- ; case mb_defaults of {
- Just tys -> return tys ; -- User-supplied defaults
- Nothing -> do
-
- -- No use-supplied default
- -- Use [Integer, Double], plus modifications
- { integer_ty <- tcMetaTy integerTyConName
- ; checkWiredInTyCon doubleTyCon
- ; string_ty <- tcMetaTy stringTyConName
- ; return (opt_deflt extended_deflts unitTy
- -- Note [Default unitTy]
- ++
- [integer_ty,doubleTy]
- ++
- opt_deflt ovl_strings string_ty) } } }
+ unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
+ non_unaries :: [CanonicalCt] -- *other* constraints
+
+ (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)
+ && not (tv `elemVarSet` untch) -- Non untouchable
+ && 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
+ -> TcTyVarSet -- Untouchables
+ -> InertSet -- Given inert
+ -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
+ -- sharing same type variable
+ -> TcS CanonicalCts
+
+disambigGroup [] _inert _untch _grp
+ = return emptyBag
+disambigGroup (default_ty:default_tys) untch inert group
+ = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
+ ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
+ -- We know this equality is canonical,
+ -- so we directly construct it as such
+ ; let given_eq = CTyEqCan { cc_id = ev
+ , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
+ , cc_tyvar = the_tv
+ , cc_rhs = default_ty }
+
+ ; success <- tryTcS (extendVarSet untch the_tv) $
+ do { given_inert <- solveOne inert given_eq
+ ; final_inert <- solveInteract given_inert (listToBag wanteds)
+ ; let (_, unsolved) = extractUnsolved final_inert
+ ; return (isEmptyBag unsolved) }
+
+ ; case success of
+ True -> -- Success: record the type variable binding, and return
+ do { setWantedTyBind the_tv default_ty
+ ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
+ ; traceTcS "disambigGoup succeeded" (ppr default_ty)
+ ; return (unitBag given_eq) }
+ False -> -- Failure: try with the next type
+ do { traceTcS "disambigGoup succeeded" (ppr default_ty)
+ ; disambigGroup default_tys untch inert group } }
where
- opt_deflt True ty = [ty]
- opt_deflt False _ = []
+ ((the_ct,the_tv):_) = group
+ wanteds = map fst group
+ wanted_ev_vars = map deCanonicaliseWanted wanteds
\end{code}
-Note [Default unitTy]
-~~~~~~~~~~~~~~~~~~~~~
-In interative mode (or with -XExtendedDefaultRules) we add () as the first type we
-try when defaulting. This has very little real impact, except in the following case.
-Consider:
- Text.Printf.printf "hello"
-This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
-want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
-default the 'a' to (), rather than to Integer (which is what would otherwise happen;
-and then GHCi doesn't attempt to print the (). So in interactive mode, we add
-() to the list of defaulting types. See Trac #1200.
-
Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
already been unified with the rigid variable from g's type sig
-%************************************************************************
-%* *
-\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}
-tcSimplifyDeriv :: InstOrigin
- -> [TyVar]
- -> ThetaType -- Wanted
- -> TcM ThetaType -- Needed
--- Given instance (wanted) => C inst_ty
--- Simplify 'wanted' as much as possible
-
-tcSimplifyDeriv orig tyvars theta
- = do { (tvs, _, tenv) <- tcInstTyVars tyvars
- -- The main loop may do unification, and that may crash if
- -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
- -- ToDo: what if two of them do get unified?
- ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
- ; (irreds, _) <- tryHardCheckLoop doc wanteds
-
- ; let (tv_dicts, others) = partition ok irreds
- (tidy_env, tidy_insts) = tidyInsts others
- ; reportNoInstances tidy_env Nothing [alt_fix] tidy_insts
- -- See Note [Exotic derived instance contexts] in TcMType
-
- ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
- simpl_theta = substTheta rev_env (map dictPred tv_dicts)
- -- This reverse-mapping is a pain, but the result
- -- should mention the original TyVars not TcTyVars
-
- ; return simpl_theta }
- where
- doc = ptext (sLit "deriving classes for a data type")
-
- ok dict | isDict dict = validDerivPred (dictPred dict)
- | otherwise = False
- alt_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration instead,"),
- ptext (sLit "so you can specify the instance context yourself")]
-\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 = do
- wanteds <- newDictBndrsO DefaultOrigin theta
- (irreds, _) <- tryHardCheckLoop doc wanteds
- addNoInstanceErrs irreds
- if null irreds then
- return ()
- else
- traceTc (ptext (sLit "tcSimplifyDefault failing")) >> failM
- where
- doc = ptext (sLit "default declaration")
-\end{code}
-
-@tcSimplifyStagedExpr@ performs a simplification but does so at a new
-stage. This is used when typechecking annotations and splices.
-
-\begin{code}
-
-tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds)
--- Type check an expression that runs at a top level stage as if
--- it were going to be spliced and then simplify it
-tcSimplifyStagedExpr stage tc_action
- = setStage stage $ do {
- -- Typecheck the expression
- (thing', lie) <- getLIE tc_action
-
- -- Solve the constraints
- ; const_binds <- tcSimplifyTop lie
-
- ; return (thing', const_binds) }
-
-\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 _ []
- = return ()
-groupErrs report_err (inst:insts)
- = do { do_one (inst:friends)
- ; groupErrs report_err others }
- where
- -- (It may seem a bit crude to compare the error messages,
- -- but it makes sure that we combine just what the user sees,
- -- 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 (pprInstArising (head insts))
-
-addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs _ []
- = return ()
-addTopIPErrs bndrs ips
- = do { dflags <- getDOpts
- ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
- where
- (tidy_env, tidy_ips) = tidyInsts ips
- mk_msg dflags ips
- = vcat [sep [ptext (sLit "Implicit parameters escape from"),
- nest 2 (ptext (sLit "the monomorphic top-level binding")
- <> plural bndrs <+> ptext (sLit "of")
- <+> pprBinders bndrs <> colon)],
- nest 2 (vcat (map ppr_ip ips)),
- monomorphism_fix dflags]
- ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
-
-topIPErrs :: [Inst] -> TcM ()
-topIPErrs dicts
- = 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 :: [Inst] -- Wanted (can include implications)
- -> TcM ()
-addNoInstanceErrs insts
- = do { let (tidy_env, tidy_insts) = tidyInsts insts
- ; reportNoInstances tidy_env Nothing [] tidy_insts }
-
-reportNoInstances
- :: TidyEnv
- -> Maybe (InstLoc, [Inst]) -- Context
- -- Nothing => top level
- -- Just (d,g) => d describes the construct
- -- with givens g
- -> [SDoc] -- Alternative fix for no-such-instance
- -> [Inst] -- What is wanted (can include implications)
- -> TcM ()
-
-reportNoInstances tidy_env mb_what alt_fix insts
- = groupErrs (report_no_instances tidy_env mb_what alt_fix) insts
-
-report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [SDoc] -> [Inst] -> TcM ()
-report_no_instances tidy_env mb_what alt_fixes insts
- = do { inst_envs <- tcGetInstEnvs
- ; let (implics, insts1) = partition isImplicInst insts
- (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
- (eqInsts, insts3) = partition isEqInst insts2
- ; traceTc (text "reportNoInstances" <+> vcat
- [ppr insts, ppr implics, ppr insts1, ppr insts2])
- ; mapM_ complain_implic implics
- ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
- ; groupErrs complain_no_inst insts3
- ; mapM_ (addErrTcM . mk_eq_err) eqInsts
- }
- where
- complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
-
- complain_implic inst -- Recurse!
- = reportNoInstances tidy_env
- (Just (tci_loc inst, tci_given inst))
- alt_fixes (tci_wanted inst)
-
- check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
- -- Right msg => overlap message
- -- Left inst => no instance
- check_overlap inst_envs wanted
- | not (isClassDict wanted) = Left wanted
- | otherwise
- = case lookupInstEnv inst_envs clas tys of
- ([], _) -> Left wanted -- No match
- -- The case of exactly one match and no unifiers means a
- -- successful lookup. That can't happen here, because dicts
- -- only end up here if they didn't match in Inst.lookupInst
- ([_],[])
- | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
- res -> Right (mk_overlap_msg wanted res)
- where
- (clas,tys) = getDictClassTys wanted
-
- mk_overlap_msg dict (matches, unifiers)
- = ASSERT( not (null matches) )
- vcat [ addInstLoc [dict] ((ptext (sLit "Overlapping instances for")
- <+> pprPred (dictPred dict))),
- sep [ptext (sLit "Matching instances") <> colon,
- nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
- 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 "To pick the first instance above, use -XIncoherentInstances"),
- ptext (sLit "when compiling the other instance declarations")])]
- where
- ispecs = [ispec | (ispec, _) <- matches]
-
- mk_eq_err :: Inst -> (TidyEnv, SDoc)
- mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
-
- mk_no_inst_err insts
- | null insts = empty
-
- | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
- not (isEmptyVarSet (tyVarsOfInsts insts))
- = vcat [ addInstLoc insts $
- sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
- , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
- , show_fixes (fix1 loc : fixes2 ++ alt_fixes) ]
-
- | otherwise -- Top level
- = vcat [ addInstLoc insts $
- ptext (sLit "No instance") <> plural insts
- <+> ptext (sLit "for") <+> pprDictsTheta insts
- , show_fixes (fixes2 ++ alt_fixes) ]
-
- where
- fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
- <+> ptext (sLit "to the context of"),
- nest 2 (ppr (instLocOrigin loc)) ]
- -- I'm not sure it helps to add the location
- -- nest 2 (ptext (sLit "at") <+> ppr (instLocSpan loc)) ]
-
- fixes2 | null instance_dicts = []
- | otherwise = [sep [ptext (sLit "add an instance declaration for"),
- pprDictsTheta instance_dicts]]
- instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
- -- Insts for which it is worth suggesting an adding an instance declaration
- -- Exclude implicit parameters, and tyvar dicts
-
- show_fixes :: [SDoc] -> SDoc
- show_fixes [] = empty
- show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"),
- nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
-
-addTopAmbigErrs :: [Inst] -> TcRn ()
-addTopAmbigErrs dicts
--- Divide into groups that share a common set of ambiguous tyvars
- = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened
- -- See Note [Avoiding spurious errors]
- mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
- where
- (tidy_env, tidy_dicts) = tidyInsts dicts
-
- tvs_of :: Inst -> [TcTyVar]
- tvs_of d = varSetElems (tyVarsOfInst d)
- cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
-
- report :: [(Inst,[TcTyVar])] -> TcM ()
- report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars
- (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
- setSrcSpan (instSpan 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
- report [] = panic "addTopAmbigErrs"
-
-
-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
- = do { dflags <- getDOpts
- ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
- ; return (tidy_env, mk_msg dflags docs) }
- where
- mk_msg _ _ | any isRuntimeUnk inst_tvs
- = vcat [ptext (sLit "Cannot resolve unknown runtime types:") <+>
- (pprWithCommas ppr inst_tvs),
- ptext (sLit "Use :print or :force to determine these types")]
- mk_msg _ [] = ptext (sLit "Probable fix: add a type signature that fixes these type variable(s)")
- -- This happens in things like
- -- f x = show (read "foo")
- -- where monomorphism doesn't play any role
- mk_msg dflags docs
- = vcat [ptext (sLit "Possible cause: the monomorphism restriction applied to the following:"),
- nest 2 (vcat docs),
- monomorphism_fix dflags]
-
-monomorphism_fix :: DynFlags -> SDoc
-monomorphism_fix dflags
- = ptext (sLit "Probable fix:") <+> vcat
- [ptext (sLit "give these definition(s) an explicit type signature"),
- if dopt Opt_MonomorphismRestriction dflags
- then ptext (sLit "or use -XNoMonomorphismRestriction")
- else empty] -- Only suggest adding "-XNoMonomorphismRestriction"
- -- if it is not already set!
-
-warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()
-warnDefault ups default_ty = do
- warn_flag <- doptM Opt_WarnTypeDefaults
- addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
- where
- dicts = [d | (d,_,_) <- ups]
-
- -- Tidy them first
- (_, tidy_dicts) = tidyInsts dicts
- warn_msg = vcat [ptext (sLit "Defaulting the following constraint(s) to type") <+>
- quotes (ppr default_ty),
- pprDictsInFull tidy_dicts]
-
-reduceDepthErr :: Int -> [Inst] -> SDoc
-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 :: [Inst] -> SDoc
-pprStack stack = vcat (map pprInstInFull stack)
-\end{code}
projects / ghc-hetmet.git / blobdiff