3 simplifyInfer, simplifySuperClass,
4 simplifyDefault, simplifyDeriv, simplifyBracket,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
25 import NameEnv ( emptyNameEnv )
31 import Class ( classKey )
32 import BasicTypes ( RuleName )
33 import Data.List ( partition )
39 *********************************************************************************
41 * External interface *
43 *********************************************************************************
46 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
47 -- Simplify top-level constraints
48 -- Usually these will be implications, when there is
49 -- nothing to quanitfy we don't wrap in a degenerate implication,
50 -- 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 { loc <- getCtLoc DefaultOrigin
64 ; wanted <- newWantedEvVars theta
65 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
66 ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
70 simplifyBracket is used when simplifying the constraints arising from
71 a Template Haskell bracket [| ... |]. We want to check that there aren't
72 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
73 Show instance), but we aren't otherwise interested in the results.
74 Nor do we care about ambiguous dictionaries etc. We will type check
75 this bracket again at its usage site.
78 simplifyBracket :: WantedConstraints -> TcM ()
79 simplifyBracket wanteds
80 = do { zonked_wanteds <- mapBagM zonkWanted wanteds
81 ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
86 *********************************************************************************
90 ***********************************************************************************
93 simplifyDeriv :: CtOrigin
95 -> ThetaType -- Wanted
96 -> TcM ThetaType -- Needed
97 -- Given instance (wanted) => C inst_ty
98 -- Simplify 'wanted' as much as possibles
99 simplifyDeriv orig tvs theta
100 = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
101 -- One reason is that the constraint solving machinery
102 -- expects *TcTyVars* not TyVars. Another is that
103 -- when looking up instances we don't want overlap
106 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
108 ; loc <- getCtLoc orig
109 ; wanted <- newWantedEvVars (substTheta skol_subst theta)
110 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
112 ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
113 ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
115 ; let (good, bad) = partition validDerivPred $
116 foldrBag ((:) . wantedEvVarPred) [] unsolved
117 -- See Note [Exotic derived instance contexts]
118 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
120 ; reportUnsolvedDeriv bad loc
121 ; return $ substTheta subst_skol good }
124 Note [Exotic derived instance contexts]
125 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
126 In a 'derived' instance declaration, we *infer* the context. It's a
127 bit unclear what rules we should apply for this; the Haskell report is
128 silent. Obviously, constraints like (Eq a) are fine, but what about
129 data T f a = MkT (f a) deriving( Eq )
130 where we'd get an Eq (f a) constraint. That's probably fine too.
132 One could go further: consider
133 data T a b c = MkT (Foo a b c) deriving( Eq )
134 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
136 Notice that this instance (just) satisfies the Paterson termination
137 conditions. Then we *could* derive an instance decl like this:
139 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
140 even though there is no instance for (C Int a), because there just
141 *might* be an instance for, say, (C Int Bool) at a site where we
142 need the equality instance for T's.
144 However, this seems pretty exotic, and it's quite tricky to allow
145 this, and yet give sensible error messages in the (much more common)
146 case where we really want that instance decl for C.
148 So for now we simply require that the derived instance context
149 should have only type-variable constraints.
151 Here is another example:
152 data Fix f = In (f (Fix f)) deriving( Eq )
153 Here, if we are prepared to allow -XUndecidableInstances we
154 could derive the instance
155 instance Eq (f (Fix f)) => Eq (Fix f)
156 but this is so delicate that I don't think it should happen inside
157 'deriving'. If you want this, write it yourself!
159 NB: if you want to lift this condition, make sure you still meet the
160 termination conditions! If not, the deriving mechanism generates
161 larger and larger constraints. Example:
163 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
165 Note the lack of a Show instance for Succ. First we'll generate
166 instance (Show (Succ a), Show a) => Show (Seq a)
168 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
169 and so on. Instead we want to complain of no instance for (Show (Succ a)).
173 Allow constraints which consist only of type variables, with no repeats.
175 *********************************************************************************
179 ***********************************************************************************
182 simplifyInfer :: Bool -- Apply monomorphism restriction
183 -> TcTyVarSet -- These type variables are free in the
184 -- types to be generalised
186 -> TcM ([TcTyVar], -- Quantify over these type variables
187 [EvVar], -- ... and these constraints
188 TcEvBinds) -- ... binding these evidence variables
189 simplifyInfer apply_mr tau_tvs wanted
190 | isEmptyBag wanted -- Trivial case is quite common
191 = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
192 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
193 ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
194 ; return (qtvs, [], emptyTcEvBinds) }
197 = do { zonked_wanted <- mapBagM zonkWanted wanted
198 ; traceTc "simplifyInfer {" $ vcat
199 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
200 , ptext (sLit "wanted =") <+> ppr zonked_wanted
201 , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
204 -- Make a guess at the quantified type variables
205 -- Then split the constraints on the baisis of those tyvars
206 -- to avoid unnecessarily simplifying a class constraint
207 -- See Note [Avoid unecessary constraint simplification]
208 ; gbl_tvs <- tcGetGlobalTyVars
209 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
210 ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
211 zonked_tau_tvs `minusVarSet` gbl_tvs
212 (perhaps_bound, surely_free)
213 = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
215 ; emitConstraints surely_free
216 ; traceTc "sinf" $ vcat
217 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
218 , ptext (sLit "surely_free =") <+> ppr surely_free
221 -- Now simplify the possibly-bound constraints
222 ; (simplified_perhaps_bound, tc_binds)
223 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
225 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
226 -- may have done some unification
227 ; gbl_tvs <- tcGetGlobalTyVars
228 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
229 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
230 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
231 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
232 constrained_tvs = tyVarsOfWantedEvVars zonked_simples
233 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
234 (final_qtvs, (bound, free))
235 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
236 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
238 ; traceTc "end simplifyInfer }" $
239 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
240 , text "wanted = " <+> ppr zonked_wanted
241 , text "qtvs = " <+> ppr final_qtvs
242 , text "free = " <+> ppr free
243 , text "bound = " <+> ppr bound ]
245 -- Turn the quantified meta-type variables into real type variables
246 ; emitConstraints (mapBag WcEvVar free)
247 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
248 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
249 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
251 ------------------------
252 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
253 -> TcM (Bag WantedEvVar, Bag EvBind)
254 -- We use this function when inferring the type of a function
255 -- The wanted constraints are already zonked
256 simplifyAsMuchAsPossible ctxt wanteds
257 = do { let untch = NoUntouchables
258 -- We allow ourselves to unify environment
259 -- variables; hence *no untouchables*
261 ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
262 <- runTcS ctxt untch $
263 simplifyApproxLoop 0 wanteds
266 ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors
268 ; return (unsolved_flats, ev_binds) }
271 simplifyApproxLoop :: Int -> WantedConstraints
272 -> TcS (Bag WantedEvVar, Bag Implication)
273 simplifyApproxLoop n wanteds
275 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
277 = do { traceTcS "simplifyApproxLoop" (vcat
278 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
279 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
281 ; let (extra_flats, thiner_unsolved_implics)
282 = approximateImplications unsolved_implics
284 = Bag.mapBag WcEvVar unsolved_flats `unionBags`
285 Bag.mapBag WcImplic thiner_unsolved_implics
287 ; -- If no new work was produced then we are done with simplifyApproxLoop
288 if isEmptyBag extra_flats
289 then do { traceTcS "simplifyApproxLoopRes" (vcat
290 [ ptext (sLit "Wanted = ") <+> ppr wanteds
291 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
292 ; return (unsolved_flats, unsolved_implics) }
294 else -- Produced new flat work wanteds, go round the loop
295 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
298 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
299 -- (wc1, impls2) <- approximateImplications impls
300 -- splits 'impls' into two parts
301 -- wc1: a bag of constraints that do not mention any skolems
302 -- impls2: a bag of *thiner* implication constraints
303 approximateImplications impls
304 = splitBag (do_implic emptyVarSet) impls
307 do_wanted :: TcTyVarSet -> WantedConstraint
308 -> (WantedConstraints, WantedConstraints)
309 do_wanted skols (WcImplic impl)
310 = let (fl_w, mb_impl) = do_implic skols impl
311 in (fl_w, mapBag WcImplic mb_impl)
312 do_wanted skols wc@(WcEvVar wev)
313 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
314 | otherwise = (emptyBag, unitBag wc)
317 do_implic :: TcTyVarSet -> Implication
318 -> (WantedConstraints, Bag Implication)
319 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
320 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
321 else unitBag impl{ ic_wanted = rest_wanted } )
323 (floatable_wanted, rest_wanted)
324 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
327 splitBag :: (a -> (WantedConstraints, Bag a))
328 -> Bag a -> (WantedConstraints, Bag a)
329 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
332 = (wcs `unionBags` b1, imps `unionBags` b2)
338 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
339 growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
340 growWanteds gbl_tvs ws tvs
341 | isEmptyBag ws = tvs
342 | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
343 growWantedEVs gbl_tvs ws tvs
344 | isEmptyBag ws = tvs
345 | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
347 growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet
348 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
349 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
350 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
351 -- X-constraint 'wanted', nuking the 'gbls' at each stage
353 growEvVar gbl_tvs ev tvs
354 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
356 ev_tvs = growPredTyVars (evVarPred ev) tvs
358 growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
360 growWanted gbl_tvs (WcEvVar wev) tvs
361 = growWantedEV gbl_tvs wev tvs
362 growWanted gbl_tvs (WcImplic implic) tvs
363 = foldrBag (growWanted inner_gbl_tvs)
364 (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
365 -- Must grow over inner givens too
368 inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
371 quantifyMe :: TyVarSet -- Quantifying over these
373 -> Bool -- True <=> quantify over this wanted
375 | isIPPred pred = True -- Note [Inheriting implicit parameters]
376 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
378 pred = wantedEvVarPred wev
380 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
381 -- False => we can *definitely* float the WantedConstraint out
382 quantifyMeWC qtvs (WcImplic implic)
383 = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
384 || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
386 inner_qtvs = qtvs `minusVarSet` ic_skols implic
388 quantifyMeWC qtvs (WcEvVar wev)
389 = quantifyMe qtvs wev
392 Note [Avoid unecessary constraint simplification]
393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
394 When inferring the type of a let-binding, with simplifyInfer,
395 try to avoid unnecessariliy simplifying class constraints.
396 Doing so aids sharing, but it also helps with delicate
398 instance C t => C [t] where ..
400 f x = let g y = ...(constraint C [t])...
402 When inferring a type for 'g', we don't want to apply the
403 instance decl, because then we can't satisfy (C t). So we
404 just notice that g isn't quantified over 't' and partition
405 the contraints before simplifying.
407 This only half-works, but then let-generalisation only half-works.
410 Note [Inheriting implicit parameters]
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
416 where f is *not* a top-level binding.
417 From the RHS of f we'll get the constraint (?y::Int).
418 There are two types we might infer for f:
422 (so we get ?y from the context of f's definition), or
424 f :: (?y::Int) => Int -> Int
426 At first you might think the first was better, becuase then
427 ?y behaves like a free variable of the definition, rather than
428 having to be passed at each call site. But of course, the WHOLE
429 IDEA is that ?y should be passed at each call site (that's what
430 dynamic binding means) so we'd better infer the second.
432 BOTTOM LINE: when *inferring types* you *must* quantify
433 over implicit parameters. See the predicate isFreeWhenInferring.
436 *********************************************************************************
440 ***********************************************************************************
442 When constructing evidence for superclasses in an instance declaration,
443 * we MUST have the "self" dictionary available, but
444 * we must NOT have its superclasses derived from "self"
446 Moreover, we must *completely* solve the constraints right now,
447 not wrap them in an implication constraint to solve later. Why?
448 Because when that implication constraint is solved there may
449 be some unrelated other solved top-level constraints that
450 recursively depend on the superclass we are building. Consider
451 class Ord a => C a where
452 instance C [Int] where ...
455 dCListInt = MkC $cNum ...
457 $cNum :: Ord [Int] -- The superclass
458 $cNum = let self = dCListInt in <solve Ord [Int]>
460 Now, if there is some *other* top-level constraint solved
464 we must not solve the (Ord [Int]) wanted from foo!!
467 simplifySuperClass :: EvVar -- The "self" dictionary
470 simplifySuperClass self wanteds
471 = do { wanteds <- mapBagM zonkWanted wanteds
472 ; loc <- getCtLoc NoScSkol
473 ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds)
474 <- runTcS SimplCheck NoUntouchables $
475 do { can_self <- canGivens loc [self]
476 ; let inert = foldlBag updInertSet emptyInert can_self
477 -- No need for solveInteract; we know it's inert
479 ; solveWanteds inert wanteds }
481 ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
482 reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors }
486 *********************************************************************************
490 ***********************************************************************************
492 Note [Simplifying RULE lhs constraints]
493 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
494 On the LHS of transformation rules we only simplify only equalitis,
495 but not dictionaries. We want to keep dictionaries unsimplified, to
496 serve as the available stuff for the RHS of the rule. We *do* want to
497 simplify equalities, however, to detect ill-typed rules that cannot be
500 Implementation: the TcSFlags carried by the TcSMonad controls the
501 amount of simplification, so simplifyRuleLhs just sets the flag
504 Example. Consider the following left-hand side of a rule
505 f (x == y) (y > z) = ...
506 If we typecheck this expression we get constraints
507 d1 :: Ord a, d2 :: Eq a
508 We do NOT want to "simplify" to the LHS
509 forall x::a, y::a, z::a, d1::Ord a.
510 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
512 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
513 f ((==) d2 x y) ((>) d1 y z) = ...
515 Here is another example:
516 fromIntegral :: (Integral a, Num b) => a -> b
517 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
518 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
519 we *dont* want to get
521 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
522 because the scsel will mess up RULE matching. Instead we want
523 forall dIntegralInt, dNumInt.
524 fromIntegral Int Int dIntegralInt dNumInt = id Int
527 g (x == y) (y == z) = ..
528 where the two dictionaries are *identical*, we do NOT WANT
529 forall x::a, y::a, z::a, d1::Eq a
530 f ((==) d1 x y) ((>) d1 y z) = ...
531 because that will only match if the dict args are (visibly) equal.
532 Instead we want to quantify over the dictionaries separately.
534 In short, simplifyRuleLhs must *only* squash equalities, leaving
535 all dicts unchanged, with absolutely no sharing.
537 HOWEVER, under a nested implication things are different
539 f :: (forall a. Eq a => a->a) -> Bool -> ...
540 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
543 Here we *must* solve the wanted (Eq a) from the given (Eq a)
544 resulting from skolemising the agument type of g. So we
545 revert to SimplCheck when going under an implication.
548 simplifyRule :: RuleName
549 -> [TcTyVar] -- Explicit skolems
550 -> WantedConstraints -- Constraints from LHS
551 -> WantedConstraints -- Constraints from RHS
552 -> TcM ([EvVar], -- LHS dicts
553 TcEvBinds, -- Evidence for LHS
554 TcEvBinds) -- Evidence for RHS
555 -- See Note [Simplifying RULE lhs constraints]
556 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
557 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
558 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
560 -- Don't quantify over equalities (judgement call here)
561 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
562 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
563 -- Dicts and implicit parameters
564 ; reportUnsolvedWantedEvVars eqs
566 -- Notice that we simplify the RHS with only the explicitly
567 -- introduced skolems, allowing the RHS to constrain any
568 -- unification variables.
569 -- Then, and only then, we call zonkQuantifiedTypeVariables
570 -- Example foo :: Ord a => a -> a
571 -- foo_spec :: Int -> Int
572 -- {-# RULE "foo" foo = foo_spec #-}
573 -- Here, it's the RHS that fixes the type variable
575 -- So we don't want to make untouchable the type
576 -- variables in the envt of the RHS, because they include
577 -- the template variables of the RULE
579 -- Hence the rather painful ad-hoc treatement here
580 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
581 ; loc <- getCtLoc (RuleSkol name)
582 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
583 Implic { ic_untch = NoUntouchables
584 , ic_env = emptyNameEnv
585 , ic_skols = mkVarSet tv_bndrs
586 , ic_scoped = panic "emitImplication"
587 , ic_given = lhs_dicts
588 , ic_wanted = rhs_wanted
589 , ic_binds = rhs_binds_var
591 ; rhs_binds2 <- readTcRef evb_ref
595 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
599 *********************************************************************************
603 ***********************************************************************************
606 simplifyCheck :: SimplContext
607 -> WantedConstraints -- Wanted
609 -- Solve a single, top-level implication constraint
610 -- e.g. typically one created from a top-level type signature
611 -- f :: forall a. [a] -> [a]
613 -- We do this even if the function has no polymorphism:
617 -- (whereas for *nested* bindings we would not create
618 -- an implication constraint for g at all.)
620 -- Fails if can't solve something in the input wanteds
621 simplifyCheck ctxt wanteds
622 = do { wanteds <- mapBagM zonkWanted wanteds
624 ; traceTc "simplifyCheck {" (vcat
625 [ ptext (sLit "wanted =") <+> ppr wanteds ])
627 ; (unsolved, frozen_errors, ev_binds)
628 <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
630 ; traceTc "simplifyCheck }" $
631 ptext (sLit "unsolved =") <+> ppr unsolved
633 ; reportUnsolved unsolved frozen_errors
638 solveWanteds :: InertSet -- Given
639 -> WantedConstraints -- Wanted
640 -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why
641 -- they are WantedConstraints and not CanonicalCts
642 Bag Implication) -- Unsolved implications
643 -- solveWanteds iterates when it is able to float equalities
644 -- out of one or more of the implications
645 solveWanteds inert wanteds
646 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
647 ; can_flats <- canWanteds $ bagToList flat_wanteds
648 ; traceTcS "solveWanteds {" $
649 vcat [ text "wanteds =" <+> ppr wanteds
650 , text "inert =" <+> ppr inert ]
651 ; (unsolved_flats, unsolved_implics)
652 <- simpl_loop 1 inert can_flats implic_wanteds
653 ; bb <- getTcEvBindsBag
654 ; tb <- getTcSTyBindsMap
655 ; traceTcS "solveWanteds }" $
656 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
657 , text "unsolved_implics =" <+> ppr unsolved_implics
658 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
659 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
662 ; solveCTyFunEqs unsolved_flats unsolved_implics
663 -- See Note [Solving Family Equations]
668 -> CanonicalCts -- May inlude givens (in the recursive call)
670 -> TcS (CanonicalCts, Bag Implication)
671 simpl_loop n inert can_ws implics
673 = trace "solveWanteds: loop" $ -- Always bleat
674 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
675 ; return (can_ws, implics) }
678 = do { traceTcS "solveWanteds: simpl_loop start {" $
679 vcat [ text "n =" <+> ppr n
680 , text "can_ws =" <+> ppr can_ws
681 , text "implics =" <+> ppr implics
682 , text "inert =" <+> ppr inert ]
683 ; inert1 <- solveInteract inert can_ws
684 ; let (inert2, unsolved_flats) = extractUnsolved inert1
686 -- NB: Importantly, inerts2 may contain *more* givens than inert
687 -- because of having solved equalities from can_ws
688 ; traceTcS "solveWanteds: done flats" $
689 vcat [ text "inerts =" <+> ppr inert2
690 , text "unsolved =" <+> ppr unsolved_flats ]
692 -- Go inside each implication
693 ; (implic_eqs, unsolved_implics)
694 <- solveNestedImplications inert2 unsolved_flats implics
696 -- Apply defaulting rules if and only if there
697 -- no floated equalities. If there are, they may
698 -- solve the remaining wanteds, so don't do defaulting.
699 ; final_eqs <- if not (isEmptyBag implic_eqs)
700 then return implic_eqs
701 else applyDefaultingRules inert2 unsolved_flats
703 -- default_eqs are *givens*, so simpl_loop may
704 -- recurse with givens in the argument
706 ; traceTcS "solveWanteds: simpl_loop end }" $
707 vcat [ text "final_eqs =" <+> ppr final_eqs
708 , text "unsolved_flats =" <+> ppr unsolved_flats
709 , text "unsolved_implics =" <+> ppr unsolved_implics ]
711 ; if isEmptyBag final_eqs then
712 return (unsolved_flats, unsolved_implics)
714 do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
715 -- final eqs is *just* a bunch of WantedEvVars
716 ; simpl_loop (n+1) inert2
717 (can_final_eqs `andCCan` unsolved_flats) unsolved_implics
718 -- Important: reiterate with inert2, not plainly inert
719 -- because inert2 may contain more givens, as the result of solving
720 -- some wanteds in the incoming can_ws
724 solveNestedImplications :: InertSet -> CanonicalCts -> Bag Implication
725 -> TcS (Bag WantedEvVar, Bag Implication)
726 solveNestedImplications inerts unsolved implics
728 = return (emptyBag, emptyBag)
730 = do { -- See Note [Preparing inert set for implications]
731 traceTcS "solveWanteds: preparing inerts for implications {" empty
732 ; inert_for_implics <- solveInteract inerts (makeGivens unsolved)
735 ; traceTcS "solveWanteds: doing nested implications {" $
736 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
737 , text "implics =" <+> ppr implics ]
739 ; let tcs_untouchables = filterVarSet isFlexiTcsTv $
740 tyVarsOfInert inert_for_implics
741 -- See Note [Extra TcsTv untouchables]
742 ; (implic_eqs, unsolved_implics)
743 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
745 ; traceTcS "solveWanteds: done nested implications }" $
746 vcat [ text "implic_eqs =" <+> ppr implic_eqs
747 , text "unsolved_implics =" <+> ppr unsolved_implics ]
749 ; return (implic_eqs, unsolved_implics) }
751 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
753 -> Implication -- Wanted
754 -> TcS (Bag WantedEvVar, -- Unsolved unification var = type
755 Bag Implication) -- Unsolved rest (always empty or singleton)
757 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
758 -- that are of the form unification var = type
760 -- 2. Maybe a unsolved implication, empty if entirely solved!
762 -- Precondition: everything is zonked by now
763 solveImplication tcs_untouchables inert
764 imp@(Implic { ic_untch = untch
765 , ic_binds = ev_binds
768 , ic_wanted = wanteds
770 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
771 recoverTcS (return (emptyBag, emptyBag)) $
772 -- Recover from nested failures. Even the top level is
773 -- just a bunch of implications, so failing at the first
775 do { traceTcS "solveImplication {" (ppr imp)
778 ; can_givens <- canGivens loc givens
779 ; given_inert <- solveInteract inert can_givens
781 -- Simplify the wanteds
782 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
784 ; let (res_flat_free, res_flat_bound)
785 = floatEqualities skols givens unsolved_flats
786 unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
787 Bag.mapBag WcImplic unsolved_implics
789 ; traceTcS "solveImplication end }" $ vcat
790 [ text "res_flat_free =" <+> ppr res_flat_free
791 , text "res_flat_bound =" <+> ppr res_flat_bound
792 , text "unsolved_implics =" <+> ppr unsolved_implics ]
794 ; let res_bag | isEmptyBag unsolved = emptyBag
795 | otherwise = unitBag (imp { ic_wanted = unsolved })
797 ; return (res_flat_free, res_bag) }
799 floatEqualities :: TcTyVarSet -> [EvVar]
800 -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
801 -- The CanonicalCts will be floated out to be used later, whereas
802 -- the remaining WantedEvVars will remain inside the implication.
803 floatEqualities skols can_given wanteds
804 | hasEqualities can_given = (emptyBag, wanteds)
805 -- Note [Float Equalities out of Implications]
806 | otherwise = partitionBag is_floatable wanteds
807 where is_floatable :: WantedEvVar -> Bool
808 is_floatable (WantedEvVar cv _)
809 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
810 is_floatable _wv = False
812 tvs_under_fsks :: Type -> TyVarSet
813 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
814 tvs_under_fsks (TyVarTy tv)
815 | not (isTcTyVar tv) = unitVarSet tv
816 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
817 | otherwise = unitVarSet tv
818 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
819 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
820 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
821 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
822 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
823 -- can mention type variables!
824 | isTyVar tv = inner_tvs `delVarSet` tv
825 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
826 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
828 inner_tvs = tvs_under_fsks ty
830 predTvs_under_fsks :: PredType -> TyVarSet
831 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
832 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
833 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
840 Note [Float Equalities out of Implications]
841 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
842 We want to float equalities out of vanilla existentials, but *not* out
843 of GADT pattern matches.
845 Note [Preparing inert set for implications]
846 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
847 Before solving the nested implications, we convert any unsolved flat wanteds
848 to givens, and add them to the inert set. Reasons:
850 a) In checking mode, suppresses unnecessary errors. We already have
851 on unsolved-wanted error; adding it to the givens prevents any
852 consequential errors from showing uop
854 b) More importantly, in inference mode, we are going to quantify over this
855 constraint, and we *don't* want to quantify over any constraints that
856 are deducible from it.
858 The unsolved wanteds are *canonical* but they may not be *inert*,
859 because when made into a given they might interact with other givens.
860 Hence the call to solveInteract. Example:
862 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
864 We were not able to solve (a ~w [beta]) but we can't just assume it as
865 given because the resulting set is not inert. Hence we have to do a
866 'solveInteract' step first.
868 Note [Extra TcsTv untouchables]
869 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
870 Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv
871 kind (such as variables from instance that have been applied, or unification flattens). These
872 variables must be passed to the implications as extra untouchable variables. Otherwise
873 we have the danger of double unifications. Example (from trac ticket #4494):
875 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
877 In this example, beta is touchable inside the implication. The first solveInteract step
878 leaves 'uf' ununified. Then we move inside the implication where a new constraint
880 emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears
881 but when we pop out again we are left with (F Int ~ uf) which will be unified by our final
882 solveCTyFunEqs stage and uf will get unified *once more* to (F Int).
884 The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables)
885 that are generated when solving the flats, and make them untouchables for the nested
886 implication. In the example above uf would become untouchable, so beta would be forced to
887 be unified as beta := uf.
889 NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out
890 of an implication becomes now untouchable next time we go inside that implication to
891 solve any residual constraints. In effect, by floating an equality out of the implication
892 we are committing to have it solved in the outside.
897 solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
898 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
899 -- See Note [Solving Family Equations]
900 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
901 -- where the newly generated equalities (alpha := F xi) have been substituted through.
902 solveCTyFunEqs cts implics
903 = do { untch <- getUntouchables
904 ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
905 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
908 ; mapM_ solve_one funeq_bnds
910 -- Apply the substitution through to eliminate the flatten
911 -- unification variables we substituted both in the unsolved flats and implics
913 = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
915 = Bag.mapBag (subst_impl funeq_bnds) implics
917 ; return (final_unsolved, final_implics) }
919 where solve_one (tv,(ty,cv,fl))
920 | not (typeKind ty `isSubKind` tyVarKind tv)
921 = addErrorTcS KindError fl (mkTyVarTy tv) ty
922 -- Must do a small kind check since TcCanonical invariants
923 -- on family equations only impose compatibility, not subkinding
924 | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
926 subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
927 subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv)
928 subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
930 subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
931 subst_wevar funeq_bnds (WantedEvVar v loc)
932 = let orig_ty = varType v
933 new_ty = substFunEqBnds funeq_bnds orig_ty
934 in WantedEvVar (setVarType v new_ty) loc
936 subst_impl :: FunEqBinds -> Implication -> Implication
937 subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
938 = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
941 type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
942 -- Invariant: if it contains:
943 -- [... a -> (ta,...) ... b -> (tb,...) ... ]
944 -- then 'ta' cannot mention 'b'
946 getSolvableCTyFunEqs :: TcsUntouchables
947 -> CanonicalCts -- Precondition: all wanteds
948 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
949 getSolvableCTyFunEqs untch cts
950 = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
951 where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
956 | Just tv <- tcGetTyVar_maybe xi
957 , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
958 , Nothing <- lookup tv extra_binds -- or in extra_binds
959 -- See Note [Solving Family Equations], Point 1
960 = ASSERT ( isWanted fl )
961 let ty_orig = mkTyConApp tc xis
962 ty_bind = substFunEqBnds extra_binds ty_orig
963 in if tv `elemVarSet` tyVarsOfType ty_bind
964 then (cts_in `extendCCans` ct, extra_binds)
965 -- See Note [Solving Family Equations], Point 2
966 else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
967 -- Postcondition met because extra_binds is already applied to ty_bind
969 dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
971 substFunEqBnds :: FunEqBinds -> TcType -> TcType
972 substFunEqBnds bnds ty
973 = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
974 -- foldr works because of the FunEqBinds invariant
979 Note [Solving Family Equations]
980 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
981 After we are done with simplification we may be left with constraints of the form:
982 [Wanted] F xis ~ beta
983 If 'beta' is a touchable unification variable not already bound in the TyBinds
984 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
986 When is it ok to do so?
987 1) 'beta' must not already be defaulted to something. Example:
989 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
990 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
991 have to report this as unsolved.
993 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
994 set [beta := F xis] only if beta is not among the free variables of xis.
996 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
997 of type family equations. See Inert Set invariants in TcInteract.
1000 *********************************************************************************
1002 * Defaulting and disamgiguation *
1004 *********************************************************************************
1006 Basic plan behind applyDefaulting rules:
1009 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
1010 For each defaultable group, do:
1011 For each possible substitution for [alpha |-> tau] where `alpha' is the
1012 group's variable, do:
1013 1) Make up new TcEvBinds
1014 2) Extend TcS with (groupVariable
1015 3) given_inert <- solveOne inert (given : a ~ tau)
1016 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1017 5) if unsolved == empty then
1018 sneakyUnify a |-> tau
1019 write the evidence bins
1020 return (final_inert ++ group_constraints,[])
1021 -- will contain the info (alpha |-> tau)!!
1022 goto next defaultable group
1023 if unsolved <> empty then
1024 throw away evidence binds
1025 try next substitution
1026 If you've run out of substitutions for this group, too bad, you failed
1027 return (inert,group)
1028 goto next defaultable group
1031 Collect all the (canonical-cts, wanteds) gathered this way.
1032 - Do a solveGiven over the canonical-cts to make sure they are inert
1033 ------------------------------------------------------------------------------------------
1037 applyDefaultingRules :: InertSet
1038 -> CanonicalCts -- All wanteds
1039 -> TcS (Bag WantedEvVar) -- All wanteds again!
1040 -- Return some *extra* givens, which express the
1041 -- type-class-default choice
1043 applyDefaultingRules inert wanteds
1044 | isEmptyBag wanteds
1047 = do { untch <- getUntouchables
1048 ; tv_cts <- mapM (defaultTyVar untch) $
1049 varSetElems (tyVarsOfCDicts wanteds)
1051 ; info@(_, default_tys, _) <- getDefaultInfo
1052 ; let groups = findDefaultableGroups info untch wanteds
1053 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1055 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1056 , text "Type defaults =" <+> ppr deflt_cts])
1058 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1061 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar)
1062 -- defaultTyVar is used on any un-instantiated meta type variables to
1063 -- default the kind of ? and ?? etc to *. This is important to ensure
1064 -- that instance declarations match. For example consider
1065 -- instance Show (a->b)
1066 -- foo x = show (\_ -> True)
1067 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1068 -- and that won't match the typeKind (*) in the instance decl.
1071 -- We look only at touchable type variables. No further constraints
1072 -- are going to affect these type variables, so it's time to do it by
1073 -- hand. However we aren't ready to default them fully to () or
1074 -- whatever, because the type-class defaulting rules have yet to run.
1076 defaultTyVar untch the_tv
1077 | isTouchableMetaTyVar_InRange untch the_tv
1078 , not (k `eqKind` default_k)
1079 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1080 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1081 ; return (unitBag (WantedEvVar ev loc)) }
1083 = return emptyBag -- The common case
1085 k = tyVarKind the_tv
1086 default_k = defaultKind k
1090 findDefaultableGroups
1093 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1094 -> TcsUntouchables -- Untouchable
1095 -> CanonicalCts -- Unsolved
1096 -> [[(CanonicalCt,TcTyVar)]]
1097 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1099 | not (performDefaulting ctxt) = []
1100 | null default_tys = []
1101 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1103 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1104 non_unaries :: [CanonicalCt] -- and *other* constraints
1106 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1107 -- Finds unary type-class constraints
1108 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1109 | Just tv <- tcGetTyVar_maybe ty
1111 find_unary cc = Right cc -- Non unary or non dictionary
1113 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1114 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1116 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1118 is_defaultable_group ds@((_,tv):_)
1119 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1120 && not (tv `elemVarSet` bad_tvs)
1121 && isTouchableMetaTyVar_InRange untch tv
1122 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1123 is_defaultable_group [] = panic "defaultable_group"
1125 defaultable_classes clss
1126 | extended_defaults = any isInteractiveClass clss
1127 | otherwise = all is_std_class clss && (any is_num_class clss)
1129 -- In interactive mode, or with -XExtendedDefaultRules,
1130 -- we default Show a to Show () to avoid graututious errors on "show []"
1131 isInteractiveClass cls
1132 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1134 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1135 -- is_num_class adds IsString to the standard numeric classes,
1136 -- when -foverloaded-strings is enabled
1138 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1139 -- Similarly is_std_class
1141 ------------------------------
1142 disambigGroup :: [Type] -- The default types
1143 -> InertSet -- Given inert
1144 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1145 -- sharing same type variable
1146 -> TcS (Bag WantedEvVar)
1148 disambigGroup [] _inert _grp
1150 disambigGroup (default_ty:default_tys) inert group
1151 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1152 ; let ct_loc = get_ct_loc (cc_flavor the_ct)
1153 ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
1154 ; let wanted_eq = CTyEqCan { cc_id = ev
1155 , cc_flavor = Wanted ct_loc
1157 , cc_rhs = default_ty }
1158 ; success <- tryTcS $
1159 do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
1160 ; let (_, unsolved) = extractUnsolved final_inert
1161 ; errs <- getTcSErrorsBag
1162 ; return (isEmptyBag unsolved && isEmptyBag errs) }
1165 True -> -- Success: record the type variable binding, and return
1166 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1167 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1168 ; return (unitBag $ WantedEvVar ev ct_loc) }
1169 False -> -- Failure: try with the next type
1170 do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
1171 ; disambigGroup default_tys inert group } }
1173 ((the_ct,the_tv):_) = group
1174 wanteds = map fst group
1175 wanted_ev_vars = map deCanonicaliseWanted wanteds
1177 get_ct_loc (Wanted l) = l
1178 get_ct_loc _ = panic "Asked to disambiguate given or derived!"
1183 Note [Avoiding spurious errors]
1184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1185 When doing the unification for defaulting, we check for skolem
1186 type variables, and simply don't default them. For example:
1187 f = (*) -- Monomorphic
1188 g :: Num a => a -> a
1190 Here, we get a complaint when checking the type signature for g,
1191 that g isn't polymorphic enough; but then we get another one when
1192 dealing with the (Num a) context arising from f's definition;
1193 we try to unify a with Int (to default it), but find that it's
1194 already been unified with the rigid variable from g's type sig