3 simplifyInfer, simplifySuperClass,
4 simplifyDefault, simplifyDeriv, simplifyBracket,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
22 import NameEnv ( emptyNameEnv )
28 import Class ( classKey )
29 import BasicTypes ( RuleName )
30 import Data.List ( partition )
36 *********************************************************************************
38 * External interface *
40 *********************************************************************************
43 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
44 -- Simplify top-level constraints
45 -- Usually these will be implications, when there is
46 -- nothing to quanitfy we don't wrap in a degenerate implication,
47 -- so we do that here instead
49 = simplifyCheck SimplCheck wanteds
52 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
53 simplifyInteractive wanteds
54 = simplifyCheck SimplInteractive wanteds
57 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
58 -> TcM () -- Succeeds iff the constraint is soluble
60 = do { loc <- getCtLoc DefaultOrigin
61 ; wanted <- newWantedEvVars theta
62 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
63 ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
67 simplifyBracket is used when simplifying the constraints arising from
68 a Template Haskell bracket [| ... |]. We want to check that there aren't
69 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
70 Show instance), but we aren't otherwise interested in the results.
71 Nor do we care about ambiguous dictionaries etc. We will type check
72 this bracket again at its usage site.
75 simplifyBracket :: WantedConstraints -> TcM ()
76 simplifyBracket wanteds
77 = do { zonked_wanteds <- mapBagM zonkWanted wanteds
78 ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
83 *********************************************************************************
87 ***********************************************************************************
90 simplifyDeriv :: CtOrigin
92 -> ThetaType -- Wanted
93 -> TcM ThetaType -- Needed
94 -- Given instance (wanted) => C inst_ty
95 -- Simplify 'wanted' as much as possibles
96 simplifyDeriv orig tvs theta
97 = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
98 -- One reason is that the constraint solving machinery
99 -- expects *TcTyVars* not TyVars. Another is that
100 -- when looking up instances we don't want overlap
103 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
105 ; loc <- getCtLoc orig
106 ; wanted <- newWantedEvVars (substTheta skol_subst theta)
107 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
109 ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
110 ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
112 ; let (good, bad) = partition validDerivPred $
113 foldrBag ((:) . wantedEvVarPred) [] unsolved
114 -- See Note [Exotic derived instance contexts]
115 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
117 ; reportUnsolvedDeriv bad loc
118 ; return $ substTheta subst_skol good }
121 Note [Exotic derived instance contexts]
122 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
123 In a 'derived' instance declaration, we *infer* the context. It's a
124 bit unclear what rules we should apply for this; the Haskell report is
125 silent. Obviously, constraints like (Eq a) are fine, but what about
126 data T f a = MkT (f a) deriving( Eq )
127 where we'd get an Eq (f a) constraint. That's probably fine too.
129 One could go further: consider
130 data T a b c = MkT (Foo a b c) deriving( Eq )
131 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
133 Notice that this instance (just) satisfies the Paterson termination
134 conditions. Then we *could* derive an instance decl like this:
136 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
137 even though there is no instance for (C Int a), because there just
138 *might* be an instance for, say, (C Int Bool) at a site where we
139 need the equality instance for T's.
141 However, this seems pretty exotic, and it's quite tricky to allow
142 this, and yet give sensible error messages in the (much more common)
143 case where we really want that instance decl for C.
145 So for now we simply require that the derived instance context
146 should have only type-variable constraints.
148 Here is another example:
149 data Fix f = In (f (Fix f)) deriving( Eq )
150 Here, if we are prepared to allow -XUndecidableInstances we
151 could derive the instance
152 instance Eq (f (Fix f)) => Eq (Fix f)
153 but this is so delicate that I don't think it should happen inside
154 'deriving'. If you want this, write it yourself!
156 NB: if you want to lift this condition, make sure you still meet the
157 termination conditions! If not, the deriving mechanism generates
158 larger and larger constraints. Example:
160 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
162 Note the lack of a Show instance for Succ. First we'll generate
163 instance (Show (Succ a), Show a) => Show (Seq a)
165 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
166 and so on. Instead we want to complain of no instance for (Show (Succ a)).
170 Allow constraints which consist only of type variables, with no repeats.
172 *********************************************************************************
176 ***********************************************************************************
179 simplifyInfer :: Bool -- Apply monomorphism restriction
180 -> TcTyVarSet -- These type variables are free in the
181 -- types to be generalised
183 -> TcM ([TcTyVar], -- Quantify over these type variables
184 [EvVar], -- ... and these constraints
185 TcEvBinds) -- ... binding these evidence variables
186 simplifyInfer apply_mr tau_tvs wanted
187 | isEmptyBag wanted -- Trivial case is quite common
188 = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
189 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
190 ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
191 ; return (qtvs, [], emptyTcEvBinds) }
194 = do { zonked_wanted <- mapBagM zonkWanted wanted
195 ; traceTc "simplifyInfer {" $ vcat
196 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
197 , ptext (sLit "wanted =") <+> ppr zonked_wanted
198 , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
201 -- Make a guess at the quantified type variables
202 -- Then split the constraints on the baisis of those tyvars
203 -- to avoid unnecessarily simplifying a class constraint
204 -- See Note [Avoid unecessary constraint simplification]
205 ; gbl_tvs <- tcGetGlobalTyVars
206 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
207 ; let proto_qtvs = zonked_tau_tvs `minusVarSet` gbl_tvs
208 (perhaps_bound, surely_free)
209 = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
210 ; emitConstraints surely_free
212 -- Now simplify the possibly-bound constraints
213 ; (simplified_perhaps_bound, tc_binds)
214 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
216 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
217 -- may have done some unification
218 ; gbl_tvs <- tcGetGlobalTyVars
219 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
220 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
221 ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
222 (bound, free) | apply_mr = (emptyBag, zonked_simples)
223 | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
225 ; traceTc "end simplifyInfer }" $
226 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
227 , text "wanted = " <+> ppr zonked_wanted
228 , text "qtvs = " <+> ppr qtvs
229 , text "free = " <+> ppr free
230 , text "bound = " <+> ppr bound ]
232 -- Turn the quantified meta-type variables into real type variables
233 ; emitConstraints (mapBag WcEvVar free)
234 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
235 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
236 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
238 ------------------------
239 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
240 -> TcM (Bag WantedEvVar, Bag EvBind)
241 -- We use this function when inferring the type of a function
242 -- The wanted constraints are already zonked
243 simplifyAsMuchAsPossible ctxt wanteds
244 = do { let untch = emptyVarSet
245 -- We allow ourselves to unify environment
246 -- variables; hence *no untouchables*
248 ; ((unsolved_flats, unsolved_implics), ev_binds)
249 <- runTcS ctxt untch $
250 simplifyApproxLoop 0 wanteds
253 ; reportUnsolved (emptyBag, unsolved_implics)
255 ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
256 ; return (final_wanted_evvars, ev_binds) }
259 simplifyApproxLoop :: Int -> WantedConstraints
260 -> TcS (CanonicalCts, Bag Implication)
261 simplifyApproxLoop n wanteds
263 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
265 = do { traceTcS "simplifyApproxLoop" (vcat
266 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
267 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
269 ; let (extra_flats, thiner_unsolved_implics)
270 = approximateImplications unsolved_implics
272 = mkWantedConstraints unsolved_flats thiner_unsolved_implics
274 ;-- If no new work was produced then we are done with simplifyApproxLoop
275 if isEmptyBag extra_flats
276 then do { traceTcS "simplifyApproxLoopRes" (vcat
277 [ ptext (sLit "Wanted = ") <+> ppr wanteds
278 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
279 ; return (unsolved_flats, unsolved_implics) }
281 else -- Produced new flat work wanteds, go round the loop
282 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
285 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
286 -- (wc1, impls2) <- approximateImplications impls
287 -- splits 'impls' into two parts
288 -- wc1: a bag of constraints that do not mention any skolems
289 -- impls2: a bag of *thiner* implication constraints
290 approximateImplications impls
291 = splitBag (do_implic emptyVarSet) impls
294 do_wanted :: TcTyVarSet -> WantedConstraint
295 -> (WantedConstraints, WantedConstraints)
296 do_wanted skols (WcImplic impl)
297 = let (fl_w, mb_impl) = do_implic skols impl
298 in (fl_w, mapBag WcImplic mb_impl)
299 do_wanted skols wc@(WcEvVar wev)
300 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
301 | otherwise = (emptyBag, unitBag wc)
304 do_implic :: TcTyVarSet -> Implication
305 -> (WantedConstraints, Bag Implication)
306 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
307 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
308 else unitBag impl{ ic_wanted = rest_wanted } )
310 (floatable_wanted, rest_wanted)
311 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
314 splitBag :: (a -> (WantedConstraints, Bag a))
315 -> Bag a -> (WantedConstraints, Bag a)
316 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
319 = (wcs `unionBags` b1, imps `unionBags` b2)
325 findQuantifiedTyVars :: Bool -- Apply the MR
326 -> Bag WantedEvVar -- Simplified constraints from RHS
327 -> TyVarSet -- Free in tau-type of definition
328 -> TyVarSet -- Free in the envt
329 -> TyVarSet -- Quantify over these
331 findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
332 | isEmptyBag wanteds = init_tvs
333 | apply_mr = init_tvs `minusVarSet` constrained_tvs
334 | otherwise = fixVarSet mk_next init_tvs
336 init_tvs = tau_tvs `minusVarSet` gbl_tvs
337 mk_next tvs = foldrBag grow_one tvs wanteds
339 grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
341 extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
343 constrained_tvs = tyVarsOfWantedEvVars wanteds
346 quantifyMe :: TyVarSet -- Quantifying over these
348 -> Bool -- True <=> quantify over this wanted
350 | isIPPred pred = True -- Note [Inheriting implicit parameters]
351 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
353 pred = wantedEvVarPred wev
355 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
356 quantifyMeWC qtvs (WcImplic implic)
357 = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted implic)
358 quantifyMeWC qtvs (WcEvVar wev)
359 = quantifyMe qtvs wev
362 Note [Avoid unecessary constraint simplification]
363 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
364 When inferring the type of a let-binding, with simplifyInfer,
365 try to avoid unnecessariliy simplifying class constraints.
366 Doing so aids sharing, but it also helps with delicate
368 instance C t => C [t] where ..
370 f x = let g y = ...(constraint C [t])...
372 When inferring a type for 'g', we don't want to apply the
373 instance decl, because then we can't satisfy (C t). So we
374 just notice that g isn't quantified over 't' and partition
375 the contraints before simplifying.
377 This only half-works, but then let-generalisation only half-works.
380 Note [Inheriting implicit parameters]
381 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
386 where f is *not* a top-level binding.
387 From the RHS of f we'll get the constraint (?y::Int).
388 There are two types we might infer for f:
392 (so we get ?y from the context of f's definition), or
394 f :: (?y::Int) => Int -> Int
396 At first you might think the first was better, becuase then
397 ?y behaves like a free variable of the definition, rather than
398 having to be passed at each call site. But of course, the WHOLE
399 IDEA is that ?y should be passed at each call site (that's what
400 dynamic binding means) so we'd better infer the second.
402 BOTTOM LINE: when *inferring types* you *must* quantify
403 over implicit parameters. See the predicate isFreeWhenInferring.
406 *********************************************************************************
410 ***********************************************************************************
412 When constructing evidence for superclasses in an instance declaration,
413 * we MUST have the "self" dictionary available, but
414 * we must NOT have its superclasses derived from "self"
416 Moreover, we must *completely* solve the constraints right now,
417 not wrap them in an implication constraint to solve later. Why?
418 Because when that implication constraint is solved there may
419 be some unrelated other solved top-level constraints that
420 recursively depend on the superclass we are building. Consider
421 class Ord a => C a where
422 instance C [Int] where ...
425 dCListInt = MkC $cNum ...
427 $cNum :: Ord [Int] -- The superclass
428 $cNum = let self = dCListInt in <solve Ord [Int]>
430 Now, if there is some *other* top-level constraint solved
434 we must not solve the (Ord [Int]) wanted from foo!!
437 simplifySuperClass :: EvVar -- The "self" dictionary
440 simplifySuperClass self wanteds
441 = do { wanteds <- mapBagM zonkWanted wanteds
442 ; loc <- getCtLoc NoScSkol
443 ; (unsolved, ev_binds)
444 <- runTcS SimplCheck emptyVarSet $
445 do { can_self <- canGivens loc [self]
446 ; let inert = foldlBag updInertSet emptyInert can_self
447 -- No need for solveInteract; we know it's inert
449 ; solveWanteds inert wanteds }
451 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
452 reportUnsolved unsolved }
456 *********************************************************************************
460 ***********************************************************************************
462 Note [Simplifying RULE lhs constraints]
463 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
464 On the LHS of transformation rules we only simplify only equalitis,
465 but not dictionaries. We want to keep dictionaries unsimplified, to
466 serve as the available stuff for the RHS of the rule. We *do* want to
467 simplify equalities, however, to detect ill-typed rules that cannot be
470 Implementation: the TcSFlags carried by the TcSMonad controls the
471 amount of simplification, so simplifyRuleLhs just sets the flag
474 Example. Consider the following left-hand side of a rule
475 f (x == y) (y > z) = ...
476 If we typecheck this expression we get constraints
477 d1 :: Ord a, d2 :: Eq a
478 We do NOT want to "simplify" to the LHS
479 forall x::a, y::a, z::a, d1::Ord a.
480 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
482 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
483 f ((==) d2 x y) ((>) d1 y z) = ...
485 Here is another example:
486 fromIntegral :: (Integral a, Num b) => a -> b
487 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
488 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
489 we *dont* want to get
491 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
492 because the scsel will mess up RULE matching. Instead we want
493 forall dIntegralInt, dNumInt.
494 fromIntegral Int Int dIntegralInt dNumInt = id Int
497 g (x == y) (y == z) = ..
498 where the two dictionaries are *identical*, we do NOT WANT
499 forall x::a, y::a, z::a, d1::Eq a
500 f ((==) d1 x y) ((>) d1 y z) = ...
501 because that will only match if the dict args are (visibly) equal.
502 Instead we want to quantify over the dictionaries separately.
504 In short, simplifyRuleLhs must *only* squash equalities, leaving
505 all dicts unchanged, with absolutely no sharing.
507 HOWEVER, under a nested implication things are different
509 f :: (forall a. Eq a => a->a) -> Bool -> ...
510 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
513 Here we *must* solve the wanted (Eq a) from the given (Eq a)
514 resulting from skolemising the agument type of g. So we
515 revert to SimplCheck when going under an implication.
518 simplifyRule :: RuleName
519 -> [TcTyVar] -- Explicit skolems
520 -> WantedConstraints -- Constraints from LHS
521 -> WantedConstraints -- Constraints from RHS
522 -> TcM ([EvVar], -- LHS dicts
523 TcEvBinds, -- Evidence for LHS
524 TcEvBinds) -- Evidence for RHS
525 -- See Note [Simplifying RULE lhs constraints]
526 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
527 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
528 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
530 -- Don't quantify over equalities (judgement call here)
531 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
532 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
533 -- Dicts and implicit parameters
534 ; reportUnsolvedWantedEvVars eqs
536 -- Notice that we simplify the RHS with only the explicitly
537 -- introduced skolems, allowing the RHS to constrain any
538 -- unification variables.
539 -- Then, and only then, we call zonkQuantifiedTypeVariables
540 -- Example foo :: Ord a => a -> a
541 -- foo_spec :: Int -> Int
542 -- {-# RULE "foo" foo = foo_spec #-}
543 -- Here, it's the RHS that fixes the type variable
545 -- So we don't want to make untouchable the type
546 -- variables in the envt of the RHS, because they include
547 -- the template variables of the RULE
549 -- Hence the rather painful ad-hoc treatement here
550 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
551 ; loc <- getCtLoc (RuleSkol name)
552 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
553 Implic { ic_untch = emptyVarSet -- No untouchables
554 , ic_env = emptyNameEnv
555 , ic_skols = mkVarSet tv_bndrs
556 , ic_scoped = panic "emitImplication"
557 , ic_given = lhs_dicts
558 , ic_wanted = rhs_wanted
559 , ic_binds = rhs_binds_var
561 ; rhs_binds2 <- readTcRef evb_ref
565 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
569 *********************************************************************************
573 ***********************************************************************************
576 simplifyCheck :: SimplContext
577 -> WantedConstraints -- Wanted
579 -- Solve a single, top-level implication constraint
580 -- e.g. typically one created from a top-level type signature
581 -- f :: forall a. [a] -> [a]
583 -- We do this even if the function has no polymorphism:
587 -- (whereas for *nested* bindings we would not create
588 -- an implication constraint for g at all.)
590 -- Fails if can't solve something in the input wanteds
591 simplifyCheck ctxt wanteds
592 = do { wanteds <- mapBagM zonkWanted wanteds
594 ; traceTc "simplifyCheck {" (vcat
595 [ ptext (sLit "wanted =") <+> ppr wanteds ])
597 ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
598 solveWanteds emptyInert wanteds
600 ; traceTc "simplifyCheck }" $
601 ptext (sLit "unsolved =") <+> ppr unsolved
603 ; reportUnsolved unsolved
608 solveWanteds :: InertSet -- Given
609 -> WantedConstraints -- Wanted
610 -> TcS (CanonicalCts, -- Unsolved flats
611 Bag Implication) -- Unsolved implications
612 -- solveWanteds iterates when it is able to float equalities
613 -- out of one or more of the implications
614 solveWanteds inert wanteds
615 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
616 ; can_flats <- canWanteds $ bagToList flat_wanteds
617 ; traceTcS "solveWanteds {" $
618 vcat [ text "wanteds =" <+> ppr wanteds
619 , text "inert =" <+> ppr inert ]
620 ; (unsolved_flats, unsolved_implics)
621 <- simpl_loop 1 can_flats implic_wanteds
622 ; traceTcS "solveWanteds }" $
623 vcat [ text "wanteds =" <+> ppr wanteds
624 , text "unsolved_flats =" <+> ppr unsolved_flats
625 , text "unsolved_implics =" <+> ppr unsolved_implics ]
626 ; return (unsolved_flats, unsolved_implics) }
629 -> CanonicalCts -- May inlude givens (in the recursive call)
631 -> TcS (CanonicalCts, Bag Implication)
632 simpl_loop n can_ws implics
634 = trace "solveWanteds: loop" $ -- Always bleat
635 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
636 ; return (can_ws, implics) }
639 = do { inert1 <- solveInteract inert can_ws
640 ; let (inert2, unsolved_flats) = extractUnsolved inert1
642 ; traceTcS "solveWanteds/done flats" $
643 vcat [ text "inerts =" <+> ppr inert2
644 , text "unsolved =" <+> ppr unsolved_flats ]
646 -- See Note [Preparing inert set for implications]
647 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
648 ; (implic_eqs, unsolved_implics)
649 <- flatMapBagPairM (solveImplication inert_for_implics) implics
651 -- Apply defaulting rules if and only if there
652 -- no floated equalities. If there are, they may
653 -- solve the remaining wanteds, so don't do defaulting.
654 ; final_eqs <- if not (isEmptyBag implic_eqs)
655 then return implic_eqs
656 else applyDefaultingRules inert2 unsolved_flats
657 -- default_eqs are *givens*, so simpl_loop may
658 -- recurse with givens in the argument
660 ; if isEmptyBag final_eqs then
661 return (unsolved_flats, unsolved_implics)
663 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
664 [ text "floated_unsolved_eqs =" <+> ppr final_eqs
665 , text "unsolved_implics = " <+> ppr unsolved_implics ]
667 (unsolved_flats `unionBags` final_eqs)
671 solveImplication :: InertSet -- Given
672 -> Implication -- Wanted
673 -> TcS (CanonicalCts, -- Unsolved unification var = type
674 Bag Implication) -- Unsolved rest (always empty or singleton)
676 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
677 -- that are of the form unification var = type
679 -- 2. Maybe a unsolved implication, empty if entirely solved!
681 -- Precondition: everything is zonked by now
682 solveImplication inert
683 imp@(Implic { ic_untch = untch
684 , ic_binds = ev_binds
687 , ic_wanted = wanteds
689 = nestImplicTcS ev_binds untch $
690 do { traceTcS "solveImplication {" (ppr imp)
693 ; can_givens <- canGivens loc givens
694 ; given_inert <- solveInteract inert can_givens
696 -- Simplify the wanteds
697 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
699 ; let (res_flat_free, res_flat_bound)
700 = floatEqualities skols givens unsolved_flats
701 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
703 ; traceTcS "solveImplication end }" $ vcat
704 [ text "res_flat_free =" <+> ppr res_flat_free
705 , text "res_flat_bound =" <+> ppr res_flat_bound
706 , text "unsolved_implics =" <+> ppr unsolved_implics ]
708 ; let res_bag | isEmptyBag unsolved = emptyBag
709 | otherwise = unitBag (imp { ic_wanted = unsolved })
711 ; return (res_flat_free, res_bag) }
713 floatEqualities :: TcTyVarSet -> [EvVar]
714 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
715 floatEqualities skols can_given wanteds
716 | hasEqualities can_given = (emptyBag, wanteds)
717 | otherwise = partitionBag is_floatable wanteds
719 is_floatable :: CanonicalCt -> Bool
720 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
721 | isMetaTyVar tv || isMetaTyVarTy ty
722 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
723 is_floatable _ = False
726 Note [Preparing inert set for implications]
727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
728 Before solving the nested implications, we convert any unsolved flat wanteds
729 to givens, and add them to the inert set. Reasons:
730 a) In checking mode, suppresses unnecessary errors. We already have
731 on unsolved-wanted error; adding it to the givens prevents any
732 consequential errors from showing uop
733 b) More importantly, in inference mode, we are going to quantify over this
734 constraint, and we *don't* want to quantify over any constraints that
735 are deducible from it.
737 The unsolved wanteds are *canonical* but they may not be *inert*,
738 because when made into a given they might interact with other givens.
739 Hence the call to solveInteract. Example:
741 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
743 We were not able to solve (a ~w [beta]) but we can't just assume it as
744 given because the resulting set is not inert. Hence we have to do a
745 'solveInteract' step first
747 *********************************************************************************
749 * Defaulting and disamgiguation *
751 *********************************************************************************
753 Basic plan behind applyDefaulting rules:
756 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
757 For each defaultable group, do:
758 For each possible substitution for [alpha |-> tau] where `alpha' is the
759 group's variable, do:
760 1) Make up new TcEvBinds
761 2) Extend TcS with (groupVariable
762 3) given_inert <- solveOne inert (given : a ~ tau)
763 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
764 5) if unsolved == empty then
765 sneakyUnify a |-> tau
766 write the evidence bins
767 return (final_inert ++ group_constraints,[])
768 -- will contain the info (alpha |-> tau)!!
769 goto next defaultable group
770 if unsolved <> empty then
771 throw away evidence binds
772 try next substitution
773 If you've run out of substitutions for this group, too bad, you failed
775 goto next defaultable group
778 Collect all the (canonical-cts, wanteds) gathered this way.
779 - Do a solveGiven over the canonical-cts to make sure they are inert
780 ------------------------------------------------------------------------------------------
784 applyDefaultingRules :: InertSet
785 -> CanonicalCts -- All wanteds
787 -- Return some *extra* givens, which express the
788 -- type-class-default choice
790 applyDefaultingRules inert wanteds
794 = do { untch <- getUntouchablesTcS
795 ; tv_cts <- mapM (defaultTyVar untch) $
796 varSetElems (tyVarsOfCanonicals wanteds)
798 ; info@(_, default_tys, _) <- getDefaultInfo
799 ; let groups = findDefaultableGroups info untch wanteds
800 ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
802 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
803 , text "Type defaults =" <+> ppr deflt_cts])
805 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
808 defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
809 -- defaultTyVar is used on any un-instantiated meta type variables to
810 -- default the kind of ? and ?? etc to *. This is important to ensure
811 -- that instance declarations match. For example consider
812 -- instance Show (a->b)
813 -- foo x = show (\_ -> True)
814 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
815 -- and that won't match the typeKind (*) in the instance decl.
818 -- We look only at touchable type variables. No further constraints
819 -- are going to affect these type variables, so it's time to do it by
820 -- hand. However we aren't ready to default them fully to () or
821 -- whatever, because the type-class defaulting rules have yet to run.
823 defaultTyVar untch the_tv
825 , not (the_tv `elemVarSet` untch)
826 , not (k `eqKind` default_k)
827 = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
828 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
829 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
830 wanted_eq = CTyEqCan { cc_id = ev
831 , cc_flavor = Wanted loc
833 , cc_rhs = better_ty }
834 ; return (unitBag wanted_eq) }
837 = return emptyCCan -- The common case
840 default_k = defaultKind k
844 findDefaultableGroups
847 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
848 -> TcTyVarSet -- Untouchable
849 -> CanonicalCts -- Unsolved
850 -> [[(CanonicalCt,TcTyVar)]]
851 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
853 | not (performDefaulting ctxt) = []
854 | null default_tys = []
855 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
857 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
858 non_unaries :: [CanonicalCt] -- and *other* constraints
860 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
861 -- Finds unary type-class constraints
862 find_unary cc@(CDictCan { cc_tyargs = [ty] })
863 | Just tv <- tcGetTyVar_maybe ty
865 find_unary cc = Right cc -- Non unary or non dictionary
867 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
868 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
870 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
872 is_defaultable_group ds@((_,tv):_)
873 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
874 && not (tv `elemVarSet` bad_tvs)
875 && not (tv `elemVarSet` untch) -- Non untouchable
876 && defaultable_classes [cc_class cc | (cc,_) <- ds]
877 is_defaultable_group [] = panic "defaultable_group"
879 defaultable_classes clss
880 | extended_defaults = any isInteractiveClass clss
881 | otherwise = all is_std_class clss && (any is_num_class clss)
883 -- In interactive mode, or with -XExtendedDefaultRules,
884 -- we default Show a to Show () to avoid graututious errors on "show []"
885 isInteractiveClass cls
886 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
888 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
889 -- is_num_class adds IsString to the standard numeric classes,
890 -- when -foverloaded-strings is enabled
892 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
893 -- Similarly is_std_class
895 ------------------------------
896 disambigGroup :: [Type] -- The default types
897 -> TcTyVarSet -- Untouchables
898 -> InertSet -- Given inert
899 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
900 -- sharing same type variable
903 disambigGroup [] _inert _untch _grp
905 disambigGroup (default_ty:default_tys) untch inert group
906 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
907 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
908 -- We know this equality is canonical,
909 -- so we directly construct it as such
910 ; let given_eq = CTyEqCan { cc_id = ev
911 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
913 , cc_rhs = default_ty }
915 ; success <- tryTcS (extendVarSet untch the_tv) $
916 do { given_inert <- solveOne inert given_eq
917 ; final_inert <- solveInteract given_inert (listToBag wanteds)
918 ; let (_, unsolved) = extractUnsolved final_inert
919 ; return (isEmptyBag unsolved) }
922 True -> -- Success: record the type variable binding, and return
923 do { setWantedTyBind the_tv default_ty
924 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
925 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
926 ; return (unitBag given_eq) }
927 False -> -- Failure: try with the next type
928 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
929 ; disambigGroup default_tys untch inert group } }
931 ((the_ct,the_tv):_) = group
932 wanteds = map fst group
933 wanted_ev_vars = map deCanonicaliseWanted wanteds
936 Note [Avoiding spurious errors]
937 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
938 When doing the unification for defaulting, we check for skolem
939 type variables, and simply don't default them. For example:
940 f = (*) -- Monomorphic
943 Here, we get a complaint when checking the type signature for g,
944 that g isn't polymorphic enough; but then we get another one when
945 dealing with the (Num a) context arising from f's definition;
946 we try to unify a with Int (to default it), but find that it's
947 already been unified with the rigid variable from g's type sig