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,
18 bindInstsOfLocalFuns, bindIrreds,
21 #include "HsVersions.h"
23 import {-# SOURCE #-} TcUnify( unifyType )
60 %************************************************************************
64 %************************************************************************
66 --------------------------------------
67 Notes on functional dependencies (a bug)
68 --------------------------------------
75 instance D a b => C a b -- Undecidable
76 -- (Not sure if it's crucial to this eg)
77 f :: C a b => a -> Bool
80 g :: C a b => a -> Bool
83 Here f typechecks, but g does not!! Reason: before doing improvement,
84 we reduce the (C a b1) constraint from the call of f to (D a b1).
86 Here is a more complicated example:
88 | > class Foo a b | a->b
90 | > class Bar a b | a->b
94 | > instance Bar Obj Obj
96 | > instance (Bar a b) => Foo a b
98 | > foo:: (Foo a b) => a -> String
101 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
107 | Could not deduce (Bar a b) from the context (Foo a b)
108 | arising from use of `foo' at <interactive>:1
110 | Add (Bar a b) to the expected type of an expression
111 | In the first argument of `runFoo', namely `foo'
112 | In the definition of `it': it = runFoo foo
114 | Why all of the sudden does GHC need the constraint Bar a b? The
115 | function foo didn't ask for that...
117 The trouble is that to type (runFoo foo), GHC has to solve the problem:
119 Given constraint Foo a b
120 Solve constraint Foo a b'
122 Notice that b and b' aren't the same. To solve this, just do
123 improvement and then they are the same. But GHC currently does
128 That is usually fine, but it isn't here, because it sees that Foo a b is
129 not the same as Foo a b', and so instead applies the instance decl for
130 instance Bar a b => Foo a b. And that's where the Bar constraint comes
133 The Right Thing is to improve whenever the constraint set changes at
134 all. Not hard in principle, but it'll take a bit of fiddling to do.
136 Note [Choosing which variables to quantify]
137 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
138 Suppose we are about to do a generalisation step. We have in our hand
141 T the type of the RHS
142 C the constraints from that RHS
144 The game is to figure out
146 Q the set of type variables over which to quantify
147 Ct the constraints we will *not* quantify over
148 Cq the constraints we will quantify over
150 So we're going to infer the type
154 and float the constraints Ct further outwards.
156 Here are the things that *must* be true:
158 (A) Q intersect fv(G) = EMPTY limits how big Q can be
159 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
161 (A) says we can't quantify over a variable that's free in the environment.
162 (B) says we must quantify over all the truly free variables in T, else
163 we won't get a sufficiently general type.
165 We do not *need* to quantify over any variable that is fixed by the
166 free vars of the environment G.
168 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
170 Example: class H x y | x->y where ...
172 fv(G) = {a} C = {H a b, H c d}
175 (A) Q intersect {a} is empty
176 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
178 So Q can be {c,d}, {b,c,d}
180 In particular, it's perfectly OK to quantify over more type variables
181 than strictly necessary; there is no need to quantify over 'b', since
182 it is determined by 'a' which is free in the envt, but it's perfectly
183 OK to do so. However we must not quantify over 'a' itself.
185 Other things being equal, however, we'd like to quantify over as few
186 variables as possible: smaller types, fewer type applications, more
187 constraints can get into Ct instead of Cq. Here's a good way to
190 Q = grow( fv(T), C ) \ oclose( fv(G), C )
192 That is, quantify over all variable that that MIGHT be fixed by the
193 call site (which influences T), but which aren't DEFINITELY fixed by
194 G. This choice definitely quantifies over enough type variables,
195 albeit perhaps too many.
197 Why grow( fv(T), C ) rather than fv(T)? Consider
199 class H x y | x->y where ...
204 If we used fv(T) = {c} we'd get the type
206 forall c. H c d => c -> b
208 And then if the fn was called at several different c's, each of
209 which fixed d differently, we'd get a unification error, because
210 d isn't quantified. Solution: quantify d. So we must quantify
211 everything that might be influenced by c.
213 Why not oclose( fv(T), C )? Because we might not be able to see
214 all the functional dependencies yet:
216 class H x y | x->y where ...
217 instance H x y => Eq (T x y) where ...
222 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
223 apparent yet, and that's wrong. We must really quantify over d too.
225 There really isn't any point in quantifying over any more than
226 grow( fv(T), C ), because the call sites can't possibly influence
227 any other type variables.
231 -------------------------------------
233 -------------------------------------
235 It's very hard to be certain when a type is ambiguous. Consider
239 instance H x y => K (x,y)
241 Is this type ambiguous?
242 forall a b. (K (a,b), Eq b) => a -> a
244 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
245 now we see that a fixes b. So we can't tell about ambiguity for sure
246 without doing a full simplification. And even that isn't possible if
247 the context has some free vars that may get unified. Urgle!
249 Here's another example: is this ambiguous?
250 forall a b. Eq (T b) => a -> a
251 Not if there's an insance decl (with no context)
252 instance Eq (T b) where ...
254 You may say of this example that we should use the instance decl right
255 away, but you can't always do that:
257 class J a b where ...
258 instance J Int b where ...
260 f :: forall a b. J a b => a -> a
262 (Notice: no functional dependency in J's class decl.)
263 Here f's type is perfectly fine, provided f is only called at Int.
264 It's premature to complain when meeting f's signature, or even
265 when inferring a type for f.
269 However, we don't *need* to report ambiguity right away. It'll always
270 show up at the call site.... and eventually at main, which needs special
271 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
273 So here's the plan. We WARN about probable ambiguity if
275 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
277 (all tested before quantification).
278 That is, all the type variables in Cq must be fixed by the the variables
279 in the environment, or by the variables in the type.
281 Notice that we union before calling oclose. Here's an example:
283 class J a b c | a b -> c
287 forall b c. (J a b c) => b -> b
289 Only if we union {a} from G with {b} from T before using oclose,
290 do we see that c is fixed.
292 It's a bit vague exactly which C we should use for this oclose call. If we
293 don't fix enough variables we might complain when we shouldn't (see
294 the above nasty example). Nothing will be perfect. That's why we can
295 only issue a warning.
298 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
300 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
302 then c is a "bubble"; there's no way it can ever improve, and it's
303 certainly ambiguous. UNLESS it is a constant (sigh). And what about
308 instance H x y => K (x,y)
310 Is this type ambiguous?
311 forall a b. (K (a,b), Eq b) => a -> a
313 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
314 is a "bubble" that's a set of constraints
316 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
318 Hence another idea. To decide Q start with fv(T) and grow it
319 by transitive closure in Cq (no functional dependencies involved).
320 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
321 The definitely-ambiguous can then float out, and get smashed at top level
322 (which squashes out the constants, like Eq (T a) above)
325 --------------------------------------
326 Notes on principal types
327 --------------------------------------
332 f x = let g y = op (y::Int) in True
334 Here the principal type of f is (forall a. a->a)
335 but we'll produce the non-principal type
336 f :: forall a. C Int => a -> a
339 --------------------------------------
340 The need for forall's in constraints
341 --------------------------------------
343 [Exchange on Haskell Cafe 5/6 Dec 2000]
345 class C t where op :: t -> Bool
346 instance C [t] where op x = True
348 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
349 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
351 The definitions of p and q differ only in the order of the components in
352 the pair on their right-hand sides. And yet:
354 ghc and "Typing Haskell in Haskell" reject p, but accept q;
355 Hugs rejects q, but accepts p;
356 hbc rejects both p and q;
357 nhc98 ... (Malcolm, can you fill in the blank for us!).
359 The type signature for f forces context reduction to take place, and
360 the results of this depend on whether or not the type of y is known,
361 which in turn depends on which component of the pair the type checker
364 Solution: if y::m a, float out the constraints
365 Monad m, forall c. C (m c)
366 When m is later unified with [], we can solve both constraints.
369 --------------------------------------
370 Notes on implicit parameters
371 --------------------------------------
373 Note [Inheriting implicit parameters]
374 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
379 where f is *not* a top-level binding.
380 From the RHS of f we'll get the constraint (?y::Int).
381 There are two types we might infer for f:
385 (so we get ?y from the context of f's definition), or
387 f :: (?y::Int) => Int -> Int
389 At first you might think the first was better, becuase then
390 ?y behaves like a free variable of the definition, rather than
391 having to be passed at each call site. But of course, the WHOLE
392 IDEA is that ?y should be passed at each call site (that's what
393 dynamic binding means) so we'd better infer the second.
395 BOTTOM LINE: when *inferring types* you *must* quantify
396 over implicit parameters. See the predicate isFreeWhenInferring.
399 Note [Implicit parameters and ambiguity]
400 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
401 What type should we infer for this?
402 f x = (show ?y, x::Int)
403 Since we must quantify over the ?y, the most plausible type is
404 f :: (Show a, ?y::a) => Int -> (String, Int)
405 But notice that the type of the RHS is (String,Int), with no type
406 varibables mentioned at all! The type of f looks ambiguous. But
407 it isn't, because at a call site we might have
408 let ?y = 5::Int in f 7
409 and all is well. In effect, implicit parameters are, well, parameters,
410 so we can take their type variables into account as part of the
411 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
414 Question 2: type signatures
415 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
416 BUT WATCH OUT: When you supply a type signature, we can't force you
417 to quantify over implicit parameters. For example:
421 This is perfectly reasonable. We do not want to insist on
423 (?x + 1) :: (?x::Int => Int)
425 That would be silly. Here, the definition site *is* the occurrence site,
426 so the above strictures don't apply. Hence the difference between
427 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
428 and tcSimplifyCheckBind (which does not).
430 What about when you supply a type signature for a binding?
431 Is it legal to give the following explicit, user type
432 signature to f, thus:
437 At first sight this seems reasonable, but it has the nasty property
438 that adding a type signature changes the dynamic semantics.
441 (let f x = (x::Int) + ?y
442 in (f 3, f 3 with ?y=5)) with ?y = 6
448 in (f 3, f 3 with ?y=5)) with ?y = 6
452 Indeed, simply inlining f (at the Haskell source level) would change the
455 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
456 semantics for a Haskell program without knowing its typing, so if you
457 change the typing you may change the semantics.
459 To make things consistent in all cases where we are *checking* against
460 a supplied signature (as opposed to inferring a type), we adopt the
463 a signature does not need to quantify over implicit params.
465 [This represents a (rather marginal) change of policy since GHC 5.02,
466 which *required* an explicit signature to quantify over all implicit
467 params for the reasons mentioned above.]
469 But that raises a new question. Consider
471 Given (signature) ?x::Int
472 Wanted (inferred) ?x::Int, ?y::Bool
474 Clearly we want to discharge the ?x and float the ?y out. But
475 what is the criterion that distinguishes them? Clearly it isn't
476 what free type variables they have. The Right Thing seems to be
477 to float a constraint that
478 neither mentions any of the quantified type variables
479 nor any of the quantified implicit parameters
481 See the predicate isFreeWhenChecking.
484 Question 3: monomorphism
485 ~~~~~~~~~~~~~~~~~~~~~~~~
486 There's a nasty corner case when the monomorphism restriction bites:
490 The argument above suggests that we *must* generalise
491 over the ?y parameter, to get
492 z :: (?y::Int) => Int,
493 but the monomorphism restriction says that we *must not*, giving
495 Why does the momomorphism restriction say this? Because if you have
497 let z = x + ?y in z+z
499 you might not expect the addition to be done twice --- but it will if
500 we follow the argument of Question 2 and generalise over ?y.
503 Question 4: top level
504 ~~~~~~~~~~~~~~~~~~~~~
505 At the top level, monomorhism makes no sense at all.
508 main = let ?x = 5 in print foo
512 woggle :: (?x :: Int) => Int -> Int
515 We definitely don't want (foo :: Int) with a top-level implicit parameter
516 (?x::Int) becuase there is no way to bind it.
521 (A) Always generalise over implicit parameters
522 Bindings that fall under the monomorphism restriction can't
526 * Inlining remains valid
527 * No unexpected loss of sharing
528 * But simple bindings like
530 will be rejected, unless you add an explicit type signature
531 (to avoid the monomorphism restriction)
532 z :: (?y::Int) => Int
534 This seems unacceptable
536 (B) Monomorphism restriction "wins"
537 Bindings that fall under the monomorphism restriction can't
539 Always generalise over implicit parameters *except* for bindings
540 that fall under the monomorphism restriction
543 * Inlining isn't valid in general
544 * No unexpected loss of sharing
545 * Simple bindings like
547 accepted (get value of ?y from binding site)
549 (C) Always generalise over implicit parameters
550 Bindings that fall under the monomorphism restriction can't
551 be generalised, EXCEPT for implicit parameters
553 * Inlining remains valid
554 * Unexpected loss of sharing (from the extra generalisation)
555 * Simple bindings like
557 accepted (get value of ?y from occurrence sites)
562 None of these choices seems very satisfactory. But at least we should
563 decide which we want to do.
565 It's really not clear what is the Right Thing To Do. If you see
569 would you expect the value of ?y to be got from the *occurrence sites*
570 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
571 case of function definitions, the answer is clearly the former, but
572 less so in the case of non-fucntion definitions. On the other hand,
573 if we say that we get the value of ?y from the definition site of 'z',
574 then inlining 'z' might change the semantics of the program.
576 Choice (C) really says "the monomorphism restriction doesn't apply
577 to implicit parameters". Which is fine, but remember that every
578 innocent binding 'x = ...' that mentions an implicit parameter in
579 the RHS becomes a *function* of that parameter, called at each
580 use of 'x'. Now, the chances are that there are no intervening 'with'
581 clauses that bind ?y, so a decent compiler should common up all
582 those function calls. So I think I strongly favour (C). Indeed,
583 one could make a similar argument for abolishing the monomorphism
584 restriction altogether.
586 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
590 %************************************************************************
592 \subsection{tcSimplifyInfer}
594 %************************************************************************
596 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
598 1. Compute Q = grow( fvs(T), C )
600 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
601 predicates will end up in Ct; we deal with them at the top level
603 3. Try improvement, using functional dependencies
605 4. If Step 3 did any unification, repeat from step 1
606 (Unification can change the result of 'grow'.)
608 Note: we don't reduce dictionaries in step 2. For example, if we have
609 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
610 after step 2. However note that we may therefore quantify over more
611 type variables than we absolutely have to.
613 For the guts, we need a loop, that alternates context reduction and
614 improvement with unification. E.g. Suppose we have
616 class C x y | x->y where ...
618 and tcSimplify is called with:
620 Then improvement unifies a with b, giving
623 If we need to unify anything, we rattle round the whole thing all over
630 -> TcTyVarSet -- fv(T); type vars
632 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)
633 [Inst], -- Dict Ids that must be bound here (zonked)
634 TcDictBinds) -- Bindings
635 -- Any free (escaping) Insts are tossed into the environment
640 tcSimplifyInfer doc tau_tvs wanted
641 = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
642 ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
643 ; gbl_tvs <- tcGetGlobalTyVars
644 ; let preds1 = fdPredsOfInsts wanted'
645 gbl_tvs1 = oclose preds1 gbl_tvs
646 qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
647 -- See Note [Choosing which variables to quantify]
649 -- To maximise sharing, remove from consideration any
650 -- constraints that don't mention qtvs at all
651 ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
654 -- To make types simple, reduce as much as possible
655 ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
656 ppr gbl_tvs1 $$ ppr free $$ ppr bound))
657 ; (irreds1, binds1) <- tryHardCheckLoop doc bound
659 -- Note [Inference and implication constraints]
660 ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
661 ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
663 -- Now work out all over again which type variables to quantify,
664 -- exactly in the same way as before, but starting from irreds2. Why?
665 -- a) By now improvment may have taken place, and we must *not*
666 -- quantify over any variable free in the environment
667 -- tc137 (function h inside g) is an example
669 -- b) Do not quantify over constraints that *now* do not
670 -- mention quantified type variables, because they are
671 -- simply ambiguous (or might be bound further out). Example:
672 -- f :: Eq b => a -> (a, b)
674 -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
675 -- We decide to quantify over 'alpha' alone, but free1 does not include f77
676 -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
677 -- constraint (Eq beta), which we dump back into the free set
678 -- See test tcfail181
680 -- c) irreds may contain type variables not previously mentioned,
681 -- e.g. instance D a x => Foo [a]
683 -- Then after simplifying we'll get (D a x), and x is fresh
684 -- We must quantify over x else it'll be totally unbound
685 ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
686 ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
687 -- Note that we start from gbl_tvs1
688 -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
689 -- we've already put some of the original preds1 into frees
690 -- E.g. wanteds = C a b (where a->b)
693 -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
694 -- irreds2 will be empty. But we don't want to generalise over b!
695 ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
696 qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
697 ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
700 -- Turn the quantified meta-type variables into real type variables
701 ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
703 -- We can't abstract over any remaining unsolved
704 -- implications so instead just float them outwards. Ugh.
705 ; let (q_dicts, implics) = partition isDict irreds3
706 ; loc <- getInstLoc (ImplicOrigin doc)
707 ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
709 ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
710 -- NB: when we are done, we might have some bindings, but
711 -- the final qtvs might be empty. See Note [NO TYVARS] below.
713 approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
714 -- Note [Inference and implication constraints]
715 -- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
716 -- - fetching any dicts inside them that are free
717 -- - using those dicts as cruder constraints, to solve the implications
718 -- - returning the extra ones too
720 approximateImplications doc want_dict irreds
722 = return (irreds, emptyBag)
724 = do { extra_dicts' <- mapM cloneDict extra_dicts
725 ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
726 -- By adding extra_dicts', we make them
727 -- available to solve the implication constraints
729 extra_dicts = get_dicts (filter isImplicInst irreds)
731 get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
732 -- Find the wanted constraints in implication constraints that satisfy
733 -- want_dict, and are not bound by forall's in the constraint itself
734 get_dicts ds = concatMap get_dict ds
736 get_dict d@(Dict {}) | want_dict d = [d]
738 get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
739 = [ d | let tv_set = mkVarSet tvs
740 , d <- get_dicts wanteds
741 , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
742 get_dict other = pprPanic "approximateImplications" (ppr other)
745 Note [Inference and implication constraints]
746 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
747 Suppose we have a wanted implication constraint (perhaps arising from
748 a nested pattern match) like
750 and we are now trying to quantify over 'a' when inferring the type for
751 a function. In principle it's possible that there might be an instance
752 instance (C a, E a) => D [a]
753 so the context (E a) would suffice. The Right Thing is to abstract over
754 the implication constraint, but we don't do that (a) because it'll be
755 surprising to programmers and (b) because we don't have the machinery to deal
756 with 'given' implications.
758 So our best approximation is to make (D [a]) part of the inferred
759 context, so we can use that to discharge the implication. Hence
760 the strange function get_dictsin approximateImplications.
762 The common cases are more clear-cut, when we have things like
764 Here, abstracting over (C b) is not an approximation at all -- but see
765 Note [Freeness and implications].
767 See Trac #1430 and test tc228.
771 -----------------------------------------------------------
772 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
773 -- against, but we don't know the type variables over which we are going to quantify.
774 -- This happens when we have a type signature for a mutually recursive group
777 -> TcTyVarSet -- fv(T)
780 -> TcM ([TyVar], -- Fully zonked, and quantified
781 TcDictBinds) -- Bindings
783 tcSimplifyInferCheck loc tau_tvs givens wanteds
784 = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
786 -- Figure out which type variables to quantify over
787 -- You might think it should just be the signature tyvars,
788 -- but in bizarre cases you can get extra ones
789 -- f :: forall a. Num a => a -> a
790 -- f x = fst (g (x, head [])) + 1
792 -- Here we infer g :: forall a b. a -> b -> (b,a)
793 -- We don't want g to be monomorphic in b just because
794 -- f isn't quantified over b.
795 ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
796 ; all_tvs <- zonkTcTyVarsAndFV all_tvs
797 ; gbl_tvs <- tcGetGlobalTyVars
798 ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
799 -- We could close gbl_tvs, but its not necessary for
800 -- soundness, and it'll only affect which tyvars, not which
801 -- dictionaries, we quantify over
803 ; qtvs' <- zonkQuantifiedTyVars qtvs
805 -- Now we are back to normal (c.f. tcSimplCheck)
806 ; implic_bind <- bindIrreds loc qtvs' givens irreds
808 ; return (qtvs', binds `unionBags` implic_bind) }
811 Note [Squashing methods]
812 ~~~~~~~~~~~~~~~~~~~~~~~~~
813 Be careful if you want to float methods more:
814 truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
815 From an application (truncate f i) we get
818 If we have also have a second occurrence of truncate, we get
821 When simplifying with i,f free, we might still notice that
822 t1=t3; but alas, the binding for t2 (which mentions t1)
823 may continue to float out!
828 class Y a b | a -> b where
831 instance Y [[a]] a where
834 k :: X a -> X a -> X a
836 g :: Num a => [X a] -> [X a]
839 h ys = ys ++ map (k (y [[0]])) xs
841 The excitement comes when simplifying the bindings for h. Initially
842 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
843 From this we get t1:=:t2, but also various bindings. We can't forget
844 the bindings (because of [LOOP]), but in fact t1 is what g is
847 The net effect of [NO TYVARS]
850 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
851 isFreeWhenInferring qtvs inst
852 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
853 && isInheritableInst inst -- and no implicit parameter involved
854 -- see Note [Inheriting implicit parameters]
856 {- No longer used (with implication constraints)
857 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
858 -> NameSet -- Quantified implicit parameters
860 isFreeWhenChecking qtvs ips inst
861 = isFreeWrtTyVars qtvs inst
862 && isFreeWrtIPs ips inst
865 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
866 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
870 %************************************************************************
872 \subsection{tcSimplifyCheck}
874 %************************************************************************
876 @tcSimplifyCheck@ is used when we know exactly the set of variables
877 we are going to quantify over. For example, a class or instance declaration.
880 -----------------------------------------------------------
881 -- tcSimplifyCheck is used when checking expression type signatures,
882 -- class decls, instance decls etc.
883 tcSimplifyCheck :: InstLoc
884 -> [TcTyVar] -- Quantify over these
887 -> TcM TcDictBinds -- Bindings
888 tcSimplifyCheck loc qtvs givens wanteds
889 = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
890 do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
891 ; implic_bind <- bindIrreds loc qtvs givens irreds
892 ; return (binds `unionBags` implic_bind) }
894 -----------------------------------------------------------
895 -- tcSimplifyCheckPat is used for existential pattern match
896 tcSimplifyCheckPat :: InstLoc
897 -> [CoVar] -> Refinement
898 -> [TcTyVar] -- Quantify over these
901 -> TcM TcDictBinds -- Bindings
902 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
903 = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
904 do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
905 ; implic_bind <- bindIrredsR loc qtvs co_vars reft
907 ; return (binds `unionBags` implic_bind) }
909 -----------------------------------------------------------
910 bindIrreds :: InstLoc -> [TcTyVar]
913 bindIrreds loc qtvs givens irreds
914 = bindIrredsR loc qtvs [] emptyRefinement givens irreds
916 bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
917 -> Refinement -> [Inst] -> [Inst]
919 -- Make a binding that binds 'irreds', by generating an implication
920 -- constraint for them, *and* throwing the constraint into the LIE
921 bindIrredsR loc qtvs co_vars reft givens irreds
925 = do { let givens' = filter isDict givens
926 -- The givens can include methods
927 -- See Note [Pruning the givens in an implication constraint]
929 -- If there are no 'givens' *and* the refinement is empty
930 -- (the refinement is like more givens), then it's safe to
931 -- partition the 'wanteds' by their qtvs, thereby trimming irreds
932 -- See Note [Freeness and implications]
933 ; irreds' <- if null givens' && isEmptyRefinement reft
935 { let qtv_set = mkVarSet qtvs
936 (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
938 ; return real_irreds }
941 ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
942 ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
943 -- This call does the real work
944 -- If irreds' is empty, it does something sensible
949 makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
951 -> TcM ([Inst], TcDictBinds)
952 -- Make a binding that binds 'irreds', by generating an implication
953 -- constraint for them, *and* throwing the constraint into the LIE
954 -- The binding looks like
955 -- (ir1, .., irn) = f qtvs givens
956 -- where f is (evidence for) the new implication constraint
957 -- f :: forall qtvs. {reft} givens => (ir1, .., irn)
958 -- qtvs includes coercion variables
960 -- This binding must line up the 'rhs' in reduceImplication
961 makeImplicationBind loc all_tvs reft
962 givens -- Guaranteed all Dicts
964 | null irreds -- If there are no irreds, we are done
965 = return ([], emptyBag)
966 | otherwise -- Otherwise we must generate a binding
967 = do { uniq <- newUnique
968 ; span <- getSrcSpanM
969 ; let name = mkInternalName uniq (mkVarOcc "ic") span
970 implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
971 tci_tyvars = all_tvs,
973 tci_wanted = irreds, tci_loc = loc }
975 ; let n_irreds = length irreds
976 irred_ids = map instToId irreds
977 tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
978 pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
979 rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
980 co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
981 bind | n_irreds==1 = VarBind (head irred_ids) rhs
982 | otherwise = PatBind { pat_lhs = L span pat,
983 pat_rhs = unguardedGRHSs rhs,
985 bind_fvs = placeHolderNames }
986 ; -- pprTrace "Make implic inst" (ppr implic_inst) $
987 return ([implic_inst], unitBag (L span bind)) }
989 -----------------------------------------------------------
990 tryHardCheckLoop :: SDoc
992 -> TcM ([Inst], TcDictBinds)
994 tryHardCheckLoop doc wanteds
995 = checkLoop (mkRedEnv doc try_me []) wanteds
997 try_me inst = ReduceMe AddSCs
998 -- Here's the try-hard bit
1000 -----------------------------------------------------------
1001 gentleCheckLoop :: InstLoc
1004 -> TcM ([Inst], TcDictBinds)
1006 gentleCheckLoop inst_loc givens wanteds
1007 = checkLoop env wanteds
1009 env = mkRedEnv (pprInstLoc inst_loc) try_me givens
1011 try_me inst | isMethodOrLit inst = ReduceMe AddSCs
1013 -- When checking against a given signature
1014 -- we MUST be very gentle: Note [Check gently]
1018 ~~~~~~~~~~~~~~~~~~~~
1019 We have to very careful about not simplifying too vigorously
1024 f :: Show b => T b -> b
1025 f (MkT x) = show [x]
1027 Inside the pattern match, which binds (a:*, x:a), we know that
1029 Hence we have a dictionary for Show [a] available; and indeed we
1030 need it. We are going to build an implication contraint
1031 forall a. (b~[a]) => Show [a]
1032 Later, we will solve this constraint using the knowledg e(Show b)
1034 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
1035 thing becomes insoluble. So we simplify gently (get rid of literals
1036 and methods only, plus common up equal things), deferring the real
1037 work until top level, when we solve the implication constraint
1038 with tryHardCheckLooop.
1042 -----------------------------------------------------------
1045 -> TcM ([Inst], TcDictBinds)
1046 -- Precondition: givens are completely rigid
1047 -- Postcondition: returned Insts are zonked
1049 checkLoop env wanteds
1050 = do { -- Givens are skolems, so no need to zonk them
1051 wanteds' <- mappM zonkInst wanteds
1053 ; (improved, binds, irreds) <- reduceContext env wanteds'
1055 ; if not improved then
1056 return (irreds, binds)
1059 -- If improvement did some unification, we go round again.
1060 -- We start again with irreds, not wanteds
1061 -- Using an instance decl might have introduced a fresh type variable
1062 -- which might have been unified, so we'd get an infinite loop
1063 -- if we started again with wanteds! See Note [LOOP]
1064 { (irreds1, binds1) <- checkLoop env irreds
1065 ; return (irreds1, binds `unionBags` binds1) } }
1070 class If b t e r | b t e -> r
1073 class Lte a b c | a b -> c where lte :: a -> b -> c
1075 instance (Lte a b l,If l b a c) => Max a b c
1077 Wanted: Max Z (S x) y
1079 Then we'll reduce using the Max instance to:
1080 (Lte Z (S x) l, If l (S x) Z y)
1081 and improve by binding l->T, after which we can do some reduction
1082 on both the Lte and If constraints. What we *can't* do is start again
1083 with (Max Z (S x) y)!
1087 %************************************************************************
1089 tcSimplifySuperClasses
1091 %************************************************************************
1093 Note [SUPERCLASS-LOOP 1]
1094 ~~~~~~~~~~~~~~~~~~~~~~~~
1095 We have to be very, very careful when generating superclasses, lest we
1096 accidentally build a loop. Here's an example:
1100 class S a => C a where { opc :: a -> a }
1101 class S b => D b where { opd :: b -> b }
1103 instance C Int where
1106 instance D Int where
1109 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1110 Simplifying, we may well get:
1111 $dfCInt = :C ds1 (opd dd)
1114 Notice that we spot that we can extract ds1 from dd.
1116 Alas! Alack! We can do the same for (instance D Int):
1118 $dfDInt = :D ds2 (opc dc)
1122 And now we've defined the superclass in terms of itself.
1124 Solution: never generate a superclass selectors at all when
1125 satisfying the superclass context of an instance declaration.
1127 Two more nasty cases are in
1132 tcSimplifySuperClasses
1137 tcSimplifySuperClasses loc givens sc_wanteds
1138 = do { (irreds, binds1) <- checkLoop env sc_wanteds
1139 ; let (tidy_env, tidy_irreds) = tidyInsts irreds
1140 ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
1143 env = mkRedEnv (pprInstLoc loc) try_me givens
1144 try_me inst = ReduceMe NoSCs
1145 -- Like tryHardCheckLoop, but with NoSCs
1149 %************************************************************************
1151 \subsection{tcSimplifyRestricted}
1153 %************************************************************************
1155 tcSimplifyRestricted infers which type variables to quantify for a
1156 group of restricted bindings. This isn't trivial.
1159 We want to quantify over a to get id :: forall a. a->a
1162 We do not want to quantify over a, because there's an Eq a
1163 constraint, so we get eq :: a->a->Bool (notice no forall)
1166 RHS has type 'tau', whose free tyvars are tau_tvs
1167 RHS has constraints 'wanteds'
1170 Quantify over (tau_tvs \ ftvs(wanteds))
1171 This is bad. The constraints may contain (Monad (ST s))
1172 where we have instance Monad (ST s) where...
1173 so there's no need to be monomorphic in s!
1175 Also the constraint might be a method constraint,
1176 whose type mentions a perfectly innocent tyvar:
1177 op :: Num a => a -> b -> a
1178 Here, b is unconstrained. A good example would be
1180 We want to infer the polymorphic type
1181 foo :: forall b. b -> b
1184 Plan B (cunning, used for a long time up to and including GHC 6.2)
1185 Step 1: Simplify the constraints as much as possible (to deal
1186 with Plan A's problem). Then set
1187 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1189 Step 2: Now simplify again, treating the constraint as 'free' if
1190 it does not mention qtvs, and trying to reduce it otherwise.
1191 The reasons for this is to maximise sharing.
1193 This fails for a very subtle reason. Suppose that in the Step 2
1194 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
1195 In the Step 1 this constraint might have been simplified, perhaps to
1196 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
1197 This won't happen in Step 2... but that in turn might prevent some other
1198 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
1199 and that in turn breaks the invariant that no constraints are quantified over.
1201 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
1206 Step 1: Simplify the constraints as much as possible (to deal
1207 with Plan A's problem). Then set
1208 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1209 Return the bindings from Step 1.
1212 A note about Plan C (arising from "bug" reported by George Russel March 2004)
1215 instance (HasBinary ty IO) => HasCodedValue ty
1217 foo :: HasCodedValue a => String -> IO a
1219 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1220 doDecodeIO codedValue view
1221 = let { act = foo "foo" } in act
1223 You might think this should work becuase the call to foo gives rise to a constraint
1224 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1225 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1226 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1228 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1232 Plan D (a variant of plan B)
1233 Step 1: Simplify the constraints as much as possible (to deal
1234 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1235 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1237 Step 2: Now simplify again, treating the constraint as 'free' if
1238 it does not mention qtvs, and trying to reduce it otherwise.
1240 The point here is that it's generally OK to have too few qtvs; that is,
1241 to make the thing more monomorphic than it could be. We don't want to
1242 do that in the common cases, but in wierd cases it's ok: the programmer
1243 can always add a signature.
1245 Too few qtvs => too many wanteds, which is what happens if you do less
1250 tcSimplifyRestricted -- Used for restricted binding groups
1251 -- i.e. ones subject to the monomorphism restriction
1254 -> [Name] -- Things bound in this group
1255 -> TcTyVarSet -- Free in the type of the RHSs
1256 -> [Inst] -- Free in the RHSs
1257 -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
1258 TcDictBinds) -- Bindings
1259 -- tcSimpifyRestricted returns no constraints to
1260 -- quantify over; by definition there are none.
1261 -- They are all thrown back in the LIE
1263 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1264 -- Zonk everything in sight
1265 = do { wanteds' <- mappM zonkInst wanteds
1267 -- 'ReduceMe': Reduce as far as we can. Don't stop at
1268 -- dicts; the idea is to get rid of as many type
1269 -- variables as possible, and we don't want to stop
1270 -- at (say) Monad (ST s), because that reduces
1271 -- immediately, with no constraint on s.
1273 -- BUT do no improvement! See Plan D above
1274 -- HOWEVER, some unification may take place, if we instantiate
1275 -- a method Inst with an equality constraint
1276 ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
1277 ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
1279 -- Next, figure out the tyvars we will quantify over
1280 ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
1281 ; gbl_tvs' <- tcGetGlobalTyVars
1282 ; constrained_dicts' <- mappM zonkInst constrained_dicts
1284 ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
1285 -- As in tcSimplifyInfer
1287 -- Do not quantify over constrained type variables:
1288 -- this is the monomorphism restriction
1289 constrained_tvs' = tyVarsOfInsts constrained_dicts'
1290 qtvs = qtvs1 `minusVarSet` constrained_tvs'
1291 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
1294 ; warn_mono <- doptM Opt_WarnMonomorphism
1295 ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
1296 (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
1297 <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
1298 ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
1300 ; traceTc (text "tcSimplifyRestricted" <+> vcat [
1301 pprInsts wanteds, pprInsts constrained_dicts',
1303 ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
1305 -- The first step may have squashed more methods than
1306 -- necessary, so try again, this time more gently, knowing the exact
1307 -- set of type variables to quantify over.
1309 -- We quantify only over constraints that are captured by qtvs;
1310 -- these will just be a subset of non-dicts. This in contrast
1311 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1312 -- all *non-inheritable* constraints too. This implements choice
1313 -- (B) under "implicit parameter and monomorphism" above.
1315 -- Remember that we may need to do *some* simplification, to
1316 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1317 -- just to float all constraints
1319 -- At top level, we *do* squash methods becuase we want to
1320 -- expose implicit parameters to the test that follows
1321 ; let is_nested_group = isNotTopLevel top_lvl
1322 try_me inst | isFreeWrtTyVars qtvs inst,
1323 (is_nested_group || isDict inst) = Stop
1324 | otherwise = ReduceMe AddSCs
1325 env = mkNoImproveRedEnv doc try_me
1326 ; (_imp, binds, irreds) <- reduceContext env wanteds'
1328 -- See "Notes on implicit parameters, Question 4: top level"
1329 ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
1330 if is_nested_group then
1332 else do { let (bad_ips, non_ips) = partition isIPDict irreds
1333 ; addTopIPErrs bndrs bad_ips
1334 ; extendLIEs non_ips }
1336 ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
1337 ; return (qtvs', binds) }
1341 %************************************************************************
1345 %************************************************************************
1347 On the LHS of transformation rules we only simplify methods and constants,
1348 getting dictionaries. We want to keep all of them unsimplified, to serve
1349 as the available stuff for the RHS of the rule.
1351 Example. Consider the following left-hand side of a rule
1353 f (x == y) (y > z) = ...
1355 If we typecheck this expression we get constraints
1357 d1 :: Ord a, d2 :: Eq a
1359 We do NOT want to "simplify" to the LHS
1361 forall x::a, y::a, z::a, d1::Ord a.
1362 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1366 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1367 f ((==) d2 x y) ((>) d1 y z) = ...
1369 Here is another example:
1371 fromIntegral :: (Integral a, Num b) => a -> b
1372 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1374 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1375 we *dont* want to get
1377 forall dIntegralInt.
1378 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1380 because the scsel will mess up RULE matching. Instead we want
1382 forall dIntegralInt, dNumInt.
1383 fromIntegral Int Int dIntegralInt dNumInt = id Int
1387 g (x == y) (y == z) = ..
1389 where the two dictionaries are *identical*, we do NOT WANT
1391 forall x::a, y::a, z::a, d1::Eq a
1392 f ((==) d1 x y) ((>) d1 y z) = ...
1394 because that will only match if the dict args are (visibly) equal.
1395 Instead we want to quantify over the dictionaries separately.
1397 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1398 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1399 from scratch, rather than further parameterise simpleReduceLoop etc
1402 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1403 tcSimplifyRuleLhs wanteds
1404 = go [] emptyBag wanteds
1407 = return (dicts, binds)
1408 go dicts binds (w:ws)
1410 = go (w:dicts) binds ws
1412 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1413 -- to fromInteger; this looks fragile to me
1414 ; lookup_result <- lookupSimpleInst w'
1415 ; case lookup_result of
1416 GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
1417 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1421 tcSimplifyBracket is used when simplifying the constraints arising from
1422 a Template Haskell bracket [| ... |]. We want to check that there aren't
1423 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1424 Show instance), but we aren't otherwise interested in the results.
1425 Nor do we care about ambiguous dictionaries etc. We will type check
1426 this bracket again at its usage site.
1429 tcSimplifyBracket :: [Inst] -> TcM ()
1430 tcSimplifyBracket wanteds
1431 = do { tryHardCheckLoop doc wanteds
1434 doc = text "tcSimplifyBracket"
1438 %************************************************************************
1440 \subsection{Filtering at a dynamic binding}
1442 %************************************************************************
1447 we must discharge all the ?x constraints from B. We also do an improvement
1448 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1450 Actually, the constraints from B might improve the types in ?x. For example
1452 f :: (?x::Int) => Char -> Char
1455 then the constraint (?x::Int) arising from the call to f will
1456 force the binding for ?x to be of type Int.
1459 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1462 -- We need a loop so that we do improvement, and then
1463 -- (next time round) generate a binding to connect the two
1465 -- Here the two ?x's have different types, and improvement
1466 -- makes them the same.
1468 tcSimplifyIPs given_ips wanteds
1469 = do { wanteds' <- mappM zonkInst wanteds
1470 ; given_ips' <- mappM zonkInst given_ips
1471 -- Unusually for checking, we *must* zonk the given_ips
1473 ; let env = mkRedEnv doc try_me given_ips'
1474 ; (improved, binds, irreds) <- reduceContext env wanteds'
1476 ; if not improved then
1477 ASSERT( all is_free irreds )
1478 do { extendLIEs irreds
1481 tcSimplifyIPs given_ips wanteds }
1483 doc = text "tcSimplifyIPs" <+> ppr given_ips
1484 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1485 is_free inst = isFreeWrtIPs ip_set inst
1487 -- Simplify any methods that mention the implicit parameter
1488 try_me inst | is_free inst = Stop
1489 | otherwise = ReduceMe NoSCs
1493 %************************************************************************
1495 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1497 %************************************************************************
1499 When doing a binding group, we may have @Insts@ of local functions.
1500 For example, we might have...
1502 let f x = x + 1 -- orig local function (overloaded)
1503 f.1 = f Int -- two instances of f
1508 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1509 where @f@ is in scope; those @Insts@ must certainly not be passed
1510 upwards towards the top-level. If the @Insts@ were binding-ified up
1511 there, they would have unresolvable references to @f@.
1513 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1514 For each method @Inst@ in the @init_lie@ that mentions one of the
1515 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1516 @LIE@), as well as the @HsBinds@ generated.
1519 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1520 -- Simlifies only MethodInsts, and generate only bindings of form
1522 -- We're careful not to even generate bindings of the form
1524 -- You'd think that'd be fine, but it interacts with what is
1525 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1527 bindInstsOfLocalFuns wanteds local_ids
1528 | null overloaded_ids
1530 = extendLIEs wanteds `thenM_`
1531 returnM emptyLHsBinds
1534 = do { (irreds, binds) <- checkLoop env for_me
1535 ; extendLIEs not_for_me
1539 env = mkRedEnv doc try_me []
1540 doc = text "bindInsts" <+> ppr local_ids
1541 overloaded_ids = filter is_overloaded local_ids
1542 is_overloaded id = isOverloadedTy (idType id)
1543 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1545 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1546 -- so it's worth building a set, so that
1547 -- lookup (in isMethodFor) is faster
1548 try_me inst | isMethod inst = ReduceMe NoSCs
1553 %************************************************************************
1555 \subsection{Data types for the reduction mechanism}
1557 %************************************************************************
1559 The main control over context reduction is here
1563 = RedEnv { red_doc :: SDoc -- The context
1564 , red_try_me :: Inst -> WhatToDo
1565 , red_improve :: Bool -- True <=> do improvement
1566 , red_givens :: [Inst] -- All guaranteed rigid
1568 -- but see Note [Rigidity]
1569 , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
1570 -- See Note [RedStack]
1574 -- The red_givens are rigid so far as cmpInst is concerned.
1575 -- There is one case where they are not totally rigid, namely in tcSimplifyIPs
1576 -- let ?x = e in ...
1577 -- Here, the given is (?x::a), where 'a' is not necy a rigid type
1578 -- But that doesn't affect the comparison, which is based only on mame.
1581 -- The red_stack pair (n,insts) pair is just used for error reporting.
1582 -- 'n' is always the depth of the stack.
1583 -- The 'insts' is the stack of Insts being reduced: to produce X
1584 -- I had to produce Y, to produce Y I had to produce Z, and so on.
1587 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
1588 mkRedEnv doc try_me givens
1589 = RedEnv { red_doc = doc, red_try_me = try_me,
1590 red_givens = givens, red_stack = (0,[]),
1591 red_improve = True }
1593 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
1594 -- Do not do improvement; no givens
1595 mkNoImproveRedEnv doc try_me
1596 = RedEnv { red_doc = doc, red_try_me = try_me,
1597 red_givens = [], red_stack = (0,[]),
1598 red_improve = True }
1601 = ReduceMe WantSCs -- Try to reduce this
1602 -- If there's no instance, add the inst to the
1603 -- irreductible ones, but don't produce an error
1604 -- message of any kind.
1605 -- It might be quite legitimate such as (Eq a)!
1607 | Stop -- Return as irreducible unless it can
1608 -- be reduced to a constant in one step
1609 -- Do not add superclasses; see
1611 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1612 -- of a predicate when adding it to the avails
1613 -- The reason for this flag is entirely the super-class loop problem
1614 -- Note [SUPER-CLASS LOOP 1]
1617 %************************************************************************
1619 \subsection[reduce]{@reduce@}
1621 %************************************************************************
1625 reduceContext :: RedEnv
1627 -> TcM (ImprovementDone,
1628 TcDictBinds, -- Dictionary bindings
1629 [Inst]) -- Irreducible
1631 reduceContext env wanteds
1632 = do { traceTc (text "reduceContext" <+> (vcat [
1633 text "----------------------",
1635 text "given" <+> ppr (red_givens env),
1636 text "wanted" <+> ppr wanteds,
1637 text "----------------------"
1640 -- Build the Avail mapping from "givens"
1641 ; init_state <- foldlM addGiven emptyAvails (red_givens env)
1644 -- Process non-implication constraints first, so that they are
1645 -- available to help solving the implication constraints
1646 -- ToDo: seems a bit inefficient and ad-hoc
1647 ; let (implics, rest) = partition isImplicInst wanteds
1648 ; avails <- reduceList env (rest ++ implics) init_state
1650 ; let improved = availsImproved avails
1651 ; (binds, irreds) <- extractResults avails wanteds
1653 ; traceTc (text "reduceContext end" <+> (vcat [
1654 text "----------------------",
1656 text "given" <+> ppr (red_givens env),
1657 text "wanted" <+> ppr wanteds,
1659 text "avails" <+> pprAvails avails,
1660 text "improved =" <+> ppr improved,
1661 text "irreds = " <+> ppr irreds,
1662 text "----------------------"
1665 ; return (improved, binds, irreds) }
1667 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
1668 tcImproveOne avails inst
1669 | not (isDict inst) = return False
1671 = do { inst_envs <- tcGetInstEnvs
1672 ; let eqns = improveOne (classInstances inst_envs)
1673 (dictPred inst, pprInstArising inst)
1674 [ (dictPred p, pprInstArising p)
1675 | p <- availsInsts avails, isDict p ]
1676 -- Avails has all the superclasses etc (good)
1677 -- It also has all the intermediates of the deduction (good)
1678 -- It does not have duplicates (good)
1679 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1680 -- so that improve will see them separate
1681 ; traceTc (text "improveOne" <+> ppr inst)
1684 unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
1685 -> TcM ImprovementDone
1686 unifyEqns [] = return False
1688 = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
1692 unify ((qtvs, pairs), what1, what2)
1693 = addErrCtxtM (mkEqnMsg what1 what2) $
1694 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1695 mapM_ (unif_pr tenv) pairs
1696 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1698 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1700 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1701 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1702 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1703 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1704 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1705 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1706 ; return (tidy_env, msg) }
1709 The main context-reduction function is @reduce@. Here's its game plan.
1712 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
1713 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
1714 = do { dopts <- getDOpts
1717 dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n)
1718 2 (ifPprDebug (nest 2 (pprStack stk))))
1721 ; if n >= ctxtStkDepth dopts then
1722 failWithTc (reduceDepthErr n stk)
1726 go [] state = return state
1727 go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
1730 -- Base case: we're done!
1731 reduce env wanted avails
1732 -- It's the same as an existing inst, or a superclass thereof
1733 | Just avail <- findAvail avails wanted
1737 = case red_try_me env wanted of {
1738 ; Stop -> try_simple (addIrred NoSCs) -- See Note [No superclasses for Stop]
1740 ; ReduceMe want_scs -> -- It should be reduced
1741 reduceInst env avails wanted `thenM` \ (avails, lookup_result) ->
1742 case lookup_result of
1743 NoInstance -> -- No such instance!
1744 -- Add it and its superclasses
1745 addIrred want_scs avails wanted
1747 GenInst [] rhs -> addWanted want_scs avails wanted rhs []
1749 GenInst wanteds' rhs -> do { avails1 <- addIrred NoSCs avails wanted
1750 ; avails2 <- reduceList env wanteds' avails1
1751 ; addWanted want_scs avails2 wanted rhs wanteds' }
1752 -- Temporarily do addIrred *before* the reduceList,
1753 -- which has the effect of adding the thing we are trying
1754 -- to prove to the database before trying to prove the things it
1755 -- needs. See note [RECURSIVE DICTIONARIES]
1756 -- NB: we must not do an addWanted before, because that adds the
1757 -- superclasses too, and thaat can lead to a spurious loop; see
1758 -- the examples in [SUPERCLASS-LOOP]
1759 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1763 -- First, see if the inst can be reduced to a constant in one step
1764 -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
1765 -- Don't bother for implication constraints, which take real work
1766 try_simple do_this_otherwise
1767 = do { res <- lookupSimpleInst wanted
1769 GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
1770 other -> do_this_otherwise avails wanted }
1774 Note [SUPERCLASS-LOOP 2]
1775 ~~~~~~~~~~~~~~~~~~~~~~~~
1776 But the above isn't enough. Suppose we are *given* d1:Ord a,
1777 and want to deduce (d2:C [a]) where
1779 class Ord a => C a where
1780 instance Ord [a] => C [a] where ...
1782 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1783 superclasses of C [a] to avails. But we must not overwrite the binding
1784 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1787 Here's another variant, immortalised in tcrun020
1788 class Monad m => C1 m
1789 class C1 m => C2 m x
1790 instance C2 Maybe Bool
1791 For the instance decl we need to build (C1 Maybe), and it's no good if
1792 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1793 before we search for C1 Maybe.
1795 Here's another example
1796 class Eq b => Foo a b
1797 instance Eq a => Foo [a] a
1801 we'll first deduce that it holds (via the instance decl). We must not
1802 then overwrite the Eq t constraint with a superclass selection!
1804 At first I had a gross hack, whereby I simply did not add superclass constraints
1805 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1806 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1807 I found a very obscure program (now tcrun021) in which improvement meant the
1808 simplifier got two bites a the cherry... so something seemed to be an Stop
1809 first time, but reducible next time.
1811 Now we implement the Right Solution, which is to check for loops directly
1812 when adding superclasses. It's a bit like the occurs check in unification.
1815 Note [RECURSIVE DICTIONARIES]
1816 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1818 data D r = ZeroD | SuccD (r (D r));
1820 instance (Eq (r (D r))) => Eq (D r) where
1821 ZeroD == ZeroD = True
1822 (SuccD a) == (SuccD b) = a == b
1825 equalDC :: D [] -> D [] -> Bool;
1828 We need to prove (Eq (D [])). Here's how we go:
1832 by instance decl, holds if
1836 by instance decl of Eq, holds if
1838 where d2 = dfEqList d3
1841 But now we can "tie the knot" to give
1847 and it'll even run! The trick is to put the thing we are trying to prove
1848 (in this case Eq (D []) into the database before trying to prove its
1849 contributing clauses.
1852 %************************************************************************
1854 Reducing a single constraint
1856 %************************************************************************
1859 ---------------------------------------------
1860 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
1861 reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
1862 tci_given = extra_givens, tci_wanted = wanteds })
1863 = reduceImplication env avails reft tvs extra_givens wanteds loc
1865 reduceInst env avails other_inst
1866 = do { result <- lookupSimpleInst other_inst
1867 ; return (avails, result) }
1871 ---------------------------------------------
1872 reduceImplication :: RedEnv
1874 -> Refinement -- May refine the givens; often empty
1875 -> [TcTyVar] -- Quantified type variables; all skolems
1876 -> [Inst] -- Extra givens; all rigid
1879 -> TcM (Avails, LookupInstResult)
1882 Suppose we are simplifying the constraint
1883 forall bs. extras => wanted
1884 in the context of an overall simplification problem with givens 'givens',
1885 and refinment 'reft'.
1888 * The refinement is often empty
1890 * The 'extra givens' need not mention any of the quantified type variables
1891 e.g. forall {}. Eq a => Eq [a]
1892 forall {}. C Int => D (Tree Int)
1894 This happens when you have something like
1896 T1 :: Eq a => a -> T a
1899 f x = ...(case x of { T1 v -> v==v })...
1902 -- ToDo: should we instantiate tvs? I think it's not necessary
1904 -- ToDo: what about improvement? There may be some improvement
1905 -- exposed as a result of the simplifications done by reduceList
1906 -- which are discarded if we back off.
1907 -- This is almost certainly Wrong, but we'll fix it when dealing
1908 -- better with equality constraints
1909 reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
1910 = do { -- Add refined givens, and the extra givens
1911 (refined_red_givens, avails)
1912 <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
1913 else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
1914 ; avails <- foldlM addGiven avails extra_givens
1916 -- Solve the sub-problem
1917 ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
1918 env' = env { red_givens = refined_red_givens ++ extra_givens
1919 , red_try_me = try_me }
1921 ; traceTc (text "reduceImplication" <+> vcat
1923 ppr (red_givens env), ppr extra_givens,
1924 ppr reft, ppr wanteds, ppr avails ])
1925 ; avails <- reduceList env' wanteds avails
1927 -- Extract the results
1928 -- Note [Reducing implication constraints]
1929 ; (binds, irreds) <- extractResults avails wanteds
1930 ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
1932 ; traceTc (text "reduceImplication result" <+> vcat
1933 [ ppr outer, ppr inner, ppr binds])
1935 -- We always discard the extra avails we've generated;
1936 -- but we remember if we have done any (global) improvement
1937 ; let ret_avails = updateImprovement orig_avails avails
1939 ; if isEmptyLHsBinds binds && null outer then -- No progress
1940 return (ret_avails, NoInstance)
1942 { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
1944 ; let dict_ids = map instToId extra_givens
1945 co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
1946 rhs = mkHsWrap co payload
1947 loc = instLocSpan inst_loc
1948 payload | [wanted] <- wanteds = HsVar (instToId wanted)
1949 | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
1951 ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
1955 Note [Reducing implication constraints]
1956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1957 Suppose we are trying to simplify
1958 (Ord a, forall b. C a b => (W [a] b, D c b))
1960 instance (C a b, Ord a) => W [a] b
1961 When solving the implication constraint, we'll start with
1963 in the Avails. Then we add (C a b -> Given) and solve. Extracting
1964 the results gives us a binding for the (W [a] b), with an Irred of
1965 (Ord a, D c b). Now, the (Ord a) comes from "outside" the implication,
1966 but the (D d b) is from "inside". So we want to generate a Rhs binding
1969 ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
1972 ic' :: forall b. C a b => D c b
1974 The 'depending on' part of the Rhs is important, because it drives
1975 the extractResults code.
1977 The "inside" and "outside" distinction is what's going on with 'inner' and
1978 'outer' in reduceImplication
1981 Note [Freeness and implications]
1982 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1983 It's hard to say when an implication constraint can be floated out. Consider
1984 forall {} Eq a => Foo [a]
1985 The (Foo [a]) doesn't mention any of the quantified variables, but it
1986 still might be partially satisfied by the (Eq a).
1988 There is a useful special case when it *is* easy to partition the
1989 constraints, namely when there are no 'givens'. Consider
1990 forall {a}. () => Bar b
1991 There are no 'givens', and so there is no reason to capture (Bar b).
1992 We can let it float out. But if there is even one constraint we
1993 must be much more careful:
1994 forall {a}. C a b => Bar (m b)
1995 because (C a b) might have a superclass (D b), from which we might
1996 deduce (Bar [b]) when m later gets instantiated to []. Ha!
1998 Here is an even more exotic example
2000 Now consider the constraint
2001 forall b. D Int b => C Int
2002 We can satisfy the (C Int) from the superclass of D, so we don't want
2003 to float the (C Int) out, even though it mentions no type variable in
2006 Note [Pruning the givens in an implication constraint]
2007 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2008 Suppose we are about to form the implication constraint
2009 forall tvs. Eq a => Ord b
2010 The (Eq a) cannot contribute to the (Ord b), because it has no access to
2011 the type variable 'b'. So we could filter out the (Eq a) from the givens.
2013 Doing so would be a bit tidier, but all the implication constraints get
2014 simplified away by the optimiser, so it's no great win. So I don't take
2015 advantage of that at the moment.
2017 If you do, BE CAREFUL of wobbly type variables.
2020 %************************************************************************
2022 Avails and AvailHow: the pool of evidence
2024 %************************************************************************
2028 data Avails = Avails !ImprovementDone !AvailEnv
2030 type ImprovementDone = Bool -- True <=> some unification has happened
2031 -- so some Irreds might now be reducible
2032 -- keys that are now
2034 type AvailEnv = FiniteMap Inst AvailHow
2036 = IsIrred -- Used for irreducible dictionaries,
2037 -- which are going to be lambda bound
2039 | Given TcId -- Used for dictionaries for which we have a binding
2040 -- e.g. those "given" in a signature
2042 | Rhs -- Used when there is a RHS
2043 (LHsExpr TcId) -- The RHS
2044 [Inst] -- Insts free in the RHS; we need these too
2046 instance Outputable Avails where
2049 pprAvails (Avails imp avails)
2050 = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
2051 , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
2052 | (inst,avail) <- fmToList avails ])]
2054 instance Outputable AvailHow where
2057 -------------------------
2058 pprAvail :: AvailHow -> SDoc
2059 pprAvail IsIrred = text "Irred"
2060 pprAvail (Given x) = text "Given" <+> ppr x
2061 pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
2063 -------------------------
2064 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
2065 extendAvailEnv env inst avail = addToFM env inst avail
2067 findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
2068 findAvailEnv env wanted = lookupFM env wanted
2069 -- NB 1: the Ord instance of Inst compares by the class/type info
2070 -- *not* by unique. So
2071 -- d1::C Int == d2::C Int
2073 emptyAvails :: Avails
2074 emptyAvails = Avails False emptyFM
2076 findAvail :: Avails -> Inst -> Maybe AvailHow
2077 findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
2079 elemAvails :: Inst -> Avails -> Bool
2080 elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
2082 extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
2084 extendAvails avails@(Avails imp env) inst avail
2085 = do { imp1 <- tcImproveOne avails inst -- Do any improvement
2086 ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
2088 availsInsts :: Avails -> [Inst]
2089 availsInsts (Avails _ avails) = keysFM avails
2091 availsImproved (Avails imp _) = imp
2093 updateImprovement :: Avails -> Avails -> Avails
2094 -- (updateImprovement a1 a2) sets a1's improvement flag from a2
2095 updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
2098 Extracting the bindings from a bunch of Avails.
2099 The bindings do *not* come back sorted in dependency order.
2100 We assume that they'll be wrapped in a big Rec, so that the
2101 dependency analyser can sort them out later
2104 extractResults :: Avails
2106 -> TcM ( TcDictBinds, -- Bindings
2107 [Inst]) -- Irreducible ones
2109 extractResults (Avails _ avails) wanteds
2110 = go avails emptyBag [] wanteds
2112 go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
2113 -> TcM (TcDictBinds, [Inst])
2114 go avails binds irreds []
2115 = returnM (binds, irreds)
2117 go avails binds irreds (w:ws)
2118 = case findAvailEnv avails w of
2119 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
2120 go avails binds irreds ws
2123 | id == w_id -> go avails binds irreds ws
2124 | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
2125 -- The sought Id can be one of the givens, via a superclass chain
2126 -- and then we definitely don't want to generate an x=x binding!
2128 Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
2129 -- The add_given handles the case where we want (Ord a, Eq a), and we
2130 -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
2131 -- This showed up in a dupliated Ord constraint in the error message for
2134 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
2136 new_binds = addBind binds w_id rhs
2140 add_given avails w = extendAvailEnv avails w (Given (instToId w))
2141 -- Don't add the same binding twice
2143 addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
2147 Note [No superclasses for Stop]
2148 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2149 When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
2150 add it to avails, so that any other equal Insts will be commoned up
2151 right here. However, we do *not* add superclasses. If we have
2154 but a is not bound here, then we *don't* want to derive dn from df
2155 here lest we lose sharing.
2158 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
2159 addWanted want_scs avails wanted rhs_expr wanteds
2160 = addAvailAndSCs want_scs avails wanted avail
2162 avail = Rhs rhs_expr wanteds
2164 addGiven :: Avails -> Inst -> TcM Avails
2165 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
2166 -- Always add superclasses for 'givens'
2168 -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
2169 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
2170 -- so the assert isn't true
2172 addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
2173 addRefinedGiven reft (refined_givens, avails) given
2174 | isDict given -- We sometimes have 'given' methods, but they
2175 -- are always optional, so we can drop them
2176 , let pred = dictPred given
2177 , isRefineablePred pred -- See Note [ImplicInst rigidity]
2178 , Just (co, pred) <- refinePred reft pred
2179 = do { new_given <- newDictBndr (instLoc given) pred
2180 ; let rhs = L (instSpan given) $
2181 HsWrap (WpCo co) (HsVar (instToId given))
2182 ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
2183 ; return (new_given:refined_givens, avails) }
2184 -- ToDo: the superclasses of the original given all exist in Avails
2185 -- so we could really just cast them, but it's more awkward to do,
2186 -- and hopefully the optimiser will spot the duplicated work
2188 = return (refined_givens, avails)
2191 Note [ImplicInst rigidity]
2192 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2194 C :: forall ab. (Eq a, Ord b) => b -> T a
2196 ...(case x of C v -> <body>)...
2198 From the case (where x::T ty) we'll get an implication constraint
2199 forall b. (Eq ty, Ord b) => <body-constraints>
2200 Now suppose <body-constraints> itself has an implication constraint
2202 forall c. <reft> => <payload>
2203 Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
2204 existential, but we probably should not apply it to the (Eq ty) because it may
2205 be wobbly. Hence the isRigidInst
2207 @Insts@ are ordered by their class/type info, rather than by their
2208 unique. This allows the context-reduction mechanism to use standard finite
2209 maps to do their stuff. It's horrible that this code is here, rather
2210 than with the Avails handling stuff in TcSimplify
2213 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
2214 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
2215 addAvailAndSCs want_scs avails irred IsIrred
2217 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
2218 addAvailAndSCs want_scs avails inst avail
2219 | not (isClassDict inst) = extendAvails avails inst avail
2220 | NoSCs <- want_scs = extendAvails avails inst avail
2221 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
2222 ; avails' <- extendAvails avails inst avail
2223 ; addSCs is_loop avails' inst }
2225 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
2226 -- Note: this compares by *type*, not by Unique
2227 deps = findAllDeps (unitVarSet (instToId inst)) avail
2228 dep_tys = map idType (varSetElems deps)
2230 findAllDeps :: IdSet -> AvailHow -> IdSet
2231 -- Find all the Insts that this one depends on
2232 -- See Note [SUPERCLASS-LOOP 2]
2233 -- Watch out, though. Since the avails may contain loops
2234 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
2235 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
2236 findAllDeps so_far other = so_far
2238 find_all :: IdSet -> Inst -> IdSet
2240 | kid_id `elemVarSet` so_far = so_far
2241 | Just avail <- findAvail avails kid = findAllDeps so_far' avail
2242 | otherwise = so_far'
2244 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
2245 kid_id = instToId kid
2247 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
2248 -- Add all the superclasses of the Inst to Avails
2249 -- The first param says "dont do this because the original thing
2250 -- depends on this one, so you'd build a loop"
2251 -- Invariant: the Inst is already in Avails.
2253 addSCs is_loop avails dict
2254 = ASSERT( isDict dict )
2255 do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
2256 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
2258 (clas, tys) = getDictClassTys dict
2259 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
2260 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
2262 add_sc avails (sc_dict, sc_sel)
2263 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
2264 | is_given sc_dict = return avails
2265 | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
2266 ; addSCs is_loop avails' sc_dict }
2268 sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
2269 co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
2271 is_given :: Inst -> Bool
2272 is_given sc_dict = case findAvail avails sc_dict of
2273 Just (Given _) -> True -- Given is cheaper than superclass selection
2277 %************************************************************************
2279 \section{tcSimplifyTop: defaulting}
2281 %************************************************************************
2284 @tcSimplifyTop@ is called once per module to simplify all the constant
2285 and ambiguous Insts.
2287 We need to be careful of one case. Suppose we have
2289 instance Num a => Num (Foo a b) where ...
2291 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2292 to (Num x), and default x to Int. But what about y??
2294 It's OK: the final zonking stage should zap y to (), which is fine.
2298 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2299 tcSimplifyTop wanteds
2300 = tc_simplify_top doc False wanteds
2302 doc = text "tcSimplifyTop"
2304 tcSimplifyInteractive wanteds
2305 = tc_simplify_top doc True wanteds
2307 doc = text "tcSimplifyInteractive"
2309 -- The TcLclEnv should be valid here, solely to improve
2310 -- error message generation for the monomorphism restriction
2311 tc_simplify_top doc interactive wanteds
2312 = do { dflags <- getDOpts
2313 ; wanteds <- mapM zonkInst wanteds
2314 ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
2316 ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
2317 ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
2319 -- Use the defaulting rules to do extra unification
2320 -- NB: irreds2 are already zonked
2321 ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
2323 -- Deal with implicit parameters
2324 ; let (bad_ips, non_ips) = partition isIPDict irreds3
2325 (ambigs, others) = partition isTyVarDict non_ips
2327 ; topIPErrs bad_ips -- Can arise from f :: Int -> Int
2329 ; addNoInstanceErrs others
2330 ; addTopAmbigErrs ambigs
2332 ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
2334 doc1 = doc <+> ptext SLIT("(first round)")
2335 doc2 = doc <+> ptext SLIT("(approximate)")
2336 doc3 = doc <+> ptext SLIT("(disambiguate)")
2339 If a dictionary constrains a type variable which is
2340 * not mentioned in the environment
2341 * and not mentioned in the type of the expression
2342 then it is ambiguous. No further information will arise to instantiate
2343 the type variable; nor will it be generalised and turned into an extra
2344 parameter to a function.
2346 It is an error for this to occur, except that Haskell provided for
2347 certain rules to be applied in the special case of numeric types.
2349 * at least one of its classes is a numeric class, and
2350 * all of its classes are numeric or standard
2351 then the type variable can be defaulted to the first type in the
2352 default-type list which is an instance of all the offending classes.
2354 So here is the function which does the work. It takes the ambiguous
2355 dictionaries and either resolves them (producing bindings) or
2356 complains. It works by splitting the dictionary list by type
2357 variable, and using @disambigOne@ to do the real business.
2359 @disambigOne@ assumes that its arguments dictionaries constrain all
2360 the same type variable.
2362 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2363 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2364 the most common use of defaulting is code like:
2366 _ccall_ foo `seqPrimIO` bar
2368 Since we're not using the result of @foo@, the result if (presumably)
2372 disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
2373 -- Just does unification to fix the default types
2374 -- The Insts are assumed to be pre-zonked
2375 disambiguate doc interactive dflags insts
2377 = return (insts, emptyBag)
2379 | null defaultable_groups
2380 = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
2381 ; return (insts, emptyBag) }
2384 = do { -- Figure out what default types to use
2385 default_tys <- getDefaultTys extended_defaulting ovl_strings
2387 ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
2388 ; mapM_ (disambigGroup default_tys) defaultable_groups
2390 -- disambigGroup does unification, hence try again
2391 ; tryHardCheckLoop doc insts }
2394 extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
2395 ovl_strings = dopt Opt_OverloadedStrings dflags
2397 unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
2398 bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
2399 (unaries, bad_tvs_s) = partitionWith find_unary insts
2400 bad_tvs = unionVarSets bad_tvs_s
2402 -- Finds unary type-class constraints
2403 find_unary d@(Dict {tci_pred = ClassP cls [ty]})
2404 | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
2405 find_unary inst = Right (tyVarsOfInst inst)
2407 -- Group by type variable
2408 defaultable_groups :: [[(Inst,Class,TcTyVar)]]
2409 defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
2410 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
2412 defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
2413 defaultable_group ds@((_,_,tv):_)
2414 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
2415 && not (tv `elemVarSet` bad_tvs)
2416 && defaultable_classes [c | (_,c,_) <- ds]
2417 defaultable_group [] = panic "defaultable_group"
2419 defaultable_classes clss
2420 | extended_defaulting = any isInteractiveClass clss
2421 | otherwise = all is_std_class clss && (any is_num_class clss)
2423 -- In interactive mode, or with -fextended-default-rules,
2424 -- we default Show a to Show () to avoid graututious errors on "show []"
2425 isInteractiveClass cls
2426 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2428 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2429 -- is_num_class adds IsString to the standard numeric classes,
2430 -- when -foverloaded-strings is enabled
2432 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2433 -- Similarly is_std_class
2435 -----------------------
2436 disambigGroup :: [Type] -- The default types
2437 -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
2438 -> TcM () -- Just does unification, to fix the default types
2440 disambigGroup default_tys dicts
2441 = try_default default_tys
2443 (_,_,tyvar) = head dicts -- Should be non-empty
2444 classes = [c | (_,c,_) <- dicts]
2446 try_default [] = return ()
2447 try_default (default_ty : default_tys)
2448 = tryTcLIE_ (try_default default_tys) $
2449 do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
2450 -- This may fail; then the tryTcLIE_ kicks in
2451 -- Failure here is caused by there being no type in the
2452 -- default list which can satisfy all the ambiguous classes.
2453 -- For example, if Real a is reqd, but the only type in the
2454 -- default list is Int.
2456 -- After this we can't fail
2457 ; warnDefault dicts default_ty
2458 ; unifyType default_ty (mkTyVarTy tyvar) }
2461 -----------------------
2462 getDefaultTys :: Bool -> Bool -> TcM [Type]
2463 getDefaultTys extended_deflts ovl_strings
2464 = do { mb_defaults <- getDeclaredDefaultTys
2465 ; case mb_defaults of {
2466 Just tys -> return tys ; -- User-supplied defaults
2469 -- No use-supplied default
2470 -- Use [Integer, Double], plus modifications
2471 { integer_ty <- tcMetaTy integerTyConName
2472 ; checkWiredInTyCon doubleTyCon
2473 ; string_ty <- tcMetaTy stringTyConName
2474 ; return (opt_deflt extended_deflts unitTy
2475 -- Note [Default unitTy]
2477 [integer_ty,doubleTy]
2479 opt_deflt ovl_strings string_ty) } } }
2481 opt_deflt True ty = [ty]
2482 opt_deflt False ty = []
2485 Note [Default unitTy]
2486 ~~~~~~~~~~~~~~~~~~~~~
2487 In interative mode (or with -fextended-default-rules) we add () as the first type we
2488 try when defaulting. This has very little real impact, except in the following case.
2490 Text.Printf.printf "hello"
2491 This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
2492 want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
2493 default the 'a' to (), rather than to Integer (which is what would otherwise happen;
2494 and then GHCi doesn't attempt to print the (). So in interactive mode, we add
2495 () to the list of defaulting types. See Trac #1200.
2497 Note [Avoiding spurious errors]
2498 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2499 When doing the unification for defaulting, we check for skolem
2500 type variables, and simply don't default them. For example:
2501 f = (*) -- Monomorphic
2502 g :: Num a => a -> a
2504 Here, we get a complaint when checking the type signature for g,
2505 that g isn't polymorphic enough; but then we get another one when
2506 dealing with the (Num a) context arising from f's definition;
2507 we try to unify a with Int (to default it), but find that it's
2508 already been unified with the rigid variable from g's type sig
2511 %************************************************************************
2513 \subsection[simple]{@Simple@ versions}
2515 %************************************************************************
2517 Much simpler versions when there are no bindings to make!
2519 @tcSimplifyThetas@ simplifies class-type constraints formed by
2520 @deriving@ declarations and when specialising instances. We are
2521 only interested in the simplified bunch of class/type constraints.
2523 It simplifies to constraints of the form (C a b c) where
2524 a,b,c are type variables. This is required for the context of
2525 instance declarations.
2528 tcSimplifyDeriv :: InstOrigin
2530 -> ThetaType -- Wanted
2531 -> TcM ThetaType -- Needed
2532 -- Given instance (wanted) => C inst_ty
2533 -- Simplify 'wanted' as much as possible
2534 -- The inst_ty is needed only for the termination check
2536 tcSimplifyDeriv orig tyvars theta
2537 = do { (tvs, _, tenv) <- tcInstTyVars tyvars
2538 -- The main loop may do unification, and that may crash if
2539 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2540 -- ToDo: what if two of them do get unified?
2541 ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
2542 ; (irreds, _) <- tryHardCheckLoop doc wanteds
2544 ; let (tv_dicts, others) = partition isTyVarDict irreds
2545 ; addNoInstanceErrs others
2547 ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2548 simpl_theta = substTheta rev_env (map dictPred tv_dicts)
2549 -- This reverse-mapping is a pain, but the result
2550 -- should mention the original TyVars not TcTyVars
2552 ; return simpl_theta }
2554 doc = ptext SLIT("deriving classes for a data type")
2557 Note [Exotic derived instance contexts]
2558 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2560 data T a b c = MkT (Foo a b c) deriving( Eq )
2561 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
2563 Notice that this instance (just) satisfies the Paterson termination
2564 conditions. Then we *could* derive an instance decl like this:
2566 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
2568 even though there is no instance for (C Int a), because there just
2569 *might* be an instance for, say, (C Int Bool) at a site where we
2570 need the equality instance for T's.
2572 However, this seems pretty exotic, and it's quite tricky to allow
2573 this, and yet give sensible error messages in the (much more common)
2574 case where we really want that instance decl for C.
2576 So for now we simply require that the derived instance context
2577 should have only type-variable constraints.
2579 Here is another example:
2580 data Fix f = In (f (Fix f)) deriving( Eq )
2581 Here, if we are prepared to allow -fallow-undecidable-instances we
2582 could derive the instance
2583 instance Eq (f (Fix f)) => Eq (Fix f)
2584 but this is so delicate that I don't think it should happen inside
2585 'deriving'. If you want this, write it yourself!
2587 NB: if you want to lift this condition, make sure you still meet the
2588 termination conditions! If not, the deriving mechanism generates
2589 larger and larger constraints. Example:
2591 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
2593 Note the lack of a Show instance for Succ. First we'll generate
2594 instance (Show (Succ a), Show a) => Show (Seq a)
2596 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
2597 and so on. Instead we want to complain of no instance for (Show (Succ a)).
2600 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2601 used with \tr{default} declarations. We are only interested in
2602 whether it worked or not.
2605 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2608 tcSimplifyDefault theta
2609 = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
2610 tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) ->
2611 addNoInstanceErrs irreds `thenM_`
2617 doc = ptext SLIT("default declaration")
2621 %************************************************************************
2623 \section{Errors and contexts}
2625 %************************************************************************
2627 ToDo: for these error messages, should we note the location as coming
2628 from the insts, or just whatever seems to be around in the monad just
2632 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2633 -> [Inst] -- The offending Insts
2635 -- Group together insts with the same origin
2636 -- We want to report them together in error messages
2638 groupErrs report_err []
2640 groupErrs report_err (inst:insts)
2641 = do_one (inst:friends) `thenM_`
2642 groupErrs report_err others
2645 -- (It may seem a bit crude to compare the error messages,
2646 -- but it makes sure that we combine just what the user sees,
2647 -- and it avoids need equality on InstLocs.)
2648 (friends, others) = partition is_friend insts
2649 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2650 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2651 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2652 -- Add location and context information derived from the Insts
2654 -- Add the "arising from..." part to a message about bunch of dicts
2655 addInstLoc :: [Inst] -> Message -> Message
2656 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
2658 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2659 addTopIPErrs bndrs []
2661 addTopIPErrs bndrs ips
2662 = do { dflags <- getDOpts
2663 ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
2665 (tidy_env, tidy_ips) = tidyInsts ips
2667 = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2668 nest 2 (ptext SLIT("the monomorphic top-level binding")
2669 <> plural bndrs <+> ptext SLIT("of")
2670 <+> pprBinders bndrs <> colon)],
2671 nest 2 (vcat (map ppr_ip ips)),
2672 monomorphism_fix dflags]
2673 ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
2675 topIPErrs :: [Inst] -> TcM ()
2677 = groupErrs report tidy_dicts
2679 (tidy_env, tidy_dicts) = tidyInsts dicts
2680 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2681 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2682 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2684 addNoInstanceErrs :: [Inst] -- Wanted (can include implications)
2686 addNoInstanceErrs insts
2687 = do { let (tidy_env, tidy_insts) = tidyInsts insts
2688 ; reportNoInstances tidy_env Nothing tidy_insts }
2692 -> Maybe (InstLoc, [Inst]) -- Context
2693 -- Nothing => top level
2694 -- Just (d,g) => d describes the construct
2696 -> [Inst] -- What is wanted (can include implications)
2699 reportNoInstances tidy_env mb_what insts
2700 = groupErrs (report_no_instances tidy_env mb_what) insts
2702 report_no_instances tidy_env mb_what insts
2703 = do { inst_envs <- tcGetInstEnvs
2704 ; let (implics, insts1) = partition isImplicInst insts
2705 (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
2706 ; traceTc (text "reportNoInstnces" <+> vcat
2707 [ppr implics, ppr insts1, ppr insts2])
2708 ; mapM_ complain_implic implics
2709 ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
2710 ; groupErrs complain_no_inst insts2 }
2712 complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
2714 complain_implic inst -- Recurse!
2715 = reportNoInstances tidy_env
2716 (Just (tci_loc inst, tci_given inst))
2719 check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
2720 -- Right msg => overlap message
2721 -- Left inst => no instance
2722 check_overlap inst_envs wanted
2723 | not (isClassDict wanted) = Left wanted
2725 = case lookupInstEnv inst_envs clas tys of
2726 -- The case of exactly one match and no unifiers means
2727 -- a successful lookup. That can't happen here, becuase
2728 -- dicts only end up here if they didn't match in Inst.lookupInst
2730 ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
2732 ([], _) -> Left wanted -- No match
2733 res -> Right (mk_overlap_msg wanted res)
2735 (clas,tys) = getDictClassTys wanted
2737 mk_overlap_msg dict (matches, unifiers)
2738 = ASSERT( not (null matches) )
2739 vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2740 <+> pprPred (dictPred dict))),
2741 sep [ptext SLIT("Matching instances") <> colon,
2742 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2743 if not (isSingleton matches)
2744 then -- Two or more matches
2746 else -- One match, plus some unifiers
2747 ASSERT( not (null unifiers) )
2748 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2749 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2750 ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
2751 ptext SLIT("when compiling the other instance declarations")])]
2753 ispecs = [ispec | (ispec, _) <- matches]
2755 mk_no_inst_err insts
2756 | null insts = empty
2758 | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
2759 not (isEmptyVarSet (tyVarsOfInsts insts))
2760 = vcat [ addInstLoc insts $
2761 sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts
2762 , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens]
2763 , show_fixes (fix1 loc : fixes2) ]
2765 | otherwise -- Top level
2766 = vcat [ addInstLoc insts $
2767 ptext SLIT("No instance") <> plural insts
2768 <+> ptext SLIT("for") <+> pprDictsTheta insts
2769 , show_fixes fixes2 ]
2772 fix1 loc = sep [ ptext SLIT("add") <+> pprDictsTheta insts
2773 <+> ptext SLIT("to the context of"),
2774 nest 2 (ppr (instLocOrigin loc)) ]
2775 -- I'm not sure it helps to add the location
2776 -- nest 2 (ptext SLIT("at") <+> ppr (instLocSpan loc)) ]
2778 fixes2 | null instance_dicts = []
2779 | otherwise = [sep [ptext SLIT("add an instance declaration for"),
2780 pprDictsTheta instance_dicts]]
2781 instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
2782 -- Insts for which it is worth suggesting an adding an instance declaration
2783 -- Exclude implicit parameters, and tyvar dicts
2785 show_fixes :: [SDoc] -> SDoc
2786 show_fixes [] = empty
2787 show_fixes (f:fs) = sep [ptext SLIT("Possible fix:"),
2788 nest 2 (vcat (f : map (ptext SLIT("or") <+>) fs))]
2790 addTopAmbigErrs dicts
2791 -- Divide into groups that share a common set of ambiguous tyvars
2792 = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened
2793 -- See Note [Avoiding spurious errors]
2794 mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2796 (tidy_env, tidy_dicts) = tidyInsts dicts
2798 tvs_of :: Inst -> [TcTyVar]
2799 tvs_of d = varSetElems (tyVarsOfInst d)
2800 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2802 report :: [(Inst,[TcTyVar])] -> TcM ()
2803 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2804 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2805 setSrcSpan (instSpan inst) $
2806 -- the location of the first one will do for the err message
2807 addErrTcM (tidy_env, msg $$ mono_msg)
2809 dicts = map fst pairs
2810 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2811 pprQuotedList tvs <+> in_msg,
2812 nest 2 (pprDictsInFull dicts)]
2813 in_msg = text "in the constraint" <> plural dicts <> colon
2814 report [] = panic "addTopAmbigErrs"
2817 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2818 -- There's an error with these Insts; if they have free type variables
2819 -- it's probably caused by the monomorphism restriction.
2820 -- Try to identify the offending variable
2821 -- ASSUMPTION: the Insts are fully zonked
2822 mkMonomorphismMsg tidy_env inst_tvs
2823 = do { dflags <- getDOpts
2824 ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
2825 ; return (tidy_env, mk_msg dflags docs) }
2827 mk_msg _ _ | any isRuntimeUnk inst_tvs
2828 = vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
2829 (pprWithCommas ppr inst_tvs),
2830 ptext SLIT("Use :print or :force to determine these types")]
2831 mk_msg _ [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2832 -- This happens in things like
2833 -- f x = show (read "foo")
2834 -- where monomorphism doesn't play any role
2836 = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2838 monomorphism_fix dflags]
2840 isRuntimeUnk :: TcTyVar -> Bool
2841 isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
2844 monomorphism_fix :: DynFlags -> SDoc
2845 monomorphism_fix dflags
2846 = ptext SLIT("Probable fix:") <+> vcat
2847 [ptext SLIT("give these definition(s) an explicit type signature"),
2848 if dopt Opt_MonomorphismRestriction dflags
2849 then ptext SLIT("or use -fno-monomorphism-restriction")
2850 else empty] -- Only suggest adding "-fno-monomorphism-restriction"
2851 -- if it is not already set!
2853 warnDefault ups default_ty
2854 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2855 addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
2857 dicts = [d | (d,_,_) <- ups]
2860 (_, tidy_dicts) = tidyInsts dicts
2861 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2862 quotes (ppr default_ty),
2863 pprDictsInFull tidy_dicts]
2865 reduceDepthErr n stack
2866 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2867 ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
2868 nest 4 (pprStack stack)]
2870 pprStack stack = vcat (map pprInstInFull stack)