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 recoverTcS (return (emptyBag, emptyBag)) $
710 -- Recover from nested failures. Even the top level is
711 -- just a bunch of implications, so failing at the first
713 do { traceTcS "solveImplication {" (ppr imp)
716 ; can_givens <- canGivens loc givens
717 ; given_inert <- solveInteract inert can_givens
719 -- Simplify the wanteds
720 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
722 ; let (res_flat_free, res_flat_bound)
723 = floatEqualities skols givens unsolved_flats
724 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
726 ; traceTcS "solveImplication end }" $ vcat
727 [ text "res_flat_free =" <+> ppr res_flat_free
728 , text "res_flat_bound =" <+> ppr res_flat_bound
729 , text "unsolved_implics =" <+> ppr unsolved_implics ]
731 ; let res_bag | isEmptyBag unsolved = emptyBag
732 | otherwise = unitBag (imp { ic_wanted = unsolved })
734 ; return (res_flat_free, res_bag) }
736 floatEqualities :: TcTyVarSet -> [EvVar]
737 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
738 floatEqualities skols can_given wanteds
739 | hasEqualities can_given = (emptyBag, wanteds)
740 | otherwise = partitionBag is_floatable wanteds
742 is_floatable :: CanonicalCt -> Bool
743 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
744 | isMetaTyVar tv || isMetaTyVarTy ty
745 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
746 is_floatable _ = False
749 Note [Preparing inert set for implications]
750 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
751 Before solving the nested implications, we convert any unsolved flat wanteds
752 to givens, and add them to the inert set. Reasons:
753 a) In checking mode, suppresses unnecessary errors. We already have
754 on unsolved-wanted error; adding it to the givens prevents any
755 consequential errors from showing uop
756 b) More importantly, in inference mode, we are going to quantify over this
757 constraint, and we *don't* want to quantify over any constraints that
758 are deducible from it.
760 The unsolved wanteds are *canonical* but they may not be *inert*,
761 because when made into a given they might interact with other givens.
762 Hence the call to solveInteract. Example:
764 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
766 We were not able to solve (a ~w [beta]) but we can't just assume it as
767 given because the resulting set is not inert. Hence we have to do a
768 'solveInteract' step first
770 *********************************************************************************
772 * Defaulting and disamgiguation *
774 *********************************************************************************
776 Basic plan behind applyDefaulting rules:
779 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
780 For each defaultable group, do:
781 For each possible substitution for [alpha |-> tau] where `alpha' is the
782 group's variable, do:
783 1) Make up new TcEvBinds
784 2) Extend TcS with (groupVariable
785 3) given_inert <- solveOne inert (given : a ~ tau)
786 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
787 5) if unsolved == empty then
788 sneakyUnify a |-> tau
789 write the evidence bins
790 return (final_inert ++ group_constraints,[])
791 -- will contain the info (alpha |-> tau)!!
792 goto next defaultable group
793 if unsolved <> empty then
794 throw away evidence binds
795 try next substitution
796 If you've run out of substitutions for this group, too bad, you failed
798 goto next defaultable group
801 Collect all the (canonical-cts, wanteds) gathered this way.
802 - Do a solveGiven over the canonical-cts to make sure they are inert
803 ------------------------------------------------------------------------------------------
807 applyDefaultingRules :: InertSet
808 -> CanonicalCts -- All wanteds
810 -- Return some *extra* givens, which express the
811 -- type-class-default choice
813 applyDefaultingRules inert wanteds
817 = do { untch <- getUntouchables
818 ; tv_cts <- mapM (defaultTyVar untch) $
819 varSetElems (tyVarsOfCDicts wanteds)
821 ; info@(_, default_tys, _) <- getDefaultInfo
822 ; let groups = findDefaultableGroups info untch wanteds
823 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
825 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
826 , text "Type defaults =" <+> ppr deflt_cts])
828 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
831 defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
832 -- defaultTyVar is used on any un-instantiated meta type variables to
833 -- default the kind of ? and ?? etc to *. This is important to ensure
834 -- that instance declarations match. For example consider
835 -- instance Show (a->b)
836 -- foo x = show (\_ -> True)
837 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
838 -- and that won't match the typeKind (*) in the instance decl.
841 -- We look only at touchable type variables. No further constraints
842 -- are going to affect these type variables, so it's time to do it by
843 -- hand. However we aren't ready to default them fully to () or
844 -- whatever, because the type-class defaulting rules have yet to run.
846 defaultTyVar untch the_tv
847 | isTouchableMetaTyVar_InRange untch the_tv
848 , not (k `eqKind` default_k)
849 = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
850 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
851 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
852 wanted_eq = CTyEqCan { cc_id = ev
853 , cc_flavor = Wanted loc
855 , cc_rhs = better_ty }
856 ; return (unitBag wanted_eq) }
859 = return emptyCCan -- The common case
862 default_k = defaultKind k
866 findDefaultableGroups
869 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
870 -> Untouchables -- Untouchable
871 -> CanonicalCts -- Unsolved
872 -> [[(CanonicalCt,TcTyVar)]]
873 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
875 | not (performDefaulting ctxt) = []
876 | null default_tys = []
877 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
879 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
880 non_unaries :: [CanonicalCt] -- and *other* constraints
882 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
883 -- Finds unary type-class constraints
884 find_unary cc@(CDictCan { cc_tyargs = [ty] })
885 | Just tv <- tcGetTyVar_maybe ty
887 find_unary cc = Right cc -- Non unary or non dictionary
889 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
890 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
892 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
894 is_defaultable_group ds@((_,tv):_)
895 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
896 && not (tv `elemVarSet` bad_tvs)
897 && isTouchableMetaTyVar_InRange untch tv
898 && defaultable_classes [cc_class cc | (cc,_) <- ds]
899 is_defaultable_group [] = panic "defaultable_group"
901 defaultable_classes clss
902 | extended_defaults = any isInteractiveClass clss
903 | otherwise = all is_std_class clss && (any is_num_class clss)
905 -- In interactive mode, or with -XExtendedDefaultRules,
906 -- we default Show a to Show () to avoid graututious errors on "show []"
907 isInteractiveClass cls
908 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
910 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
911 -- is_num_class adds IsString to the standard numeric classes,
912 -- when -foverloaded-strings is enabled
914 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
915 -- Similarly is_std_class
917 ------------------------------
918 disambigGroup :: [Type] -- The default types
919 -> InertSet -- Given inert
920 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
921 -- sharing same type variable
924 disambigGroup [] _inert _grp
926 disambigGroup (default_ty:default_tys) inert group
927 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
928 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
929 -- We know this equality is canonical,
930 -- so we directly construct it as such
931 ; let given_eq = CTyEqCan { cc_id = ev
932 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
934 , cc_rhs = default_ty }
936 ; success <- tryTcS $
937 do { given_inert <- solveOne inert given_eq
938 ; final_inert <- solveInteract given_inert (listToBag wanteds)
939 ; let (_, unsolved) = extractUnsolved final_inert
940 ; return (isEmptyBag unsolved) }
943 True -> -- Success: record the type variable binding, and return
944 do { setWantedTyBind the_tv default_ty
945 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
946 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
947 ; return (unitBag given_eq) }
948 False -> -- Failure: try with the next type
949 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
950 ; disambigGroup default_tys inert group } }
952 ((the_ct,the_tv):_) = group
953 wanteds = map fst group
954 wanted_ev_vars = map deCanonicaliseWanted wanteds
957 Note [Avoiding spurious errors]
958 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
959 When doing the unification for defaulting, we check for skolem
960 type variables, and simply don't default them. For example:
961 f = (*) -- Monomorphic
964 Here, we get a complaint when checking the type signature for g,
965 that g isn't polymorphic enough; but then we get another one when
966 dealing with the (Num a) context arising from f's definition;
967 we try to unify a with Int (to default it), but find that it's
968 already been unified with the rigid variable from g's type sig