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
213 ; emitConstraints surely_free
214 ; traceTc "sinf" (ppr proto_qtvs $$ ppr perhaps_bound $$ ppr surely_free)
216 -- Now simplify the possibly-bound constraints
217 ; (simplified_perhaps_bound, tc_binds)
218 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
220 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
221 -- may have done some unification
222 ; gbl_tvs <- tcGetGlobalTyVars
223 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
224 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
225 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
226 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
227 constrained_tvs = tyVarsOfWantedEvVars zonked_simples
228 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
229 (final_qtvs, (bound, free))
230 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
231 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
233 ; traceTc "end simplifyInfer }" $
234 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
235 , text "wanted = " <+> ppr zonked_wanted
236 , text "qtvs = " <+> ppr final_qtvs
237 , text "free = " <+> ppr free
238 , text "bound = " <+> ppr bound ]
240 -- Turn the quantified meta-type variables into real type variables
241 ; emitConstraints (mapBag WcEvVar free)
242 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
243 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
244 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
246 ------------------------
247 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
248 -> TcM (Bag WantedEvVar, Bag EvBind)
249 -- We use this function when inferring the type of a function
250 -- The wanted constraints are already zonked
251 simplifyAsMuchAsPossible ctxt wanteds
252 = do { let untch = NoUntouchables
253 -- We allow ourselves to unify environment
254 -- variables; hence *no untouchables*
256 ; ((unsolved_flats, unsolved_implics), ev_binds)
257 <- runTcS ctxt untch $
258 simplifyApproxLoop 0 wanteds
261 ; reportUnsolved (emptyBag, unsolved_implics)
263 ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
264 ; return (final_wanted_evvars, ev_binds) }
267 simplifyApproxLoop :: Int -> WantedConstraints
268 -> TcS (CanonicalCts, Bag Implication)
269 simplifyApproxLoop n wanteds
271 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
273 = do { traceTcS "simplifyApproxLoop" (vcat
274 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
275 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
277 ; let (extra_flats, thiner_unsolved_implics)
278 = approximateImplications unsolved_implics
280 = mkWantedConstraints unsolved_flats thiner_unsolved_implics
282 ;-- If no new work was produced then we are done with simplifyApproxLoop
283 if isEmptyBag extra_flats
284 then do { traceTcS "simplifyApproxLoopRes" (vcat
285 [ ptext (sLit "Wanted = ") <+> ppr wanteds
286 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
287 ; return (unsolved_flats, unsolved_implics) }
289 else -- Produced new flat work wanteds, go round the loop
290 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
293 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
294 -- (wc1, impls2) <- approximateImplications impls
295 -- splits 'impls' into two parts
296 -- wc1: a bag of constraints that do not mention any skolems
297 -- impls2: a bag of *thiner* implication constraints
298 approximateImplications impls
299 = splitBag (do_implic emptyVarSet) impls
302 do_wanted :: TcTyVarSet -> WantedConstraint
303 -> (WantedConstraints, WantedConstraints)
304 do_wanted skols (WcImplic impl)
305 = let (fl_w, mb_impl) = do_implic skols impl
306 in (fl_w, mapBag WcImplic mb_impl)
307 do_wanted skols wc@(WcEvVar wev)
308 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
309 | otherwise = (emptyBag, unitBag wc)
312 do_implic :: TcTyVarSet -> Implication
313 -> (WantedConstraints, Bag Implication)
314 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
315 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
316 else unitBag impl{ ic_wanted = rest_wanted } )
318 (floatable_wanted, rest_wanted)
319 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
322 splitBag :: (a -> (WantedConstraints, Bag a))
323 -> Bag a -> (WantedConstraints, Bag a)
324 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
327 = (wcs `unionBags` b1, imps `unionBags` b2)
333 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
334 growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
335 growWanteds gbl_tvs ws tvs
336 | isEmptyBag ws = tvs
337 | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
338 growWantedEVs gbl_tvs ws tvs
339 | isEmptyBag ws = tvs
340 | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
342 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
343 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
344 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
345 -- X-constraint 'wanted', nuking the 'gbls' at each stage
346 growWantedEV gbl_tvs wev tvs
347 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
349 ev_tvs = growPredTyVars (wantedEvVarPred wev) tvs
351 growWanted gbl_tvs (WcEvVar wev) tvs
352 = growWantedEV gbl_tvs wev tvs
353 growWanted gbl_tvs (WcImplic implic) tvs
354 = foldrBag (growWanted (gbl_tvs `unionVarSet` ic_skols implic))
355 tvs (ic_wanted implic)
358 quantifyMe :: TyVarSet -- Quantifying over these
360 -> Bool -- True <=> quantify over this wanted
362 | isIPPred pred = True -- Note [Inheriting implicit parameters]
363 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
365 pred = wantedEvVarPred wev
367 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
368 quantifyMeWC qtvs (WcImplic implic)
369 = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted implic)
370 quantifyMeWC qtvs (WcEvVar wev)
371 = quantifyMe qtvs wev
374 Note [Avoid unecessary constraint simplification]
375 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
376 When inferring the type of a let-binding, with simplifyInfer,
377 try to avoid unnecessariliy simplifying class constraints.
378 Doing so aids sharing, but it also helps with delicate
380 instance C t => C [t] where ..
382 f x = let g y = ...(constraint C [t])...
384 When inferring a type for 'g', we don't want to apply the
385 instance decl, because then we can't satisfy (C t). So we
386 just notice that g isn't quantified over 't' and partition
387 the contraints before simplifying.
389 This only half-works, but then let-generalisation only half-works.
392 Note [Inheriting implicit parameters]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
398 where f is *not* a top-level binding.
399 From the RHS of f we'll get the constraint (?y::Int).
400 There are two types we might infer for f:
404 (so we get ?y from the context of f's definition), or
406 f :: (?y::Int) => Int -> Int
408 At first you might think the first was better, becuase then
409 ?y behaves like a free variable of the definition, rather than
410 having to be passed at each call site. But of course, the WHOLE
411 IDEA is that ?y should be passed at each call site (that's what
412 dynamic binding means) so we'd better infer the second.
414 BOTTOM LINE: when *inferring types* you *must* quantify
415 over implicit parameters. See the predicate isFreeWhenInferring.
418 *********************************************************************************
422 ***********************************************************************************
424 When constructing evidence for superclasses in an instance declaration,
425 * we MUST have the "self" dictionary available, but
426 * we must NOT have its superclasses derived from "self"
428 Moreover, we must *completely* solve the constraints right now,
429 not wrap them in an implication constraint to solve later. Why?
430 Because when that implication constraint is solved there may
431 be some unrelated other solved top-level constraints that
432 recursively depend on the superclass we are building. Consider
433 class Ord a => C a where
434 instance C [Int] where ...
437 dCListInt = MkC $cNum ...
439 $cNum :: Ord [Int] -- The superclass
440 $cNum = let self = dCListInt in <solve Ord [Int]>
442 Now, if there is some *other* top-level constraint solved
446 we must not solve the (Ord [Int]) wanted from foo!!
449 simplifySuperClass :: EvVar -- The "self" dictionary
452 simplifySuperClass self wanteds
453 = do { wanteds <- mapBagM zonkWanted wanteds
454 ; loc <- getCtLoc NoScSkol
455 ; (unsolved, ev_binds)
456 <- runTcS SimplCheck NoUntouchables $
457 do { can_self <- canGivens loc [self]
458 ; let inert = foldlBag updInertSet emptyInert can_self
459 -- No need for solveInteract; we know it's inert
461 ; solveWanteds inert wanteds }
463 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
464 reportUnsolved unsolved }
468 *********************************************************************************
472 ***********************************************************************************
474 Note [Simplifying RULE lhs constraints]
475 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
476 On the LHS of transformation rules we only simplify only equalitis,
477 but not dictionaries. We want to keep dictionaries unsimplified, to
478 serve as the available stuff for the RHS of the rule. We *do* want to
479 simplify equalities, however, to detect ill-typed rules that cannot be
482 Implementation: the TcSFlags carried by the TcSMonad controls the
483 amount of simplification, so simplifyRuleLhs just sets the flag
486 Example. Consider the following left-hand side of a rule
487 f (x == y) (y > z) = ...
488 If we typecheck this expression we get constraints
489 d1 :: Ord a, d2 :: Eq a
490 We do NOT want to "simplify" to the LHS
491 forall x::a, y::a, z::a, d1::Ord a.
492 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
494 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
495 f ((==) d2 x y) ((>) d1 y z) = ...
497 Here is another example:
498 fromIntegral :: (Integral a, Num b) => a -> b
499 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
500 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
501 we *dont* want to get
503 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
504 because the scsel will mess up RULE matching. Instead we want
505 forall dIntegralInt, dNumInt.
506 fromIntegral Int Int dIntegralInt dNumInt = id Int
509 g (x == y) (y == z) = ..
510 where the two dictionaries are *identical*, we do NOT WANT
511 forall x::a, y::a, z::a, d1::Eq a
512 f ((==) d1 x y) ((>) d1 y z) = ...
513 because that will only match if the dict args are (visibly) equal.
514 Instead we want to quantify over the dictionaries separately.
516 In short, simplifyRuleLhs must *only* squash equalities, leaving
517 all dicts unchanged, with absolutely no sharing.
519 HOWEVER, under a nested implication things are different
521 f :: (forall a. Eq a => a->a) -> Bool -> ...
522 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
525 Here we *must* solve the wanted (Eq a) from the given (Eq a)
526 resulting from skolemising the agument type of g. So we
527 revert to SimplCheck when going under an implication.
530 simplifyRule :: RuleName
531 -> [TcTyVar] -- Explicit skolems
532 -> WantedConstraints -- Constraints from LHS
533 -> WantedConstraints -- Constraints from RHS
534 -> TcM ([EvVar], -- LHS dicts
535 TcEvBinds, -- Evidence for LHS
536 TcEvBinds) -- Evidence for RHS
537 -- See Note [Simplifying RULE lhs constraints]
538 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
539 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
540 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
542 -- Don't quantify over equalities (judgement call here)
543 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
544 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
545 -- Dicts and implicit parameters
546 ; reportUnsolvedWantedEvVars eqs
548 -- Notice that we simplify the RHS with only the explicitly
549 -- introduced skolems, allowing the RHS to constrain any
550 -- unification variables.
551 -- Then, and only then, we call zonkQuantifiedTypeVariables
552 -- Example foo :: Ord a => a -> a
553 -- foo_spec :: Int -> Int
554 -- {-# RULE "foo" foo = foo_spec #-}
555 -- Here, it's the RHS that fixes the type variable
557 -- So we don't want to make untouchable the type
558 -- variables in the envt of the RHS, because they include
559 -- the template variables of the RULE
561 -- Hence the rather painful ad-hoc treatement here
562 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
563 ; loc <- getCtLoc (RuleSkol name)
564 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
565 Implic { ic_untch = NoUntouchables
566 , ic_env = emptyNameEnv
567 , ic_skols = mkVarSet tv_bndrs
568 , ic_scoped = panic "emitImplication"
569 , ic_given = lhs_dicts
570 , ic_wanted = rhs_wanted
571 , ic_binds = rhs_binds_var
573 ; rhs_binds2 <- readTcRef evb_ref
577 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
581 *********************************************************************************
585 ***********************************************************************************
588 simplifyCheck :: SimplContext
589 -> WantedConstraints -- Wanted
591 -- Solve a single, top-level implication constraint
592 -- e.g. typically one created from a top-level type signature
593 -- f :: forall a. [a] -> [a]
595 -- We do this even if the function has no polymorphism:
599 -- (whereas for *nested* bindings we would not create
600 -- an implication constraint for g at all.)
602 -- Fails if can't solve something in the input wanteds
603 simplifyCheck ctxt wanteds
604 = do { wanteds <- mapBagM zonkWanted wanteds
606 ; traceTc "simplifyCheck {" (vcat
607 [ ptext (sLit "wanted =") <+> ppr wanteds ])
609 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
610 solveWanteds emptyInert wanteds
612 ; traceTc "simplifyCheck }" $
613 ptext (sLit "unsolved =") <+> ppr unsolved
615 ; reportUnsolved unsolved
620 solveWanteds :: InertSet -- Given
621 -> WantedConstraints -- Wanted
622 -> TcS (CanonicalCts, -- Unsolved flats
623 Bag Implication) -- Unsolved implications
624 -- solveWanteds iterates when it is able to float equalities
625 -- out of one or more of the implications
626 solveWanteds inert wanteds
627 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
628 ; can_flats <- canWanteds $ bagToList flat_wanteds
629 ; traceTcS "solveWanteds {" $
630 vcat [ text "wanteds =" <+> ppr wanteds
631 , text "inert =" <+> ppr inert ]
632 ; (unsolved_flats, unsolved_implics)
633 <- simpl_loop 1 can_flats implic_wanteds
634 ; bb <- getTcEvBindsBag
635 ; traceTcS "solveWanteds }" $
636 vcat [ text "wanteds =" <+> ppr wanteds
637 , text "unsolved_flats =" <+> ppr unsolved_flats
638 , text "unsolved_implics =" <+> ppr unsolved_implics
639 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
641 ; return (unsolved_flats, unsolved_implics) }
644 -> CanonicalCts -- May inlude givens (in the recursive call)
646 -> TcS (CanonicalCts, Bag Implication)
647 simpl_loop n can_ws implics
649 = trace "solveWanteds: loop" $ -- Always bleat
650 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
651 ; return (can_ws, implics) }
654 = do { inert1 <- solveInteract inert can_ws
655 ; let (inert2, unsolved_flats) = extractUnsolved inert1
657 ; traceTcS "solveWanteds/done flats" $
658 vcat [ text "inerts =" <+> ppr inert2
659 , text "unsolved =" <+> ppr unsolved_flats ]
661 -- See Note [Preparing inert set for implications]
662 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
663 ; (implic_eqs, unsolved_implics)
664 <- flatMapBagPairM (solveImplication inert_for_implics) implics
666 -- Apply defaulting rules if and only if there
667 -- no floated equalities. If there are, they may
668 -- solve the remaining wanteds, so don't do defaulting.
669 ; final_eqs <- if not (isEmptyBag implic_eqs)
670 then return implic_eqs
671 else applyDefaultingRules inert2 unsolved_flats
672 -- default_eqs are *givens*, so simpl_loop may
673 -- recurse with givens in the argument
675 ; if isEmptyBag final_eqs then
676 return (unsolved_flats, unsolved_implics)
678 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
679 [ text "floated_unsolved_eqs =" <+> ppr final_eqs
680 , text "unsolved_implics = " <+> ppr unsolved_implics ]
682 (unsolved_flats `unionBags` final_eqs)
686 solveImplication :: InertSet -- Given
687 -> Implication -- Wanted
688 -> TcS (CanonicalCts, -- Unsolved unification var = type
689 Bag Implication) -- Unsolved rest (always empty or singleton)
691 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
692 -- that are of the form unification var = type
694 -- 2. Maybe a unsolved implication, empty if entirely solved!
696 -- Precondition: everything is zonked by now
697 solveImplication inert
698 imp@(Implic { ic_untch = untch
699 , ic_binds = ev_binds
702 , ic_wanted = wanteds
704 = nestImplicTcS ev_binds untch $
705 do { traceTcS "solveImplication {" (ppr imp)
708 ; can_givens <- canGivens loc givens
709 ; given_inert <- solveInteract inert can_givens
711 -- Simplify the wanteds
712 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
714 ; let (res_flat_free, res_flat_bound)
715 = floatEqualities skols givens unsolved_flats
716 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
718 ; traceTcS "solveImplication end }" $ vcat
719 [ text "res_flat_free =" <+> ppr res_flat_free
720 , text "res_flat_bound =" <+> ppr res_flat_bound
721 , text "unsolved_implics =" <+> ppr unsolved_implics ]
723 ; let res_bag | isEmptyBag unsolved = emptyBag
724 | otherwise = unitBag (imp { ic_wanted = unsolved })
726 ; return (res_flat_free, res_bag) }
728 floatEqualities :: TcTyVarSet -> [EvVar]
729 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
730 floatEqualities skols can_given wanteds
731 | hasEqualities can_given = (emptyBag, wanteds)
732 | otherwise = partitionBag is_floatable wanteds
734 is_floatable :: CanonicalCt -> Bool
735 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
736 | isMetaTyVar tv || isMetaTyVarTy ty
737 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
738 is_floatable _ = False
741 Note [Preparing inert set for implications]
742 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
743 Before solving the nested implications, we convert any unsolved flat wanteds
744 to givens, and add them to the inert set. Reasons:
745 a) In checking mode, suppresses unnecessary errors. We already have
746 on unsolved-wanted error; adding it to the givens prevents any
747 consequential errors from showing uop
748 b) More importantly, in inference mode, we are going to quantify over this
749 constraint, and we *don't* want to quantify over any constraints that
750 are deducible from it.
752 The unsolved wanteds are *canonical* but they may not be *inert*,
753 because when made into a given they might interact with other givens.
754 Hence the call to solveInteract. Example:
756 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
758 We were not able to solve (a ~w [beta]) but we can't just assume it as
759 given because the resulting set is not inert. Hence we have to do a
760 'solveInteract' step first
762 *********************************************************************************
764 * Defaulting and disamgiguation *
766 *********************************************************************************
768 Basic plan behind applyDefaulting rules:
771 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
772 For each defaultable group, do:
773 For each possible substitution for [alpha |-> tau] where `alpha' is the
774 group's variable, do:
775 1) Make up new TcEvBinds
776 2) Extend TcS with (groupVariable
777 3) given_inert <- solveOne inert (given : a ~ tau)
778 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
779 5) if unsolved == empty then
780 sneakyUnify a |-> tau
781 write the evidence bins
782 return (final_inert ++ group_constraints,[])
783 -- will contain the info (alpha |-> tau)!!
784 goto next defaultable group
785 if unsolved <> empty then
786 throw away evidence binds
787 try next substitution
788 If you've run out of substitutions for this group, too bad, you failed
790 goto next defaultable group
793 Collect all the (canonical-cts, wanteds) gathered this way.
794 - Do a solveGiven over the canonical-cts to make sure they are inert
795 ------------------------------------------------------------------------------------------
799 applyDefaultingRules :: InertSet
800 -> CanonicalCts -- All wanteds
802 -- Return some *extra* givens, which express the
803 -- type-class-default choice
805 applyDefaultingRules inert wanteds
809 = do { untch <- getUntouchables
810 ; tv_cts <- mapM (defaultTyVar untch) $
811 varSetElems (tyVarsOfCanonicals wanteds)
813 ; info@(_, default_tys, _) <- getDefaultInfo
814 ; let groups = findDefaultableGroups info untch wanteds
815 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
817 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
818 , text "Type defaults =" <+> ppr deflt_cts])
820 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
823 defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
824 -- defaultTyVar is used on any un-instantiated meta type variables to
825 -- default the kind of ? and ?? etc to *. This is important to ensure
826 -- that instance declarations match. For example consider
827 -- instance Show (a->b)
828 -- foo x = show (\_ -> True)
829 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
830 -- and that won't match the typeKind (*) in the instance decl.
833 -- We look only at touchable type variables. No further constraints
834 -- are going to affect these type variables, so it's time to do it by
835 -- hand. However we aren't ready to default them fully to () or
836 -- whatever, because the type-class defaulting rules have yet to run.
838 defaultTyVar untch the_tv
840 , inTouchableRange untch the_tv
841 , not (k `eqKind` default_k)
842 = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
843 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
844 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
845 wanted_eq = CTyEqCan { cc_id = ev
846 , cc_flavor = Wanted loc
848 , cc_rhs = better_ty }
849 ; return (unitBag wanted_eq) }
852 = return emptyCCan -- The common case
855 default_k = defaultKind k
859 findDefaultableGroups
862 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
863 -> Untouchables -- Untouchable
864 -> CanonicalCts -- Unsolved
865 -> [[(CanonicalCt,TcTyVar)]]
866 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
868 | not (performDefaulting ctxt) = []
869 | null default_tys = []
870 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
872 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
873 non_unaries :: [CanonicalCt] -- and *other* constraints
875 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
876 -- Finds unary type-class constraints
877 find_unary cc@(CDictCan { cc_tyargs = [ty] })
878 | Just tv <- tcGetTyVar_maybe ty
880 find_unary cc = Right cc -- Non unary or non dictionary
882 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
883 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
885 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
887 is_defaultable_group ds@((_,tv):_)
888 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
889 && not (tv `elemVarSet` bad_tvs)
890 && inTouchableRange untch tv
891 && defaultable_classes [cc_class cc | (cc,_) <- ds]
892 is_defaultable_group [] = panic "defaultable_group"
894 defaultable_classes clss
895 | extended_defaults = any isInteractiveClass clss
896 | otherwise = all is_std_class clss && (any is_num_class clss)
898 -- In interactive mode, or with -XExtendedDefaultRules,
899 -- we default Show a to Show () to avoid graututious errors on "show []"
900 isInteractiveClass cls
901 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
903 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
904 -- is_num_class adds IsString to the standard numeric classes,
905 -- when -foverloaded-strings is enabled
907 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
908 -- Similarly is_std_class
910 ------------------------------
911 disambigGroup :: [Type] -- The default types
912 -> InertSet -- Given inert
913 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
914 -- sharing same type variable
917 disambigGroup [] _inert _grp
919 disambigGroup (default_ty:default_tys) inert group
920 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
921 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
922 -- We know this equality is canonical,
923 -- so we directly construct it as such
924 ; let given_eq = CTyEqCan { cc_id = ev
925 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
927 , cc_rhs = default_ty }
929 ; success <- tryTcS $
930 do { given_inert <- solveOne inert given_eq
931 ; final_inert <- solveInteract given_inert (listToBag wanteds)
932 ; let (_, unsolved) = extractUnsolved final_inert
933 ; return (isEmptyBag unsolved) }
936 True -> -- Success: record the type variable binding, and return
937 do { setWantedTyBind the_tv default_ty
938 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
939 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
940 ; return (unitBag given_eq) }
941 False -> -- Failure: try with the next type
942 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
943 ; disambigGroup default_tys inert group } }
945 ((the_ct,the_tv):_) = group
946 wanteds = map fst group
947 wanted_ev_vars = map deCanonicaliseWanted wanteds
950 Note [Avoiding spurious errors]
951 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
952 When doing the unification for defaulting, we check for skolem
953 type variables, and simply don't default them. For example:
954 f = (*) -- Monomorphic
957 Here, we get a complaint when checking the type signature for g,
958 that g isn't polymorphic enough; but then we get another one when
959 dealing with the (Num a) context arising from f's definition;
960 we try to unify a with Int (to default it), but find that it's
961 already been unified with the rigid variable from g's type sig