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 = growWanteds gbl_tvs zonked_wanted $
208 zonked_tau_tvs `minusVarSet` gbl_tvs
209 (perhaps_bound, surely_free)
210 = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
211 ; emitConstraints surely_free
212 ; traceTc "sinf" (ppr proto_qtvs $$ ppr perhaps_bound $$ ppr surely_free)
214 -- Now simplify the possibly-bound constraints
215 ; (simplified_perhaps_bound, tc_binds)
216 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
218 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
219 -- may have done some unification
220 ; gbl_tvs <- tcGetGlobalTyVars
221 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
222 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
223 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
224 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
225 constrained_tvs = tyVarsOfWantedEvVars zonked_simples
226 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
227 (final_qtvs, (bound, free))
228 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
229 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
231 ; traceTc "end simplifyInfer }" $
232 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
233 , text "wanted = " <+> ppr zonked_wanted
234 , text "qtvs = " <+> ppr final_qtvs
235 , text "free = " <+> ppr free
236 , text "bound = " <+> ppr bound ]
238 -- Turn the quantified meta-type variables into real type variables
239 ; emitConstraints (mapBag WcEvVar free)
240 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
241 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
242 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
244 ------------------------
245 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
246 -> TcM (Bag WantedEvVar, Bag EvBind)
247 -- We use this function when inferring the type of a function
248 -- The wanted constraints are already zonked
249 simplifyAsMuchAsPossible ctxt wanteds
250 = do { let untch = NoUntouchables
251 -- We allow ourselves to unify environment
252 -- variables; hence *no untouchables*
254 ; ((unsolved_flats, unsolved_implics), ev_binds)
255 <- runTcS ctxt untch $
256 simplifyApproxLoop 0 wanteds
259 ; reportUnsolved (emptyBag, unsolved_implics)
261 ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
262 ; return (final_wanted_evvars, ev_binds) }
265 simplifyApproxLoop :: Int -> WantedConstraints
266 -> TcS (CanonicalCts, Bag Implication)
267 simplifyApproxLoop n wanteds
269 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
271 = do { traceTcS "simplifyApproxLoop" (vcat
272 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
273 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
275 ; let (extra_flats, thiner_unsolved_implics)
276 = approximateImplications unsolved_implics
278 = mkWantedConstraints unsolved_flats thiner_unsolved_implics
280 ;-- If no new work was produced then we are done with simplifyApproxLoop
281 if isEmptyBag extra_flats
282 then do { traceTcS "simplifyApproxLoopRes" (vcat
283 [ ptext (sLit "Wanted = ") <+> ppr wanteds
284 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
285 ; return (unsolved_flats, unsolved_implics) }
287 else -- Produced new flat work wanteds, go round the loop
288 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
291 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
292 -- (wc1, impls2) <- approximateImplications impls
293 -- splits 'impls' into two parts
294 -- wc1: a bag of constraints that do not mention any skolems
295 -- impls2: a bag of *thiner* implication constraints
296 approximateImplications impls
297 = splitBag (do_implic emptyVarSet) impls
300 do_wanted :: TcTyVarSet -> WantedConstraint
301 -> (WantedConstraints, WantedConstraints)
302 do_wanted skols (WcImplic impl)
303 = let (fl_w, mb_impl) = do_implic skols impl
304 in (fl_w, mapBag WcImplic mb_impl)
305 do_wanted skols wc@(WcEvVar wev)
306 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
307 | otherwise = (emptyBag, unitBag wc)
310 do_implic :: TcTyVarSet -> Implication
311 -> (WantedConstraints, Bag Implication)
312 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
313 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
314 else unitBag impl{ ic_wanted = rest_wanted } )
316 (floatable_wanted, rest_wanted)
317 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
320 splitBag :: (a -> (WantedConstraints, Bag a))
321 -> Bag a -> (WantedConstraints, Bag a)
322 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
325 = (wcs `unionBags` b1, imps `unionBags` b2)
331 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
332 growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
333 growWanteds gbl_tvs ws tvs
334 | isEmptyBag ws = tvs
335 | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
336 growWantedEVs gbl_tvs ws tvs
337 | isEmptyBag ws = tvs
338 | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
340 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
341 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
342 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
343 -- X-constraint 'wanted', nuking the 'gbls' at each stage
344 growWantedEV gbl_tvs wev tvs
345 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
347 ev_tvs = growPredTyVars (wantedEvVarPred wev) tvs
349 growWanted gbl_tvs (WcEvVar wev) tvs
350 = growWantedEV gbl_tvs wev tvs
351 growWanted gbl_tvs (WcImplic implic) tvs
352 = foldrBag (growWanted (gbl_tvs `unionVarSet` ic_skols implic))
353 tvs (ic_wanted implic)
356 quantifyMe :: TyVarSet -- Quantifying over these
358 -> Bool -- True <=> quantify over this wanted
360 | isIPPred pred = True -- Note [Inheriting implicit parameters]
361 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
363 pred = wantedEvVarPred wev
365 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
366 quantifyMeWC qtvs (WcImplic implic)
367 = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted implic)
368 quantifyMeWC qtvs (WcEvVar wev)
369 = quantifyMe qtvs wev
372 Note [Avoid unecessary constraint simplification]
373 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
374 When inferring the type of a let-binding, with simplifyInfer,
375 try to avoid unnecessariliy simplifying class constraints.
376 Doing so aids sharing, but it also helps with delicate
378 instance C t => C [t] where ..
380 f x = let g y = ...(constraint C [t])...
382 When inferring a type for 'g', we don't want to apply the
383 instance decl, because then we can't satisfy (C t). So we
384 just notice that g isn't quantified over 't' and partition
385 the contraints before simplifying.
387 This only half-works, but then let-generalisation only half-works.
390 Note [Inheriting implicit parameters]
391 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
396 where f is *not* a top-level binding.
397 From the RHS of f we'll get the constraint (?y::Int).
398 There are two types we might infer for f:
402 (so we get ?y from the context of f's definition), or
404 f :: (?y::Int) => Int -> Int
406 At first you might think the first was better, becuase then
407 ?y behaves like a free variable of the definition, rather than
408 having to be passed at each call site. But of course, the WHOLE
409 IDEA is that ?y should be passed at each call site (that's what
410 dynamic binding means) so we'd better infer the second.
412 BOTTOM LINE: when *inferring types* you *must* quantify
413 over implicit parameters. See the predicate isFreeWhenInferring.
416 *********************************************************************************
420 ***********************************************************************************
422 When constructing evidence for superclasses in an instance declaration,
423 * we MUST have the "self" dictionary available, but
424 * we must NOT have its superclasses derived from "self"
426 Moreover, we must *completely* solve the constraints right now,
427 not wrap them in an implication constraint to solve later. Why?
428 Because when that implication constraint is solved there may
429 be some unrelated other solved top-level constraints that
430 recursively depend on the superclass we are building. Consider
431 class Ord a => C a where
432 instance C [Int] where ...
435 dCListInt = MkC $cNum ...
437 $cNum :: Ord [Int] -- The superclass
438 $cNum = let self = dCListInt in <solve Ord [Int]>
440 Now, if there is some *other* top-level constraint solved
444 we must not solve the (Ord [Int]) wanted from foo!!
447 simplifySuperClass :: EvVar -- The "self" dictionary
450 simplifySuperClass self wanteds
451 = do { wanteds <- mapBagM zonkWanted wanteds
452 ; loc <- getCtLoc NoScSkol
453 ; (unsolved, ev_binds)
454 <- runTcS SimplCheck NoUntouchables $
455 do { can_self <- canGivens loc [self]
456 ; let inert = foldlBag updInertSet emptyInert can_self
457 -- No need for solveInteract; we know it's inert
459 ; solveWanteds inert wanteds }
461 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
462 reportUnsolved unsolved }
466 *********************************************************************************
470 ***********************************************************************************
472 Note [Simplifying RULE lhs constraints]
473 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
474 On the LHS of transformation rules we only simplify only equalitis,
475 but not dictionaries. We want to keep dictionaries unsimplified, to
476 serve as the available stuff for the RHS of the rule. We *do* want to
477 simplify equalities, however, to detect ill-typed rules that cannot be
480 Implementation: the TcSFlags carried by the TcSMonad controls the
481 amount of simplification, so simplifyRuleLhs just sets the flag
484 Example. Consider the following left-hand side of a rule
485 f (x == y) (y > z) = ...
486 If we typecheck this expression we get constraints
487 d1 :: Ord a, d2 :: Eq a
488 We do NOT want to "simplify" to the LHS
489 forall x::a, y::a, z::a, d1::Ord a.
490 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
492 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
493 f ((==) d2 x y) ((>) d1 y z) = ...
495 Here is another example:
496 fromIntegral :: (Integral a, Num b) => a -> b
497 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
498 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
499 we *dont* want to get
501 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
502 because the scsel will mess up RULE matching. Instead we want
503 forall dIntegralInt, dNumInt.
504 fromIntegral Int Int dIntegralInt dNumInt = id Int
507 g (x == y) (y == z) = ..
508 where the two dictionaries are *identical*, we do NOT WANT
509 forall x::a, y::a, z::a, d1::Eq a
510 f ((==) d1 x y) ((>) d1 y z) = ...
511 because that will only match if the dict args are (visibly) equal.
512 Instead we want to quantify over the dictionaries separately.
514 In short, simplifyRuleLhs must *only* squash equalities, leaving
515 all dicts unchanged, with absolutely no sharing.
517 HOWEVER, under a nested implication things are different
519 f :: (forall a. Eq a => a->a) -> Bool -> ...
520 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
523 Here we *must* solve the wanted (Eq a) from the given (Eq a)
524 resulting from skolemising the agument type of g. So we
525 revert to SimplCheck when going under an implication.
528 simplifyRule :: RuleName
529 -> [TcTyVar] -- Explicit skolems
530 -> WantedConstraints -- Constraints from LHS
531 -> WantedConstraints -- Constraints from RHS
532 -> TcM ([EvVar], -- LHS dicts
533 TcEvBinds, -- Evidence for LHS
534 TcEvBinds) -- Evidence for RHS
535 -- See Note [Simplifying RULE lhs constraints]
536 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
537 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
538 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
540 -- Don't quantify over equalities (judgement call here)
541 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
542 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
543 -- Dicts and implicit parameters
544 ; reportUnsolvedWantedEvVars eqs
546 -- Notice that we simplify the RHS with only the explicitly
547 -- introduced skolems, allowing the RHS to constrain any
548 -- unification variables.
549 -- Then, and only then, we call zonkQuantifiedTypeVariables
550 -- Example foo :: Ord a => a -> a
551 -- foo_spec :: Int -> Int
552 -- {-# RULE "foo" foo = foo_spec #-}
553 -- Here, it's the RHS that fixes the type variable
555 -- So we don't want to make untouchable the type
556 -- variables in the envt of the RHS, because they include
557 -- the template variables of the RULE
559 -- Hence the rather painful ad-hoc treatement here
560 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
561 ; loc <- getCtLoc (RuleSkol name)
562 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
563 Implic { ic_untch = NoUntouchables
564 , ic_env = emptyNameEnv
565 , ic_skols = mkVarSet tv_bndrs
566 , ic_scoped = panic "emitImplication"
567 , ic_given = lhs_dicts
568 , ic_wanted = rhs_wanted
569 , ic_binds = rhs_binds_var
571 ; rhs_binds2 <- readTcRef evb_ref
575 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
579 *********************************************************************************
583 ***********************************************************************************
586 simplifyCheck :: SimplContext
587 -> WantedConstraints -- Wanted
589 -- Solve a single, top-level implication constraint
590 -- e.g. typically one created from a top-level type signature
591 -- f :: forall a. [a] -> [a]
593 -- We do this even if the function has no polymorphism:
597 -- (whereas for *nested* bindings we would not create
598 -- an implication constraint for g at all.)
600 -- Fails if can't solve something in the input wanteds
601 simplifyCheck ctxt wanteds
602 = do { wanteds <- mapBagM zonkWanted wanteds
604 ; traceTc "simplifyCheck {" (vcat
605 [ ptext (sLit "wanted =") <+> ppr wanteds ])
607 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
608 solveWanteds emptyInert wanteds
610 ; traceTc "simplifyCheck }" $
611 ptext (sLit "unsolved =") <+> ppr unsolved
613 ; reportUnsolved unsolved
618 solveWanteds :: InertSet -- Given
619 -> WantedConstraints -- Wanted
620 -> TcS (CanonicalCts, -- Unsolved flats
621 Bag Implication) -- Unsolved implications
622 -- solveWanteds iterates when it is able to float equalities
623 -- out of one or more of the implications
624 solveWanteds inert wanteds
625 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
626 ; can_flats <- canWanteds $ bagToList flat_wanteds
627 ; traceTcS "solveWanteds {" $
628 vcat [ text "wanteds =" <+> ppr wanteds
629 , text "inert =" <+> ppr inert ]
630 ; (unsolved_flats, unsolved_implics)
631 <- simpl_loop 1 can_flats implic_wanteds
632 ; traceTcS "solveWanteds }" $
633 vcat [ text "wanteds =" <+> ppr wanteds
634 , text "unsolved_flats =" <+> ppr unsolved_flats
635 , text "unsolved_implics =" <+> ppr unsolved_implics ]
636 ; return (unsolved_flats, unsolved_implics) }
639 -> CanonicalCts -- May inlude givens (in the recursive call)
641 -> TcS (CanonicalCts, Bag Implication)
642 simpl_loop n can_ws implics
644 = trace "solveWanteds: loop" $ -- Always bleat
645 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
646 ; return (can_ws, implics) }
649 = do { inert1 <- solveInteract inert can_ws
650 ; let (inert2, unsolved_flats) = extractUnsolved inert1
652 ; traceTcS "solveWanteds/done flats" $
653 vcat [ text "inerts =" <+> ppr inert2
654 , text "unsolved =" <+> ppr unsolved_flats ]
656 -- See Note [Preparing inert set for implications]
657 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
658 ; (implic_eqs, unsolved_implics)
659 <- flatMapBagPairM (solveImplication inert_for_implics) implics
661 -- Apply defaulting rules if and only if there
662 -- no floated equalities. If there are, they may
663 -- solve the remaining wanteds, so don't do defaulting.
664 ; final_eqs <- if not (isEmptyBag implic_eqs)
665 then return implic_eqs
666 else applyDefaultingRules inert2 unsolved_flats
667 -- default_eqs are *givens*, so simpl_loop may
668 -- recurse with givens in the argument
670 ; if isEmptyBag final_eqs then
671 return (unsolved_flats, unsolved_implics)
673 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
674 [ text "floated_unsolved_eqs =" <+> ppr final_eqs
675 , text "unsolved_implics = " <+> ppr unsolved_implics ]
677 (unsolved_flats `unionBags` final_eqs)
681 solveImplication :: InertSet -- Given
682 -> Implication -- Wanted
683 -> TcS (CanonicalCts, -- Unsolved unification var = type
684 Bag Implication) -- Unsolved rest (always empty or singleton)
686 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
687 -- that are of the form unification var = type
689 -- 2. Maybe a unsolved implication, empty if entirely solved!
691 -- Precondition: everything is zonked by now
692 solveImplication inert
693 imp@(Implic { ic_untch = untch
694 , ic_binds = ev_binds
697 , ic_wanted = wanteds
699 = nestImplicTcS ev_binds untch $
700 do { traceTcS "solveImplication {" (ppr imp)
703 ; can_givens <- canGivens loc givens
704 ; given_inert <- solveInteract inert can_givens
706 -- Simplify the wanteds
707 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
709 ; let (res_flat_free, res_flat_bound)
710 = floatEqualities skols givens unsolved_flats
711 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
713 ; traceTcS "solveImplication end }" $ vcat
714 [ text "res_flat_free =" <+> ppr res_flat_free
715 , text "res_flat_bound =" <+> ppr res_flat_bound
716 , text "unsolved_implics =" <+> ppr unsolved_implics ]
718 ; let res_bag | isEmptyBag unsolved = emptyBag
719 | otherwise = unitBag (imp { ic_wanted = unsolved })
721 ; return (res_flat_free, res_bag) }
723 floatEqualities :: TcTyVarSet -> [EvVar]
724 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
725 floatEqualities skols can_given wanteds
726 | hasEqualities can_given = (emptyBag, wanteds)
727 | otherwise = partitionBag is_floatable wanteds
729 is_floatable :: CanonicalCt -> Bool
730 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
731 | isMetaTyVar tv || isMetaTyVarTy ty
732 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
733 is_floatable _ = False
736 Note [Preparing inert set for implications]
737 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
738 Before solving the nested implications, we convert any unsolved flat wanteds
739 to givens, and add them to the inert set. Reasons:
740 a) In checking mode, suppresses unnecessary errors. We already have
741 on unsolved-wanted error; adding it to the givens prevents any
742 consequential errors from showing uop
743 b) More importantly, in inference mode, we are going to quantify over this
744 constraint, and we *don't* want to quantify over any constraints that
745 are deducible from it.
747 The unsolved wanteds are *canonical* but they may not be *inert*,
748 because when made into a given they might interact with other givens.
749 Hence the call to solveInteract. Example:
751 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
753 We were not able to solve (a ~w [beta]) but we can't just assume it as
754 given because the resulting set is not inert. Hence we have to do a
755 'solveInteract' step first
757 *********************************************************************************
759 * Defaulting and disamgiguation *
761 *********************************************************************************
763 Basic plan behind applyDefaulting rules:
766 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
767 For each defaultable group, do:
768 For each possible substitution for [alpha |-> tau] where `alpha' is the
769 group's variable, do:
770 1) Make up new TcEvBinds
771 2) Extend TcS with (groupVariable
772 3) given_inert <- solveOne inert (given : a ~ tau)
773 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
774 5) if unsolved == empty then
775 sneakyUnify a |-> tau
776 write the evidence bins
777 return (final_inert ++ group_constraints,[])
778 -- will contain the info (alpha |-> tau)!!
779 goto next defaultable group
780 if unsolved <> empty then
781 throw away evidence binds
782 try next substitution
783 If you've run out of substitutions for this group, too bad, you failed
785 goto next defaultable group
788 Collect all the (canonical-cts, wanteds) gathered this way.
789 - Do a solveGiven over the canonical-cts to make sure they are inert
790 ------------------------------------------------------------------------------------------
794 applyDefaultingRules :: InertSet
795 -> CanonicalCts -- All wanteds
797 -- Return some *extra* givens, which express the
798 -- type-class-default choice
800 applyDefaultingRules inert wanteds
804 = do { untch <- getUntouchables
805 ; tv_cts <- mapM (defaultTyVar untch) $
806 varSetElems (tyVarsOfCanonicals wanteds)
808 ; info@(_, default_tys, _) <- getDefaultInfo
809 ; let groups = findDefaultableGroups info untch wanteds
810 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
812 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
813 , text "Type defaults =" <+> ppr deflt_cts])
815 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
818 defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
819 -- defaultTyVar is used on any un-instantiated meta type variables to
820 -- default the kind of ? and ?? etc to *. This is important to ensure
821 -- that instance declarations match. For example consider
822 -- instance Show (a->b)
823 -- foo x = show (\_ -> True)
824 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
825 -- and that won't match the typeKind (*) in the instance decl.
828 -- We look only at touchable type variables. No further constraints
829 -- are going to affect these type variables, so it's time to do it by
830 -- hand. However we aren't ready to default them fully to () or
831 -- whatever, because the type-class defaulting rules have yet to run.
833 defaultTyVar untch the_tv
835 , inTouchableRange untch the_tv
836 , not (k `eqKind` default_k)
837 = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
838 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
839 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
840 wanted_eq = CTyEqCan { cc_id = ev
841 , cc_flavor = Wanted loc
843 , cc_rhs = better_ty }
844 ; return (unitBag wanted_eq) }
847 = return emptyCCan -- The common case
850 default_k = defaultKind k
854 findDefaultableGroups
857 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
858 -> Untouchables -- Untouchable
859 -> CanonicalCts -- Unsolved
860 -> [[(CanonicalCt,TcTyVar)]]
861 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
863 | not (performDefaulting ctxt) = []
864 | null default_tys = []
865 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
867 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
868 non_unaries :: [CanonicalCt] -- and *other* constraints
870 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
871 -- Finds unary type-class constraints
872 find_unary cc@(CDictCan { cc_tyargs = [ty] })
873 | Just tv <- tcGetTyVar_maybe ty
875 find_unary cc = Right cc -- Non unary or non dictionary
877 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
878 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
880 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
882 is_defaultable_group ds@((_,tv):_)
883 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
884 && not (tv `elemVarSet` bad_tvs)
885 && inTouchableRange untch tv
886 && defaultable_classes [cc_class cc | (cc,_) <- ds]
887 is_defaultable_group [] = panic "defaultable_group"
889 defaultable_classes clss
890 | extended_defaults = any isInteractiveClass clss
891 | otherwise = all is_std_class clss && (any is_num_class clss)
893 -- In interactive mode, or with -XExtendedDefaultRules,
894 -- we default Show a to Show () to avoid graututious errors on "show []"
895 isInteractiveClass cls
896 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
898 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
899 -- is_num_class adds IsString to the standard numeric classes,
900 -- when -foverloaded-strings is enabled
902 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
903 -- Similarly is_std_class
905 ------------------------------
906 disambigGroup :: [Type] -- The default types
907 -> InertSet -- Given inert
908 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
909 -- sharing same type variable
912 disambigGroup [] _inert _grp
914 disambigGroup (default_ty:default_tys) inert group
915 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
916 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
917 -- We know this equality is canonical,
918 -- so we directly construct it as such
919 ; let given_eq = CTyEqCan { cc_id = ev
920 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
922 , cc_rhs = default_ty }
924 ; success <- tryTcS $
925 do { given_inert <- solveOne inert given_eq
926 ; final_inert <- solveInteract given_inert (listToBag wanteds)
927 ; let (_, unsolved) = extractUnsolved final_inert
928 ; return (isEmptyBag unsolved) }
931 True -> -- Success: record the type variable binding, and return
932 do { setWantedTyBind the_tv default_ty
933 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
934 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
935 ; return (unitBag given_eq) }
936 False -> -- Failure: try with the next type
937 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
938 ; disambigGroup default_tys inert group } }
940 ((the_ct,the_tv):_) = group
941 wanteds = map fst group
942 wanted_ev_vars = map deCanonicaliseWanted wanteds
945 Note [Avoiding spurious errors]
946 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
947 When doing the unification for defaulting, we check for skolem
948 type variables, and simply don't default them. For example:
949 f = (*) -- Monomorphic
952 Here, we get a complaint when checking the type signature for g,
953 that g isn't polymorphic enough; but then we get another one when
954 dealing with the (Num a) context arising from f's definition;
955 we try to unify a with Int (to default it), but find that it's
956 already been unified with the rigid variable from g's type sig