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,
23 #include "HsVersions.h"
25 import {-# SOURCE #-} TcUnify( unifyType )
66 %************************************************************************
70 %************************************************************************
72 --------------------------------------
73 Notes on functional dependencies (a bug)
74 --------------------------------------
81 instance D a b => C a b -- Undecidable
82 -- (Not sure if it's crucial to this eg)
83 f :: C a b => a -> Bool
86 g :: C a b => a -> Bool
89 Here f typechecks, but g does not!! Reason: before doing improvement,
90 we reduce the (C a b1) constraint from the call of f to (D a b1).
92 Here is a more complicated example:
94 | > class Foo a b | a->b
96 | > class Bar a b | a->b
100 | > instance Bar Obj Obj
102 | > instance (Bar a b) => Foo a b
104 | > foo:: (Foo a b) => a -> String
107 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
113 | Could not deduce (Bar a b) from the context (Foo a b)
114 | arising from use of `foo' at <interactive>:1
116 | Add (Bar a b) to the expected type of an expression
117 | In the first argument of `runFoo', namely `foo'
118 | In the definition of `it': it = runFoo foo
120 | Why all of the sudden does GHC need the constraint Bar a b? The
121 | function foo didn't ask for that...
123 The trouble is that to type (runFoo foo), GHC has to solve the problem:
125 Given constraint Foo a b
126 Solve constraint Foo a b'
128 Notice that b and b' aren't the same. To solve this, just do
129 improvement and then they are the same. But GHC currently does
134 That is usually fine, but it isn't here, because it sees that Foo a b is
135 not the same as Foo a b', and so instead applies the instance decl for
136 instance Bar a b => Foo a b. And that's where the Bar constraint comes
139 The Right Thing is to improve whenever the constraint set changes at
140 all. Not hard in principle, but it'll take a bit of fiddling to do.
142 Note [Choosing which variables to quantify]
143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
144 Suppose we are about to do a generalisation step. We have in our hand
147 T the type of the RHS
148 C the constraints from that RHS
150 The game is to figure out
152 Q the set of type variables over which to quantify
153 Ct the constraints we will *not* quantify over
154 Cq the constraints we will quantify over
156 So we're going to infer the type
160 and float the constraints Ct further outwards.
162 Here are the things that *must* be true:
164 (A) Q intersect fv(G) = EMPTY limits how big Q can be
165 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
167 (A) says we can't quantify over a variable that's free in the environment.
168 (B) says we must quantify over all the truly free variables in T, else
169 we won't get a sufficiently general type.
171 We do not *need* to quantify over any variable that is fixed by the
172 free vars of the environment G.
174 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
176 Example: class H x y | x->y where ...
178 fv(G) = {a} C = {H a b, H c d}
181 (A) Q intersect {a} is empty
182 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
184 So Q can be {c,d}, {b,c,d}
186 In particular, it's perfectly OK to quantify over more type variables
187 than strictly necessary; there is no need to quantify over 'b', since
188 it is determined by 'a' which is free in the envt, but it's perfectly
189 OK to do so. However we must not quantify over 'a' itself.
191 Other things being equal, however, we'd like to quantify over as few
192 variables as possible: smaller types, fewer type applications, more
193 constraints can get into Ct instead of Cq. Here's a good way to
196 Q = grow( fv(T), C ) \ oclose( fv(G), C )
198 That is, quantify over all variable that that MIGHT be fixed by the
199 call site (which influences T), but which aren't DEFINITELY fixed by
200 G. This choice definitely quantifies over enough type variables,
201 albeit perhaps too many.
203 Why grow( fv(T), C ) rather than fv(T)? Consider
205 class H x y | x->y where ...
210 If we used fv(T) = {c} we'd get the type
212 forall c. H c d => c -> b
214 And then if the fn was called at several different c's, each of
215 which fixed d differently, we'd get a unification error, because
216 d isn't quantified. Solution: quantify d. So we must quantify
217 everything that might be influenced by c.
219 Why not oclose( fv(T), C )? Because we might not be able to see
220 all the functional dependencies yet:
222 class H x y | x->y where ...
223 instance H x y => Eq (T x y) where ...
228 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
229 apparent yet, and that's wrong. We must really quantify over d too.
231 There really isn't any point in quantifying over any more than
232 grow( fv(T), C ), because the call sites can't possibly influence
233 any other type variables.
237 -------------------------------------
239 -------------------------------------
241 It's very hard to be certain when a type is ambiguous. Consider
245 instance H x y => K (x,y)
247 Is this type ambiguous?
248 forall a b. (K (a,b), Eq b) => a -> a
250 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
251 now we see that a fixes b. So we can't tell about ambiguity for sure
252 without doing a full simplification. And even that isn't possible if
253 the context has some free vars that may get unified. Urgle!
255 Here's another example: is this ambiguous?
256 forall a b. Eq (T b) => a -> a
257 Not if there's an insance decl (with no context)
258 instance Eq (T b) where ...
260 You may say of this example that we should use the instance decl right
261 away, but you can't always do that:
263 class J a b where ...
264 instance J Int b where ...
266 f :: forall a b. J a b => a -> a
268 (Notice: no functional dependency in J's class decl.)
269 Here f's type is perfectly fine, provided f is only called at Int.
270 It's premature to complain when meeting f's signature, or even
271 when inferring a type for f.
275 However, we don't *need* to report ambiguity right away. It'll always
276 show up at the call site.... and eventually at main, which needs special
277 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
279 So here's the plan. We WARN about probable ambiguity if
281 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
283 (all tested before quantification).
284 That is, all the type variables in Cq must be fixed by the the variables
285 in the environment, or by the variables in the type.
287 Notice that we union before calling oclose. Here's an example:
289 class J a b c | a b -> c
293 forall b c. (J a b c) => b -> b
295 Only if we union {a} from G with {b} from T before using oclose,
296 do we see that c is fixed.
298 It's a bit vague exactly which C we should use for this oclose call. If we
299 don't fix enough variables we might complain when we shouldn't (see
300 the above nasty example). Nothing will be perfect. That's why we can
301 only issue a warning.
304 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
306 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
308 then c is a "bubble"; there's no way it can ever improve, and it's
309 certainly ambiguous. UNLESS it is a constant (sigh). And what about
314 instance H x y => K (x,y)
316 Is this type ambiguous?
317 forall a b. (K (a,b), Eq b) => a -> a
319 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
320 is a "bubble" that's a set of constraints
322 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
324 Hence another idea. To decide Q start with fv(T) and grow it
325 by transitive closure in Cq (no functional dependencies involved).
326 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
327 The definitely-ambiguous can then float out, and get smashed at top level
328 (which squashes out the constants, like Eq (T a) above)
331 --------------------------------------
332 Notes on principal types
333 --------------------------------------
338 f x = let g y = op (y::Int) in True
340 Here the principal type of f is (forall a. a->a)
341 but we'll produce the non-principal type
342 f :: forall a. C Int => a -> a
345 --------------------------------------
346 The need for forall's in constraints
347 --------------------------------------
349 [Exchange on Haskell Cafe 5/6 Dec 2000]
351 class C t where op :: t -> Bool
352 instance C [t] where op x = True
354 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
355 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
357 The definitions of p and q differ only in the order of the components in
358 the pair on their right-hand sides. And yet:
360 ghc and "Typing Haskell in Haskell" reject p, but accept q;
361 Hugs rejects q, but accepts p;
362 hbc rejects both p and q;
363 nhc98 ... (Malcolm, can you fill in the blank for us!).
365 The type signature for f forces context reduction to take place, and
366 the results of this depend on whether or not the type of y is known,
367 which in turn depends on which component of the pair the type checker
370 Solution: if y::m a, float out the constraints
371 Monad m, forall c. C (m c)
372 When m is later unified with [], we can solve both constraints.
375 --------------------------------------
376 Notes on implicit parameters
377 --------------------------------------
379 Note [Inheriting implicit parameters]
380 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
385 where f is *not* a top-level binding.
386 From the RHS of f we'll get the constraint (?y::Int).
387 There are two types we might infer for f:
391 (so we get ?y from the context of f's definition), or
393 f :: (?y::Int) => Int -> Int
395 At first you might think the first was better, becuase then
396 ?y behaves like a free variable of the definition, rather than
397 having to be passed at each call site. But of course, the WHOLE
398 IDEA is that ?y should be passed at each call site (that's what
399 dynamic binding means) so we'd better infer the second.
401 BOTTOM LINE: when *inferring types* you *must* quantify
402 over implicit parameters. See the predicate isFreeWhenInferring.
405 Note [Implicit parameters and ambiguity]
406 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
407 What type should we infer for this?
408 f x = (show ?y, x::Int)
409 Since we must quantify over the ?y, the most plausible type is
410 f :: (Show a, ?y::a) => Int -> (String, Int)
411 But notice that the type of the RHS is (String,Int), with no type
412 varibables mentioned at all! The type of f looks ambiguous. But
413 it isn't, because at a call site we might have
414 let ?y = 5::Int in f 7
415 and all is well. In effect, implicit parameters are, well, parameters,
416 so we can take their type variables into account as part of the
417 "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
420 Question 2: type signatures
421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
422 BUT WATCH OUT: When you supply a type signature, we can't force you
423 to quantify over implicit parameters. For example:
427 This is perfectly reasonable. We do not want to insist on
429 (?x + 1) :: (?x::Int => Int)
431 That would be silly. Here, the definition site *is* the occurrence site,
432 so the above strictures don't apply. Hence the difference between
433 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
434 and tcSimplifyCheckBind (which does not).
436 What about when you supply a type signature for a binding?
437 Is it legal to give the following explicit, user type
438 signature to f, thus:
443 At first sight this seems reasonable, but it has the nasty property
444 that adding a type signature changes the dynamic semantics.
447 (let f x = (x::Int) + ?y
448 in (f 3, f 3 with ?y=5)) with ?y = 6
454 in (f 3, f 3 with ?y=5)) with ?y = 6
458 Indeed, simply inlining f (at the Haskell source level) would change the
461 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
462 semantics for a Haskell program without knowing its typing, so if you
463 change the typing you may change the semantics.
465 To make things consistent in all cases where we are *checking* against
466 a supplied signature (as opposed to inferring a type), we adopt the
469 a signature does not need to quantify over implicit params.
471 [This represents a (rather marginal) change of policy since GHC 5.02,
472 which *required* an explicit signature to quantify over all implicit
473 params for the reasons mentioned above.]
475 But that raises a new question. Consider
477 Given (signature) ?x::Int
478 Wanted (inferred) ?x::Int, ?y::Bool
480 Clearly we want to discharge the ?x and float the ?y out. But
481 what is the criterion that distinguishes them? Clearly it isn't
482 what free type variables they have. The Right Thing seems to be
483 to float a constraint that
484 neither mentions any of the quantified type variables
485 nor any of the quantified implicit parameters
487 See the predicate isFreeWhenChecking.
490 Question 3: monomorphism
491 ~~~~~~~~~~~~~~~~~~~~~~~~
492 There's a nasty corner case when the monomorphism restriction bites:
496 The argument above suggests that we *must* generalise
497 over the ?y parameter, to get
498 z :: (?y::Int) => Int,
499 but the monomorphism restriction says that we *must not*, giving
501 Why does the momomorphism restriction say this? Because if you have
503 let z = x + ?y in z+z
505 you might not expect the addition to be done twice --- but it will if
506 we follow the argument of Question 2 and generalise over ?y.
509 Question 4: top level
510 ~~~~~~~~~~~~~~~~~~~~~
511 At the top level, monomorhism makes no sense at all.
514 main = let ?x = 5 in print foo
518 woggle :: (?x :: Int) => Int -> Int
521 We definitely don't want (foo :: Int) with a top-level implicit parameter
522 (?x::Int) becuase there is no way to bind it.
527 (A) Always generalise over implicit parameters
528 Bindings that fall under the monomorphism restriction can't
532 * Inlining remains valid
533 * No unexpected loss of sharing
534 * But simple bindings like
536 will be rejected, unless you add an explicit type signature
537 (to avoid the monomorphism restriction)
538 z :: (?y::Int) => Int
540 This seems unacceptable
542 (B) Monomorphism restriction "wins"
543 Bindings that fall under the monomorphism restriction can't
545 Always generalise over implicit parameters *except* for bindings
546 that fall under the monomorphism restriction
549 * Inlining isn't valid in general
550 * No unexpected loss of sharing
551 * Simple bindings like
553 accepted (get value of ?y from binding site)
555 (C) Always generalise over implicit parameters
556 Bindings that fall under the monomorphism restriction can't
557 be generalised, EXCEPT for implicit parameters
559 * Inlining remains valid
560 * Unexpected loss of sharing (from the extra generalisation)
561 * Simple bindings like
563 accepted (get value of ?y from occurrence sites)
568 None of these choices seems very satisfactory. But at least we should
569 decide which we want to do.
571 It's really not clear what is the Right Thing To Do. If you see
575 would you expect the value of ?y to be got from the *occurrence sites*
576 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
577 case of function definitions, the answer is clearly the former, but
578 less so in the case of non-fucntion definitions. On the other hand,
579 if we say that we get the value of ?y from the definition site of 'z',
580 then inlining 'z' might change the semantics of the program.
582 Choice (C) really says "the monomorphism restriction doesn't apply
583 to implicit parameters". Which is fine, but remember that every
584 innocent binding 'x = ...' that mentions an implicit parameter in
585 the RHS becomes a *function* of that parameter, called at each
586 use of 'x'. Now, the chances are that there are no intervening 'with'
587 clauses that bind ?y, so a decent compiler should common up all
588 those function calls. So I think I strongly favour (C). Indeed,
589 one could make a similar argument for abolishing the monomorphism
590 restriction altogether.
592 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
596 %************************************************************************
598 \subsection{tcSimplifyInfer}
600 %************************************************************************
602 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
604 1. Compute Q = grow( fvs(T), C )
606 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
607 predicates will end up in Ct; we deal with them at the top level
609 3. Try improvement, using functional dependencies
611 4. If Step 3 did any unification, repeat from step 1
612 (Unification can change the result of 'grow'.)
614 Note: we don't reduce dictionaries in step 2. For example, if we have
615 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
616 after step 2. However note that we may therefore quantify over more
617 type variables than we absolutely have to.
619 For the guts, we need a loop, that alternates context reduction and
620 improvement with unification. E.g. Suppose we have
622 class C x y | x->y where ...
624 and tcSimplify is called with:
626 Then improvement unifies a with b, giving
629 If we need to unify anything, we rattle round the whole thing all over
636 -> TcTyVarSet -- fv(T); type vars
638 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)
639 [Inst], -- Dict Ids that must be bound here (zonked)
640 TcDictBinds) -- Bindings
641 -- Any free (escaping) Insts are tossed into the environment
646 tcSimplifyInfer doc tau_tvs wanted
647 = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
648 ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
649 ; gbl_tvs <- tcGetGlobalTyVars
650 ; let preds1 = fdPredsOfInsts wanted'
651 gbl_tvs1 = oclose preds1 gbl_tvs
652 qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
653 -- See Note [Choosing which variables to quantify]
655 -- To maximise sharing, remove from consideration any
656 -- constraints that don't mention qtvs at all
657 ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
660 -- To make types simple, reduce as much as possible
661 ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
662 ppr gbl_tvs1 $$ ppr free $$ ppr bound))
663 ; (irreds1, binds1) <- tryHardCheckLoop doc bound
665 -- Note [Inference and implication constraints]
666 ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
667 ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
669 -- Now work out all over again which type variables to quantify,
670 -- exactly in the same way as before, but starting from irreds2. Why?
671 -- a) By now improvment may have taken place, and we must *not*
672 -- quantify over any variable free in the environment
673 -- tc137 (function h inside g) is an example
675 -- b) Do not quantify over constraints that *now* do not
676 -- mention quantified type variables, because they are
677 -- simply ambiguous (or might be bound further out). Example:
678 -- f :: Eq b => a -> (a, b)
680 -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
681 -- We decide to quantify over 'alpha' alone, but free1 does not include f77
682 -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
683 -- constraint (Eq beta), which we dump back into the free set
684 -- See test tcfail181
686 -- c) irreds may contain type variables not previously mentioned,
687 -- e.g. instance D a x => Foo [a]
689 -- Then after simplifying we'll get (D a x), and x is fresh
690 -- We must quantify over x else it'll be totally unbound
691 ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
692 ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
693 -- Note that we start from gbl_tvs1
694 -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
695 -- we've already put some of the original preds1 into frees
696 -- E.g. wanteds = C a b (where a->b)
699 -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
700 -- irreds2 will be empty. But we don't want to generalise over b!
701 ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
702 qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
703 ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
706 -- Turn the quantified meta-type variables into real type variables
707 ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
709 -- We can't abstract over any remaining unsolved
710 -- implications so instead just float them outwards. Ugh.
711 ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
712 ; loc <- getInstLoc (ImplicOrigin doc)
713 ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
715 -- Prepare equality instances for quantification
716 ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
717 ; q_eqs <- mappM finalizeEqInst q_eqs0
719 ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
720 -- NB: when we are done, we might have some bindings, but
721 -- the final qtvs might be empty. See Note [NO TYVARS] below.
723 approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
724 -- Note [Inference and implication constraints]
725 -- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
726 -- - fetching any dicts inside them that are free
727 -- - using those dicts as cruder constraints, to solve the implications
728 -- - returning the extra ones too
730 approximateImplications doc want_dict irreds
732 = return (irreds, emptyBag)
734 = do { extra_dicts' <- mapM cloneDict extra_dicts
735 ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
736 -- By adding extra_dicts', we make them
737 -- available to solve the implication constraints
739 extra_dicts = get_dicts (filter isImplicInst irreds)
741 get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
742 -- Find the wanted constraints in implication constraints that satisfy
743 -- want_dict, and are not bound by forall's in the constraint itself
744 get_dicts ds = concatMap get_dict ds
746 get_dict d@(Dict {}) | want_dict d = [d]
748 get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
749 = [ d | let tv_set = mkVarSet tvs
750 , d <- get_dicts wanteds
751 , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
752 get_dict i@(EqInst {}) | want_dict i = [i]
754 get_dict other = pprPanic "approximateImplications" (ppr other)
757 Note [Inference and implication constraints]
758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
759 Suppose we have a wanted implication constraint (perhaps arising from
760 a nested pattern match) like
762 and we are now trying to quantify over 'a' when inferring the type for
763 a function. In principle it's possible that there might be an instance
764 instance (C a, E a) => D [a]
765 so the context (E a) would suffice. The Right Thing is to abstract over
766 the implication constraint, but we don't do that (a) because it'll be
767 surprising to programmers and (b) because we don't have the machinery to deal
768 with 'given' implications.
770 So our best approximation is to make (D [a]) part of the inferred
771 context, so we can use that to discharge the implication. Hence
772 the strange function get_dictsin approximateImplications.
774 The common cases are more clear-cut, when we have things like
776 Here, abstracting over (C b) is not an approximation at all -- but see
777 Note [Freeness and implications].
779 See Trac #1430 and test tc228.
783 -----------------------------------------------------------
784 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
785 -- against, but we don't know the type variables over which we are going to quantify.
786 -- This happens when we have a type signature for a mutually recursive group
789 -> TcTyVarSet -- fv(T)
792 -> TcM ([TyVar], -- Fully zonked, and quantified
793 TcDictBinds) -- Bindings
795 tcSimplifyInferCheck loc tau_tvs givens wanteds
796 = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
797 ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
799 -- Figure out which type variables to quantify over
800 -- You might think it should just be the signature tyvars,
801 -- but in bizarre cases you can get extra ones
802 -- f :: forall a. Num a => a -> a
803 -- f x = fst (g (x, head [])) + 1
805 -- Here we infer g :: forall a b. a -> b -> (b,a)
806 -- We don't want g to be monomorphic in b just because
807 -- f isn't quantified over b.
808 ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
809 ; all_tvs <- zonkTcTyVarsAndFV all_tvs
810 ; gbl_tvs <- tcGetGlobalTyVars
811 ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs)
812 -- We could close gbl_tvs, but its not necessary for
813 -- soundness, and it'll only affect which tyvars, not which
814 -- dictionaries, we quantify over
816 ; qtvs' <- zonkQuantifiedTyVars qtvs
818 -- Now we are back to normal (c.f. tcSimplCheck)
819 ; implic_bind <- bindIrreds loc qtvs' givens irreds
821 ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
822 ; return (qtvs', binds `unionBags` implic_bind) }
825 Note [Squashing methods]
826 ~~~~~~~~~~~~~~~~~~~~~~~~~
827 Be careful if you want to float methods more:
828 truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
829 From an application (truncate f i) we get
832 If we have also have a second occurrence of truncate, we get
835 When simplifying with i,f free, we might still notice that
836 t1=t3; but alas, the binding for t2 (which mentions t1)
837 may continue to float out!
842 class Y a b | a -> b where
845 instance Y [[a]] a where
848 k :: X a -> X a -> X a
850 g :: Num a => [X a] -> [X a]
853 h ys = ys ++ map (k (y [[0]])) xs
855 The excitement comes when simplifying the bindings for h. Initially
856 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
857 From this we get t1:=:t2, but also various bindings. We can't forget
858 the bindings (because of [LOOP]), but in fact t1 is what g is
861 The net effect of [NO TYVARS]
864 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
865 isFreeWhenInferring qtvs inst
866 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
867 && isInheritableInst inst -- and no implicit parameter involved
868 -- see Note [Inheriting implicit parameters]
870 {- No longer used (with implication constraints)
871 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
872 -> NameSet -- Quantified implicit parameters
874 isFreeWhenChecking qtvs ips inst
875 = isFreeWrtTyVars qtvs inst
876 && isFreeWrtIPs ips inst
879 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
880 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
884 %************************************************************************
886 \subsection{tcSimplifyCheck}
888 %************************************************************************
890 @tcSimplifyCheck@ is used when we know exactly the set of variables
891 we are going to quantify over. For example, a class or instance declaration.
894 -----------------------------------------------------------
895 -- tcSimplifyCheck is used when checking expression type signatures,
896 -- class decls, instance decls etc.
897 tcSimplifyCheck :: InstLoc
898 -> [TcTyVar] -- Quantify over these
901 -> TcM TcDictBinds -- Bindings
902 tcSimplifyCheck loc qtvs givens wanteds
903 = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
904 do { traceTc (text "tcSimplifyCheck")
905 ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
906 ; implic_bind <- bindIrreds loc qtvs givens irreds
907 ; return (binds `unionBags` implic_bind) }
909 -----------------------------------------------------------
910 -- tcSimplifyCheckPat is used for existential pattern match
911 tcSimplifyCheckPat :: InstLoc
912 -> [CoVar] -> Refinement
913 -> [TcTyVar] -- Quantify over these
916 -> TcM TcDictBinds -- Bindings
917 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
918 = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
919 do { traceTc (text "tcSimplifyCheckPat")
920 ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
921 ; implic_bind <- bindIrredsR loc qtvs co_vars reft
923 ; return (binds `unionBags` implic_bind) }
925 -----------------------------------------------------------
926 bindIrreds :: InstLoc -> [TcTyVar]
929 bindIrreds loc qtvs givens irreds
930 = bindIrredsR loc qtvs [] emptyRefinement givens irreds
932 bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
933 -> Refinement -> [Inst] -> [Inst]
935 -- Make a binding that binds 'irreds', by generating an implication
936 -- constraint for them, *and* throwing the constraint into the LIE
937 bindIrredsR loc qtvs co_vars reft givens irreds
941 = do { let givens' = filter isDict givens
942 -- The givens can include methods
943 -- See Note [Pruning the givens in an implication constraint]
945 -- If there are no 'givens' *and* the refinement is empty
946 -- (the refinement is like more givens), then it's safe to
947 -- partition the 'wanteds' by their qtvs, thereby trimming irreds
948 -- See Note [Freeness and implications]
949 ; irreds' <- if null givens' && isEmptyRefinement reft
951 { let qtv_set = mkVarSet qtvs
952 (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
954 ; return real_irreds }
957 ; let all_tvs = qtvs ++ co_vars -- Abstract over all these
958 ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
959 -- This call does the real work
960 -- If irreds' is empty, it does something sensible
965 makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
967 -> TcM ([Inst], TcDictBinds)
968 -- Make a binding that binds 'irreds', by generating an implication
969 -- constraint for them, *and* throwing the constraint into the LIE
970 -- The binding looks like
971 -- (ir1, .., irn) = f qtvs givens
972 -- where f is (evidence for) the new implication constraint
973 -- f :: forall qtvs. {reft} givens => (ir1, .., irn)
974 -- qtvs includes coercion variables
976 -- This binding must line up the 'rhs' in reduceImplication
977 makeImplicationBind loc all_tvs reft
978 givens -- Guaranteed all Dicts (TOMDO: true?)
980 | null irreds -- If there are no irreds, we are done
981 = return ([], emptyBag)
982 | otherwise -- Otherwise we must generate a binding
983 = do { uniq <- newUnique
984 ; span <- getSrcSpanM
985 ; let (eq_givens,dict_givens) = partitionGivenEqInsts givens
986 eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
987 ; let name = mkInternalName uniq (mkVarOcc "ic") span
988 implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
989 tci_tyvars = all_tvs,
990 tci_given = (eq_givens ++ dict_givens),
991 tci_wanted = irreds, tci_loc = loc }
993 -- only create binder for dict_irreds
995 (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds
996 n_dict_irreds = length dict_irreds
997 dict_irred_ids = map instToId dict_irreds
998 tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
999 pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
1000 rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
1001 co = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
1002 bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs
1003 | otherwise = PatBind { pat_lhs = L span pat,
1004 pat_rhs = unguardedGRHSs rhs,
1005 pat_rhs_ty = tup_ty,
1006 bind_fvs = placeHolderNames }
1007 ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
1008 return ([implic_inst], unitBag (L span bind)) }
1010 -----------------------------------------------------------
1011 tryHardCheckLoop :: SDoc
1013 -> TcM ([Inst], TcDictBinds)
1015 tryHardCheckLoop doc wanteds
1016 = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
1017 ; return (irreds,binds)
1020 try_me inst = ReduceMe AddSCs
1021 -- Here's the try-hard bit
1023 -----------------------------------------------------------
1024 gentleCheckLoop :: InstLoc
1027 -> TcM ([Inst], TcDictBinds)
1029 gentleCheckLoop inst_loc givens wanteds
1030 = do { (irreds,binds,_) <- checkLoop env wanteds
1031 ; return (irreds,binds)
1034 env = mkRedEnv (pprInstLoc inst_loc) try_me givens
1036 try_me inst | isMethodOrLit inst = ReduceMe AddSCs
1038 -- When checking against a given signature
1039 -- we MUST be very gentle: Note [Check gently]
1043 ~~~~~~~~~~~~~~~~~~~~
1044 We have to very careful about not simplifying too vigorously
1049 f :: Show b => T b -> b
1050 f (MkT x) = show [x]
1052 Inside the pattern match, which binds (a:*, x:a), we know that
1054 Hence we have a dictionary for Show [a] available; and indeed we
1055 need it. We are going to build an implication contraint
1056 forall a. (b~[a]) => Show [a]
1057 Later, we will solve this constraint using the knowledg e(Show b)
1059 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
1060 thing becomes insoluble. So we simplify gently (get rid of literals
1061 and methods only, plus common up equal things), deferring the real
1062 work until top level, when we solve the implication constraint
1063 with tryHardCheckLooop.
1067 -----------------------------------------------------------
1070 -> TcM ([Inst], TcDictBinds,
1071 [Inst]) -- needed givens
1072 -- Precondition: givens are completely rigid
1073 -- Postcondition: returned Insts are zonked
1075 checkLoop env wanteds
1077 where go env wanteds needed_givens
1078 = do { -- Givens are skolems, so no need to zonk them
1079 wanteds' <- zonkInsts wanteds
1081 ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
1083 ; let all_needed_givens = needed_givens ++ more_needed_givens
1085 ; if not improved then
1086 return (irreds, binds, all_needed_givens)
1089 -- If improvement did some unification, we go round again.
1090 -- We start again with irreds, not wanteds
1091 -- Using an instance decl might have introduced a fresh type variable
1092 -- which might have been unified, so we'd get an infinite loop
1093 -- if we started again with wanteds! See Note [LOOP]
1094 { (irreds1, binds1, all_needed_givens1) <- go env irreds all_needed_givens
1095 ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
1100 class If b t e r | b t e -> r
1103 class Lte a b c | a b -> c where lte :: a -> b -> c
1105 instance (Lte a b l,If l b a c) => Max a b c
1107 Wanted: Max Z (S x) y
1109 Then we'll reduce using the Max instance to:
1110 (Lte Z (S x) l, If l (S x) Z y)
1111 and improve by binding l->T, after which we can do some reduction
1112 on both the Lte and If constraints. What we *can't* do is start again
1113 with (Max Z (S x) y)!
1117 %************************************************************************
1119 tcSimplifySuperClasses
1121 %************************************************************************
1123 Note [SUPERCLASS-LOOP 1]
1124 ~~~~~~~~~~~~~~~~~~~~~~~~
1125 We have to be very, very careful when generating superclasses, lest we
1126 accidentally build a loop. Here's an example:
1130 class S a => C a where { opc :: a -> a }
1131 class S b => D b where { opd :: b -> b }
1133 instance C Int where
1136 instance D Int where
1139 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1140 Simplifying, we may well get:
1141 $dfCInt = :C ds1 (opd dd)
1144 Notice that we spot that we can extract ds1 from dd.
1146 Alas! Alack! We can do the same for (instance D Int):
1148 $dfDInt = :D ds2 (opc dc)
1152 And now we've defined the superclass in terms of itself.
1154 Solution: never generate a superclass selectors at all when
1155 satisfying the superclass context of an instance declaration.
1157 Two more nasty cases are in
1162 tcSimplifySuperClasses
1167 tcSimplifySuperClasses loc givens sc_wanteds
1168 = do { traceTc (text "tcSimplifySuperClasses")
1169 ; (irreds,binds1,_) <- checkLoop env sc_wanteds
1170 ; let (tidy_env, tidy_irreds) = tidyInsts irreds
1171 ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
1174 env = mkRedEnv (pprInstLoc loc) try_me givens
1175 try_me inst = ReduceMe NoSCs
1176 -- Like tryHardCheckLoop, but with NoSCs
1180 %************************************************************************
1182 \subsection{tcSimplifyRestricted}
1184 %************************************************************************
1186 tcSimplifyRestricted infers which type variables to quantify for a
1187 group of restricted bindings. This isn't trivial.
1190 We want to quantify over a to get id :: forall a. a->a
1193 We do not want to quantify over a, because there's an Eq a
1194 constraint, so we get eq :: a->a->Bool (notice no forall)
1197 RHS has type 'tau', whose free tyvars are tau_tvs
1198 RHS has constraints 'wanteds'
1201 Quantify over (tau_tvs \ ftvs(wanteds))
1202 This is bad. The constraints may contain (Monad (ST s))
1203 where we have instance Monad (ST s) where...
1204 so there's no need to be monomorphic in s!
1206 Also the constraint might be a method constraint,
1207 whose type mentions a perfectly innocent tyvar:
1208 op :: Num a => a -> b -> a
1209 Here, b is unconstrained. A good example would be
1211 We want to infer the polymorphic type
1212 foo :: forall b. b -> b
1215 Plan B (cunning, used for a long time up to and including GHC 6.2)
1216 Step 1: Simplify the constraints as much as possible (to deal
1217 with Plan A's problem). Then set
1218 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1220 Step 2: Now simplify again, treating the constraint as 'free' if
1221 it does not mention qtvs, and trying to reduce it otherwise.
1222 The reasons for this is to maximise sharing.
1224 This fails for a very subtle reason. Suppose that in the Step 2
1225 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
1226 In the Step 1 this constraint might have been simplified, perhaps to
1227 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
1228 This won't happen in Step 2... but that in turn might prevent some other
1229 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
1230 and that in turn breaks the invariant that no constraints are quantified over.
1232 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
1237 Step 1: Simplify the constraints as much as possible (to deal
1238 with Plan A's problem). Then set
1239 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1240 Return the bindings from Step 1.
1243 A note about Plan C (arising from "bug" reported by George Russel March 2004)
1246 instance (HasBinary ty IO) => HasCodedValue ty
1248 foo :: HasCodedValue a => String -> IO a
1250 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1251 doDecodeIO codedValue view
1252 = let { act = foo "foo" } in act
1254 You might think this should work becuase the call to foo gives rise to a constraint
1255 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1256 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1257 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1259 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1263 Plan D (a variant of plan B)
1264 Step 1: Simplify the constraints as much as possible (to deal
1265 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1266 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1268 Step 2: Now simplify again, treating the constraint as 'free' if
1269 it does not mention qtvs, and trying to reduce it otherwise.
1271 The point here is that it's generally OK to have too few qtvs; that is,
1272 to make the thing more monomorphic than it could be. We don't want to
1273 do that in the common cases, but in wierd cases it's ok: the programmer
1274 can always add a signature.
1276 Too few qtvs => too many wanteds, which is what happens if you do less
1281 tcSimplifyRestricted -- Used for restricted binding groups
1282 -- i.e. ones subject to the monomorphism restriction
1285 -> [Name] -- Things bound in this group
1286 -> TcTyVarSet -- Free in the type of the RHSs
1287 -> [Inst] -- Free in the RHSs
1288 -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
1289 TcDictBinds) -- Bindings
1290 -- tcSimpifyRestricted returns no constraints to
1291 -- quantify over; by definition there are none.
1292 -- They are all thrown back in the LIE
1294 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1295 -- Zonk everything in sight
1296 = do { traceTc (text "tcSimplifyRestricted")
1297 ; wanteds' <- zonkInsts wanteds
1299 -- 'ReduceMe': Reduce as far as we can. Don't stop at
1300 -- dicts; the idea is to get rid of as many type
1301 -- variables as possible, and we don't want to stop
1302 -- at (say) Monad (ST s), because that reduces
1303 -- immediately, with no constraint on s.
1305 -- BUT do no improvement! See Plan D above
1306 -- HOWEVER, some unification may take place, if we instantiate
1307 -- a method Inst with an equality constraint
1308 ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
1309 ; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds'
1311 -- Next, figure out the tyvars we will quantify over
1312 ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
1313 ; gbl_tvs' <- tcGetGlobalTyVars
1314 ; constrained_dicts' <- zonkInsts constrained_dicts
1316 ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
1317 -- As in tcSimplifyInfer
1319 -- Do not quantify over constrained type variables:
1320 -- this is the monomorphism restriction
1321 constrained_tvs' = tyVarsOfInsts constrained_dicts'
1322 qtvs = qtvs1 `minusVarSet` constrained_tvs'
1323 pp_bndrs = pprWithCommas (quotes . ppr) bndrs
1326 ; warn_mono <- doptM Opt_WarnMonomorphism
1327 ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
1328 (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
1329 <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
1330 ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
1332 ; traceTc (text "tcSimplifyRestricted" <+> vcat [
1333 pprInsts wanteds, pprInsts constrained_dicts',
1335 ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
1337 -- The first step may have squashed more methods than
1338 -- necessary, so try again, this time more gently, knowing the exact
1339 -- set of type variables to quantify over.
1341 -- We quantify only over constraints that are captured by qtvs;
1342 -- these will just be a subset of non-dicts. This in contrast
1343 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1344 -- all *non-inheritable* constraints too. This implements choice
1345 -- (B) under "implicit parameter and monomorphism" above.
1347 -- Remember that we may need to do *some* simplification, to
1348 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1349 -- just to float all constraints
1351 -- At top level, we *do* squash methods becuase we want to
1352 -- expose implicit parameters to the test that follows
1353 ; let is_nested_group = isNotTopLevel top_lvl
1354 try_me inst | isFreeWrtTyVars qtvs inst,
1355 (is_nested_group || isDict inst) = Stop
1356 | otherwise = ReduceMe AddSCs
1357 env = mkNoImproveRedEnv doc try_me
1358 ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
1360 -- See "Notes on implicit parameters, Question 4: top level"
1361 ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured
1362 if is_nested_group then
1364 else do { let (bad_ips, non_ips) = partition isIPDict irreds
1365 ; addTopIPErrs bndrs bad_ips
1366 ; extendLIEs non_ips }
1368 ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
1369 ; return (qtvs', binds) }
1373 %************************************************************************
1377 %************************************************************************
1379 On the LHS of transformation rules we only simplify methods and constants,
1380 getting dictionaries. We want to keep all of them unsimplified, to serve
1381 as the available stuff for the RHS of the rule.
1383 Example. Consider the following left-hand side of a rule
1385 f (x == y) (y > z) = ...
1387 If we typecheck this expression we get constraints
1389 d1 :: Ord a, d2 :: Eq a
1391 We do NOT want to "simplify" to the LHS
1393 forall x::a, y::a, z::a, d1::Ord a.
1394 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1398 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1399 f ((==) d2 x y) ((>) d1 y z) = ...
1401 Here is another example:
1403 fromIntegral :: (Integral a, Num b) => a -> b
1404 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1406 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1407 we *dont* want to get
1409 forall dIntegralInt.
1410 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1412 because the scsel will mess up RULE matching. Instead we want
1414 forall dIntegralInt, dNumInt.
1415 fromIntegral Int Int dIntegralInt dNumInt = id Int
1419 g (x == y) (y == z) = ..
1421 where the two dictionaries are *identical*, we do NOT WANT
1423 forall x::a, y::a, z::a, d1::Eq a
1424 f ((==) d1 x y) ((>) d1 y z) = ...
1426 because that will only match if the dict args are (visibly) equal.
1427 Instead we want to quantify over the dictionaries separately.
1429 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1430 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1431 from scratch, rather than further parameterise simpleReduceLoop etc
1434 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1435 tcSimplifyRuleLhs wanteds
1436 = go [] emptyBag wanteds
1439 = return (dicts, binds)
1440 go dicts binds (w:ws)
1442 = go (w:dicts) binds ws
1444 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1445 -- to fromInteger; this looks fragile to me
1446 ; lookup_result <- lookupSimpleInst w'
1447 ; case lookup_result of
1448 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
1449 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1453 tcSimplifyBracket is used when simplifying the constraints arising from
1454 a Template Haskell bracket [| ... |]. We want to check that there aren't
1455 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1456 Show instance), but we aren't otherwise interested in the results.
1457 Nor do we care about ambiguous dictionaries etc. We will type check
1458 this bracket again at its usage site.
1461 tcSimplifyBracket :: [Inst] -> TcM ()
1462 tcSimplifyBracket wanteds
1463 = do { tryHardCheckLoop doc wanteds
1466 doc = text "tcSimplifyBracket"
1470 %************************************************************************
1472 \subsection{Filtering at a dynamic binding}
1474 %************************************************************************
1479 we must discharge all the ?x constraints from B. We also do an improvement
1480 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1482 Actually, the constraints from B might improve the types in ?x. For example
1484 f :: (?x::Int) => Char -> Char
1487 then the constraint (?x::Int) arising from the call to f will
1488 force the binding for ?x to be of type Int.
1491 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1494 -- We need a loop so that we do improvement, and then
1495 -- (next time round) generate a binding to connect the two
1497 -- Here the two ?x's have different types, and improvement
1498 -- makes them the same.
1500 tcSimplifyIPs given_ips wanteds
1501 = do { wanteds' <- zonkInsts wanteds
1502 ; given_ips' <- zonkInsts given_ips
1503 -- Unusually for checking, we *must* zonk the given_ips
1505 ; let env = mkRedEnv doc try_me given_ips'
1506 ; (improved, binds, irreds, _) <- reduceContext env wanteds'
1508 ; if not improved then
1509 ASSERT( all is_free irreds )
1510 do { extendLIEs irreds
1513 tcSimplifyIPs given_ips wanteds }
1515 doc = text "tcSimplifyIPs" <+> ppr given_ips
1516 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1517 is_free inst = isFreeWrtIPs ip_set inst
1519 -- Simplify any methods that mention the implicit parameter
1520 try_me inst | is_free inst = Stop
1521 | otherwise = ReduceMe NoSCs
1525 %************************************************************************
1527 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1529 %************************************************************************
1531 When doing a binding group, we may have @Insts@ of local functions.
1532 For example, we might have...
1534 let f x = x + 1 -- orig local function (overloaded)
1535 f.1 = f Int -- two instances of f
1540 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1541 where @f@ is in scope; those @Insts@ must certainly not be passed
1542 upwards towards the top-level. If the @Insts@ were binding-ified up
1543 there, they would have unresolvable references to @f@.
1545 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1546 For each method @Inst@ in the @init_lie@ that mentions one of the
1547 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1548 @LIE@), as well as the @HsBinds@ generated.
1551 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1552 -- Simlifies only MethodInsts, and generate only bindings of form
1554 -- We're careful not to even generate bindings of the form
1556 -- You'd think that'd be fine, but it interacts with what is
1557 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1559 bindInstsOfLocalFuns wanteds local_ids
1560 | null overloaded_ids
1562 = extendLIEs wanteds `thenM_`
1563 returnM emptyLHsBinds
1566 = do { (irreds, binds,_) <- checkLoop env for_me
1567 ; extendLIEs not_for_me
1571 env = mkRedEnv doc try_me []
1572 doc = text "bindInsts" <+> ppr local_ids
1573 overloaded_ids = filter is_overloaded local_ids
1574 is_overloaded id = isOverloadedTy (idType id)
1575 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1577 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1578 -- so it's worth building a set, so that
1579 -- lookup (in isMethodFor) is faster
1580 try_me inst | isMethod inst = ReduceMe NoSCs
1585 %************************************************************************
1587 \subsection{Data types for the reduction mechanism}
1589 %************************************************************************
1591 The main control over context reduction is here
1595 = RedEnv { red_doc :: SDoc -- The context
1596 , red_try_me :: Inst -> WhatToDo
1597 , red_improve :: Bool -- True <=> do improvement
1598 , red_givens :: [Inst] -- All guaranteed rigid
1600 -- but see Note [Rigidity]
1601 , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg)
1602 -- See Note [RedStack]
1606 -- The red_givens are rigid so far as cmpInst is concerned.
1607 -- There is one case where they are not totally rigid, namely in tcSimplifyIPs
1608 -- let ?x = e in ...
1609 -- Here, the given is (?x::a), where 'a' is not necy a rigid type
1610 -- But that doesn't affect the comparison, which is based only on mame.
1613 -- The red_stack pair (n,insts) pair is just used for error reporting.
1614 -- 'n' is always the depth of the stack.
1615 -- The 'insts' is the stack of Insts being reduced: to produce X
1616 -- I had to produce Y, to produce Y I had to produce Z, and so on.
1619 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
1620 mkRedEnv doc try_me givens
1621 = RedEnv { red_doc = doc, red_try_me = try_me,
1622 red_givens = givens, red_stack = (0,[]),
1623 red_improve = True }
1625 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
1626 -- Do not do improvement; no givens
1627 mkNoImproveRedEnv doc try_me
1628 = RedEnv { red_doc = doc, red_try_me = try_me,
1629 red_givens = [], red_stack = (0,[]),
1630 red_improve = True }
1633 = ReduceMe WantSCs -- Try to reduce this
1634 -- If there's no instance, add the inst to the
1635 -- irreductible ones, but don't produce an error
1636 -- message of any kind.
1637 -- It might be quite legitimate such as (Eq a)!
1639 | Stop -- Return as irreducible unless it can
1640 -- be reduced to a constant in one step
1641 -- Do not add superclasses; see
1643 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1644 -- of a predicate when adding it to the avails
1645 -- The reason for this flag is entirely the super-class loop problem
1646 -- Note [SUPER-CLASS LOOP 1]
1649 %************************************************************************
1651 \subsection[reduce]{@reduce@}
1653 %************************************************************************
1657 reduceContext :: RedEnv
1659 -> TcM (ImprovementDone,
1660 TcDictBinds, -- Dictionary bindings
1661 [Inst], -- Irreducible
1662 [Inst]) -- Needed givens
1664 reduceContext env wanteds
1665 = do { traceTc (text "reduceContext" <+> (vcat [
1666 text "----------------------",
1668 text "given" <+> ppr (red_givens env),
1669 text "wanted" <+> ppr wanteds,
1670 text "----------------------"
1674 ; let givens = red_givens env
1675 (given_eqs0,given_dicts0) = partitionGivenEqInsts givens
1676 (wanted_eqs,wanted_dicts) = partitionWantedEqInsts wanteds
1678 ; -- 1. Normalise the *given* *equality* constraints
1679 (given_eqs,eliminate_skolems) <- normaliseGivens given_eqs0
1681 ; -- 2. Normalise the *given* *dictionary* constraints
1682 -- wrt. the toplevel and given equations
1683 (given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0
1685 ; -- 3. Solve the *wanted* *equation* constraints
1686 eq_irreds0 <- solveWanteds given_eqs wanted_eqs
1688 -- 4. Normalise the *wanted* equality constraints with respect to each other
1689 ; eq_irreds <- normaliseWanteds eq_irreds0
1691 -- -- Do the real work
1692 -- -- Process non-implication constraints first, so that they are
1693 -- -- available to help solving the implication constraints
1694 -- -- ToDo: seems a bit inefficient and ad-hoc
1695 -- ; let (implics, rest) = partition isImplicInst wanteds
1696 -- ; avails <- reduceList env (rest ++ implics) init_state
1698 -- 5. Build the Avail mapping from "given_dicts"
1699 ; init_state <- foldlM addGiven emptyAvails given_dicts
1701 -- 6. Solve the *wanted* *dictionary* constraints
1702 -- This may expose some further equational constraints...
1703 ; wanted_dicts' <- zonkInsts wanted_dicts
1704 ; avails <- reduceList env wanted_dicts' init_state
1705 ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
1706 ; traceTc (text "reduceContext extractresults" <+> vcat
1707 [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens])
1709 ; -- 7. Normalise the *wanted* *dictionary* constraints
1710 -- wrt. the toplevel and given equations
1711 (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
1713 ; -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
1714 (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
1716 ; -- 9. eliminate the artificial skolem constants introduced in 1.
1719 -- If there was some FD improvement,
1720 -- or new wanted equations have been exposed,
1721 -- we should have another go at solving.
1722 ; let improved = availsImproved avails
1723 || (not $ isEmptyBag normalise_binds1)
1724 || (not $ isEmptyBag normalise_binds2)
1725 || (not $ null $ fst $ partitionGivenEqInsts irreds)
1727 ; traceTc (text "reduceContext end" <+> (vcat [
1728 text "----------------------",
1730 text "given" <+> ppr (red_givens env),
1731 text "wanted" <+> ppr wanteds,
1733 text "avails" <+> pprAvails avails,
1734 text "improved =" <+> ppr improved,
1735 text "irreds = " <+> ppr irreds,
1736 text "binds = " <+> ppr binds,
1737 text "needed givens = " <+> ppr needed_givens,
1738 text "----------------------"
1741 ; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) }
1743 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
1744 tcImproveOne avails inst
1745 | not (isDict inst) = return False
1747 = do { inst_envs <- tcGetInstEnvs
1748 ; let eqns = improveOne (classInstances inst_envs)
1749 (dictPred inst, pprInstArising inst)
1750 [ (dictPred p, pprInstArising p)
1751 | p <- availsInsts avails, isDict p ]
1752 -- Avails has all the superclasses etc (good)
1753 -- It also has all the intermediates of the deduction (good)
1754 -- It does not have duplicates (good)
1755 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1756 -- so that improve will see them separate
1757 ; traceTc (text "improveOne" <+> ppr inst)
1760 unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
1761 -> TcM ImprovementDone
1762 unifyEqns [] = return False
1764 = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
1768 unify ((qtvs, pairs), what1, what2)
1769 = addErrCtxtM (mkEqnMsg what1 what2) $
1770 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1771 mapM_ (unif_pr tenv) pairs
1772 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1774 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1776 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1777 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1778 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1779 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1780 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1781 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1782 ; return (tidy_env, msg) }
1785 The main context-reduction function is @reduce@. Here's its game plan.
1788 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
1789 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
1790 = do { dopts <- getDOpts
1793 dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n)
1794 2 (ifPprDebug (nest 2 (pprStack stk))))
1797 ; if n >= ctxtStkDepth dopts then
1798 failWithTc (reduceDepthErr n stk)
1802 go [] state = return state
1803 go (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state)
1804 ; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
1807 -- Base case: we're done!
1808 reduce env wanted avails
1809 -- It's the same as an existing inst, or a superclass thereof
1810 | Just avail <- findAvail avails wanted
1811 = do { traceTc (text "reduce: found " <+> ppr wanted)
1816 = do { traceTc (text "reduce" <+> ppr avails <+> ppr wanted)
1817 ; case red_try_me env wanted of {
1818 Stop -> try_simple (addIrred NoSCs);
1819 -- See Note [No superclasses for Stop]
1821 ReduceMe want_scs -> do -- It should be reduced
1822 { (avails, lookup_result) <- reduceInst env avails wanted
1823 ; case lookup_result of
1824 NoInstance -> addIrred want_scs avails wanted
1825 -- Add it and its superclasses
1827 GenInst [] rhs -> addWanted want_scs avails wanted rhs []
1829 GenInst wanteds' rhs
1830 -> do { avails1 <- addIrred NoSCs avails wanted
1831 ; avails2 <- reduceList env wanteds' avails1
1832 ; addWanted want_scs avails2 wanted rhs wanteds' } }
1833 -- Temporarily do addIrred *before* the reduceList,
1834 -- which has the effect of adding the thing we are trying
1835 -- to prove to the database before trying to prove the things it
1836 -- needs. See note [RECURSIVE DICTIONARIES]
1837 -- NB: we must not do an addWanted before, because that adds the
1838 -- superclasses too, and that can lead to a spurious loop; see
1839 -- the examples in [SUPERCLASS-LOOP]
1840 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1843 -- First, see if the inst can be reduced to a constant in one step
1844 -- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
1845 -- Don't bother for implication constraints, which take real work
1846 try_simple do_this_otherwise
1847 = do { res <- lookupSimpleInst wanted
1849 GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
1850 other -> do_this_otherwise avails wanted }
1854 Note [SUPERCLASS-LOOP 2]
1855 ~~~~~~~~~~~~~~~~~~~~~~~~
1856 But the above isn't enough. Suppose we are *given* d1:Ord a,
1857 and want to deduce (d2:C [a]) where
1859 class Ord a => C a where
1860 instance Ord [a] => C [a] where ...
1862 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1863 superclasses of C [a] to avails. But we must not overwrite the binding
1864 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1867 Here's another variant, immortalised in tcrun020
1868 class Monad m => C1 m
1869 class C1 m => C2 m x
1870 instance C2 Maybe Bool
1871 For the instance decl we need to build (C1 Maybe), and it's no good if
1872 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1873 before we search for C1 Maybe.
1875 Here's another example
1876 class Eq b => Foo a b
1877 instance Eq a => Foo [a] a
1881 we'll first deduce that it holds (via the instance decl). We must not
1882 then overwrite the Eq t constraint with a superclass selection!
1884 At first I had a gross hack, whereby I simply did not add superclass constraints
1885 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1886 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1887 I found a very obscure program (now tcrun021) in which improvement meant the
1888 simplifier got two bites a the cherry... so something seemed to be an Stop
1889 first time, but reducible next time.
1891 Now we implement the Right Solution, which is to check for loops directly
1892 when adding superclasses. It's a bit like the occurs check in unification.
1895 Note [RECURSIVE DICTIONARIES]
1896 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1898 data D r = ZeroD | SuccD (r (D r));
1900 instance (Eq (r (D r))) => Eq (D r) where
1901 ZeroD == ZeroD = True
1902 (SuccD a) == (SuccD b) = a == b
1905 equalDC :: D [] -> D [] -> Bool;
1908 We need to prove (Eq (D [])). Here's how we go:
1912 by instance decl, holds if
1916 by instance decl of Eq, holds if
1918 where d2 = dfEqList d3
1921 But now we can "tie the knot" to give
1927 and it'll even run! The trick is to put the thing we are trying to prove
1928 (in this case Eq (D []) into the database before trying to prove its
1929 contributing clauses.
1932 %************************************************************************
1934 Reducing a single constraint
1936 %************************************************************************
1939 ---------------------------------------------
1940 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
1941 reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
1942 tci_given = extra_givens, tci_wanted = wanteds })
1943 = reduceImplication env avails reft tvs extra_givens wanteds loc
1945 reduceInst env avails other_inst
1946 = do { result <- lookupSimpleInst other_inst
1947 ; return (avails, result) }
1950 Note [Equational Constraints in Implication Constraints]
1951 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1953 An equational constraint is of the form
1955 where Given and Wanted may contain both equational and dictionary
1956 constraints. The delay and reduction of these two kinds of constraints
1959 -) In the generated code, wanted Dictionary constraints are wrapped up in an
1960 implication constraint that is created at the code site where the wanted
1961 dictionaries can be reduced via a let-binding. This let-bound implication
1962 constraint is deconstructed at the use-site of the wanted dictionaries.
1964 -) While the reduction of equational constraints is also delayed, the delay
1965 is not manifest in the generated code. The required evidence is generated
1966 in the code directly at the use-site. There is no let-binding and deconstruction
1967 necessary. The main disadvantage is that we cannot exploit sharing as the
1968 same evidence may be generated at multiple use-sites. However, this disadvantage
1969 is limited because it only concerns coercions which are erased.
1971 The different treatment is motivated by the different in representation. Dictionary
1972 constraints require manifest runtime dictionaries, while equations require coercions
1976 ---------------------------------------------
1977 reduceImplication :: RedEnv
1979 -> Refinement -- May refine the givens; often empty
1980 -> [TcTyVar] -- Quantified type variables; all skolems
1981 -> [Inst] -- Extra givens; all rigid
1984 -> TcM (Avails, LookupInstResult)
1987 Suppose we are simplifying the constraint
1988 forall bs. extras => wanted
1989 in the context of an overall simplification problem with givens 'givens',
1990 and refinment 'reft'.
1993 * The refinement is often empty
1995 * The 'extra givens' need not mention any of the quantified type variables
1996 e.g. forall {}. Eq a => Eq [a]
1997 forall {}. C Int => D (Tree Int)
1999 This happens when you have something like
2001 T1 :: Eq a => a -> T a
2004 f x = ...(case x of { T1 v -> v==v })...
2007 -- ToDo: should we instantiate tvs? I think it's not necessary
2009 -- Note on coercion variables:
2011 -- The extra given coercion variables are bound at two different sites:
2012 -- -) in the creation context of the implication constraint
2013 -- the solved equational constraints use these binders
2015 -- -) at the solving site of the implication constraint
2016 -- the solved dictionaries use these binders
2017 -- these binders are generated by reduceImplication
2019 reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
2020 = do { -- Add refined givens, and the extra givens
2022 (refined_red_givens,refined_avails)
2023 <- if isEmptyRefinement reft then return (red_givens env,orig_avails)
2024 else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
2026 -- Solve the sub-problem
2027 ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
2028 env' = env { red_givens = refined_red_givens ++ extra_givens ++ availsInsts orig_avails
2029 , red_try_me = try_me }
2031 ; traceTc (text "reduceImplication" <+> vcat
2033 ppr (red_givens env), ppr extra_givens,
2034 ppr reft, ppr wanteds])
2035 ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
2036 ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_givens]
2038 -- Note [Reducing implication constraints]
2039 -- Tom -- update note, put somewhere!
2041 ; traceTc (text "reduceImplication result" <+> vcat
2042 [ppr irreds, ppr binds, ppr needed_givens1])
2043 -- ; avails <- reduceList env' wanteds avails
2045 -- -- Extract the binding
2046 -- ; (binds, irreds) <- extractResults avails wanteds
2047 ; (refinement_binds,needed_givens) <- extractLocalResults refined_avails needed_givens1
2048 ; traceTc (text "reduceImplication local results" <+> vcat
2049 [ppr refinement_binds, ppr needed_givens])
2051 ; -- extract superclass binds
2052 -- (sc_binds,_) <- extractResults avails []
2053 -- ; traceTc (text "reduceImplication sc_binds" <+> vcat
2054 -- [ppr sc_binds, ppr avails])
2057 -- We always discard the extra avails we've generated;
2058 -- but we remember if we have done any (global) improvement
2059 -- ; let ret_avails = avails
2060 ; let ret_avails = orig_avails
2061 -- ; let ret_avails = updateImprovement orig_avails avails
2063 ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
2065 -- Porgress is no longer measered by the number of bindings
2066 -- ; if isEmptyLHsBinds binds then -- No progress
2067 ; if (isEmptyLHsBinds binds) && (not $ null irreds) then
2068 return (ret_avails, NoInstance)
2071 ; (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
2072 -- This binding is useless if the recursive simplification
2073 -- made no progress; but currently we don't try to optimise that
2074 -- case. After all, we only try hard to reduce at top level, or
2075 -- when inferring types.
2077 ; let dict_wanteds = filter (not . isEqInst) wanteds
2078 (extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens
2079 dict_ids = map instToId extra_dict_givens
2080 -- TOMDO: given equational constraints bug!
2081 -- we need a different evidence for given
2082 -- equations depending on whether we solve
2083 -- dictionary constraints or equational constraints
2084 eq_tyvars = uniqSetToList $ tyVarsOfTypes $ map eqInstType extra_eq_givens
2085 -- dict_ids = map instToId extra_givens
2086 co = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` refinement_binds `unionBags` bind)
2087 rhs = mkHsWrap co payload
2088 loc = instLocSpan inst_loc
2089 payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
2090 | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
2093 ; traceTc (text "reduceImplication ->" <+> vcat
2096 -- If there are any irreds, we back off and return NoInstance
2097 ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
2102 Note [Reducing implication constraints]
2103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2104 Suppose we are trying to simplify
2105 (Ord a, forall b. C a b => (W [a] b, D c b))
2107 instance (C a b, Ord a) => W [a] b
2108 When solving the implication constraint, we'll start with
2110 in the Avails. Then we add (C a b -> Given) and solve. Extracting
2111 the results gives us a binding for the (W [a] b), with an Irred of
2112 (Ord a, D c b). Now, the (Ord a) comes from "outside" the implication,
2113 but the (D d b) is from "inside". So we want to generate a Rhs binding
2116 ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
2119 ic' :: forall b. C a b => D c b
2121 The 'depending on' part of the Rhs is important, because it drives
2122 the extractResults code.
2124 The "inside" and "outside" distinction is what's going on with 'inner' and
2125 'outer' in reduceImplication
2128 Note [Freeness and implications]
2129 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2130 It's hard to say when an implication constraint can be floated out. Consider
2131 forall {} Eq a => Foo [a]
2132 The (Foo [a]) doesn't mention any of the quantified variables, but it
2133 still might be partially satisfied by the (Eq a).
2135 There is a useful special case when it *is* easy to partition the
2136 constraints, namely when there are no 'givens'. Consider
2137 forall {a}. () => Bar b
2138 There are no 'givens', and so there is no reason to capture (Bar b).
2139 We can let it float out. But if there is even one constraint we
2140 must be much more careful:
2141 forall {a}. C a b => Bar (m b)
2142 because (C a b) might have a superclass (D b), from which we might
2143 deduce (Bar [b]) when m later gets instantiated to []. Ha!
2145 Here is an even more exotic example
2147 Now consider the constraint
2148 forall b. D Int b => C Int
2149 We can satisfy the (C Int) from the superclass of D, so we don't want
2150 to float the (C Int) out, even though it mentions no type variable in
2153 Note [Pruning the givens in an implication constraint]
2154 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2155 Suppose we are about to form the implication constraint
2156 forall tvs. Eq a => Ord b
2157 The (Eq a) cannot contribute to the (Ord b), because it has no access to
2158 the type variable 'b'. So we could filter out the (Eq a) from the givens.
2160 Doing so would be a bit tidier, but all the implication constraints get
2161 simplified away by the optimiser, so it's no great win. So I don't take
2162 advantage of that at the moment.
2164 If you do, BE CAREFUL of wobbly type variables.
2167 %************************************************************************
2169 Avails and AvailHow: the pool of evidence
2171 %************************************************************************
2175 data Avails = Avails !ImprovementDone !AvailEnv
2177 type ImprovementDone = Bool -- True <=> some unification has happened
2178 -- so some Irreds might now be reducible
2179 -- keys that are now
2181 type AvailEnv = FiniteMap Inst AvailHow
2183 = IsIrred -- Used for irreducible dictionaries,
2184 -- which are going to be lambda bound
2186 | Given TcId -- Used for dictionaries for which we have a binding
2187 -- e.g. those "given" in a signature
2189 | Rhs -- Used when there is a RHS
2190 (LHsExpr TcId) -- The RHS
2191 [Inst] -- Insts free in the RHS; we need these too
2193 instance Outputable Avails where
2196 pprAvails (Avails imp avails)
2197 = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
2198 , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
2199 | (inst,avail) <- fmToList avails ])]
2201 instance Outputable AvailHow where
2204 -------------------------
2205 pprAvail :: AvailHow -> SDoc
2206 pprAvail IsIrred = text "Irred"
2207 pprAvail (Given x) = text "Given" <+> ppr x
2208 pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
2210 -------------------------
2211 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
2212 extendAvailEnv env inst avail = addToFM env inst avail
2214 findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
2215 findAvailEnv env wanted = lookupFM env wanted
2216 -- NB 1: the Ord instance of Inst compares by the class/type info
2217 -- *not* by unique. So
2218 -- d1::C Int == d2::C Int
2220 emptyAvails :: Avails
2221 emptyAvails = Avails False emptyFM
2223 findAvail :: Avails -> Inst -> Maybe AvailHow
2224 findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
2226 elemAvails :: Inst -> Avails -> Bool
2227 elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
2229 extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
2231 extendAvails avails@(Avails imp env) inst avail
2232 = do { imp1 <- tcImproveOne avails inst -- Do any improvement
2233 ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
2235 availsInsts :: Avails -> [Inst]
2236 availsInsts (Avails _ avails) = keysFM avails
2238 availsImproved (Avails imp _) = imp
2240 updateImprovement :: Avails -> Avails -> Avails
2241 -- (updateImprovement a1 a2) sets a1's improvement flag from a2
2242 updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
2245 Extracting the bindings from a bunch of Avails.
2246 The bindings do *not* come back sorted in dependency order.
2247 We assume that they'll be wrapped in a big Rec, so that the
2248 dependency analyser can sort them out later
2251 extractResults :: Avails
2253 -> TcM ( TcDictBinds, -- Bindings
2254 [Inst], -- Irreducible ones
2255 [Inst]) -- Needed givens, i.e. ones used in the bindings
2257 extractResults (Avails _ avails) wanteds
2258 = go avails emptyBag [] [] wanteds
2260 go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
2261 -> TcM (TcDictBinds, [Inst], [Inst])
2262 go avails binds irreds givens []
2263 = returnM (binds, irreds, givens)
2265 go avails binds irreds givens (w:ws)
2266 = case findAvailEnv avails w of
2267 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
2268 go avails binds irreds givens ws
2271 | id == w_id -> go avails binds irreds (w:givens) ws
2272 | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w id:givens) ws
2273 -- The sought Id can be one of the givens, via a superclass chain
2274 -- and then we definitely don't want to generate an x=x binding!
2276 Just IsIrred -> go (add_given avails w) binds (w:irreds) givens ws
2277 -- The add_given handles the case where we want (Ord a, Eq a), and we
2278 -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
2279 -- This showed up in a dupliated Ord constraint in the error message for
2282 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
2284 new_binds = addBind binds w rhs
2287 update_id m@(Method{}) id = m {tci_id = id}
2288 update_id w id = w {tci_name = idName id}
2290 add_given avails w = extendAvailEnv avails w (Given (instToId w))
2292 extractLocalResults :: Avails
2294 -> TcM ( TcDictBinds, -- Bindings
2295 [Inst]) -- Needed givens, i.e. ones used in the bindings
2297 extractLocalResults (Avails _ avails) wanteds
2298 = go avails emptyBag [] wanteds
2300 go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
2301 -> TcM (TcDictBinds, [Inst])
2302 go avails binds givens []
2303 = returnM (binds, givens)
2305 go avails binds givens (w:ws)
2306 = case findAvailEnv avails w of
2307 Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
2308 go avails binds givens ws
2311 go avails binds givens ws
2314 | id == w_id -> go avails binds (w:givens) ws
2315 | otherwise -> go avails binds (w{tci_name=idName id}:givens) ws
2316 -- The sought Id can be one of the givens, via a superclass chain
2317 -- and then we definitely don't want to generate an x=x binding!
2319 Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
2321 new_binds = addBind binds w rhs
2325 add_given avails w = extendAvailEnv avails w (Given (instToId w))
2329 Note [No superclasses for Stop]
2330 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2331 When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
2332 add it to avails, so that any other equal Insts will be commoned up
2333 right here. However, we do *not* add superclasses. If we have
2336 but a is not bound here, then we *don't* want to derive dn from df
2337 here lest we lose sharing.
2340 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
2341 addWanted want_scs avails wanted rhs_expr wanteds
2342 = addAvailAndSCs want_scs avails wanted avail
2344 avail = Rhs rhs_expr wanteds
2346 addGiven :: Avails -> Inst -> TcM Avails
2347 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
2348 -- Always add superclasses for 'givens'
2350 -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
2351 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
2352 -- so the assert isn't true
2354 addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
2355 addRefinedGiven reft (refined_givens, avails) given
2356 | isDict given -- We sometimes have 'given' methods, but they
2357 -- are always optional, so we can drop them
2358 , let pred = dictPred given
2359 , isRefineablePred pred -- See Note [ImplicInst rigidity]
2360 , Just (co, pred) <- refinePred reft pred
2361 = do { new_given <- newDictBndr (instLoc given) pred
2362 ; let rhs = L (instSpan given) $
2363 HsWrap (WpCo co) (HsVar (instToId given))
2364 ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
2365 ; return (new_given:refined_givens, avails) }
2366 -- ToDo: the superclasses of the original given all exist in Avails
2367 -- so we could really just cast them, but it's more awkward to do,
2368 -- and hopefully the optimiser will spot the duplicated work
2370 = return (refined_givens, avails)
2372 addRefinedGiven' :: Refinement -> [Inst] -> Inst -> TcM [Inst]
2373 addRefinedGiven' reft refined_givens given
2374 | isDict given -- We sometimes have 'given' methods, but they
2375 -- are always optional, so we can drop them
2376 , let pred = dictPred given
2377 , isRefineablePred pred -- See Note [ImplicInst rigidity]
2378 , Just (co, pred) <- refinePred reft pred
2379 = do { new_given <- newDictBndr (instLoc given) pred
2380 ; return (new_given:refined_givens) }
2381 -- ToDo: the superclasses of the original given all exist in Avails
2382 -- so we could really just cast them, but it's more awkward to do,
2383 -- and hopefully the optimiser will spot the duplicated work
2385 = return refined_givens
2388 Note [ImplicInst rigidity]
2389 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2391 C :: forall ab. (Eq a, Ord b) => b -> T a
2393 ...(case x of C v -> <body>)...
2395 From the case (where x::T ty) we'll get an implication constraint
2396 forall b. (Eq ty, Ord b) => <body-constraints>
2397 Now suppose <body-constraints> itself has an implication constraint
2399 forall c. <reft> => <payload>
2400 Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
2401 existential, but we probably should not apply it to the (Eq ty) because it may
2402 be wobbly. Hence the isRigidInst
2404 @Insts@ are ordered by their class/type info, rather than by their
2405 unique. This allows the context-reduction mechanism to use standard finite
2406 maps to do their stuff. It's horrible that this code is here, rather
2407 than with the Avails handling stuff in TcSimplify
2410 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
2411 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
2412 addAvailAndSCs want_scs avails irred IsIrred
2414 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
2415 addAvailAndSCs want_scs avails inst avail
2416 | not (isClassDict inst) = extendAvails avails inst avail
2417 | NoSCs <- want_scs = extendAvails avails inst avail
2418 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
2419 ; avails' <- extendAvails avails inst avail
2420 ; addSCs is_loop avails' inst }
2422 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
2423 -- Note: this compares by *type*, not by Unique
2424 deps = findAllDeps (unitVarSet (instToId inst)) avail
2425 dep_tys = map idType (varSetElems deps)
2427 findAllDeps :: IdSet -> AvailHow -> IdSet
2428 -- Find all the Insts that this one depends on
2429 -- See Note [SUPERCLASS-LOOP 2]
2430 -- Watch out, though. Since the avails may contain loops
2431 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
2432 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
2433 findAllDeps so_far other = so_far
2435 find_all :: IdSet -> Inst -> IdSet
2437 | kid_id `elemVarSet` so_far = so_far
2438 | Just avail <- findAvail avails kid = findAllDeps so_far' avail
2439 | otherwise = so_far'
2441 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
2442 kid_id = instToId kid
2444 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
2445 -- Add all the superclasses of the Inst to Avails
2446 -- The first param says "dont do this because the original thing
2447 -- depends on this one, so you'd build a loop"
2448 -- Invariant: the Inst is already in Avails.
2450 addSCs is_loop avails dict
2451 = ASSERT( isDict dict )
2452 do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
2453 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
2455 (clas, tys) = getDictClassTys dict
2456 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
2457 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
2459 add_sc avails (sc_dict, sc_sel)
2460 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
2461 | is_given sc_dict = return avails
2462 | otherwise = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
2463 ; addSCs is_loop avails' sc_dict }
2465 sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
2466 co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
2468 is_given :: Inst -> Bool
2469 is_given sc_dict = case findAvail avails sc_dict of
2470 Just (Given _) -> True -- Given is cheaper than superclass selection
2474 %************************************************************************
2476 \section{tcSimplifyTop: defaulting}
2478 %************************************************************************
2481 @tcSimplifyTop@ is called once per module to simplify all the constant
2482 and ambiguous Insts.
2484 We need to be careful of one case. Suppose we have
2486 instance Num a => Num (Foo a b) where ...
2488 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2489 to (Num x), and default x to Int. But what about y??
2491 It's OK: the final zonking stage should zap y to (), which is fine.
2495 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2496 tcSimplifyTop wanteds
2497 = tc_simplify_top doc False wanteds
2499 doc = text "tcSimplifyTop"
2501 tcSimplifyInteractive wanteds
2502 = tc_simplify_top doc True wanteds
2504 doc = text "tcSimplifyInteractive"
2506 -- The TcLclEnv should be valid here, solely to improve
2507 -- error message generation for the monomorphism restriction
2508 tc_simplify_top doc interactive wanteds
2509 = do { dflags <- getDOpts
2510 ; wanteds <- zonkInsts wanteds
2511 ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
2513 ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
2514 ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
2515 ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
2516 ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
2517 ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
2519 -- Use the defaulting rules to do extra unification
2520 -- NB: irreds2 are already zonked
2521 ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
2523 -- Deal with implicit parameters
2524 ; let (bad_ips, non_ips) = partition isIPDict irreds3
2525 (ambigs, others) = partition isTyVarDict non_ips
2527 ; topIPErrs bad_ips -- Can arise from f :: Int -> Int
2529 ; addNoInstanceErrs others
2530 ; addTopAmbigErrs ambigs
2532 ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
2534 doc1 = doc <+> ptext SLIT("(first round)")
2535 doc2 = doc <+> ptext SLIT("(approximate)")
2536 doc3 = doc <+> ptext SLIT("(disambiguate)")
2539 If a dictionary constrains a type variable which is
2540 * not mentioned in the environment
2541 * and not mentioned in the type of the expression
2542 then it is ambiguous. No further information will arise to instantiate
2543 the type variable; nor will it be generalised and turned into an extra
2544 parameter to a function.
2546 It is an error for this to occur, except that Haskell provided for
2547 certain rules to be applied in the special case of numeric types.
2549 * at least one of its classes is a numeric class, and
2550 * all of its classes are numeric or standard
2551 then the type variable can be defaulted to the first type in the
2552 default-type list which is an instance of all the offending classes.
2554 So here is the function which does the work. It takes the ambiguous
2555 dictionaries and either resolves them (producing bindings) or
2556 complains. It works by splitting the dictionary list by type
2557 variable, and using @disambigOne@ to do the real business.
2559 @disambigOne@ assumes that its arguments dictionaries constrain all
2560 the same type variable.
2562 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2563 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2564 the most common use of defaulting is code like:
2566 _ccall_ foo `seqPrimIO` bar
2568 Since we're not using the result of @foo@, the result if (presumably)
2572 disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
2573 -- Just does unification to fix the default types
2574 -- The Insts are assumed to be pre-zonked
2575 disambiguate doc interactive dflags insts
2577 = return (insts, emptyBag)
2579 | null defaultable_groups
2580 = do { traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
2581 ; return (insts, emptyBag) }
2584 = do { -- Figure out what default types to use
2585 default_tys <- getDefaultTys extended_defaulting ovl_strings
2587 ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
2588 ; mapM_ (disambigGroup default_tys) defaultable_groups
2590 -- disambigGroup does unification, hence try again
2591 ; tryHardCheckLoop doc insts }
2594 extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
2595 ovl_strings = dopt Opt_OverloadedStrings dflags
2597 unaries :: [(Inst, Class, TcTyVar)] -- (C tv) constraints
2598 bad_tvs :: TcTyVarSet -- Tyvars mentioned by *other* constraints
2599 (unaries, bad_tvs_s) = partitionWith find_unary insts
2600 bad_tvs = unionVarSets bad_tvs_s
2602 -- Finds unary type-class constraints
2603 find_unary d@(Dict {tci_pred = ClassP cls [ty]})
2604 | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
2605 find_unary inst = Right (tyVarsOfInst inst)
2607 -- Group by type variable
2608 defaultable_groups :: [[(Inst,Class,TcTyVar)]]
2609 defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
2610 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
2612 defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
2613 defaultable_group ds@((_,_,tv):_)
2614 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
2615 && not (tv `elemVarSet` bad_tvs)
2616 && defaultable_classes [c | (_,c,_) <- ds]
2617 defaultable_group [] = panic "defaultable_group"
2619 defaultable_classes clss
2620 | extended_defaulting = any isInteractiveClass clss
2621 | otherwise = all is_std_class clss && (any is_num_class clss)
2623 -- In interactive mode, or with -fextended-default-rules,
2624 -- we default Show a to Show () to avoid graututious errors on "show []"
2625 isInteractiveClass cls
2626 = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2628 is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2629 -- is_num_class adds IsString to the standard numeric classes,
2630 -- when -foverloaded-strings is enabled
2632 is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2633 -- Similarly is_std_class
2635 -----------------------
2636 disambigGroup :: [Type] -- The default types
2637 -> [(Inst,Class,TcTyVar)] -- All standard classes of form (C a)
2638 -> TcM () -- Just does unification, to fix the default types
2640 disambigGroup default_tys dicts
2641 = try_default default_tys
2643 (_,_,tyvar) = ASSERT(not (null dicts)) head dicts -- Should be non-empty
2644 classes = [c | (_,c,_) <- dicts]
2646 try_default [] = return ()
2647 try_default (default_ty : default_tys)
2648 = tryTcLIE_ (try_default default_tys) $
2649 do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
2650 -- This may fail; then the tryTcLIE_ kicks in
2651 -- Failure here is caused by there being no type in the
2652 -- default list which can satisfy all the ambiguous classes.
2653 -- For example, if Real a is reqd, but the only type in the
2654 -- default list is Int.
2656 -- After this we can't fail
2657 ; warnDefault dicts default_ty
2658 ; unifyType default_ty (mkTyVarTy tyvar)
2659 ; return () -- TOMDO: do something with the coercion
2663 -----------------------
2664 getDefaultTys :: Bool -> Bool -> TcM [Type]
2665 getDefaultTys extended_deflts ovl_strings
2666 = do { mb_defaults <- getDeclaredDefaultTys
2667 ; case mb_defaults of {
2668 Just tys -> return tys ; -- User-supplied defaults
2671 -- No use-supplied default
2672 -- Use [Integer, Double], plus modifications
2673 { integer_ty <- tcMetaTy integerTyConName
2674 ; checkWiredInTyCon doubleTyCon
2675 ; string_ty <- tcMetaTy stringTyConName
2676 ; return (opt_deflt extended_deflts unitTy
2677 -- Note [Default unitTy]
2679 [integer_ty,doubleTy]
2681 opt_deflt ovl_strings string_ty) } } }
2683 opt_deflt True ty = [ty]
2684 opt_deflt False ty = []
2687 Note [Default unitTy]
2688 ~~~~~~~~~~~~~~~~~~~~~
2689 In interative mode (or with -fextended-default-rules) we add () as the first type we
2690 try when defaulting. This has very little real impact, except in the following case.
2692 Text.Printf.printf "hello"
2693 This has type (forall a. IO a); it prints "hello", and returns 'undefined'. We don't
2694 want the GHCi repl loop to try to print that 'undefined'. The neatest thing is to
2695 default the 'a' to (), rather than to Integer (which is what would otherwise happen;
2696 and then GHCi doesn't attempt to print the (). So in interactive mode, we add
2697 () to the list of defaulting types. See Trac #1200.
2699 Note [Avoiding spurious errors]
2700 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2701 When doing the unification for defaulting, we check for skolem
2702 type variables, and simply don't default them. For example:
2703 f = (*) -- Monomorphic
2704 g :: Num a => a -> a
2706 Here, we get a complaint when checking the type signature for g,
2707 that g isn't polymorphic enough; but then we get another one when
2708 dealing with the (Num a) context arising from f's definition;
2709 we try to unify a with Int (to default it), but find that it's
2710 already been unified with the rigid variable from g's type sig
2713 %************************************************************************
2715 \subsection[simple]{@Simple@ versions}
2717 %************************************************************************
2719 Much simpler versions when there are no bindings to make!
2721 @tcSimplifyThetas@ simplifies class-type constraints formed by
2722 @deriving@ declarations and when specialising instances. We are
2723 only interested in the simplified bunch of class/type constraints.
2725 It simplifies to constraints of the form (C a b c) where
2726 a,b,c are type variables. This is required for the context of
2727 instance declarations.
2730 tcSimplifyDeriv :: InstOrigin
2732 -> ThetaType -- Wanted
2733 -> TcM ThetaType -- Needed
2734 -- Given instance (wanted) => C inst_ty
2735 -- Simplify 'wanted' as much as possible
2736 -- The inst_ty is needed only for the termination check
2738 tcSimplifyDeriv orig tyvars theta
2739 = do { (tvs, _, tenv) <- tcInstTyVars tyvars
2740 -- The main loop may do unification, and that may crash if
2741 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2742 -- ToDo: what if two of them do get unified?
2743 ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
2744 ; (irreds, _) <- tryHardCheckLoop doc wanteds
2746 ; let (tv_dicts, others) = partition isTyVarDict irreds
2747 ; addNoInstanceErrs others
2749 ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2750 simpl_theta = substTheta rev_env (map dictPred tv_dicts)
2751 -- This reverse-mapping is a pain, but the result
2752 -- should mention the original TyVars not TcTyVars
2754 ; return simpl_theta }
2756 doc = ptext SLIT("deriving classes for a data type")
2759 Note [Exotic derived instance contexts]
2760 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2762 data T a b c = MkT (Foo a b c) deriving( Eq )
2763 instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
2765 Notice that this instance (just) satisfies the Paterson termination
2766 conditions. Then we *could* derive an instance decl like this:
2768 instance (C Int a, Eq b, Eq c) => Eq (T a b c)
2770 even though there is no instance for (C Int a), because there just
2771 *might* be an instance for, say, (C Int Bool) at a site where we
2772 need the equality instance for T's.
2774 However, this seems pretty exotic, and it's quite tricky to allow
2775 this, and yet give sensible error messages in the (much more common)
2776 case where we really want that instance decl for C.
2778 So for now we simply require that the derived instance context
2779 should have only type-variable constraints.
2781 Here is another example:
2782 data Fix f = In (f (Fix f)) deriving( Eq )
2783 Here, if we are prepared to allow -fallow-undecidable-instances we
2784 could derive the instance
2785 instance Eq (f (Fix f)) => Eq (Fix f)
2786 but this is so delicate that I don't think it should happen inside
2787 'deriving'. If you want this, write it yourself!
2789 NB: if you want to lift this condition, make sure you still meet the
2790 termination conditions! If not, the deriving mechanism generates
2791 larger and larger constraints. Example:
2793 data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
2795 Note the lack of a Show instance for Succ. First we'll generate
2796 instance (Show (Succ a), Show a) => Show (Seq a)
2798 instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
2799 and so on. Instead we want to complain of no instance for (Show (Succ a)).
2802 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2803 used with \tr{default} declarations. We are only interested in
2804 whether it worked or not.
2807 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2810 tcSimplifyDefault theta
2811 = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
2812 tryHardCheckLoop doc wanteds `thenM` \ (irreds, _) ->
2813 addNoInstanceErrs irreds `thenM_`
2819 doc = ptext SLIT("default declaration")
2823 %************************************************************************
2825 \section{Errors and contexts}
2827 %************************************************************************
2829 ToDo: for these error messages, should we note the location as coming
2830 from the insts, or just whatever seems to be around in the monad just
2834 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2835 -> [Inst] -- The offending Insts
2837 -- Group together insts with the same origin
2838 -- We want to report them together in error messages
2840 groupErrs report_err []
2842 groupErrs report_err (inst:insts)
2843 = do_one (inst:friends) `thenM_`
2844 groupErrs report_err others
2847 -- (It may seem a bit crude to compare the error messages,
2848 -- but it makes sure that we combine just what the user sees,
2849 -- and it avoids need equality on InstLocs.)
2850 (friends, others) = partition is_friend insts
2851 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2852 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2853 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2854 -- Add location and context information derived from the Insts
2856 -- Add the "arising from..." part to a message about bunch of dicts
2857 addInstLoc :: [Inst] -> Message -> Message
2858 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
2860 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2861 addTopIPErrs bndrs []
2863 addTopIPErrs bndrs ips
2864 = do { dflags <- getDOpts
2865 ; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
2867 (tidy_env, tidy_ips) = tidyInsts ips
2869 = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2870 nest 2 (ptext SLIT("the monomorphic top-level binding")
2871 <> plural bndrs <+> ptext SLIT("of")
2872 <+> pprBinders bndrs <> colon)],
2873 nest 2 (vcat (map ppr_ip ips)),
2874 monomorphism_fix dflags]
2875 ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
2877 topIPErrs :: [Inst] -> TcM ()
2879 = groupErrs report tidy_dicts
2881 (tidy_env, tidy_dicts) = tidyInsts dicts
2882 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2883 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2884 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2886 addNoInstanceErrs :: [Inst] -- Wanted (can include implications)
2888 addNoInstanceErrs insts
2889 = do { let (tidy_env, tidy_insts) = tidyInsts insts
2890 ; reportNoInstances tidy_env Nothing tidy_insts }
2894 -> Maybe (InstLoc, [Inst]) -- Context
2895 -- Nothing => top level
2896 -- Just (d,g) => d describes the construct
2898 -> [Inst] -- What is wanted (can include implications)
2901 reportNoInstances tidy_env mb_what insts
2902 = groupErrs (report_no_instances tidy_env mb_what) insts
2904 report_no_instances tidy_env mb_what insts
2905 = do { inst_envs <- tcGetInstEnvs
2906 ; let (implics, insts1) = partition isImplicInst insts
2907 (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
2908 (eqInsts, insts3) = partition isEqInst insts2
2909 ; traceTc (text "reportNoInstances" <+> vcat
2910 [ppr implics, ppr insts1, ppr insts2])
2911 ; mapM_ complain_implic implics
2912 ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
2913 ; groupErrs complain_no_inst insts3
2914 ; mapM_ complain_eq eqInsts
2917 complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
2919 complain_implic inst -- Recurse!
2920 = reportNoInstances tidy_env
2921 (Just (tci_loc inst, tci_given inst))
2924 complain_eq EqInst {tci_left = lty, tci_right = rty,
2925 tci_loc = InstLoc _ _ ctxt}
2926 = do { (env, msg) <- misMatchMsg lty rty
2928 failWithTcM (env, msg)
2931 check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
2932 -- Right msg => overlap message
2933 -- Left inst => no instance
2934 check_overlap inst_envs wanted
2935 | not (isClassDict wanted) = Left wanted
2937 = case lookupInstEnv inst_envs clas tys of
2938 -- The case of exactly one match and no unifiers means a
2939 -- successful lookup. That can't happen here, because dicts
2940 -- only end up here if they didn't match in Inst.lookupInst
2942 ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
2944 ([], _) -> Left wanted -- No match
2945 res -> Right (mk_overlap_msg wanted res)
2947 (clas,tys) = getDictClassTys wanted
2949 mk_overlap_msg dict (matches, unifiers)
2950 = ASSERT( not (null matches) )
2951 vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2952 <+> pprPred (dictPred dict))),
2953 sep [ptext SLIT("Matching instances") <> colon,
2954 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2955 if not (isSingleton matches)
2956 then -- Two or more matches
2958 else -- One match, plus some unifiers
2959 ASSERT( not (null unifiers) )
2960 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2961 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2962 ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
2963 ptext SLIT("when compiling the other instance declarations")])]
2965 ispecs = [ispec | (ispec, _) <- matches]
2967 mk_no_inst_err insts
2968 | null insts = empty
2970 | Just (loc, givens) <- mb_what, -- Nested (type signatures, instance decls)
2971 not (isEmptyVarSet (tyVarsOfInsts insts))
2972 = vcat [ addInstLoc insts $
2973 sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts
2974 , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens]
2975 , show_fixes (fix1 loc : fixes2) ]
2977 | otherwise -- Top level
2978 = vcat [ addInstLoc insts $
2979 ptext SLIT("No instance") <> plural insts
2980 <+> ptext SLIT("for") <+> pprDictsTheta insts
2981 , show_fixes fixes2 ]
2984 fix1 loc = sep [ ptext SLIT("add") <+> pprDictsTheta insts
2985 <+> ptext SLIT("to the context of"),
2986 nest 2 (ppr (instLocOrigin loc)) ]
2987 -- I'm not sure it helps to add the location
2988 -- nest 2 (ptext SLIT("at") <+> ppr (instLocSpan loc)) ]
2990 fixes2 | null instance_dicts = []
2991 | otherwise = [sep [ptext SLIT("add an instance declaration for"),
2992 pprDictsTheta instance_dicts]]
2993 instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
2994 -- Insts for which it is worth suggesting an adding an instance declaration
2995 -- Exclude implicit parameters, and tyvar dicts
2997 show_fixes :: [SDoc] -> SDoc
2998 show_fixes [] = empty
2999 show_fixes (f:fs) = sep [ptext SLIT("Possible fix:"),
3000 nest 2 (vcat (f : map (ptext SLIT("or") <+>) fs))]
3002 addTopAmbigErrs dicts
3003 -- Divide into groups that share a common set of ambiguous tyvars
3004 = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened
3005 -- See Note [Avoiding spurious errors]
3006 mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
3008 (tidy_env, tidy_dicts) = tidyInsts dicts
3010 tvs_of :: Inst -> [TcTyVar]
3011 tvs_of d = varSetElems (tyVarsOfInst d)
3012 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
3014 report :: [(Inst,[TcTyVar])] -> TcM ()
3015 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
3016 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
3017 setSrcSpan (instSpan inst) $
3018 -- the location of the first one will do for the err message
3019 addErrTcM (tidy_env, msg $$ mono_msg)
3021 dicts = map fst pairs
3022 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
3023 pprQuotedList tvs <+> in_msg,
3024 nest 2 (pprDictsInFull dicts)]
3025 in_msg = text "in the constraint" <> plural dicts <> colon
3026 report [] = panic "addTopAmbigErrs"
3029 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
3030 -- There's an error with these Insts; if they have free type variables
3031 -- it's probably caused by the monomorphism restriction.
3032 -- Try to identify the offending variable
3033 -- ASSUMPTION: the Insts are fully zonked
3034 mkMonomorphismMsg tidy_env inst_tvs
3035 = do { dflags <- getDOpts
3036 ; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
3037 ; return (tidy_env, mk_msg dflags docs) }
3039 mk_msg _ _ | any isRuntimeUnk inst_tvs
3040 = vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
3041 (pprWithCommas ppr inst_tvs),
3042 ptext SLIT("Use :print or :force to determine these types")]
3043 mk_msg _ [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
3044 -- This happens in things like
3045 -- f x = show (read "foo")
3046 -- where monomorphism doesn't play any role
3048 = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
3050 monomorphism_fix dflags]
3052 isRuntimeUnk :: TcTyVar -> Bool
3053 isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
3056 monomorphism_fix :: DynFlags -> SDoc
3057 monomorphism_fix dflags
3058 = ptext SLIT("Probable fix:") <+> vcat
3059 [ptext SLIT("give these definition(s) an explicit type signature"),
3060 if dopt Opt_MonomorphismRestriction dflags
3061 then ptext SLIT("or use -fno-monomorphism-restriction")
3062 else empty] -- Only suggest adding "-fno-monomorphism-restriction"
3063 -- if it is not already set!
3065 warnDefault ups default_ty
3066 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
3067 addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
3069 dicts = [d | (d,_,_) <- ups]
3072 (_, tidy_dicts) = tidyInsts dicts
3073 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
3074 quotes (ppr default_ty),
3075 pprDictsInFull tidy_dicts]
3077 reduceDepthErr n stack
3078 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
3079 ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
3080 nest 4 (pprStack stack)]
3082 pprStack stack = vcat (map pprInstInFull stack)
3084 -----------------------
3085 misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
3086 -- Generate the message when two types fail to match,
3087 -- going to some trouble to make it helpful.
3088 -- The argument order is: actual type, expected type
3089 misMatchMsg ty_act ty_exp
3090 = do { env0 <- tcInitTidyEnv
3091 ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp ty_act
3092 ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ty_exp
3094 sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
3096 ptext SLIT("against inferred type") <+> pp_act],
3097 nest 2 (extra_exp $$ extra_act)]) }
3099 ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc)
3100 ppr_ty env ty other_ty
3101 = do { ty' <- zonkTcType ty
3102 ; let (env1, tidy_ty) = tidyOpenType env ty'
3103 ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty
3104 ; return (env2, quotes (ppr tidy_ty), extra) }
3106 -- (ppr_extra env ty other_ty) shows extra info about 'ty'
3107 ppr_extra env (TyVarTy tv) other_ty
3108 | isSkolemTyVar tv || isSigTyVar tv
3109 = return (env1, pprSkolTvBinding tv1)
3111 (env1, tv1) = tidySkolemTyVar env tv
3113 ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _)
3114 | getOccName tc1 == getOccName tc2
3115 = -- This case helps with messages that would otherwise say
3116 -- Could not match 'T' does not match 'M.T'
3117 -- which is not helpful
3118 do { this_mod <- getModule
3119 ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) }
3121 tc_mod = nameModule (getName tc1)
3122 tc_pkg = modulePackageId tc_mod
3123 tc2_pkg = modulePackageId (nameModule (getName tc2))
3125 | tc_mod == this_mod = ptext SLIT("in this module")
3127 | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg
3128 -- Suppress the module name if (a) it's from another package
3129 -- (b) other_ty isn't from that same package
3131 | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg
3133 home_pkg = tc_pkg == modulePackageId this_mod
3134 pp_pkg | home_pkg = empty
3135 | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg)
3137 ppr_extra env ty other_ty = return (env, empty) -- Normal case