4 simplifyDefault, simplifyDeriv, simplifyBracket,
5 simplifyRule, simplifyTop, simplifyInteractive
8 #include "HsVersions.h"
24 import NameEnv ( emptyNameEnv )
30 import Class ( classKey )
31 import BasicTypes ( RuleName )
32 import Data.List ( partition )
38 *********************************************************************************
40 * External interface *
42 *********************************************************************************
45 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
46 -- Simplify top-level constraints
47 -- Usually these will be implications,
48 -- but when there is nothing to quantify we don't wrap
49 -- in a degenerate implication, so we do that here instead
51 = simplifyCheck SimplCheck wanteds
54 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
55 simplifyInteractive wanteds
56 = simplifyCheck SimplInteractive wanteds
59 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
60 -> TcM () -- Succeeds iff the constraint is soluble
62 = do { loc <- getCtLoc DefaultOrigin
63 ; wanted <- newWantedEvVars theta
64 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
65 ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
69 simplifyBracket is used when simplifying the constraints arising from
70 a Template Haskell bracket [| ... |]. We want to check that there aren't
71 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
72 Show instance), but we aren't otherwise interested in the results.
73 Nor do we care about ambiguous dictionaries etc. We will type check
74 this bracket again at its usage site.
77 simplifyBracket :: WantedConstraints -> TcM ()
78 simplifyBracket wanteds
79 = do { zonked_wanteds <- mapBagM zonkWanted wanteds
80 ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
85 *********************************************************************************
89 ***********************************************************************************
92 simplifyDeriv :: CtOrigin
94 -> ThetaType -- Wanted
95 -> TcM ThetaType -- Needed
96 -- Given instance (wanted) => C inst_ty
97 -- Simplify 'wanted' as much as possibles
98 simplifyDeriv orig tvs theta
99 = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
100 -- One reason is that the constraint solving machinery
101 -- expects *TcTyVars* not TyVars. Another is that
102 -- when looking up instances we don't want overlap
105 ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
107 ; loc <- getCtLoc orig
108 ; wanted <- newWantedEvVars (substTheta skol_subst theta)
109 ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
111 ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
112 ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
114 ; let (good, bad) = partition validDerivPred $
115 foldrBag ((:) . wantedEvVarPred) [] unsolved
116 -- See Note [Exotic derived instance contexts]
117 subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
119 ; reportUnsolvedDeriv bad loc
120 ; return $ substTheta subst_skol good }
123 Note [Exotic derived instance contexts]
124 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
125 In a 'derived' instance declaration, we *infer* the context. It's a
126 bit unclear what rules we should apply for this; the Haskell report is
127 silent. Obviously, constraints like (Eq a) are fine, but what about
128 data T f a = MkT (f a) deriving( Eq )
129 where we'd get an Eq (f a) constraint. That's probably fine too.
131 One could go further: consider
132 data T a b c = MkT (Foo a b c) deriving( Eq )
133 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
135 Notice that this instance (just) satisfies the Paterson termination
136 conditions. Then we *could* derive an instance decl like this:
138 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
139 even though there is no instance for (C Int a), because there just
140 *might* be an instance for, say, (C Int Bool) at a site where we
141 need the equality instance for T's.
143 However, this seems pretty exotic, and it's quite tricky to allow
144 this, and yet give sensible error messages in the (much more common)
145 case where we really want that instance decl for C.
147 So for now we simply require that the derived instance context
148 should have only type-variable constraints.
150 Here is another example:
151 data Fix f = In (f (Fix f)) deriving( Eq )
152 Here, if we are prepared to allow -XUndecidableInstances we
153 could derive the instance
154 instance Eq (f (Fix f)) => Eq (Fix f)
155 but this is so delicate that I don't think it should happen inside
156 'deriving'. If you want this, write it yourself!
158 NB: if you want to lift this condition, make sure you still meet the
159 termination conditions! If not, the deriving mechanism generates
160 larger and larger constraints. Example:
162 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
164 Note the lack of a Show instance for Succ. First we'll generate
165 instance (Show (Succ a), Show a) => Show (Seq a)
167 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
168 and so on. Instead we want to complain of no instance for (Show (Succ a)).
172 Allow constraints which consist only of type variables, with no repeats.
174 *********************************************************************************
178 ***********************************************************************************
181 simplifyInfer :: Bool -- Apply monomorphism restriction
182 -> TcTyVarSet -- These type variables are free in the
183 -- types to be generalised
185 -> TcM ([TcTyVar], -- Quantify over these type variables
186 [EvVar], -- ... and these constraints
187 TcEvBinds) -- ... binding these evidence variables
188 simplifyInfer apply_mr tau_tvs wanted
189 | isEmptyBag wanted -- Trivial case is quite common
190 = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
191 ; gbl_tvs <- tcGetGlobalTyVars -- Already zonked
192 ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
193 ; return (qtvs, [], emptyTcEvBinds) }
196 = do { zonked_wanted <- mapBagM zonkWanted wanted
197 ; traceTc "simplifyInfer {" $ vcat
198 [ ptext (sLit "apply_mr =") <+> ppr apply_mr
199 , ptext (sLit "wanted =") <+> ppr zonked_wanted
200 , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
203 -- Make a guess at the quantified type variables
204 -- Then split the constraints on the baisis of those tyvars
205 -- to avoid unnecessarily simplifying a class constraint
206 -- See Note [Avoid unecessary constraint simplification]
207 ; gbl_tvs <- tcGetGlobalTyVars
208 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
209 ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
210 zonked_tau_tvs `minusVarSet` gbl_tvs
211 (perhaps_bound, surely_free)
212 = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
214 ; emitConstraints surely_free
215 ; traceTc "sinf" $ vcat
216 [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
217 , ptext (sLit "surely_free =") <+> ppr surely_free
220 -- Now simplify the possibly-bound constraints
221 ; (simplified_perhaps_bound, tc_binds)
222 <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
224 -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
225 -- may have done some unification
226 ; gbl_tvs <- tcGetGlobalTyVars
227 ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
228 ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
229 ; let init_tvs = zonked_tau_tvs `minusVarSet` gbl_tvs
230 mr_qtvs = init_tvs `minusVarSet` constrained_tvs
231 constrained_tvs = tyVarsOfWantedEvVars zonked_simples
232 qtvs = growWantedEVs gbl_tvs zonked_simples init_tvs
233 (final_qtvs, (bound, free))
234 | apply_mr = (mr_qtvs, (emptyBag, zonked_simples))
235 | otherwise = (qtvs, partitionBag (quantifyMe qtvs) zonked_simples)
237 ; traceTc "end simplifyInfer }" $
238 vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
239 , text "wanted = " <+> ppr zonked_wanted
240 , text "qtvs = " <+> ppr final_qtvs
241 , text "free = " <+> ppr free
242 , text "bound = " <+> ppr bound ]
244 -- Turn the quantified meta-type variables into real type variables
245 ; emitConstraints (mapBag WcEvVar free)
246 ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
247 ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
248 ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
250 ------------------------
251 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
252 -> TcM (Bag WantedEvVar, Bag EvBind)
253 -- We use this function when inferring the type of a function
254 -- The wanted constraints are already zonked
255 simplifyAsMuchAsPossible ctxt wanteds
256 = do { let untch = NoUntouchables
257 -- We allow ourselves to unify environment
258 -- variables; hence *no untouchables*
260 ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
261 <- runTcS ctxt untch $
262 simplifyApproxLoop 0 wanteds
265 ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors
267 ; return (unsolved_flats, ev_binds) }
270 simplifyApproxLoop :: Int -> WantedConstraints
271 -> TcS (Bag WantedEvVar, Bag Implication)
272 simplifyApproxLoop n wanteds
274 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
276 = do { traceTcS "simplifyApproxLoop" (vcat
277 [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
278 ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
280 ; let (extra_flats, thiner_unsolved_implics)
281 = approximateImplications unsolved_implics
283 = Bag.mapBag WcEvVar unsolved_flats `unionBags`
284 Bag.mapBag WcImplic thiner_unsolved_implics
286 ; -- If no new work was produced then we are done with simplifyApproxLoop
287 if isEmptyBag extra_flats
288 then do { traceTcS "simplifyApproxLoopRes" (vcat
289 [ ptext (sLit "Wanted = ") <+> ppr wanteds
290 , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
291 ; return (unsolved_flats, unsolved_implics) }
293 else -- Produced new flat work wanteds, go round the loop
294 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
297 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
298 -- (wc1, impls2) <- approximateImplications impls
299 -- splits 'impls' into two parts
300 -- wc1: a bag of constraints that do not mention any skolems
301 -- impls2: a bag of *thiner* implication constraints
302 approximateImplications impls
303 = splitBag (do_implic emptyVarSet) impls
306 do_wanted :: TcTyVarSet -> WantedConstraint
307 -> (WantedConstraints, WantedConstraints)
308 do_wanted skols (WcImplic impl)
309 = let (fl_w, mb_impl) = do_implic skols impl
310 in (fl_w, mapBag WcImplic mb_impl)
311 do_wanted skols wc@(WcEvVar wev)
312 | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
313 | otherwise = (emptyBag, unitBag wc)
316 do_implic :: TcTyVarSet -> Implication
317 -> (WantedConstraints, Bag Implication)
318 do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
319 = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
320 else unitBag impl{ ic_wanted = rest_wanted } )
322 (floatable_wanted, rest_wanted)
323 = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
326 splitBag :: (a -> (WantedConstraints, Bag a))
327 -> Bag a -> (WantedConstraints, Bag a)
328 splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
331 = (wcs `unionBags` b1, imps `unionBags` b2)
337 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
338 growWanteds :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
339 growWanteds gbl_tvs ws tvs
340 | isEmptyBag ws = tvs
341 | otherwise = fixVarSet (\tvs -> foldrBag (growWanted gbl_tvs) tvs ws) tvs
342 growWantedEVs gbl_tvs ws tvs
343 | isEmptyBag ws = tvs
344 | otherwise = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
346 growEvVar :: TyVarSet -> EvVar -> TyVarSet -> TyVarSet
347 growWantedEV :: TyVarSet -> WantedEvVar -> TyVarSet -> TyVarSet
348 growWanted :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
349 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
350 -- X-constraint 'wanted', nuking the 'gbls' at each stage
352 growEvVar gbl_tvs ev tvs
353 = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
355 ev_tvs = growPredTyVars (evVarPred ev) tvs
357 growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
359 growWanted gbl_tvs (WcEvVar wev) tvs
360 = growWantedEV gbl_tvs wev tvs
361 growWanted gbl_tvs (WcImplic implic) tvs
362 = foldrBag (growWanted inner_gbl_tvs)
363 (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
364 -- Must grow over inner givens too
367 inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
370 quantifyMe :: TyVarSet -- Quantifying over these
372 -> Bool -- True <=> quantify over this wanted
374 | isIPPred pred = True -- Note [Inheriting implicit parameters]
375 | otherwise = tyVarsOfPred pred `intersectsVarSet` qtvs
377 pred = wantedEvVarPred wev
379 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
380 -- False => we can *definitely* float the WantedConstraint out
381 quantifyMeWC qtvs (WcImplic implic)
382 = (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
383 || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
385 inner_qtvs = qtvs `minusVarSet` ic_skols implic
387 quantifyMeWC qtvs (WcEvVar wev)
388 = quantifyMe qtvs wev
391 Note [Avoid unecessary constraint simplification]
392 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
393 When inferring the type of a let-binding, with simplifyInfer,
394 try to avoid unnecessariliy simplifying class constraints.
395 Doing so aids sharing, but it also helps with delicate
397 instance C t => C [t] where ..
399 f x = let g y = ...(constraint C [t])...
401 When inferring a type for 'g', we don't want to apply the
402 instance decl, because then we can't satisfy (C t). So we
403 just notice that g isn't quantified over 't' and partition
404 the contraints before simplifying.
406 This only half-works, but then let-generalisation only half-works.
409 Note [Inheriting implicit parameters]
410 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
415 where f is *not* a top-level binding.
416 From the RHS of f we'll get the constraint (?y::Int).
417 There are two types we might infer for f:
421 (so we get ?y from the context of f's definition), or
423 f :: (?y::Int) => Int -> Int
425 At first you might think the first was better, becuase then
426 ?y behaves like a free variable of the definition, rather than
427 having to be passed at each call site. But of course, the WHOLE
428 IDEA is that ?y should be passed at each call site (that's what
429 dynamic binding means) so we'd better infer the second.
431 BOTTOM LINE: when *inferring types* you *must* quantify
432 over implicit parameters. See the predicate isFreeWhenInferring.
435 *********************************************************************************
439 ***********************************************************************************
441 Note [Simplifying RULE lhs constraints]
442 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
443 On the LHS of transformation rules we only simplify only equalities,
444 but not dictionaries. We want to keep dictionaries unsimplified, to
445 serve as the available stuff for the RHS of the rule. We *do* want to
446 simplify equalities, however, to detect ill-typed rules that cannot be
449 Implementation: the TcSFlags carried by the TcSMonad controls the
450 amount of simplification, so simplifyRuleLhs just sets the flag
453 Example. Consider the following left-hand side of a rule
454 f (x == y) (y > z) = ...
455 If we typecheck this expression we get constraints
456 d1 :: Ord a, d2 :: Eq a
457 We do NOT want to "simplify" to the LHS
458 forall x::a, y::a, z::a, d1::Ord a.
459 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
461 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
462 f ((==) d2 x y) ((>) d1 y z) = ...
464 Here is another example:
465 fromIntegral :: (Integral a, Num b) => a -> b
466 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
467 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
468 we *dont* want to get
470 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
471 because the scsel will mess up RULE matching. Instead we want
472 forall dIntegralInt, dNumInt.
473 fromIntegral Int Int dIntegralInt dNumInt = id Int
476 g (x == y) (y == z) = ..
477 where the two dictionaries are *identical*, we do NOT WANT
478 forall x::a, y::a, z::a, d1::Eq a
479 f ((==) d1 x y) ((>) d1 y z) = ...
480 because that will only match if the dict args are (visibly) equal.
481 Instead we want to quantify over the dictionaries separately.
483 In short, simplifyRuleLhs must *only* squash equalities, leaving
484 all dicts unchanged, with absolutely no sharing.
486 HOWEVER, under a nested implication things are different
488 f :: (forall a. Eq a => a->a) -> Bool -> ...
489 {-# RULES "foo" forall (v::forall b. Eq b => b->b).
492 Here we *must* solve the wanted (Eq a) from the given (Eq a)
493 resulting from skolemising the agument type of g. So we
494 revert to SimplCheck when going under an implication.
497 simplifyRule :: RuleName
498 -> [TcTyVar] -- Explicit skolems
499 -> WantedConstraints -- Constraints from LHS
500 -> WantedConstraints -- Constraints from RHS
501 -> TcM ([EvVar], -- LHS dicts
502 TcEvBinds, -- Evidence for LHS
503 TcEvBinds) -- Evidence for RHS
504 -- See Note [Simplifying RULE lhs constraints]
505 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
506 = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
507 ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
509 -- Don't quantify over equalities (judgement call here)
510 ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
511 lhs_dicts = map wantedEvVarToVar (bagToList dicts)
512 -- Dicts and implicit parameters
513 ; reportUnsolvedWantedEvVars eqs
515 -- Notice that we simplify the RHS with only the explicitly
516 -- introduced skolems, allowing the RHS to constrain any
517 -- unification variables.
518 -- Then, and only then, we call zonkQuantifiedTypeVariables
519 -- Example foo :: Ord a => a -> a
520 -- foo_spec :: Int -> Int
521 -- {-# RULE "foo" foo = foo_spec #-}
522 -- Here, it's the RHS that fixes the type variable
524 -- So we don't want to make untouchable the type
525 -- variables in the envt of the RHS, because they include
526 -- the template variables of the RULE
528 -- Hence the rather painful ad-hoc treatement here
529 ; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
530 ; loc <- getCtLoc (RuleSkol name)
531 ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
532 Implic { ic_untch = NoUntouchables
533 , ic_env = emptyNameEnv
534 , ic_skols = mkVarSet tv_bndrs
535 , ic_scoped = panic "emitImplication"
536 , ic_given = lhs_dicts
537 , ic_wanted = rhs_wanted
538 , ic_binds = rhs_binds_var
540 ; rhs_binds2 <- readTcRef evb_ref
544 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
548 *********************************************************************************
552 ***********************************************************************************
555 simplifyCheck :: SimplContext
556 -> WantedConstraints -- Wanted
558 -- Solve a single, top-level implication constraint
559 -- e.g. typically one created from a top-level type signature
560 -- f :: forall a. [a] -> [a]
562 -- We do this even if the function has no polymorphism:
566 -- (whereas for *nested* bindings we would not create
567 -- an implication constraint for g at all.)
569 -- Fails if can't solve something in the input wanteds
570 simplifyCheck ctxt wanteds
571 = do { wanteds <- mapBagM zonkWanted wanteds
573 ; traceTc "simplifyCheck {" (vcat
574 [ ptext (sLit "wanted =") <+> ppr wanteds ])
576 ; (unsolved, frozen_errors, ev_binds)
577 <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
579 ; traceTc "simplifyCheck }" $
580 ptext (sLit "unsolved =") <+> ppr unsolved
582 ; reportUnsolved unsolved frozen_errors
587 solveWanteds :: InertSet -- Given
588 -> WantedConstraints -- Wanted
589 -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why
590 -- they are WantedConstraints and not CanonicalCts
591 Bag Implication) -- Unsolved implications
592 -- solveWanteds iterates when it is able to float equalities
593 -- out of one or more of the implications
594 solveWanteds inert wanteds
595 = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
596 ; traceTcS "solveWanteds {" $
597 vcat [ text "wanteds =" <+> ppr wanteds
598 , text "inert =" <+> ppr inert ]
599 ; (unsolved_flats, unsolved_implics)
600 <- simpl_loop 1 inert flat_wanteds implic_wanteds
601 ; bb <- getTcEvBindsBag
602 ; tb <- getTcSTyBindsMap
603 ; traceTcS "solveWanteds }" $
604 vcat [ text "unsolved_flats =" <+> ppr unsolved_flats
605 , text "unsolved_implics =" <+> ppr unsolved_implics
606 , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
607 , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb))
610 ; solveCTyFunEqs unsolved_flats unsolved_implics
611 -- See Note [Solving Family Equations]
618 -> TcS (CanonicalCts, Bag Implication)
619 simpl_loop n inert work_items implics
621 = trace "solveWanteds: loop" $ -- Always bleat
622 do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively
624 -- We don't want to call the canonicalizer on those wanted ev vars
625 -- so try one last time to solveInteract them
626 ; inert1 <- solveInteract inert $
627 mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items
628 ; let (_, unsolved_cans) = extractUnsolved inert1
629 ; return (unsolved_cans, implics) }
632 = do { traceTcS "solveWanteds: simpl_loop start {" $
633 vcat [ text "n =" <+> ppr n
634 , text "work_items =" <+> ppr work_items
635 , text "implics =" <+> ppr implics
636 , text "inert =" <+> ppr inert ]
637 ; inert1 <- solveInteract inert $
638 mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items
639 ; let (inert2, unsolved_cans) = extractUnsolved inert1
641 = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans
643 -- NB: Importantly, inerts2 may contain *more* givens than inert
644 -- because of having solved equalities from can_ws
645 ; traceTcS "solveWanteds: done flats" $
646 vcat [ text "inerts =" <+> ppr inert2
647 , text "unsolved =" <+> ppr unsolved_cans ]
649 -- Go inside each implication
650 ; (implic_eqs, unsolved_implics)
651 <- solveNestedImplications inert2 unsolved_wevvars implics
653 -- Apply defaulting rules if and only if there
654 -- no floated equalities. If there are, they may
655 -- solve the remaining wanteds, so don't do defaulting.
656 ; final_eqs <- if not (isEmptyBag implic_eqs)
657 then return implic_eqs
658 else applyDefaultingRules inert2 unsolved_cans
660 ; traceTcS "solveWanteds: simpl_loop end }" $
661 vcat [ text "final_eqs =" <+> ppr final_eqs
662 , text "unsolved_flats =" <+> ppr unsolved_cans
663 , text "unsolved_implics =" <+> ppr unsolved_implics ]
665 ; if isEmptyBag final_eqs then
666 return (unsolved_cans, unsolved_implics)
668 simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars
669 (final_eqs `unionBags` unsolved_wevvars) unsolved_implics
670 -- Important: reiterate with inert2, not plainly inert
671 -- because inert2 may contain more givens, as the result of solving
672 -- some wanteds in the incoming can_ws
675 solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
676 -> TcS (Bag WantedEvVar, Bag Implication)
677 solveNestedImplications inerts unsolved implics
679 = return (emptyBag, emptyBag)
681 = do { -- See Note [Preparing inert set for implications]
682 traceTcS "solveWanteds: preparing inerts for implications {" empty
683 ; inert_for_implics <- solveInteract inerts (makeGivens unsolved)
686 ; traceTcS "solveWanteds: doing nested implications {" $
687 vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
688 , text "implics =" <+> ppr implics ]
690 ; let tcs_untouchables = filterVarSet isFlexiTcsTv $
691 tyVarsOfInert inert_for_implics
692 -- See Note [Extra TcsTv untouchables]
693 ; (implic_eqs, unsolved_implics)
694 <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
696 ; traceTcS "solveWanteds: done nested implications }" $
697 vcat [ text "implic_eqs =" <+> ppr implic_eqs
698 , text "unsolved_implics =" <+> ppr unsolved_implics ]
700 ; return (implic_eqs, unsolved_implics) }
702 solveImplication :: TcTyVarSet -- Untouchable TcS unification variables
704 -> Implication -- Wanted
705 -> TcS (Bag WantedEvVar, -- Unsolved unification var = type
706 Bag Implication) -- Unsolved rest (always empty or singleton)
708 -- 1. A bag of floatable wanted constraints, not mentioning any skolems,
709 -- that are of the form unification var = type
711 -- 2. Maybe a unsolved implication, empty if entirely solved!
713 -- Precondition: everything is zonked by now
714 solveImplication tcs_untouchables inert
715 imp@(Implic { ic_untch = untch
716 , ic_binds = ev_binds
719 , ic_wanted = wanteds
721 = nestImplicTcS ev_binds (untch, tcs_untouchables) $
722 recoverTcS (return (emptyBag, emptyBag)) $
723 -- Recover from nested failures. Even the top level is
724 -- just a bunch of implications, so failing at the first
726 do { traceTcS "solveImplication {" (ppr imp)
729 -- ; can_givens <- canGivens loc givens
730 -- ; let given_fl = Given loc
731 ; given_inert <- solveInteract inert $
732 mapBag (\c -> (Given loc,c)) (listToBag givens)
734 -- Simplify the wanteds
735 ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
737 ; let (res_flat_free, res_flat_bound)
738 = floatEqualities skols givens unsolved_flats
739 unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
740 Bag.mapBag WcImplic unsolved_implics
742 ; traceTcS "solveImplication end }" $ vcat
743 [ text "res_flat_free =" <+> ppr res_flat_free
744 , text "res_flat_bound =" <+> ppr res_flat_bound
745 , text "unsolved_implics =" <+> ppr unsolved_implics ]
747 ; let res_bag | isEmptyBag unsolved = emptyBag
748 | otherwise = unitBag (imp { ic_wanted = unsolved })
750 ; return (res_flat_free, res_bag) }
752 floatEqualities :: TcTyVarSet -> [EvVar]
753 -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
754 -- The CanonicalCts will be floated out to be used later, whereas
755 -- the remaining WantedEvVars will remain inside the implication.
756 floatEqualities skols can_given wanteds
757 | hasEqualities can_given = (emptyBag, wanteds)
758 -- Note [Float Equalities out of Implications]
759 | otherwise = partitionBag is_floatable wanteds
760 where is_floatable :: WantedEvVar -> Bool
761 is_floatable (WantedEvVar cv _)
762 | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
763 is_floatable _wv = False
765 tvs_under_fsks :: Type -> TyVarSet
766 -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
767 tvs_under_fsks (TyVarTy tv)
768 | not (isTcTyVar tv) = unitVarSet tv
769 | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
770 | otherwise = unitVarSet tv
771 tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
772 tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty
773 tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
774 tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
775 tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
776 -- can mention type variables!
777 | isTyVar tv = inner_tvs `delVarSet` tv
778 | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
779 inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
781 inner_tvs = tvs_under_fsks ty
783 predTvs_under_fsks :: PredType -> TyVarSet
784 predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty
785 predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys)
786 predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
793 Note [Float Equalities out of Implications]
794 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
795 We want to float equalities out of vanilla existentials, but *not* out
796 of GADT pattern matches.
798 Note [Preparing inert set for implications]
799 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
800 Before solving the nested implications, we convert any unsolved flat wanteds
801 to givens, and add them to the inert set. Reasons:
803 a) In checking mode, suppresses unnecessary errors. We already have
804 on unsolved-wanted error; adding it to the givens prevents any
805 consequential errors from showing uop
807 b) More importantly, in inference mode, we are going to quantify over this
808 constraint, and we *don't* want to quantify over any constraints that
809 are deducible from it.
811 The unsolved wanteds are *canonical* but they may not be *inert*,
812 because when made into a given they might interact with other givens.
813 Hence the call to solveInteract. Example:
815 Original inert set = (d :_g D a) /\ (co :_w a ~ [beta])
817 We were not able to solve (a ~w [beta]) but we can't just assume it as
818 given because the resulting set is not inert. Hence we have to do a
819 'solveInteract' step first.
821 Note [Extra TcsTv untouchables]
822 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
823 Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv
824 kind (such as variables from instance that have been applied, or unification flattens). These
825 variables must be passed to the implications as extra untouchable variables. Otherwise
826 we have the danger of double unifications. Example (from trac ticket #4494):
828 (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
830 In this example, beta is touchable inside the implication. The first solveInteract step
831 leaves 'uf' ununified. Then we move inside the implication where a new constraint
833 emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears
834 but when we pop out again we are left with (F Int ~ uf) which will be unified by our final
835 solveCTyFunEqs stage and uf will get unified *once more* to (F Int).
837 The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables)
838 that are generated when solving the flats, and make them untouchables for the nested
839 implication. In the example above uf would become untouchable, so beta would be forced to
840 be unified as beta := uf.
842 NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out
843 of an implication becomes now untouchable next time we go inside that implication to
844 solve any residual constraints. In effect, by floating an equality out of the implication
845 we are committing to have it solved in the outside.
850 solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
851 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
852 -- See Note [Solving Family Equations]
853 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
854 -- where the newly generated equalities (alpha := F xi) have been substituted through.
855 solveCTyFunEqs cts implics
856 = do { untch <- getUntouchables
857 ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
858 ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
861 ; mapM_ solve_one funeq_bnds
863 -- Apply the substitution through to eliminate the flatten
864 -- unification variables we substituted both in the unsolved flats and implics
866 = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
868 = Bag.mapBag (subst_impl funeq_bnds) implics
870 ; return (final_unsolved, final_implics) }
872 where solve_one (tv,(ty,cv,fl))
873 | not (typeKind ty `isSubKind` tyVarKind tv)
874 = addErrorTcS KindError fl (mkTyVarTy tv) ty
875 -- Must do a small kind check since TcCanonical invariants
876 -- on family equations only impose compatibility, not subkinding
877 | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
879 subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
880 subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv)
881 subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
883 subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
884 subst_wevar funeq_bnds (WantedEvVar v loc)
885 = let orig_ty = varType v
886 new_ty = substFunEqBnds funeq_bnds orig_ty
887 in WantedEvVar (setVarType v new_ty) loc
889 subst_impl :: FunEqBinds -> Implication -> Implication
890 subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
891 = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
894 type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
895 -- Invariant: if it contains:
896 -- [... a -> (ta,...) ... b -> (tb,...) ... ]
897 -- then 'ta' cannot mention 'b'
899 getSolvableCTyFunEqs :: TcsUntouchables
900 -> CanonicalCts -- Precondition: all wanteds
901 -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
902 getSolvableCTyFunEqs untch cts
903 = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
904 where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
909 | Just tv <- tcGetTyVar_maybe xi
910 , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
911 , Nothing <- lookup tv extra_binds -- or in extra_binds
912 -- See Note [Solving Family Equations], Point 1
913 = ASSERT ( isWanted fl )
914 let ty_orig = mkTyConApp tc xis
915 ty_bind = substFunEqBnds extra_binds ty_orig
916 in if tv `elemVarSet` tyVarsOfType ty_bind
917 then (cts_in `extendCCans` ct, extra_binds)
918 -- See Note [Solving Family Equations], Point 2
919 else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
920 -- Postcondition met because extra_binds is already applied to ty_bind
922 dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
924 substFunEqBnds :: FunEqBinds -> TcType -> TcType
925 substFunEqBnds bnds ty
926 = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
927 -- foldr works because of the FunEqBinds invariant
932 Note [Solving Family Equations]
933 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
934 After we are done with simplification we may be left with constraints of the form:
935 [Wanted] F xis ~ beta
936 If 'beta' is a touchable unification variable not already bound in the TyBinds
937 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
939 When is it ok to do so?
940 1) 'beta' must not already be defaulted to something. Example:
942 [Wanted] F Int ~ beta <~ Will default [beta := F Int]
943 [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
944 have to report this as unsolved.
946 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
947 set [beta := F xis] only if beta is not among the free variables of xis.
949 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
950 of type family equations. See Inert Set invariants in TcInteract.
953 *********************************************************************************
955 * Defaulting and disamgiguation *
957 *********************************************************************************
959 Basic plan behind applyDefaulting rules:
962 Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
963 For each defaultable group, do:
964 For each possible substitution for [alpha |-> tau] where `alpha' is the
965 group's variable, do:
966 1) Make up new TcEvBinds
967 2) Extend TcS with (groupVariable
968 3) given_inert <- solveOne inert (given : a ~ tau)
969 4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
970 5) if unsolved == empty then
971 sneakyUnify a |-> tau
972 write the evidence bins
973 return (final_inert ++ group_constraints,[])
974 -- will contain the info (alpha |-> tau)!!
975 goto next defaultable group
976 if unsolved <> empty then
977 throw away evidence binds
978 try next substitution
979 If you've run out of substitutions for this group, too bad, you failed
981 goto next defaultable group
984 Collect all the (canonical-cts, wanteds) gathered this way.
985 - Do a solveGiven over the canonical-cts to make sure they are inert
986 ------------------------------------------------------------------------------------------
990 applyDefaultingRules :: InertSet
991 -> CanonicalCts -- All wanteds
992 -> TcS (Bag WantedEvVar) -- All wanteds again!
993 -- Return some *extra* givens, which express the
994 -- type-class-default choice
996 applyDefaultingRules inert wanteds
1000 = do { untch <- getUntouchables
1001 ; tv_cts <- mapM (defaultTyVar untch) $
1002 varSetElems (tyVarsOfCDicts wanteds)
1004 ; info@(_, default_tys, _) <- getDefaultInfo
1005 ; let groups = findDefaultableGroups info untch wanteds
1006 ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1008 ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1009 , text "Type defaults =" <+> ppr deflt_cts])
1011 ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1014 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar)
1015 -- defaultTyVar is used on any un-instantiated meta type variables to
1016 -- default the kind of ? and ?? etc to *. This is important to ensure
1017 -- that instance declarations match. For example consider
1018 -- instance Show (a->b)
1019 -- foo x = show (\_ -> True)
1020 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1021 -- and that won't match the typeKind (*) in the instance decl.
1024 -- We look only at touchable type variables. No further constraints
1025 -- are going to affect these type variables, so it's time to do it by
1026 -- hand. However we aren't ready to default them fully to () or
1027 -- whatever, because the type-class defaulting rules have yet to run.
1029 defaultTyVar untch the_tv
1030 | isTouchableMetaTyVar_InRange untch the_tv
1031 , not (k `eqKind` default_k)
1032 = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1033 ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1034 ; return (unitBag (WantedEvVar ev loc)) }
1036 = return emptyBag -- The common case
1038 k = tyVarKind the_tv
1039 default_k = defaultKind k
1043 findDefaultableGroups
1046 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
1047 -> TcsUntouchables -- Untouchable
1048 -> CanonicalCts -- Unsolved
1049 -> [[(CanonicalCt,TcTyVar)]]
1050 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1052 | not (performDefaulting ctxt) = []
1053 | null default_tys = []
1054 | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1056 unaries :: [(CanonicalCt, TcTyVar)] -- (C tv) constraints
1057 non_unaries :: [CanonicalCt] -- and *other* constraints
1059 (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1060 -- Finds unary type-class constraints
1061 find_unary cc@(CDictCan { cc_tyargs = [ty] })
1062 | Just tv <- tcGetTyVar_maybe ty
1064 find_unary cc = Right cc -- Non unary or non dictionary
1066 bad_tvs :: TcTyVarSet -- TyVars mentioned by non-unaries
1067 bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1069 cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1071 is_defaultable_group ds@((_,tv):_)
1072 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
1073 && not (tv `elemVarSet` bad_tvs)
1074 && isTouchableMetaTyVar_InRange untch tv
1075 && defaultable_classes [cc_class cc | (cc,_) <- ds]
1076 is_defaultable_group [] = panic "defaultable_group"
1078 defaultable_classes clss
1079 | extended_defaults = any isInteractiveClass clss
1080 | otherwise = all is_std_class clss && (any is_num_class clss)
1082 -- In interactive mode, or with -XExtendedDefaultRules,
1083 -- we default Show a to Show () to avoid graututious errors on "show []"
1084 isInteractiveClass cls
1085 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1087 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1088 -- is_num_class adds IsString to the standard numeric classes,
1089 -- when -foverloaded-strings is enabled
1091 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1092 -- Similarly is_std_class
1094 ------------------------------
1095 disambigGroup :: [Type] -- The default types
1096 -> InertSet -- Given inert
1097 -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a)
1098 -- sharing same type variable
1099 -> TcS (Bag WantedEvVar)
1101 disambigGroup [] _inert _grp
1103 disambigGroup (default_ty:default_tys) inert group
1104 = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1105 ; let ct_loc = get_ct_loc (cc_flavor the_ct)
1106 ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
1107 ; success <- tryTcS $
1108 do { final_inert <- solveInteract inert $
1109 consBag (Wanted ct_loc, ev) wanted_to_solve
1110 ; let (_, unsolved) = extractUnsolved final_inert
1111 ; errs <- getTcSErrorsBag
1112 ; return (isEmptyBag unsolved && isEmptyBag errs) }
1114 True -> -- Success: record the type variable binding, and return
1115 do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1116 ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1117 ; return (unitBag $ WantedEvVar ev ct_loc) }
1118 False -> -- Failure: try with the next type
1119 do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
1120 ; disambigGroup default_tys inert group } }
1122 ((the_ct,the_tv):_) = group
1123 wanteds = map fst group
1124 wanted_ev_vars = map deCanonicaliseWanted wanteds
1125 wanted_to_solve = listToBag $
1126 map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars
1128 get_ct_loc (Wanted l) = l
1129 get_ct_loc _ = panic "Asked to disambiguate given or derived!"
1134 Note [Avoiding spurious errors]
1135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1136 When doing the unification for defaulting, we check for skolem
1137 type variables, and simply don't default them. For example:
1138 f = (*) -- Monomorphic
1139 g :: Num a => a -> a
1141 Here, we get a complaint when checking the type signature for g,
1142 that g isn't polymorphic enough; but then we get another one when
1143 dealing with the (Num a) context arising from f's definition;
1144 we try to unify a with Int (to default it), but find that it's
1145 already been unified with the rigid variable from g's type sig