-%
-% (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
- ) 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 Inst
-import TcEnv
-import InstEnv
-import TcGadt
+import TcErrors
+import TcCanonical
import TcMType
-import TcType
-import TcIface
+import TcType
+import TcSMonad
+import TcInteract
+import Inst
import Var
-import TyCon
-import Name
-import NameSet
-import Class
-import FunDeps
-import PrelInfo
-import PrelNames
-import Type
-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 Data.List
+import PrelInfo
+import PrelNames
+import Class ( classKey )
+import BasicTypes ( RuleName )
+import Data.List ( partition )
+import Outputable
+import FastString
\end{code}
-%************************************************************************
-%* *
-\subsection{NOTES}
-%* *
-%************************************************************************
-
- --------------------------------------
- Notes on functional dependencies (a bug)
- --------------------------------------
-
-Consider this:
-
- class C a b | a -> b
- class D a b | a -> b
-
- instance D a b => C a b -- Undecidable
- -- (Not sure if it's crucial to this eg)
- f :: C a b => a -> Bool
- f _ = True
-
- g :: C a b => a -> Bool
- g = f
-
-Here f typechecks, but g does not!! Reason: before doing improvement,
-we reduce the (C a b1) constraint from the call of f to (D a b1).
-
-Here is a more complicated example:
-
-| > class Foo a b | a->b
-| >
-| > class Bar a b | a->b
-| >
-| > data Obj = Obj
-| >
-| > instance Bar Obj Obj
-| >
-| > instance (Bar a b) => Foo a b
-| >
-| > foo:: (Foo a b) => a -> String
-| > foo _ = "works"
-| >
-| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
-| > runFoo f = f Obj
-|
-| *Test> runFoo foo
-|
-| <interactive>:1:
-| Could not deduce (Bar a b) from the context (Foo a b)
-| arising from use of `foo' at <interactive>:1
-| Probable fix:
-| Add (Bar a b) to the expected type of an expression
-| In the first argument of `runFoo', namely `foo'
-| In the definition of `it': it = runFoo foo
-|
-| Why all of the sudden does GHC need the constraint Bar a b? The
-| function foo didn't ask for that...
-
-The trouble is that to type (runFoo foo), GHC has to solve the problem:
-
- Given constraint Foo a b
- Solve constraint Foo a b'
-
-Notice that b and b' aren't the same. To solve this, just do
-improvement and then they are the same. But GHC currently does
- simplify constraints
- apply improvement
- and loop
-
-That is usually fine, but it isn't here, because it sees that Foo a b is
-not the same as Foo a b', and so instead applies the instance decl for
-instance Bar a b => Foo a b. And that's where the Bar constraint comes
-from.
-
-The Right Thing is to improve whenever the constraint set changes at
-all. Not hard in principle, but it'll take a bit of fiddling to do.
-
-
-
- --------------------------------------
- Notes on quantification
- --------------------------------------
-
-Suppose we are about to do a generalisation step.
-We have in our hand
-
- G the environment
- T the type of the RHS
- C the constraints from that RHS
-
-The game is to figure out
-
- Q the set of type variables over which to quantify
- Ct the constraints we will *not* quantify over
- Cq the constraints we will quantify over
-
-So we're going to infer the type
-
- forall Q. Cq => T
-
-and float the constraints Ct further outwards.
-
-Here are the things that *must* be true:
-
- (A) Q intersect fv(G) = EMPTY limits how big Q can be
- (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
-
-(A) says we can't quantify over a variable that's free in the
-environment. (B) says we must quantify over all the truly free
-variables in T, else we won't get a sufficiently general type. We do
-not *need* to quantify over any variable that is fixed by the free
-vars of the environment G.
-
- BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
-
-Example: class H x y | x->y where ...
-
- fv(G) = {a} C = {H a b, H c d}
- T = c -> b
-
- (A) Q intersect {a} is empty
- (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
-
- So Q can be {c,d}, {b,c,d}
-
-Other things being equal, however, we'd like to quantify over as few
-variables as possible: smaller types, fewer type applications, more
-constraints can get into Ct instead of Cq.
-
-
------------------------------------------
-We will make use of
-
- fv(T) the free type vars of T
-
- oclose(vs,C) The result of extending the set of tyvars vs
- using the functional dependencies from C
-
- grow(vs,C) The result of extend the set of tyvars vs
- using all conceivable links from C.
-
- E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
- Then grow(vs,C) = {a,b,c}
-
- Note that grow(vs,C) `superset` grow(vs,simplify(C))
- That is, simplfication can only shrink the result of grow.
-
-Notice that
- oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
- grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
-
-
------------------------------------------
-
-Choosing Q
-~~~~~~~~~~
-Here's a good way to choose Q:
-
- Q = grow( fv(T), C ) \ oclose( fv(G), C )
+*********************************************************************************
+* *
+* External interface *
+* *
+*********************************************************************************
-That is, quantify over all variable that that MIGHT be fixed by the
-call site (which influences T), but which aren't DEFINITELY fixed by
-G. This choice definitely quantifies over enough type variables,
-albeit perhaps too many.
-
-Why grow( fv(T), C ) rather than fv(T)? Consider
-
- class H x y | x->y where ...
-
- T = c->c
- C = (H c d)
-
- If we used fv(T) = {c} we'd get the type
-
- forall c. H c d => c -> b
-
- And then if the fn was called at several different c's, each of
- which fixed d differently, we'd get a unification error, because
- d isn't quantified. Solution: quantify d. So we must quantify
- everything that might be influenced by c.
-
-Why not oclose( fv(T), C )? Because we might not be able to see
-all the functional dependencies yet:
-
- class H x y | x->y where ...
- instance H x y => Eq (T x y) where ...
-
- T = c->c
- C = (Eq (T c d))
-
- Now oclose(fv(T),C) = {c}, because the functional dependency isn't
- apparent yet, and that's wrong. We must really quantify over d too.
-
-
-There really isn't any point in quantifying over any more than
-grow( fv(T), C ), because the call sites can't possibly influence
-any other type variables.
-
-
-
--------------------------------------
- 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
+\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}
-Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
-is a "bubble" that's a set of constraints
+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.
- Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
+\begin{code}
+simplifyBracket :: WantedConstraints -> TcM ()
+simplifyBracket wanteds
+ = do { zonked_wanteds <- mapBagM zonkWanted wanteds
+ ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
+ ; return () }
+\end{code}
-Hence another idea. To decide Q start with fv(T) and grow it
-by transitive closure in Cq (no functional dependencies involved).
-Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
-The definitely-ambiguous can then float out, and get smashed at top level
-(which squashes out the constants, like Eq (T a) above)
+*********************************************************************************
+* *
+* Deriving
+* *
+***********************************************************************************
- --------------------------------------
- Notes on principal types
- --------------------------------------
+\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}
- class C a where
- op :: a -> a
+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.
- f x = let g y = op (y::Int) in True
+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)
-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
+Notice that this instance (just) satisfies the Paterson termination
+conditions. Then we *could* derive an instance decl like this:
+ instance (C Int a, Eq b, Eq c) => Eq (T a b c)
+even though there is no instance for (C Int a), because there just
+*might* be an instance for, say, (C Int Bool) at a site where we
+need the equality instance for T's.
- --------------------------------------
- The need for forall's in constraints
- --------------------------------------
+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.
-[Exchange on Haskell Cafe 5/6 Dec 2000]
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
- class C t where op :: t -> Bool
- instance C [t] where op x = True
+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
- 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)
+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 definitions of p and q differ only in the order of the components in
-the pair on their right-hand sides. And yet:
+The bottom line
+~~~~~~~~~~~~~~~
+Allow constraints which consist only of type variables, with no repeats.
- 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!).
+*********************************************************************************
+* *
+* 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]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
- f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
- f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type
-varibables mentioned at all! The type of f looks ambiguous. But
-it isn't, because at a call site we might have
- let ?y = 5::Int in f 7
-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.
-
-
-\begin{code}
-tcSimplifyInfer
- :: SDoc
- -> TcTyVarSet -- fv(T); type vars
- -> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- TcDictBinds, -- Bindings
- [TcId]) -- Dict Ids that must be bound here (zonked)
- -- Any free (escaping) Insts are tossed into the environment
-\end{code}
-
-
-\begin{code}
-tcSimplifyInfer doc tau_tvs wanted_lie
- = do { let try_me inst | isDict inst = Stop -- Dicts
- | otherwise = ReduceMe NoSCs -- Lits, Methods,
- -- and impliciation constraints
- -- In an effort to make the inferred types simple, we try
- -- to squeeze out implication constraints if we can.
- -- See Note [Squashing methods]
-
- ; (binds1, irreds) <- checkLoop (mkRedEnv doc try_me []) wanted_lie
-
- ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let preds = fdPredsOfInsts irreds
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
- (free, bound) = partition (isFreeWhenInferring qtvs) irreds
-
- -- Remove redundant superclasses from 'bound'
- -- The 'Stop' try_me result does not do so,
- -- see Note [No superclasses for Stop]
- ; let try_me inst = ReduceMe AddSCs
- ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) bound
-
- ; extendLIEs free
- ; return (varSetElems qtvs, binds1 `unionBags` binds2, map instToId irreds) }
- -- NB: when we are done, we might have some bindings, but
- -- the final qtvs might be empty. See Note [NO TYVARS] below.
-\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 qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
-isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyCheck}
-%* *
-%************************************************************************
-
-@tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over. For example, a class or instance declaration.
-
-\begin{code}
------------------------------------------------------------
--- tcSimplifyCheck 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 isSkolemTyVar qtvs )
- do { (binds, irreds) <- innerCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc [] emptyRefinement
- qtvs givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
--- tcSimplifyCheckPat is used for existential pattern match
-tcSimplifyCheckPat :: InstLoc
- -> [CoVar] -> Refinement
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
- = ASSERT( all isSkolemTyVar qtvs )
- do { (binds, irreds) <- innerCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc co_vars reft
- qtvs givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
-bindIrreds :: InstLoc -> [CoVar] -> Refinement
- -> [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
-bindIrreds loc co_vars reft qtvs givens irreds
- = do { let givens' = filter isDict givens
- -- The givens can include methods
-
- -- 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
-
- ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
- ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
- -- This call does the real work
- ; extendLIEs implics
- ; return bind }
-
-
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
- -> [Inst] -> [Inst]
- -> TcM ([Inst], TcDictBinds)
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
--- The binding looks like
--- (ir1, .., irn) = f qtvs givens
--- where f is (evidence for) the new implication constraint
---
--- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
- givens -- Guaranteed all Dicts
- 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 name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
- implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
- tci_tyvars = all_tvs,
- tci_given = givens,
- tci_wanted = irreds, tci_loc = loc }
-
- ; let n_irreds = length irreds
- irred_ids = map instToId irreds
- tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
- pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
- rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | n_irreds==1 = VarBind (head irred_ids) rhs
- | otherwise = PatBind { pat_lhs = L span pat,
- pat_rhs = unguardedGRHSs rhs,
- pat_rhs_ty = tup_ty,
- bind_fvs = placeHolderNames }
- ; -- pprTrace "Make implic inst" (ppr implic_inst) $
- return ([implic_inst], unitBag (L span bind)) }
-
------------------------------------------------------------
-topCheckLoop :: SDoc
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
-
-topCheckLoop doc wanteds
- = checkLoop (mkRedEnv doc try_me []) wanteds
- where
- try_me inst = ReduceMe AddSCs
-
------------------------------------------------------------
-innerCheckLoop :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
-
-innerCheckLoop inst_loc givens wanteds
- = checkLoop env wanteds
- where
- env = mkRedEnv (pprInstLoc inst_loc) try_me givens
-
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
- | otherwise = Stop
- -- When checking against a given signature
- -- we MUST be very gentle: Note [Check gently]
-\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 topCheckLooop.
-
-
-\begin{code}
------------------------------------------------------------
-checkLoop :: RedEnv
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds,
- [Inst]) -- Irreducible
--- Precondition: the try_me never returns Free
--- givens are completely rigid
-
-checkLoop env wanteds
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- mappM zonkInst wanteds
-
- ; (improved, binds, irreds) <- reduceContext env wanteds'
-
- ; if not improved then
- return (binds, irreds)
- 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, irreds1) <- checkLoop env irreds
- ; return (binds `unionBags` binds1, irreds1) } }
-\end{code}
-
-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)!
-
+*********************************************************************************
+* *
+* 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}
------------------------------------------------------------
--- 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 ([TcTyVar], -- Variables over which to quantify
- TcDictBinds) -- Bindings
-
-tcSimplifyInferCheck loc tau_tvs givens wanteds
- = do { (binds, irreds) <- innerCheckLoop 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
-
- -- Now we are back to normal (c.f. tcSimplCheck)
- ; implic_bind <- bindIrreds loc [] emptyRefinement
- qtvs givens irreds
- ; return (qtvs, binds `unionBags` implic_bind) }
+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}
-%************************************************************************
-%* *
- tcSimplifySuperClasses
-%* *
-%************************************************************************
+*********************************************************************************
+* *
+* RULES *
+* *
+***********************************************************************************
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
+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.
- class S a
-
- class S a => C a where { opc :: a -> a }
- class S b => D b where { opd :: b -> b }
-
- instance C Int where
- opc = opd
-
- instance D Int where
- opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
- $dfCInt = :C ds1 (opd dd)
- dd = $dfDInt
- ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
-
-Alas! Alack! We can do the same for (instance D Int):
-
- $dfDInt = :D ds2 (opc dc)
- dc = $dfCInt
- ds2 = $p1 dc
-
-And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
-Two more nasty cases are in
- tcrun021
- tcrun033
-
-\begin{code}
-tcSimplifySuperClasses
- :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
- = do { (binds1, irreds) <- checkLoop env sc_wanteds
- ; let (tidy_env, tidy_irreds) = tidyInsts irreds
- ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
- ; return binds1 }
- where
- env = mkRedEnv (pprInstLoc loc) try_me givens
- try_me inst = ReduceMe NoSCs
- -- Like topCheckLoop, but with NoSCs
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyRestricted}
-%* *
-%************************************************************************
-
-tcSimplifyRestricted infers which type variables to quantify for a
-group of restricted bindings. This isn't trivial.
-
-Eg1: id = \x -> x
- We want to quantify over a to get id :: forall a. a->a
-
-Eg2: eq = (==)
- We do not want to quantify over a, because there's an Eq a
- constraint, so we get eq :: a->a->Bool (notice no forall)
-
-So, assume:
- RHS has type 'tau', whose free tyvars are tau_tvs
- RHS has constraints 'wanteds'
-
-Plan A (simple)
- Quantify over (tau_tvs \ ftvs(wanteds))
- This is bad. The constraints may contain (Monad (ST s))
- where we have instance Monad (ST s) where...
- so there's no need to be monomorphic in s!
-
- Also the constraint might be a method constraint,
- whose type mentions a perfectly innocent tyvar:
- op :: Num a => a -> b -> a
- Here, b is unconstrained. A good example would be
- foo = op (3::Int)
- We want to infer the polymorphic type
- foo :: forall b. b -> b
-
-
-Plan B (cunning, used for a long time up to and including GHC 6.2)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
- The reasons for this is to maximise sharing.
-
- This fails for a very subtle reason. Suppose that in the Step 2
- a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
- In the Step 1 this constraint might have been simplified, perhaps to
- (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
- This won't happen in Step 2... but that in turn might prevent some other
- constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
- and that in turn breaks the invariant that no constraints are quantified over.
-
- Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
- the problem.
-
-
-Plan C (brutal)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
- Return the bindings from Step 1.
-
-
-A note about Plan C (arising from "bug" reported by George Russel March 2004)
-Consider this:
-
- instance (HasBinary ty IO) => HasCodedValue ty
-
- foo :: HasCodedValue a => String -> IO a
-
- doDecodeIO :: HasCodedValue a => () -> () -> IO a
- doDecodeIO codedValue view
- = let { act = foo "foo" } in act
-
-You might think this should work becuase the call to foo gives rise to a constraint
-(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
-restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
-constraint using the (rather bogus) instance declaration, and now we are stuffed.
-
-I claim this is not really a bug -- but it bit Sergey as well as George. So here's
-plan D
-
-
-Plan D (a variant of plan B)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
-
- The point here is that it's generally OK to have too few qtvs; that is,
- to make the thing more monomorphic than it could be. We don't want to
- do that in the common cases, but in wierd cases it's ok: the programmer
- can always add a signature.
-
- Too few qtvs => too many wanteds, which is what happens if you do less
- improvement.
-
-
-\begin{code}
-tcSimplifyRestricted -- Used for restricted binding groups
- -- i.e. ones subject to the monomorphism restriction
- :: SDoc
- -> TopLevelFlag
- -> [Name] -- Things bound in this group
- -> TcTyVarSet -- Free in the type of the RHSs
- -> [Inst] -- Free in the RHSs
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
- TcDictBinds) -- Bindings
- -- tcSimpifyRestricted returns no constraints to
- -- quantify over; by definition there are none.
- -- They are all thrown back in the LIE
-
-tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
- -- Zonk everything in sight
- = mappM zonkInst wanteds `thenM` \ wanteds' ->
-
- -- 'ReduceMe': Reduce as far as we can. Don't stop at
- -- dicts; the idea is to get rid of as many type
- -- variables as possible, and we don't want to stop
- -- at (say) Monad (ST s), because that reduces
- -- immediately, with no constraint on s.
- --
- -- BUT do no improvement! See Plan D above
- -- HOWEVER, some unification may take place, if we instantiate
- -- a method Inst with an equality constraint
- let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
- in
- reduceContext env wanteds' `thenM` \ (_imp, _binds, constrained_dicts) ->
-
- -- Next, figure out the tyvars we will quantify over
- zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
- tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
- mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' ->
- let
- constrained_tvs' = tyVarsOfInsts constrained_dicts'
- qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
- `minusVarSet` constrained_tvs'
- in
- traceTc (text "tcSimplifyRestricted" <+> vcat [
- pprInsts wanteds, pprInsts constrained_dicts',
- ppr _binds,
- ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) `thenM_`
-
- -- The first step may have squashed more methods than
- -- necessary, so try again, this time more gently, knowing the exact
- -- set of type variables to quantify over.
- --
- -- We quantify only over constraints that are captured by qtvs;
- -- these will just be a subset of non-dicts. This in contrast
- -- to normal inference (using isFreeWhenInferring) in which we quantify over
- -- all *non-inheritable* constraints too. This implements choice
- -- (B) under "implicit parameter and monomorphism" above.
- --
- -- Remember that we may need to do *some* simplification, to
- -- (for example) squash {Monad (ST s)} into {}. It's not enough
- -- just to float all constraints
- --
- -- At top level, we *do* squash methods becuase we want to
- -- expose implicit parameters to the test that follows
- let
- is_nested_group = isNotTopLevel top_lvl
- try_me inst | isFreeWrtTyVars qtvs inst,
- (is_nested_group || isDict inst) = Stop
- | otherwise = ReduceMe AddSCs
- env = mkNoImproveRedEnv doc try_me
- in
- reduceContext env wanteds' `thenM` \ (_imp, binds, irreds) ->
- ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
-
- -- See "Notes on implicit parameters, Question 4: top level"
- if is_nested_group then
- extendLIEs irreds `thenM_`
- returnM (varSetElems qtvs, binds)
- else
- let
- (non_ips, bad_ips) = partition isClassDict irreds
- in
- addTopIPErrs bndrs bad_ips `thenM_`
- extendLIEs non_ips `thenM_`
- returnM (varSetElems qtvs, binds)
-\end{code}
-
-
-%************************************************************************
-%* *
- tcSimplifyRuleLhs
-%* *
-%************************************************************************
-
-On the LHS of transformation rules we only simplify methods and constants,
-getting dictionaries. We want to keep all of them unsimplified, to serve
-as the available stuff for the RHS of the rule.
+Implementation: the TcSFlags carried by the TcSMonad controls the
+amount of simplification, so simplifyRuleLhs just sets the flag
+appropriately.
Example. Consider the following left-hand side of a rule
-
f (x == y) (y > z) = ...
-
If we typecheck this expression we get constraints
-
d1 :: Ord a, d2 :: Eq a
-
We do NOT want to "simplify" to the LHS
-
forall x::a, y::a, z::a, d1::Ord a.
f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
-
Instead we want
-
forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
f ((==) d2 x y) ((>) d1 y z) = ...
Here is another example:
-
fromIntegral :: (Integral a, Num b) => a -> b
{-# RULES "foo" fromIntegral = id :: Int -> Int #-}
-
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
-
forall dIntegralInt.
fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
-
because the scsel will mess up RULE matching. Instead we want
-
forall dIntegralInt, dNumInt.
fromIntegral Int Int dIntegralInt dNumInt = id Int
Even if we have
-
g (x == y) (y == z) = ..
-
where the two dictionaries are *identical*, we do NOT WANT
-
forall x::a, y::a, z::a, d1::Eq a
f ((==) d1 x y) ((>) d1 y z) = ...
-
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.
-In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
-all dicts unchanged, with absolutely no sharing. It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
-
-\begin{code}
-tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
-tcSimplifyRuleLhs wanteds
- = go [] emptyBag wanteds
- where
- go dicts binds []
- = return (dicts, binds)
- go dicts binds (w:ws)
- | isDict w
- = go (w:dicts) binds ws
- | otherwise
- = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
- -- to fromInteger; this looks fragile to me
- ; lookup_result <- lookupSimpleInst w'
- ; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
- NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
- }
-\end{code}
-
-tcSimplifyBracket is used when simplifying the constraints arising from
-a Template Haskell bracket [| ... |]. We want to check that there aren't
-any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
-Show instance), but we aren't otherwise interested in the results.
-Nor do we care about ambiguous dictionaries etc. We will type check
-this bracket again at its usage site.
-
-\begin{code}
-tcSimplifyBracket :: [Inst] -> TcM ()
-tcSimplifyBracket wanteds
- = do { topCheckLoop doc wanteds
- ; return () }
- where
- doc = text "tcSimplifyBracket"
-\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.
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.
-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.
+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}
-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' <- mappM zonkInst wanteds
- ; given_ips' <- mappM zonkInst given_ips
- -- Unusually for checking, we *must* zonk the given_ips
-
- ; let env = mkRedEnv doc try_me given_ips'
- ; (improved, binds, irreds) <- reduceContext env wanteds'
-
- ; if not improved then
- ASSERT( all is_free irreds )
- do { extendLIEs irreds
- ; return binds }
- else
- tcSimplifyIPs given_ips wanteds }
- where
- doc = text "tcSimplifyIPs" <+> ppr given_ips
- ip_set = mkNameSet (ipNamesOfInsts given_ips)
- is_free inst = isFreeWrtIPs ip_set inst
-
- -- Simplify any methods that mention the implicit parameter
- try_me inst | is_free inst = Stop
- | otherwise = ReduceMe NoSCs
+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[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.
+*********************************************************************************
+* *
+* Main Simplifier *
+* *
+***********************************************************************************
\begin{code}
-bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
--- Simlifies only MethodInsts, and generate only bindings of form
--- fm = f tys dicts
--- We're careful not to even generate bindings of the form
--- d1 = d2
--- You'd think that'd be fine, but it interacts with what is
--- arguably a bug in Match.tidyEqnInfo (see notes there)
-
-bindInstsOfLocalFuns wanteds local_ids
- | null overloaded_ids
- -- Common case
- = extendLIEs wanteds `thenM_`
- returnM emptyLHsBinds
-
- | otherwise
- = do { (binds, irreds) <- checkLoop env for_me
- ; extendLIEs not_for_me
- ; extendLIEs irreds
- ; return binds }
- where
- env = mkRedEnv doc try_me []
- doc = text "bindInsts" <+> ppr local_ids
- overloaded_ids = filter is_overloaded local_ids
- is_overloaded id = isOverloadedTy (idType id)
- (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
-
- overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
- -- so it's worth building a set, so that
- -- lookup (in isMethodFor) is faster
- try_me inst | isMethod inst = ReduceMe NoSCs
- | otherwise = Stop
-\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
- -- but see Note [Rigidity]
- , 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 }
-
-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 WantSCs -- 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]
-\end{code}
-
-%************************************************************************
-%* *
-\subsection[reduce]{@reduce@}
-%* *
-%************************************************************************
-
-
-\begin{code}
-reduceContext :: RedEnv
- -> [Inst] -- Wanted
- -> TcM (ImprovementDone,
- TcDictBinds, -- Dictionary bindings
- [Inst]) -- Irreducible
-
-reduceContext env wanteds
- = do { traceTc (text "reduceContext" <+> (vcat [
- text "----------------------",
- red_doc env,
- text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds,
- text "----------------------"
- ]))
-
- -- Build the Avail mapping from "givens"
- ; init_state <- foldlM addGiven emptyAvails (red_givens env)
-
- -- Do the real work
- ; avails <- reduceList env wanteds init_state
-
- ; let improved = availsImproved avails
- ; (binds, irreds) <- extractResults avails wanteds
-
- ; traceTc (text "reduceContext end" <+> (vcat [
- text "----------------------",
- red_doc env,
- text "given" <+> ppr (red_givens env),
- text "wanted" <+> ppr wanteds,
- text "----",
- text "avails" <+> pprAvails avails,
- text "improved =" <+> ppr improved,
- text "----------------------"
- ]))
-
- ; return (improved, binds, irreds) }
-
-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))
- ; mappM_ unify eqns
- ; return True }
- where
- unify ((qtvs, pairs), what1, what2)
- = addErrCtxtM (mkEqnMsg what1 what2) $
- tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
- mapM_ (unif_pr tenv) pairs
- unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
-
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
-
-mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
- = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
- ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
- ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
- nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
- nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
- ; return (tidy_env, msg) }
-\end{code}
-
-The main context-reduction function is @reduce@. Here's its game plan.
-
-\begin{code}
-reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
-reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
- = do { dopts <- getDOpts
-#ifdef DEBUG
- ; if n > 8 then
- dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n)
- 2 (ifPprDebug (nest 2 (pprStack stk))))
- else return ()
-#endif
- ; if n >= ctxtStkDepth dopts then
- failWithTc (reduceDepthErr n stk)
- else
- go wanteds state }
+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
- 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 env wanted avails
- -- It's the same as an existing inst, or a superclass thereof
- | Just avail <- findAvail avails wanted
- = returnM avails
-
- | otherwise
- = case red_try_me env wanted of {
- ; Stop -> try_simple (addIrred NoSCs) -- See Note [No superclasses for Stop]
-
- ; ReduceMe want_scs -> -- It should be reduced
- reduceInst env avails wanted `thenM` \ (avails, lookup_result) ->
- case lookup_result of
- NoInstance -> -- No such instance!
- -- Add it and its superclasses
- addIrred want_scs avails wanted
-
- GenInst [] rhs -> addWanted want_scs avails wanted rhs []
-
- GenInst wanteds' rhs -> do { avails1 <- addIrred NoSCs avails wanted
- ; avails2 <- reduceList env wanteds' avails1
- ; addWanted want_scs avails2 wanted rhs wanteds' }
- -- Temporarily do addIrred *before* the reduceList,
- -- which has the effect of adding the thing we are trying
- -- to prove to the database before trying to prove the things it
- -- needs. See note [RECURSIVE DICTIONARIES]
- -- NB: we must not do an addWanted before, because that adds the
- -- superclasses too, and thaat can lead to a spurious loop; see
- -- the examples in [SUPERCLASS-LOOP]
- -- So we do an addIrred before, and then overwrite it afterwards with addWanted
-
- }
+ 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
- -- 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 []
- other -> do_this_otherwise avails wanted }
+ 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}
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough. Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
-
- class Ord a => C a where
- instance Ord [a] => C [a] where ...
-
-Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
-superclasses of C [a] to avails. But we must not overwrite the binding
-for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
-build a loop!
-
-Here's another variant, immortalised in tcrun020
- class Monad m => C1 m
- class C1 m => C2 m x
- instance C2 Maybe Bool
-For the instance decl we need to build (C1 Maybe), and it's no good if
-we run around and add (C2 Maybe Bool) and its superclasses to the avails
-before we search for C1 Maybe.
-
-Here's another example
- class Eq b => Foo a b
- instance Eq a => Foo [a] a
-If we are reducing
- (Foo [t] t)
-
-we'll first deduce that it holds (via the instance decl). We must not
-then overwrite the Eq t constraint with a superclass selection!
-
-At first I had a gross hack, whereby I simply did not add superclass constraints
-in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
-becuase it lost legitimate superclass sharing, and it still didn't do the job:
-I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an 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.
-
-
-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.
-
-
-%************************************************************************
-%* *
- Reducing a single constraint
-%* *
-%************************************************************************
-
-\begin{code}
----------------------------------------------
-reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
- tci_given = extra_givens, tci_wanted = wanteds })
- = reduceImplication env avails reft tvs extra_givens wanteds loc
-
-reduceInst env avails other_inst
- = do { result <- lookupSimpleInst other_inst
- ; return (avails, result) }
-\end{code}
-
-\begin{code}
----------------------------------------------
-reduceImplication :: RedEnv
- -> Avails
- -> Refinement -- May refine the givens; often empty
- -> [TcTyVar] -- Quantified type variables; all skolems
- -> [Inst] -- Extra givens; all rigid
- -> [Inst] -- Wanted
- -> InstLoc
- -> TcM (Avails, LookupInstResult)
-\end{code}
-
-Suppose we are simplifying the constraint
- forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens',
-and refinment 'reft'.
-
-Note that
- * The refinement is often empty
-
- * The 'extra givens' need not mention any of the quantified type variables
- e.g. forall {}. Eq a => Eq [a]
- forall {}. C Int => D (Tree Int)
-
- This happens when you have something like
- data T a where
- T1 :: Eq a => a -> T a
-
- f :: T a -> Int
- f x = ...(case x of { T1 v -> v==v })...
-
-\begin{code}
- -- ToDo: should we instantiate tvs? I think it's not necessary
- --
- -- ToDo: what about improvement? There may be some improvement
- -- exposed as a result of the simplifications done by reduceList
- -- which are discarded if we back off.
- -- This is almost certainly Wrong, but we'll fix it when dealing
- -- better with equality constraints
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
- = do { -- Add refined givens, and the extra givens
- (refined_red_givens, avails)
- <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
- else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
- ; avails <- foldlM addGiven avails extra_givens
-
- -- Solve the sub-problem
- ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
- env' = env { red_givens = refined_red_givens ++ extra_givens
- , red_try_me = try_me }
-
- ; traceTc (text "reduceImplication" <+> vcat
- [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ])
- ; avails <- reduceList env' wanteds avails
-
- -- Extract the binding (no frees, because try_me never says Free)
- ; (binds, irreds) <- extractResults avails wanteds
+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:
- -- We always discard the extra avails we've generated;
- -- but we remember if we have done any (global) improvement
- ; let ret_avails = updateImprovement orig_avails avails
-
- ; if isEmptyLHsBinds binds then -- No progress
- return (ret_avails, NoInstance)
- else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
- -- This binding is useless if the recursive simplification
- -- made no progress; but currently we don't try to optimise that
- -- case. After all, we only try hard to reduce at top level, or
- -- when inferring types.
-
- ; let dict_ids = map instToId extra_givens
- co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
- rhs = mkHsWrap co payload
- loc = instLocSpan inst_loc
- payload | isSingleton wanteds = HsVar (instToId (head wanteds))
- | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
-
- -- If there are any irreds, we back off and return NoInstance
- ; return (ret_avails, GenInst implic_insts (L loc rhs))
- } }
-\end{code}
-
-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!
-
-%************************************************************************
-%* *
- 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 TcId -- Used for dictionaries for which we have a binding
- -- e.g. those "given" in a signature
-
- | Rhs -- Used when there is a RHS
- (LHsExpr TcId) -- The RHS
- [Inst] -- Insts free in the RHS; we need these too
-
-instance Outputable Avails where
- ppr = pprAvails
-
-pprAvails (Avails imp avails)
- = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
- , nest 2 (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) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
-
--------------------------
-extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
-extendAvailEnv env inst avail = addToFM env inst avail
-
-findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
-findAvailEnv env wanted = lookupFM env wanted
- -- NB 1: the Ord instance of Inst compares by the class/type info
- -- *not* by unique. So
- -- d1::C Int == d2::C Int
-
-emptyAvails :: Avails
-emptyAvails = Avails False emptyFM
-
-findAvail :: Avails -> Inst -> Maybe AvailHow
-findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
-
-elemAvails :: Inst -> Avails -> Bool
-elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
-
-extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
--- Does improvement
-extendAvails avails@(Avails imp env) inst avail
- = do { imp1 <- tcImproveOne avails inst -- Do any improvement
- ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
-
-availsInsts :: Avails -> [Inst]
-availsInsts (Avails _ avails) = keysFM avails
-
-availsImproved (Avails imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
-\end{code}
-
-Extracting the bindings from a bunch of Avails.
-The bindings do *not* come back sorted in dependency order.
-We assume that they'll be wrapped in a big Rec, so that the
-dependency analyser can sort them out later
-
-\begin{code}
-extractResults :: Avails
- -> [Inst] -- Wanted
- -> TcM ( TcDictBinds, -- Bindings
- [Inst]) -- Irreducible ones
-
-extractResults (Avails _ avails) wanteds
- = go avails emptyBag [] wanteds
- where
- go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
- -> TcM (TcDictBinds, [Inst])
- go avails binds irreds []
- = returnM (binds, irreds)
-
- go avails binds irreds (w:ws)
- = case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
-
- Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
-
- Just (Given id)
- | id == instToId w
- -> go avails binds irreds ws
- -- The sought Id can be one of the givens, via a superclass chain
- -- and then we definitely don't want to generate an x=x binding!
-
- | otherwise
- -> go avails (addBind binds w (nlHsVar id)) irreds ws
-
- Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
- where
- new_binds = addBind binds w rhs
- where
- w_span = instSpan w
- w_id = instToId w
-
- add_given avails w = extendAvailEnv avails w (Given (instToId w))
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
- (VarBind (instToId inst) rhs))
-\end{code}
-
+ 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
+------------------------------------------------------------------------------------------
-Note [No superclasses for Stop]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
-add it to avails, so that any other equal Insts will be commoned up
-right here. However, we do *not* add superclasses. If we have
- df::Floating a
- dn::Num a
-but a is not bound here, then we *don't* want to derive dn from df
-here lest we lose sharing.
\begin{code}
-addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted want_scs avails wanted rhs_expr wanteds
- = addAvailAndSCs want_scs avails wanted avail
- where
- avail = Rhs rhs_expr wanteds
-
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
- -- Always add superclasses for 'givens'
- --
- -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
- -- decl for Ord t we can add both Ord t and Eq t as 'givens',
- -- so the assert isn't true
-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
- | isDict given -- We sometimes have 'given' methods, but they
- -- are always optional, so we can drop them
- , Just (co, pred) <- refinePred reft (dictPred given)
- = do { new_given <- newDictBndr (instLoc given) pred
- ; let rhs = L (instSpan given) $
- HsWrap (WpCo co) (HsVar (instToId given))
- ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
- ; return (new_given:refined_givens, avails) }
- -- ToDo: the superclasses of the original given all exist in Avails
- -- so we could really just cast them, but it's more awkward to do,
- -- and hopefully the optimiser will spot the duplicated work
+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
- = return (refined_givens, avails)
-
-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 (instToId inst)) avail
- dep_tys = map idType (varSetElems deps)
-
- findAllDeps :: IdSet -> AvailHow -> IdSet
- -- Find all the Insts that this one depends on
- -- See Note [SUPERCLASS-LOOP 2]
- -- Watch out, though. Since the avails may contain loops
- -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
- findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
- findAllDeps so_far other = so_far
-
- find_all :: IdSet -> Inst -> IdSet
- find_all so_far kid
- | 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 "dont do this because the original thing
- -- depends on this one, so you'd build a loop"
- -- Invariant: the Inst is already in Avails.
-
-addSCs is_loop avails dict
- = ASSERT( isDict dict )
- do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
- ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
+ = 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.
+--
+-- 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 DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
+ -- 'DefaultOrigin' is strictly the declaration, but it's convenient
+ 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
- (clas, tys) = getDictClassTys dict
- (tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
-
- add_sc avails (sc_dict, sc_sel)
- | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
- | is_given sc_dict = return avails
- | otherwise = 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 (instToId dict) <.> mkWpTyApps tys
-
- is_given :: Inst -> Bool
- is_given sc_dict = case findAvail avails sc_dict of
- Just (Given _) -> True -- Given is cheaper than superclass selection
- other -> False
-\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 doc interactive wanteds
- = do { wanteds <- mapM zonkInst wanteds
- ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
-
- ; (binds1, irreds1) <- topCheckLoop doc wanteds
-
- ; if null irreds1 then
- return binds1
- else do
- -- OK, so there are some errors
- { -- Use the defaulting rules to do extra unification
- -- NB: irreds are already zonked
- ; extended_default <- if interactive then return True
- else doptM Opt_ExtendedDefaultRules
- ; disambiguate extended_default irreds1 -- Does unification
- ; (binds2, irreds2) <- topCheckLoop doc irreds1
-
- -- Deal with implicit parameter
- ; let (bad_ips, non_ips) = partition isIPDict irreds2
- (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) }}
-\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 :: Bool -> [Inst] -> TcM ()
- -- Just does unification to fix the default types
- -- The Insts are assumed to be pre-zonked
-disambiguate extended_defaulting insts
- | null defaultable_groups
- = return ()
- | otherwise
- = do { -- Figure out what default types to use
- mb_defaults <- getDefaultTys
- ; default_tys <- case mb_defaults of
- Just tys -> return tys
- Nothing -> -- No use-supplied default;
- -- use [Integer, Double]
- do { integer_ty <- tcMetaTy integerTyConName
- ; checkWiredInTyCon doubleTyCon
- ; return [integer_ty, doubleTy] }
- ; mapM_ (disambigGroup default_tys) defaultable_groups }
- where
- unaries :: [(Inst,Class, TcTyVar)] -- (C tv) constraints
- bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
- (unaries, bad_tvs) = getDefaultableDicts insts
-
- -- 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):_)
- = not (isSkolemTyVar 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 isStandardClass clss && any isNumericClass clss
-
- -- In interactive mode, or with -fextended-default-rules,
- -- we default Show a to Show () to avoid graututious errors on "show []"
- isInteractiveClass cls
- = isNumericClass cls
- || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
-
-
-disambigGroup :: [Type] -- The default types
- -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
- -> TcM () -- Just does unification, to fix the default types
-
-disambigGroup default_tys dicts
- = try_default default_tys
+ unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
+ non_unaries :: [CanonicalCt] -- and *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
- (_,_,tyvar) = head dicts -- Should be non-empty
- classes = [c | (_,c,_) <- dicts]
-
- try_default [] = return ()
- try_default (default_ty : default_tys)
- = tryTcLIE_ (try_default default_tys) $
- do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
- -- This may fail; then the tryTcLIE_ kicks in
- -- Failure here is caused by there being no type in the
- -- default list which can satisfy all the ambiguous classes.
- -- For example, if Real a is reqd, but the only type in the
- -- default list is Int.
-
- -- After this we can't fail
- ; warnDefault dicts default_ty
- ; unifyType default_ty (mkTyVarTy tyvar) }
+ ((the_ct,the_tv):_) = group
+ wanteds = map fst group
+ wanted_ev_vars = map deCanonicaliseWanted wanteds
\end{code}
Note [Avoiding spurious errors]
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
- -> TyCon
- -> [TyVar]
- -> ThetaType -- Wanted
- -> TcM ThetaType -- Needed
-
-tcSimplifyDeriv orig tc tyvars theta
- = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
- -- The main loop may do unification, and that may crash if
- -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
- -- ToDo: what if two of them do get unified?
- newDictBndrsO orig (substTheta tenv theta) `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (_, irreds) ->
-
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
- let
- inst_ty = mkTyConApp tc (mkTyVarTys tvs)
- (ok_insts, bad_insts) = partition is_ok_inst irreds
- is_ok_inst inst
- = isDict inst -- Exclude implication consraints
- && (isTyVarClassPred pred || (gla_exts && ok_gla_pred pred))
- where
- pred = dictPred inst
-
- ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred])
- -- See Note [Deriving context]
-
- tv_set = mkVarSet tvs
- simpl_theta = map dictPred ok_insts
- weird_preds = [pred | pred <- simpl_theta
- , not (tyVarsOfPred pred `subVarSet` tv_set)]
-
- -- Check for a bizarre corner case, when the derived instance decl should
- -- have form instance C a b => D (T a) where ...
- -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
- -- of problems; in particular, it's hard to compare solutions for
- -- equality when finding the fixpoint. So I just rule it out for now.
-
- rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
- -- This reverse-mapping is a Royal Pain,
- -- but the result should mention TyVars not TcTyVars
- in
- -- In effect, the bad and wierd insts cover all of the cases that
- -- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv
- -- * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance)
- -- * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance)
- addNoInstanceErrs bad_insts `thenM_`
- mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
- returnM (substTheta rev_env simpl_theta)
- where
- doc = ptext SLIT("deriving classes for a data type")
-\end{code}
-
-Note [Deriving context]
-~~~~~~~~~~~~~~~~~~~~~~~
-With -fglasgow-exts, we allow things like (C Int a) in the simplified
-context for a derived instance declaration, because at a use of this
-instance, we might know that a=Bool, and have an instance for (C Int
-Bool)
-
-We nevertheless insist that each predicate meets the termination
-conditions. If not, the deriving mechanism generates larger and larger
-constraints. Example:
- data Succ a = S a
- data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ. First we'll generate
- instance (Show (Succ a), Show a) => Show (Seq a)
-and then
- instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on. Instead we want to complain of no instance for (Show (Succ a)).
-
-
-
-@tcSimplifyDefault@ just checks class-type constraints, essentially;
-used with \tr{default} declarations. We are only interested in
-whether it worked or not.
-
-\begin{code}
-tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
- -> TcM ()
-
-tcSimplifyDefault theta
- = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (_, irreds) ->
- addNoInstanceErrs irreds `thenM_`
- if null irreds then
- returnM ()
- else
- failM
- where
- doc = ptext SLIT("default declaration")
-\end{code}
-
-
-%************************************************************************
-%* *
-\section{Errors and contexts}
-%* *
-%************************************************************************
-
-ToDo: for these error messages, should we note the location as coming
-from the insts, or just whatever seems to be around in the monad just
-now?
-
-\begin{code}
-groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
- -> [Inst] -- The offending Insts
- -> TcM ()
--- Group together insts with the same origin
--- We want to report them together in error messages
-
-groupErrs report_err []
- = returnM ()
-groupErrs report_err (inst:insts)
- = do_one (inst:friends) `thenM_`
- groupErrs report_err others
-
- where
- -- (It may seem a bit crude to compare the error messages,
- -- but it makes sure that we combine just what the user sees,
- -- and it avoids need equality on InstLocs.)
- (friends, others) = partition is_friend insts
- loc_msg = showSDoc (pprInstLoc (instLoc inst))
- is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
- do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
- -- Add location and context information derived from the Insts
-
--- Add the "arising from..." part to a message about bunch of dicts
-addInstLoc :: [Inst] -> Message -> Message
-addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
-
-addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs []
- = return ()
-addTopIPErrs bndrs ips
- = addErrTcM (tidy_env, mk_msg tidy_ips)
- where
- (tidy_env, tidy_ips) = tidyInsts ips
- mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
- nest 2 (ptext SLIT("the monomorphic top-level binding")
- <> plural bndrs <+> ptext SLIT("of")
- <+> pprBinders bndrs <> colon)],
- nest 2 (vcat (map ppr_ip ips)),
- monomorphism_fix]
- 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
- -> [Inst] -- What is wanted (can include implications)
- -> TcM ()
-
-reportNoInstances tidy_env mb_what insts
- = groupErrs (report_no_instances tidy_env mb_what) insts
-
-report_no_instances tidy_env mb_what insts
- = do { inst_envs <- tcGetInstEnvs
- ; let (implics, insts1) = partition isImplicInst insts
- (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
- ; traceTc (text "reportNoInstnces" <+> vcat
- [ppr implics, ppr insts1, ppr insts2])
- ; mapM_ complain_implic implics
- ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
- ; groupErrs complain_no_inst insts2 }
- where
- complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
-
- complain_implic inst -- Recurse!
- = reportNoInstances tidy_env
- (Just (tci_loc inst, tci_given inst))
- (tci_wanted inst)
-
- check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
- -- Right msg => overlap message
- -- Left inst => no instance
- check_overlap inst_envs wanted
- | not (isClassDict wanted) = Left wanted
- | otherwise
- = case lookupInstEnv inst_envs clas tys of
- -- The case of exactly one match and no unifiers means
- -- a successful lookup. That can't happen here, becuase
- -- dicts only end up here if they didn't match in Inst.lookupInst
-#ifdef DEBUG
- ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
-#endif
- ([], _) -> Left wanted -- No match
- res -> Right (mk_overlap_msg wanted res)
- where
- (clas,tys) = getDictClassTys wanted
-
- mk_overlap_msg dict (matches, unifiers)
- = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
- <+> pprPred (dictPred dict))),
- sep [ptext SLIT("Matching instances") <> colon,
- nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
- ASSERT( not (null matches) )
- if not (isSingleton matches)
- then -- Two or more matches
- empty
- else -- One match, plus some unifiers
- ASSERT( not (null unifiers) )
- parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
- quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
- ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
- where
- ispecs = [ispec | (_, ispec) <- matches]
-
- mk_no_inst_err insts
- | null insts = empty
-
- | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
- not (isEmptyVarSet (tyVarsOfInsts insts))
- = vcat [ addInstLoc insts $
- sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts
- , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens]
- , show_fixes (fix1 loc : fixes2) ]
-
- | otherwise -- Top level
- = vcat [ addInstLoc insts $
- ptext SLIT("No instance") <> plural insts
- <+> ptext SLIT("for") <+> pprDictsTheta insts
- , show_fixes fixes2 ]
-
- 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 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) : _) -- The pairs share a common set of ambiguous tyvars
- = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
- 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
- = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
- returnM (tidy_env, mk_msg docs)
- where
- mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
- -- This happens in things like
- -- f x = show (read "foo")
- -- where monomorphism doesn't play any role
- mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
- nest 2 (vcat docs),
- monomorphism_fix
- ]
-monomorphism_fix :: SDoc
-monomorphism_fix = ptext SLIT("Probable fix:") <+>
- (ptext SLIT("give these definition(s) an explicit type signature")
- $$ ptext SLIT("or use -fno-monomorphism-restriction"))
-
-warnDefault ups default_ty
- = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
- addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
- where
- dicts = [d | (d,_,_) <- ups]
-
- -- Tidy them first
- (_, tidy_dicts) = tidyInsts dicts
- warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
- quotes (ppr default_ty),
- pprDictsInFull tidy_dicts]
-
--- Used for the ...Thetas variants; all top level
-badDerivedPred pred
- = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
- ptext SLIT("type variables that are not data type parameters"),
- nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
-
-reduceDepthErr n stack
- = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
- ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
- nest 4 (pprStack stack)]
-
-pprStack stack = vcat (map pprInstInFull stack)
-\end{code}