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 (varSetElems 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 ; (simple_wanted, tc_binds)
202 <- simplifyAsMuchAsPossible SimplInfer zonked_wanted
204 ; gbl_tvs <- tcGetGlobalTyVars
205 ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
206 ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted
207 ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
208 (bound, free) | apply_mr = (emptyBag, zonked_simples)
209 | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
211 ; traceTc "end simplifyInfer }" $
212 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
213 , text "wanted = " <+> ppr zonked_wanted
214 , text "qtvs = " <+> ppr qtvs
215 , text "free = " <+> ppr free
216 , text "bound = " <+> ppr bound ]
218 -- Turn the quantified meta-type variables into real type variables
219 ; emitConstraints (mapBag WcEvVar free)
220 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
221 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
222 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
224 ------------------------
225 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
226 -> TcM (Bag WantedEvVar, Bag EvBind)
227 -- We use this function when inferring the type of a function
228 -- The wanted constraints are already zonked
229 simplifyAsMuchAsPossible ctxt wanteds
230 = do { let untch = emptyVarSet
231 -- We allow ourselves to unify environment
232 -- variables; hence *no untouchables*
234 ; ((unsolved_flats, unsolved_implics), ev_binds)
235 <- runTcS ctxt untch $
236 simplifyApproxLoop 0 wanteds
239 ; mapBagM_ reportUnsolvedImplication unsolved_implics
241 ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
242 ; return (final_wanted_evvars, ev_binds) }
245 simplifyApproxLoop :: Int -> WantedConstraints
246 -> TcS (CanonicalCts, Bag Implication)
247 simplifyApproxLoop n wanteds
249 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
251 = do { traceTcS "simplifyApproxLoop" (vcat
252 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
253 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
255 ; let (extra_flats, thiner_unsolved_implics)
256 = approximateImplications unsolved_implics
258 = mkWantedConstraints unsolved_flats thiner_unsolved_implics
260 ;-- If no new work was produced then we are done with simplifyApproxLoop
261 if isEmptyBag extra_flats
262 then do { traceTcS "simplifyApproxLoopRes" (vcat
263 [ ptext (sLit "Wanted = ") <+> ppr wanteds
264 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
265 ; return (unsolved_flats, unsolved_implics) }
267 else -- Produced new flat work wanteds, go round the loop
268 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
271 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
272 -- (wc1, impls2) <- approximateImplications impls
273 -- splits 'impls' into two parts
274 -- wc1: a bag of constraints that do not mention any skolems
275 -- impls2: a bag of *thiner* implication constraints
276 approximateImplications impls
277 = splitBag (do_implic emptyVarSet) impls
280 do_wanted :: TcTyVarSet -> WantedConstraint
281 -> (WantedConstraints, WantedConstraints)
282 do_wanted skols (WcImplic impl)
283 = let (fl_w, mb_impl) = do_implic skols impl
284 in (fl_w, mapBag WcImplic mb_impl)
285 do_wanted skols wc@(WcEvVar wev)
286 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
287 | otherwise = (emptyBag, unitBag wc)
290 do_implic :: TcTyVarSet -> Implication
291 -> (WantedConstraints, Bag Implication)
292 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
293 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
294 else unitBag impl{ ic_wanted = rest_wanted } )
296 (floatable_wanted, rest_wanted)
297 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
300 splitBag :: (a -> (WantedConstraints, Bag a))
301 -> Bag a -> (WantedConstraints, Bag a)
302 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
305 = (wcs `unionBags` b1, imps `unionBags` b2)
311 findQuantifiedTyVars :: Bool -- Apply the MR
312 -> Bag WantedEvVar -- Simplified constraints from RHS
313 -> TyVarSet -- Free in tau-type of definition
314 -> TyVarSet -- Free in the envt
315 -> TyVarSet -- Quantify over these
317 findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
318 | isEmptyBag wanteds = init_tvs
319 | apply_mr = init_tvs `minusVarSet` constrained_tvs
320 | otherwise = fixVarSet mk_next init_tvs
322 init_tvs = tau_tvs `minusVarSet` gbl_tvs
323 mk_next tvs = foldrBag grow_one tvs wanteds
325 grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
327 extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
329 constrained_tvs = tyVarsOfWantedEvVars wanteds
332 quantifyMe :: TyVarSet -- Quantifying over these
334 -> Bool -- True <=> quantify over this wanted
336 | isIPPred pred = True -- Note [Inheriting implicit parameters]
337 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
339 pred = wantedEvVarPred wev
342 Note [Inheriting implicit parameters]
343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
348 where f is *not* a top-level binding.
349 From the RHS of f we'll get the constraint (?y::Int).
350 There are two types we might infer for f:
354 (so we get ?y from the context of f's definition), or
356 f :: (?y::Int) => Int -> Int
358 At first you might think the first was better, becuase then
359 ?y behaves like a free variable of the definition, rather than
360 having to be passed at each call site. But of course, the WHOLE
361 IDEA is that ?y should be passed at each call site (that's what
362 dynamic binding means) so we'd better infer the second.
364 BOTTOM LINE: when *inferring types* you *must* quantify
365 over implicit parameters. See the predicate isFreeWhenInferring.
368 *********************************************************************************
372 ***********************************************************************************
374 When constructing evidence for superclasses in an instance declaration,
375 * we MUST have the "self" dictionary available, but
376 * we must NOT have its superclasses derived from "self"
378 Moreover, we must *completely* solve the constraints right now,
379 not wrap them in an implication constraint to solve later. Why?
380 Because when that implication constraint is solved there may
381 be some unrelated other solved top-level constraints that
382 recursively depend on the superclass we are building. Consider
383 class Ord a => C a where
384 instance C [Int] where ...
387 dCListInt = MkC $cNum ...
389 $cNum :: Ord [Int] -- The superclass
390 $cNum = let self = dCListInt in <solve Ord [Int]>
392 Now, if there is some *other* top-level constraint solved
396 we must not solve the (Ord [Int]) wanted from foo!!
399 simplifySuperClass :: EvVar -- The "self" dictionary
402 simplifySuperClass self wanteds
403 = do { wanteds <- mapBagM zonkWanted wanteds
404 ; loc <- getCtLoc NoScSkol
405 ; (unsolved, ev_binds)
406 <- runTcS SimplCheck emptyVarSet $
407 do { can_self <- canGivens loc [self]
408 ; let inert = foldlBag extendInertSet emptyInert can_self
409 -- No need for solveInteract; we know it's inert
411 ; solveWanteds inert wanteds }
413 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
414 reportUnsolved unsolved }
418 *********************************************************************************
422 ***********************************************************************************
424 Note [Simplifying RULE lhs constraints]
425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
426 On the LHS of transformation rules we only simplify only equalitis,
427 but not dictionaries. We want to keep dictionaries unsimplified, to
428 serve as the available stuff for the RHS of the rule. We *do* want to
429 simplify equalities, however, to detect ill-typed rules that cannot be
432 Implementation: the TcSFlags carried by the TcSMonad controls the
433 amount of simplification, so simplifyRuleLhs just sets the flag
436 Example. Consider the following left-hand side of a rule
437 f (x == y) (y > z) = ...
438 If we typecheck this expression we get constraints
439 d1 :: Ord a, d2 :: Eq a
440 We do NOT want to "simplify" to the LHS
441 forall x::a, y::a, z::a, d1::Ord a.
442 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
444 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
445 f ((==) d2 x y) ((>) d1 y z) = ...
447 Here is another example:
448 fromIntegral :: (Integral a, Num b) => a -> b
449 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
450 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
451 we *dont* want to get
453 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
454 because the scsel will mess up RULE matching. Instead we want
455 forall dIntegralInt, dNumInt.
456 fromIntegral Int Int dIntegralInt dNumInt = id Int
459 g (x == y) (y == z) = ..
460 where the two dictionaries are *identical*, we do NOT WANT
461 forall x::a, y::a, z::a, d1::Eq a
462 f ((==) d1 x y) ((>) d1 y z) = ...
463 because that will only match if the dict args are (visibly) equal.
464 Instead we want to quantify over the dictionaries separately.
466 In short, simplifyRuleLhs must *only* squash equalities, leaving
467 all dicts unchanged, with absolutely no sharing.
469 HOWEVER, under a nested implication things are different
471 f :: (forall a. Eq a => a->a) -> Bool -> ...
472 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
475 Here we *must* solve the wanted (Eq a) from the given (Eq a)
476 resulting from skolemising the agument type of g. So we
477 revert to SimplCheck when going under an implication.
480 simplifyRule :: RuleName
481 -> [TcTyVar] -- Explicit skolems
482 -> WantedConstraints -- Constraints from LHS
483 -> WantedConstraints -- Constraints from RHS
484 -> TcM ([EvVar], -- LHS dicts
485 TcEvBinds, -- Evidence for LHS
486 TcEvBinds) -- Evidence for RHS
487 -- See Note [Simplifying RULE lhs constraints]
488 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
489 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
490 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
492 -- Don't quantify over equalities (judgement call here)
493 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
494 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
495 -- Dicts and implicit parameters
496 ; reportUnsolvedWantedEvVars eqs
498 -- Notice that we simplify the RHS with only the explicitly
499 -- introduced skolems, allowing the RHS to constrain any
500 -- unification variables.
501 -- Then, and only then, we call zonkQuantifiedTypeVariables
502 -- Example foo :: Ord a => a -> a
503 -- foo_spec :: Int -> Int
504 -- {-# RULE "foo" foo = foo_spec #-}
505 -- Here, it's the RHS that fixes the type variable
507 -- So we don't want to make untouchable the type
508 -- variables in the envt of the RHS, because they include
509 -- the template variables of the RULE
511 -- Hence the rather painful ad-hoc treatement here
512 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
513 ; loc <- getCtLoc (RuleSkol name)
514 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
515 Implic { ic_env_tvs = emptyVarSet -- No untouchables
516 , ic_env = emptyNameEnv
517 , ic_skols = mkVarSet tv_bndrs
518 , ic_scoped = panic "emitImplication"
519 , ic_given = lhs_dicts
520 , ic_wanted = rhs_wanted
521 , ic_binds = rhs_binds_var
523 ; rhs_binds2 <- readTcRef evb_ref
527 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
531 *********************************************************************************
535 ***********************************************************************************
538 simplifyCheck :: SimplContext
539 -> WantedConstraints -- Wanted
541 -- Solve a single, top-level implication constraint
542 -- e.g. typically one created from a top-level type signature
543 -- f :: forall a. [a] -> [a]
545 -- We do this even if the function has no polymorphism:
549 -- (whereas for *nested* bindings we would not create
550 -- an implication constraint for g at all.)
552 -- Fails if can't solve something in the input wanteds
553 simplifyCheck ctxt wanteds
554 = do { wanteds <- mapBagM zonkWanted wanteds
556 ; traceTc "simplifyCheck {" (vcat
557 [ ptext (sLit "wanted =") <+> ppr wanteds ])
559 ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
560 solveWanteds emptyInert wanteds
562 ; traceTc "simplifyCheck }" $
563 ptext (sLit "unsolved =") <+> ppr unsolved
565 ; reportUnsolved unsolved
570 solveWanteds :: InertSet -- Given
571 -> WantedConstraints -- Wanted
572 -> TcS (CanonicalCts, -- Unsolved flats
573 Bag Implication) -- Unsolved implications
574 -- solveWanteds iterates when it is able to float equalities
575 -- out of one or more of the implications
576 solveWanteds inert wanteds
577 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
578 ; can_flats <- canWanteds $ bagToList flat_wanteds
579 ; traceTcS "solveWanteds {" $
580 vcat [ text "wanteds =" <+> ppr wanteds
581 , text "inert =" <+> ppr inert ]
582 ; (unsolved_flats, unsolved_implics)
583 <- simpl_loop 1 can_flats implic_wanteds
584 ; traceTcS "solveWanteds }" $
585 vcat [ text "wanteds =" <+> ppr wanteds
586 , text "unsolved_flats =" <+> ppr unsolved_flats
587 , text "unsolved_implics =" <+> ppr unsolved_implics ]
588 ; return (unsolved_flats, unsolved_implics) }
591 -> CanonicalCts -- May inlude givens (in the recursive call)
593 -> TcS (CanonicalCts, Bag Implication)
594 simpl_loop n can_ws implics
596 = trace "solveWanteds: loop" $ -- Always bleat
597 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
598 ; return (can_ws, implics) }
601 = do { inert1 <- solveInteract inert can_ws
602 ; let (inert2, unsolved_flats) = extractUnsolved inert1
604 ; traceTcS "solveWanteds/done flats" $
605 vcat [ text "inerts =" <+> ppr inert2
606 , text "unsolved =" <+> ppr unsolved_flats ]
608 -- See Note [Preparing inert set for implications]
609 ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
610 ; (implic_eqs, unsolved_implics)
611 <- flatMapBagPairM (solveImplication inert_for_implics) implics
613 -- Apply defaulting rules if and only if there
614 -- no floated equalities. If there are, they may
615 -- solve the remaining wanteds, so don't do defaulting.
616 ; final_eqs <- if not (isEmptyBag implic_eqs)
617 then return implic_eqs
618 else applyDefaultingRules inert2 unsolved_flats
619 -- default_eqs are *givens*, so simpl_loop may
620 -- recurse with givens in the argument
622 ; if isEmptyBag final_eqs then
623 return (unsolved_flats, unsolved_implics)
625 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
626 [ text "floated_unsolved_eqs =" <+> ppr final_eqs
627 , text "unsolved_implics = " <+> ppr unsolved_implics ]
629 (unsolved_flats `unionBags` final_eqs)
633 solveImplication :: InertSet -- Given
634 -> Implication -- Wanted
635 -> TcS (CanonicalCts, -- Unsolved unification var = type
636 Bag Implication) -- Unsolved rest (always empty or singleton)
638 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
639 -- that are of the form unification var = type
641 -- 2. Maybe a unsolved implication, empty if entirely solved!
643 -- Precondition: everything is zonked by now
644 solveImplication inert
645 imp@(Implic { ic_env_tvs = untch
646 , ic_binds = ev_binds
649 , ic_wanted = wanteds
651 = nestImplicTcS ev_binds untch $
652 do { traceTcS "solveImplication {" (ppr imp)
655 ; can_givens <- canGivens loc givens
656 ; given_inert <- solveInteract inert can_givens
658 -- Simplify the wanteds
659 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
661 ; let (res_flat_free, res_flat_bound)
662 = floatEqualities skols givens unsolved_flats
663 unsolved = mkWantedConstraints res_flat_bound unsolved_implics
665 ; traceTcS "solveImplication end }" $ vcat
666 [ text "res_flat_free =" <+> ppr res_flat_free
667 , text "res_flat_bound =" <+> ppr res_flat_bound
668 , text "unsolved_implics =" <+> ppr unsolved_implics ]
670 ; let res_bag | isEmptyBag unsolved = emptyBag
671 | otherwise = unitBag (imp { ic_wanted = unsolved })
673 ; return (res_flat_free, res_bag) }
675 floatEqualities :: TcTyVarSet -> [EvVar]
676 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
677 floatEqualities skols can_given wanteds
678 | hasEqualities can_given = (emptyBag, wanteds)
679 | otherwise = partitionBag is_floatable wanteds
681 is_floatable :: CanonicalCt -> Bool
682 is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
683 | isMetaTyVar tv || isMetaTyVarTy ty
684 = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
685 is_floatable _ = False
688 Note [Preparing inert set for implications]
689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
690 Before solving the nested implications, we convert any unsolved flat wanteds
691 to givens, and add them to the inert set. Reasons:
692 a) In checking mode, suppresses unnecessary errors. We already have
693 on unsolved-wanted error; adding it to the givens prevents any
694 consequential errors from showing uop
695 b) More importantly, in inference mode, we are going to quantify over this
696 constraint, and we *don't* want to quantify over any constraints that
697 are deducible from it.
699 The unsolved wanteds are *canonical* but they may not be *inert*,
700 because when made into a given they might interact with other givens.
701 Hence the call to solveInteract. Example:
703 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
705 We were not able to solve (a ~w [beta]) but we can't just assume it as
706 given because the resulting set is not inert. Hence we have to do a
707 'solveInteract' step first
709 *********************************************************************************
711 * Defaulting and disamgiguation *
713 *********************************************************************************
715 Basic plan behind applyDefaulting rules:
718 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
719 For each defaultable group, do:
720 For each possible substitution for [alpha |-> tau] where `alpha' is the
721 group's variable, do:
722 1) Make up new TcEvBinds
723 2) Extend TcS with (groupVariable
724 3) given_inert <- solveOne inert (given : a ~ tau)
725 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
726 5) if unsolved == empty then
727 sneakyUnify a |-> tau
728 write the evidence bins
729 return (final_inert ++ group_constraints,[])
730 -- will contain the info (alpha |-> tau)!!
731 goto next defaultable group
732 if unsolved <> empty then
733 throw away evidence binds
734 try next substitution
735 If you've run out of substitutions for this group, too bad, you failed
737 goto next defaultable group
740 Collect all the (canonical-cts, wanteds) gathered this way.
741 - Do a solveGiven over the canonical-cts to make sure they are inert
742 ------------------------------------------------------------------------------------------
746 applyDefaultingRules :: InertSet
747 -> CanonicalCts -- All wanteds
749 -- Return some *extra* givens, which express the
750 -- type-class-default choice
752 applyDefaultingRules inert wanteds
756 = do { untch <- getUntouchablesTcS
757 ; tv_cts <- mapM (defaultTyVar untch) $
758 varSetElems (tyVarsOfCanonicals wanteds)
760 ; info@(_, default_tys, _) <- getDefaultInfo
761 ; let groups = findDefaultableGroups info untch wanteds
762 ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
764 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
765 , text "Type defaults =" <+> ppr deflt_cts])
767 ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
770 defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
771 -- defaultTyVar is used on any un-instantiated meta type variables to
772 -- default the kind of ? and ?? etc to *. This is important to ensure
773 -- that instance declarations match. For example consider
774 -- instance Show (a->b)
775 -- foo x = show (\_ -> True)
776 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
777 -- and that won't match the typeKind (*) in the instance decl.
780 -- We look only at touchable type variables. No further constraints
781 -- are going to affect these type variables, so it's time to do it by
782 -- hand. However we aren't ready to default them fully to () or
783 -- whatever, because the type-class defaulting rules have yet to run.
785 defaultTyVar untch the_tv
787 , not (the_tv `elemVarSet` untch)
788 , not (k `eqKind` default_k)
789 = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
790 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
791 -- 'DefaultOrigin' is strictly the declaration, but it's convenient
792 wanted_eq = CTyEqCan { cc_id = ev
793 , cc_flavor = Wanted loc
795 , cc_rhs = better_ty }
796 ; return (unitBag wanted_eq) }
799 = return emptyCCan -- The common case
802 default_k = defaultKind k
806 findDefaultableGroups
809 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
810 -> TcTyVarSet -- Untouchable
811 -> CanonicalCts -- Unsolved
812 -> [[(CanonicalCt,TcTyVar)]]
813 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
815 | not (performDefaulting ctxt) = []
816 | null default_tys = []
817 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
819 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
820 non_unaries :: [CanonicalCt] -- and *other* constraints
822 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
823 -- Finds unary type-class constraints
824 find_unary cc@(CDictCan { cc_tyargs = [ty] })
825 | Just tv <- tcGetTyVar_maybe ty
827 find_unary cc = Right cc -- Non unary or non dictionary
829 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
830 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
832 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
834 is_defaultable_group ds@((_,tv):_)
835 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
836 && not (tv `elemVarSet` bad_tvs)
837 && not (tv `elemVarSet` untch) -- Non untouchable
838 && defaultable_classes [cc_class cc | (cc,_) <- ds]
839 is_defaultable_group [] = panic "defaultable_group"
841 defaultable_classes clss
842 | extended_defaults = any isInteractiveClass clss
843 | otherwise = all is_std_class clss && (any is_num_class clss)
845 -- In interactive mode, or with -XExtendedDefaultRules,
846 -- we default Show a to Show () to avoid graututious errors on "show []"
847 isInteractiveClass cls
848 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
850 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
851 -- is_num_class adds IsString to the standard numeric classes,
852 -- when -foverloaded-strings is enabled
854 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
855 -- Similarly is_std_class
857 ------------------------------
858 disambigGroup :: [Type] -- The default types
859 -> TcTyVarSet -- Untouchables
860 -> InertSet -- Given inert
861 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
862 -- sharing same type variable
865 disambigGroup [] _inert _untch _grp
867 disambigGroup (default_ty:default_tys) untch inert group
868 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
869 ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
870 -- We know this equality is canonical,
871 -- so we directly construct it as such
872 ; let given_eq = CTyEqCan { cc_id = ev
873 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
875 , cc_rhs = default_ty }
877 ; success <- tryTcS (extendVarSet untch the_tv) $
878 do { given_inert <- solveOne inert given_eq
879 ; final_inert <- solveInteract given_inert (listToBag wanteds)
880 ; let (_, unsolved) = extractUnsolved final_inert
881 ; return (isEmptyBag unsolved) }
884 True -> -- Success: record the type variable binding, and return
885 do { setWantedTyBind the_tv default_ty
886 ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
887 ; traceTcS "disambigGoup succeeded" (ppr default_ty)
888 ; return (unitBag given_eq) }
889 False -> -- Failure: try with the next type
890 do { traceTcS "disambigGoup succeeded" (ppr default_ty)
891 ; disambigGroup default_tys untch inert group } }
893 ((the_ct,the_tv):_) = group
894 wanteds = map fst group
895 wanted_ev_vars = map deCanonicaliseWanted wanteds
898 Note [Avoiding spurious errors]
899 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
900 When doing the unification for defaulting, we check for skolem
901 type variables, and simply don't default them. For example:
902 f = (*) -- Monomorphic
905 Here, we get a complaint when checking the type signature for g,
906 that g isn't polymorphic enough; but then we get another one when
907 dealing with the (Num a) context arising from f's definition;
908 we try to unify a with Int (to default it), but find that it's
909 already been unified with the rigid variable from g's type sig