4 simplifyDefault, simplifyDeriv,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
18 import Unify( niFixTvSubst, niSubstTvSet )
25 import NameEnv ( emptyNameEnv )
31 import Class ( classKey )
32 import BasicTypes ( RuleName, TopLevelFlag, isTopLevel )
33 import Control.Monad ( when )
39 *********************************************************************************
41 * External interface *
43 *********************************************************************************
46 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
47 -- Simplify top-level constraints
48 -- Usually these will be implications,
49 -- but when there is nothing to quantify we don't wrap
50 -- in a degenerate implication, 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 { wanted <- newFlatWanteds DefaultOrigin theta
64 ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted)
70 *********************************************************************************
74 ***********************************************************************************
77 simplifyDeriv :: CtOrigin
79 -> ThetaType -- Wanted
80 -> TcM ThetaType -- Needed
81 -- Given instance (wanted) => C inst_ty
82 -- Simplify 'wanted' as much as possibles
83 -- Fail if not possible
84 simplifyDeriv orig tvs theta
85 = do { tvs_skols <- tcInstSuperSkolTyVars tvs -- Skolemize
86 -- One reason is that the constraint solving machinery
87 -- expects *TcTyVars* not TyVars. Another is that
88 -- when looking up instances we don't want overlap
91 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
92 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
94 ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
96 ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
97 ; (residual_wanted, _binds)
98 <- runTcS SimplInfer NoUntouchables $
99 solveWanteds emptyInert (mkFlatWC wanted)
101 ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
102 -- See Note [Exotic derived instance contexts]
103 get_good :: WantedEvVar -> Either PredType WantedEvVar
104 get_good wev | validDerivPred p = Left p
105 | otherwise = Right wev
106 where p = evVarOfPred wev
108 ; reportUnsolved (residual_wanted { wc_flat = bad })
110 ; let min_theta = mkMinimalBySCs (bagToList good)
111 ; return (substTheta subst_skol min_theta) }
114 Note [Exotic derived instance contexts]
115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
116 In a 'derived' instance declaration, we *infer* the context. It's a
117 bit unclear what rules we should apply for this; the Haskell report is
118 silent. Obviously, constraints like (Eq a) are fine, but what about
119 data T f a = MkT (f a) deriving( Eq )
120 where we'd get an Eq (f a) constraint. That's probably fine too.
122 One could go further: consider
123 data T a b c = MkT (Foo a b c) deriving( Eq )
124 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
126 Notice that this instance (just) satisfies the Paterson termination
127 conditions. Then we *could* derive an instance decl like this:
129 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
130 even though there is no instance for (C Int a), because there just
131 *might* be an instance for, say, (C Int Bool) at a site where we
132 need the equality instance for T's.
134 However, this seems pretty exotic, and it's quite tricky to allow
135 this, and yet give sensible error messages in the (much more common)
136 case where we really want that instance decl for C.
138 So for now we simply require that the derived instance context
139 should have only type-variable constraints.
141 Here is another example:
142 data Fix f = In (f (Fix f)) deriving( Eq )
143 Here, if we are prepared to allow -XUndecidableInstances we
144 could derive the instance
145 instance Eq (f (Fix f)) => Eq (Fix f)
146 but this is so delicate that I don't think it should happen inside
147 'deriving'. If you want this, write it yourself!
149 NB: if you want to lift this condition, make sure you still meet the
150 termination conditions! If not, the deriving mechanism generates
151 larger and larger constraints. Example:
153 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
155 Note the lack of a Show instance for Succ. First we'll generate
156 instance (Show (Succ a), Show a) => Show (Seq a)
158 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
159 and so on. Instead we want to complain of no instance for (Show (Succ a)).
163 Allow constraints which consist only of type variables, with no repeats.
165 *********************************************************************************
169 ***********************************************************************************
172 simplifyInfer :: TopLevelFlag
173 -> Bool -- Apply monomorphism restriction
174 -> [(Name, TcTauType)] -- Variables to be generalised,
175 -- and their tau-types
177 -> TcM ([TcTyVar], -- Quantify over these type variables
178 [EvVar], -- ... and these constraints
179 TcEvBinds) -- ... binding these evidence variables
180 simplifyInfer top_lvl apply_mr name_taus wanteds
182 = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
183 ; zonked_taus <- zonkTcTypes (map snd name_taus)
184 ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
185 ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
186 ; return (qtvs, [], emptyTcEvBinds) }
189 = do { zonked_wanteds <- zonkWC wanteds
190 ; zonked_taus <- zonkTcTypes (map snd name_taus)
191 ; gbl_tvs <- tcGetGlobalTyVars
193 ; traceTc "simplifyInfer {" $ vcat
194 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
195 , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
196 , ptext (sLit "wanted =") <+> ppr zonked_wanteds
200 -- Make a guess at the quantified type variables
201 -- Then split the constraints on the baisis of those tyvars
202 -- to avoid unnecessarily simplifying a class constraint
203 -- See Note [Avoid unecessary constraint simplification]
204 ; let zonked_tau_tvs = get_tau_tvs zonked_taus
205 proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
206 zonked_tau_tvs `minusVarSet` gbl_tvs
207 (perhaps_bound, surely_free)
208 = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
210 ; traceTc "simplifyInfer proto" $ vcat
211 [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
212 , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
213 , ptext (sLit "surely_fref =") <+> ppr surely_free
216 ; emitFlats surely_free
217 ; traceTc "sinf" $ vcat
218 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
219 , ptext (sLit "surely_free =") <+> ppr surely_free
223 -- Now simplify the possibly-bound constraints
224 ; (simpl_results, tc_binds0)
225 <- runTcS SimplInfer NoUntouchables $
226 simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
228 ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
229 (do { reportUnsolved simpl_results; failM })
232 -- Split again simplified_perhaps_bound, because some unifications
233 -- may have happened, and emit the free constraints.
234 ; gbl_tvs <- tcGetGlobalTyVars
235 ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
236 ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
237 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
238 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
239 constrained_tvs = tyVarsOfEvVarXs zonked_simples
240 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
241 (final_qtvs, (bound, free))
242 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
243 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
246 ; if isEmptyVarSet final_qtvs && isEmptyBag bound
247 then ASSERT( isEmptyBag (wc_insol simpl_results) )
248 do { traceTc "} simplifyInfer/no quantification" empty
249 ; emitImplications (wc_impl simpl_results)
250 ; return ([], [], EvBinds tc_binds0) }
253 -- Step 4, zonk quantified variables
254 { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
255 ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
256 | (name, ty) <- name_taus ]
257 -- Don't add the quantified variables here, because
258 -- they are also bound in ic_skols and we want them to be
260 skol_info = InferSkol poly_ids
262 ; gloc <- getCtLoc skol_info
263 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
266 -- Minimize `bound' and emit an implication
267 ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
268 ; ev_binds_var <- newTcEvBinds
269 ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
270 ; lcl_env <- getLclTypeEnv
271 ; let implic = Implic { ic_untch = NoUntouchables
273 , ic_skols = mkVarSet qtvs_to_return
274 , ic_given = minimal_bound_ev_vars
275 , ic_wanted = simpl_results { wc_flat = bound }
277 , ic_binds = ev_binds_var
279 ; emitImplication implic
280 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
281 vcat [ ptext (sLit "implic =") <+> ppr implic
282 -- ic_skols, ic_given give rest of result
283 , ptext (sLit "qtvs =") <+> ppr final_qtvs
284 , ptext (sLit "spb =") <+> ppr zonked_simples
285 , ptext (sLit "bound =") <+> ppr bound ]
289 ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
291 get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
292 | otherwise = exactTyVarsOfTypes
293 -- See Note [Silly type synonym] in TcType
297 Note [Minimize by Superclasses]
298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
300 When we quantify over a constraint, in simplifyInfer we need to
301 quantify over a constraint that is minimal in some sense: For
302 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
303 we'd like to quantify over Ord alpha, because we can just get Eq alpha
304 from superclass selection from Ord alpha. This minimization is what
305 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
306 to check the original wanted.
309 simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
310 simplifyWithApprox wanted
311 = do { traceTcS "simplifyApproxLoop" (ppr wanted)
313 ; results <- solveWanteds emptyInert wanted
315 ; let (residual_implics, floats) = approximateImplications (wc_impl results)
317 -- If no new work was produced then we are done with simplifyApproxLoop
318 ; if insolubleWC results || isEmptyBag floats
321 else solveWanteds emptyInert
322 (WC { wc_flat = floats `unionBags` wc_flat results
323 , wc_impl = residual_implics
324 , wc_insol = emptyBag }) }
326 approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
327 -- Extracts any nested constraints that don't mention the skolems
328 approximateImplications impls
329 = do_bag (float_implic emptyVarSet) impls
331 do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
332 do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
333 plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
334 plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
336 float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
337 float_implic skols imp
338 = (unitBag (imp { ic_wanted = wanted' }), floats)
340 (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
342 float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
343 = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
345 (flat', floats1) = do_bag (float_flat skols) flat
346 (implic', floats2) = do_bag (float_implic skols) implic
348 float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
350 | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
351 | otherwise = (unitBag wev, emptyBag)
355 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
356 -- X-constraint 'wanted', nuking the 'gbls' at each stage
357 -- It's conservative in that if the seed could *possibly*
358 -- grow to include a type variable, then it does
360 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
361 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
363 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
364 growWantedEVs gbl_tvs ws tvs
365 | isEmptyBag ws = tvs
366 | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
368 -------- Helper functions, do not do fixpoint ------------------------
369 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
370 growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) .
371 growPreds gbl_tvs evVarOfPred (wc_flat wc) .
372 growPreds gbl_tvs evVarOfPred (wc_insol wc)
374 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
375 growImplics gbl_tvs implics tvs
376 = foldrBag grow_implic tvs implics
378 grow_implic implic tvs
379 = grow tvs `minusVarSet` ic_skols implic
381 grow = growWC gbl_tvs (ic_wanted implic) .
382 growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
383 -- We must grow from givens too; see test IPRun
385 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
386 growPreds gbl_tvs get_pred items tvs
387 = foldrBag extend tvs items
389 extend item tvs = tvs `unionVarSet`
390 (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
393 quantifyMe :: TyVarSet -- Quantifying over these
395 -> Bool -- True <=> quantify over this wanted
397 | isIPPred pred = True -- Note [Inheriting implicit parameters]
398 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
400 pred = evVarOfPred wev
403 Note [Avoid unecessary constraint simplification]
404 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
405 When inferring the type of a let-binding, with simplifyInfer,
406 try to avoid unnecessariliy simplifying class constraints.
407 Doing so aids sharing, but it also helps with delicate
409 instance C t => C [t] where ..
411 f x = let g y = ...(constraint C [t])...
413 When inferring a type for 'g', we don't want to apply the
414 instance decl, because then we can't satisfy (C t). So we
415 just notice that g isn't quantified over 't' and partition
416 the contraints before simplifying.
418 This only half-works, but then let-generalisation only half-works.
421 Note [Inheriting implicit parameters]
422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
427 where f is *not* a top-level binding.
428 From the RHS of f we'll get the constraint (?y::Int).
429 There are two types we might infer for f:
433 (so we get ?y from the context of f's definition), or
435 f :: (?y::Int) => Int -> Int
437 At first you might think the first was better, becuase then
438 ?y behaves like a free variable of the definition, rather than
439 having to be passed at each call site. But of course, the WHOLE
440 IDEA is that ?y should be passed at each call site (that's what
441 dynamic binding means) so we'd better infer the second.
443 BOTTOM LINE: when *inferring types* you *must* quantify
444 over implicit parameters. See the predicate isFreeWhenInferring.
447 *********************************************************************************
451 ***********************************************************************************
453 Note [Simplifying RULE lhs constraints]
454 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
455 On the LHS of transformation rules we only simplify only equalities,
456 but not dictionaries. We want to keep dictionaries unsimplified, to
457 serve as the available stuff for the RHS of the rule. We *do* want to
458 simplify equalities, however, to detect ill-typed rules that cannot be
461 Implementation: the TcSFlags carried by the TcSMonad controls the
462 amount of simplification, so simplifyRuleLhs just sets the flag
465 Example. Consider the following left-hand side of a rule
466 f (x == y) (y > z) = ...
467 If we typecheck this expression we get constraints
468 d1 :: Ord a, d2 :: Eq a
469 We do NOT want to "simplify" to the LHS
470 forall x::a, y::a, z::a, d1::Ord a.
471 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
473 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
474 f ((==) d2 x y) ((>) d1 y z) = ...
476 Here is another example:
477 fromIntegral :: (Integral a, Num b) => a -> b
478 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
479 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
480 we *dont* want to get
482 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
483 because the scsel will mess up RULE matching. Instead we want
484 forall dIntegralInt, dNumInt.
485 fromIntegral Int Int dIntegralInt dNumInt = id Int
488 g (x == y) (y == z) = ..
489 where the two dictionaries are *identical*, we do NOT WANT
490 forall x::a, y::a, z::a, d1::Eq a
491 f ((==) d1 x y) ((>) d1 y z) = ...
492 because that will only match if the dict args are (visibly) equal.
493 Instead we want to quantify over the dictionaries separately.
495 In short, simplifyRuleLhs must *only* squash equalities, leaving
496 all dicts unchanged, with absolutely no sharing.
498 HOWEVER, under a nested implication things are different
500 f :: (forall a. Eq a => a->a) -> Bool -> ...
501 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
504 Here we *must* solve the wanted (Eq a) from the given (Eq a)
505 resulting from skolemising the agument type of g. So we
506 revert to SimplCheck when going under an implication.
509 simplifyRule :: RuleName
510 -> [TcTyVar] -- Explicit skolems
511 -> WantedConstraints -- Constraints from LHS
512 -> WantedConstraints -- Constraints from RHS
513 -> TcM ([EvVar], -- LHS dicts
514 TcEvBinds, -- Evidence for LHS
515 TcEvBinds) -- Evidence for RHS
516 -- See Note [Simplifying RULE lhs constraints]
517 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
518 = do { loc <- getCtLoc (RuleSkol name)
519 ; zonked_lhs <- zonkWC lhs_wanted
520 ; let untch = NoUntouchables
521 -- We allow ourselves to unify environment
522 -- variables; hence *no untouchables*
524 ; (lhs_results, lhs_binds)
525 <- runTcS SimplRuleLhs untch $
526 solveWanteds emptyInert zonked_lhs
528 ; traceTc "simplifyRule" $
529 vcat [ text "zonked_lhs" <+> ppr zonked_lhs
530 , text "lhs_results" <+> ppr lhs_results
531 , text "lhs_binds" <+> ppr lhs_binds
532 , text "rhs_wanted" <+> ppr rhs_wanted ]
535 -- Don't quantify over equalities (judgement call here)
536 ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
537 (wc_flat lhs_results)
538 lhs_dicts = map evVarOf (bagToList dicts)
539 -- Dicts and implicit parameters
541 -- Fail if we have not got down to unsolved flats
542 ; ev_binds_var <- newTcEvBinds
543 ; emitImplication $ Implic { ic_untch = untch
544 , ic_env = emptyNameEnv
545 , ic_skols = mkVarSet tv_bndrs
546 , ic_given = lhs_dicts
547 , ic_wanted = lhs_results { wc_flat = eqs }
548 , ic_insol = insolubleWC lhs_results
549 , ic_binds = ev_binds_var
552 -- Notice that we simplify the RHS with only the explicitly
553 -- introduced skolems, allowing the RHS to constrain any
554 -- unification variables.
555 -- Then, and only then, we call zonkQuantifiedTypeVariables
556 -- Example foo :: Ord a => a -> a
557 -- foo_spec :: Int -> Int
558 -- {-# RULE "foo" foo = foo_spec #-}
559 -- Here, it's the RHS that fixes the type variable
561 -- So we don't want to make untouchable the type
562 -- variables in the envt of the RHS, because they include
563 -- the template variables of the RULE
565 -- Hence the rather painful ad-hoc treatement here
566 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
567 ; rhs_binds1 <- simplifyCheck SimplCheck $
568 WC { wc_flat = emptyBag
569 , wc_insol = emptyBag
570 , wc_impl = unitBag $
571 Implic { ic_untch = NoUntouchables
572 , ic_env = emptyNameEnv
573 , ic_skols = mkVarSet tv_bndrs
574 , ic_given = lhs_dicts
575 , ic_wanted = rhs_wanted
576 , ic_insol = insolubleWC rhs_wanted
577 , ic_binds = rhs_binds_var
579 ; rhs_binds2 <- readTcRef evb_ref
583 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
587 *********************************************************************************
591 ***********************************************************************************
594 simplifyCheck :: SimplContext
595 -> WantedConstraints -- Wanted
597 -- Solve a single, top-level implication constraint
598 -- e.g. typically one created from a top-level type signature
599 -- f :: forall a. [a] -> [a]
601 -- We do this even if the function has no polymorphism:
605 -- (whereas for *nested* bindings we would not create
606 -- an implication constraint for g at all.)
608 -- Fails if can't solve something in the input wanteds
609 simplifyCheck ctxt wanteds
610 = do { wanteds <- zonkWC wanteds
612 ; traceTc "simplifyCheck {" (vcat
613 [ ptext (sLit "wanted =") <+> ppr wanteds ])
615 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
616 solveWanteds emptyInert wanteds
618 ; traceTc "simplifyCheck }" $
619 ptext (sLit "unsolved =") <+> ppr unsolved
621 ; reportUnsolved unsolved
626 solveWanteds :: InertSet -- Given
628 -> TcS WantedConstraints
629 solveWanteds inert wanted
630 = do { (unsolved_flats, unsolved_implics, insols)
631 <- solve_wanteds inert wanted
632 ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived
633 , wc_impl = unsolved_implics
634 , wc_insol = insols }) }
636 solve_wanteds :: InertSet -- Given
638 -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
639 -- solve_wanteds iterates when it is able to float equalities
640 -- out of one or more of the implications
641 solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
642 = do { traceTcS "solveWanteds {" (ppr wanted)
645 -- Discard from insols all the derived/given constraints
646 -- because they will show up again when we try to solve
647 -- everything else. Solving them a second time is a bit
648 -- of a waste, but the code is simple, and the program is
650 ; let all_flats = flats `unionBags` keepWanted insols
651 ; inert1 <- solveInteractWanted inert (bagToList all_flats)
653 ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
655 ; bb <- getTcEvBindsBag
656 ; tb <- getTcSTyBindsMap
657 ; traceTcS "solveWanteds }" $
658 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
659 , text "unsolved_implics =" <+> ppr unsolved_implics
660 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
661 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
664 ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
665 -- See Note [Solving Family Equations]
666 -- NB: remaining_flats has already had subst applied
668 ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
670 ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
671 , mapBag (substImplication subst) unsolved_implics
672 , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
678 -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
679 simpl_loop n inert implics
681 = trace "solveWanteds: loop" $ -- Always bleat
682 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
683 ; let (_, unsolved_cans) = extractUnsolved inert
684 ; return (unsolved_cans, implics) }
687 = do { traceTcS "solveWanteds: simpl_loop start {" $
688 vcat [ text "n =" <+> ppr n
689 , text "implics =" <+> ppr implics
690 , text "inert =" <+> ppr inert ]
692 ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
693 -- unsolved_cans contains either Wanted or Derived!
695 ; (implic_eqs, unsolved_implics)
696 <- solveNestedImplications just_given_inert unsolved_cans implics
698 -- Apply defaulting rules if and only if there
699 -- no floated equalities. If there are, they may
700 -- solve the remaining wanteds, so don't do defaulting.
701 ; improve_eqs <- if not (isEmptyBag implic_eqs)
702 then return implic_eqs
703 else applyDefaultingRules just_given_inert unsolved_cans
705 ; traceTcS "solveWanteds: simpl_loop end }" $
706 vcat [ text "improve_eqs =" <+> ppr improve_eqs
707 , text "unsolved_flats =" <+> ppr unsolved_cans
708 , text "unsolved_implics =" <+> ppr unsolved_implics ]
710 ; (improve_eqs_already_in_inert, inert_with_improvement)
711 <- solveInteract inert improve_eqs
713 ; if improve_eqs_already_in_inert then
714 return (unsolved_cans, unsolved_implics)
716 simpl_loop (n+1) inert_with_improvement
717 -- Contain unsolved_cans and the improve_eqs
721 givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
722 -- Extract the *wanted* ones from CanonicalCts
723 -- and make them into *givens*
724 givensFromWanteds = foldrBag getWanted emptyBag
726 getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
728 | not (isCFrozenErr cc)
729 , Wanted loc <- cc_flavor cc
730 , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
731 = given `consBag` givens
733 = givens -- We are not helping anyone by pushing a Derived in!
734 -- Because if we could not solve it to start with
735 -- we are not going to do either inside the impl constraint
737 solveNestedImplications :: InertSet -> CanonicalCts
739 -> TcS (Bag FlavoredEvVar, Bag Implication)
740 solveNestedImplications just_given_inert unsolved_cans implics
742 = return (emptyBag, emptyBag)
744 = do { -- See Note [Preparing inert set for implications]
745 -- Push the unsolved wanteds inwards, but as givens
746 traceTcS "solveWanteds: preparing inerts for implications {" empty
748 ; let pushed_givens = givensFromWanteds unsolved_cans
749 tcs_untouchables = filterVarSet isFlexiTcsTv $
750 tyVarsOfEvVarXs pushed_givens
751 -- See Note [Extra TcsTv untouchables]
753 ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
755 ; traceTcS "solveWanteds: } now doing nested implications {" $
756 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
757 , text "implics =" <+> ppr implics ]
759 ; (implic_eqs, unsolved_implics)
760 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
762 ; traceTcS "solveWanteds: done nested implications }" $
763 vcat [ text "implic_eqs =" <+> ppr implic_eqs
764 , text "unsolved_implics =" <+> ppr unsolved_implics ]
766 ; return (implic_eqs, unsolved_implics) }
768 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
770 -> Implication -- Wanted
771 -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
772 Bag Implication) -- Unsolved rest (always empty or singleton)
774 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
775 -- that are of the form unification var = type
777 -- 2. Maybe a unsolved implication, empty if entirely solved!
779 -- Precondition: everything is zonked by now
780 solveImplication tcs_untouchables inert
781 imp@(Implic { ic_untch = untch
782 , ic_binds = ev_binds
785 , ic_wanted = wanteds
787 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
788 recoverTcS (return (emptyBag, emptyBag)) $
789 -- Recover from nested failures. Even the top level is
790 -- just a bunch of implications, so failing at the first
792 do { traceTcS "solveImplication {" (ppr imp)
795 ; given_inert <- solveInteractGiven inert loc givens
797 -- Simplify the wanteds
798 ; (unsolved_flats, unsolved_implics, insols)
799 <- solve_wanteds given_inert wanteds
801 ; let (res_flat_free, res_flat_bound)
802 = floatEqualities skols givens unsolved_flats
803 final_flat = keepWanted res_flat_bound
805 ; let res_wanted = WC { wc_flat = final_flat
806 , wc_impl = unsolved_implics
807 , wc_insol = insols }
808 res_implic = unitImplication $
809 imp { ic_wanted = res_wanted
810 , ic_insol = insolubleWC res_wanted }
812 ; traceTcS "solveImplication end }" $ vcat
813 [ text "res_flat_free =" <+> ppr res_flat_free
814 , text "res_implic =" <+> ppr res_implic ]
816 ; return (res_flat_free, res_implic) }
819 floatEqualities :: TcTyVarSet -> [EvVar]
820 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
821 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
822 -- and come from the input wanted ev vars or deriveds
823 floatEqualities skols can_given wantders
824 | hasEqualities can_given = (emptyBag, wantders)
825 -- Note [Float Equalities out of Implications]
826 | otherwise = partitionBag is_floatable wantders
829 where is_floatable :: FlavoredEvVar -> Bool
830 is_floatable (EvVarX cv _fl)
831 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
832 is_floatable _flev = False
834 tvs_under_fsks :: Type -> TyVarSet
835 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
836 tvs_under_fsks (TyVarTy tv)
837 | not (isTcTyVar tv) = unitVarSet tv
838 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
839 | otherwise = unitVarSet tv
840 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
841 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
842 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
843 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
844 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
845 -- can mention type variables!
846 | isTyVar tv = inner_tvs `delVarSet` tv
847 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
848 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
850 inner_tvs = tvs_under_fsks ty
852 predTvs_under_fsks :: PredType -> TyVarSet
853 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
854 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
855 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
858 Note [Preparing inert set for implications]
859 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
860 Before solving the nested implications, we convert any unsolved flat wanteds
861 to givens, and add them to the inert set. Reasons:
863 a) In checking mode, suppresses unnecessary errors. We already have
864 on unsolved-wanted error; adding it to the givens prevents any
865 consequential errors from showing up
867 b) More importantly, in inference mode, we are going to quantify over this
868 constraint, and we *don't* want to quantify over any constraints that
869 are deducible from it.
871 c) Flattened type-family equalities must be exposed to the nested
872 constraints. Consider
873 F b ~ alpha, (forall c. F b ~ alpha)
874 Obviously this is soluble with [alpha := F b]. But the
875 unification is only done by solveCTyFunEqs, right at the end of
876 solveWanteds, and if we aren't careful we'll end up with an
877 unsolved goal inside the implication. We need to "push" the
878 as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
879 can be used to solve the inner (F b
880 ~ alpha). See Trac #4935.
882 d) There are other cases where interactions between wanteds that can help
883 to solve a constraint. For example
887 (C Int alpha), (forall d. C d blah => C Int a)
889 If we push the (C Int alpha) inwards, as a given, it can produce
890 a fundep (alpha~a) and this can float out again and be used to
891 fix alpha. (In general we can't float class constraints out just
892 in case (C d blah) might help to solve (C Int a).)
894 The unsolved wanteds are *canonical* but they may not be *inert*,
895 because when made into a given they might interact with other givens.
896 Hence the call to solveInteract. Example:
898 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
900 We were not able to solve (a ~w [beta]) but we can't just assume it as
901 given because the resulting set is not inert. Hence we have to do a
902 'solveInteract' step first.
904 Note [Extra TcsTv untouchables]
905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
906 Furthemore, we record the inert set simplifier-generated unification
907 variables of the TcsTv kind (such as variables from instance that have
908 been applied, or unification flattens). These variables must be passed
909 to the implications as extra untouchable variables. Otherwise we have
910 the danger of double unifications. Example (from trac ticket #4494):
912 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
914 In this example, beta is touchable inside the implication. The first
915 solveInteract step leaves 'uf' ununified. Then we move inside the
916 implication where a new constraint
918 emerges. We may spontaneously solve it to get uf := beta, so the whole
919 implication disappears but when we pop out again we are left with (F
920 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
921 uf will get unified *once more* to (F Int).
923 The solution is to record the TcsTvs (i.e. the simplifier-generated
924 unification variables) that are generated when solving the flats, and
925 make them untouchables for the nested implication. In the example
926 above uf would become untouchable, so beta would be forced to be
927 unified as beta := uf.
929 NB: A consequence is that every simplifier-generated TcsTv variable
930 that gets floated out of an implication becomes now untouchable
931 next time we go inside that implication to solve any residual
932 constraints. In effect, by floating an equality out of the
933 implication we are committing to have it solved in the outside.
935 Note [Float Equalities out of Implications]
936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
937 We want to float equalities out of vanilla existentials, but *not* out
938 of GADT pattern matches.
943 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
944 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
945 -- See Note [Solving Family Equations]
946 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
947 -- where the newly generated equalities (alpha := F xi) have been substituted through.
949 = do { untch <- getUntouchables
950 ; let (unsolved_can_cts, (ni_subst, cv_binds))
951 = getSolvableCTyFunEqs untch cts
952 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
953 , ppr ni_subst, ppr cv_binds
955 ; mapM_ solve_one cv_binds
957 ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
959 solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty
962 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
963 -- The TvSubstEnv is not idempotent, but is loop-free
964 -- See Note [Non-idempotent substitution] in Unify
965 emptyFunEqBinds :: FunEqBinds
966 emptyFunEqBinds = (emptyVarEnv, [])
968 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
969 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
970 = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
973 getSolvableCTyFunEqs :: TcsUntouchables
974 -> CanonicalCts -- Precondition: all Wanteds or Derived!
975 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
976 getSolvableCTyFunEqs untch cts
977 = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
979 dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
980 -> (CanonicalCts, FunEqBinds)
981 dflt_funeq (cts_in, feb@(tv_subst, _))
982 (CFunEqCan { cc_id = cv
987 | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
989 , isTouchableMetaTyVar_InRange untch tv
990 -- And it's a *touchable* unification variable
992 , typeKind xi `isSubKind` tyVarKind tv
993 -- Must do a small kind check since TcCanonical invariants
994 -- on family equations only impose compatibility, not subkinding
996 , not (tv `elemVarEnv` tv_subst)
997 -- Check not in extra_binds
998 -- See Note [Solving Family Equations], Point 1
1000 , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1001 -- Occurs check: see Note [Solving Family Equations], Point 2
1002 = ASSERT ( not (isGiven fl) )
1003 (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
1005 dflt_funeq (cts_in, fun_eq_binds) ct
1006 = (cts_in `extendCCans` ct, fun_eq_binds)
1009 Note [Solving Family Equations]
1010 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1011 After we are done with simplification we may be left with constraints of the form:
1012 [Wanted] F xis ~ beta
1013 If 'beta' is a touchable unification variable not already bound in the TyBinds
1014 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1016 When is it ok to do so?
1017 1) 'beta' must not already be defaulted to something. Example:
1019 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1020 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1021 have to report this as unsolved.
1023 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1024 set [beta := F xis] only if beta is not among the free variables of xis.
1026 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1027 of type family equations. See Inert Set invariants in TcInteract.
1030 *********************************************************************************
1032 * Defaulting and disamgiguation *
1034 *********************************************************************************
1036 Basic plan behind applyDefaulting rules:
1039 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
1040 For each defaultable group, do:
1041 For each possible substitution for [alpha |-> tau] where `alpha' is the
1042 group's variable, do:
1043 1) Make up new TcEvBinds
1044 2) Extend TcS with (groupVariable
1045 3) given_inert <- solveOne inert (given : a ~ tau)
1046 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1047 5) if unsolved == empty then
1048 sneakyUnify a |-> tau
1049 write the evidence bins
1050 return (final_inert ++ group_constraints,[])
1051 -- will contain the info (alpha |-> tau)!!
1052 goto next defaultable group
1053 if unsolved <> empty then
1054 throw away evidence binds
1055 try next substitution
1056 If you've run out of substitutions for this group, too bad, you failed
1057 return (inert,group)
1058 goto next defaultable group
1061 Collect all the (canonical-cts, wanteds) gathered this way.
1062 - Do a solveGiven over the canonical-cts to make sure they are inert
1063 ------------------------------------------------------------------------------------------
1067 applyDefaultingRules :: InertSet
1068 -> CanonicalCts -- All wanteds
1069 -> TcS (Bag FlavoredEvVar) -- All wanteds again!
1070 -- Return some *extra* givens, which express the
1071 -- type-class-default choice
1073 applyDefaultingRules inert wanteds
1074 | isEmptyBag wanteds
1077 = do { untch <- getUntouchables
1078 ; tv_cts <- mapM (defaultTyVar untch) $
1079 varSetElems (tyVarsOfCDicts wanteds)
1081 ; info@(_, default_tys, _) <- getDefaultInfo
1082 ; let groups = findDefaultableGroups info untch wanteds
1083 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1085 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1086 , text "Type defaults =" <+> ppr deflt_cts])
1088 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1091 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1092 -- defaultTyVar is used on any un-instantiated meta type variables to
1093 -- default the kind of ? and ?? etc to *. This is important to ensure
1094 -- that instance declarations match. For example consider
1095 -- instance Show (a->b)
1096 -- foo x = show (\_ -> True)
1097 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1098 -- and that won't match the typeKind (*) in the instance decl.
1101 -- We look only at touchable type variables. No further constraints
1102 -- are going to affect these type variables, so it's time to do it by
1103 -- hand. However we aren't ready to default them fully to () or
1104 -- whatever, because the type-class defaulting rules have yet to run.
1106 defaultTyVar untch the_tv
1107 | isTouchableMetaTyVar_InRange untch the_tv
1108 , not (k `eqKind` default_k)
1109 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1110 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1111 ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1113 = return emptyBag -- The common case
1115 k = tyVarKind the_tv
1116 default_k = defaultKind k
1120 findDefaultableGroups
1123 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1124 -> TcsUntouchables -- Untouchable
1125 -> CanonicalCts -- Unsolved
1126 -> [[(CanonicalCt,TcTyVar)]]
1127 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1129 | not (performDefaulting ctxt) = []
1130 | null default_tys = []
1131 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1133 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1134 non_unaries :: [CanonicalCt] -- and *other* constraints
1136 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1137 -- Finds unary type-class constraints
1138 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1139 | Just tv <- tcGetTyVar_maybe ty
1141 find_unary cc = Right cc -- Non unary or non dictionary
1143 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1144 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1146 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1148 is_defaultable_group ds@((_,tv):_)
1149 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1150 && not (tv `elemVarSet` bad_tvs)
1151 && isTouchableMetaTyVar_InRange untch tv
1152 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1153 is_defaultable_group [] = panic "defaultable_group"
1155 defaultable_classes clss
1156 | extended_defaults = any isInteractiveClass clss
1157 | otherwise = all is_std_class clss && (any is_num_class clss)
1159 -- In interactive mode, or with -XExtendedDefaultRules,
1160 -- we default Show a to Show () to avoid graututious errors on "show []"
1161 isInteractiveClass cls
1162 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1164 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1165 -- is_num_class adds IsString to the standard numeric classes,
1166 -- when -foverloaded-strings is enabled
1168 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1169 -- Similarly is_std_class
1171 ------------------------------
1172 disambigGroup :: [Type] -- The default types
1173 -> InertSet -- Given inert
1174 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1175 -- sharing same type variable
1176 -> TcS (Bag FlavoredEvVar)
1178 disambigGroup [] _inert _grp
1180 disambigGroup (default_ty:default_tys) inert group
1181 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1182 ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1183 ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1184 derived_eq = mkEvVarX ev der_flav
1186 ; success <- tryTcS $
1187 do { (_,final_inert) <- solveInteract inert $ listToBag $
1188 derived_eq : wanted_ev_vars
1189 ; let (_, unsolved) = extractUnsolved final_inert
1190 ; let wanted_unsolved = filterBag isWantedCt unsolved
1191 -- Don't care about Derived's
1192 ; return (isEmptyBag wanted_unsolved) }
1194 True -> -- Success: record the type variable binding, and return
1195 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1196 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1197 ; return (unitBag derived_eq) }
1198 False -> -- Failure: try with the next type
1199 do { traceTcS "disambigGroup failed, will try other default types"
1201 ; disambigGroup default_tys inert group } }
1203 ((the_ct,the_tv):_) = group
1204 wanteds = map fst group
1205 wanted_ev_vars :: [FlavoredEvVar]
1206 wanted_ev_vars = map deCanonicalise wanteds
1208 mk_derived_flavor :: CtFlavor -> CtFlavor
1209 mk_derived_flavor (Wanted loc) = Derived loc
1210 mk_derived_flavor _ = panic "Asked to disambiguate given or derived!"
1213 Note [Avoiding spurious errors]
1214 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1215 When doing the unification for defaulting, we check for skolem
1216 type variables, and simply don't default them. For example:
1217 f = (*) -- Monomorphic
1218 g :: Num a => a -> a
1220 Here, we get a complaint when checking the type signature for g,
1221 that g isn't polymorphic enough; but then we get another one when
1222 dealing with the (Num a) context arising from f's definition;
1223 we try to unify a with Int (to default it), but find that it's
1224 already been unified with the rigid variable from g's type sig
1228 *********************************************************************************
1232 *********************************************************************************
1235 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1236 newFlatWanteds orig theta
1237 = do { loc <- getCtLoc orig
1238 ; evs <- newWantedEvVars theta
1239 ; return (listToBag [EvVarX w loc | w <- evs]) }