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 <- tcInstSkolTyVars tvs -- Skolemize
86 -- The constraint solving machinery
87 -- expects *TcTyVars* not TyVars.
88 -- We use *non-overlappable* (vanilla) skolems
89 -- See Note [Overlap and deriving]
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 [Overlap and deriving]
115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
116 Consider some overlapping instances:
117 data Show a => Show [a] where ..
118 data Show [Char] where ...
120 Now a data type with deriving:
121 data T a = MkT [a] deriving( Show )
123 We want to get the derived instance
124 instance Show [a] => Show (T a) where...
126 instance Show a => Show (T a) where...
127 so that the (Show (T Char)) instance does the Right Thing
129 It's very like the situation when we're inferring the type
133 f :: Show [a] => a -> String
135 BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
136 the context for the derived instance.
137 Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
139 Note [Exotic derived instance contexts]
140 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
141 In a 'derived' instance declaration, we *infer* the context. It's a
142 bit unclear what rules we should apply for this; the Haskell report is
143 silent. Obviously, constraints like (Eq a) are fine, but what about
144 data T f a = MkT (f a) deriving( Eq )
145 where we'd get an Eq (f a) constraint. That's probably fine too.
147 One could go further: consider
148 data T a b c = MkT (Foo a b c) deriving( Eq )
149 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
151 Notice that this instance (just) satisfies the Paterson termination
152 conditions. Then we *could* derive an instance decl like this:
154 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
155 even though there is no instance for (C Int a), because there just
156 *might* be an instance for, say, (C Int Bool) at a site where we
157 need the equality instance for T's.
159 However, this seems pretty exotic, and it's quite tricky to allow
160 this, and yet give sensible error messages in the (much more common)
161 case where we really want that instance decl for C.
163 So for now we simply require that the derived instance context
164 should have only type-variable constraints.
166 Here is another example:
167 data Fix f = In (f (Fix f)) deriving( Eq )
168 Here, if we are prepared to allow -XUndecidableInstances we
169 could derive the instance
170 instance Eq (f (Fix f)) => Eq (Fix f)
171 but this is so delicate that I don't think it should happen inside
172 'deriving'. If you want this, write it yourself!
174 NB: if you want to lift this condition, make sure you still meet the
175 termination conditions! If not, the deriving mechanism generates
176 larger and larger constraints. Example:
178 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
180 Note the lack of a Show instance for Succ. First we'll generate
181 instance (Show (Succ a), Show a) => Show (Seq a)
183 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
184 and so on. Instead we want to complain of no instance for (Show (Succ a)).
188 Allow constraints which consist only of type variables, with no repeats.
190 *********************************************************************************
194 ***********************************************************************************
197 simplifyInfer :: TopLevelFlag
198 -> Bool -- Apply monomorphism restriction
199 -> [(Name, TcTauType)] -- Variables to be generalised,
200 -- and their tau-types
202 -> TcM ([TcTyVar], -- Quantify over these type variables
203 [EvVar], -- ... and these constraints
204 TcEvBinds) -- ... binding these evidence variables
205 simplifyInfer top_lvl apply_mr name_taus wanteds
207 = do { gbl_tvs <- tcGetGlobalTyVars -- Already zonked
208 ; zonked_taus <- zonkTcTypes (map snd name_taus)
209 ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
210 ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
211 ; return (qtvs, [], emptyTcEvBinds) }
214 = do { zonked_wanteds <- zonkWC wanteds
215 ; zonked_taus <- zonkTcTypes (map snd name_taus)
216 ; gbl_tvs <- tcGetGlobalTyVars
218 ; traceTc "simplifyInfer {" $ vcat
219 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
220 , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
221 , ptext (sLit "wanted =") <+> ppr zonked_wanteds
225 -- Make a guess at the quantified type variables
226 -- Then split the constraints on the baisis of those tyvars
227 -- to avoid unnecessarily simplifying a class constraint
228 -- See Note [Avoid unecessary constraint simplification]
229 ; let zonked_tau_tvs = get_tau_tvs zonked_taus
230 proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
231 zonked_tau_tvs `minusVarSet` gbl_tvs
232 (perhaps_bound, surely_free)
233 = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
235 ; traceTc "simplifyInfer proto" $ vcat
236 [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
237 , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
238 , ptext (sLit "surely_fref =") <+> ppr surely_free
241 ; emitFlats surely_free
242 ; traceTc "sinf" $ vcat
243 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
244 , ptext (sLit "surely_free =") <+> ppr surely_free
248 -- Now simplify the possibly-bound constraints
249 ; (simpl_results, tc_binds0)
250 <- runTcS SimplInfer NoUntouchables $
251 simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
253 ; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
254 (do { reportUnsolved simpl_results; failM })
257 -- Split again simplified_perhaps_bound, because some unifications
258 -- may have happened, and emit the free constraints.
259 ; gbl_tvs <- tcGetGlobalTyVars
260 ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
261 ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
262 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
263 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
264 constrained_tvs = tyVarsOfEvVarXs zonked_simples
265 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
266 (final_qtvs, (bound, free))
267 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
268 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
271 ; if isEmptyVarSet final_qtvs && isEmptyBag bound
272 then ASSERT( isEmptyBag (wc_insol simpl_results) )
273 do { traceTc "} simplifyInfer/no quantification" empty
274 ; emitImplications (wc_impl simpl_results)
275 ; return ([], [], EvBinds tc_binds0) }
278 -- Step 4, zonk quantified variables
279 { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
280 ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
281 | (name, ty) <- name_taus ]
282 -- Don't add the quantified variables here, because
283 -- they are also bound in ic_skols and we want them to be
285 skol_info = InferSkol poly_ids
287 ; gloc <- getCtLoc skol_info
288 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
291 -- Minimize `bound' and emit an implication
292 ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
293 ; ev_binds_var <- newTcEvBinds
294 ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
295 ; lcl_env <- getLclTypeEnv
296 ; let implic = Implic { ic_untch = NoUntouchables
298 , ic_skols = mkVarSet qtvs_to_return
299 , ic_given = minimal_bound_ev_vars
300 , ic_wanted = simpl_results { wc_flat = bound }
302 , ic_binds = ev_binds_var
304 ; emitImplication implic
305 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
306 vcat [ ptext (sLit "implic =") <+> ppr implic
307 -- ic_skols, ic_given give rest of result
308 , ptext (sLit "qtvs =") <+> ppr final_qtvs
309 , ptext (sLit "spb =") <+> ppr zonked_simples
310 , ptext (sLit "bound =") <+> ppr bound ]
314 ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
316 get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
317 | otherwise = exactTyVarsOfTypes
318 -- See Note [Silly type synonym] in TcType
322 Note [Minimize by Superclasses]
323 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
325 When we quantify over a constraint, in simplifyInfer we need to
326 quantify over a constraint that is minimal in some sense: For
327 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
328 we'd like to quantify over Ord alpha, because we can just get Eq alpha
329 from superclass selection from Ord alpha. This minimization is what
330 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
331 to check the original wanted.
334 simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
335 simplifyWithApprox wanted
336 = do { traceTcS "simplifyApproxLoop" (ppr wanted)
338 ; results <- solveWanteds emptyInert wanted
340 ; let (residual_implics, floats) = approximateImplications (wc_impl results)
342 -- If no new work was produced then we are done with simplifyApproxLoop
343 ; if insolubleWC results || isEmptyBag floats
346 else solveWanteds emptyInert
347 (WC { wc_flat = floats `unionBags` wc_flat results
348 , wc_impl = residual_implics
349 , wc_insol = emptyBag }) }
351 approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
352 -- Extracts any nested constraints that don't mention the skolems
353 approximateImplications impls
354 = do_bag (float_implic emptyVarSet) impls
356 do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
357 do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
358 plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
359 plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
361 float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
362 float_implic skols imp
363 = (unitBag (imp { ic_wanted = wanted' }), floats)
365 (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
367 float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
368 = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
370 (flat', floats1) = do_bag (float_flat skols) flat
371 (implic', floats2) = do_bag (float_implic skols) implic
373 float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
375 | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
376 | otherwise = (unitBag wev, emptyBag)
380 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
381 -- X-constraint 'wanted', nuking the 'gbls' at each stage
382 -- It's conservative in that if the seed could *possibly*
383 -- grow to include a type variable, then it does
385 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
386 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
388 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
389 growWantedEVs gbl_tvs ws tvs
390 | isEmptyBag ws = tvs
391 | otherwise = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
393 -------- Helper functions, do not do fixpoint ------------------------
394 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
395 growWC gbl_tvs wc = growImplics gbl_tvs (wc_impl wc) .
396 growPreds gbl_tvs evVarOfPred (wc_flat wc) .
397 growPreds gbl_tvs evVarOfPred (wc_insol wc)
399 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
400 growImplics gbl_tvs implics tvs
401 = foldrBag grow_implic tvs implics
403 grow_implic implic tvs
404 = grow tvs `minusVarSet` ic_skols implic
406 grow = growWC gbl_tvs (ic_wanted implic) .
407 growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
408 -- We must grow from givens too; see test IPRun
410 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
411 growPreds gbl_tvs get_pred items tvs
412 = foldrBag extend tvs items
414 extend item tvs = tvs `unionVarSet`
415 (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
418 quantifyMe :: TyVarSet -- Quantifying over these
420 -> Bool -- True <=> quantify over this wanted
422 | isIPPred pred = True -- Note [Inheriting implicit parameters]
423 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
425 pred = evVarOfPred wev
428 Note [Avoid unecessary constraint simplification]
429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 When inferring the type of a let-binding, with simplifyInfer,
431 try to avoid unnecessariliy simplifying class constraints.
432 Doing so aids sharing, but it also helps with delicate
434 instance C t => C [t] where ..
436 f x = let g y = ...(constraint C [t])...
438 When inferring a type for 'g', we don't want to apply the
439 instance decl, because then we can't satisfy (C t). So we
440 just notice that g isn't quantified over 't' and partition
441 the contraints before simplifying.
443 This only half-works, but then let-generalisation only half-works.
446 Note [Inheriting implicit parameters]
447 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
452 where f is *not* a top-level binding.
453 From the RHS of f we'll get the constraint (?y::Int).
454 There are two types we might infer for f:
458 (so we get ?y from the context of f's definition), or
460 f :: (?y::Int) => Int -> Int
462 At first you might think the first was better, becuase then
463 ?y behaves like a free variable of the definition, rather than
464 having to be passed at each call site. But of course, the WHOLE
465 IDEA is that ?y should be passed at each call site (that's what
466 dynamic binding means) so we'd better infer the second.
468 BOTTOM LINE: when *inferring types* you *must* quantify
469 over implicit parameters. See the predicate isFreeWhenInferring.
472 *********************************************************************************
476 ***********************************************************************************
478 Note [Simplifying RULE lhs constraints]
479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
480 On the LHS of transformation rules we only simplify only equalities,
481 but not dictionaries. We want to keep dictionaries unsimplified, to
482 serve as the available stuff for the RHS of the rule. We *do* want to
483 simplify equalities, however, to detect ill-typed rules that cannot be
486 Implementation: the TcSFlags carried by the TcSMonad controls the
487 amount of simplification, so simplifyRuleLhs just sets the flag
490 Example. Consider the following left-hand side of a rule
491 f (x == y) (y > z) = ...
492 If we typecheck this expression we get constraints
493 d1 :: Ord a, d2 :: Eq a
494 We do NOT want to "simplify" to the LHS
495 forall x::a, y::a, z::a, d1::Ord a.
496 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
498 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
499 f ((==) d2 x y) ((>) d1 y z) = ...
501 Here is another example:
502 fromIntegral :: (Integral a, Num b) => a -> b
503 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
504 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
505 we *dont* want to get
507 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
508 because the scsel will mess up RULE matching. Instead we want
509 forall dIntegralInt, dNumInt.
510 fromIntegral Int Int dIntegralInt dNumInt = id Int
513 g (x == y) (y == z) = ..
514 where the two dictionaries are *identical*, we do NOT WANT
515 forall x::a, y::a, z::a, d1::Eq a
516 f ((==) d1 x y) ((>) d1 y z) = ...
517 because that will only match if the dict args are (visibly) equal.
518 Instead we want to quantify over the dictionaries separately.
520 In short, simplifyRuleLhs must *only* squash equalities, leaving
521 all dicts unchanged, with absolutely no sharing.
523 HOWEVER, under a nested implication things are different
525 f :: (forall a. Eq a => a->a) -> Bool -> ...
526 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
529 Here we *must* solve the wanted (Eq a) from the given (Eq a)
530 resulting from skolemising the agument type of g. So we
531 revert to SimplCheck when going under an implication.
534 simplifyRule :: RuleName
535 -> [TcTyVar] -- Explicit skolems
536 -> WantedConstraints -- Constraints from LHS
537 -> WantedConstraints -- Constraints from RHS
538 -> TcM ([EvVar], -- LHS dicts
539 TcEvBinds, -- Evidence for LHS
540 TcEvBinds) -- Evidence for RHS
541 -- See Note [Simplifying RULE lhs constraints]
542 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
543 = do { loc <- getCtLoc (RuleSkol name)
544 ; zonked_lhs <- zonkWC lhs_wanted
545 ; let untch = NoUntouchables
546 -- We allow ourselves to unify environment
547 -- variables; hence *no untouchables*
549 ; (lhs_results, lhs_binds)
550 <- runTcS SimplRuleLhs untch $
551 solveWanteds emptyInert zonked_lhs
553 ; traceTc "simplifyRule" $
554 vcat [ text "zonked_lhs" <+> ppr zonked_lhs
555 , text "lhs_results" <+> ppr lhs_results
556 , text "lhs_binds" <+> ppr lhs_binds
557 , text "rhs_wanted" <+> ppr rhs_wanted ]
560 -- Don't quantify over equalities (judgement call here)
561 ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
562 (wc_flat lhs_results)
563 lhs_dicts = map evVarOf (bagToList dicts)
564 -- Dicts and implicit parameters
566 -- Fail if we have not got down to unsolved flats
567 ; ev_binds_var <- newTcEvBinds
568 ; emitImplication $ Implic { ic_untch = untch
569 , ic_env = emptyNameEnv
570 , ic_skols = mkVarSet tv_bndrs
571 , ic_given = lhs_dicts
572 , ic_wanted = lhs_results { wc_flat = eqs }
573 , ic_insol = insolubleWC lhs_results
574 , ic_binds = ev_binds_var
577 -- Notice that we simplify the RHS with only the explicitly
578 -- introduced skolems, allowing the RHS to constrain any
579 -- unification variables.
580 -- Then, and only then, we call zonkQuantifiedTypeVariables
581 -- Example foo :: Ord a => a -> a
582 -- foo_spec :: Int -> Int
583 -- {-# RULE "foo" foo = foo_spec #-}
584 -- Here, it's the RHS that fixes the type variable
586 -- So we don't want to make untouchable the type
587 -- variables in the envt of the RHS, because they include
588 -- the template variables of the RULE
590 -- Hence the rather painful ad-hoc treatement here
591 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
592 ; rhs_binds1 <- simplifyCheck SimplCheck $
593 WC { wc_flat = emptyBag
594 , wc_insol = emptyBag
595 , wc_impl = unitBag $
596 Implic { ic_untch = NoUntouchables
597 , ic_env = emptyNameEnv
598 , ic_skols = mkVarSet tv_bndrs
599 , ic_given = lhs_dicts
600 , ic_wanted = rhs_wanted
601 , ic_insol = insolubleWC rhs_wanted
602 , ic_binds = rhs_binds_var
604 ; rhs_binds2 <- readTcRef evb_ref
608 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
612 *********************************************************************************
616 ***********************************************************************************
619 simplifyCheck :: SimplContext
620 -> WantedConstraints -- Wanted
622 -- Solve a single, top-level implication constraint
623 -- e.g. typically one created from a top-level type signature
624 -- f :: forall a. [a] -> [a]
626 -- We do this even if the function has no polymorphism:
630 -- (whereas for *nested* bindings we would not create
631 -- an implication constraint for g at all.)
633 -- Fails if can't solve something in the input wanteds
634 simplifyCheck ctxt wanteds
635 = do { wanteds <- zonkWC wanteds
637 ; traceTc "simplifyCheck {" (vcat
638 [ ptext (sLit "wanted =") <+> ppr wanteds ])
640 ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
641 solveWanteds emptyInert wanteds
643 ; traceTc "simplifyCheck }" $
644 ptext (sLit "unsolved =") <+> ppr unsolved
646 ; reportUnsolved unsolved
651 solveWanteds :: InertSet -- Given
653 -> TcS WantedConstraints
654 solveWanteds inert wanted
655 = do { (unsolved_flats, unsolved_implics, insols)
656 <- solve_wanteds inert wanted
657 ; return (WC { wc_flat = keepWanted unsolved_flats -- Discard Derived
658 , wc_impl = unsolved_implics
659 , wc_insol = insols }) }
661 solve_wanteds :: InertSet -- Given
663 -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
664 -- solve_wanteds iterates when it is able to float equalities
665 -- out of one or more of the implications
666 solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
667 = do { traceTcS "solveWanteds {" (ppr wanted)
670 -- Discard from insols all the derived/given constraints
671 -- because they will show up again when we try to solve
672 -- everything else. Solving them a second time is a bit
673 -- of a waste, but the code is simple, and the program is
675 ; let all_flats = flats `unionBags` keepWanted insols
676 ; inert1 <- solveInteractWanted inert (bagToList all_flats)
678 ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
680 ; bb <- getTcEvBindsBag
681 ; tb <- getTcSTyBindsMap
682 ; traceTcS "solveWanteds }" $
683 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
684 , text "unsolved_implics =" <+> ppr unsolved_implics
685 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
686 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
689 ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
690 -- See Note [Solving Family Equations]
691 -- NB: remaining_flats has already had subst applied
693 ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
695 ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
696 , mapBag (substImplication subst) unsolved_implics
697 , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
703 -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
704 simpl_loop n inert implics
706 = trace "solveWanteds: loop" $ -- Always bleat
707 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
708 ; let (_, unsolved_cans) = extractUnsolved inert
709 ; return (unsolved_cans, implics) }
712 = do { traceTcS "solveWanteds: simpl_loop start {" $
713 vcat [ text "n =" <+> ppr n
714 , text "implics =" <+> ppr implics
715 , text "inert =" <+> ppr inert ]
717 ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
718 -- unsolved_cans contains either Wanted or Derived!
720 ; (implic_eqs, unsolved_implics)
721 <- solveNestedImplications just_given_inert unsolved_cans implics
723 -- Apply defaulting rules if and only if there
724 -- no floated equalities. If there are, they may
725 -- solve the remaining wanteds, so don't do defaulting.
726 ; improve_eqs <- if not (isEmptyBag implic_eqs)
727 then return implic_eqs
728 else applyDefaultingRules just_given_inert unsolved_cans
730 ; traceTcS "solveWanteds: simpl_loop end }" $
731 vcat [ text "improve_eqs =" <+> ppr improve_eqs
732 , text "unsolved_flats =" <+> ppr unsolved_cans
733 , text "unsolved_implics =" <+> ppr unsolved_implics ]
735 ; (improve_eqs_already_in_inert, inert_with_improvement)
736 <- solveInteract inert improve_eqs
738 ; if improve_eqs_already_in_inert then
739 return (unsolved_cans, unsolved_implics)
741 simpl_loop (n+1) inert_with_improvement
742 -- Contain unsolved_cans and the improve_eqs
746 givensFromWanteds :: CanonicalCts -> Bag FlavoredEvVar
747 -- Extract the *wanted* ones from CanonicalCts
748 -- and make them into *givens*
749 givensFromWanteds = foldrBag getWanted emptyBag
751 getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
753 | not (isCFrozenErr cc)
754 , Wanted loc <- cc_flavor cc
755 , let given = mkEvVarX (cc_id cc) (Given (setCtLocOrigin loc UnkSkol))
756 = given `consBag` givens
758 = givens -- We are not helping anyone by pushing a Derived in!
759 -- Because if we could not solve it to start with
760 -- we are not going to do either inside the impl constraint
762 solveNestedImplications :: InertSet -> CanonicalCts
764 -> TcS (Bag FlavoredEvVar, Bag Implication)
765 solveNestedImplications just_given_inert unsolved_cans implics
767 = return (emptyBag, emptyBag)
769 = do { -- See Note [Preparing inert set for implications]
770 -- Push the unsolved wanteds inwards, but as givens
771 let pushed_givens = givensFromWanteds unsolved_cans
772 tcs_untouchables = filterVarSet isFlexiTcsTv $
773 tyVarsOfEvVarXs pushed_givens
774 -- See Note [Extra TcsTv untouchables]
776 ; traceTcS "solveWanteds: preparing inerts for implications {"
777 (vcat [ppr tcs_untouchables, ppr pushed_givens])
779 ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
781 ; traceTcS "solveWanteds: } now doing nested implications {" $
782 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
783 , text "implics =" <+> ppr implics ]
785 ; (implic_eqs, unsolved_implics)
786 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
788 ; traceTcS "solveWanteds: done nested implications }" $
789 vcat [ text "implic_eqs =" <+> ppr implic_eqs
790 , text "unsolved_implics =" <+> ppr unsolved_implics ]
792 ; return (implic_eqs, unsolved_implics) }
794 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
796 -> Implication -- Wanted
797 -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
798 Bag Implication) -- Unsolved rest (always empty or singleton)
800 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
801 -- that are of the form unification var = type
803 -- 2. Maybe a unsolved implication, empty if entirely solved!
805 -- Precondition: everything is zonked by now
806 solveImplication tcs_untouchables inert
807 imp@(Implic { ic_untch = untch
808 , ic_binds = ev_binds
811 , ic_wanted = wanteds
813 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
814 recoverTcS (return (emptyBag, emptyBag)) $
815 -- Recover from nested failures. Even the top level is
816 -- just a bunch of implications, so failing at the first
818 do { traceTcS "solveImplication {" (ppr imp)
821 ; given_inert <- solveInteractGiven inert loc givens
823 -- Simplify the wanteds
824 ; (unsolved_flats, unsolved_implics, insols)
825 <- solve_wanteds given_inert wanteds
827 ; let (res_flat_free, res_flat_bound)
828 = floatEqualities skols givens unsolved_flats
829 final_flat = keepWanted res_flat_bound
831 ; let res_wanted = WC { wc_flat = final_flat
832 , wc_impl = unsolved_implics
833 , wc_insol = insols }
834 res_implic = unitImplication $
835 imp { ic_wanted = res_wanted
836 , ic_insol = insolubleWC res_wanted }
838 ; traceTcS "solveImplication end }" $ vcat
839 [ text "res_flat_free =" <+> ppr res_flat_free
840 , text "res_implic =" <+> ppr res_implic ]
842 ; return (res_flat_free, res_implic) }
845 floatEqualities :: TcTyVarSet -> [EvVar]
846 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
847 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
848 -- and come from the input wanted ev vars or deriveds
849 floatEqualities skols can_given wantders
850 | hasEqualities can_given = (emptyBag, wantders)
851 -- Note [Float Equalities out of Implications]
852 | otherwise = partitionBag is_floatable wantders
855 where is_floatable :: FlavoredEvVar -> Bool
856 is_floatable (EvVarX cv _fl)
857 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
858 is_floatable _flev = False
860 tvs_under_fsks :: Type -> TyVarSet
861 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
862 tvs_under_fsks (TyVarTy tv)
863 | not (isTcTyVar tv) = unitVarSet tv
864 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
865 | otherwise = unitVarSet tv
866 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
867 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
868 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
869 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
870 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
871 -- can mention type variables!
872 | isTyVar tv = inner_tvs `delVarSet` tv
873 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
874 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
876 inner_tvs = tvs_under_fsks ty
878 predTvs_under_fsks :: PredType -> TyVarSet
879 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
880 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
881 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
884 Note [Preparing inert set for implications]
885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
886 Before solving the nested implications, we convert any unsolved flat wanteds
887 to givens, and add them to the inert set. Reasons:
889 a) In checking mode, suppresses unnecessary errors. We already have
890 on unsolved-wanted error; adding it to the givens prevents any
891 consequential errors from showing up
893 b) More importantly, in inference mode, we are going to quantify over this
894 constraint, and we *don't* want to quantify over any constraints that
895 are deducible from it.
897 c) Flattened type-family equalities must be exposed to the nested
898 constraints. Consider
899 F b ~ alpha, (forall c. F b ~ alpha)
900 Obviously this is soluble with [alpha := F b]. But the
901 unification is only done by solveCTyFunEqs, right at the end of
902 solveWanteds, and if we aren't careful we'll end up with an
903 unsolved goal inside the implication. We need to "push" the
904 as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
905 can be used to solve the inner (F b
906 ~ alpha). See Trac #4935.
908 d) There are other cases where interactions between wanteds that can help
909 to solve a constraint. For example
913 (C Int alpha), (forall d. C d blah => C Int a)
915 If we push the (C Int alpha) inwards, as a given, it can produce
916 a fundep (alpha~a) and this can float out again and be used to
917 fix alpha. (In general we can't float class constraints out just
918 in case (C d blah) might help to solve (C Int a).)
920 The unsolved wanteds are *canonical* but they may not be *inert*,
921 because when made into a given they might interact with other givens.
922 Hence the call to solveInteract. Example:
924 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
926 We were not able to solve (a ~w [beta]) but we can't just assume it as
927 given because the resulting set is not inert. Hence we have to do a
928 'solveInteract' step first.
930 Note [Extra TcsTv untouchables]
931 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
932 Furthemore, we record the inert set simplifier-generated unification
933 variables of the TcsTv kind (such as variables from instance that have
934 been applied, or unification flattens). These variables must be passed
935 to the implications as extra untouchable variables. Otherwise we have
936 the danger of double unifications. Example (from trac ticket #4494):
938 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
940 In this example, beta is touchable inside the implication. The first
941 solveInteract step leaves 'uf' ununified. Then we move inside the
942 implication where a new constraint
944 emerges. We may spontaneously solve it to get uf := beta, so the whole
945 implication disappears but when we pop out again we are left with (F
946 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
947 uf will get unified *once more* to (F Int).
949 The solution is to record the TcsTvs (i.e. the simplifier-generated
950 unification variables) that are generated when solving the flats, and
951 make them untouchables for the nested implication. In the example
952 above uf would become untouchable, so beta would be forced to be
953 unified as beta := uf.
955 NB: A consequence is that every simplifier-generated TcsTv variable
956 that gets floated out of an implication becomes now untouchable
957 next time we go inside that implication to solve any residual
958 constraints. In effect, by floating an equality out of the
959 implication we are committing to have it solved in the outside.
961 Note [Float Equalities out of Implications]
962 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
963 We want to float equalities out of vanilla existentials, but *not* out
964 of GADT pattern matches.
969 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
970 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
971 -- See Note [Solving Family Equations]
972 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
973 -- where the newly generated equalities (alpha := F xi) have been substituted through.
975 = do { untch <- getUntouchables
976 ; let (unsolved_can_cts, (ni_subst, cv_binds))
977 = getSolvableCTyFunEqs untch cts
978 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
979 , ppr ni_subst, ppr cv_binds
981 ; mapM_ solve_one cv_binds
983 ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
985 solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
988 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
989 -- The TvSubstEnv is not idempotent, but is loop-free
990 -- See Note [Non-idempotent substitution] in Unify
991 emptyFunEqBinds :: FunEqBinds
992 emptyFunEqBinds = (emptyVarEnv, [])
994 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
995 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
996 = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
999 getSolvableCTyFunEqs :: TcsUntouchables
1000 -> CanonicalCts -- Precondition: all Wanteds or Derived!
1001 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
1002 getSolvableCTyFunEqs untch cts
1003 = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
1005 dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
1006 -> (CanonicalCts, FunEqBinds)
1007 dflt_funeq (cts_in, feb@(tv_subst, _))
1008 (CFunEqCan { cc_id = cv
1013 | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
1015 , isTouchableMetaTyVar_InRange untch tv
1016 -- And it's a *touchable* unification variable
1018 , typeKind xi `isSubKind` tyVarKind tv
1019 -- Must do a small kind check since TcCanonical invariants
1020 -- on family equations only impose compatibility, not subkinding
1022 , not (tv `elemVarEnv` tv_subst)
1023 -- Check not in extra_binds
1024 -- See Note [Solving Family Equations], Point 1
1026 , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1027 -- Occurs check: see Note [Solving Family Equations], Point 2
1028 = ASSERT ( not (isGiven fl) )
1029 (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
1031 dflt_funeq (cts_in, fun_eq_binds) ct
1032 = (cts_in `extendCCans` ct, fun_eq_binds)
1035 Note [Solving Family Equations]
1036 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1037 After we are done with simplification we may be left with constraints of the form:
1038 [Wanted] F xis ~ beta
1039 If 'beta' is a touchable unification variable not already bound in the TyBinds
1040 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1042 When is it ok to do so?
1043 1) 'beta' must not already be defaulted to something. Example:
1045 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1046 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1047 have to report this as unsolved.
1049 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1050 set [beta := F xis] only if beta is not among the free variables of xis.
1052 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1053 of type family equations. See Inert Set invariants in TcInteract.
1056 *********************************************************************************
1058 * Defaulting and disamgiguation *
1060 *********************************************************************************
1062 Basic plan behind applyDefaulting rules:
1065 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
1066 For each defaultable group, do:
1067 For each possible substitution for [alpha |-> tau] where `alpha' is the
1068 group's variable, do:
1069 1) Make up new TcEvBinds
1070 2) Extend TcS with (groupVariable
1071 3) given_inert <- solveOne inert (given : a ~ tau)
1072 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1073 5) if unsolved == empty then
1074 sneakyUnify a |-> tau
1075 write the evidence bins
1076 return (final_inert ++ group_constraints,[])
1077 -- will contain the info (alpha |-> tau)!!
1078 goto next defaultable group
1079 if unsolved <> empty then
1080 throw away evidence binds
1081 try next substitution
1082 If you've run out of substitutions for this group, too bad, you failed
1083 return (inert,group)
1084 goto next defaultable group
1087 Collect all the (canonical-cts, wanteds) gathered this way.
1088 - Do a solveGiven over the canonical-cts to make sure they are inert
1089 ------------------------------------------------------------------------------------------
1093 applyDefaultingRules :: InertSet
1094 -> CanonicalCts -- All wanteds
1095 -> TcS (Bag FlavoredEvVar) -- All wanteds again!
1096 -- Return some *extra* givens, which express the
1097 -- type-class-default choice
1099 applyDefaultingRules inert wanteds
1100 | isEmptyBag wanteds
1103 = do { untch <- getUntouchables
1104 ; tv_cts <- mapM (defaultTyVar untch) $
1105 varSetElems (tyVarsOfCDicts wanteds)
1107 ; info@(_, default_tys, _) <- getDefaultInfo
1108 ; let groups = findDefaultableGroups info untch wanteds
1109 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1111 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1112 , text "Type defaults =" <+> ppr deflt_cts])
1114 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1117 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1118 -- defaultTyVar is used on any un-instantiated meta type variables to
1119 -- default the kind of ? and ?? etc to *. This is important to ensure
1120 -- that instance declarations match. For example consider
1121 -- instance Show (a->b)
1122 -- foo x = show (\_ -> True)
1123 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1124 -- and that won't match the typeKind (*) in the instance decl.
1127 -- We look only at touchable type variables. No further constraints
1128 -- are going to affect these type variables, so it's time to do it by
1129 -- hand. However we aren't ready to default them fully to () or
1130 -- whatever, because the type-class defaulting rules have yet to run.
1132 defaultTyVar untch the_tv
1133 | isTouchableMetaTyVar_InRange untch the_tv
1134 , not (k `eqKind` default_k)
1135 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1136 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1137 ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1139 = return emptyBag -- The common case
1141 k = tyVarKind the_tv
1142 default_k = defaultKind k
1146 findDefaultableGroups
1149 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1150 -> TcsUntouchables -- Untouchable
1151 -> CanonicalCts -- Unsolved
1152 -> [[(CanonicalCt,TcTyVar)]]
1153 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1155 | not (performDefaulting ctxt) = []
1156 | null default_tys = []
1157 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1159 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1160 non_unaries :: [CanonicalCt] -- and *other* constraints
1162 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1163 -- Finds unary type-class constraints
1164 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1165 | Just tv <- tcGetTyVar_maybe ty
1167 find_unary cc = Right cc -- Non unary or non dictionary
1169 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1170 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1172 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1174 is_defaultable_group ds@((_,tv):_)
1175 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1176 && not (tv `elemVarSet` bad_tvs)
1177 && isTouchableMetaTyVar_InRange untch tv
1178 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1179 is_defaultable_group [] = panic "defaultable_group"
1181 defaultable_classes clss
1182 | extended_defaults = any isInteractiveClass clss
1183 | otherwise = all is_std_class clss && (any is_num_class clss)
1185 -- In interactive mode, or with -XExtendedDefaultRules,
1186 -- we default Show a to Show () to avoid graututious errors on "show []"
1187 isInteractiveClass cls
1188 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1190 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1191 -- is_num_class adds IsString to the standard numeric classes,
1192 -- when -foverloaded-strings is enabled
1194 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1195 -- Similarly is_std_class
1197 ------------------------------
1198 disambigGroup :: [Type] -- The default types
1199 -> InertSet -- Given inert
1200 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1201 -- sharing same type variable
1202 -> TcS (Bag FlavoredEvVar)
1204 disambigGroup [] _inert _grp
1206 disambigGroup (default_ty:default_tys) inert group
1207 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1208 ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1209 ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1210 derived_eq = mkEvVarX ev der_flav
1212 ; success <- tryTcS $
1213 do { (_,final_inert) <- solveInteract inert $ listToBag $
1214 derived_eq : wanted_ev_vars
1215 ; let (_, unsolved) = extractUnsolved final_inert
1216 ; let wanted_unsolved = filterBag isWantedCt unsolved
1217 -- Don't care about Derived's
1218 ; return (isEmptyBag wanted_unsolved) }
1220 True -> -- Success: record the type variable binding, and return
1221 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1222 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1223 ; return (unitBag derived_eq) }
1224 False -> -- Failure: try with the next type
1225 do { traceTcS "disambigGroup failed, will try other default types"
1227 ; disambigGroup default_tys inert group } }
1229 ((the_ct,the_tv):_) = group
1230 wanteds = map fst group
1231 wanted_ev_vars :: [FlavoredEvVar]
1232 wanted_ev_vars = map deCanonicalise wanteds
1234 mk_derived_flavor :: CtFlavor -> CtFlavor
1235 mk_derived_flavor (Wanted loc) = Derived loc
1236 mk_derived_flavor _ = panic "Asked to disambiguate given or derived!"
1239 Note [Avoiding spurious errors]
1240 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1241 When doing the unification for defaulting, we check for skolem
1242 type variables, and simply don't default them. For example:
1243 f = (*) -- Monomorphic
1244 g :: Num a => a -> a
1246 Here, we get a complaint when checking the type signature for g,
1247 that g isn't polymorphic enough; but then we get another one when
1248 dealing with the (Num a) context arising from f's definition;
1249 we try to unify a with Int (to default it), but find that it's
1250 already been unified with the rigid variable from g's type sig
1254 *********************************************************************************
1258 *********************************************************************************
1261 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1262 newFlatWanteds orig theta
1263 = do { loc <- getCtLoc orig
1264 ; evs <- newWantedEvVars theta
1265 ; return (listToBag [EvVarX w loc | w <- evs]) }