3 simplifyInfer, simplifySuperClass,
4 simplifyDefault, simplifyDeriv, simplifyBracket,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
21 import VarEnv ( varEnvElts )
24 import NameEnv ( emptyNameEnv )
30 import Class ( classKey )
31 import BasicTypes ( RuleName )
32 import Data.List ( partition )
38 *********************************************************************************
40 * External interface *
42 *********************************************************************************
45 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
46 -- Simplify top-level constraints
47 -- Usually these will be implications, when there is
48 -- nothing to quanitfy we don't wrap in a degenerate implication,
49 -- so we do that here instead
51 = simplifyCheck SimplCheck wanteds
54 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
55 simplifyInteractive wanteds
56 = simplifyCheck SimplInteractive wanteds
59 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
60 -> TcM () -- Succeeds iff the constraint is soluble
62 = do { loc <- getCtLoc DefaultOrigin
63 ; wanted <- newWantedEvVars theta
64 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
65 ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
69 simplifyBracket is used when simplifying the constraints arising from
70 a Template Haskell bracket [| ... |]. We want to check that there aren't
71 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
72 Show instance), but we aren't otherwise interested in the results.
73 Nor do we care about ambiguous dictionaries etc. We will type check
74 this bracket again at its usage site.
77 simplifyBracket :: WantedConstraints -> TcM ()
78 simplifyBracket wanteds
79 = do { zonked_wanteds <- mapBagM zonkWanted wanteds
80 ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
85 *********************************************************************************
89 ***********************************************************************************
92 simplifyDeriv :: CtOrigin
94 -> ThetaType -- Wanted
95 -> TcM ThetaType -- Needed
96 -- Given instance (wanted) => C inst_ty
97 -- Simplify 'wanted' as much as possibles
98 simplifyDeriv orig tvs theta
99 = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
100 -- One reason is that the constraint solving machinery
101 -- expects *TcTyVars* not TyVars. Another is that
102 -- when looking up instances we don't want overlap
105 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
107 ; loc <- getCtLoc orig
108 ; wanted <- newWantedEvVars (substTheta skol_subst theta)
109 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
111 ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
112 ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
114 ; let (good, bad) = partition validDerivPred $
115 foldrBag ((:) . wantedEvVarPred) [] unsolved
116 -- See Note [Exotic derived instance contexts]
117 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
119 ; reportUnsolvedDeriv bad loc
120 ; return $ substTheta subst_skol good }
123 Note [Exotic derived instance contexts]
124 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
125 In a 'derived' instance declaration, we *infer* the context. It's a
126 bit unclear what rules we should apply for this; the Haskell report is
127 silent. Obviously, constraints like (Eq a) are fine, but what about
128 data T f a = MkT (f a) deriving( Eq )
129 where we'd get an Eq (f a) constraint. That's probably fine too.
131 One could go further: consider
132 data T a b c = MkT (Foo a b c) deriving( Eq )
133 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
135 Notice that this instance (just) satisfies the Paterson termination
136 conditions. Then we *could* derive an instance decl like this:
138 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
139 even though there is no instance for (C Int a), because there just
140 *might* be an instance for, say, (C Int Bool) at a site where we
141 need the equality instance for T's.
143 However, this seems pretty exotic, and it's quite tricky to allow
144 this, and yet give sensible error messages in the (much more common)
145 case where we really want that instance decl for C.
147 So for now we simply require that the derived instance context
148 should have only type-variable constraints.
150 Here is another example:
151 data Fix f = In (f (Fix f)) deriving( Eq )
152 Here, if we are prepared to allow -XUndecidableInstances we
153 could derive the instance
154 instance Eq (f (Fix f)) => Eq (Fix f)
155 but this is so delicate that I don't think it should happen inside
156 'deriving'. If you want this, write it yourself!
158 NB: if you want to lift this condition, make sure you still meet the
159 termination conditions! If not, the deriving mechanism generates
160 larger and larger constraints. Example:
162 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
164 Note the lack of a Show instance for Succ. First we'll generate
165 instance (Show (Succ a), Show a) => Show (Seq a)
167 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
168 and so on. Instead we want to complain of no instance for (Show (Succ a)).
172 Allow constraints which consist only of type variables, with no repeats.
174 *********************************************************************************
178 ***********************************************************************************
181 simplifyInfer :: Bool -- Apply monomorphism restriction
182 -> TcTyVarSet -- These type variables are free in the
183 -- types to be generalised
185 -> TcM ([TcTyVar], -- Quantify over these type variables
186 [EvVar], -- ... and these constraints
187 TcEvBinds) -- ... binding these evidence variables
188 simplifyInfer apply_mr tau_tvs wanted
189 | isEmptyBag wanted -- Trivial case is quite common
190 = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
191 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
192 ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
193 ; return (qtvs, [], emptyTcEvBinds) }
196 = do { zonked_wanted <- mapBagM zonkWanted wanted
197 ; traceTc "simplifyInfer {" $ vcat
198 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
199 , ptext (sLit "wanted =") <+> ppr zonked_wanted
200 , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
203 -- Make a guess at the quantified type variables
204 -- Then split the constraints on the baisis of those tyvars
205 -- to avoid unnecessarily simplifying a class constraint
206 -- See Note [Avoid unecessary constraint simplification]
207 ; gbl_tvs <- tcGetGlobalTyVars
208 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
209 ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
210 zonked_tau_tvs `minusVarSet` gbl_tvs
211 (perhaps_bound, surely_free)
212 = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
214 ; emitConstraints surely_free
215 ; traceTc "sinf" $ vcat
216 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
217 , ptext (sLit "surely_free =") <+> ppr surely_free
220 -- Now simplify the possibly-bound constraints
221 ; (simplified_perhaps_bound, tc_binds)
222 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
224 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
225 -- may have done some unification
226 ; gbl_tvs <- tcGetGlobalTyVars
227 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
228 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
229 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
230 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
231 constrained_tvs = tyVarsOfWantedEvVars zonked_simples
232 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
233 (final_qtvs, (bound, free))
234 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
235 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
237 ; traceTc "end simplifyInfer }" $
238 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
239 , text "wanted = " <+> ppr zonked_wanted
240 , text "qtvs = " <+> ppr final_qtvs
241 , text "free = " <+> ppr free
242 , text "bound = " <+> ppr bound ]
244 -- Turn the quantified meta-type variables into real type variables
245 ; emitConstraints (mapBag WcEvVar free)
246 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
247 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
248 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
250 ------------------------
251 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
252 -> TcM (Bag WantedEvVar, Bag EvBind)
253 -- We use this function when inferring the type of a function
254 -- The wanted constraints are already zonked
255 simplifyAsMuchAsPossible ctxt wanteds
256 = do { let untch = NoUntouchables
257 -- We allow ourselves to unify environment
258 -- variables; hence *no untouchables*
260 ; ((unsolved_flats, unsolved_implics), ev_binds)
261 <- runTcS ctxt untch $
262 simplifyApproxLoop 0 wanteds
265 ; reportUnsolved (emptyBag, unsolved_implics)
267 ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
268 ; return (final_wanted_evvars, ev_binds) }
271 simplifyApproxLoop :: Int -> WantedConstraints
272 -> TcS (CanonicalCts, Bag Implication)
273 simplifyApproxLoop n wanteds
275 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
277 = do { traceTcS "simplifyApproxLoop" (vcat
278 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
279 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
281 ; let (extra_flats, thiner_unsolved_implics)
282 = approximateImplications unsolved_implics
284 = mkWantedConstraints unsolved_flats thiner_unsolved_implics
286 ;-- If no new work was produced then we are done with simplifyApproxLoop
287 if isEmptyBag extra_flats
288 then do { traceTcS "simplifyApproxLoopRes" (vcat
289 [ ptext (sLit "Wanted = ") <+> ppr wanteds
290 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
291 ; return (unsolved_flats, unsolved_implics) }
293 else -- Produced new flat work wanteds, go round the loop
294 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
297 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
298 -- (wc1, impls2) <- approximateImplications impls
299 -- splits 'impls' into two parts
300 -- wc1: a bag of constraints that do not mention any skolems
301 -- impls2: a bag of *thiner* implication constraints
302 approximateImplications impls
303 = splitBag (do_implic emptyVarSet) impls
306 do_wanted :: TcTyVarSet -> WantedConstraint
307 -> (WantedConstraints, WantedConstraints)
308 do_wanted skols (WcImplic impl)
309 = let (fl_w, mb_impl) = do_implic skols impl
310 in (fl_w, mapBag WcImplic mb_impl)
311 do_wanted skols wc@(WcEvVar wev)
312 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
313 | otherwise = (emptyBag, unitBag wc)
316 do_implic :: TcTyVarSet -> Implication
317 -> (WantedConstraints, Bag Implication)
318 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
319 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
320 else unitBag impl{ ic_wanted = rest_wanted } )
322 (floatable_wanted, rest_wanted)
323 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
326 splitBag :: (a -> (WantedConstraints, Bag a))
327 -> Bag a -> (WantedConstraints, Bag a)
328 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
331 = (wcs `unionBags` b1, imps `unionBags` b2)
337 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
338 growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
339 growWanteds gbl_tvs ws tvs
340 | isEmptyBag ws = tvs
341 | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
342 growWantedEVs gbl_tvs ws tvs
343 | isEmptyBag ws = tvs
344 | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
346 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
347 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
348 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
349 -- X-constraint 'wanted', nuking the 'gbls' at each stage
350 growWantedEV gbl_tvs wev tvs
351 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
353 ev_tvs = growPredTyVars (wantedEvVarPred wev) tvs
355 growWanted gbl_tvs (WcEvVar wev) tvs
356 = growWantedEV gbl_tvs wev tvs
357 growWanted gbl_tvs (WcImplic implic) tvs
358 = foldrBag (growWanted (gbl_tvs `unionVarSet` ic_skols implic))
359 tvs (ic_wanted implic)
362 quantifyMe :: TyVarSet -- Quantifying over these
364 -> Bool -- True <=> quantify over this wanted
366 | isIPPred pred = True -- Note [Inheriting implicit parameters]
367 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
369 pred = wantedEvVarPred wev
371 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
372 quantifyMeWC qtvs (WcImplic implic)
373 = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted implic)
374 quantifyMeWC qtvs (WcEvVar wev)
375 = quantifyMe qtvs wev
378 Note [Avoid unecessary constraint simplification]
379 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
380 When inferring the type of a let-binding, with simplifyInfer,
381 try to avoid unnecessariliy simplifying class constraints.
382 Doing so aids sharing, but it also helps with delicate
384 instance C t => C [t] where ..
386 f x = let g y = ...(constraint C [t])...
388 When inferring a type for 'g', we don't want to apply the
389 instance decl, because then we can't satisfy (C t). So we
390 just notice that g isn't quantified over 't' and partition
391 the contraints before simplifying.
393 This only half-works, but then let-generalisation only half-works.
396 Note [Inheriting implicit parameters]
397 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402 where f is *not* a top-level binding.
403 From the RHS of f we'll get the constraint (?y::Int).
404 There are two types we might infer for f:
408 (so we get ?y from the context of f's definition), or
410 f :: (?y::Int) => Int -> Int
412 At first you might think the first was better, becuase then
413 ?y behaves like a free variable of the definition, rather than
414 having to be passed at each call site. But of course, the WHOLE
415 IDEA is that ?y should be passed at each call site (that's what
416 dynamic binding means) so we'd better infer the second.
418 BOTTOM LINE: when *inferring types* you *must* quantify
419 over implicit parameters. See the predicate isFreeWhenInferring.
422 *********************************************************************************
426 ***********************************************************************************
428 When constructing evidence for superclasses in an instance declaration,
429 * we MUST have the "self" dictionary available, but
430 * we must NOT have its superclasses derived from "self"
432 Moreover, we must *completely* solve the constraints right now,
433 not wrap them in an implication constraint to solve later. Why?
434 Because when that implication constraint is solved there may
435 be some unrelated other solved top-level constraints that
436 recursively depend on the superclass we are building. Consider
437 class Ord a => C a where
438 instance C [Int] where ...
441 dCListInt = MkC $cNum ...
443 $cNum :: Ord [Int] -- The superclass
444 $cNum = let self = dCListInt in <solve Ord [Int]>
446 Now, if there is some *other* top-level constraint solved
450 we must not solve the (Ord [Int]) wanted from foo!!
453 simplifySuperClass :: EvVar -- The "self" dictionary
456 simplifySuperClass self wanteds
457 = do { wanteds <- mapBagM zonkWanted wanteds
458 ; loc <- getCtLoc NoScSkol
459 ; (unsolved, ev_binds)
460 <- runTcS SimplCheck NoUntouchables $
461 do { can_self <- canGivens loc [self]
462 ; let inert = foldlBag updInertSet emptyInert can_self
463 -- No need for solveInteract; we know it's inert
465 ; solveWanteds inert wanteds }
467 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
468 reportUnsolved unsolved }
472 *********************************************************************************
476 ***********************************************************************************
478 Note [Simplifying RULE lhs constraints]
479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
480 On the LHS of transformation rules we only simplify only equalitis,
481 but not dictionaries. We want to keep dictionaries unsimplified, to
482 serve as the available stuff for the RHS of the rule. We *do* want to
483 simplify equalities, however, to detect ill-typed rules that cannot be
486 Implementation: the TcSFlags carried by the TcSMonad controls the
487 amount of simplification, so simplifyRuleLhs just sets the flag
490 Example. Consider the following left-hand side of a rule
491 f (x == y) (y > z) = ...
492 If we typecheck this expression we get constraints
493 d1 :: Ord a, d2 :: Eq a
494 We do NOT want to "simplify" to the LHS
495 forall x::a, y::a, z::a, d1::Ord a.
496 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
498 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
499 f ((==) d2 x y) ((>) d1 y z) = ...
501 Here is another example:
502 fromIntegral :: (Integral a, Num b) => a -> b
503 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
504 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
505 we *dont* want to get
507 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
508 because the scsel will mess up RULE matching. Instead we want
509 forall dIntegralInt, dNumInt.
510 fromIntegral Int Int dIntegralInt dNumInt = id Int
513 g (x == y) (y == z) = ..
514 where the two dictionaries are *identical*, we do NOT WANT
515 forall x::a, y::a, z::a, d1::Eq a
516 f ((==) d1 x y) ((>) d1 y z) = ...
517 because that will only match if the dict args are (visibly) equal.
518 Instead we want to quantify over the dictionaries separately.
520 In short, simplifyRuleLhs must *only* squash equalities, leaving
521 all dicts unchanged, with absolutely no sharing.
523 HOWEVER, under a nested implication things are different
525 f :: (forall a. Eq a => a->a) -> Bool -> ...
526 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
529 Here we *must* solve the wanted (Eq a) from the given (Eq a)
530 resulting from skolemising the agument type of g. So we
531 revert to SimplCheck when going under an implication.
534 simplifyRule :: RuleName
535 -> [TcTyVar] -- Explicit skolems
536 -> WantedConstraints -- Constraints from LHS
537 -> WantedConstraints -- Constraints from RHS
538 -> TcM ([EvVar], -- LHS dicts
539 TcEvBinds, -- Evidence for LHS
540 TcEvBinds) -- Evidence for RHS
541 -- See Note [Simplifying RULE lhs constraints]
542 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
543 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
544 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
546 -- Don't quantify over equalities (judgement call here)
547 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
548 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
549 -- Dicts and implicit parameters
550 ; reportUnsolvedWantedEvVars eqs
552 -- Notice that we simplify the RHS with only the explicitly
553 -- introduced skolems, allowing the RHS to constrain any
554 -- unification variables.
555 -- Then, and only then, we call zonkQuantifiedTypeVariables
556 -- Example foo :: Ord a => a -> a
557 -- foo_spec :: Int -> Int
558 -- {-# RULE "foo" foo = foo_spec #-}
559 -- Here, it's the RHS that fixes the type variable
561 -- So we don't want to make untouchable the type
562 -- variables in the envt of the RHS, because they include
563 -- the template variables of the RULE
565 -- Hence the rather painful ad-hoc treatement here
566 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
567 ; loc <- getCtLoc (RuleSkol name)
568 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
569 Implic { ic_untch = NoUntouchables
570 , ic_env = emptyNameEnv
571 , ic_skols = mkVarSet tv_bndrs
572 , ic_scoped = panic "emitImplication"
573 , ic_given = lhs_dicts
574 , ic_wanted = rhs_wanted
575 , ic_binds = rhs_binds_var
577 ; rhs_binds2 <- readTcRef evb_ref
581 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
585 *********************************************************************************
589 ***********************************************************************************
592 simplifyCheck :: SimplContext
593 -> WantedConstraints -- Wanted
595 -- Solve a single, top-level implication constraint
596 -- e.g. typically one created from a top-level type signature
597 -- f :: forall a. [a] -> [a]
599 -- We do this even if the function has no polymorphism:
603 -- (whereas for *nested* bindings we would not create
604 -- an implication constraint for g at all.)
606 -- Fails if can't solve something in the input wanteds
607 simplifyCheck ctxt wanteds
608 = do { wanteds <- mapBagM zonkWanted wanteds
610 ; traceTc "simplifyCheck {" (vcat
611 [ ptext (sLit "wanted =") <+> ppr wanteds ])
613 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
614 solveWanteds emptyInert wanteds
616 ; traceTc "simplifyCheck }" $
617 ptext (sLit "unsolved =") <+> ppr unsolved
619 ; reportUnsolved unsolved
624 solveWanteds :: InertSet -- Given
625 -> WantedConstraints -- Wanted
626 -> TcS (CanonicalCts, -- Unsolved flats
627 Bag Implication) -- Unsolved implications
628 -- solveWanteds iterates when it is able to float equalities
629 -- out of one or more of the implications
630 solveWanteds inert wanteds
631 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
632 ; can_flats <- canWanteds $ bagToList flat_wanteds
633 ; traceTcS "solveWanteds {" $
634 vcat [ text "wanteds =" <+> ppr wanteds
635 , text "inert =" <+> ppr inert ]
636 ; (unsolved_flats, unsolved_implics)
637 <- simpl_loop 1 can_flats implic_wanteds
638 ; bb <- getTcEvBindsBag
639 ; traceTcS "solveWanteds }" $
640 vcat [ text "wanteds =" <+> ppr wanteds
641 , text "unsolved_flats =" <+> ppr unsolved_flats
642 , text "unsolved_implics =" <+> ppr unsolved_implics
643 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
645 ; return (unsolved_flats, unsolved_implics) }
648 -> CanonicalCts -- May inlude givens (in the recursive call)
650 -> TcS (CanonicalCts, Bag Implication)
651 simpl_loop n can_ws implics
653 = trace "solveWanteds: loop" $ -- Always bleat
654 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
655 ; return (can_ws, implics) }
658 = do { inert1 <- solveInteract inert can_ws
659 ; let (inert2, unsolved_flats) = extractUnsolved inert1
661 ; traceTcS "solveWanteds/done flats" $
662 vcat [ text "inerts =" <+> ppr inert2
663 , text "unsolved =" <+> ppr unsolved_flats ]
665 -- See Note [Preparing inert set for implications]
666 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
667 ; (implic_eqs, unsolved_implics)
668 <- flatMapBagPairM (solveImplication inert_for_implics) implics
670 -- Apply defaulting rules if and only if there
671 -- no floated equalities. If there are, they may
672 -- solve the remaining wanteds, so don't do defaulting.
673 ; final_eqs <- if not (isEmptyBag implic_eqs)
674 then return implic_eqs
675 else applyDefaultingRules inert2 unsolved_flats
676 -- default_eqs are *givens*, so simpl_loop may
677 -- recurse with givens in the argument
679 ; if isEmptyBag final_eqs then
680 return (unsolved_flats, unsolved_implics)
682 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
683 [ text "floated_unsolved_eqs =" <+> ppr final_eqs
684 , text "unsolved_implics = " <+> ppr unsolved_implics ]
686 (unsolved_flats `unionBags` final_eqs)
690 solveImplication :: InertSet -- Given
691 -> Implication -- Wanted
692 -> TcS (CanonicalCts, -- Unsolved unification var = type
693 Bag Implication) -- Unsolved rest (always empty or singleton)
695 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
696 -- that are of the form unification var = type
698 -- 2. Maybe a unsolved implication, empty if entirely solved!
700 -- Precondition: everything is zonked by now
701 solveImplication inert
702 imp@(Implic { ic_untch = untch
703 , ic_binds = ev_binds
706 , ic_wanted = wanteds
708 = nestImplicTcS ev_binds untch $
709 do { traceTcS "solveImplication {" (ppr imp)
712 ; can_givens <- canGivens loc givens
713 ; given_inert <- solveInteract inert can_givens
715 -- Simplify the wanteds
716 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
718 ; let (res_flat_free, res_flat_bound)
719 = floatEqualities skols givens unsolved_flats
720 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
722 ; traceTcS "solveImplication end }" $ vcat
723 [ text "res_flat_free =" <+> ppr res_flat_free
724 , text "res_flat_bound =" <+> ppr res_flat_bound
725 , text "unsolved_implics =" <+> ppr unsolved_implics ]
727 ; let res_bag | isEmptyBag unsolved = emptyBag
728 | otherwise = unitBag (imp { ic_wanted = unsolved })
730 ; return (res_flat_free, res_bag) }
732 floatEqualities :: TcTyVarSet -> [EvVar]
733 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
734 floatEqualities skols can_given wanteds
735 | hasEqualities can_given = (emptyBag, wanteds)
736 | otherwise = partitionBag is_floatable wanteds
738 is_floatable :: CanonicalCt -> Bool
739 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
740 | isMetaTyVar tv || isMetaTyVarTy ty
741 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
742 is_floatable _ = False
745 Note [Preparing inert set for implications]
746 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
747 Before solving the nested implications, we convert any unsolved flat wanteds
748 to givens, and add them to the inert set. Reasons:
749 a) In checking mode, suppresses unnecessary errors. We already have
750 on unsolved-wanted error; adding it to the givens prevents any
751 consequential errors from showing uop
752 b) More importantly, in inference mode, we are going to quantify over this
753 constraint, and we *don't* want to quantify over any constraints that
754 are deducible from it.
756 The unsolved wanteds are *canonical* but they may not be *inert*,
757 because when made into a given they might interact with other givens.
758 Hence the call to solveInteract. Example:
760 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
762 We were not able to solve (a ~w [beta]) but we can't just assume it as
763 given because the resulting set is not inert. Hence we have to do a
764 'solveInteract' step first
766 *********************************************************************************
768 * Defaulting and disamgiguation *
770 *********************************************************************************
772 Basic plan behind applyDefaulting rules:
775 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
776 For each defaultable group, do:
777 For each possible substitution for [alpha |-> tau] where `alpha' is the
778 group's variable, do:
779 1) Make up new TcEvBinds
780 2) Extend TcS with (groupVariable
781 3) given_inert <- solveOne inert (given : a ~ tau)
782 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
783 5) if unsolved == empty then
784 sneakyUnify a |-> tau
785 write the evidence bins
786 return (final_inert ++ group_constraints,[])
787 -- will contain the info (alpha |-> tau)!!
788 goto next defaultable group
789 if unsolved <> empty then
790 throw away evidence binds
791 try next substitution
792 If you've run out of substitutions for this group, too bad, you failed
794 goto next defaultable group
797 Collect all the (canonical-cts, wanteds) gathered this way.
798 - Do a solveGiven over the canonical-cts to make sure they are inert
799 ------------------------------------------------------------------------------------------
803 applyDefaultingRules :: InertSet
804 -> CanonicalCts -- All wanteds
806 -- Return some *extra* givens, which express the
807 -- type-class-default choice
809 applyDefaultingRules inert wanteds
813 = do { untch <- getUntouchables
814 ; tv_cts <- mapM (defaultTyVar untch) $
815 varSetElems (tyVarsOfCDicts wanteds)
817 ; info@(_, default_tys, _) <- getDefaultInfo
818 ; let groups = findDefaultableGroups info untch wanteds
819 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
821 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
822 , text "Type defaults =" <+> ppr deflt_cts])
824 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
827 defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
828 -- defaultTyVar is used on any un-instantiated meta type variables to
829 -- default the kind of ? and ?? etc to *. This is important to ensure
830 -- that instance declarations match. For example consider
831 -- instance Show (a->b)
832 -- foo x = show (\_ -> True)
833 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
834 -- and that won't match the typeKind (*) in the instance decl.
837 -- We look only at touchable type variables. No further constraints
838 -- are going to affect these type variables, so it's time to do it by
839 -- hand. However we aren't ready to default them fully to () or
840 -- whatever, because the type-class defaulting rules have yet to run.
842 defaultTyVar untch the_tv
843 | isTouchableMetaTyVar_InRange untch the_tv
844 , not (k `eqKind` default_k)
845 = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
846 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
847 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
848 wanted_eq = CTyEqCan { cc_id = ev
849 , cc_flavor = Wanted loc
851 , cc_rhs = better_ty }
852 ; return (unitBag wanted_eq) }
855 = return emptyCCan -- The common case
858 default_k = defaultKind k
862 findDefaultableGroups
865 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
866 -> Untouchables -- Untouchable
867 -> CanonicalCts -- Unsolved
868 -> [[(CanonicalCt,TcTyVar)]]
869 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
871 | not (performDefaulting ctxt) = []
872 | null default_tys = []
873 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
875 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
876 non_unaries :: [CanonicalCt] -- and *other* constraints
878 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
879 -- Finds unary type-class constraints
880 find_unary cc@(CDictCan { cc_tyargs = [ty] })
881 | Just tv <- tcGetTyVar_maybe ty
883 find_unary cc = Right cc -- Non unary or non dictionary
885 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
886 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
888 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
890 is_defaultable_group ds@((_,tv):_)
891 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
892 && not (tv `elemVarSet` bad_tvs)
893 && isTouchableMetaTyVar_InRange untch tv
894 && defaultable_classes [cc_class cc | (cc,_) <- ds]
895 is_defaultable_group [] = panic "defaultable_group"
897 defaultable_classes clss
898 | extended_defaults = any isInteractiveClass clss
899 | otherwise = all is_std_class clss && (any is_num_class clss)
901 -- In interactive mode, or with -XExtendedDefaultRules,
902 -- we default Show a to Show () to avoid graututious errors on "show []"
903 isInteractiveClass cls
904 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
906 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
907 -- is_num_class adds IsString to the standard numeric classes,
908 -- when -foverloaded-strings is enabled
910 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
911 -- Similarly is_std_class
913 ------------------------------
914 disambigGroup :: [Type] -- The default types
915 -> InertSet -- Given inert
916 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
917 -- sharing same type variable
920 disambigGroup [] _inert _grp
922 disambigGroup (default_ty:default_tys) inert group
923 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
924 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
925 -- We know this equality is canonical,
926 -- so we directly construct it as such
927 ; let given_eq = CTyEqCan { cc_id = ev
928 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
930 , cc_rhs = default_ty }
932 ; success <- tryTcS $
933 do { given_inert <- solveOne inert given_eq
934 ; final_inert <- solveInteract given_inert (listToBag wanteds)
935 ; let (_, unsolved) = extractUnsolved final_inert
936 ; return (isEmptyBag unsolved) }
939 True -> -- Success: record the type variable binding, and return
940 do { setWantedTyBind the_tv default_ty
941 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
942 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
943 ; return (unitBag given_eq) }
944 False -> -- Failure: try with the next type
945 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
946 ; disambigGroup default_tys inert group } }
948 ((the_ct,the_tv):_) = group
949 wanteds = map fst group
950 wanted_ev_vars = map deCanonicaliseWanted wanteds
953 Note [Avoiding spurious errors]
954 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
955 When doing the unification for defaulting, we check for skolem
956 type variables, and simply don't default them. For example:
957 f = (*) -- Monomorphic
960 Here, we get a complaint when checking the type signature for g,
961 that g isn't polymorphic enough; but then we get another one when
962 dealing with the (Num a) context arising from f's definition;
963 we try to unify a with Int (to default it), but find that it's
964 already been unified with the rigid variable from g's type sig