2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyRuleLhs, tcSimplifyIPs,
13 tcSimplifySuperClasses,
14 tcSimplifyTop, tcSimplifyInteractive,
15 tcSimplifyBracket, tcSimplifyCheckPat,
17 tcSimplifyDeriv, tcSimplifyDefault,
25 #include "HsVersions.h"
27 import {-# SOURCE #-} TcUnify( unifyType )
31 import TcHsSyn ( hsLPatType )
39 import DsUtils -- Big-tuple functions
69 %************************************************************************
73 %************************************************************************
75 --------------------------------------
76 Notes on functional dependencies (a bug)
77 --------------------------------------
84 instance D a b => C a b -- Undecidable
85 -- (Not sure if it's crucial to this eg)
86 f :: C a b => a -> Bool
89 g :: C a b => a -> Bool
92 Here f typechecks, but g does not!! Reason: before doing improvement,
93 we reduce the (C a b1) constraint from the call of f to (D a b1).
95 Here is a more complicated example:
98 > class Foo a b | a->b
100 > class Bar a b | a->b
104 > instance Bar Obj Obj
106 > instance (Bar a b) => Foo a b
108 > foo:: (Foo a b) => a -> String
111 > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
117 Could not deduce (Bar a b) from the context (Foo a b)
118 arising from use of `foo' at <interactive>:1
120 Add (Bar a b) to the expected type of an expression
121 In the first argument of `runFoo', namely `foo'
122 In the definition of `it': it = runFoo foo
124 Why all of the sudden does GHC need the constraint Bar a b? The
125 function foo didn't ask for that...
128 The trouble is that to type (runFoo foo), GHC has to solve the problem:
130 Given constraint Foo a b
131 Solve constraint Foo a b'
133 Notice that b and b' aren't the same. To solve this, just do
134 improvement and then they are the same. But GHC currently does
139 That is usually fine, but it isn't here, because it sees that Foo a b is
140 not the same as Foo a b', and so instead applies the instance decl for
141 instance Bar a b => Foo a b. And that's where the Bar constraint comes
144 The Right Thing is to improve whenever the constraint set changes at
145 all. Not hard in principle, but it'll take a bit of fiddling to do.
147 Note [Choosing which variables to quantify]
148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
149 Suppose we are about to do a generalisation step. We have in our hand
152 T the type of the RHS
153 C the constraints from that RHS
155 The game is to figure out
157 Q the set of type variables over which to quantify
158 Ct the constraints we will *not* quantify over
159 Cq the constraints we will quantify over
161 So we're going to infer the type
165 and float the constraints Ct further outwards.
167 Here are the things that *must* be true:
169 (A) Q intersect fv(G) = EMPTY limits how big Q can be
170 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
172 (A) says we can't quantify over a variable that's free in the environment.
173 (B) says we must quantify over all the truly free variables in T, else
174 we won't get a sufficiently general type.
176 We do not *need* to quantify over any variable that is fixed by the
177 free vars of the environment G.
179 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
181 Example: class H x y | x->y where ...
183 fv(G) = {a} C = {H a b, H c d}
186 (A) Q intersect {a} is empty
187 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
189 So Q can be {c,d}, {b,c,d}
191 In particular, it's perfectly OK to quantify over more type variables
192 than strictly necessary; there is no need to quantify over 'b', since
193 it is determined by 'a' which is free in the envt, but it's perfectly
194 OK to do so. However we must not quantify over 'a' itself.
196 Other things being equal, however, we'd like to quantify over as few
197 variables as possible: smaller types, fewer type applications, more
198 constraints can get into Ct instead of Cq. Here's a good way to
201 Q = grow( fv(T), C ) \ oclose( fv(G), C )
203 That is, quantify over all variable that that MIGHT be fixed by the
204 call site (which influences T), but which aren't DEFINITELY fixed by
205 G. This choice definitely quantifies over enough type variables,
206 albeit perhaps too many.
208 Why grow( fv(T), C ) rather than fv(T)? Consider
210 class H x y | x->y where ...
215 If we used fv(T) = {c} we'd get the type
217 forall c. H c d => c -> b
219 And then if the fn was called at several different c's, each of
220 which fixed d differently, we'd get a unification error, because
221 d isn't quantified. Solution: quantify d. So we must quantify
222 everything that might be influenced by c.
224 Why not oclose( fv(T), C )? Because we might not be able to see
225 all the functional dependencies yet:
227 class H x y | x->y where ...
228 instance H x y => Eq (T x y) where ...
233 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
234 apparent yet, and that's wrong. We must really quantify over d too.
236 There really isn't any point in quantifying over any more than
237 grow( fv(T), C ), because the call sites can't possibly influence
238 any other type variables.
242 -------------------------------------
244 -------------------------------------
246 It's very hard to be certain when a type is ambiguous. Consider
250 instance H x y => K (x,y)
252 Is this type ambiguous?
253 forall a b. (K (a,b), Eq b) => a -> a
255 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
256 now we see that a fixes b. So we can't tell about ambiguity for sure
257 without doing a full simplification. And even that isn't possible if
258 the context has some free vars that may get unified. Urgle!
260 Here's another example: is this ambiguous?
261 forall a b. Eq (T b) => a -> a
262 Not if there's an insance decl (with no context)
263 instance Eq (T b) where ...
265 You may say of this example that we should use the instance decl right
266 away, but you can't always do that:
268 class J a b where ...
269 instance J Int b where ...
271 f :: forall a b. J a b => a -> a
273 (Notice: no functional dependency in J's class decl.)
274 Here f's type is perfectly fine, provided f is only called at Int.
275 It's premature to complain when meeting f's signature, or even
276 when inferring a type for f.
280 However, we don't *need* to report ambiguity right away. It'll always
281 show up at the call site.... and eventually at main, which needs special
282 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
284 So here's the plan. We WARN about probable ambiguity if
286 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
288 (all tested before quantification).
289 That is, all the type variables in Cq must be fixed by the the variables
290 in the environment, or by the variables in the type.
292 Notice that we union before calling oclose. Here's an example:
294 class J a b c | a b -> c
298 forall b c. (J a b c) => b -> b
300 Only if we union {a} from G with {b} from T before using oclose,
301 do we see that c is fixed.
303 It's a bit vague exactly which C we should use for this oclose call. If we
304 don't fix enough variables we might complain when we shouldn't (see
305 the above nasty example). Nothing will be perfect. That's why we can
306 only issue a warning.
309 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
311 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
313 then c is a "bubble"; there's no way it can ever improve, and it's
314 certainly ambiguous. UNLESS it is a constant (sigh). And what about
319 instance H x y => K (x,y)
321 Is this type ambiguous?
322 forall a b. (K (a,b), Eq b) => a -> a
324 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
325 is a "bubble" that's a set of constraints
327 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
329 Hence another idea. To decide Q start with fv(T) and grow it
330 by transitive closure in Cq (no functional dependencies involved).
331 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
332 The definitely-ambiguous can then float out, and get smashed at top level
333 (which squashes out the constants, like Eq (T a) above)
336 --------------------------------------
337 Notes on principal types
338 --------------------------------------
343 f x = let g y = op (y::Int) in True
345 Here the principal type of f is (forall a. a->a)
346 but we'll produce the non-principal type
347 f :: forall a. C Int => a -> a
350 --------------------------------------
351 The need for forall's in constraints
352 --------------------------------------
354 [Exchange on Haskell Cafe 5/6 Dec 2000]
356 class C t where op :: t -> Bool
357 instance C [t] where op x = True
359 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
360 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
362 The definitions of p and q differ only in the order of the components in
363 the pair on their right-hand sides. And yet:
365 ghc and "Typing Haskell in Haskell" reject p, but accept q;
366 Hugs rejects q, but accepts p;
367 hbc rejects both p and q;
368 nhc98 ... (Malcolm, can you fill in the blank for us!).
370 The type signature for f forces context reduction to take place, and
371 the results of this depend on whether or not the type of y is known,
372 which in turn depends on which component of the pair the type checker
375 Solution: if y::m a, float out the constraints
376 Monad m, forall c. C (m c)
377 When m is later unified with [], we can solve both constraints.
380 --------------------------------------
381 Notes on implicit parameters
382 --------------------------------------
384 Note [Inheriting implicit parameters]
385 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
390 where f is *not* a top-level binding.
391 From the RHS of f we'll get the constraint (?y::Int).
392 There are two types we might infer for f:
396 (so we get ?y from the context of f's definition), or
398 f :: (?y::Int) => Int -> Int
400 At first you might think the first was better, becuase then
401 ?y behaves like a free variable of the definition, rather than
402 having to be passed at each call site. But of course, the WHOLE
403 IDEA is that ?y should be passed at each call site (that's what
404 dynamic binding means) so we'd better infer the second.
406 BOTTOM LINE: when *inferring types* you *must* quantify
407 over implicit parameters. See the predicate isFreeWhenInferring.
410 Note [Implicit parameters and ambiguity]
411 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
412 Only a *class* predicate can give rise to ambiguity
413 An *implicit parameter* cannot. For example:
414 foo :: (?x :: [a]) => Int
416 is fine. The call site will suppply a particular 'x'
418 Furthermore, the type variables fixed by an implicit parameter
419 propagate to the others. E.g.
420 foo :: (Show a, ?x::[a]) => Int
422 The type of foo looks ambiguous. But it isn't, because at a call site
424 let ?x = 5::Int in foo
425 and all is well. In effect, implicit parameters are, well, parameters,
426 so we can take their type variables into account as part of the
427 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
430 Question 2: type signatures
431 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
432 BUT WATCH OUT: When you supply a type signature, we can't force you
433 to quantify over implicit parameters. For example:
437 This is perfectly reasonable. We do not want to insist on
439 (?x + 1) :: (?x::Int => Int)
441 That would be silly. Here, the definition site *is* the occurrence site,
442 so the above strictures don't apply. Hence the difference between
443 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
444 and tcSimplifyCheckBind (which does not).
446 What about when you supply a type signature for a binding?
447 Is it legal to give the following explicit, user type
448 signature to f, thus:
453 At first sight this seems reasonable, but it has the nasty property
454 that adding a type signature changes the dynamic semantics.
457 (let f x = (x::Int) + ?y
458 in (f 3, f 3 with ?y=5)) with ?y = 6
464 in (f 3, f 3 with ?y=5)) with ?y = 6
468 Indeed, simply inlining f (at the Haskell source level) would change the
471 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
472 semantics for a Haskell program without knowing its typing, so if you
473 change the typing you may change the semantics.
475 To make things consistent in all cases where we are *checking* against
476 a supplied signature (as opposed to inferring a type), we adopt the
479 a signature does not need to quantify over implicit params.
481 [This represents a (rather marginal) change of policy since GHC 5.02,
482 which *required* an explicit signature to quantify over all implicit
483 params for the reasons mentioned above.]
485 But that raises a new question. Consider
487 Given (signature) ?x::Int
488 Wanted (inferred) ?x::Int, ?y::Bool
490 Clearly we want to discharge the ?x and float the ?y out. But
491 what is the criterion that distinguishes them? Clearly it isn't
492 what free type variables they have. The Right Thing seems to be
493 to float a constraint that
494 neither mentions any of the quantified type variables
495 nor any of the quantified implicit parameters
497 See the predicate isFreeWhenChecking.
500 Question 3: monomorphism
501 ~~~~~~~~~~~~~~~~~~~~~~~~
502 There's a nasty corner case when the monomorphism restriction bites:
506 The argument above suggests that we *must* generalise
507 over the ?y parameter, to get
508 z :: (?y::Int) => Int,
509 but the monomorphism restriction says that we *must not*, giving
511 Why does the momomorphism restriction say this? Because if you have
513 let z = x + ?y in z+z
515 you might not expect the addition to be done twice --- but it will if
516 we follow the argument of Question 2 and generalise over ?y.
519 Question 4: top level
520 ~~~~~~~~~~~~~~~~~~~~~
521 At the top level, monomorhism makes no sense at all.
524 main = let ?x = 5 in print foo
528 woggle :: (?x :: Int) => Int -> Int
531 We definitely don't want (foo :: Int) with a top-level implicit parameter
532 (?x::Int) becuase there is no way to bind it.
537 (A) Always generalise over implicit parameters
538 Bindings that fall under the monomorphism restriction can't
542 * Inlining remains valid
543 * No unexpected loss of sharing
544 * But simple bindings like
546 will be rejected, unless you add an explicit type signature
547 (to avoid the monomorphism restriction)
548 z :: (?y::Int) => Int
550 This seems unacceptable
552 (B) Monomorphism restriction "wins"
553 Bindings that fall under the monomorphism restriction can't
555 Always generalise over implicit parameters *except* for bindings
556 that fall under the monomorphism restriction
559 * Inlining isn't valid in general
560 * No unexpected loss of sharing
561 * Simple bindings like
563 accepted (get value of ?y from binding site)
565 (C) Always generalise over implicit parameters
566 Bindings that fall under the monomorphism restriction can't
567 be generalised, EXCEPT for implicit parameters
569 * Inlining remains valid
570 * Unexpected loss of sharing (from the extra generalisation)
571 * Simple bindings like
573 accepted (get value of ?y from occurrence sites)
578 None of these choices seems very satisfactory. But at least we should
579 decide which we want to do.
581 It's really not clear what is the Right Thing To Do. If you see
585 would you expect the value of ?y to be got from the *occurrence sites*
586 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
587 case of function definitions, the answer is clearly the former, but
588 less so in the case of non-fucntion definitions. On the other hand,
589 if we say that we get the value of ?y from the definition site of 'z',
590 then inlining 'z' might change the semantics of the program.
592 Choice (C) really says "the monomorphism restriction doesn't apply
593 to implicit parameters". Which is fine, but remember that every
594 innocent binding 'x = ...' that mentions an implicit parameter in
595 the RHS becomes a *function* of that parameter, called at each
596 use of 'x'. Now, the chances are that there are no intervening 'with'
597 clauses that bind ?y, so a decent compiler should common up all
598 those function calls. So I think I strongly favour (C). Indeed,
599 one could make a similar argument for abolishing the monomorphism
600 restriction altogether.
602 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
606 %************************************************************************
608 \subsection{tcSimplifyInfer}
610 %************************************************************************
612 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
614 1. Compute Q = grow( fvs(T), C )
616 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
617 predicates will end up in Ct; we deal with them at the top level
619 3. Try improvement, using functional dependencies
621 4. If Step 3 did any unification, repeat from step 1
622 (Unification can change the result of 'grow'.)
624 Note: we don't reduce dictionaries in step 2. For example, if we have
625 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
626 after step 2. However note that we may therefore quantify over more
627 type variables than we absolutely have to.
629 For the guts, we need a loop, that alternates context reduction and
630 improvement with unification. E.g. Suppose we have
632 class C x y | x->y where ...
634 and tcSimplify is called with:
636 Then improvement unifies a with b, giving
639 If we need to unify anything, we rattle round the whole thing all over
646 -> TcTyVarSet -- fv(T); type vars
648 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)
649 [Inst], -- Dict Ids that must be bound here (zonked)
650 TcDictBinds) -- Bindings
651 -- Any free (escaping) Insts are tossed into the environment
656 tcSimplifyInfer doc tau_tvs wanted
657 = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
658 ; wanted' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars
659 ; gbl_tvs <- tcGetGlobalTyVars
660 ; let preds1 = fdPredsOfInsts wanted'
661 gbl_tvs1 = oclose preds1 gbl_tvs
662 qtvs = growInstsTyVars wanted' tau_tvs1 `minusVarSet` gbl_tvs1
663 -- See Note [Choosing which variables to quantify]
665 -- To maximise sharing, remove from consideration any
666 -- constraints that don't mention qtvs at all
667 ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
670 -- To make types simple, reduce as much as possible
671 ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (growInstsTyVars wanted' tau_tvs1) $$ ppr gbl_tvs $$
672 ppr gbl_tvs1 $$ ppr free $$ ppr bound))
673 ; (irreds1, binds1) <- tryHardCheckLoop doc bound
675 -- Note [Inference and implication constraints]
676 ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
677 ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
679 -- Now work out all over again which type variables to quantify,
680 -- exactly in the same way as before, but starting from irreds2. Why?
681 -- a) By now improvment may have taken place, and we must *not*
682 -- quantify over any variable free in the environment
683 -- tc137 (function h inside g) is an example
685 -- b) Do not quantify over constraints that *now* do not
686 -- mention quantified type variables, because they are
687 -- simply ambiguous (or might be bound further out). Example:
688 -- f :: Eq b => a -> (a, b)
690 -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
691 -- We decide to quantify over 'alpha' alone, but free1 does not include f77
692 -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
693 -- constraint (Eq beta), which we dump back into the free set
694 -- See test tcfail181
696 -- c) irreds may contain type variables not previously mentioned,
697 -- e.g. instance D a x => Foo [a]
699 -- Then after simplifying we'll get (D a x), and x is fresh
700 -- We must quantify over x else it'll be totally unbound
701 ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
702 ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
703 -- Note that we start from gbl_tvs1
704 -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
705 -- we've already put some of the original preds1 into frees
706 -- E.g. wanteds = C a b (where a->b)
709 -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
710 -- irreds2 will be empty. But we don't want to generalise over b!
711 ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
712 qtvs = growInstsTyVars irreds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
713 ---------------------------------------------------
714 -- BUG WARNING: there's a nasty bug lurking here
715 -- fdPredsOfInsts may return preds that mention variables quantified in
716 -- one of the implication constraints in irreds2; and that is clearly wrong:
717 -- we might quantify over too many variables through accidental capture
718 ---------------------------------------------------
719 ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
722 -- Turn the quantified meta-type variables into real type variables
723 ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
725 -- We can't abstract over any remaining unsolved
726 -- implications so instead just float them outwards. Ugh.
727 ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
728 ; loc <- getInstLoc (ImplicOrigin doc)
729 ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
731 -- Prepare equality instances for quantification
732 ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
733 ; q_eqs <- mapM finalizeEqInst q_eqs0
735 ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
736 -- NB: when we are done, we might have some bindings, but
737 -- the final qtvs might be empty. See Note [NO TYVARS] below.
739 approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
740 -- Note [Inference and implication constraints]
741 -- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
742 -- - fetching any dicts inside them that are free
743 -- - using those dicts as cruder constraints, to solve the implications
744 -- - returning the extra ones too
746 approximateImplications doc want_dict irreds
748 = return (irreds, emptyBag)
750 = do { extra_dicts' <- mapM cloneDict extra_dicts
751 ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
752 -- By adding extra_dicts', we make them
753 -- available to solve the implication constraints
755 extra_dicts = get_dicts (filter isImplicInst irreds)
757 get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
758 -- Find the wanted constraints in implication constraints that satisfy
759 -- want_dict, and are not bound by forall's in the constraint itself
760 get_dicts ds = concatMap get_dict ds
762 get_dict d@(Dict {}) | want_dict d = [d]
764 get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
765 = [ d | let tv_set = mkVarSet tvs
766 , d <- get_dicts wanteds
767 , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
768 get_dict i@(EqInst {}) | want_dict i = [i]
770 get_dict other = pprPanic "approximateImplications" (ppr other)
773 Note [Inference and implication constraints]
774 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
775 Suppose we have a wanted implication constraint (perhaps arising from
776 a nested pattern match) like
778 and we are now trying to quantify over 'a' when inferring the type for
779 a function. In principle it's possible that there might be an instance
780 instance (C a, E a) => D [a]
781 so the context (E a) would suffice. The Right Thing is to abstract over
782 the implication constraint, but we don't do that (a) because it'll be
783 surprising to programmers and (b) because we don't have the machinery to deal
784 with 'given' implications.
786 So our best approximation is to make (D [a]) part of the inferred
787 context, so we can use that to discharge the implication. Hence
788 the strange function get_dicts in approximateImplications.
790 The common cases are more clear-cut, when we have things like
792 Here, abstracting over (C b) is not an approximation at all -- but see
793 Note [Freeness and implications].
795 See Trac #1430 and test tc228.
799 -----------------------------------------------------------
800 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
801 -- against, but we don't know the type variables over which we are going to quantify.
802 -- This happens when we have a type signature for a mutually recursive group
805 -> TcTyVarSet -- fv(T)
808 -> TcM ([TyVar], -- Fully zonked, and quantified
809 TcDictBinds) -- Bindings
811 tcSimplifyInferCheck loc tau_tvs givens wanteds
812 = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
813 ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
815 -- Figure out which type variables to quantify over
816 -- You might think it should just be the signature tyvars,
817 -- but in bizarre cases you can get extra ones
818 -- f :: forall a. Num a => a -> a
819 -- f x = fst (g (x, head [])) + 1
821 -- Here we infer g :: forall a b. a -> b -> (b,a)
822 -- We don't want g to be monomorphic in b just because
823 -- f isn't quantified over b.
824 ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
825 ; all_tvs <- zonkTcTyVarsAndFV all_tvs
826 ; gbl_tvs <- tcGetGlobalTyVars
827 ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
828 -- We could close gbl_tvs, but its not necessary for
829 -- soundness, and it'll only affect which tyvars, not which
830 -- dictionaries, we quantify over
832 ; qtvs' <- zonkQuantifiedTyVars qtvs
834 -- Now we are back to normal (c.f. tcSimplCheck)
835 ; implic_bind <- bindIrreds loc qtvs' givens irreds
837 ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
838 ; return (qtvs', binds `unionBags` implic_bind) }
841 Note [Squashing methods]
842 ~~~~~~~~~~~~~~~~~~~~~~~~~
843 Be careful if you want to float methods more:
844 truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
845 From an application (truncate f i) we get
848 If we have also have a second occurrence of truncate, we get
851 When simplifying with i,f free, we might still notice that
852 t1=t3; but alas, the binding for t2 (which mentions t1)
853 may continue to float out!
858 class Y a b | a -> b where
861 instance Y [[a]] a where
864 k :: X a -> X a -> X a
866 g :: Num a => [X a] -> [X a]
869 h ys = ys ++ map (k (y [[0]])) xs
871 The excitement comes when simplifying the bindings for h. Initially
872 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
873 From this we get t1~t2, but also various bindings. We can't forget
874 the bindings (because of [LOOP]), but in fact t1 is what g is
877 The net effect of [NO TYVARS]
880 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
881 isFreeWhenInferring qtvs inst
882 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
883 && isInheritableInst inst -- and no implicit parameter involved
884 -- see Note [Inheriting implicit parameters]
886 {- No longer used (with implication constraints)
887 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
888 -> NameSet -- Quantified implicit parameters
890 isFreeWhenChecking qtvs ips inst
891 = isFreeWrtTyVars qtvs inst
892 && isFreeWrtIPs ips inst
895 isFreeWrtTyVars :: VarSet -> Inst -> Bool
896 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
897 isFreeWrtIPs :: NameSet -> Inst -> Bool
898 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
902 %************************************************************************
904 \subsection{tcSimplifyCheck}
906 %************************************************************************
908 @tcSimplifyCheck@ is used when we know exactly the set of variables
909 we are going to quantify over. For example, a class or instance declaration.
912 -----------------------------------------------------------
913 -- tcSimplifyCheck is used when checking expression type signatures,
914 -- class decls, instance decls etc.
915 tcSimplifyCheck :: InstLoc
916 -> [TcTyVar] -- Quantify over these
919 -> TcM TcDictBinds -- Bindings
920 tcSimplifyCheck loc qtvs givens wanteds
921 = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
922 do { traceTc (text "tcSimplifyCheck")
923 ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
924 ; implic_bind <- bindIrreds loc qtvs givens irreds
925 ; return (binds `unionBags` implic_bind) }
927 -----------------------------------------------------------
928 -- tcSimplifyCheckPat is used for existential pattern match
929 tcSimplifyCheckPat :: InstLoc
930 -> [TcTyVar] -- Quantify over these
933 -> TcM TcDictBinds -- Bindings
934 tcSimplifyCheckPat loc qtvs givens wanteds
935 = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
936 do { traceTc (text "tcSimplifyCheckPat")
937 ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
938 ; implic_bind <- bindIrredsR loc qtvs givens irreds
939 ; return (binds `unionBags` implic_bind) }
941 -----------------------------------------------------------
942 bindIrreds :: InstLoc -> [TcTyVar]
945 bindIrreds loc qtvs givens irreds
946 = bindIrredsR loc qtvs givens irreds
948 bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds
949 -- Make a binding that binds 'irreds', by generating an implication
950 -- constraint for them, *and* throwing the constraint into the LIE
951 bindIrredsR loc qtvs givens irreds
955 = do { let givens' = filter isAbstractableInst givens
956 -- The givens can (redundantly) include methods
957 -- We want to retain both EqInsts and Dicts
958 -- There should be no implicadtion constraints
959 -- See Note [Pruning the givens in an implication constraint]
961 -- If there are no 'givens', then it's safe to
962 -- partition the 'wanteds' by their qtvs, thereby trimming irreds
963 -- See Note [Freeness and implications]
964 ; irreds' <- if null givens'
966 { let qtv_set = mkVarSet qtvs
967 (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
969 ; return real_irreds }
972 ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
973 -- This call does the real work
974 -- If irreds' is empty, it does something sensible
979 makeImplicationBind :: InstLoc -> [TcTyVar]
981 -> TcM ([Inst], TcDictBinds)
982 -- Make a binding that binds 'irreds', by generating an implication
983 -- constraint for them.
985 -- The binding looks like
986 -- (ir1, .., irn) = f qtvs givens
987 -- where f is (evidence for) the new implication constraint
988 -- f :: forall qtvs. givens => (ir1, .., irn)
989 -- qtvs includes coercion variables
991 -- This binding must line up the 'rhs' in reduceImplication
992 makeImplicationBind loc all_tvs
993 givens -- Guaranteed all Dicts or EqInsts
995 | null irreds -- If there are no irreds, we are done
996 = return ([], emptyBag)
997 | otherwise -- Otherwise we must generate a binding
998 = do { uniq <- newUnique
999 ; span <- getSrcSpanM
1000 ; let (eq_givens, dict_givens) = partition isEqInst givens
1002 -- extract equality binders
1003 eq_cotvs = map eqInstType eq_givens
1005 -- make the implication constraint instance
1006 name = mkInternalName uniq (mkVarOcc "ic") span
1007 implic_inst = ImplicInst { tci_name = name,
1008 tci_tyvars = all_tvs,
1009 tci_given = eq_givens ++ dict_givens,
1010 -- same order as binders
1011 tci_wanted = irreds,
1014 -- create binders for the irreducible dictionaries
1015 dict_irreds = filter (not . isEqInst) irreds
1016 dict_irred_ids = map instToId dict_irreds
1017 lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
1019 -- create the binding
1020 rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
1021 co = mkWpApps (map instToId dict_givens)
1022 <.> mkWpTyApps eq_cotvs
1023 <.> mkWpTyApps (mkTyVarTys all_tvs)
1024 bind | [dict_irred_id] <- dict_irred_ids
1025 = VarBind dict_irred_id rhs
1027 = PatBind { pat_lhs = lpat
1028 , pat_rhs = unguardedGRHSs rhs
1029 , pat_rhs_ty = hsLPatType lpat
1030 , bind_fvs = placeHolderNames
1033 ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
1034 ; return ([implic_inst], unitBag (L span bind))
1037 -----------------------------------------------------------
1038 tryHardCheckLoop :: SDoc
1040 -> TcM ([Inst], TcDictBinds)
1042 tryHardCheckLoop doc wanteds
1043 = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
1044 ; return (irreds,binds)
1048 -- Here's the try-hard bit
1050 -----------------------------------------------------------
1051 gentleCheckLoop :: InstLoc
1054 -> TcM ([Inst], TcDictBinds)
1056 gentleCheckLoop inst_loc givens wanteds
1057 = do { (irreds,binds) <- checkLoop env wanteds
1058 ; return (irreds,binds)
1061 env = mkRedEnv (pprInstLoc inst_loc) try_me givens
1063 try_me inst | isMethodOrLit inst = ReduceMe
1065 -- When checking against a given signature
1066 -- we MUST be very gentle: Note [Check gently]
1068 gentleInferLoop :: SDoc -> [Inst]
1069 -> TcM ([Inst], TcDictBinds)
1070 gentleInferLoop doc wanteds
1071 = do { (irreds, binds) <- checkLoop env wanteds
1072 ; return (irreds, binds) }
1074 env = mkInferRedEnv doc try_me
1075 try_me inst | isMethodOrLit inst = ReduceMe
1080 ~~~~~~~~~~~~~~~~~~~~
1081 We have to very careful about not simplifying too vigorously
1086 f :: Show b => T b -> b
1087 f (MkT x) = show [x]
1089 Inside the pattern match, which binds (a:*, x:a), we know that
1091 Hence we have a dictionary for Show [a] available; and indeed we
1092 need it. We are going to build an implication contraint
1093 forall a. (b~[a]) => Show [a]
1094 Later, we will solve this constraint using the knowledge (Show b)
1096 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
1097 thing becomes insoluble. So we simplify gently (get rid of literals
1098 and methods only, plus common up equal things), deferring the real
1099 work until top level, when we solve the implication constraint
1100 with tryHardCheckLooop.
1104 -----------------------------------------------------------
1107 -> TcM ([Inst], TcDictBinds)
1108 -- Precondition: givens are completely rigid
1109 -- Postcondition: returned Insts are zonked
1111 checkLoop env wanteds
1113 where go env wanteds
1114 = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
1115 ; env' <- zonkRedEnv env
1116 ; wanteds' <- zonkInsts wanteds
1118 ; (improved, binds, irreds) <- reduceContext env' wanteds'
1120 ; if null irreds || not improved then
1121 return (irreds, binds)
1124 -- If improvement did some unification, we go round again.
1125 -- We start again with irreds, not wanteds
1126 -- Using an instance decl might have introduced a fresh type
1127 -- variable which might have been unified, so we'd get an
1128 -- infinite loop if we started again with wanteds!
1130 { (irreds1, binds1) <- go env' irreds
1131 ; return (irreds1, binds `unionBags` binds1) } }
1134 Note [Zonking RedEnv]
1135 ~~~~~~~~~~~~~~~~~~~~~
1136 It might appear as if the givens in RedEnv are always rigid, but that is not
1137 necessarily the case for programs involving higher-rank types that have class
1138 contexts constraining the higher-rank variables. An example from tc237 in the
1141 class Modular s a | s -> a
1143 wim :: forall a w. Integral a
1144 => a -> (forall s. Modular s a => M s w) -> w
1145 wim i k = error "urk"
1147 test5 :: (Modular s a, Integral a) => M s a
1150 test4 = wim 4 test4'
1152 Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
1153 quantified further outside. When type checking test4, we have to check
1154 whether the signature of test5 is an instance of
1156 (forall s. Modular s a => M s w)
1158 Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
1161 Given the FD of Modular in this example, class improvement will instantiate
1162 t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
1163 Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
1164 the givens, we will get into a loop as improveOne uses the unification engine
1165 Unify.tcUnifyTys, which doesn't know about mutable type variables.
1170 class If b t e r | b t e -> r
1173 class Lte a b c | a b -> c where lte :: a -> b -> c
1175 instance (Lte a b l,If l b a c) => Max a b c
1177 Wanted: Max Z (S x) y
1179 Then we'll reduce using the Max instance to:
1180 (Lte Z (S x) l, If l (S x) Z y)
1181 and improve by binding l->T, after which we can do some reduction
1182 on both the Lte and If constraints. What we *can't* do is start again
1183 with (Max Z (S x) y)!
1187 %************************************************************************
1189 tcSimplifySuperClasses
1191 %************************************************************************
1193 Note [SUPERCLASS-LOOP 1]
1194 ~~~~~~~~~~~~~~~~~~~~~~~~
1195 We have to be very, very careful when generating superclasses, lest we
1196 accidentally build a loop. Here's an example:
1200 class S a => C a where { opc :: a -> a }
1201 class S b => D b where { opd :: b -> b }
1203 instance C Int where
1206 instance D Int where
1209 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1210 Simplifying, we may well get:
1211 $dfCInt = :C ds1 (opd dd)
1214 Notice that we spot that we can extract ds1 from dd.
1216 Alas! Alack! We can do the same for (instance D Int):
1218 $dfDInt = :D ds2 (opc dc)
1222 And now we've defined the superclass in terms of itself.
1223 Two more nasty cases are in
1228 - Satisfy the superclass context *all by itself*
1229 (tcSimplifySuperClasses)
1230 - And do so completely; i.e. no left-over constraints
1231 to mix with the constraints arising from method declarations
1234 Note [Recursive instances and superclases]
1235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1236 Consider this code, which arises in the context of "Scrap Your
1237 Boilerplate with Class".
1241 instance Sat (ctx Char) => Data ctx Char
1242 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1244 class Data Maybe a => Foo a
1246 instance Foo t => Sat (Maybe t)
1248 instance Data Maybe a => Foo a
1249 instance Foo a => Foo [a]
1252 In the instance for Foo [a], when generating evidence for the superclasses
1253 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1254 Using the instance for Data, we therefore need
1255 (Sat (Maybe [a], Data Maybe a)
1256 But we are given (Foo a), and hence its superclass (Data Maybe a).
1257 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1258 we need (Foo [a]). And that is the very dictionary we are bulding
1259 an instance for! So we must put that in the "givens". So in this
1261 Given: Foo a, Foo [a]
1262 Watend: Data Maybe [a]
1264 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1265 the givens, which is what 'addGiven' would normally do. Why? Because
1266 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1267 by selecting a superclass from Foo [a], which simply makes a loop.
1269 On the other hand we *must* put the superclasses of (Foo a) in
1270 the givens, as you can see from the derivation described above.
1272 Conclusion: in the very special case of tcSimplifySuperClasses
1273 we have one 'given' (namely the "this" dictionary) whose superclasses
1274 must not be added to 'givens' by addGiven.
1276 There is a complication though. Suppose there are equalities
1277 instance (Eq a, a~b) => Num (a,b)
1278 Then we normalise the 'givens' wrt the equalities, so the original
1279 given "this" dictionary is cast to one of a different type. So it's a
1280 bit trickier than before to identify the "special" dictionary whose
1281 superclasses must not be added. See test
1282 indexed-types/should_run/EqInInstance
1284 We need a persistent property of the dictionary to record this
1285 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1286 but cool), which is maintained by dictionary normalisation.
1287 Specifically, the InstLocOrigin is
1289 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1293 tcSimplifySuperClasses
1295 -> Inst -- The dict whose superclasses
1296 -- are being figured out
1300 tcSimplifySuperClasses loc this givens sc_wanteds
1301 = do { traceTc (text "tcSimplifySuperClasses")
1303 -- Note [Recursive instances and superclases]
1304 ; no_sc_loc <- getInstLoc NoScOrigin
1305 ; let no_sc_this = setInstLoc this no_sc_loc
1307 ; let env = RedEnv { red_doc = pprInstLoc loc,
1308 red_try_me = try_me,
1309 red_givens = no_sc_this : givens,
1311 red_improve = False } -- No unification vars
1314 ; (irreds,binds1) <- checkLoop env sc_wanteds
1315 ; let (tidy_env, tidy_irreds) = tidyInsts irreds
1316 ; reportNoInstances tidy_env (Just (loc, givens)) [] tidy_irreds
1319 try_me _ = ReduceMe -- Try hard, so we completely solve the superclass
1320 -- constraints right here. See Note [SUPERCLASS-LOOP 1]
1324 %************************************************************************
1326 \subsection{tcSimplifyRestricted}
1328 %************************************************************************
1330 tcSimplifyRestricted infers which type variables to quantify for a
1331 group of restricted bindings. This isn't trivial.
1334 We want to quantify over a to get id :: forall a. a->a
1337 We do not want to quantify over a, because there's an Eq a
1338 constraint, so we get eq :: a->a->Bool (notice no forall)
1341 RHS has type 'tau', whose free tyvars are tau_tvs
1342 RHS has constraints 'wanteds'
1345 Quantify over (tau_tvs \ ftvs(wanteds))
1346 This is bad. The constraints may contain (Monad (ST s))
1347 where we have instance Monad (ST s) where...
1348 so there's no need to be monomorphic in s!
1350 Also the constraint might be a method constraint,
1351 whose type mentions a perfectly innocent tyvar:
1352 op :: Num a => a -> b -> a
1353 Here, b is unconstrained. A good example would be
1355 We want to infer the polymorphic type
1356 foo :: forall b. b -> b
1359 Plan B (cunning, used for a long time up to and including GHC 6.2)
1360 Step 1: Simplify the constraints as much as possible (to deal
1361 with Plan A's problem). Then set
1362 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1364 Step 2: Now simplify again, treating the constraint as 'free' if
1365 it does not mention qtvs, and trying to reduce it otherwise.
1366 The reasons for this is to maximise sharing.
1368 This fails for a very subtle reason. Suppose that in the Step 2
1369 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
1370 In the Step 1 this constraint might have been simplified, perhaps to
1371 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
1372 This won't happen in Step 2... but that in turn might prevent some other
1373 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
1374 and that in turn breaks the invariant that no constraints are quantified over.
1376 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
1381 Step 1: Simplify the constraints as much as possible (to deal
1382 with Plan A's problem). Then set
1383 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1384 Return the bindings from Step 1.
1387 A note about Plan C (arising from "bug" reported by George Russel March 2004)
1390 instance (HasBinary ty IO) => HasCodedValue ty
1392 foo :: HasCodedValue a => String -> IO a
1394 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1395 doDecodeIO codedValue view
1396 = let { act = foo "foo" } in act
1398 You might think this should work becuase the call to foo gives rise to a constraint
1399 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1400 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1401 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1403 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1407 Plan D (a variant of plan B)
1408 Step 1: Simplify the constraints as much as possible (to deal
1409 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1410 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1412 Step 2: Now simplify again, treating the constraint as 'free' if
1413 it does not mention qtvs, and trying to reduce it otherwise.
1415 The point here is that it's generally OK to have too few qtvs; that is,
1416 to make the thing more monomorphic than it could be. We don't want to
1417 do that in the common cases, but in wierd cases it's ok: the programmer
1418 can always add a signature.
1420 Too few qtvs => too many wanteds, which is what happens if you do less
1425 tcSimplifyRestricted -- Used for restricted binding groups
1426 -- i.e. ones subject to the monomorphism restriction
1429 -> [Name] -- Things bound in this group
1430 -> TcTyVarSet -- Free in the type of the RHSs
1431 -> [Inst] -- Free in the RHSs
1432 -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
1433 TcDictBinds) -- Bindings
1434 -- tcSimpifyRestricted returns no constraints to
1435 -- quantify over; by definition there are none.
1436 -- They are all thrown back in the LIE
1438 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1439 -- Zonk everything in sight
1440 = do { traceTc (text "tcSimplifyRestricted")
1441 ; wanteds_z <- zonkInsts wanteds
1443 -- 'ReduceMe': Reduce as far as we can. Don't stop at
1444 -- dicts; the idea is to get rid of as many type
1445 -- variables as possible, and we don't want to stop
1446 -- at (say) Monad (ST s), because that reduces
1447 -- immediately, with no constraint on s.
1449 -- BUT do no improvement! See Plan D above
1450 -- HOWEVER, some unification may take place, if we instantiate
1451 -- a method Inst with an equality constraint
1452 ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
1453 ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z
1455 -- Next, figure out the tyvars we will quantify over
1456 ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
1457 ; gbl_tvs' <- tcGetGlobalTyVars
1458 ; constrained_dicts' <- zonkInsts constrained_dicts
1460 ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
1461 -- As in tcSimplifyInfer
1463 -- Do not quantify over constrained type variables:
1464 -- this is the monomorphism restriction
1465 constrained_tvs' = tyVarsOfInsts constrained_dicts'
1466 qtvs = qtvs1 `minusVarSet` constrained_tvs'
1467 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
1470 ; warn_mono <- doptM Opt_WarnMonomorphism
1471 ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
1472 (vcat[ ptext (sLit "the Monomorphism Restriction applies to the binding")
1473 <> plural bndrs <+> ptext (sLit "for") <+> pp_bndrs,
1474 ptext (sLit "Consider giving a type signature for") <+> pp_bndrs])
1476 ; traceTc (text "tcSimplifyRestricted" <+> vcat [
1477 pprInsts wanteds, pprInsts constrained_dicts',
1479 ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
1481 -- Zonk wanteds again! The first call to reduceContext may have
1482 -- instantiated some variables.
1483 -- FIXME: If red_improve would work, we could propagate that into
1484 -- the equality solver, too, to prevent instantating any
1486 ; wanteds_zz <- zonkInsts wanteds_z
1488 -- The first step may have squashed more methods than
1489 -- necessary, so try again, this time more gently, knowing the exact
1490 -- set of type variables to quantify over.
1492 -- We quantify only over constraints that are captured by qtvs;
1493 -- these will just be a subset of non-dicts. This in contrast
1494 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1495 -- all *non-inheritable* constraints too. This implements choice
1496 -- (B) under "implicit parameter and monomorphism" above.
1498 -- Remember that we may need to do *some* simplification, to
1499 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1500 -- just to float all constraints
1502 -- At top level, we *do* squash methods becuase we want to
1503 -- expose implicit parameters to the test that follows
1504 ; let is_nested_group = isNotTopLevel top_lvl
1505 try_me inst | isFreeWrtTyVars qtvs inst,
1506 (is_nested_group || isDict inst) = Stop
1507 | otherwise = ReduceMe
1508 env = mkNoImproveRedEnv doc try_me
1509 ; (_imp, binds, irreds) <- reduceContext env wanteds_zz
1511 -- See "Notes on implicit parameters, Question 4: top level"
1512 ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
1513 if is_nested_group then
1515 else do { let (bad_ips, non_ips) = partition isIPDict irreds
1516 ; addTopIPErrs bndrs bad_ips
1517 ; extendLIEs non_ips }
1519 ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
1520 ; return (qtvs', binds) }
1524 %************************************************************************
1528 %************************************************************************
1530 On the LHS of transformation rules we only simplify methods and constants,
1531 getting dictionaries. We want to keep all of them unsimplified, to serve
1532 as the available stuff for the RHS of the rule.
1534 Example. Consider the following left-hand side of a rule
1536 f (x == y) (y > z) = ...
1538 If we typecheck this expression we get constraints
1540 d1 :: Ord a, d2 :: Eq a
1542 We do NOT want to "simplify" to the LHS
1544 forall x::a, y::a, z::a, d1::Ord a.
1545 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1549 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1550 f ((==) d2 x y) ((>) d1 y z) = ...
1552 Here is another example:
1554 fromIntegral :: (Integral a, Num b) => a -> b
1555 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1557 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1558 we *dont* want to get
1560 forall dIntegralInt.
1561 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1563 because the scsel will mess up RULE matching. Instead we want
1565 forall dIntegralInt, dNumInt.
1566 fromIntegral Int Int dIntegralInt dNumInt = id Int
1570 g (x == y) (y == z) = ..
1572 where the two dictionaries are *identical*, we do NOT WANT
1574 forall x::a, y::a, z::a, d1::Eq a
1575 f ((==) d1 x y) ((>) d1 y z) = ...
1577 because that will only match if the dict args are (visibly) equal.
1578 Instead we want to quantify over the dictionaries separately.
1580 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1581 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1582 from scratch, rather than further parameterise simpleReduceLoop etc.
1583 Simpler, maybe, but alas not simple (see Trac #2494)
1585 * Type errors may give rise to an (unsatisfiable) equality constraint
1587 * Applications of a higher-rank function on the LHS may give
1588 rise to an implication constraint, esp if there are unsatisfiable
1589 equality constraints inside.
1592 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1593 tcSimplifyRuleLhs wanteds
1594 = do { wanteds' <- zonkInsts wanteds
1595 ; (irreds, binds) <- go [] emptyBag wanteds'
1596 ; let (dicts, bad_irreds) = partition isDict irreds
1597 ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
1598 ; addNoInstanceErrs (nub bad_irreds)
1599 -- The nub removes duplicates, which has
1600 -- not happened otherwise (see notes above)
1601 ; return (dicts, binds) }
1603 go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
1605 = return (irreds, binds)
1606 go irreds binds (w:ws)
1608 = go (w:irreds) binds ws
1609 | isImplicInst w -- Have a go at reducing the implication
1610 = do { (binds1, irreds1) <- reduceImplication red_env w
1611 ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
1612 ; go (bad_irreds ++ irreds)
1613 (binds `unionBags` binds1)
1616 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1617 -- to fromInteger; this looks fragile to me
1618 ; lookup_result <- lookupSimpleInst w'
1619 ; case lookup_result of
1620 NoInstance -> go (w:irreds) binds ws
1621 GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
1623 binds' = addInstToDictBind binds w rhs
1626 -- Sigh: we need to reduce inside implications
1627 red_env = mkInferRedEnv doc try_me
1628 doc = ptext (sLit "Implication constraint in RULE lhs")
1629 try_me inst | isMethodOrLit inst = ReduceMe
1630 | otherwise = Stop -- Be gentle
1633 tcSimplifyBracket is used when simplifying the constraints arising from
1634 a Template Haskell bracket [| ... |]. We want to check that there aren't
1635 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1636 Show instance), but we aren't otherwise interested in the results.
1637 Nor do we care about ambiguous dictionaries etc. We will type check
1638 this bracket again at its usage site.
1641 tcSimplifyBracket :: [Inst] -> TcM ()
1642 tcSimplifyBracket wanteds
1643 = do { tryHardCheckLoop doc wanteds
1646 doc = text "tcSimplifyBracket"
1650 %************************************************************************
1652 \subsection{Filtering at a dynamic binding}
1654 %************************************************************************
1659 we must discharge all the ?x constraints from B. We also do an improvement
1660 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1662 Actually, the constraints from B might improve the types in ?x. For example
1664 f :: (?x::Int) => Char -> Char
1667 then the constraint (?x::Int) arising from the call to f will
1668 force the binding for ?x to be of type Int.
1671 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1674 -- We need a loop so that we do improvement, and then
1675 -- (next time round) generate a binding to connect the two
1677 -- Here the two ?x's have different types, and improvement
1678 -- makes them the same.
1680 tcSimplifyIPs given_ips wanteds
1681 = do { wanteds' <- zonkInsts wanteds
1682 ; given_ips' <- zonkInsts given_ips
1683 -- Unusually for checking, we *must* zonk the given_ips
1685 ; let env = mkRedEnv doc try_me given_ips'
1686 ; (improved, binds, irreds) <- reduceContext env wanteds'
1688 ; if null irreds || not improved then
1689 ASSERT( all is_free irreds )
1690 do { extendLIEs irreds
1693 -- If improvement did some unification, we go round again.
1694 -- We start again with irreds, not wanteds
1695 -- Using an instance decl might have introduced a fresh type
1696 -- variable which might have been unified, so we'd get an
1697 -- infinite loop if we started again with wanteds!
1699 { binds1 <- tcSimplifyIPs given_ips' irreds
1700 ; return $ binds `unionBags` binds1
1703 doc = text "tcSimplifyIPs" <+> ppr given_ips
1704 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1705 is_free inst = isFreeWrtIPs ip_set inst
1707 -- Simplify any methods that mention the implicit parameter
1708 try_me inst | is_free inst = Stop
1709 | otherwise = ReduceMe
1713 %************************************************************************
1715 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1717 %************************************************************************
1719 When doing a binding group, we may have @Insts@ of local functions.
1720 For example, we might have...
1722 let f x = x + 1 -- orig local function (overloaded)
1723 f.1 = f Int -- two instances of f
1728 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1729 where @f@ is in scope; those @Insts@ must certainly not be passed
1730 upwards towards the top-level. If the @Insts@ were binding-ified up
1731 there, they would have unresolvable references to @f@.
1733 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1734 For each method @Inst@ in the @init_lie@ that mentions one of the
1735 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1736 @LIE@), as well as the @HsBinds@ generated.
1739 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1740 -- Simlifies only MethodInsts, and generate only bindings of form
1742 -- We're careful not to even generate bindings of the form
1744 -- You'd think that'd be fine, but it interacts with what is
1745 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1747 bindInstsOfLocalFuns wanteds local_ids
1748 | null overloaded_ids = do
1751 return emptyLHsBinds
1754 = do { (irreds, binds) <- gentleInferLoop doc for_me
1755 ; extendLIEs not_for_me
1759 doc = text "bindInsts" <+> ppr local_ids
1760 overloaded_ids = filter is_overloaded local_ids
1761 is_overloaded id = isOverloadedTy (idType id)
1762 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1764 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1765 -- so it's worth building a set, so that
1766 -- lookup (in isMethodFor) is faster
1770 %************************************************************************
1772 \subsection{Data types for the reduction mechanism}
1774 %************************************************************************
1776 The main control over context reduction is here
1780 = RedEnv { red_doc :: SDoc -- The context
1781 , red_try_me :: Inst -> WhatToDo
1782 , red_improve :: Bool -- True <=> do improvement
1783 , red_givens :: [Inst] -- All guaranteed rigid
1784 -- Always dicts & equalities
1785 -- but see Note [Rigidity]
1787 , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
1788 -- See Note [RedStack]
1792 -- The red_givens are rigid so far as cmpInst is concerned.
1793 -- There is one case where they are not totally rigid, namely in tcSimplifyIPs
1794 -- let ?x = e in ...
1795 -- Here, the given is (?x::a), where 'a' is not necy a rigid type
1796 -- But that doesn't affect the comparison, which is based only on mame.
1799 -- The red_stack pair (n,insts) pair is just used for error reporting.
1800 -- 'n' is always the depth of the stack.
1801 -- The 'insts' is the stack of Insts being reduced: to produce X
1802 -- I had to produce Y, to produce Y I had to produce Z, and so on.
1805 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
1806 mkRedEnv doc try_me givens
1807 = RedEnv { red_doc = doc, red_try_me = try_me,
1808 red_givens = givens,
1810 red_improve = True }
1812 mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
1814 mkInferRedEnv doc try_me
1815 = RedEnv { red_doc = doc, red_try_me = try_me,
1818 red_improve = True }
1820 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
1821 -- Do not do improvement; no givens
1822 mkNoImproveRedEnv doc try_me
1823 = RedEnv { red_doc = doc, red_try_me = try_me,
1826 red_improve = True }
1829 = ReduceMe -- Try to reduce this
1830 -- If there's no instance, add the inst to the
1831 -- irreductible ones, but don't produce an error
1832 -- message of any kind.
1833 -- It might be quite legitimate such as (Eq a)!
1835 | Stop -- Return as irreducible unless it can
1836 -- be reduced to a constant in one step
1837 -- Do not add superclasses; see
1839 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1840 -- of a predicate when adding it to the avails
1841 -- The reason for this flag is entirely the super-class loop problem
1842 -- Note [SUPER-CLASS LOOP 1]
1844 zonkRedEnv :: RedEnv -> TcM RedEnv
1846 = do { givens' <- mapM zonkInst (red_givens env)
1847 ; return $ env {red_givens = givens'}
1852 %************************************************************************
1854 \subsection[reduce]{@reduce@}
1856 %************************************************************************
1858 Note [Ancestor Equalities]
1859 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1860 During context reduction, we add to the wanted equalities also those
1861 equalities that (transitively) occur in superclass contexts of wanted
1862 class constraints. Consider the following code
1864 class a ~ Int => C a
1867 If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
1868 substituting Int for a. Hence, we ultimately want (C Int), which we
1869 discharge with the explicit instance.
1872 reduceContext :: RedEnv
1874 -> TcM (ImprovementDone,
1875 TcDictBinds, -- Dictionary bindings
1876 [Inst]) -- Irreducible
1878 reduceContext env wanteds0
1879 = do { traceTc (text "reduceContext" <+> (vcat [
1880 text "----------------------",
1882 text "given" <+> ppr (red_givens env),
1883 text "wanted" <+> ppr wanteds0,
1884 text "----------------------"
1887 -- We want to add as wanted equalities those that (transitively)
1888 -- occur in superclass contexts of wanted class constraints.
1889 -- See Note [Ancestor Equalities]
1890 ; ancestor_eqs <- ancestorEqualities wanteds0
1891 ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
1893 -- Normalise and solve all equality constraints as far as possible
1894 -- and normalise all dictionary constraints wrt to the reduced
1895 -- equalities. The returned wanted constraints include the
1896 -- irreducible wanted equalities.
1897 ; let wanteds = wanteds0 ++ ancestor_eqs
1898 givens = red_givens env
1902 eq_improved) <- tcReduceEqs givens wanteds
1903 ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
1904 [ppr givens', ppr wanteds', ppr normalise_binds]
1906 -- Build the Avail mapping from "given_dicts"
1907 ; (init_state, _) <- getLIE $ do
1908 { init_state <- foldlM addGiven emptyAvails givens'
1912 -- Solve the *wanted* *dictionary* constraints (not implications)
1913 -- This may expose some further equational constraints in the course
1914 -- of improvement due to functional dependencies if any of the
1915 -- involved unifications gets deferred.
1916 ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
1917 ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
1918 -- The getLIE is reqd because reduceList does improvement
1919 -- (via extendAvails) which may in turn do unification
1922 dict_irreds) <- extractResults avails wanted_dicts
1923 ; traceTc $ text "reduceContext: extractResults" <+> vcat
1924 [ppr avails, ppr wanted_dicts, ppr dict_binds]
1926 -- Solve the wanted *implications*. In doing so, we can provide
1927 -- as "given" all the dicts that were originally given,
1928 -- *or* for which we now have bindings,
1929 -- *or* which are now irreds
1930 -- NB: Equality irreds need to be converted, as the recursive
1931 -- invocation of the solver will still treat them as wanteds
1933 ; let implic_env = env { red_givens
1934 = givens ++ bound_dicts ++
1935 map wantedToLocalEqInst dict_irreds }
1936 ; (implic_binds_s, implic_irreds_s)
1937 <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
1938 ; let implic_binds = unionManyBags implic_binds_s
1939 implic_irreds = concat implic_irreds_s
1941 -- Collect all irreducible instances, and determine whether we should
1942 -- go round again. We do so in either of two cases:
1943 -- (1) If dictionary reduction or equality solving led to
1944 -- improvement (i.e., instantiated type variables).
1945 -- (2) If we reduced dictionaries (i.e., got dictionary bindings),
1946 -- they may have exposed further opportunities to normalise
1947 -- family applications. See Note [Dictionary Improvement]
1949 -- NB: We do *not* go around for new extra_eqs. Morally, we should,
1950 -- but we can't without risking non-termination (see #2688). By
1951 -- not going around, we miss some legal programs mixing FDs and
1952 -- TFs, but we never claimed to support such programs in the
1953 -- current implementation anyway.
1955 ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs
1956 avails_improved = availsImproved avails
1957 improvedFlexible = avails_improved || eq_improved
1958 reduced_dicts = not (isEmptyBag dict_binds)
1959 improved = improvedFlexible || reduced_dicts
1961 improvedHint = (if avails_improved then " [AVAILS]" else "") ++
1962 (if eq_improved then " [EQ]" else "")
1964 ; traceTc (text "reduceContext end" <+> (vcat [
1965 text "----------------------",
1967 text "given" <+> ppr givens,
1968 text "wanted" <+> ppr wanteds0,
1970 text "avails" <+> pprAvails avails,
1971 text "improved =" <+> ppr improved <+> text improvedHint,
1972 text "(all) irreds = " <+> ppr all_irreds,
1973 text "dict-binds = " <+> ppr dict_binds,
1974 text "implic-binds = " <+> ppr implic_binds,
1975 text "----------------------"
1979 normalise_binds `unionBags` dict_binds
1980 `unionBags` implic_binds,
1984 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
1985 tcImproveOne avails inst
1986 | not (isDict inst) = return False
1988 = do { inst_envs <- tcGetInstEnvs
1989 ; let eqns = improveOne (classInstances inst_envs)
1990 (dictPred inst, pprInstArising inst)
1991 [ (dictPred p, pprInstArising p)
1992 | p <- availsInsts avails, isDict p ]
1993 -- Avails has all the superclasses etc (good)
1994 -- It also has all the intermediates of the deduction (good)
1995 -- It does not have duplicates (good)
1996 -- NB that (?x::t1) and (?x::t2) will be held separately in
1997 -- avails so that improve will see them separate
1998 ; traceTc (text "improveOne" <+> ppr inst)
2001 unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))]
2002 -> TcM ImprovementDone
2003 unifyEqns [] = return False
2005 = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
2006 ; improved <- mapM unify eqns
2007 ; return $ or improved
2010 unify ((qtvs, pairs), what1, what2)
2011 = addErrCtxtM (mkEqnMsg what1 what2) $
2012 do { let freeTyVars = unionVarSets (map tvs_pr pairs)
2014 ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
2015 ; mapM_ (unif_pr tenv) pairs
2016 ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
2019 unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
2021 tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
2023 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
2024 pprEquationDoc (eqn, (p1, _), (p2, _))
2025 = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
2027 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
2028 -> TcM (TidyEnv, SDoc)
2029 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
2030 = do { pred1' <- zonkTcPredType pred1
2031 ; pred2' <- zonkTcPredType pred2
2032 ; let { pred1'' = tidyPred tidy_env pred1'
2033 ; pred2'' = tidyPred tidy_env pred2' }
2034 ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
2035 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
2036 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
2037 ; return (tidy_env, msg) }
2040 Note [Dictionary Improvement]
2041 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2042 In reduceContext, we first reduce equalities and then class constraints.
2043 However, the letter may expose further opportunities for the former. Hence,
2044 we need to go around again if dictionary reduction produced any dictionary
2045 bindings. The following example demonstrated the point:
2047 data EX _x _y (p :: * -> *)
2052 class Base (Def p) => Prop p where
2056 instance Prop () where
2059 instance (Base (Def (p ANY))) => Base (EX _x _y p)
2060 instance (Prop (p ANY)) => Prop (EX _x _y p) where
2061 type Def (EX _x _y p) = EX _x _y p
2064 instance Prop (FOO x) where
2065 type Def (FOO x) = ()
2068 instance Prop BAR where
2069 type Def BAR = EX () () FOO
2071 During checking the last instance declaration, we need to check the superclass
2072 cosntraint Base (Def BAR), which family normalisation reduced to
2073 Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us
2074 Base (Def (FOO ANY)), which again requires family normalisation of Def to
2075 Base () before we can finish.
2078 The main context-reduction function is @reduce@. Here's its game plan.
2081 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
2082 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
2083 = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
2085 ; when (debugIsOn && (n > 8)) $ do
2086 debugDumpTcRn (hang (ptext (sLit "Interesting! Context reduction stack depth") <+> int n)
2087 2 (ifPprDebug (nest 2 (pprStack stk))))
2088 ; if n >= ctxtStkDepth dopts then
2089 failWithTc (reduceDepthErr n stk)
2093 go [] state = return state
2094 go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
2097 -- Base case: we're done!
2098 reduce :: RedEnv -> Inst -> Avails -> TcM Avails
2099 reduce env wanted avails
2101 -- We don't reduce equalities here (and they must not end up as irreds
2106 -- It's the same as an existing inst, or a superclass thereof
2107 | Just _ <- findAvail avails wanted
2108 = do { traceTc (text "reduce: found " <+> ppr wanted)
2113 = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
2114 ; case red_try_me env wanted of {
2115 Stop -> try_simple (addIrred NoSCs);
2116 -- See Note [No superclasses for Stop]
2118 ReduceMe -> do -- It should be reduced
2119 { (avails, lookup_result) <- reduceInst env avails wanted
2120 ; case lookup_result of
2121 NoInstance -> addIrred AddSCs avails wanted
2122 -- Add it and its superclasses
2124 GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
2126 GenInst wanteds' rhs
2127 -> do { avails1 <- addIrred NoSCs avails wanted
2128 ; avails2 <- reduceList env wanteds' avails1
2129 ; addWanted AddSCs avails2 wanted rhs wanteds' } }
2130 -- Temporarily do addIrred *before* the reduceList,
2131 -- which has the effect of adding the thing we are trying
2132 -- to prove to the database before trying to prove the things it
2133 -- needs. See note [RECURSIVE DICTIONARIES]
2134 -- NB: we must not do an addWanted before, because that adds the
2135 -- superclasses too, and that can lead to a spurious loop; see
2136 -- the examples in [SUPERCLASS-LOOP]
2137 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
2140 -- First, see if the inst can be reduced to a constant in one step
2141 -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
2142 -- Don't bother for implication constraints, which take real work
2143 try_simple do_this_otherwise
2144 = do { res <- lookupSimpleInst wanted
2146 GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
2147 _ -> do_this_otherwise avails wanted }
2151 Note [RECURSIVE DICTIONARIES]
2152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2154 data D r = ZeroD | SuccD (r (D r));
2156 instance (Eq (r (D r))) => Eq (D r) where
2157 ZeroD == ZeroD = True
2158 (SuccD a) == (SuccD b) = a == b
2161 equalDC :: D [] -> D [] -> Bool;
2164 We need to prove (Eq (D [])). Here's how we go:
2168 by instance decl, holds if
2172 by instance decl of Eq, holds if
2174 where d2 = dfEqList d3
2177 But now we can "tie the knot" to give
2183 and it'll even run! The trick is to put the thing we are trying to prove
2184 (in this case Eq (D []) into the database before trying to prove its
2185 contributing clauses.
2187 Note [SUPERCLASS-LOOP 2]
2188 ~~~~~~~~~~~~~~~~~~~~~~~~
2189 We need to be careful when adding "the constaint we are trying to prove".
2190 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
2192 class Ord a => C a where
2193 instance Ord [a] => C [a] where ...
2195 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
2196 superclasses of C [a] to avails. But we must not overwrite the binding
2197 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
2200 Here's another variant, immortalised in tcrun020
2201 class Monad m => C1 m
2202 class C1 m => C2 m x
2203 instance C2 Maybe Bool
2204 For the instance decl we need to build (C1 Maybe), and it's no good if
2205 we run around and add (C2 Maybe Bool) and its superclasses to the avails
2206 before we search for C1 Maybe.
2208 Here's another example
2209 class Eq b => Foo a b
2210 instance Eq a => Foo [a] a
2214 we'll first deduce that it holds (via the instance decl). We must not
2215 then overwrite the Eq t constraint with a superclass selection!
2217 At first I had a gross hack, whereby I simply did not add superclass constraints
2218 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
2219 becuase it lost legitimate superclass sharing, and it still didn't do the job:
2220 I found a very obscure program (now tcrun021) in which improvement meant the
2221 simplifier got two bites a the cherry... so something seemed to be an Stop
2222 first time, but reducible next time.
2224 Now we implement the Right Solution, which is to check for loops directly
2225 when adding superclasses. It's a bit like the occurs check in unification.
2229 %************************************************************************
2231 Reducing a single constraint
2233 %************************************************************************
2236 ---------------------------------------------
2237 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
2238 reduceInst _ avails other_inst
2239 = do { result <- lookupSimpleInst other_inst
2240 ; return (avails, result) }
2243 Note [Equational Constraints in Implication Constraints]
2244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2246 An implication constraint is of the form
2248 where Given and Wanted may contain both equational and dictionary
2249 constraints. The delay and reduction of these two kinds of constraints
2252 -) In the generated code, wanted Dictionary constraints are wrapped up in an
2253 implication constraint that is created at the code site where the wanted
2254 dictionaries can be reduced via a let-binding. This let-bound implication
2255 constraint is deconstructed at the use-site of the wanted dictionaries.
2257 -) While the reduction of equational constraints is also delayed, the delay
2258 is not manifest in the generated code. The required evidence is generated
2259 in the code directly at the use-site. There is no let-binding and deconstruction
2260 necessary. The main disadvantage is that we cannot exploit sharing as the
2261 same evidence may be generated at multiple use-sites. However, this disadvantage
2262 is limited because it only concerns coercions which are erased.
2264 The different treatment is motivated by the different in representation. Dictionary
2265 constraints require manifest runtime dictionaries, while equations require coercions
2269 ---------------------------------------------
2270 reduceImplication :: RedEnv
2272 -> TcM (TcDictBinds, [Inst])
2275 Suppose we are simplifying the constraint
2276 forall bs. extras => wanted
2277 in the context of an overall simplification problem with givens 'givens'.
2280 * The 'givens' need not mention any of the quantified type variables
2281 e.g. forall {}. Eq a => Eq [a]
2282 forall {}. C Int => D (Tree Int)
2284 This happens when you have something like
2286 T1 :: Eq a => a -> T a
2289 f x = ...(case x of { T1 v -> v==v })...
2292 -- ToDo: should we instantiate tvs? I think it's not necessary
2294 -- Note on coercion variables:
2296 -- The extra given coercion variables are bound at two different
2299 -- -) in the creation context of the implication constraint
2300 -- the solved equational constraints use these binders
2302 -- -) at the solving site of the implication constraint
2303 -- the solved dictionaries use these binders;
2304 -- these binders are generated by reduceImplication
2306 -- Note [Binders for equalities]
2307 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2308 -- To reuse the binders of local/given equalities in the binders of
2309 -- implication constraints, it is crucial that these given equalities
2310 -- always have the form
2312 -- where cotv is a simple coercion type variable (and not a more
2313 -- complex coercion term). We require that the extra_givens always
2314 -- have this form and exploit the special form when generating binders.
2315 reduceImplication env
2316 orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
2318 tci_given = extra_givens, tci_wanted = wanteds
2320 = do { -- Solve the sub-problem
2321 ; let try_me _ = ReduceMe -- Note [Freeness and implications]
2322 env' = env { red_givens = extra_givens ++ red_givens env
2323 , red_doc = sep [ptext (sLit "reduceImplication for")
2325 nest 2 (parens $ ptext (sLit "within")
2327 , red_try_me = try_me }
2329 ; traceTc (text "reduceImplication" <+> vcat
2330 [ ppr (red_givens env), ppr extra_givens,
2332 ; (irreds, binds) <- checkLoop env' wanteds
2334 ; traceTc (text "reduceImplication result" <+> vcat
2335 [ppr irreds, ppr binds])
2337 ; -- extract superclass binds
2338 -- (sc_binds,_) <- extractResults avails []
2339 -- ; traceTc (text "reduceImplication sc_binds" <+> vcat
2340 -- [ppr sc_binds, ppr avails])
2343 -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
2344 -- Then we must iterate the outer loop too!
2346 ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
2347 -- we solve wanted eqs by side effect!
2349 -- Progress is no longer measered by the number of bindings
2350 -- If there are any irreds, but no bindings and no solved
2351 -- equalities, we back off and do nothing
2352 ; let backOff = isEmptyLHsBinds binds && -- no new bindings
2353 (not $ null irreds) && -- but still some irreds
2354 didntSolveWantedEqs -- no instantiated cotv
2356 ; if backOff then -- No progress
2357 return (emptyBag, [orig_implic])
2359 { (simpler_implic_insts, bind)
2360 <- makeImplicationBind inst_loc tvs extra_givens irreds
2361 -- This binding is useless if the recursive simplification
2362 -- made no progress; but currently we don't try to optimise that
2363 -- case. After all, we only try hard to reduce at top level, or
2364 -- when inferring types.
2366 ; let -- extract Id binders for dicts and CoTyVar binders for eqs;
2367 -- see Note [Binders for equalities]
2368 (extra_eq_givens, extra_dict_givens) = partition isEqInst
2370 eq_cotvs = map instToVar extra_eq_givens
2371 dict_ids = map instToId extra_dict_givens
2373 -- Note [Always inline implication constraints]
2374 wrap_inline | null dict_ids = idHsWrapper
2375 | otherwise = WpInline
2378 <.> mkWpTyLams eq_cotvs
2379 <.> mkWpLams dict_ids
2380 <.> WpLet (binds `unionBags` bind)
2381 rhs = mkLHsWrap co payload
2382 loc = instLocSpan inst_loc
2383 -- wanted equalities are solved by updating their
2384 -- cotv; we don't generate bindings for them
2385 dict_bndrs = map (L loc . HsVar . instToId)
2386 . filter (not . isEqInst)
2388 payload = mkBigLHsTup dict_bndrs
2391 ; traceTc (vcat [text "reduceImplication" <+> ppr name,
2392 ppr simpler_implic_insts,
2393 text "->" <+> ppr rhs])
2394 ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),
2395 simpler_implic_insts)
2398 reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
2401 Note [Always inline implication constraints]
2402 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2403 Suppose an implication constraint floats out of an INLINE function.
2404 Then although the implication has a single call site, it won't be
2405 inlined. And that is bad because it means that even if there is really
2406 *no* overloading (type signatures specify the exact types) there will
2407 still be dictionary passing in the resulting code. To avert this,
2408 we mark the implication constraints themselves as INLINE, at least when
2409 there is no loss of sharing as a result.
2411 Note [Freeness and implications]
2412 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2413 It's hard to say when an implication constraint can be floated out. Consider
2414 forall {} Eq a => Foo [a]
2415 The (Foo [a]) doesn't mention any of the quantified variables, but it
2416 still might be partially satisfied by the (Eq a).
2418 There is a useful special case when it *is* easy to partition the
2419 constraints, namely when there are no 'givens'. Consider
2420 forall {a}. () => Bar b
2421 There are no 'givens', and so there is no reason to capture (Bar b).
2422 We can let it float out. But if there is even one constraint we
2423 must be much more careful:
2424 forall {a}. C a b => Bar (m b)
2425 because (C a b) might have a superclass (D b), from which we might
2426 deduce (Bar [b]) when m later gets instantiated to []. Ha!
2428 Here is an even more exotic example
2430 Now consider the constraint
2431 forall b. D Int b => C Int
2432 We can satisfy the (C Int) from the superclass of D, so we don't want
2433 to float the (C Int) out, even though it mentions no type variable in
2436 One more example: the constraint
2438 instance (C a, E c) => E (a,c)
2440 constraint: forall b. D Int b => E (Int,c)
2442 You might think that the (D Int b) can't possibly contribute
2443 to solving (E (Int,c)), since the latter mentions 'c'. But
2444 in fact it can, because solving the (E (Int,c)) constraint needs
2447 and the (C Int) can be satisfied from the superclass of (D Int b).
2448 So we must still not float (E (Int,c)) out.
2450 To think about: special cases for unary type classes?
2452 Note [Pruning the givens in an implication constraint]
2453 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2454 Suppose we are about to form the implication constraint
2455 forall tvs. Eq a => Ord b
2456 The (Eq a) cannot contribute to the (Ord b), because it has no access to
2457 the type variable 'b'. So we could filter out the (Eq a) from the givens.
2458 But BE CAREFUL of the examples above in [Freeness and implications].
2460 Doing so would be a bit tidier, but all the implication constraints get
2461 simplified away by the optimiser, so it's no great win. So I don't take
2462 advantage of that at the moment.
2464 If you do, BE CAREFUL of wobbly type variables.
2467 %************************************************************************
2469 Avails and AvailHow: the pool of evidence
2471 %************************************************************************
2475 data Avails = Avails !ImprovementDone !AvailEnv
2477 type ImprovementDone = Bool -- True <=> some unification has happened
2478 -- so some Irreds might now be reducible
2479 -- keys that are now
2481 type AvailEnv = FiniteMap Inst AvailHow
2483 = IsIrred -- Used for irreducible dictionaries,
2484 -- which are going to be lambda bound
2486 | Given Inst -- Used for dictionaries for which we have a binding
2487 -- e.g. those "given" in a signature
2489 | Rhs -- Used when there is a RHS
2490 (LHsExpr TcId) -- The RHS
2491 [Inst] -- Insts free in the RHS; we need these too
2493 instance Outputable Avails where
2496 pprAvails :: Avails -> SDoc
2497 pprAvails (Avails imp avails)
2498 = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
2500 vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
2501 | (inst,avail) <- fmToList avails ]]
2503 instance Outputable AvailHow where
2506 -------------------------
2507 pprAvail :: AvailHow -> SDoc
2508 pprAvail IsIrred = text "Irred"
2509 pprAvail (Given x) = text "Given" <+> ppr x
2510 pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
2513 -------------------------
2514 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
2515 extendAvailEnv env inst avail = addToFM env inst avail
2517 findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
2518 findAvailEnv env wanted = lookupFM env wanted
2519 -- NB 1: the Ord instance of Inst compares by the class/type info
2520 -- *not* by unique. So
2521 -- d1::C Int == d2::C Int
2523 emptyAvails :: Avails
2524 emptyAvails = Avails False emptyFM
2526 findAvail :: Avails -> Inst -> Maybe AvailHow
2527 findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
2529 elemAvails :: Inst -> Avails -> Bool
2530 elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
2532 extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
2534 extendAvails avails@(Avails imp env) inst avail
2535 = do { imp1 <- tcImproveOne avails inst -- Do any improvement
2536 ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
2538 availsInsts :: Avails -> [Inst]
2539 availsInsts (Avails _ avails) = keysFM avails
2541 availsImproved :: Avails -> ImprovementDone
2542 availsImproved (Avails imp _) = imp
2545 Extracting the bindings from a bunch of Avails.
2546 The bindings do *not* come back sorted in dependency order.
2547 We assume that they'll be wrapped in a big Rec, so that the
2548 dependency analyser can sort them out later
2551 type DoneEnv = FiniteMap Inst [Id]
2552 -- Tracks which things we have evidence for
2554 extractResults :: Avails
2556 -> TcM (TcDictBinds, -- Bindings
2557 [Inst], -- The insts bound by the bindings
2558 [Inst]) -- Irreducible ones
2559 -- Note [Reducing implication constraints]
2561 extractResults (Avails _ avails) wanteds
2562 = go emptyBag [] [] emptyFM wanteds
2564 go :: TcDictBinds -- Bindings for dicts
2565 -> [Inst] -- Bound by the bindings
2567 -> DoneEnv -- Has an entry for each inst in the above three sets
2569 -> TcM (TcDictBinds, [Inst], [Inst])
2570 go binds bound_dicts irreds _ []
2571 = return (binds, bound_dicts, irreds)
2573 go binds bound_dicts irreds done (w:ws)
2575 = go binds bound_dicts (w:irreds) done' ws
2577 | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
2578 = if w_id `elem` done_ids then
2579 go binds bound_dicts irreds done ws
2581 go (add_bind (nlHsVar done_id)) bound_dicts irreds
2582 (addToFM done w (done_id : w_id : rest_done_ids)) ws
2584 | otherwise -- Not yet done
2585 = case findAvailEnv avails w of
2586 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
2587 go binds bound_dicts irreds done ws
2589 Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
2591 Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
2593 Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws
2596 binds' | w_id == g_id = binds
2597 | otherwise = add_bind (nlHsVar g_id)
2600 done' = addToFM done w [w_id]
2601 add_bind rhs = addInstToDictBind binds w rhs
2605 Note [No superclasses for Stop]
2606 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2607 When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
2608 add it to avails, so that any other equal Insts will be commoned up
2609 right here. However, we do *not* add superclasses. If we have
2612 but a is not bound here, then we *don't* want to derive dn from df
2613 here lest we lose sharing.
2616 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
2617 addWanted want_scs avails wanted rhs_expr wanteds
2618 = addAvailAndSCs want_scs avails wanted avail
2620 avail = Rhs rhs_expr wanteds
2622 addGiven :: Avails -> Inst -> TcM Avails
2623 addGiven avails given
2624 = addAvailAndSCs want_scs avails given (Given given)
2626 want_scs = case instLocOrigin (instLoc given) of
2629 -- Conditionally add superclasses for 'given'
2630 -- See Note [Recursive instances and superclases]
2632 -- No ASSERT( not (given `elemAvails` avails) ) because in an
2633 -- instance decl for Ord t we can add both Ord t and Eq t as
2634 -- 'givens', so the assert isn't true
2638 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
2639 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
2640 addAvailAndSCs want_scs avails irred IsIrred
2642 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
2643 addAvailAndSCs want_scs avails inst avail
2644 | not (isClassDict inst) = extendAvails avails inst avail
2645 | NoSCs <- want_scs = extendAvails avails inst avail
2646 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
2647 ; avails' <- extendAvails avails inst avail
2648 ; addSCs is_loop avails' inst }
2650 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
2651 -- Note: this compares by *type*, not by Unique
2652 deps = findAllDeps (unitVarSet (instToVar inst)) avail
2653 dep_tys = map idType (varSetElems deps)
2655 findAllDeps :: IdSet -> AvailHow -> IdSet
2656 -- Find all the Insts that this one depends on
2657 -- See Note [SUPERCLASS-LOOP 2]
2658 -- Watch out, though. Since the avails may contain loops
2659 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
2660 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
2661 findAllDeps so_far _ = so_far
2663 find_all :: IdSet -> Inst -> IdSet
2665 | isEqInst kid = so_far
2666 | kid_id `elemVarSet` so_far = so_far
2667 | Just avail <- findAvail avails kid = findAllDeps so_far' avail
2668 | otherwise = so_far'
2670 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
2671 kid_id = instToId kid
2673 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
2674 -- Add all the superclasses of the Inst to Avails
2675 -- The first param says "don't do this because the original thing
2676 -- depends on this one, so you'd build a loop"
2677 -- Invariant: the Inst is already in Avails.
2679 addSCs is_loop avails dict
2680 = ASSERT( isDict dict )
2681 do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
2682 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
2684 (clas, tys) = getDictClassTys dict
2685 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
2686 sc_theta' = filter (not . isEqPred) $
2687 substTheta (zipTopTvSubst tyvars tys) sc_theta
2689 add_sc avails (sc_dict, sc_sel)
2690 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
2691 | is_given sc_dict = return avails
2692 | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
2693 ; addSCs is_loop avails' sc_dict }
2695 sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
2696 co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys
2698 is_given :: Inst -> Bool
2699 is_given sc_dict = case findAvail avails sc_dict of
2700 Just (Given _) -> True -- Given is cheaper than superclass selection
2703 -- From the a set of insts obtain all equalities that (transitively) occur in
2704 -- superclass contexts of class constraints (aka the ancestor equalities).
2706 ancestorEqualities :: [Inst] -> TcM [Inst]
2708 = mapM mkWantedEqInst -- turn only equality predicates..
2709 . filter isEqPred -- ..into wanted equality insts
2711 . addAEsToBag emptyBag -- collect the superclass constraints..
2712 . map dictPred -- ..of all predicates in a bag
2713 . filter isClassDict
2715 addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
2716 addAEsToBag bag [] = bag
2717 addAEsToBag bag (pred:preds)
2718 | pred `elemBag` bag = addAEsToBag bag preds
2719 | isEqPred pred = addAEsToBag bagWithPred preds
2720 | isClassPred pred = addAEsToBag bagWithPred predsWithSCs
2721 | otherwise = addAEsToBag bag preds
2723 bagWithPred = bag `snocBag` pred
2724 predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
2726 (tyvars, sc_theta, _, _) = classBigSig clas
2727 (clas, tys) = getClassPredTys pred
2731 %************************************************************************
2733 \section{tcSimplifyTop: defaulting}
2735 %************************************************************************
2738 @tcSimplifyTop@ is called once per module to simplify all the constant
2739 and ambiguous Insts.
2741 We need to be careful of one case. Suppose we have
2743 instance Num a => Num (Foo a b) where ...
2745 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2746 to (Num x), and default x to Int. But what about y??
2748 It's OK: the final zonking stage should zap y to (), which is fine.
2752 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2753 tcSimplifyTop wanteds
2754 = tc_simplify_top doc False wanteds
2756 doc = text "tcSimplifyTop"
2758 tcSimplifyInteractive wanteds
2759 = tc_simplify_top doc True wanteds
2761 doc = text "tcSimplifyInteractive"
2763 -- The TcLclEnv should be valid here, solely to improve
2764 -- error message generation for the monomorphism restriction
2765 tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))
2766 tc_simplify_top doc interactive wanteds
2767 = do { dflags <- getDOpts
2768 ; wanteds <- zonkInsts wanteds
2769 ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
2771 ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
2772 ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
2773 -- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
2774 ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
2775 ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
2776 ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
2778 -- Use the defaulting rules to do extra unification
2779 -- NB: irreds2 are already zonked
2780 ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
2782 -- Deal with implicit parameters
2783 ; let (bad_ips, non_ips) = partition isIPDict irreds3
2784 (ambigs, others) = partition isTyVarDict non_ips
2786 ; topIPErrs bad_ips -- Can arise from f :: Int -> Int
2788 ; addNoInstanceErrs others
2789 ; addTopAmbigErrs ambigs
2791 ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
2793 doc1 = doc <+> ptext (sLit "(first round)")
2794 doc2 = doc <+> ptext (sLit "(approximate)")
2795 doc3 = doc <+> ptext (sLit "(disambiguate)")
2798 If a dictionary constrains a type variable which is
2799 * not mentioned in the environment
2800 * and not mentioned in the type of the expression
2801 then it is ambiguous. No further information will arise to instantiate
2802 the type variable; nor will it be generalised and turned into an extra
2803 parameter to a function.
2805 It is an error for this to occur, except that Haskell provided for
2806 certain rules to be applied in the special case of numeric types.
2808 * at least one of its classes is a numeric class, and
2809 * all of its classes are numeric or standard
2810 then the type variable can be defaulted to the first type in the
2811 default-type list which is an instance of all the offending classes.
2813 So here is the function which does the work. It takes the ambiguous
2814 dictionaries and either resolves them (producing bindings) or
2815 complains. It works by splitting the dictionary list by type
2816 variable, and using @disambigOne@ to do the real business.
2818 @disambigOne@ assumes that its arguments dictionaries constrain all
2819 the same type variable.
2821 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2822 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2823 the most common use of defaulting is code like:
2825 _ccall_ foo `seqPrimIO` bar
2827 Since we're not using the result of @foo@, the result if (presumably)
2831 disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
2832 -- Just does unification to fix the default types
2833 -- The Insts are assumed to be pre-zonked
2834 disambiguate doc interactive dflags insts
2836 = return (insts, emptyBag)
2838 | null defaultable_groups
2839 = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
2840 ; return (insts, emptyBag) }
2843 = do { -- Figure out what default types to use
2844 default_tys <- getDefaultTys extended_defaulting ovl_strings
2846 ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
2847 ; mapM_ (disambigGroup default_tys) defaultable_groups
2849 -- disambigGroup does unification, hence try again
2850 ; tryHardCheckLoop doc insts }
2853 extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
2854 ovl_strings = dopt Opt_OverloadedStrings dflags
2856 unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
2857 bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
2858 (unaries, bad_tvs_s) = partitionWith find_unary insts
2859 bad_tvs = unionVarSets bad_tvs_s
2861 -- Finds unary type-class constraints
2862 find_unary d@(Dict {tci_pred = ClassP cls [ty]})
2863 | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
2864 find_unary inst = Right (tyVarsOfInst inst)
2866 -- Group by type variable
2867 defaultable_groups :: [[(Inst,Class,TcTyVar)]]
2868 defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
2869 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
2871 defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
2872 defaultable_group ds@((_,_,tv):_)
2873 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
2874 && not (tv `elemVarSet` bad_tvs)
2875 && defaultable_classes [c | (_,c,_) <- ds]
2876 defaultable_group [] = panic "defaultable_group"
2878 defaultable_classes clss
2879 | extended_defaulting = any isInteractiveClass clss
2880 | otherwise = all is_std_class clss && (any is_num_class clss)
2882 -- In interactive mode, or with -XExtendedDefaultRules,
2883 -- we default Show a to Show () to avoid graututious errors on "show []"
2884 isInteractiveClass cls
2885 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2887 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2888 -- is_num_class adds IsString to the standard numeric classes,
2889 -- when -foverloaded-strings is enabled
2891 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2892 -- Similarly is_std_class
2894 -----------------------
2895 disambigGroup :: [Type] -- The default types
2896 -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
2897 -> TcM () -- Just does unification, to fix the default types
2899 disambigGroup default_tys dicts
2900 = try_default default_tys
2902 (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty
2903 classes = [c | (_,c,_) <- dicts]
2905 try_default [] = return ()
2906 try_default (default_ty : default_tys)
2907 = tryTcLIE_ (try_default default_tys) $
2908 do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
2909 -- This may fail; then the tryTcLIE_ kicks in
2910 -- Failure here is caused by there being no type in the
2911 -- default list which can satisfy all the ambiguous classes.
2912 -- For example, if Real a is reqd, but the only type in the
2913 -- default list is Int.
2915 -- After this we can't fail
2916 ; warnDefault dicts default_ty
2917 ; unifyType default_ty (mkTyVarTy tyvar)
2918 ; return () -- TOMDO: do something with the coercion
2922 -----------------------
2923 getDefaultTys :: Bool -> Bool -> TcM [Type]
2924 getDefaultTys extended_deflts ovl_strings
2925 = do { mb_defaults <- getDeclaredDefaultTys
2926 ; case mb_defaults of {
2927 Just tys -> return tys ; -- User-supplied defaults
2930 -- No use-supplied default
2931 -- Use [Integer, Double], plus modifications
2932 { integer_ty <- tcMetaTy integerTyConName
2933 ; checkWiredInTyCon doubleTyCon
2934 ; string_ty <- tcMetaTy stringTyConName
2935 ; return (opt_deflt extended_deflts unitTy
2936 -- Note [Default unitTy]
2938 [integer_ty,doubleTy]
2940 opt_deflt ovl_strings string_ty) } } }
2942 opt_deflt True ty = [ty]
2943 opt_deflt False _ = []
2946 Note [Default unitTy]
2947 ~~~~~~~~~~~~~~~~~~~~~
2948 In interative mode (or with -XExtendedDefaultRules) we add () as the first type we
2949 try when defaulting. This has very little real impact, except in the following case.
2951 Text.Printf.printf "hello"
2952 This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
2953 want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
2954 default the 'a' to (), rather than to Integer (which is what would otherwise happen;
2955 and then GHCi doesn't attempt to print the (). So in interactive mode, we add
2956 () to the list of defaulting types. See Trac #1200.
2958 Note [Avoiding spurious errors]
2959 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2960 When doing the unification for defaulting, we check for skolem
2961 type variables, and simply don't default them. For example:
2962 f = (*) -- Monomorphic
2963 g :: Num a => a -> a
2965 Here, we get a complaint when checking the type signature for g,
2966 that g isn't polymorphic enough; but then we get another one when
2967 dealing with the (Num a) context arising from f's definition;
2968 we try to unify a with Int (to default it), but find that it's
2969 already been unified with the rigid variable from g's type sig
2972 %************************************************************************
2974 \subsection[simple]{@Simple@ versions}
2976 %************************************************************************
2978 Much simpler versions when there are no bindings to make!
2980 @tcSimplifyThetas@ simplifies class-type constraints formed by
2981 @deriving@ declarations and when specialising instances. We are
2982 only interested in the simplified bunch of class/type constraints.
2984 It simplifies to constraints of the form (C a b c) where
2985 a,b,c are type variables. This is required for the context of
2986 instance declarations.
2989 tcSimplifyDeriv :: InstOrigin
2991 -> ThetaType -- Wanted
2992 -> TcM ThetaType -- Needed
2993 -- Given instance (wanted) => C inst_ty
2994 -- Simplify 'wanted' as much as possible
2996 tcSimplifyDeriv orig tyvars theta
2997 = do { (tvs, _, tenv) <- tcInstTyVars tyvars
2998 -- The main loop may do unification, and that may crash if
2999 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
3000 -- ToDo: what if two of them do get unified?
3001 ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
3002 ; (irreds, _) <- tryHardCheckLoop doc wanteds
3004 ; let (tv_dicts, others) = partition ok irreds
3005 (tidy_env, tidy_insts) = tidyInsts others
3006 ; reportNoInstances tidy_env Nothing [alt_fix] tidy_insts
3007 -- See Note [Exotic derived instance contexts] in TcMType
3009 ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
3010 simpl_theta = substTheta rev_env (map dictPred tv_dicts)
3011 -- This reverse-mapping is a pain, but the result
3012 -- should mention the original TyVars not TcTyVars
3014 ; return simpl_theta }
3016 doc = ptext (sLit "deriving classes for a data type")
3018 ok dict | isDict dict = validDerivPred (dictPred dict)
3020 alt_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration instead,"),
3021 ptext (sLit "so you can specify the instance context yourself")]
3025 @tcSimplifyDefault@ just checks class-type constraints, essentially;
3026 used with \tr{default} declarations. We are only interested in
3027 whether it worked or not.
3030 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
3033 tcSimplifyDefault theta = do
3034 wanteds <- newDictBndrsO DefaultOrigin theta
3035 (irreds, _) <- tryHardCheckLoop doc wanteds
3036 addNoInstanceErrs irreds
3040 traceTc (ptext (sLit "tcSimplifyDefault failing")) >> failM
3042 doc = ptext (sLit "default declaration")
3045 @tcSimplifyStagedExpr@ performs a simplification but does so at a new
3046 stage. This is used when typechecking annotations and splices.
3050 tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds)
3051 -- Type check an expression that runs at a top level stage as if
3052 -- it were going to be spliced and then simplify it
3053 tcSimplifyStagedExpr stage tc_action
3054 = setStage stage $ do {
3055 -- Typecheck the expression
3056 (thing', lie) <- getLIE tc_action
3058 -- Solve the constraints
3059 ; const_binds <- tcSimplifyTop lie
3061 ; return (thing', const_binds) }
3066 %************************************************************************
3068 \section{Errors and contexts}
3070 %************************************************************************
3072 ToDo: for these error messages, should we note the location as coming
3073 from the insts, or just whatever seems to be around in the monad just
3077 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
3078 -> [Inst] -- The offending Insts
3080 -- Group together insts with the same origin
3081 -- We want to report them together in error messages
3085 groupErrs report_err (inst:insts)
3086 = do { do_one (inst:friends)
3087 ; groupErrs report_err others }
3089 -- (It may seem a bit crude to compare the error messages,
3090 -- but it makes sure that we combine just what the user sees,
3091 -- and it avoids need equality on InstLocs.)
3092 (friends, others) = partition is_friend insts
3093 loc_msg = showSDoc (pprInstLoc (instLoc inst))
3094 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
3095 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
3096 -- Add location and context information derived from the Insts
3098 -- Add the "arising from..." part to a message about bunch of dicts
3099 addInstLoc :: [Inst] -> Message -> Message
3100 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
3102 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
3105 addTopIPErrs bndrs ips
3106 = do { dflags <- getDOpts
3107 ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
3109 (tidy_env, tidy_ips) = tidyInsts ips
3111 = vcat [sep [ptext (sLit "Implicit parameters escape from"),
3112 nest 2 (ptext (sLit "the monomorphic top-level binding")
3113 <> plural bndrs <+> ptext (sLit "of")
3114 <+> pprBinders bndrs <> colon)],
3115 nest 2 (vcat (map ppr_ip ips)),
3116 monomorphism_fix dflags]
3117 ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
3119 topIPErrs :: [Inst] -> TcM ()
3121 = groupErrs report tidy_dicts
3123 (tidy_env, tidy_dicts) = tidyInsts dicts
3124 report dicts = addErrTcM (tidy_env, mk_msg dicts)
3125 mk_msg dicts = addInstLoc dicts (ptext (sLit "Unbound implicit parameter") <>
3126 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
3128 addNoInstanceErrs :: [Inst] -- Wanted (can include implications)
3130 addNoInstanceErrs insts
3131 = do { let (tidy_env, tidy_insts) = tidyInsts insts
3132 ; reportNoInstances tidy_env Nothing [] tidy_insts }
3136 -> Maybe (InstLoc, [Inst]) -- Context
3137 -- Nothing => top level
3138 -- Just (d,g) => d describes the construct
3140 -> [SDoc] -- Alternative fix for no-such-instance
3141 -> [Inst] -- What is wanted (can include implications)
3144 reportNoInstances tidy_env mb_what alt_fix insts
3145 = groupErrs (report_no_instances tidy_env mb_what alt_fix) insts
3147 report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [SDoc] -> [Inst] -> TcM ()
3148 report_no_instances tidy_env mb_what alt_fixes insts
3149 = do { inst_envs <- tcGetInstEnvs
3150 ; let (implics, insts1) = partition isImplicInst insts
3151 (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
3152 (eqInsts, insts3) = partition isEqInst insts2
3153 ; traceTc (text "reportNoInstances" <+> vcat
3154 [ppr insts, ppr implics, ppr insts1, ppr insts2])
3155 ; mapM_ complain_implic implics
3156 ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
3157 ; groupErrs complain_no_inst insts3
3158 ; mapM_ (addErrTcM . mk_eq_err) eqInsts
3161 complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
3163 complain_implic inst -- Recurse!
3164 = reportNoInstances tidy_env
3165 (Just (tci_loc inst, tci_given inst))
3166 alt_fixes (tci_wanted inst)
3168 check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
3169 -- Right msg => overlap message
3170 -- Left inst => no instance
3171 check_overlap inst_envs wanted
3172 | not (isClassDict wanted) = Left wanted
3174 = case lookupInstEnv inst_envs clas tys of
3175 ([], _) -> Left wanted -- No match
3176 -- The case of exactly one match and no unifiers means a
3177 -- successful lookup. That can't happen here, because dicts
3178 -- only end up here if they didn't match in Inst.lookupInst
3180 | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
3181 res -> Right (mk_overlap_msg wanted res)
3183 (clas,tys) = getDictClassTys wanted
3185 mk_overlap_msg dict (matches, unifiers)
3186 = ASSERT( not (null matches) )
3187 vcat [ addInstLoc [dict] ((ptext (sLit "Overlapping instances for")
3188 <+> pprPred (dictPred dict))),
3189 sep [ptext (sLit "Matching instances") <> colon,
3190 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
3191 if not (isSingleton matches)
3192 then -- Two or more matches
3194 else -- One match, plus some unifiers
3195 ASSERT( not (null unifiers) )
3196 parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
3197 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
3198 ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
3199 ptext (sLit "when compiling the other instance declarations")])]
3201 ispecs = [ispec | (ispec, _) <- matches]
3203 mk_eq_err :: Inst -> (TidyEnv, SDoc)
3204 mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
3206 mk_no_inst_err insts
3207 | null insts = empty
3209 | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
3210 not (isEmptyVarSet (tyVarsOfInsts insts))
3211 = vcat [ addInstLoc insts $
3212 sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
3213 , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
3214 , show_fixes (fix1 loc : fixes2 ++ alt_fixes) ]
3216 | otherwise -- Top level
3217 = vcat [ addInstLoc insts $
3218 ptext (sLit "No instance") <> plural insts
3219 <+> ptext (sLit "for") <+> pprDictsTheta insts
3220 , show_fixes (fixes2 ++ alt_fixes) ]
3223 fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
3224 <+> ptext (sLit "to the context of"),
3225 nest 2 (ppr (instLocOrigin loc)) ]
3226 -- I'm not sure it helps to add the location
3227 -- nest 2 (ptext (sLit "at") <+> ppr (instLocSpan loc)) ]
3229 fixes2 | null instance_dicts = []
3230 | otherwise = [sep [ptext (sLit "add an instance declaration for"),
3231 pprDictsTheta instance_dicts]]
3232 instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
3233 -- Insts for which it is worth suggesting an adding an instance declaration
3234 -- Exclude implicit parameters, and tyvar dicts
3236 show_fixes :: [SDoc] -> SDoc
3237 show_fixes [] = empty
3238 show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"),
3239 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
3241 addTopAmbigErrs :: [Inst] -> TcRn ()
3242 addTopAmbigErrs dicts
3243 -- Divide into groups that share a common set of ambiguous tyvars
3244 = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened
3245 -- See Note [Avoiding spurious errors]
3246 mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
3248 (tidy_env, tidy_dicts) = tidyInsts dicts
3250 tvs_of :: Inst -> [TcTyVar]
3251 tvs_of d = varSetElems (tyVarsOfInst d)
3252 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
3254 report :: [(Inst,[TcTyVar])] -> TcM ()
3255 report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars
3256 (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
3257 setSrcSpan (instSpan inst) $
3258 -- the location of the first one will do for the err message
3259 addErrTcM (tidy_env, msg $$ mono_msg)
3261 dicts = map fst pairs
3262 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
3263 pprQuotedList tvs <+> in_msg,
3264 nest 2 (pprDictsInFull dicts)]
3265 in_msg = text "in the constraint" <> plural dicts <> colon
3266 report [] = panic "addTopAmbigErrs"
3269 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
3270 -- There's an error with these Insts; if they have free type variables
3271 -- it's probably caused by the monomorphism restriction.
3272 -- Try to identify the offending variable
3273 -- ASSUMPTION: the Insts are fully zonked
3274 mkMonomorphismMsg tidy_env inst_tvs
3275 = do { dflags <- getDOpts
3276 ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
3277 ; return (tidy_env, mk_msg dflags docs) }
3279 mk_msg _ _ | any isRuntimeUnk inst_tvs
3280 = vcat [ptext (sLit "Cannot resolve unknown runtime types:") <+>
3281 (pprWithCommas ppr inst_tvs),
3282 ptext (sLit "Use :print or :force to determine these types")]
3283 mk_msg _ [] = ptext (sLit "Probable fix: add a type signature that fixes these type variable(s)")
3284 -- This happens in things like
3285 -- f x = show (read "foo")
3286 -- where monomorphism doesn't play any role
3288 = vcat [ptext (sLit "Possible cause: the monomorphism restriction applied to the following:"),
3290 monomorphism_fix dflags]
3292 monomorphism_fix :: DynFlags -> SDoc
3293 monomorphism_fix dflags
3294 = ptext (sLit "Probable fix:") <+> vcat
3295 [ptext (sLit "give these definition(s) an explicit type signature"),
3296 if dopt Opt_MonomorphismRestriction dflags
3297 then ptext (sLit "or use -XNoMonomorphismRestriction")
3298 else empty] -- Only suggest adding "-XNoMonomorphismRestriction"
3299 -- if it is not already set!
3301 warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()
3302 warnDefault ups default_ty = do
3303 warn_flag <- doptM Opt_WarnTypeDefaults
3304 addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
3306 dicts = [d | (d,_,_) <- ups]
3309 (_, tidy_dicts) = tidyInsts dicts
3310 warn_msg = vcat [ptext (sLit "Defaulting the following constraint(s) to type") <+>
3311 quotes (ppr default_ty),
3312 pprDictsInFull tidy_dicts]
3314 reduceDepthErr :: Int -> [Inst] -> SDoc
3315 reduceDepthErr n stack
3316 = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
3317 ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
3318 nest 4 (pprStack stack)]
3320 pprStack :: [Inst] -> SDoc
3321 pprStack stack = vcat (map pprInstInFull stack)