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 growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet
347 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
348 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
349 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
350 -- X-constraint 'wanted', nuking the 'gbls' at each stage
352 growEvVar gbl_tvs ev tvs
353 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
355 ev_tvs = growPredTyVars (evVarPred ev) tvs
357 growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
359 growWanted gbl_tvs (WcEvVar wev) tvs
360 = growWantedEV gbl_tvs wev tvs
361 growWanted gbl_tvs (WcImplic implic) tvs
362 = foldrBag (growWanted inner_gbl_tvs)
363 (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
364 -- Must grow over inner givens too
367 inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
370 quantifyMe :: TyVarSet -- Quantifying over these
372 -> Bool -- True <=> quantify over this wanted
374 | isIPPred pred = True -- Note [Inheriting implicit parameters]
375 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
377 pred = wantedEvVarPred wev
379 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
380 -- False => we can *definitely* float the WantedConstraint out
381 quantifyMeWC qtvs (WcImplic implic)
382 = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
383 || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
385 inner_qtvs = qtvs `minusVarSet` ic_skols implic
387 quantifyMeWC qtvs (WcEvVar wev)
388 = quantifyMe qtvs wev
391 Note [Avoid unecessary constraint simplification]
392 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
393 When inferring the type of a let-binding, with simplifyInfer,
394 try to avoid unnecessariliy simplifying class constraints.
395 Doing so aids sharing, but it also helps with delicate
397 instance C t => C [t] where ..
399 f x = let g y = ...(constraint C [t])...
401 When inferring a type for 'g', we don't want to apply the
402 instance decl, because then we can't satisfy (C t). So we
403 just notice that g isn't quantified over 't' and partition
404 the contraints before simplifying.
406 This only half-works, but then let-generalisation only half-works.
409 Note [Inheriting implicit parameters]
410 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
415 where f is *not* a top-level binding.
416 From the RHS of f we'll get the constraint (?y::Int).
417 There are two types we might infer for f:
421 (so we get ?y from the context of f's definition), or
423 f :: (?y::Int) => Int -> Int
425 At first you might think the first was better, becuase then
426 ?y behaves like a free variable of the definition, rather than
427 having to be passed at each call site. But of course, the WHOLE
428 IDEA is that ?y should be passed at each call site (that's what
429 dynamic binding means) so we'd better infer the second.
431 BOTTOM LINE: when *inferring types* you *must* quantify
432 over implicit parameters. See the predicate isFreeWhenInferring.
435 *********************************************************************************
439 ***********************************************************************************
441 When constructing evidence for superclasses in an instance declaration,
442 * we MUST have the "self" dictionary available, but
443 * we must NOT have its superclasses derived from "self"
445 Moreover, we must *completely* solve the constraints right now,
446 not wrap them in an implication constraint to solve later. Why?
447 Because when that implication constraint is solved there may
448 be some unrelated other solved top-level constraints that
449 recursively depend on the superclass we are building. Consider
450 class Ord a => C a where
451 instance C [Int] where ...
454 dCListInt = MkC $cNum ...
456 $cNum :: Ord [Int] -- The superclass
457 $cNum = let self = dCListInt in <solve Ord [Int]>
459 Now, if there is some *other* top-level constraint solved
463 we must not solve the (Ord [Int]) wanted from foo!!
466 simplifySuperClass :: EvVar -- The "self" dictionary
469 simplifySuperClass self wanteds
470 = do { wanteds <- mapBagM zonkWanted wanteds
471 ; loc <- getCtLoc NoScSkol
472 ; (unsolved, ev_binds)
473 <- runTcS SimplCheck NoUntouchables $
474 do { can_self <- canGivens loc [self]
475 ; let inert = foldlBag updInertSet emptyInert can_self
476 -- No need for solveInteract; we know it's inert
478 ; solveWanteds inert wanteds }
480 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
481 reportUnsolved unsolved }
485 *********************************************************************************
489 ***********************************************************************************
491 Note [Simplifying RULE lhs constraints]
492 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
493 On the LHS of transformation rules we only simplify only equalitis,
494 but not dictionaries. We want to keep dictionaries unsimplified, to
495 serve as the available stuff for the RHS of the rule. We *do* want to
496 simplify equalities, however, to detect ill-typed rules that cannot be
499 Implementation: the TcSFlags carried by the TcSMonad controls the
500 amount of simplification, so simplifyRuleLhs just sets the flag
503 Example. Consider the following left-hand side of a rule
504 f (x == y) (y > z) = ...
505 If we typecheck this expression we get constraints
506 d1 :: Ord a, d2 :: Eq a
507 We do NOT want to "simplify" to the LHS
508 forall x::a, y::a, z::a, d1::Ord a.
509 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
511 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
512 f ((==) d2 x y) ((>) d1 y z) = ...
514 Here is another example:
515 fromIntegral :: (Integral a, Num b) => a -> b
516 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
517 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
518 we *dont* want to get
520 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
521 because the scsel will mess up RULE matching. Instead we want
522 forall dIntegralInt, dNumInt.
523 fromIntegral Int Int dIntegralInt dNumInt = id Int
526 g (x == y) (y == z) = ..
527 where the two dictionaries are *identical*, we do NOT WANT
528 forall x::a, y::a, z::a, d1::Eq a
529 f ((==) d1 x y) ((>) d1 y z) = ...
530 because that will only match if the dict args are (visibly) equal.
531 Instead we want to quantify over the dictionaries separately.
533 In short, simplifyRuleLhs must *only* squash equalities, leaving
534 all dicts unchanged, with absolutely no sharing.
536 HOWEVER, under a nested implication things are different
538 f :: (forall a. Eq a => a->a) -> Bool -> ...
539 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
542 Here we *must* solve the wanted (Eq a) from the given (Eq a)
543 resulting from skolemising the agument type of g. So we
544 revert to SimplCheck when going under an implication.
547 simplifyRule :: RuleName
548 -> [TcTyVar] -- Explicit skolems
549 -> WantedConstraints -- Constraints from LHS
550 -> WantedConstraints -- Constraints from RHS
551 -> TcM ([EvVar], -- LHS dicts
552 TcEvBinds, -- Evidence for LHS
553 TcEvBinds) -- Evidence for RHS
554 -- See Note [Simplifying RULE lhs constraints]
555 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
556 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
557 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
559 -- Don't quantify over equalities (judgement call here)
560 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
561 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
562 -- Dicts and implicit parameters
563 ; reportUnsolvedWantedEvVars eqs
565 -- Notice that we simplify the RHS with only the explicitly
566 -- introduced skolems, allowing the RHS to constrain any
567 -- unification variables.
568 -- Then, and only then, we call zonkQuantifiedTypeVariables
569 -- Example foo :: Ord a => a -> a
570 -- foo_spec :: Int -> Int
571 -- {-# RULE "foo" foo = foo_spec #-}
572 -- Here, it's the RHS that fixes the type variable
574 -- So we don't want to make untouchable the type
575 -- variables in the envt of the RHS, because they include
576 -- the template variables of the RULE
578 -- Hence the rather painful ad-hoc treatement here
579 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
580 ; loc <- getCtLoc (RuleSkol name)
581 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
582 Implic { ic_untch = NoUntouchables
583 , ic_env = emptyNameEnv
584 , ic_skols = mkVarSet tv_bndrs
585 , ic_scoped = panic "emitImplication"
586 , ic_given = lhs_dicts
587 , ic_wanted = rhs_wanted
588 , ic_binds = rhs_binds_var
590 ; rhs_binds2 <- readTcRef evb_ref
594 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
598 *********************************************************************************
602 ***********************************************************************************
605 simplifyCheck :: SimplContext
606 -> WantedConstraints -- Wanted
608 -- Solve a single, top-level implication constraint
609 -- e.g. typically one created from a top-level type signature
610 -- f :: forall a. [a] -> [a]
612 -- We do this even if the function has no polymorphism:
616 -- (whereas for *nested* bindings we would not create
617 -- an implication constraint for g at all.)
619 -- Fails if can't solve something in the input wanteds
620 simplifyCheck ctxt wanteds
621 = do { wanteds <- mapBagM zonkWanted wanteds
623 ; traceTc "simplifyCheck {" (vcat
624 [ ptext (sLit "wanted =") <+> ppr wanteds ])
626 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
627 solveWanteds emptyInert wanteds
629 ; traceTc "simplifyCheck }" $
630 ptext (sLit "unsolved =") <+> ppr unsolved
632 ; reportUnsolved unsolved
637 solveWanteds :: InertSet -- Given
638 -> WantedConstraints -- Wanted
639 -> TcS (CanonicalCts, -- Unsolved flats
640 Bag Implication) -- Unsolved implications
641 -- solveWanteds iterates when it is able to float equalities
642 -- out of one or more of the implications
643 solveWanteds inert wanteds
644 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
645 ; can_flats <- canWanteds $ bagToList flat_wanteds
646 ; traceTcS "solveWanteds {" $
647 vcat [ text "wanteds =" <+> ppr wanteds
648 , text "inert =" <+> ppr inert ]
649 ; (unsolved_flats, unsolved_implics)
650 <- simpl_loop 1 can_flats implic_wanteds
651 ; bb <- getTcEvBindsBag
652 ; traceTcS "solveWanteds }" $
653 vcat [ text "wanteds =" <+> ppr wanteds
654 , text "unsolved_flats =" <+> ppr unsolved_flats
655 , text "unsolved_implics =" <+> ppr unsolved_implics
656 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
658 ; return (unsolved_flats, unsolved_implics) }
661 -> CanonicalCts -- May inlude givens (in the recursive call)
663 -> TcS (CanonicalCts, Bag Implication)
664 simpl_loop n can_ws implics
666 = trace "solveWanteds: loop" $ -- Always bleat
667 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
668 ; return (can_ws, implics) }
671 = do { inert1 <- solveInteract inert can_ws
672 ; let (inert2, unsolved_flats) = extractUnsolved inert1
674 ; traceTcS "solveWanteds/done flats" $
675 vcat [ text "inerts =" <+> ppr inert2
676 , text "unsolved =" <+> ppr unsolved_flats ]
678 -- See Note [Preparing inert set for implications]
679 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
680 ; (implic_eqs, unsolved_implics)
681 <- flatMapBagPairM (solveImplication inert_for_implics) implics
683 -- Apply defaulting rules if and only if there
684 -- no floated equalities. If there are, they may
685 -- solve the remaining wanteds, so don't do defaulting.
686 ; final_eqs <- if not (isEmptyBag implic_eqs)
687 then return implic_eqs
688 else applyDefaultingRules inert2 unsolved_flats
689 -- default_eqs are *givens*, so simpl_loop may
690 -- recurse with givens in the argument
692 ; if isEmptyBag final_eqs then
693 return (unsolved_flats, unsolved_implics)
695 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
696 [ text "floated_unsolved_eqs =" <+> ppr final_eqs
697 , text "unsolved_implics = " <+> ppr unsolved_implics ]
699 (unsolved_flats `unionBags` final_eqs)
703 solveImplication :: InertSet -- Given
704 -> Implication -- Wanted
705 -> TcS (CanonicalCts, -- Unsolved unification var = type
706 Bag Implication) -- Unsolved rest (always empty or singleton)
708 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
709 -- that are of the form unification var = type
711 -- 2. Maybe a unsolved implication, empty if entirely solved!
713 -- Precondition: everything is zonked by now
714 solveImplication inert
715 imp@(Implic { ic_untch = untch
716 , ic_binds = ev_binds
719 , ic_wanted = wanteds
721 = nestImplicTcS ev_binds untch $
722 recoverTcS (return (emptyBag, emptyBag)) $
723 -- Recover from nested failures. Even the top level is
724 -- just a bunch of implications, so failing at the first
726 do { traceTcS "solveImplication {" (ppr imp)
729 ; can_givens <- canGivens loc givens
730 ; given_inert <- solveInteract inert can_givens
732 -- Simplify the wanteds
733 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
735 ; let (res_flat_free, res_flat_bound)
736 = floatEqualities skols givens unsolved_flats
737 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
739 ; traceTcS "solveImplication end }" $ vcat
740 [ text "res_flat_free =" <+> ppr res_flat_free
741 , text "res_flat_bound =" <+> ppr res_flat_bound
742 , text "unsolved_implics =" <+> ppr unsolved_implics ]
744 ; let res_bag | isEmptyBag unsolved = emptyBag
745 | otherwise = unitBag (imp { ic_wanted = unsolved })
747 ; return (res_flat_free, res_bag) }
749 floatEqualities :: TcTyVarSet -> [EvVar]
750 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
751 floatEqualities skols can_given wanteds
752 | hasEqualities can_given = (emptyBag, wanteds)
753 | otherwise = partitionBag is_floatable wanteds
755 is_floatable :: CanonicalCt -> Bool
756 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
757 | isMetaTyVar tv || isMetaTyVarTy ty
758 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
759 is_floatable _ = False
762 Note [Preparing inert set for implications]
763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
764 Before solving the nested implications, we convert any unsolved flat wanteds
765 to givens, and add them to the inert set. Reasons:
766 a) In checking mode, suppresses unnecessary errors. We already have
767 on unsolved-wanted error; adding it to the givens prevents any
768 consequential errors from showing uop
769 b) More importantly, in inference mode, we are going to quantify over this
770 constraint, and we *don't* want to quantify over any constraints that
771 are deducible from it.
773 The unsolved wanteds are *canonical* but they may not be *inert*,
774 because when made into a given they might interact with other givens.
775 Hence the call to solveInteract. Example:
777 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
779 We were not able to solve (a ~w [beta]) but we can't just assume it as
780 given because the resulting set is not inert. Hence we have to do a
781 'solveInteract' step first
783 *********************************************************************************
785 * Defaulting and disamgiguation *
787 *********************************************************************************
789 Basic plan behind applyDefaulting rules:
792 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
793 For each defaultable group, do:
794 For each possible substitution for [alpha |-> tau] where `alpha' is the
795 group's variable, do:
796 1) Make up new TcEvBinds
797 2) Extend TcS with (groupVariable
798 3) given_inert <- solveOne inert (given : a ~ tau)
799 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
800 5) if unsolved == empty then
801 sneakyUnify a |-> tau
802 write the evidence bins
803 return (final_inert ++ group_constraints,[])
804 -- will contain the info (alpha |-> tau)!!
805 goto next defaultable group
806 if unsolved <> empty then
807 throw away evidence binds
808 try next substitution
809 If you've run out of substitutions for this group, too bad, you failed
811 goto next defaultable group
814 Collect all the (canonical-cts, wanteds) gathered this way.
815 - Do a solveGiven over the canonical-cts to make sure they are inert
816 ------------------------------------------------------------------------------------------
820 applyDefaultingRules :: InertSet
821 -> CanonicalCts -- All wanteds
823 -- Return some *extra* givens, which express the
824 -- type-class-default choice
826 applyDefaultingRules inert wanteds
830 = do { untch <- getUntouchables
831 ; tv_cts <- mapM (defaultTyVar untch) $
832 varSetElems (tyVarsOfCDicts wanteds)
834 ; info@(_, default_tys, _) <- getDefaultInfo
835 ; let groups = findDefaultableGroups info untch wanteds
836 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
838 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
839 , text "Type defaults =" <+> ppr deflt_cts])
841 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
844 defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
845 -- defaultTyVar is used on any un-instantiated meta type variables to
846 -- default the kind of ? and ?? etc to *. This is important to ensure
847 -- that instance declarations match. For example consider
848 -- instance Show (a->b)
849 -- foo x = show (\_ -> True)
850 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
851 -- and that won't match the typeKind (*) in the instance decl.
854 -- We look only at touchable type variables. No further constraints
855 -- are going to affect these type variables, so it's time to do it by
856 -- hand. However we aren't ready to default them fully to () or
857 -- whatever, because the type-class defaulting rules have yet to run.
859 defaultTyVar untch the_tv
860 | isTouchableMetaTyVar_InRange untch the_tv
861 , not (k `eqKind` default_k)
862 = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
863 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
864 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
865 wanted_eq = CTyEqCan { cc_id = ev
866 , cc_flavor = Wanted loc
868 , cc_rhs = better_ty }
869 ; return (unitBag wanted_eq) }
872 = return emptyCCan -- The common case
875 default_k = defaultKind k
879 findDefaultableGroups
882 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
883 -> Untouchables -- Untouchable
884 -> CanonicalCts -- Unsolved
885 -> [[(CanonicalCt,TcTyVar)]]
886 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
888 | not (performDefaulting ctxt) = []
889 | null default_tys = []
890 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
892 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
893 non_unaries :: [CanonicalCt] -- and *other* constraints
895 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
896 -- Finds unary type-class constraints
897 find_unary cc@(CDictCan { cc_tyargs = [ty] })
898 | Just tv <- tcGetTyVar_maybe ty
900 find_unary cc = Right cc -- Non unary or non dictionary
902 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
903 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
905 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
907 is_defaultable_group ds@((_,tv):_)
908 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
909 && not (tv `elemVarSet` bad_tvs)
910 && isTouchableMetaTyVar_InRange untch tv
911 && defaultable_classes [cc_class cc | (cc,_) <- ds]
912 is_defaultable_group [] = panic "defaultable_group"
914 defaultable_classes clss
915 | extended_defaults = any isInteractiveClass clss
916 | otherwise = all is_std_class clss && (any is_num_class clss)
918 -- In interactive mode, or with -XExtendedDefaultRules,
919 -- we default Show a to Show () to avoid graututious errors on "show []"
920 isInteractiveClass cls
921 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
923 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
924 -- is_num_class adds IsString to the standard numeric classes,
925 -- when -foverloaded-strings is enabled
927 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
928 -- Similarly is_std_class
930 ------------------------------
931 disambigGroup :: [Type] -- The default types
932 -> InertSet -- Given inert
933 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
934 -- sharing same type variable
937 disambigGroup [] _inert _grp
939 disambigGroup (default_ty:default_tys) inert group
940 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
941 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
942 -- We know this equality is canonical,
943 -- so we directly construct it as such
944 ; let given_eq = CTyEqCan { cc_id = ev
945 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
947 , cc_rhs = default_ty }
949 ; success <- tryTcS $
950 do { given_inert <- solveOne inert given_eq
951 ; final_inert <- solveInteract given_inert (listToBag wanteds)
952 ; let (_, unsolved) = extractUnsolved final_inert
953 ; return (isEmptyBag unsolved) }
956 True -> -- Success: record the type variable binding, and return
957 do { setWantedTyBind the_tv default_ty
958 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
959 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
960 ; return (unitBag given_eq) }
961 False -> -- Failure: try with the next type
962 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
963 ; disambigGroup default_tys inert group } }
965 ((the_ct,the_tv):_) = group
966 wanteds = map fst group
967 wanted_ev_vars = map deCanonicaliseWanted wanteds
970 Note [Avoiding spurious errors]
971 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
972 When doing the unification for defaulting, we check for skolem
973 type variables, and simply don't default them. For example:
974 f = (*) -- Monomorphic
977 Here, we get a complaint when checking the type signature for g,
978 that g isn't polymorphic enough; but then we get another one when
979 dealing with the (Num a) context arising from f's definition;
980 we try to unify a with Int (to default it), but find that it's
981 already been unified with the rigid variable from g's type sig