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 (ptext (sLit "top level"))) 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 (ptext (sLit "defaults")))
71 *********************************************************************************
75 ***********************************************************************************
78 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 pred 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
95 doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)
97 ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
99 ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
100 ; (residual_wanted, _binds)
101 <- runTcS (SimplInfer doc) NoUntouchables $
102 solveWanteds emptyInert (mkFlatWC wanted)
104 ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
105 -- See Note [Exotic derived instance contexts]
106 get_good :: WantedEvVar -> Either PredType WantedEvVar
107 get_good wev | validDerivPred p = Left p
108 | otherwise = Right wev
109 where p = evVarOfPred wev
111 ; reportUnsolved (residual_wanted { wc_flat = bad })
113 ; let min_theta = mkMinimalBySCs (bagToList good)
114 ; return (substTheta subst_skol min_theta) }
117 Note [Overlap and deriving]
118 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
119 Consider some overlapping instances:
120 data Show a => Show [a] where ..
121 data Show [Char] where ...
123 Now a data type with deriving:
124 data T a = MkT [a] deriving( Show )
126 We want to get the derived instance
127 instance Show [a] => Show (T a) where...
129 instance Show a => Show (T a) where...
130 so that the (Show (T Char)) instance does the Right Thing
132 It's very like the situation when we're inferring the type
136 f :: Show [a] => a -> String
138 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
139 the context for the derived instance.
140 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
142 Note [Exotic derived instance contexts]
143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
144 In a 'derived' instance declaration, we *infer* the context. It's a
145 bit unclear what rules we should apply for this; the Haskell report is
146 silent. Obviously, constraints like (Eq a) are fine, but what about
147 data T f a = MkT (f a) deriving( Eq )
148 where we'd get an Eq (f a) constraint. That's probably fine too.
150 One could go further: consider
151 data T a b c = MkT (Foo a b c) deriving( Eq )
152 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
154 Notice that this instance (just) satisfies the Paterson termination
155 conditions. Then we *could* derive an instance decl like this:
157 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
158 even though there is no instance for (C Int a), because there just
159 *might* be an instance for, say, (C Int Bool) at a site where we
160 need the equality instance for T's.
162 However, this seems pretty exotic, and it's quite tricky to allow
163 this, and yet give sensible error messages in the (much more common)
164 case where we really want that instance decl for C.
166 So for now we simply require that the derived instance context
167 should have only type-variable constraints.
169 Here is another example:
170 data Fix f = In (f (Fix f)) deriving( Eq )
171 Here, if we are prepared to allow -XUndecidableInstances we
172 could derive the instance
173 instance Eq (f (Fix f)) => Eq (Fix f)
174 but this is so delicate that I don't think it should happen inside
175 'deriving'. If you want this, write it yourself!
177 NB: if you want to lift this condition, make sure you still meet the
178 termination conditions! If not, the deriving mechanism generates
179 larger and larger constraints. Example:
181 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
183 Note the lack of a Show instance for Succ. First we'll generate
184 instance (Show (Succ a), Show a) => Show (Seq a)
186 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
187 and so on. Instead we want to complain of no instance for (Show (Succ a)).
191 Allow constraints which consist only of type variables, with no repeats.
193 *********************************************************************************
197 ***********************************************************************************
200 simplifyInfer :: TopLevelFlag
201 -> Bool -- Apply monomorphism restriction
202 -> [(Name, TcTauType)] -- Variables to be generalised,
203 -- and their tau-types
205 -> TcM ([TcTyVar], -- Quantify over these type variables
206 [EvVar], -- ... and these constraints
207 TcEvBinds) -- ... binding these evidence variables
208 simplifyInfer top_lvl apply_mr name_taus wanteds
210 = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
211 ; zonked_taus <- zonkTcTypes (map snd name_taus)
212 ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
213 ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
214 ; return (qtvs, [], emptyTcEvBinds) }
217 = do { zonked_wanteds <- zonkWC wanteds
218 ; zonked_taus <- zonkTcTypes (map snd name_taus)
219 ; gbl_tvs <- tcGetGlobalTyVars
221 ; traceTc "simplifyInfer {" $ vcat
222 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
223 , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
224 , ptext (sLit "wanted =") <+> ppr zonked_wanteds
228 -- Make a guess at the quantified type variables
229 -- Then split the constraints on the baisis of those tyvars
230 -- to avoid unnecessarily simplifying a class constraint
231 -- See Note [Avoid unecessary constraint simplification]
232 ; let zonked_tau_tvs = get_tau_tvs zonked_taus
233 proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
234 zonked_tau_tvs `minusVarSet` gbl_tvs
235 (perhaps_bound, surely_free)
236 = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
238 ; traceTc "simplifyInfer proto" $ vcat
239 [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
240 , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
241 , ptext (sLit "surely_fref =") <+> ppr surely_free
244 ; emitFlats surely_free
245 ; traceTc "sinf" $ vcat
246 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
247 , ptext (sLit "surely_free =") <+> ppr surely_free
251 -- Now simplify the possibly-bound constraints
252 ; (simpl_results, tc_binds0)
253 <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $
254 simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
256 ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
257 (do { reportUnsolved simpl_results; failM })
260 -- Split again simplified_perhaps_bound, because some unifications
261 -- may have happened, and emit the free constraints.
262 ; gbl_tvs <- tcGetGlobalTyVars
263 ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
264 ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
265 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
266 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
267 constrained_tvs = tyVarsOfEvVarXs zonked_simples
268 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
269 (final_qtvs, (bound, free))
270 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
271 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
274 ; if isEmptyVarSet final_qtvs && isEmptyBag bound
275 then ASSERT( isEmptyBag (wc_insol simpl_results) )
276 do { traceTc "} simplifyInfer/no quantification" empty
277 ; emitImplications (wc_impl simpl_results)
278 ; return ([], [], EvBinds tc_binds0) }
281 -- Step 4, zonk quantified variables
282 { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
283 ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
284 | (name, ty) <- name_taus ]
285 -- Don't add the quantified variables here, because
286 -- they are also bound in ic_skols and we want them to be
288 skol_info = InferSkol poly_ids
290 ; gloc <- getCtLoc skol_info
291 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
294 -- Minimize `bound' and emit an implication
295 ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
296 ; ev_binds_var <- newTcEvBinds
297 ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
298 ; lcl_env <- getLclTypeEnv
299 ; let implic = Implic { ic_untch = NoUntouchables
301 , ic_skols = mkVarSet qtvs_to_return
302 , ic_given = minimal_bound_ev_vars
303 , ic_wanted = simpl_results { wc_flat = bound }
305 , ic_binds = ev_binds_var
307 ; emitImplication implic
308 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
309 vcat [ ptext (sLit "implic =") <+> ppr implic
310 -- ic_skols, ic_given give rest of result
311 , ptext (sLit "qtvs =") <+> ppr final_qtvs
312 , ptext (sLit "spb =") <+> ppr zonked_simples
313 , ptext (sLit "bound =") <+> ppr bound ]
317 ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
319 get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
320 | otherwise = exactTyVarsOfTypes
321 -- See Note [Silly type synonym] in TcType
325 Note [Minimize by Superclasses]
326 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
328 When we quantify over a constraint, in simplifyInfer we need to
329 quantify over a constraint that is minimal in some sense: For
330 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
331 we'd like to quantify over Ord alpha, because we can just get Eq alpha
332 from superclass selection from Ord alpha. This minimization is what
333 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
334 to check the original wanted.
337 simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
338 simplifyWithApprox wanted
339 = do { traceTcS "simplifyApproxLoop" (ppr wanted)
341 ; results <- solveWanteds emptyInert wanted
343 ; let (residual_implics, floats) = approximateImplications (wc_impl results)
345 -- If no new work was produced then we are done with simplifyApproxLoop
346 ; if insolubleWC results || isEmptyBag floats
349 else solveWanteds emptyInert
350 (WC { wc_flat = floats `unionBags` wc_flat results
351 , wc_impl = residual_implics
352 , wc_insol = emptyBag }) }
354 approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
355 -- Extracts any nested constraints that don't mention the skolems
356 approximateImplications impls
357 = do_bag (float_implic emptyVarSet) impls
359 do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
360 do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
361 plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
362 plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
364 float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
365 float_implic skols imp
366 = (unitBag (imp { ic_wanted = wanted' }), floats)
368 (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
370 float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
371 = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
373 (flat', floats1) = do_bag (float_flat skols) flat
374 (implic', floats2) = do_bag (float_implic skols) implic
376 float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
378 | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
379 | otherwise = (unitBag wev, emptyBag)
383 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
384 -- X-constraint 'wanted', nuking the 'gbls' at each stage
385 -- It's conservative in that if the seed could *possibly*
386 -- grow to include a type variable, then it does
388 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
389 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
391 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
392 growWantedEVs gbl_tvs ws tvs
393 | isEmptyBag ws = tvs
394 | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
396 -------- Helper functions, do not do fixpoint ------------------------
397 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
398 growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) .
399 growPreds gbl_tvs evVarOfPred (wc_flat wc) .
400 growPreds gbl_tvs evVarOfPred (wc_insol wc)
402 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
403 growImplics gbl_tvs implics tvs
404 = foldrBag grow_implic tvs implics
406 grow_implic implic tvs
407 = grow tvs `minusVarSet` ic_skols implic
409 grow = growWC gbl_tvs (ic_wanted implic) .
410 growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
411 -- We must grow from givens too; see test IPRun
413 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
414 growPreds gbl_tvs get_pred items tvs
415 = foldrBag extend tvs items
417 extend item tvs = tvs `unionVarSet`
418 (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
421 quantifyMe :: TyVarSet -- Quantifying over these
423 -> Bool -- True <=> quantify over this wanted
425 | isIPPred pred = True -- Note [Inheriting implicit parameters]
426 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
428 pred = evVarOfPred wev
431 Note [Avoid unecessary constraint simplification]
432 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
433 When inferring the type of a let-binding, with simplifyInfer,
434 try to avoid unnecessariliy simplifying class constraints.
435 Doing so aids sharing, but it also helps with delicate
437 instance C t => C [t] where ..
439 f x = let g y = ...(constraint C [t])...
441 When inferring a type for 'g', we don't want to apply the
442 instance decl, because then we can't satisfy (C t). So we
443 just notice that g isn't quantified over 't' and partition
444 the contraints before simplifying.
446 This only half-works, but then let-generalisation only half-works.
449 Note [Inheriting implicit parameters]
450 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
455 where f is *not* a top-level binding.
456 From the RHS of f we'll get the constraint (?y::Int).
457 There are two types we might infer for f:
461 (so we get ?y from the context of f's definition), or
463 f :: (?y::Int) => Int -> Int
465 At first you might think the first was better, becuase then
466 ?y behaves like a free variable of the definition, rather than
467 having to be passed at each call site. But of course, the WHOLE
468 IDEA is that ?y should be passed at each call site (that's what
469 dynamic binding means) so we'd better infer the second.
471 BOTTOM LINE: when *inferring types* you *must* quantify
472 over implicit parameters. See the predicate isFreeWhenInferring.
475 *********************************************************************************
479 ***********************************************************************************
481 Note [Simplifying RULE lhs constraints]
482 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
483 On the LHS of transformation rules we only simplify only equalities,
484 but not dictionaries. We want to keep dictionaries unsimplified, to
485 serve as the available stuff for the RHS of the rule. We *do* want to
486 simplify equalities, however, to detect ill-typed rules that cannot be
489 Implementation: the TcSFlags carried by the TcSMonad controls the
490 amount of simplification, so simplifyRuleLhs just sets the flag
493 Example. Consider the following left-hand side of a rule
494 f (x == y) (y > z) = ...
495 If we typecheck this expression we get constraints
496 d1 :: Ord a, d2 :: Eq a
497 We do NOT want to "simplify" to the LHS
498 forall x::a, y::a, z::a, d1::Ord a.
499 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
501 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
502 f ((==) d2 x y) ((>) d1 y z) = ...
504 Here is another example:
505 fromIntegral :: (Integral a, Num b) => a -> b
506 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
507 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
508 we *dont* want to get
510 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
511 because the scsel will mess up RULE matching. Instead we want
512 forall dIntegralInt, dNumInt.
513 fromIntegral Int Int dIntegralInt dNumInt = id Int
516 g (x == y) (y == z) = ..
517 where the two dictionaries are *identical*, we do NOT WANT
518 forall x::a, y::a, z::a, d1::Eq a
519 f ((==) d1 x y) ((>) d1 y z) = ...
520 because that will only match if the dict args are (visibly) equal.
521 Instead we want to quantify over the dictionaries separately.
523 In short, simplifyRuleLhs must *only* squash equalities, leaving
524 all dicts unchanged, with absolutely no sharing.
526 HOWEVER, under a nested implication things are different
528 f :: (forall a. Eq a => a->a) -> Bool -> ...
529 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
532 Here we *must* solve the wanted (Eq a) from the given (Eq a)
533 resulting from skolemising the agument type of g. So we
534 revert to SimplCheck when going under an implication.
537 simplifyRule :: RuleName
538 -> [TcTyVar] -- Explicit skolems
539 -> WantedConstraints -- Constraints from LHS
540 -> WantedConstraints -- Constraints from RHS
541 -> TcM ([EvVar], -- LHS dicts
542 TcEvBinds, -- Evidence for LHS
543 TcEvBinds) -- Evidence for RHS
544 -- See Note [Simplifying RULE lhs constraints]
545 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
546 = do { loc <- getCtLoc (RuleSkol name)
547 ; zonked_lhs <- zonkWC lhs_wanted
548 ; let untch = NoUntouchables
549 -- We allow ourselves to unify environment
550 -- variables; hence *no untouchables*
552 ; (lhs_results, lhs_binds)
553 <- runTcS (SimplRuleLhs name) untch $
554 solveWanteds emptyInert zonked_lhs
556 ; traceTc "simplifyRule" $
557 vcat [ text "zonked_lhs" <+> ppr zonked_lhs
558 , text "lhs_results" <+> ppr lhs_results
559 , text "lhs_binds" <+> ppr lhs_binds
560 , text "rhs_wanted" <+> ppr rhs_wanted ]
563 -- Don't quantify over equalities (judgement call here)
564 ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
565 (wc_flat lhs_results)
566 lhs_dicts = map evVarOf (bagToList dicts)
567 -- Dicts and implicit parameters
569 -- Fail if we have not got down to unsolved flats
570 ; ev_binds_var <- newTcEvBinds
571 ; emitImplication $ Implic { ic_untch = untch
572 , ic_env = emptyNameEnv
573 , ic_skols = mkVarSet tv_bndrs
574 , ic_given = lhs_dicts
575 , ic_wanted = lhs_results { wc_flat = eqs }
576 , ic_insol = insolubleWC lhs_results
577 , ic_binds = ev_binds_var
580 -- Notice that we simplify the RHS with only the explicitly
581 -- introduced skolems, allowing the RHS to constrain any
582 -- unification variables.
583 -- Then, and only then, we call zonkQuantifiedTypeVariables
584 -- Example foo :: Ord a => a -> a
585 -- foo_spec :: Int -> Int
586 -- {-# RULE "foo" foo = foo_spec #-}
587 -- Here, it's the RHS that fixes the type variable
589 -- So we don't want to make untouchable the type
590 -- variables in the envt of the RHS, because they include
591 -- the template variables of the RULE
593 -- Hence the rather painful ad-hoc treatement here
594 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
595 ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
596 ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
597 WC { wc_flat = emptyBag
598 , wc_insol = emptyBag
599 , wc_impl = unitBag $
600 Implic { ic_untch = NoUntouchables
601 , ic_env = emptyNameEnv
602 , ic_skols = mkVarSet tv_bndrs
603 , ic_given = lhs_dicts
604 , ic_wanted = rhs_wanted
605 , ic_insol = insolubleWC rhs_wanted
606 , ic_binds = rhs_binds_var
608 ; rhs_binds2 <- readTcRef evb_ref
612 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
616 *********************************************************************************
620 ***********************************************************************************
623 simplifyCheck :: SimplContext
624 -> WantedConstraints -- Wanted
626 -- Solve a single, top-level implication constraint
627 -- e.g. typically one created from a top-level type signature
628 -- f :: forall a. [a] -> [a]
630 -- We do this even if the function has no polymorphism:
634 -- (whereas for *nested* bindings we would not create
635 -- an implication constraint for g at all.)
637 -- Fails if can't solve something in the input wanteds
638 simplifyCheck ctxt wanteds
639 = do { wanteds <- zonkWC wanteds
641 ; traceTc "simplifyCheck {" (vcat
642 [ ptext (sLit "wanted =") <+> ppr wanteds ])
644 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
645 solveWanteds emptyInert wanteds
647 ; traceTc "simplifyCheck }" $
648 ptext (sLit "unsolved =") <+> ppr unsolved
650 ; reportUnsolved unsolved
655 solveWanteds :: InertSet -- Given
657 -> TcS WantedConstraints
658 solveWanteds inert wanted
659 = do { (unsolved_flats, unsolved_implics, insols)
660 <- solve_wanteds inert wanted
661 ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived
662 , wc_impl = unsolved_implics
663 , wc_insol = insols }) }
665 solve_wanteds :: InertSet -- Given
667 -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
668 -- solve_wanteds iterates when it is able to float equalities
669 -- out of one or more of the implications
670 solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
671 = do { traceTcS "solveWanteds {" (ppr wanted)
674 -- Discard from insols all the derived/given constraints
675 -- because they will show up again when we try to solve
676 -- everything else. Solving them a second time is a bit
677 -- of a waste, but the code is simple, and the program is
679 ; let all_flats = flats `unionBags` keepWanted insols
680 ; inert1 <- solveInteractWanted inert (bagToList all_flats)
682 ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
684 ; bb <- getTcEvBindsBag
685 ; tb <- getTcSTyBindsMap
686 ; traceTcS "solveWanteds }" $
687 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
688 , text "unsolved_implics =" <+> ppr unsolved_implics
689 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
690 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
693 ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
694 -- See Note [Solving Family Equations]
695 -- NB: remaining_flats has already had subst applied
697 ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
699 ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
700 , mapBag (substImplication subst) unsolved_implics
701 , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
707 -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
708 simpl_loop n inert implics
710 = trace "solveWanteds: loop" $ -- Always bleat
711 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
712 ; let (_, unsolved_cans) = extractUnsolved inert
713 ; return (unsolved_cans, implics) }
716 = do { traceTcS "solveWanteds: simpl_loop start {" $
717 vcat [ text "n =" <+> ppr n
718 , text "implics =" <+> ppr implics
719 , text "inert =" <+> ppr inert ]
721 ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
722 -- unsolved_cans contains either Wanted or Derived!
724 ; (implic_eqs, unsolved_implics)
725 <- solveNestedImplications just_given_inert unsolved_cans implics
727 -- Apply defaulting rules if and only if there
728 -- no floated equalities. If there are, they may
729 -- solve the remaining wanteds, so don't do defaulting.
730 ; improve_eqs <- if not (isEmptyBag implic_eqs)
731 then return implic_eqs
732 else applyDefaultingRules just_given_inert unsolved_cans
734 ; traceTcS "solveWanteds: simpl_loop end }" $
735 vcat [ text "improve_eqs =" <+> ppr improve_eqs
736 , text "unsolved_flats =" <+> ppr unsolved_cans
737 , text "unsolved_implics =" <+> ppr unsolved_implics ]
739 ; (improve_eqs_already_in_inert, inert_with_improvement)
740 <- solveInteract inert improve_eqs
742 ; if improve_eqs_already_in_inert then
743 return (unsolved_cans, unsolved_implics)
745 simpl_loop (n+1) inert_with_improvement
746 -- Contain unsolved_cans and the improve_eqs
750 givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
751 -- Extract the *wanted* ones from CanonicalCts
752 -- and make them into *givens*
753 givensFromWanteds = foldrBag getWanted emptyBag
755 getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
757 | not (isCFrozenErr cc)
758 , Wanted loc <- cc_flavor cc
759 , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
760 = given `consBag` givens
762 = givens -- We are not helping anyone by pushing a Derived in!
763 -- Because if we could not solve it to start with
764 -- we are not going to do either inside the impl constraint
766 solveNestedImplications :: InertSet -> CanonicalCts
768 -> TcS (Bag FlavoredEvVar, Bag Implication)
769 solveNestedImplications just_given_inert unsolved_cans implics
771 = return (emptyBag, emptyBag)
773 = do { -- See Note [Preparing inert set for implications]
774 -- Push the unsolved wanteds inwards, but as givens
775 let pushed_givens = givensFromWanteds unsolved_cans
776 tcs_untouchables = filterVarSet isFlexiTcsTv $
777 tyVarsOfEvVarXs pushed_givens
778 -- See Note [Extra TcsTv untouchables]
780 ; traceTcS "solveWanteds: preparing inerts for implications {"
781 (vcat [ppr tcs_untouchables, ppr pushed_givens])
783 ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
785 ; traceTcS "solveWanteds: } now doing nested implications {" $
786 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
787 , text "implics =" <+> ppr implics ]
789 ; (implic_eqs, unsolved_implics)
790 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
792 ; traceTcS "solveWanteds: done nested implications }" $
793 vcat [ text "implic_eqs =" <+> ppr implic_eqs
794 , text "unsolved_implics =" <+> ppr unsolved_implics ]
796 ; return (implic_eqs, unsolved_implics) }
798 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
800 -> Implication -- Wanted
801 -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
802 Bag Implication) -- Unsolved rest (always empty or singleton)
804 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
805 -- that are of the form unification var = type
807 -- 2. Maybe a unsolved implication, empty if entirely solved!
809 -- Precondition: everything is zonked by now
810 solveImplication tcs_untouchables inert
811 imp@(Implic { ic_untch = untch
812 , ic_binds = ev_binds
815 , ic_wanted = wanteds
817 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
818 recoverTcS (return (emptyBag, emptyBag)) $
819 -- Recover from nested failures. Even the top level is
820 -- just a bunch of implications, so failing at the first
822 do { traceTcS "solveImplication {" (ppr imp)
825 ; given_inert <- solveInteractGiven inert loc givens
827 -- Simplify the wanteds
828 ; (unsolved_flats, unsolved_implics, insols)
829 <- solve_wanteds given_inert wanteds
831 ; let (res_flat_free, res_flat_bound)
832 = floatEqualities skols givens unsolved_flats
833 final_flat = keepWanted res_flat_bound
835 ; let res_wanted = WC { wc_flat = final_flat
836 , wc_impl = unsolved_implics
837 , wc_insol = insols }
838 res_implic = unitImplication $
839 imp { ic_wanted = res_wanted
840 , ic_insol = insolubleWC res_wanted }
842 ; traceTcS "solveImplication end }" $ vcat
843 [ text "res_flat_free =" <+> ppr res_flat_free
844 , text "res_implic =" <+> ppr res_implic ]
846 ; return (res_flat_free, res_implic) }
849 floatEqualities :: TcTyVarSet -> [EvVar]
850 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
851 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
852 -- and come from the input wanted ev vars or deriveds
853 floatEqualities skols can_given wantders
854 | hasEqualities can_given = (emptyBag, wantders)
855 -- Note [Float Equalities out of Implications]
856 | otherwise = partitionBag is_floatable wantders
859 where is_floatable :: FlavoredEvVar -> Bool
860 is_floatable (EvVarX cv _fl)
861 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
862 is_floatable _flev = False
864 tvs_under_fsks :: Type -> TyVarSet
865 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
866 tvs_under_fsks (TyVarTy tv)
867 | not (isTcTyVar tv) = unitVarSet tv
868 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
869 | otherwise = unitVarSet tv
870 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
871 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
872 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
873 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
874 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
875 -- can mention type variables!
876 | isTyVar tv = inner_tvs `delVarSet` tv
877 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
878 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
880 inner_tvs = tvs_under_fsks ty
882 predTvs_under_fsks :: PredType -> TyVarSet
883 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
884 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
885 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
888 Note [Preparing inert set for implications]
889 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
890 Before solving the nested implications, we convert any unsolved flat wanteds
891 to givens, and add them to the inert set. Reasons:
893 a) In checking mode, suppresses unnecessary errors. We already have
894 on unsolved-wanted error; adding it to the givens prevents any
895 consequential errors from showing up
897 b) More importantly, in inference mode, we are going to quantify over this
898 constraint, and we *don't* want to quantify over any constraints that
899 are deducible from it.
901 c) Flattened type-family equalities must be exposed to the nested
902 constraints. Consider
903 F b ~ alpha, (forall c. F b ~ alpha)
904 Obviously this is soluble with [alpha := F b]. But the
905 unification is only done by solveCTyFunEqs, right at the end of
906 solveWanteds, and if we aren't careful we'll end up with an
907 unsolved goal inside the implication. We need to "push" the
908 as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
909 can be used to solve the inner (F b
910 ~ alpha). See Trac #4935.
912 d) There are other cases where interactions between wanteds that can help
913 to solve a constraint. For example
917 (C Int alpha), (forall d. C d blah => C Int a)
919 If we push the (C Int alpha) inwards, as a given, it can produce
920 a fundep (alpha~a) and this can float out again and be used to
921 fix alpha. (In general we can't float class constraints out just
922 in case (C d blah) might help to solve (C Int a).)
924 The unsolved wanteds are *canonical* but they may not be *inert*,
925 because when made into a given they might interact with other givens.
926 Hence the call to solveInteract. Example:
928 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
930 We were not able to solve (a ~w [beta]) but we can't just assume it as
931 given because the resulting set is not inert. Hence we have to do a
932 'solveInteract' step first.
934 Note [Extra TcsTv untouchables]
935 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
936 Furthemore, we record the inert set simplifier-generated unification
937 variables of the TcsTv kind (such as variables from instance that have
938 been applied, or unification flattens). These variables must be passed
939 to the implications as extra untouchable variables. Otherwise we have
940 the danger of double unifications. Example (from trac ticket #4494):
942 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
944 In this example, beta is touchable inside the implication. The first
945 solveInteract step leaves 'uf' ununified. Then we move inside the
946 implication where a new constraint
948 emerges. We may spontaneously solve it to get uf := beta, so the whole
949 implication disappears but when we pop out again we are left with (F
950 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
951 uf will get unified *once more* to (F Int).
953 The solution is to record the TcsTvs (i.e. the simplifier-generated
954 unification variables) that are generated when solving the flats, and
955 make them untouchables for the nested implication. In the example
956 above uf would become untouchable, so beta would be forced to be
957 unified as beta := uf.
959 NB: A consequence is that every simplifier-generated TcsTv variable
960 that gets floated out of an implication becomes now untouchable
961 next time we go inside that implication to solve any residual
962 constraints. In effect, by floating an equality out of the
963 implication we are committing to have it solved in the outside.
965 Note [Float Equalities out of Implications]
966 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
967 We want to float equalities out of vanilla existentials, but *not* out
968 of GADT pattern matches.
973 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
974 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
975 -- See Note [Solving Family Equations]
976 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
977 -- where the newly generated equalities (alpha := F xi) have been substituted through.
979 = do { untch <- getUntouchables
980 ; let (unsolved_can_cts, (ni_subst, cv_binds))
981 = getSolvableCTyFunEqs untch cts
982 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
983 , ppr ni_subst, ppr cv_binds
985 ; mapM_ solve_one cv_binds
987 ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
989 solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
992 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
993 -- The TvSubstEnv is not idempotent, but is loop-free
994 -- See Note [Non-idempotent substitution] in Unify
995 emptyFunEqBinds :: FunEqBinds
996 emptyFunEqBinds = (emptyVarEnv, [])
998 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
999 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
1000 = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
1003 getSolvableCTyFunEqs :: TcsUntouchables
1004 -> CanonicalCts -- Precondition: all Wanteds or Derived!
1005 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
1006 getSolvableCTyFunEqs untch cts
1007 = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
1009 dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
1010 -> (CanonicalCts, FunEqBinds)
1011 dflt_funeq (cts_in, feb@(tv_subst, _))
1012 (CFunEqCan { cc_id = cv
1017 | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
1019 , isTouchableMetaTyVar_InRange untch tv
1020 -- And it's a *touchable* unification variable
1022 , typeKind xi `isSubKind` tyVarKind tv
1023 -- Must do a small kind check since TcCanonical invariants
1024 -- on family equations only impose compatibility, not subkinding
1026 , not (tv `elemVarEnv` tv_subst)
1027 -- Check not in extra_binds
1028 -- See Note [Solving Family Equations], Point 1
1030 , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1031 -- Occurs check: see Note [Solving Family Equations], Point 2
1032 = ASSERT ( not (isGiven fl) )
1033 (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
1035 dflt_funeq (cts_in, fun_eq_binds) ct
1036 = (cts_in `extendCCans` ct, fun_eq_binds)
1039 Note [Solving Family Equations]
1040 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1041 After we are done with simplification we may be left with constraints of the form:
1042 [Wanted] F xis ~ beta
1043 If 'beta' is a touchable unification variable not already bound in the TyBinds
1044 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1046 When is it ok to do so?
1047 1) 'beta' must not already be defaulted to something. Example:
1049 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1050 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1051 have to report this as unsolved.
1053 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1054 set [beta := F xis] only if beta is not among the free variables of xis.
1056 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1057 of type family equations. See Inert Set invariants in TcInteract.
1060 *********************************************************************************
1062 * Defaulting and disamgiguation *
1064 *********************************************************************************
1066 Basic plan behind applyDefaulting rules:
1069 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
1070 For each defaultable group, do:
1071 For each possible substitution for [alpha |-> tau] where `alpha' is the
1072 group's variable, do:
1073 1) Make up new TcEvBinds
1074 2) Extend TcS with (groupVariable
1075 3) given_inert <- solveOne inert (given : a ~ tau)
1076 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1077 5) if unsolved == empty then
1078 sneakyUnify a |-> tau
1079 write the evidence bins
1080 return (final_inert ++ group_constraints,[])
1081 -- will contain the info (alpha |-> tau)!!
1082 goto next defaultable group
1083 if unsolved <> empty then
1084 throw away evidence binds
1085 try next substitution
1086 If you've run out of substitutions for this group, too bad, you failed
1087 return (inert,group)
1088 goto next defaultable group
1091 Collect all the (canonical-cts, wanteds) gathered this way.
1092 - Do a solveGiven over the canonical-cts to make sure they are inert
1093 ------------------------------------------------------------------------------------------
1097 applyDefaultingRules :: InertSet
1098 -> CanonicalCts -- All wanteds
1099 -> TcS (Bag FlavoredEvVar) -- All wanteds again!
1100 -- Return some *extra* givens, which express the
1101 -- type-class-default choice
1103 applyDefaultingRules inert wanteds
1104 | isEmptyBag wanteds
1107 = do { untch <- getUntouchables
1108 ; tv_cts <- mapM (defaultTyVar untch) $
1109 varSetElems (tyVarsOfCDicts wanteds)
1111 ; info@(_, default_tys, _) <- getDefaultInfo
1112 ; let groups = findDefaultableGroups info untch wanteds
1113 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1115 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1116 , text "Type defaults =" <+> ppr deflt_cts])
1118 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1121 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1122 -- defaultTyVar is used on any un-instantiated meta type variables to
1123 -- default the kind of ? and ?? etc to *. This is important to ensure
1124 -- that instance declarations match. For example consider
1125 -- instance Show (a->b)
1126 -- foo x = show (\_ -> True)
1127 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1128 -- and that won't match the typeKind (*) in the instance decl.
1131 -- We look only at touchable type variables. No further constraints
1132 -- are going to affect these type variables, so it's time to do it by
1133 -- hand. However we aren't ready to default them fully to () or
1134 -- whatever, because the type-class defaulting rules have yet to run.
1136 defaultTyVar untch the_tv
1137 | isTouchableMetaTyVar_InRange untch the_tv
1138 , not (k `eqKind` default_k)
1139 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1140 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1141 ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1143 = return emptyBag -- The common case
1145 k = tyVarKind the_tv
1146 default_k = defaultKind k
1150 findDefaultableGroups
1153 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1154 -> TcsUntouchables -- Untouchable
1155 -> CanonicalCts -- Unsolved
1156 -> [[(CanonicalCt,TcTyVar)]]
1157 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1159 | not (performDefaulting ctxt) = []
1160 | null default_tys = []
1161 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1163 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1164 non_unaries :: [CanonicalCt] -- and *other* constraints
1166 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1167 -- Finds unary type-class constraints
1168 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1169 | Just tv <- tcGetTyVar_maybe ty
1171 find_unary cc = Right cc -- Non unary or non dictionary
1173 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1174 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1176 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1178 is_defaultable_group ds@((_,tv):_)
1179 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1180 && not (tv `elemVarSet` bad_tvs)
1181 && isTouchableMetaTyVar_InRange untch tv
1182 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1183 is_defaultable_group [] = panic "defaultable_group"
1185 defaultable_classes clss
1186 | extended_defaults = any isInteractiveClass clss
1187 | otherwise = all is_std_class clss && (any is_num_class clss)
1189 -- In interactive mode, or with -XExtendedDefaultRules,
1190 -- we default Show a to Show () to avoid graututious errors on "show []"
1191 isInteractiveClass cls
1192 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1194 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1195 -- is_num_class adds IsString to the standard numeric classes,
1196 -- when -foverloaded-strings is enabled
1198 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1199 -- Similarly is_std_class
1201 ------------------------------
1202 disambigGroup :: [Type] -- The default types
1203 -> InertSet -- Given inert
1204 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1205 -- sharing same type variable
1206 -> TcS (Bag FlavoredEvVar)
1208 disambigGroup [] _inert _grp
1210 disambigGroup (default_ty:default_tys) inert group
1211 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1212 ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1213 ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1214 derived_eq = mkEvVarX ev der_flav
1216 ; success <- tryTcS $
1217 do { (_,final_inert) <- solveInteract inert $ listToBag $
1218 derived_eq : wanted_ev_vars
1219 ; let (_, unsolved) = extractUnsolved final_inert
1220 ; let wanted_unsolved = filterBag isWantedCt unsolved
1221 -- Don't care about Derived's
1222 ; return (isEmptyBag wanted_unsolved) }
1224 True -> -- Success: record the type variable binding, and return
1225 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1226 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1227 ; return (unitBag derived_eq) }
1228 False -> -- Failure: try with the next type
1229 do { traceTcS "disambigGroup failed, will try other default types"
1231 ; disambigGroup default_tys inert group } }
1233 ((the_ct,the_tv):_) = group
1234 wanteds = map fst group
1235 wanted_ev_vars :: [FlavoredEvVar]
1236 wanted_ev_vars = map deCanonicalise wanteds
1238 mk_derived_flavor :: CtFlavor -> CtFlavor
1239 mk_derived_flavor (Wanted loc) = Derived loc
1240 mk_derived_flavor _ = panic "Asked to disambiguate given or derived!"
1243 Note [Avoiding spurious errors]
1244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1245 When doing the unification for defaulting, we check for skolem
1246 type variables, and simply don't default them. For example:
1247 f = (*) -- Monomorphic
1248 g :: Num a => a -> a
1250 Here, we get a complaint when checking the type signature for g,
1251 that g isn't polymorphic enough; but then we get another one when
1252 dealing with the (Num a) context arising from f's definition;
1253 we try to unify a with Int (to default it), but find that it's
1254 already been unified with the rigid variable from g's type sig
1258 *********************************************************************************
1262 *********************************************************************************
1265 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1266 newFlatWanteds orig theta
1267 = do { loc <- getCtLoc orig
1268 ; evs <- newWantedEvVars theta
1269 ; return (listToBag [EvVarX w loc | w <- evs]) }