3 simplifyInfer, simplifySuperClass,
4 simplifyDefault, simplifyDeriv, simplifyBracket,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
25 import NameEnv ( emptyNameEnv )
31 import Class ( classKey )
32 import BasicTypes ( RuleName )
33 import Data.List ( partition )
39 *********************************************************************************
41 * External interface *
43 *********************************************************************************
46 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
47 -- Simplify top-level constraints
48 -- Usually these will be implications, when there is
49 -- nothing to quanitfy we don't wrap in a degenerate implication,
50 -- so we do that here instead
52 = simplifyCheck SimplCheck wanteds
55 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
56 simplifyInteractive wanteds
57 = simplifyCheck SimplInteractive wanteds
60 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
61 -> TcM () -- Succeeds iff the constraint is soluble
63 = do { loc <- getCtLoc DefaultOrigin
64 ; wanted <- newWantedEvVars theta
65 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
66 ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
70 simplifyBracket is used when simplifying the constraints arising from
71 a Template Haskell bracket [| ... |]. We want to check that there aren't
72 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
73 Show instance), but we aren't otherwise interested in the results.
74 Nor do we care about ambiguous dictionaries etc. We will type check
75 this bracket again at its usage site.
78 simplifyBracket :: WantedConstraints -> TcM ()
79 simplifyBracket wanteds
80 = do { zonked_wanteds <- mapBagM zonkWanted wanteds
81 ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
86 *********************************************************************************
90 ***********************************************************************************
93 simplifyDeriv :: CtOrigin
95 -> ThetaType -- Wanted
96 -> TcM ThetaType -- Needed
97 -- Given instance (wanted) => C inst_ty
98 -- Simplify 'wanted' as much as possibles
99 simplifyDeriv orig tvs theta
100 = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
101 -- One reason is that the constraint solving machinery
102 -- expects *TcTyVars* not TyVars. Another is that
103 -- when looking up instances we don't want overlap
106 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
108 ; loc <- getCtLoc orig
109 ; wanted <- newWantedEvVars (substTheta skol_subst theta)
110 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
112 ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
113 ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
115 ; let (good, bad) = partition validDerivPred $
116 foldrBag ((:) . wantedEvVarPred) [] unsolved
117 -- See Note [Exotic derived instance contexts]
118 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
120 ; reportUnsolvedDeriv bad loc
121 ; return $ substTheta subst_skol good }
124 Note [Exotic derived instance contexts]
125 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
126 In a 'derived' instance declaration, we *infer* the context. It's a
127 bit unclear what rules we should apply for this; the Haskell report is
128 silent. Obviously, constraints like (Eq a) are fine, but what about
129 data T f a = MkT (f a) deriving( Eq )
130 where we'd get an Eq (f a) constraint. That's probably fine too.
132 One could go further: consider
133 data T a b c = MkT (Foo a b c) deriving( Eq )
134 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
136 Notice that this instance (just) satisfies the Paterson termination
137 conditions. Then we *could* derive an instance decl like this:
139 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
140 even though there is no instance for (C Int a), because there just
141 *might* be an instance for, say, (C Int Bool) at a site where we
142 need the equality instance for T's.
144 However, this seems pretty exotic, and it's quite tricky to allow
145 this, and yet give sensible error messages in the (much more common)
146 case where we really want that instance decl for C.
148 So for now we simply require that the derived instance context
149 should have only type-variable constraints.
151 Here is another example:
152 data Fix f = In (f (Fix f)) deriving( Eq )
153 Here, if we are prepared to allow -XUndecidableInstances we
154 could derive the instance
155 instance Eq (f (Fix f)) => Eq (Fix f)
156 but this is so delicate that I don't think it should happen inside
157 'deriving'. If you want this, write it yourself!
159 NB: if you want to lift this condition, make sure you still meet the
160 termination conditions! If not, the deriving mechanism generates
161 larger and larger constraints. Example:
163 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
165 Note the lack of a Show instance for Succ. First we'll generate
166 instance (Show (Succ a), Show a) => Show (Seq a)
168 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
169 and so on. Instead we want to complain of no instance for (Show (Succ a)).
173 Allow constraints which consist only of type variables, with no repeats.
175 *********************************************************************************
179 ***********************************************************************************
182 simplifyInfer :: Bool -- Apply monomorphism restriction
183 -> TcTyVarSet -- These type variables are free in the
184 -- types to be generalised
186 -> TcM ([TcTyVar], -- Quantify over these type variables
187 [EvVar], -- ... and these constraints
188 TcEvBinds) -- ... binding these evidence variables
189 simplifyInfer apply_mr tau_tvs wanted
190 | isEmptyBag wanted -- Trivial case is quite common
191 = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
192 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
193 ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
194 ; return (qtvs, [], emptyTcEvBinds) }
197 = do { zonked_wanted <- mapBagM zonkWanted wanted
198 ; traceTc "simplifyInfer {" $ vcat
199 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
200 , ptext (sLit "wanted =") <+> ppr zonked_wanted
201 , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
204 -- Make a guess at the quantified type variables
205 -- Then split the constraints on the baisis of those tyvars
206 -- to avoid unnecessarily simplifying a class constraint
207 -- See Note [Avoid unecessary constraint simplification]
208 ; gbl_tvs <- tcGetGlobalTyVars
209 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
210 ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
211 zonked_tau_tvs `minusVarSet` gbl_tvs
212 (perhaps_bound, surely_free)
213 = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
215 ; emitConstraints surely_free
216 ; traceTc "sinf" $ vcat
217 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
218 , ptext (sLit "surely_free =") <+> ppr surely_free
221 -- Now simplify the possibly-bound constraints
222 ; (simplified_perhaps_bound, tc_binds)
223 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
225 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
226 -- may have done some unification
227 ; gbl_tvs <- tcGetGlobalTyVars
228 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
229 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
230 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
231 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
232 constrained_tvs = tyVarsOfWantedEvVars zonked_simples
233 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
234 (final_qtvs, (bound, free))
235 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
236 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
238 ; traceTc "end simplifyInfer }" $
239 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
240 , text "wanted = " <+> ppr zonked_wanted
241 , text "qtvs = " <+> ppr final_qtvs
242 , text "free = " <+> ppr free
243 , text "bound = " <+> ppr bound ]
245 -- Turn the quantified meta-type variables into real type variables
246 ; emitConstraints (mapBag WcEvVar free)
247 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
248 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
249 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
251 ------------------------
252 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
253 -> TcM (Bag WantedEvVar, Bag EvBind)
254 -- We use this function when inferring the type of a function
255 -- The wanted constraints are already zonked
256 simplifyAsMuchAsPossible ctxt wanteds
257 = do { let untch = NoUntouchables
258 -- We allow ourselves to unify environment
259 -- variables; hence *no untouchables*
261 ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
262 <- runTcS ctxt untch $
263 simplifyApproxLoop 0 wanteds
266 ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors
268 ; return (unsolved_flats, ev_binds) }
271 simplifyApproxLoop :: Int -> WantedConstraints
272 -> TcS (Bag WantedEvVar, 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 = Bag.mapBag WcEvVar unsolved_flats `unionBags`
285 Bag.mapBag WcImplic thiner_unsolved_implics
287 ; -- If no new work was produced then we are done with simplifyApproxLoop
288 if isEmptyBag extra_flats
289 then do { traceTcS "simplifyApproxLoopRes" (vcat
290 [ ptext (sLit "Wanted = ") <+> ppr wanteds
291 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
292 ; return (unsolved_flats, unsolved_implics) }
294 else -- Produced new flat work wanteds, go round the loop
295 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
298 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
299 -- (wc1, impls2) <- approximateImplications impls
300 -- splits 'impls' into two parts
301 -- wc1: a bag of constraints that do not mention any skolems
302 -- impls2: a bag of *thiner* implication constraints
303 approximateImplications impls
304 = splitBag (do_implic emptyVarSet) impls
307 do_wanted :: TcTyVarSet -> WantedConstraint
308 -> (WantedConstraints, WantedConstraints)
309 do_wanted skols (WcImplic impl)
310 = let (fl_w, mb_impl) = do_implic skols impl
311 in (fl_w, mapBag WcImplic mb_impl)
312 do_wanted skols wc@(WcEvVar wev)
313 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
314 | otherwise = (emptyBag, unitBag wc)
317 do_implic :: TcTyVarSet -> Implication
318 -> (WantedConstraints, Bag Implication)
319 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
320 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
321 else unitBag impl{ ic_wanted = rest_wanted } )
323 (floatable_wanted, rest_wanted)
324 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
327 splitBag :: (a -> (WantedConstraints, Bag a))
328 -> Bag a -> (WantedConstraints, Bag a)
329 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
332 = (wcs `unionBags` b1, imps `unionBags` b2)
338 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
339 growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
340 growWanteds gbl_tvs ws tvs
341 | isEmptyBag ws = tvs
342 | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
343 growWantedEVs gbl_tvs ws tvs
344 | isEmptyBag ws = tvs
345 | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
347 growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet
348 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
349 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
350 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
351 -- X-constraint 'wanted', nuking the 'gbls' at each stage
353 growEvVar gbl_tvs ev tvs
354 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
356 ev_tvs = growPredTyVars (evVarPred ev) tvs
358 growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
360 growWanted gbl_tvs (WcEvVar wev) tvs
361 = growWantedEV gbl_tvs wev tvs
362 growWanted gbl_tvs (WcImplic implic) tvs
363 = foldrBag (growWanted inner_gbl_tvs)
364 (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
365 -- Must grow over inner givens too
368 inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
371 quantifyMe :: TyVarSet -- Quantifying over these
373 -> Bool -- True <=> quantify over this wanted
375 | isIPPred pred = True -- Note [Inheriting implicit parameters]
376 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
378 pred = wantedEvVarPred wev
380 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
381 -- False => we can *definitely* float the WantedConstraint out
382 quantifyMeWC qtvs (WcImplic implic)
383 = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
384 || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
386 inner_qtvs = qtvs `minusVarSet` ic_skols implic
388 quantifyMeWC qtvs (WcEvVar wev)
389 = quantifyMe qtvs wev
392 Note [Avoid unecessary constraint simplification]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 When inferring the type of a let-binding, with simplifyInfer,
395 try to avoid unnecessariliy simplifying class constraints.
396 Doing so aids sharing, but it also helps with delicate
398 instance C t => C [t] where ..
400 f x = let g y = ...(constraint C [t])...
402 When inferring a type for 'g', we don't want to apply the
403 instance decl, because then we can't satisfy (C t). So we
404 just notice that g isn't quantified over 't' and partition
405 the contraints before simplifying.
407 This only half-works, but then let-generalisation only half-works.
410 Note [Inheriting implicit parameters]
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
416 where f is *not* a top-level binding.
417 From the RHS of f we'll get the constraint (?y::Int).
418 There are two types we might infer for f:
422 (so we get ?y from the context of f's definition), or
424 f :: (?y::Int) => Int -> Int
426 At first you might think the first was better, becuase then
427 ?y behaves like a free variable of the definition, rather than
428 having to be passed at each call site. But of course, the WHOLE
429 IDEA is that ?y should be passed at each call site (that's what
430 dynamic binding means) so we'd better infer the second.
432 BOTTOM LINE: when *inferring types* you *must* quantify
433 over implicit parameters. See the predicate isFreeWhenInferring.
436 *********************************************************************************
440 ***********************************************************************************
442 When constructing evidence for superclasses in an instance declaration,
443 * we MUST have the "self" dictionary available, but
444 * we must NOT have its superclasses derived from "self"
446 Moreover, we must *completely* solve the constraints right now,
447 not wrap them in an implication constraint to solve later. Why?
448 Because when that implication constraint is solved there may
449 be some unrelated other solved top-level constraints that
450 recursively depend on the superclass we are building. Consider
451 class Ord a => C a where
452 instance C [Int] where ...
455 dCListInt = MkC $cNum ...
457 $cNum :: Ord [Int] -- The superclass
458 $cNum = let self = dCListInt in <solve Ord [Int]>
460 Now, if there is some *other* top-level constraint solved
464 we must not solve the (Ord [Int]) wanted from foo!!
467 simplifySuperClass :: EvVar -- The "self" dictionary
470 simplifySuperClass self wanteds
471 = do { wanteds <- mapBagM zonkWanted wanteds
472 ; loc <- getCtLoc NoScSkol
473 ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds)
474 <- runTcS SimplCheck NoUntouchables $
475 do { can_self <- canGivens loc [self]
476 ; let inert = foldlBag updInertSet emptyInert can_self
477 -- No need for solveInteract; we know it's inert
479 ; solveWanteds inert wanteds }
481 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
482 reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors }
486 *********************************************************************************
490 ***********************************************************************************
492 Note [Simplifying RULE lhs constraints]
493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
494 On the LHS of transformation rules we only simplify only equalitis,
495 but not dictionaries. We want to keep dictionaries unsimplified, to
496 serve as the available stuff for the RHS of the rule. We *do* want to
497 simplify equalities, however, to detect ill-typed rules that cannot be
500 Implementation: the TcSFlags carried by the TcSMonad controls the
501 amount of simplification, so simplifyRuleLhs just sets the flag
504 Example. Consider the following left-hand side of a rule
505 f (x == y) (y > z) = ...
506 If we typecheck this expression we get constraints
507 d1 :: Ord a, d2 :: Eq a
508 We do NOT want to "simplify" to the LHS
509 forall x::a, y::a, z::a, d1::Ord a.
510 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
512 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
513 f ((==) d2 x y) ((>) d1 y z) = ...
515 Here is another example:
516 fromIntegral :: (Integral a, Num b) => a -> b
517 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
518 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
519 we *dont* want to get
521 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
522 because the scsel will mess up RULE matching. Instead we want
523 forall dIntegralInt, dNumInt.
524 fromIntegral Int Int dIntegralInt dNumInt = id Int
527 g (x == y) (y == z) = ..
528 where the two dictionaries are *identical*, we do NOT WANT
529 forall x::a, y::a, z::a, d1::Eq a
530 f ((==) d1 x y) ((>) d1 y z) = ...
531 because that will only match if the dict args are (visibly) equal.
532 Instead we want to quantify over the dictionaries separately.
534 In short, simplifyRuleLhs must *only* squash equalities, leaving
535 all dicts unchanged, with absolutely no sharing.
537 HOWEVER, under a nested implication things are different
539 f :: (forall a. Eq a => a->a) -> Bool -> ...
540 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
543 Here we *must* solve the wanted (Eq a) from the given (Eq a)
544 resulting from skolemising the agument type of g. So we
545 revert to SimplCheck when going under an implication.
548 simplifyRule :: RuleName
549 -> [TcTyVar] -- Explicit skolems
550 -> WantedConstraints -- Constraints from LHS
551 -> WantedConstraints -- Constraints from RHS
552 -> TcM ([EvVar], -- LHS dicts
553 TcEvBinds, -- Evidence for LHS
554 TcEvBinds) -- Evidence for RHS
555 -- See Note [Simplifying RULE lhs constraints]
556 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
557 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
558 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
560 -- Don't quantify over equalities (judgement call here)
561 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
562 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
563 -- Dicts and implicit parameters
564 ; reportUnsolvedWantedEvVars eqs
566 -- Notice that we simplify the RHS with only the explicitly
567 -- introduced skolems, allowing the RHS to constrain any
568 -- unification variables.
569 -- Then, and only then, we call zonkQuantifiedTypeVariables
570 -- Example foo :: Ord a => a -> a
571 -- foo_spec :: Int -> Int
572 -- {-# RULE "foo" foo = foo_spec #-}
573 -- Here, it's the RHS that fixes the type variable
575 -- So we don't want to make untouchable the type
576 -- variables in the envt of the RHS, because they include
577 -- the template variables of the RULE
579 -- Hence the rather painful ad-hoc treatement here
580 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
581 ; loc <- getCtLoc (RuleSkol name)
582 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
583 Implic { ic_untch = NoUntouchables
584 , ic_env = emptyNameEnv
585 , ic_skols = mkVarSet tv_bndrs
586 , ic_scoped = panic "emitImplication"
587 , ic_given = lhs_dicts
588 , ic_wanted = rhs_wanted
589 , ic_binds = rhs_binds_var
591 ; rhs_binds2 <- readTcRef evb_ref
595 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
599 *********************************************************************************
603 ***********************************************************************************
606 simplifyCheck :: SimplContext
607 -> WantedConstraints -- Wanted
609 -- Solve a single, top-level implication constraint
610 -- e.g. typically one created from a top-level type signature
611 -- f :: forall a. [a] -> [a]
613 -- We do this even if the function has no polymorphism:
617 -- (whereas for *nested* bindings we would not create
618 -- an implication constraint for g at all.)
620 -- Fails if can't solve something in the input wanteds
621 simplifyCheck ctxt wanteds
622 = do { wanteds <- mapBagM zonkWanted wanteds
624 ; traceTc "simplifyCheck {" (vcat
625 [ ptext (sLit "wanted =") <+> ppr wanteds ])
627 ; (unsolved, frozen_errors, ev_binds)
628 <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
630 ; traceTc "simplifyCheck }" $
631 ptext (sLit "unsolved =") <+> ppr unsolved
633 ; reportUnsolved unsolved frozen_errors
638 solveWanteds :: InertSet -- Given
639 -> WantedConstraints -- Wanted
640 -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why
641 -- they are WantedConstraints and not CanonicalCts
642 Bag Implication) -- Unsolved implications
643 -- solveWanteds iterates when it is able to float equalities
644 -- out of one or more of the implications
645 solveWanteds inert wanteds
646 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
647 ; can_flats <- canWanteds $ bagToList flat_wanteds
648 ; traceTcS "solveWanteds {" $
649 vcat [ text "wanteds =" <+> ppr wanteds
650 , text "inert =" <+> ppr inert ]
651 ; (unsolved_flats, unsolved_implics)
652 <- simpl_loop 1 inert can_flats implic_wanteds
653 ; bb <- getTcEvBindsBag
654 ; tb <- getTcSTyBindsMap
655 ; traceTcS "solveWanteds }" $
656 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
657 , text "unsolved_implics =" <+> ppr unsolved_implics
658 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
659 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
662 ; solveCTyFunEqs unsolved_flats unsolved_implics
663 -- See Note [Solving Family Equations]
668 -> CanonicalCts -- May inlude givens (in the recursive call)
670 -> TcS (CanonicalCts, Bag Implication)
671 simpl_loop n inert can_ws implics
673 = trace "solveWanteds: loop" $ -- Always bleat
674 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
675 ; return (can_ws, implics) }
678 = do { traceTcS "solveWanteds: simpl_loop start {" $
679 vcat [ text "n =" <+> ppr n
680 , text "can_ws =" <+> ppr can_ws
681 , text "implics =" <+> ppr implics
682 , text "inert =" <+> ppr inert ]
683 ; inert1 <- solveInteract inert can_ws
684 ; let (inert2, unsolved_flats) = extractUnsolved inert1
686 -- NB: Importantly, inerts2 may contain *more* givens than inert
687 -- because of having solved equalities from can_ws
688 ; traceTcS "solveWanteds: done flats" $
689 vcat [ text "inerts =" <+> ppr inert2
690 , text "unsolved =" <+> ppr unsolved_flats ]
692 -- See Note [Preparing inert set for implications]
693 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
694 ; traceTcS "solveWanteds: doing nested implications {" $
695 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
696 , text "implics =" <+> ppr implics ]
697 ; (implic_eqs, unsolved_implics)
698 <- flatMapBagPairM (solveImplication inert_for_implics) implics
700 ; traceTcS "solveWanteds: done nested implications }" $
701 vcat [ text "implic_eqs =" <+> ppr implic_eqs
702 , text "unsolved_implics =" <+> ppr unsolved_implics ]
704 -- Apply defaulting rules if and only if there
705 -- no floated equalities. If there are, they may
706 -- solve the remaining wanteds, so don't do defaulting.
707 ; final_eqs <- if not (isEmptyBag implic_eqs)
708 then return implic_eqs
709 else applyDefaultingRules inert2 unsolved_flats
711 -- default_eqs are *givens*, so simpl_loop may
712 -- recurse with givens in the argument
714 ; traceTcS "solveWanteds: simpl_loop end }" $
715 vcat [ text "final_eqs =" <+> ppr final_eqs
716 , text "unsolved_flats =" <+> ppr unsolved_flats
717 , text "unsolved_implics =" <+> ppr unsolved_implics ]
719 ; if isEmptyBag final_eqs then
720 return (unsolved_flats, unsolved_implics)
722 do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
723 -- final eqs is *just* a bunch of WantedEvVars
724 ; simpl_loop (n+1) inert2
725 (can_final_eqs `andCCan` unsolved_flats) unsolved_implics
726 -- Important: reiterate with inert2, not plainly inert
727 -- because inert2 may contain more givens, as the result of solving
728 -- some wanteds in the incoming can_ws
731 solveImplication :: InertSet -- Given
732 -> Implication -- Wanted
733 -> TcS (Bag WantedEvVar, -- Unsolved unification var = type
734 Bag Implication) -- Unsolved rest (always empty or singleton)
736 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
737 -- that are of the form unification var = type
739 -- 2. Maybe a unsolved implication, empty if entirely solved!
741 -- Precondition: everything is zonked by now
742 solveImplication inert
743 imp@(Implic { ic_untch = untch
744 , ic_binds = ev_binds
747 , ic_wanted = wanteds
749 = nestImplicTcS ev_binds untch $
750 recoverTcS (return (emptyBag, emptyBag)) $
751 -- Recover from nested failures. Even the top level is
752 -- just a bunch of implications, so failing at the first
754 do { traceTcS "solveImplication {" (ppr imp)
757 ; can_givens <- canGivens loc givens
758 ; given_inert <- solveInteract inert can_givens
760 -- Simplify the wanteds
761 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
763 ; let (res_flat_free, res_flat_bound)
764 = floatEqualities skols givens unsolved_flats
765 unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
766 Bag.mapBag WcImplic unsolved_implics
768 ; traceTcS "solveImplication end }" $ vcat
769 [ text "res_flat_free =" <+> ppr res_flat_free
770 , text "res_flat_bound =" <+> ppr res_flat_bound
771 , text "unsolved_implics =" <+> ppr unsolved_implics ]
773 ; let res_bag | isEmptyBag unsolved = emptyBag
774 | otherwise = unitBag (imp { ic_wanted = unsolved })
776 ; return (res_flat_free, res_bag) }
778 floatEqualities :: TcTyVarSet -> [EvVar]
779 -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
780 -- The CanonicalCts will be floated out to be used later, whereas
781 -- the remaining WantedEvVars will remain inside the implication.
782 floatEqualities skols can_given wanteds
783 | hasEqualities can_given = (emptyBag, wanteds)
784 -- Note [Float Equalities out of Implications]
785 | otherwise = partitionBag is_floatable wanteds
786 where is_floatable :: WantedEvVar -> Bool
787 is_floatable (WantedEvVar cv _)
788 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
789 is_floatable _wv = False
791 tvs_under_fsks :: Type -> TyVarSet
792 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
793 tvs_under_fsks (TyVarTy tv)
794 | not (isTcTyVar tv) = unitVarSet tv
795 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
796 | otherwise = unitVarSet tv
797 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
798 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
799 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
800 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
801 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
802 -- can mention type variables!
803 | isTyVar tv = inner_tvs `delVarSet` tv
804 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
805 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
807 inner_tvs = tvs_under_fsks ty
809 predTvs_under_fsks :: PredType -> TyVarSet
810 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
811 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
812 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
819 Note [Float Equalities out of Implications]
820 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
821 We want to float equalities out of vanilla existentials, but *not* out
822 of GADT pattern matches.
824 Note [Preparing inert set for implications]
825 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
826 Before solving the nested implications, we convert any unsolved flat wanteds
827 to givens, and add them to the inert set. Reasons:
828 a) In checking mode, suppresses unnecessary errors. We already have
829 on unsolved-wanted error; adding it to the givens prevents any
830 consequential errors from showing uop
831 b) More importantly, in inference mode, we are going to quantify over this
832 constraint, and we *don't* want to quantify over any constraints that
833 are deducible from it.
835 The unsolved wanteds are *canonical* but they may not be *inert*,
836 because when made into a given they might interact with other givens.
837 Hence the call to solveInteract. Example:
839 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
841 We were not able to solve (a ~w [beta]) but we can't just assume it as
842 given because the resulting set is not inert. Hence we have to do a
843 'solveInteract' step first
847 solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
848 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
849 -- See Note [Solving Family Equations]
850 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
851 -- where the newly generated equalities (alpha := F xi) have been substituted through.
852 solveCTyFunEqs cts implics
853 = do { untch <- getUntouchables
854 ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
855 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
858 ; mapM_ solve_one funeq_bnds
860 -- Apply the substitution through to eliminate the flatten
861 -- unification variables we substituted both in the unsolved flats and implics
863 = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
865 = Bag.mapBag (subst_impl funeq_bnds) implics
867 ; return (final_unsolved, final_implics) }
869 where solve_one (tv,(ty,cv,fl))
870 | not (typeKind ty `isSubKind` tyVarKind tv)
871 = addErrorTcS KindError fl (mkTyVarTy tv) ty
872 -- Must do a small kind check since TcCanonical invariants
873 -- on family equations only impose compatibility, not subkinding
874 | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
876 subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
877 subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv)
878 subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
880 subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
881 subst_wevar funeq_bnds (WantedEvVar v loc)
882 = let orig_ty = varType v
883 new_ty = substFunEqBnds funeq_bnds orig_ty
884 in WantedEvVar (setVarType v new_ty) loc
886 subst_impl :: FunEqBinds -> Implication -> Implication
887 subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
888 = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
891 type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
892 -- Invariant: if it contains:
893 -- [... a -> (ta,...) ... b -> (tb,...) ... ]
894 -- then 'ta' cannot mention 'b'
896 getSolvableCTyFunEqs :: Untouchables
897 -> CanonicalCts -- Precondition: all wanteds
898 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
899 getSolvableCTyFunEqs untch cts
900 = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
901 where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
906 | Just tv <- tcGetTyVar_maybe xi
907 , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
908 , Nothing <- lookup tv extra_binds -- or in extra_binds
909 -- See Note [Solving Family Equations], Point 1
910 = ASSERT ( isWanted fl )
911 let ty_orig = mkTyConApp tc xis
912 ty_bind = substFunEqBnds extra_binds ty_orig
913 in if tv `elemVarSet` tyVarsOfType ty_bind
914 then (cts_in `extendCCans` ct, extra_binds)
915 -- See Note [Solving Family Equations], Point 2
916 else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
917 -- Postcondition met because extra_binds is already applied to ty_bind
919 dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
921 substFunEqBnds :: FunEqBinds -> TcType -> TcType
922 substFunEqBnds bnds ty
923 = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
924 -- foldr works because of the FunEqBinds invariant
929 Note [Solving Family Equations]
930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
931 After we are done with simplification we may be left with constraints of the form:
932 [Wanted] F xis ~ beta
933 If 'beta' is a touchable unification variable not already bound in the TyBinds
934 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
936 When is it ok to do so?
937 1) 'beta' must not already be defaulted to something. Example:
939 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
940 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
941 have to report this as unsolved.
943 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
944 set [beta := F xis] only if beta is not among the free variables of xis.
946 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
947 of type family equations. See Inert Set invariants in TcInteract.
950 *********************************************************************************
952 * Defaulting and disamgiguation *
954 *********************************************************************************
956 Basic plan behind applyDefaulting rules:
959 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
960 For each defaultable group, do:
961 For each possible substitution for [alpha |-> tau] where `alpha' is the
962 group's variable, do:
963 1) Make up new TcEvBinds
964 2) Extend TcS with (groupVariable
965 3) given_inert <- solveOne inert (given : a ~ tau)
966 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
967 5) if unsolved == empty then
968 sneakyUnify a |-> tau
969 write the evidence bins
970 return (final_inert ++ group_constraints,[])
971 -- will contain the info (alpha |-> tau)!!
972 goto next defaultable group
973 if unsolved <> empty then
974 throw away evidence binds
975 try next substitution
976 If you've run out of substitutions for this group, too bad, you failed
978 goto next defaultable group
981 Collect all the (canonical-cts, wanteds) gathered this way.
982 - Do a solveGiven over the canonical-cts to make sure they are inert
983 ------------------------------------------------------------------------------------------
987 applyDefaultingRules :: InertSet
988 -> CanonicalCts -- All wanteds
989 -> TcS (Bag WantedEvVar) -- All wanteds again!
990 -- Return some *extra* givens, which express the
991 -- type-class-default choice
993 applyDefaultingRules inert wanteds
997 = do { untch <- getUntouchables
998 ; tv_cts <- mapM (defaultTyVar untch) $
999 varSetElems (tyVarsOfCDicts wanteds)
1001 ; info@(_, default_tys, _) <- getDefaultInfo
1002 ; let groups = findDefaultableGroups info untch wanteds
1003 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1005 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1006 , text "Type defaults =" <+> ppr deflt_cts])
1008 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1011 defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar)
1012 -- defaultTyVar is used on any un-instantiated meta type variables to
1013 -- default the kind of ? and ?? etc to *. This is important to ensure
1014 -- that instance declarations match. For example consider
1015 -- instance Show (a->b)
1016 -- foo x = show (\_ -> True)
1017 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1018 -- and that won't match the typeKind (*) in the instance decl.
1021 -- We look only at touchable type variables. No further constraints
1022 -- are going to affect these type variables, so it's time to do it by
1023 -- hand. However we aren't ready to default them fully to () or
1024 -- whatever, because the type-class defaulting rules have yet to run.
1026 defaultTyVar untch the_tv
1027 | isTouchableMetaTyVar_InRange untch the_tv
1028 , not (k `eqKind` default_k)
1029 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1030 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1031 ; return (unitBag (WantedEvVar ev loc)) }
1033 = return emptyBag -- The common case
1035 k = tyVarKind the_tv
1036 default_k = defaultKind k
1040 findDefaultableGroups
1043 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1044 -> Untouchables -- Untouchable
1045 -> CanonicalCts -- Unsolved
1046 -> [[(CanonicalCt,TcTyVar)]]
1047 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1049 | not (performDefaulting ctxt) = []
1050 | null default_tys = []
1051 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1053 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1054 non_unaries :: [CanonicalCt] -- and *other* constraints
1056 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1057 -- Finds unary type-class constraints
1058 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1059 | Just tv <- tcGetTyVar_maybe ty
1061 find_unary cc = Right cc -- Non unary or non dictionary
1063 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1064 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1066 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1068 is_defaultable_group ds@((_,tv):_)
1069 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1070 && not (tv `elemVarSet` bad_tvs)
1071 && isTouchableMetaTyVar_InRange untch tv
1072 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1073 is_defaultable_group [] = panic "defaultable_group"
1075 defaultable_classes clss
1076 | extended_defaults = any isInteractiveClass clss
1077 | otherwise = all is_std_class clss && (any is_num_class clss)
1079 -- In interactive mode, or with -XExtendedDefaultRules,
1080 -- we default Show a to Show () to avoid graututious errors on "show []"
1081 isInteractiveClass cls
1082 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1084 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1085 -- is_num_class adds IsString to the standard numeric classes,
1086 -- when -foverloaded-strings is enabled
1088 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1089 -- Similarly is_std_class
1091 ------------------------------
1092 disambigGroup :: [Type] -- The default types
1093 -> InertSet -- Given inert
1094 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1095 -- sharing same type variable
1096 -> TcS (Bag WantedEvVar)
1098 disambigGroup [] _inert _grp
1100 disambigGroup (default_ty:default_tys) inert group
1101 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1102 ; let ct_loc = get_ct_loc (cc_flavor the_ct)
1103 ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
1104 ; let wanted_eq = CTyEqCan { cc_id = ev
1105 , cc_flavor = Wanted ct_loc
1107 , cc_rhs = default_ty }
1108 ; success <- tryTcS $
1109 do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
1110 ; let (_, unsolved) = extractUnsolved final_inert
1111 ; errs <- getTcSErrorsBag
1112 ; return (isEmptyBag unsolved && isEmptyBag errs) }
1115 True -> -- Success: record the type variable binding, and return
1116 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1117 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1118 ; return (unitBag $ WantedEvVar ev ct_loc) }
1119 False -> -- Failure: try with the next type
1120 do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
1121 ; disambigGroup default_tys inert group } }
1123 ((the_ct,the_tv):_) = group
1124 wanteds = map fst group
1125 wanted_ev_vars = map deCanonicaliseWanted wanteds
1127 get_ct_loc (Wanted l) = l
1128 get_ct_loc _ = panic "Asked to disambiguate given or derived!"
1133 Note [Avoiding spurious errors]
1134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1135 When doing the unification for defaulting, we check for skolem
1136 type variables, and simply don't default them. For example:
1137 f = (*) -- Monomorphic
1138 g :: Num a => a -> a
1140 Here, we get a complaint when checking the type signature for g,
1141 that g isn't polymorphic enough; but then we get another one when
1142 dealing with the (Num a) context arising from f's definition;
1143 we try to unify a with Int (to default it), but find that it's
1144 already been unified with the rigid variable from g's type sig