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 :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar
751 -- Extract the Wanted ones from CanonicalCts and conver to
752 -- Givens; not Given/Solved, see Note [Preparing inert set for implications]
753 givensFromWanteds _ctxt = foldrBag getWanted emptyBag
755 getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
758 = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol)
759 in given `consBag` givens -- and not mkSolvedFlavor,
760 -- see Note [Preparing inert set for implications]
763 pushable_wanted :: CanonicalCt -> Bool
765 | not (isCFrozenErr cc)
767 = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
770 solveNestedImplications :: InertSet -> CanonicalCts
772 -> TcS (Bag FlavoredEvVar, Bag Implication)
773 solveNestedImplications just_given_inert unsolved_cans implics
775 = return (emptyBag, emptyBag)
777 = do { -- See Note [Preparing inert set for implications]
778 -- Push the unsolved wanteds inwards, but as givens
780 ; simpl_ctx <- getTcSContext
782 ; let pushed_givens = givensFromWanteds simpl_ctx unsolved_cans
783 tcs_untouchables = filterVarSet isFlexiTcsTv $
784 tyVarsOfEvVarXs pushed_givens
785 -- See Note [Extra TcsTv untouchables]
787 ; traceTcS "solveWanteds: preparing inerts for implications {"
788 (vcat [ppr tcs_untouchables, ppr pushed_givens])
790 ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
792 ; traceTcS "solveWanteds: } now doing nested implications {" $
793 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
794 , text "implics =" <+> ppr implics ]
796 ; (implic_eqs, unsolved_implics)
797 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
799 ; traceTcS "solveWanteds: done nested implications }" $
800 vcat [ text "implic_eqs =" <+> ppr implic_eqs
801 , text "unsolved_implics =" <+> ppr unsolved_implics ]
803 ; return (implic_eqs, unsolved_implics) }
805 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
807 -> Implication -- Wanted
808 -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
809 Bag Implication) -- Unsolved rest (always empty or singleton)
811 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
812 -- that are of the form unification var = type
814 -- 2. Maybe a unsolved implication, empty if entirely solved!
816 -- Precondition: everything is zonked by now
817 solveImplication tcs_untouchables inert
818 imp@(Implic { ic_untch = untch
819 , ic_binds = ev_binds
822 , ic_wanted = wanteds
824 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
825 recoverTcS (return (emptyBag, emptyBag)) $
826 -- Recover from nested failures. Even the top level is
827 -- just a bunch of implications, so failing at the first
829 do { traceTcS "solveImplication {" (ppr imp)
832 ; given_inert <- solveInteractGiven inert loc givens
834 -- Simplify the wanteds
835 ; (unsolved_flats, unsolved_implics, insols)
836 <- solve_wanteds given_inert wanteds
838 ; let (res_flat_free, res_flat_bound)
839 = floatEqualities skols givens unsolved_flats
840 final_flat = keepWanted res_flat_bound
842 ; let res_wanted = WC { wc_flat = final_flat
843 , wc_impl = unsolved_implics
844 , wc_insol = insols }
845 res_implic = unitImplication $
846 imp { ic_wanted = res_wanted
847 , ic_insol = insolubleWC res_wanted }
849 ; traceTcS "solveImplication end }" $ vcat
850 [ text "res_flat_free =" <+> ppr res_flat_free
851 , text "res_implic =" <+> ppr res_implic ]
853 ; return (res_flat_free, res_implic) }
856 floatEqualities :: TcTyVarSet -> [EvVar]
857 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
858 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
859 -- and come from the input wanted ev vars or deriveds
860 floatEqualities skols can_given wantders
861 | hasEqualities can_given = (emptyBag, wantders)
862 -- Note [Float Equalities out of Implications]
863 | otherwise = partitionBag is_floatable wantders
866 where is_floatable :: FlavoredEvVar -> Bool
867 is_floatable (EvVarX cv _fl)
868 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
869 is_floatable _flev = False
871 tvs_under_fsks :: Type -> TyVarSet
872 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
873 tvs_under_fsks (TyVarTy tv)
874 | not (isTcTyVar tv) = unitVarSet tv
875 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
876 | otherwise = unitVarSet tv
877 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
878 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
879 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
880 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
881 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
882 -- can mention type variables!
883 | isTyVar tv = inner_tvs `delVarSet` tv
884 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
885 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
887 inner_tvs = tvs_under_fsks ty
889 predTvs_under_fsks :: PredType -> TyVarSet
890 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
891 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
892 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
895 Note [Preparing inert set for implications]
896 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
897 Before solving the nested implications, we convert any unsolved flat wanteds
898 to givens, and add them to the inert set. Reasons:
900 a) In checking mode, suppresses unnecessary errors. We already have
901 on unsolved-wanted error; adding it to the givens prevents any
902 consequential errors from showing up
904 b) More importantly, in inference mode, we are going to quantify over this
905 constraint, and we *don't* want to quantify over any constraints that
906 are deducible from it.
908 c) Flattened type-family equalities must be exposed to the nested
909 constraints. Consider
910 F b ~ alpha, (forall c. F b ~ alpha)
911 Obviously this is soluble with [alpha := F b]. But the
912 unification is only done by solveCTyFunEqs, right at the end of
913 solveWanteds, and if we aren't careful we'll end up with an
914 unsolved goal inside the implication. We need to "push" the
915 as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
916 can be used to solve the inner (F b
917 ~ alpha). See Trac #4935.
919 d) There are other cases where interactions between wanteds that can help
920 to solve a constraint. For example
924 (C Int alpha), (forall d. C d blah => C Int a)
926 If we push the (C Int alpha) inwards, as a given, it can produce
927 a fundep (alpha~a) and this can float out again and be used to
928 fix alpha. (In general we can't float class constraints out just
929 in case (C d blah) might help to solve (C Int a).)
931 The unsolved wanteds are *canonical* but they may not be *inert*,
932 because when made into a given they might interact with other givens.
933 Hence the call to solveInteract. Example:
935 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
937 We were not able to solve (a ~w [beta]) but we can't just assume it as
938 given because the resulting set is not inert. Hence we have to do a
939 'solveInteract' step first.
941 Finally, note that we convert them to [Given] and NOT [Given/Solved].
942 The reason is that Given/Solved are weaker than Givens and may be discarded.
943 As an example consider the inference case, where we may have, the following
944 original constraints:
946 (F Int ~ a => F Int ~ a)
947 If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next
948 given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting
949 the (F Int ~ a) insoluble. Hence we should really convert the residual
950 wanteds to plain old Given.
952 We need only push in unsolved equalities both in checking mode and inference mode:
954 (1) In checking mode we should not push given dictionaries in because of
955 example LongWayOverlapping.hs, where we might get strange overlap
956 errors between far-away constraints in the program. But even in
957 checking mode, we must still push type family equations. Consider:
959 type instance F True a b = a
960 type instance F False a b = b
963 (c ~ True) => a ~ gamma
964 (c ~ False) => b ~ gamma
966 Since solveCTyFunEqs happens at the very end of solving, the only way to solve
967 the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not
968 merely Given/Solved because it has to interact with the top-level instance
969 environment) and push it inside the implications. Now, when we come out again at
970 the end, having solved the implications solveCTyFunEqs will solve this equality.
972 (2) In inference mode, we recheck the final constraint in checking mode and
973 hence we will be able to solve inner implications from top-level quantified
974 constraints nonetheless.
977 Note [Extra TcsTv untouchables]
978 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
979 Furthemore, we record the inert set simplifier-generated unification
980 variables of the TcsTv kind (such as variables from instance that have
981 been applied, or unification flattens). These variables must be passed
982 to the implications as extra untouchable variables. Otherwise we have
983 the danger of double unifications. Example (from trac ticket #4494):
985 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
987 In this example, beta is touchable inside the implication. The first
988 solveInteract step leaves 'uf' ununified. Then we move inside the
989 implication where a new constraint
991 emerges. We may spontaneously solve it to get uf := beta, so the whole
992 implication disappears but when we pop out again we are left with (F
993 Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
994 uf will get unified *once more* to (F Int).
996 The solution is to record the TcsTvs (i.e. the simplifier-generated
997 unification variables) that are generated when solving the flats, and
998 make them untouchables for the nested implication. In the example
999 above uf would become untouchable, so beta would be forced to be
1000 unified as beta := uf.
1002 NB: A consequence is that every simplifier-generated TcsTv variable
1003 that gets floated out of an implication becomes now untouchable
1004 next time we go inside that implication to solve any residual
1005 constraints. In effect, by floating an equality out of the
1006 implication we are committing to have it solved in the outside.
1008 Note [Float Equalities out of Implications]
1009 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1010 We want to float equalities out of vanilla existentials, but *not* out
1011 of GADT pattern matches.
1016 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
1017 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
1018 -- See Note [Solving Family Equations]
1019 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
1020 -- where the newly generated equalities (alpha := F xi) have been substituted through.
1022 = do { untch <- getUntouchables
1023 ; let (unsolved_can_cts, (ni_subst, cv_binds))
1024 = getSolvableCTyFunEqs untch cts
1025 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
1026 , ppr ni_subst, ppr cv_binds
1028 ; mapM_ solve_one cv_binds
1030 ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
1032 solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
1035 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
1036 -- The TvSubstEnv is not idempotent, but is loop-free
1037 -- See Note [Non-idempotent substitution] in Unify
1038 emptyFunEqBinds :: FunEqBinds
1039 emptyFunEqBinds = (emptyVarEnv, [])
1041 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
1042 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
1043 = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
1046 getSolvableCTyFunEqs :: TcsUntouchables
1047 -> CanonicalCts -- Precondition: all Wanteds or Derived!
1048 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
1049 getSolvableCTyFunEqs untch cts
1050 = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
1052 dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
1053 -> (CanonicalCts, FunEqBinds)
1054 dflt_funeq (cts_in, feb@(tv_subst, _))
1055 (CFunEqCan { cc_id = cv
1060 | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
1062 , isTouchableMetaTyVar_InRange untch tv
1063 -- And it's a *touchable* unification variable
1065 , typeKind xi `isSubKind` tyVarKind tv
1066 -- Must do a small kind check since TcCanonical invariants
1067 -- on family equations only impose compatibility, not subkinding
1069 , not (tv `elemVarEnv` tv_subst)
1070 -- Check not in extra_binds
1071 -- See Note [Solving Family Equations], Point 1
1073 , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
1074 -- Occurs check: see Note [Solving Family Equations], Point 2
1075 = ASSERT ( not (isGivenOrSolved fl) )
1076 (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
1078 dflt_funeq (cts_in, fun_eq_binds) ct
1079 = (cts_in `extendCCans` ct, fun_eq_binds)
1082 Note [Solving Family Equations]
1083 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1084 After we are done with simplification we may be left with constraints of the form:
1085 [Wanted] F xis ~ beta
1086 If 'beta' is a touchable unification variable not already bound in the TyBinds
1087 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
1089 When is it ok to do so?
1090 1) 'beta' must not already be defaulted to something. Example:
1092 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
1093 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
1094 have to report this as unsolved.
1096 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
1097 set [beta := F xis] only if beta is not among the free variables of xis.
1099 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
1100 of type family equations. See Inert Set invariants in TcInteract.
1103 *********************************************************************************
1105 * Defaulting and disamgiguation *
1107 *********************************************************************************
1109 Basic plan behind applyDefaulting rules:
1112 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
1113 For each defaultable group, do:
1114 For each possible substitution for [alpha |-> tau] where `alpha' is the
1115 group's variable, do:
1116 1) Make up new TcEvBinds
1117 2) Extend TcS with (groupVariable
1118 3) given_inert <- solveOne inert (given : a ~ tau)
1119 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1120 5) if unsolved == empty then
1121 sneakyUnify a |-> tau
1122 write the evidence bins
1123 return (final_inert ++ group_constraints,[])
1124 -- will contain the info (alpha |-> tau)!!
1125 goto next defaultable group
1126 if unsolved <> empty then
1127 throw away evidence binds
1128 try next substitution
1129 If you've run out of substitutions for this group, too bad, you failed
1130 return (inert,group)
1131 goto next defaultable group
1134 Collect all the (canonical-cts, wanteds) gathered this way.
1135 - Do a solveGiven over the canonical-cts to make sure they are inert
1136 ------------------------------------------------------------------------------------------
1140 applyDefaultingRules :: InertSet
1141 -> CanonicalCts -- All wanteds
1142 -> TcS (Bag FlavoredEvVar) -- All wanteds again!
1143 -- Return some *extra* givens, which express the
1144 -- type-class-default choice
1146 applyDefaultingRules inert wanteds
1147 | isEmptyBag wanteds
1150 = do { untch <- getUntouchables
1151 ; tv_cts <- mapM (defaultTyVar untch) $
1152 varSetElems (tyVarsOfCDicts wanteds)
1154 ; info@(_, default_tys, _) <- getDefaultInfo
1155 ; let groups = findDefaultableGroups info untch wanteds
1156 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1158 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1159 , text "Type defaults =" <+> ppr deflt_cts])
1161 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1164 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1165 -- defaultTyVar is used on any un-instantiated meta type variables to
1166 -- default the kind of ? and ?? etc to *. This is important to ensure
1167 -- that instance declarations match. For example consider
1168 -- instance Show (a->b)
1169 -- foo x = show (\_ -> True)
1170 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1171 -- and that won't match the typeKind (*) in the instance decl.
1174 -- We look only at touchable type variables. No further constraints
1175 -- are going to affect these type variables, so it's time to do it by
1176 -- hand. However we aren't ready to default them fully to () or
1177 -- whatever, because the type-class defaulting rules have yet to run.
1179 defaultTyVar untch the_tv
1180 | isTouchableMetaTyVar_InRange untch the_tv
1181 , not (k `eqKind` default_k)
1182 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1183 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1184 ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1186 = return emptyBag -- The common case
1188 k = tyVarKind the_tv
1189 default_k = defaultKind k
1193 findDefaultableGroups
1196 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1197 -> TcsUntouchables -- Untouchable
1198 -> CanonicalCts -- Unsolved
1199 -> [[(CanonicalCt,TcTyVar)]]
1200 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1202 | not (performDefaulting ctxt) = []
1203 | null default_tys = []
1204 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1206 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1207 non_unaries :: [CanonicalCt] -- and *other* constraints
1209 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1210 -- Finds unary type-class constraints
1211 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1212 | Just tv <- tcGetTyVar_maybe ty
1214 find_unary cc = Right cc -- Non unary or non dictionary
1216 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1217 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1219 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1221 is_defaultable_group ds@((_,tv):_)
1222 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1223 && not (tv `elemVarSet` bad_tvs)
1224 && isTouchableMetaTyVar_InRange untch tv
1225 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1226 is_defaultable_group [] = panic "defaultable_group"
1228 defaultable_classes clss
1229 | extended_defaults = any isInteractiveClass clss
1230 | otherwise = all is_std_class clss && (any is_num_class clss)
1232 -- In interactive mode, or with -XExtendedDefaultRules,
1233 -- we default Show a to Show () to avoid graututious errors on "show []"
1234 isInteractiveClass cls
1235 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1237 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1238 -- is_num_class adds IsString to the standard numeric classes,
1239 -- when -foverloaded-strings is enabled
1241 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1242 -- Similarly is_std_class
1244 ------------------------------
1245 disambigGroup :: [Type] -- The default types
1246 -> InertSet -- Given inert
1247 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1248 -- sharing same type variable
1249 -> TcS (Bag FlavoredEvVar)
1251 disambigGroup [] _inert _grp
1253 disambigGroup (default_ty:default_tys) inert group
1254 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1255 ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1256 ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1257 derived_eq = mkEvVarX ev der_flav
1259 ; success <- tryTcS $
1260 do { (_,final_inert) <- solveInteract inert $ listToBag $
1261 derived_eq : wanted_ev_vars
1262 ; let (_, unsolved) = extractUnsolved final_inert
1263 ; let wanted_unsolved = filterBag isWantedCt unsolved
1264 -- Don't care about Derived's
1265 ; return (isEmptyBag wanted_unsolved) }
1267 True -> -- Success: record the type variable binding, and return
1268 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1269 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1270 ; return (unitBag derived_eq) }
1271 False -> -- Failure: try with the next type
1272 do { traceTcS "disambigGroup failed, will try other default types"
1274 ; disambigGroup default_tys inert group } }
1276 ((the_ct,the_tv):_) = group
1277 wanteds = map fst group
1278 wanted_ev_vars :: [FlavoredEvVar]
1279 wanted_ev_vars = map deCanonicalise wanteds
1281 mk_derived_flavor :: CtFlavor -> CtFlavor
1282 mk_derived_flavor (Wanted loc) = Derived loc
1283 mk_derived_flavor _ = panic "Asked to disambiguate given or derived!"
1286 Note [Avoiding spurious errors]
1287 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1288 When doing the unification for defaulting, we check for skolem
1289 type variables, and simply don't default them. For example:
1290 f = (*) -- Monomorphic
1291 g :: Num a => a -> a
1293 Here, we get a complaint when checking the type signature for g,
1294 that g isn't polymorphic enough; but then we get another one when
1295 dealing with the (Num a) context arising from f's definition;
1296 we try to unify a with Int (to default it), but find that it's
1297 already been unified with the rigid variable from g's type sig
1301 *********************************************************************************
1305 *********************************************************************************
1308 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1309 newFlatWanteds orig theta
1310 = do { loc <- getCtLoc orig
1311 ; evs <- newWantedEvVars theta
1312 ; return (listToBag [EvVarX w loc | w <- evs]) }