4 simplifyDefault, simplifyDeriv,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
18 import Id ( evVarPred )
19 import Unify ( niFixTvSubst, niSubstTvSet )
27 import NameEnv ( emptyNameEnv )
33 import Class ( classKey )
34 import BasicTypes ( RuleName, TopLevelFlag, isTopLevel )
35 import Control.Monad ( when )
41 *********************************************************************************
43 * External interface *
45 *********************************************************************************
48 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
49 -- Simplify top-level constraints
50 -- Usually these will be implications,
51 -- but when there is nothing to quantify we don't wrap
52 -- in a degenerate implication, so we do that here instead
54 = simplifyCheck SimplCheck wanteds
57 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
58 simplifyInteractive wanteds
59 = simplifyCheck SimplInteractive wanteds
62 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
63 -> TcM () -- Succeeds iff the constraint is soluble
65 = do { wanted <- newFlatWanteds DefaultOrigin theta
66 ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted)
72 *********************************************************************************
76 ***********************************************************************************
79 simplifyDeriv :: CtOrigin
81 -> ThetaType -- Wanted
82 -> TcM ThetaType -- Needed
83 -- Given instance (wanted) => C inst_ty
84 -- Simplify 'wanted' as much as possibles
85 -- Fail if not possible
86 simplifyDeriv orig tvs theta
87 = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
88 -- The constraint solving machinery
89 -- expects *TcTyVars* not TyVars.
90 -- We use *non-overlappable* (vanilla) skolems
91 -- See Note [Overlap and deriving]
93 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
94 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
96 ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
98 ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
99 ; (residual_wanted, _binds)
100 <- runTcS SimplInfer NoUntouchables $
101 solveWanteds emptyInert (mkFlatWC wanted)
103 ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
104 -- See Note [Exotic derived instance contexts]
105 get_good :: WantedEvVar -> Either PredType WantedEvVar
106 get_good wev | validDerivPred p = Left p
107 | otherwise = Right wev
108 where p = evVarOfPred wev
110 ; reportUnsolved (residual_wanted { wc_flat = bad })
112 ; let min_theta = mkMinimalBySCs (bagToList good)
113 ; return (substTheta subst_skol min_theta) }
116 Note [Overlap and deriving]
117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
118 Consider some overlapping instances:
119 data Show a => Show [a] where ..
120 data Show [Char] where ...
122 Now a data type with deriving:
123 data T a = MkT [a] deriving( Show )
125 We want to get the derived instance
126 instance Show [a] => Show (T a) where...
128 instance Show a => Show (T a) where...
129 so that the (Show (T Char)) instance does the Right Thing
131 It's very like the situation when we're inferring the type
135 f :: Show [a] => a -> String
137 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
138 the context for the derived instance.
139 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
141 Note [Exotic derived instance contexts]
142 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
143 In a 'derived' instance declaration, we *infer* the context. It's a
144 bit unclear what rules we should apply for this; the Haskell report is
145 silent. Obviously, constraints like (Eq a) are fine, but what about
146 data T f a = MkT (f a) deriving( Eq )
147 where we'd get an Eq (f a) constraint. That's probably fine too.
149 One could go further: consider
150 data T a b c = MkT (Foo a b c) deriving( Eq )
151 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
153 Notice that this instance (just) satisfies the Paterson termination
154 conditions. Then we *could* derive an instance decl like this:
156 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
157 even though there is no instance for (C Int a), because there just
158 *might* be an instance for, say, (C Int Bool) at a site where we
159 need the equality instance for T's.
161 However, this seems pretty exotic, and it's quite tricky to allow
162 this, and yet give sensible error messages in the (much more common)
163 case where we really want that instance decl for C.
165 So for now we simply require that the derived instance context
166 should have only type-variable constraints.
168 Here is another example:
169 data Fix f = In (f (Fix f)) deriving( Eq )
170 Here, if we are prepared to allow -XUndecidableInstances we
171 could derive the instance
172 instance Eq (f (Fix f)) => Eq (Fix f)
173 but this is so delicate that I don't think it should happen inside
174 'deriving'. If you want this, write it yourself!
176 NB: if you want to lift this condition, make sure you still meet the
177 termination conditions! If not, the deriving mechanism generates
178 larger and larger constraints. Example:
180 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
182 Note the lack of a Show instance for Succ. First we'll generate
183 instance (Show (Succ a), Show a) => Show (Seq a)
185 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
186 and so on. Instead we want to complain of no instance for (Show (Succ a)).
190 Allow constraints which consist only of type variables, with no repeats.
192 *********************************************************************************
196 ***********************************************************************************
199 simplifyInfer :: TopLevelFlag
200 -> Bool -- Apply monomorphism restriction
201 -> [(Name, TcTauType)] -- Variables to be generalised,
202 -- and their tau-types
204 -> TcM ([TcTyVar], -- Quantify over these type variables
205 [EvVar], -- ... and these constraints
206 TcEvBinds) -- ... binding these evidence variables
207 simplifyInfer top_lvl apply_mr name_taus wanteds
209 = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
210 ; zonked_taus <- zonkTcTypes (map snd name_taus)
211 ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
212 ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
213 ; return (qtvs, [], emptyTcEvBinds) }
216 = do { zonked_wanteds <- zonkWC wanteds
217 ; zonked_taus <- zonkTcTypes (map snd name_taus)
218 ; gbl_tvs <- tcGetGlobalTyVars
220 ; traceTc "simplifyInfer {" $ vcat
221 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
222 , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
223 , ptext (sLit "wanted =") <+> ppr zonked_wanteds
227 -- Make a guess at the quantified type variables
228 -- Then split the constraints on the baisis of those tyvars
229 -- to avoid unnecessarily simplifying a class constraint
230 -- See Note [Avoid unecessary constraint simplification]
231 ; let zonked_tau_tvs = get_tau_tvs zonked_taus
232 proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
233 zonked_tau_tvs `minusVarSet` gbl_tvs
234 (perhaps_bound, surely_free)
235 = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
237 ; traceTc "simplifyInfer proto" $ vcat
238 [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
239 , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
240 , ptext (sLit "surely_fref =") <+> ppr surely_free
243 ; emitFlats surely_free
244 ; traceTc "sinf" $ vcat
245 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
246 , ptext (sLit "surely_free =") <+> ppr surely_free
250 -- Now simplify the possibly-bound constraints
251 ; (simpl_results, tc_binds0)
252 <- runTcS SimplInfer NoUntouchables $
253 simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
255 ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
256 (do { reportUnsolved simpl_results; failM })
259 -- Split again simplified_perhaps_bound, because some unifications
260 -- may have happened, and emit the free constraints.
261 ; gbl_tvs <- tcGetGlobalTyVars
262 ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
263 ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
264 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
265 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
266 constrained_tvs = tyVarsOfEvVarXs zonked_simples
267 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
268 (final_qtvs, (bound, free))
269 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
270 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
273 ; if isEmptyVarSet final_qtvs && isEmptyBag bound
274 then ASSERT( isEmptyBag (wc_insol simpl_results) )
275 do { traceTc "} simplifyInfer/no quantification" empty
276 ; emitImplications (wc_impl simpl_results)
277 ; return ([], [], EvBinds tc_binds0) }
280 -- Step 4, zonk quantified variables
281 { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
282 ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
283 | (name, ty) <- name_taus ]
284 -- Don't add the quantified variables here, because
285 -- they are also bound in ic_skols and we want them to be
287 skol_info = InferSkol poly_ids
289 ; gloc <- getCtLoc skol_info
290 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
293 -- Minimize `bound' and emit an implication
294 ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
295 ; ev_binds_var <- newTcEvBinds
296 ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
297 ; lcl_env <- getLclTypeEnv
298 ; let implic = Implic { ic_untch = NoUntouchables
300 , ic_skols = mkVarSet qtvs_to_return
301 , ic_given = minimal_bound_ev_vars
302 , ic_wanted = simpl_results { wc_flat = bound }
304 , ic_binds = ev_binds_var
306 ; emitImplication implic
307 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
308 vcat [ ptext (sLit "implic =") <+> ppr implic
309 -- ic_skols, ic_given give rest of result
310 , ptext (sLit "qtvs =") <+> ppr final_qtvs
311 , ptext (sLit "spb =") <+> ppr zonked_simples
312 , ptext (sLit "bound =") <+> ppr bound ]
316 ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
318 get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
319 | otherwise = exactTyVarsOfTypes
320 -- See Note [Silly type synonym] in TcType
324 Note [Minimize by Superclasses]
325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
327 When we quantify over a constraint, in simplifyInfer we need to
328 quantify over a constraint that is minimal in some sense: For
329 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
330 we'd like to quantify over Ord alpha, because we can just get Eq alpha
331 from superclass selection from Ord alpha. This minimization is what
332 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
333 to check the original wanted.
336 simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
337 simplifyWithApprox wanted
338 = do { traceTcS "simplifyApproxLoop" (ppr wanted)
340 ; results <- solveWanteds emptyInert wanted
342 ; let (residual_implics, floats) = approximateImplications (wc_impl results)
344 -- If no new work was produced then we are done with simplifyApproxLoop
345 ; if insolubleWC results || isEmptyBag floats
348 else solveWanteds emptyInert
349 (WC { wc_flat = floats `unionBags` wc_flat results
350 , wc_impl = residual_implics
351 , wc_insol = emptyBag }) }
353 approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
354 -- Extracts any nested constraints that don't mention the skolems
355 approximateImplications impls
356 = do_bag (float_implic emptyVarSet) impls
358 do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
359 do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
360 plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
361 plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
363 float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
364 float_implic skols imp
365 = (unitBag (imp { ic_wanted = wanted' }), floats)
367 (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
369 float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
370 = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
372 (flat', floats1) = do_bag (float_flat skols) flat
373 (implic', floats2) = do_bag (float_implic skols) implic
375 float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
377 | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
378 | otherwise = (unitBag wev, emptyBag)
382 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
383 -- X-constraint 'wanted', nuking the 'gbls' at each stage
384 -- It's conservative in that if the seed could *possibly*
385 -- grow to include a type variable, then it does
387 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
388 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
390 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
391 growWantedEVs gbl_tvs ws tvs
392 | isEmptyBag ws = tvs
393 | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
395 -------- Helper functions, do not do fixpoint ------------------------
396 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
397 growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) .
398 growPreds gbl_tvs evVarOfPred (wc_flat wc) .
399 growPreds gbl_tvs evVarOfPred (wc_insol wc)
401 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
402 growImplics gbl_tvs implics tvs
403 = foldrBag grow_implic tvs implics
405 grow_implic implic tvs
406 = grow tvs `minusVarSet` ic_skols implic
408 grow = growWC gbl_tvs (ic_wanted implic) .
409 growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
410 -- We must grow from givens too; see test IPRun
412 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
413 growPreds gbl_tvs get_pred items tvs
414 = foldrBag extend tvs items
416 extend item tvs = tvs `unionVarSet`
417 (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
420 quantifyMe :: TyVarSet -- Quantifying over these
422 -> Bool -- True <=> quantify over this wanted
424 | isIPPred pred = True -- Note [Inheriting implicit parameters]
425 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
427 pred = evVarOfPred wev
430 Note [Avoid unecessary constraint simplification]
431 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
432 When inferring the type of a let-binding, with simplifyInfer,
433 try to avoid unnecessariliy simplifying class constraints.
434 Doing so aids sharing, but it also helps with delicate
436 instance C t => C [t] where ..
438 f x = let g y = ...(constraint C [t])...
440 When inferring a type for 'g', we don't want to apply the
441 instance decl, because then we can't satisfy (C t). So we
442 just notice that g isn't quantified over 't' and partition
443 the contraints before simplifying.
445 This only half-works, but then let-generalisation only half-works.
448 Note [Inheriting implicit parameters]
449 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
454 where f is *not* a top-level binding.
455 From the RHS of f we'll get the constraint (?y::Int).
456 There are two types we might infer for f:
460 (so we get ?y from the context of f's definition), or
462 f :: (?y::Int) => Int -> Int
464 At first you might think the first was better, becuase then
465 ?y behaves like a free variable of the definition, rather than
466 having to be passed at each call site. But of course, the WHOLE
467 IDEA is that ?y should be passed at each call site (that's what
468 dynamic binding means) so we'd better infer the second.
470 BOTTOM LINE: when *inferring types* you *must* quantify
471 over implicit parameters. See the predicate isFreeWhenInferring.
474 *********************************************************************************
478 ***********************************************************************************
480 Note [Simplifying RULE lhs constraints]
481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
482 On the LHS of transformation rules we only simplify only equalities,
483 but not dictionaries. We want to keep dictionaries unsimplified, to
484 serve as the available stuff for the RHS of the rule. We *do* want to
485 simplify equalities, however, to detect ill-typed rules that cannot be
488 Implementation: the TcSFlags carried by the TcSMonad controls the
489 amount of simplification, so simplifyRuleLhs just sets the flag
492 Example. Consider the following left-hand side of a rule
493 f (x == y) (y > z) = ...
494 If we typecheck this expression we get constraints
495 d1 :: Ord a, d2 :: Eq a
496 We do NOT want to "simplify" to the LHS
497 forall x::a, y::a, z::a, d1::Ord a.
498 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
500 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
501 f ((==) d2 x y) ((>) d1 y z) = ...
503 Here is another example:
504 fromIntegral :: (Integral a, Num b) => a -> b
505 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
506 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
507 we *dont* want to get
509 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
510 because the scsel will mess up RULE matching. Instead we want
511 forall dIntegralInt, dNumInt.
512 fromIntegral Int Int dIntegralInt dNumInt = id Int
515 g (x == y) (y == z) = ..
516 where the two dictionaries are *identical*, we do NOT WANT
517 forall x::a, y::a, z::a, d1::Eq a
518 f ((==) d1 x y) ((>) d1 y z) = ...
519 because that will only match if the dict args are (visibly) equal.
520 Instead we want to quantify over the dictionaries separately.
522 In short, simplifyRuleLhs must *only* squash equalities, leaving
523 all dicts unchanged, with absolutely no sharing.
525 HOWEVER, under a nested implication things are different
527 f :: (forall a. Eq a => a->a) -> Bool -> ...
528 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
531 Here we *must* solve the wanted (Eq a) from the given (Eq a)
532 resulting from skolemising the agument type of g. So we
533 revert to SimplCheck when going under an implication.
536 simplifyRule :: RuleName
537 -> [TcTyVar] -- Explicit skolems
538 -> WantedConstraints -- Constraints from LHS
539 -> WantedConstraints -- Constraints from RHS
540 -> TcM ([EvVar], -- LHS dicts
541 TcEvBinds, -- Evidence for LHS
542 TcEvBinds) -- Evidence for RHS
543 -- See Note [Simplifying RULE lhs constraints]
544 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
545 = do { loc <- getCtLoc (RuleSkol name)
546 ; zonked_lhs <- zonkWC lhs_wanted
547 ; let untch = NoUntouchables
548 -- We allow ourselves to unify environment
549 -- variables; hence *no untouchables*
551 ; (lhs_results, lhs_binds)
552 <- runTcS SimplRuleLhs untch $
553 solveWanteds emptyInert zonked_lhs
555 ; traceTc "simplifyRule" $
556 vcat [ text "zonked_lhs" <+> ppr zonked_lhs
557 , text "lhs_results" <+> ppr lhs_results
558 , text "lhs_binds" <+> ppr lhs_binds
559 , text "rhs_wanted" <+> ppr rhs_wanted ]
562 -- Don't quantify over equalities (judgement call here)
563 ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
564 (wc_flat lhs_results)
565 lhs_dicts = map evVarOf (bagToList dicts)
566 -- Dicts and implicit parameters
568 -- Fail if we have not got down to unsolved flats
569 ; ev_binds_var <- newTcEvBinds
570 ; emitImplication $ Implic { ic_untch = untch
571 , ic_env = emptyNameEnv
572 , ic_skols = mkVarSet tv_bndrs
573 , ic_given = lhs_dicts
574 , ic_wanted = lhs_results { wc_flat = eqs }
575 , ic_insol = insolubleWC lhs_results
576 , ic_binds = ev_binds_var
579 -- Notice that we simplify the RHS with only the explicitly
580 -- introduced skolems, allowing the RHS to constrain any
581 -- unification variables.
582 -- Then, and only then, we call zonkQuantifiedTypeVariables
583 -- Example foo :: Ord a => a -> a
584 -- foo_spec :: Int -> Int
585 -- {-# RULE "foo" foo = foo_spec #-}
586 -- Here, it's the RHS that fixes the type variable
588 -- So we don't want to make untouchable the type
589 -- variables in the envt of the RHS, because they include
590 -- the template variables of the RULE
592 -- Hence the rather painful ad-hoc treatement here
593 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
594 ; rhs_binds1 <- simplifyCheck SimplCheck $
595 WC { wc_flat = emptyBag
596 , wc_insol = emptyBag
597 , wc_impl = unitBag $
598 Implic { ic_untch = NoUntouchables
599 , ic_env = emptyNameEnv
600 , ic_skols = mkVarSet tv_bndrs
601 , ic_given = lhs_dicts
602 , ic_wanted = rhs_wanted
603 , ic_insol = insolubleWC rhs_wanted
604 , ic_binds = rhs_binds_var
606 ; rhs_binds2 <- readTcRef evb_ref
610 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
614 *********************************************************************************
618 ***********************************************************************************
621 simplifyCheck :: SimplContext
622 -> WantedConstraints -- Wanted
624 -- Solve a single, top-level implication constraint
625 -- e.g. typically one created from a top-level type signature
626 -- f :: forall a. [a] -> [a]
628 -- We do this even if the function has no polymorphism:
632 -- (whereas for *nested* bindings we would not create
633 -- an implication constraint for g at all.)
635 -- Fails if can't solve something in the input wanteds
636 simplifyCheck ctxt wanteds
637 = do { wanteds <- zonkWC wanteds
639 ; traceTc "simplifyCheck {" (vcat
640 [ ptext (sLit "wanted =") <+> ppr wanteds ])
642 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
643 solveWanteds emptyInert wanteds
645 ; traceTc "simplifyCheck }" $
646 ptext (sLit "unsolved =") <+> ppr unsolved
648 ; reportUnsolved unsolved
653 solveWanteds :: InertSet -- Given
655 -> TcS WantedConstraints
656 solveWanteds inert wanted
657 = do { (unsolved_flats, unsolved_implics, insols)
658 <- solve_wanteds inert wanted
659 ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived
660 , wc_impl = unsolved_implics
661 , wc_insol = insols }) }
663 solve_wanteds :: InertSet -- Given
665 -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
666 -- solve_wanteds iterates when it is able to float equalities
667 -- out of one or more of the implications
668 solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
669 = do { traceTcS "solveWanteds {" (ppr wanted)
672 -- Discard from insols all the derived/given constraints
673 -- because they will show up again when we try to solve
674 -- everything else. Solving them a second time is a bit
675 -- of a waste, but the code is simple, and the program is
677 ; let all_flats = flats `unionBags` keepWanted insols
678 ; inert1 <- solveInteractWanted inert (bagToList all_flats)
680 ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
682 ; bb <- getTcEvBindsBag
683 ; tb <- getTcSTyBindsMap
684 ; traceTcS "solveWanteds }" $
685 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
686 , text "unsolved_implics =" <+> ppr unsolved_implics
687 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
688 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
691 ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
692 -- See Note [Solving Family Equations]
693 -- NB: remaining_flats has already had subst applied
695 ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
697 ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
698 , mapBag (substImplication subst) unsolved_implics
699 , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
705 -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
706 simpl_loop n inert implics
708 = trace "solveWanteds: loop" $ -- Always bleat
709 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
710 ; let (_, unsolved_cans) = extractUnsolved inert
711 ; return (unsolved_cans, implics) }
714 = do { traceTcS "solveWanteds: simpl_loop start {" $
715 vcat [ text "n =" <+> ppr n
716 , text "implics =" <+> ppr implics
717 , text "inert =" <+> ppr inert ]
719 ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
720 -- unsolved_cans contains either Wanted or Derived!
722 ; (implic_eqs, unsolved_implics)
723 <- solveNestedImplications just_given_inert unsolved_cans implics
725 -- Apply defaulting rules if and only if there
726 -- no floated equalities. If there are, they may
727 -- solve the remaining wanteds, so don't do defaulting.
728 ; improve_eqs <- if not (isEmptyBag implic_eqs)
729 then return implic_eqs
730 else applyDefaultingRules just_given_inert unsolved_cans
732 ; traceTcS "solveWanteds: simpl_loop end }" $
733 vcat [ text "improve_eqs =" <+> ppr improve_eqs
734 , text "unsolved_flats =" <+> ppr unsolved_cans
735 , text "unsolved_implics =" <+> ppr unsolved_implics ]
737 ; (improve_eqs_already_in_inert, inert_with_improvement)
738 <- solveInteract inert improve_eqs
740 ; if improve_eqs_already_in_inert then
741 return (unsolved_cans, unsolved_implics)
743 simpl_loop (n+1) inert_with_improvement
744 -- Contain unsolved_cans and the improve_eqs
748 givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
749 -- Extract the *wanted* ones from CanonicalCts
750 -- and make them into *givens*
751 givensFromWanteds = foldrBag getWanted emptyBag
753 getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
755 | not (isCFrozenErr cc)
756 , Wanted loc <- cc_flavor cc
757 , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
758 = given `consBag` givens
760 = givens -- We are not helping anyone by pushing a Derived in!
761 -- Because if we could not solve it to start with
762 -- we are not going to do either inside the impl constraint
764 solveNestedImplications :: InertSet -> CanonicalCts
766 -> TcS (Bag FlavoredEvVar, Bag Implication)
767 solveNestedImplications just_given_inert unsolved_cans implics
769 = return (emptyBag, emptyBag)
771 = do { -- See Note [Preparing inert set for implications]
772 -- Push the unsolved wanteds inwards, but as givens
773 let pushed_givens = givensFromWanteds unsolved_cans
774 tcs_untouchables = filterVarSet isFlexiTcsTv $
775 tyVarsOfEvVarXs pushed_givens
776 -- See Note [Extra TcsTv untouchables]
778 ; traceTcS "solveWanteds: preparing inerts for implications {"
779 (vcat [ppr tcs_untouchables, ppr pushed_givens])
781 ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
783 ; traceTcS "solveWanteds: } now doing nested implications {" $
784 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
785 , text "implics =" <+> ppr implics ]
787 ; (implic_eqs, unsolved_implics)
788 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
790 ; traceTcS "solveWanteds: done nested implications }" $
791 vcat [ text "implic_eqs =" <+> ppr implic_eqs
792 , text "unsolved_implics =" <+> ppr unsolved_implics ]
794 ; return (implic_eqs, unsolved_implics) }
796 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
798 -> Implication -- Wanted
799 -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
800 Bag Implication) -- Unsolved rest (always empty or singleton)
802 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
803 -- that are of the form unification var = type
805 -- 2. Maybe a unsolved implication, empty if entirely solved!
807 -- Precondition: everything is zonked by now
808 solveImplication tcs_untouchables inert
809 imp@(Implic { ic_untch = untch
810 , ic_binds = ev_binds
813 , ic_wanted = wanteds
815 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
816 recoverTcS (return (emptyBag, emptyBag)) $
817 -- Recover from nested failures. Even the top level is
818 -- just a bunch of implications, so failing at the first
820 do { traceTcS "solveImplication {" (ppr imp)
823 ; given_inert <- solveInteractGiven inert loc givens
825 -- Simplify the wanteds
826 ; (unsolved_flats, unsolved_implics, insols)
827 <- solve_wanteds given_inert wanteds
829 ; let (res_flat_free, res_flat_bound)
830 = floatEqualities skols givens unsolved_flats
831 final_flat = keepWanted res_flat_bound
833 ; let res_wanted = WC { wc_flat = final_flat
834 , wc_impl = unsolved_implics
835 , wc_insol = insols }
836 res_implic = unitImplication $
837 imp { ic_wanted = res_wanted
838 , ic_insol = insolubleWC res_wanted }
840 ; traceTcS "solveImplication end }" $ vcat
841 [ text "res_flat_free =" <+> ppr res_flat_free
842 , text "res_implic =" <+> ppr res_implic ]
844 ; return (res_flat_free, res_implic) }
847 floatEqualities :: TcTyVarSet -> [EvVar]
848 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
849 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
850 -- and come from the input wanted ev vars or deriveds
851 floatEqualities skols can_given wantders
852 | hasEqualities can_given = (emptyBag, wantders)
853 -- Note [Float Equalities out of Implications]
854 | otherwise = partitionBag is_floatable wantders
857 where is_floatable :: FlavoredEvVar -> Bool
858 is_floatable (EvVarX cv _fl)
859 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
860 is_floatable _flev = False
862 tvs_under_fsks :: Type -> TyVarSet
863 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
864 tvs_under_fsks (TyVarTy tv)
865 | not (isTcTyVar tv) = unitVarSet tv
866 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
867 | otherwise = unitVarSet tv
868 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
869 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
870 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
871 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
872 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
873 -- can mention type variables!
874 | isTyVar tv = inner_tvs `delVarSet` tv
875 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
876 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
878 inner_tvs = tvs_under_fsks ty
880 predTvs_under_fsks :: PredType -> TyVarSet
881 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
882 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
883 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
886 Note [Preparing inert set for implications]
887 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
888 Before solving the nested implications, we convert any unsolved flat wanteds
889 to givens, and add them to the inert set. Reasons:
891 a) In checking mode, suppresses unnecessary errors. We already have
892 on unsolved-wanted error; adding it to the givens prevents any
893 consequential errors from showing up
895 b) More importantly, in inference mode, we are going to quantify over this
896 constraint, and we *don't* want to quantify over any constraints that
897 are deducible from it.
899 c) Flattened type-family equalities must be exposed to the nested
900 constraints. Consider
901 F b ~ alpha, (forall c. F b ~ alpha)
902 Obviously this is soluble with [alpha := F b]. But the
903 unification is only done by solveCTyFunEqs, right at the end of
904 solveWanteds, and if we aren't careful we'll end up with an
905 unsolved goal inside the implication. We need to "push" the
906 as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
907 can be used to solve the inner (F b
908 ~ alpha). See Trac #4935.
910 d) There are other cases where interactions between wanteds that can help
911 to solve a constraint. For example
915 (C Int alpha), (forall d. C d blah => C Int a)
917 If we push the (C Int alpha) inwards, as a given, it can produce
918 a fundep (alpha~a) and this can float out again and be used to
919 fix alpha. (In general we can't float class constraints out just
920 in case (C d blah) might help to solve (C Int a).)
922 The unsolved wanteds are *canonical* but they may not be *inert*,
923 because when made into a given they might interact with other givens.
924 Hence the call to solveInteract. Example:
926 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
928 We were not able to solve (a ~w [beta]) but we can't just assume it as
929 given because the resulting set is not inert. Hence we have to do a
930 'solveInteract' step first.
932 Note [Extra TcsTv untouchables]
933 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
934 Furthemore, we record the inert set simplifier-generated unification
935 variables of the TcsTv kind (such as variables from instance that have
936 been applied, or unification flattens). These variables must be passed
937 to the implications as extra untouchable variables. Otherwise we have
938 the danger of double unifications. Example (from trac ticket #4494):
940 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
942 In this example, beta is touchable inside the implication. The first
943 solveInteract step leaves 'uf' ununified. Then we move inside the
944 implication where a new constraint
946 emerges. We may spontaneously solve it to get uf := beta, so the whole
947 implication disappears but when we pop out again we are left with (F
948 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
949 uf will get unified *once more* to (F Int).
951 The solution is to record the TcsTvs (i.e. the simplifier-generated
952 unification variables) that are generated when solving the flats, and
953 make them untouchables for the nested implication. In the example
954 above uf would become untouchable, so beta would be forced to be
955 unified as beta := uf.
957 NB: A consequence is that every simplifier-generated TcsTv variable
958 that gets floated out of an implication becomes now untouchable
959 next time we go inside that implication to solve any residual
960 constraints. In effect, by floating an equality out of the
961 implication we are committing to have it solved in the outside.
963 Note [Float Equalities out of Implications]
964 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
965 We want to float equalities out of vanilla existentials, but *not* out
966 of GADT pattern matches.
971 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
972 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
973 -- See Note [Solving Family Equations]
974 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
975 -- where the newly generated equalities (alpha := F xi) have been substituted through.
977 = do { untch <- getUntouchables
978 ; let (unsolved_can_cts, (ni_subst, cv_binds))
979 = getSolvableCTyFunEqs untch cts
980 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
981 , ppr ni_subst, ppr cv_binds
983 ; mapM_ solve_one cv_binds
985 ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
987 solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
988 ; setCoBind cv (mkReflCo ty) }
991 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
992 -- The TvSubstEnv is not idempotent, but is loop-free
993 -- See Note [Non-idempotent substitution] in Unify
994 emptyFunEqBinds :: FunEqBinds
995 emptyFunEqBinds = (emptyVarEnv, [])
997 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
998 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
999 = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
1002 getSolvableCTyFunEqs :: TcsUntouchables
1003 -> CanonicalCts -- Precondition: all Wanteds or Derived!
1004 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
1005 getSolvableCTyFunEqs untch cts
1006 = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
1008 dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
1009 -> (CanonicalCts, FunEqBinds)
1010 dflt_funeq (cts_in, feb@(tv_subst, _))
1011 (CFunEqCan { cc_id = cv
1016 | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
1018 , isTouchableMetaTyVar_InRange untch tv
1019 -- And it's a *touchable* unification variable
1021 , typeKind xi `isSubKind` tyVarKind tv
1022 -- Must do a small kind check since TcCanonical invariants
1023 -- on family equations only impose compatibility, not subkinding
1025 , not (tv `elemVarEnv` tv_subst)
1026 -- Check not in extra_binds
1027 -- See Note [Solving Family Equations], Point 1
1029 , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1030 -- Occurs check: see Note [Solving Family Equations], Point 2
1031 = ASSERT ( not (isGiven fl) )
1032 (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
1034 dflt_funeq (cts_in, fun_eq_binds) ct
1035 = (cts_in `extendCCans` ct, fun_eq_binds)
1038 Note [Solving Family Equations]
1039 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1040 After we are done with simplification we may be left with constraints of the form:
1041 [Wanted] F xis ~ beta
1042 If 'beta' is a touchable unification variable not already bound in the TyBinds
1043 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1045 When is it ok to do so?
1046 1) 'beta' must not already be defaulted to something. Example:
1048 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1049 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1050 have to report this as unsolved.
1052 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1053 set [beta := F xis] only if beta is not among the free variables of xis.
1055 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1056 of type family equations. See Inert Set invariants in TcInteract.
1059 *********************************************************************************
1061 * Defaulting and disamgiguation *
1063 *********************************************************************************
1065 Basic plan behind applyDefaulting rules:
1068 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
1069 For each defaultable group, do:
1070 For each possible substitution for [alpha |-> tau] where `alpha' is the
1071 group's variable, do:
1072 1) Make up new TcEvBinds
1073 2) Extend TcS with (groupVariable
1074 3) given_inert <- solveOne inert (given : a ~ tau)
1075 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1076 5) if unsolved == empty then
1077 sneakyUnify a |-> tau
1078 write the evidence bins
1079 return (final_inert ++ group_constraints,[])
1080 -- will contain the info (alpha |-> tau)!!
1081 goto next defaultable group
1082 if unsolved <> empty then
1083 throw away evidence binds
1084 try next substitution
1085 If you've run out of substitutions for this group, too bad, you failed
1086 return (inert,group)
1087 goto next defaultable group
1090 Collect all the (canonical-cts, wanteds) gathered this way.
1091 - Do a solveGiven over the canonical-cts to make sure they are inert
1092 ------------------------------------------------------------------------------------------
1096 applyDefaultingRules :: InertSet
1097 -> CanonicalCts -- All wanteds
1098 -> TcS (Bag FlavoredEvVar) -- All wanteds again!
1099 -- Return some *extra* givens, which express the
1100 -- type-class-default choice
1102 applyDefaultingRules inert wanteds
1103 | isEmptyBag wanteds
1106 = do { untch <- getUntouchables
1107 ; tv_cts <- mapM (defaultTyVar untch) $
1108 varSetElems (tyVarsOfCDicts wanteds)
1110 ; info@(_, default_tys, _) <- getDefaultInfo
1111 ; let groups = findDefaultableGroups info untch wanteds
1112 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1114 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1115 , text "Type defaults =" <+> ppr deflt_cts])
1117 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1120 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1121 -- defaultTyVar is used on any un-instantiated meta type variables to
1122 -- default the kind of ? and ?? etc to *. This is important to ensure
1123 -- that instance declarations match. For example consider
1124 -- instance Show (a->b)
1125 -- foo x = show (\_ -> True)
1126 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1127 -- and that won't match the typeKind (*) in the instance decl.
1130 -- We look only at touchable type variables. No further constraints
1131 -- are going to affect these type variables, so it's time to do it by
1132 -- hand. However we aren't ready to default them fully to () or
1133 -- whatever, because the type-class defaulting rules have yet to run.
1135 defaultTyVar untch the_tv
1136 | isTouchableMetaTyVar_InRange untch the_tv
1137 , not (k `eqKind` default_k)
1138 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1139 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1140 ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1142 = return emptyBag -- The common case
1144 k = tyVarKind the_tv
1145 default_k = defaultKind k
1149 findDefaultableGroups
1152 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1153 -> TcsUntouchables -- Untouchable
1154 -> CanonicalCts -- Unsolved
1155 -> [[(CanonicalCt,TcTyVar)]]
1156 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1158 | not (performDefaulting ctxt) = []
1159 | null default_tys = []
1160 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1162 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1163 non_unaries :: [CanonicalCt] -- and *other* constraints
1165 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1166 -- Finds unary type-class constraints
1167 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1168 | Just tv <- tcGetTyVar_maybe ty
1170 find_unary cc = Right cc -- Non unary or non dictionary
1172 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1173 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1175 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1177 is_defaultable_group ds@((_,tv):_)
1178 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1179 && not (tv `elemVarSet` bad_tvs)
1180 && isTouchableMetaTyVar_InRange untch tv
1181 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1182 is_defaultable_group [] = panic "defaultable_group"
1184 defaultable_classes clss
1185 | extended_defaults = any isInteractiveClass clss
1186 | otherwise = all is_std_class clss && (any is_num_class clss)
1188 -- In interactive mode, or with -XExtendedDefaultRules,
1189 -- we default Show a to Show () to avoid graututious errors on "show []"
1190 isInteractiveClass cls
1191 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1193 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1194 -- is_num_class adds IsString to the standard numeric classes,
1195 -- when -foverloaded-strings is enabled
1197 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1198 -- Similarly is_std_class
1200 ------------------------------
1201 disambigGroup :: [Type] -- The default types
1202 -> InertSet -- Given inert
1203 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1204 -- sharing same type variable
1205 -> TcS (Bag FlavoredEvVar)
1207 disambigGroup [] _inert _grp
1209 disambigGroup (default_ty:default_tys) inert group
1210 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1211 ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1212 ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1213 derived_eq = mkEvVarX ev der_flav
1215 ; success <- tryTcS $
1216 do { (_,final_inert) <- solveInteract inert $ listToBag $
1217 derived_eq : wanted_ev_vars
1218 ; let (_, unsolved) = extractUnsolved final_inert
1219 ; let wanted_unsolved = filterBag isWantedCt unsolved
1220 -- Don't care about Derived's
1221 ; return (isEmptyBag wanted_unsolved) }
1223 True -> -- Success: record the type variable binding, and return
1224 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1225 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1226 ; return (unitBag derived_eq) }
1227 False -> -- Failure: try with the next type
1228 do { traceTcS "disambigGroup failed, will try other default types"
1230 ; disambigGroup default_tys inert group } }
1232 ((the_ct,the_tv):_) = group
1233 wanteds = map fst group
1234 wanted_ev_vars :: [FlavoredEvVar]
1235 wanted_ev_vars = map deCanonicalise wanteds
1237 mk_derived_flavor :: CtFlavor -> CtFlavor
1238 mk_derived_flavor (Wanted loc) = Derived loc
1239 mk_derived_flavor _ = panic "Asked to disambiguate given or derived!"
1242 Note [Avoiding spurious errors]
1243 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1244 When doing the unification for defaulting, we check for skolem
1245 type variables, and simply don't default them. For example:
1246 f = (*) -- Monomorphic
1247 g :: Num a => a -> a
1249 Here, we get a complaint when checking the type signature for g,
1250 that g isn't polymorphic enough; but then we get another one when
1251 dealing with the (Num a) context arising from f's definition;
1252 we try to unify a with Int (to default it), but find that it's
1253 already been unified with the rigid variable from g's type sig
1257 *********************************************************************************
1261 *********************************************************************************
1264 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1265 newFlatWanteds orig theta
1266 = do { loc <- getCtLoc orig
1267 ; evs <- newWantedEvVars theta
1268 ; return (listToBag [EvVarX w loc | w <- evs]) }