2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs,
13 tcSimplifyTop, tcSimplifyInteractive,
16 tcSimplifyDeriv, tcSimplifyDefault,
20 #include "HsVersions.h"
22 import {-# SOURCE #-} TcUnify( unifyTauTy )
24 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
25 import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
28 import Inst ( lookupInst, LookupInstResult(..),
29 tyVarsOfInst, fdPredsOfInsts, newDicts,
30 isDict, isClassDict, isLinearInst, linearInstType,
31 isStdClassTyVarDict, isMethodFor, isMethod,
32 instToId, tyVarsOfInsts, cloneDict,
33 ipNamesOfInsts, ipNamesOfInst, dictPred,
34 instBindingRequired, fdPredsOfInst,
35 newDictsFromOld, tcInstClassOp,
36 getDictClassTys, isTyVarDict,
37 instLoc, zonkInst, tidyInsts, tidyMoreInsts,
38 Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
39 isIPDict, isInheritableInst, pprDFuns, pprDictsTheta
41 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals )
42 import InstEnv ( lookupInstEnv, classInstances )
43 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
44 import TcType ( TcTyVar, TcTyVarSet, ThetaType,
45 mkClassPred, isOverloadedTy, mkTyConApp,
46 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
47 tyVarsOfPred, tcEqType, pprPred )
48 import Id ( idType, mkUserLocal )
50 import Name ( getOccName, getSrcLoc )
51 import NameSet ( NameSet, mkNameSet, elemNameSet )
52 import Class ( classBigSig, classKey )
53 import FunDeps ( oclose, grow, improve, pprEquationDoc )
54 import PrelInfo ( isNumericClass )
55 import PrelNames ( splitName, fstName, sndName, integerTyConName,
56 showClassKey, eqClassKey, ordClassKey )
57 import Type ( zipTopTvSubst, substTheta, substTy )
58 import TysWiredIn ( pairTyCon, doubleTy )
59 import ErrUtils ( Message )
61 import VarEnv ( TidyEnv )
65 import ListSetOps ( equivClasses )
66 import Util ( zipEqual, isSingleton )
67 import List ( partition )
68 import SrcLoc ( Located(..) )
73 %************************************************************************
77 %************************************************************************
79 --------------------------------------
80 Notes on functional dependencies (a bug)
81 --------------------------------------
83 | > class Foo a b | a->b
85 | > class Bar a b | a->b
89 | > instance Bar Obj Obj
91 | > instance (Bar a b) => Foo a b
93 | > foo:: (Foo a b) => a -> String
96 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
102 | Could not deduce (Bar a b) from the context (Foo a b)
103 | arising from use of `foo' at <interactive>:1
105 | Add (Bar a b) to the expected type of an expression
106 | In the first argument of `runFoo', namely `foo'
107 | In the definition of `it': it = runFoo foo
109 | Why all of the sudden does GHC need the constraint Bar a b? The
110 | function foo didn't ask for that...
112 The trouble is that to type (runFoo foo), GHC has to solve the problem:
114 Given constraint Foo a b
115 Solve constraint Foo a b'
117 Notice that b and b' aren't the same. To solve this, just do
118 improvement and then they are the same. But GHC currently does
123 That is usually fine, but it isn't here, because it sees that Foo a b is
124 not the same as Foo a b', and so instead applies the instance decl for
125 instance Bar a b => Foo a b. And that's where the Bar constraint comes
128 The Right Thing is to improve whenever the constraint set changes at
129 all. Not hard in principle, but it'll take a bit of fiddling to do.
133 --------------------------------------
134 Notes on quantification
135 --------------------------------------
137 Suppose we are about to do a generalisation step.
141 T the type of the RHS
142 C the constraints from that RHS
144 The game is to figure out
146 Q the set of type variables over which to quantify
147 Ct the constraints we will *not* quantify over
148 Cq the constraints we will quantify over
150 So we're going to infer the type
154 and float the constraints Ct further outwards.
156 Here are the things that *must* be true:
158 (A) Q intersect fv(G) = EMPTY limits how big Q can be
159 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
161 (A) says we can't quantify over a variable that's free in the
162 environment. (B) says we must quantify over all the truly free
163 variables in T, else we won't get a sufficiently general type. We do
164 not *need* to quantify over any variable that is fixed by the free
165 vars of the environment G.
167 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
169 Example: class H x y | x->y where ...
171 fv(G) = {a} C = {H a b, H c d}
174 (A) Q intersect {a} is empty
175 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
177 So Q can be {c,d}, {b,c,d}
179 Other things being equal, however, we'd like to quantify over as few
180 variables as possible: smaller types, fewer type applications, more
181 constraints can get into Ct instead of Cq.
184 -----------------------------------------
187 fv(T) the free type vars of T
189 oclose(vs,C) The result of extending the set of tyvars vs
190 using the functional dependencies from C
192 grow(vs,C) The result of extend the set of tyvars vs
193 using all conceivable links from C.
195 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
196 Then grow(vs,C) = {a,b,c}
198 Note that grow(vs,C) `superset` grow(vs,simplify(C))
199 That is, simplfication can only shrink the result of grow.
202 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
203 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
206 -----------------------------------------
210 Here's a good way to choose Q:
212 Q = grow( fv(T), C ) \ oclose( fv(G), C )
214 That is, quantify over all variable that that MIGHT be fixed by the
215 call site (which influences T), but which aren't DEFINITELY fixed by
216 G. This choice definitely quantifies over enough type variables,
217 albeit perhaps too many.
219 Why grow( fv(T), C ) rather than fv(T)? Consider
221 class H x y | x->y where ...
226 If we used fv(T) = {c} we'd get the type
228 forall c. H c d => c -> b
230 And then if the fn was called at several different c's, each of
231 which fixed d differently, we'd get a unification error, because
232 d isn't quantified. Solution: quantify d. So we must quantify
233 everything that might be influenced by c.
235 Why not oclose( fv(T), C )? Because we might not be able to see
236 all the functional dependencies yet:
238 class H x y | x->y where ...
239 instance H x y => Eq (T x y) where ...
244 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
245 apparent yet, and that's wrong. We must really quantify over d too.
248 There really isn't any point in quantifying over any more than
249 grow( fv(T), C ), because the call sites can't possibly influence
250 any other type variables.
254 --------------------------------------
256 --------------------------------------
258 It's very hard to be certain when a type is ambiguous. Consider
262 instance H x y => K (x,y)
264 Is this type ambiguous?
265 forall a b. (K (a,b), Eq b) => a -> a
267 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
268 now we see that a fixes b. So we can't tell about ambiguity for sure
269 without doing a full simplification. And even that isn't possible if
270 the context has some free vars that may get unified. Urgle!
272 Here's another example: is this ambiguous?
273 forall a b. Eq (T b) => a -> a
274 Not if there's an insance decl (with no context)
275 instance Eq (T b) where ...
277 You may say of this example that we should use the instance decl right
278 away, but you can't always do that:
280 class J a b where ...
281 instance J Int b where ...
283 f :: forall a b. J a b => a -> a
285 (Notice: no functional dependency in J's class decl.)
286 Here f's type is perfectly fine, provided f is only called at Int.
287 It's premature to complain when meeting f's signature, or even
288 when inferring a type for f.
292 However, we don't *need* to report ambiguity right away. It'll always
293 show up at the call site.... and eventually at main, which needs special
294 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
296 So here's the plan. We WARN about probable ambiguity if
298 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
300 (all tested before quantification).
301 That is, all the type variables in Cq must be fixed by the the variables
302 in the environment, or by the variables in the type.
304 Notice that we union before calling oclose. Here's an example:
306 class J a b c | a b -> c
310 forall b c. (J a b c) => b -> b
312 Only if we union {a} from G with {b} from T before using oclose,
313 do we see that c is fixed.
315 It's a bit vague exactly which C we should use for this oclose call. If we
316 don't fix enough variables we might complain when we shouldn't (see
317 the above nasty example). Nothing will be perfect. That's why we can
318 only issue a warning.
321 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
323 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
325 then c is a "bubble"; there's no way it can ever improve, and it's
326 certainly ambiguous. UNLESS it is a constant (sigh). And what about
331 instance H x y => K (x,y)
333 Is this type ambiguous?
334 forall a b. (K (a,b), Eq b) => a -> a
336 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
337 is a "bubble" that's a set of constraints
339 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
341 Hence another idea. To decide Q start with fv(T) and grow it
342 by transitive closure in Cq (no functional dependencies involved).
343 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
344 The definitely-ambiguous can then float out, and get smashed at top level
345 (which squashes out the constants, like Eq (T a) above)
348 --------------------------------------
349 Notes on principal types
350 --------------------------------------
355 f x = let g y = op (y::Int) in True
357 Here the principal type of f is (forall a. a->a)
358 but we'll produce the non-principal type
359 f :: forall a. C Int => a -> a
362 --------------------------------------
363 The need for forall's in constraints
364 --------------------------------------
366 [Exchange on Haskell Cafe 5/6 Dec 2000]
368 class C t where op :: t -> Bool
369 instance C [t] where op x = True
371 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
372 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
374 The definitions of p and q differ only in the order of the components in
375 the pair on their right-hand sides. And yet:
377 ghc and "Typing Haskell in Haskell" reject p, but accept q;
378 Hugs rejects q, but accepts p;
379 hbc rejects both p and q;
380 nhc98 ... (Malcolm, can you fill in the blank for us!).
382 The type signature for f forces context reduction to take place, and
383 the results of this depend on whether or not the type of y is known,
384 which in turn depends on which component of the pair the type checker
387 Solution: if y::m a, float out the constraints
388 Monad m, forall c. C (m c)
389 When m is later unified with [], we can solve both constraints.
392 --------------------------------------
393 Notes on implicit parameters
394 --------------------------------------
396 Question 1: can we "inherit" implicit parameters
397 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402 where f is *not* a top-level binding.
403 From the RHS of f we'll get the constraint (?y::Int).
404 There are two types we might infer for f:
408 (so we get ?y from the context of f's definition), or
410 f :: (?y::Int) => Int -> Int
412 At first you might think the first was better, becuase then
413 ?y behaves like a free variable of the definition, rather than
414 having to be passed at each call site. But of course, the WHOLE
415 IDEA is that ?y should be passed at each call site (that's what
416 dynamic binding means) so we'd better infer the second.
418 BOTTOM LINE: when *inferring types* you *must* quantify
419 over implicit parameters. See the predicate isFreeWhenInferring.
422 Question 2: type signatures
423 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
424 BUT WATCH OUT: When you supply a type signature, we can't force you
425 to quantify over implicit parameters. For example:
429 This is perfectly reasonable. We do not want to insist on
431 (?x + 1) :: (?x::Int => Int)
433 That would be silly. Here, the definition site *is* the occurrence site,
434 so the above strictures don't apply. Hence the difference between
435 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
436 and tcSimplifyCheckBind (which does not).
438 What about when you supply a type signature for a binding?
439 Is it legal to give the following explicit, user type
440 signature to f, thus:
445 At first sight this seems reasonable, but it has the nasty property
446 that adding a type signature changes the dynamic semantics.
449 (let f x = (x::Int) + ?y
450 in (f 3, f 3 with ?y=5)) with ?y = 6
456 in (f 3, f 3 with ?y=5)) with ?y = 6
460 Indeed, simply inlining f (at the Haskell source level) would change the
463 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
464 semantics for a Haskell program without knowing its typing, so if you
465 change the typing you may change the semantics.
467 To make things consistent in all cases where we are *checking* against
468 a supplied signature (as opposed to inferring a type), we adopt the
471 a signature does not need to quantify over implicit params.
473 [This represents a (rather marginal) change of policy since GHC 5.02,
474 which *required* an explicit signature to quantify over all implicit
475 params for the reasons mentioned above.]
477 But that raises a new question. Consider
479 Given (signature) ?x::Int
480 Wanted (inferred) ?x::Int, ?y::Bool
482 Clearly we want to discharge the ?x and float the ?y out. But
483 what is the criterion that distinguishes them? Clearly it isn't
484 what free type variables they have. The Right Thing seems to be
485 to float a constraint that
486 neither mentions any of the quantified type variables
487 nor any of the quantified implicit parameters
489 See the predicate isFreeWhenChecking.
492 Question 3: monomorphism
493 ~~~~~~~~~~~~~~~~~~~~~~~~
494 There's a nasty corner case when the monomorphism restriction bites:
498 The argument above suggests that we *must* generalise
499 over the ?y parameter, to get
500 z :: (?y::Int) => Int,
501 but the monomorphism restriction says that we *must not*, giving
503 Why does the momomorphism restriction say this? Because if you have
505 let z = x + ?y in z+z
507 you might not expect the addition to be done twice --- but it will if
508 we follow the argument of Question 2 and generalise over ?y.
514 (A) Always generalise over implicit parameters
515 Bindings that fall under the monomorphism restriction can't
519 * Inlining remains valid
520 * No unexpected loss of sharing
521 * But simple bindings like
523 will be rejected, unless you add an explicit type signature
524 (to avoid the monomorphism restriction)
525 z :: (?y::Int) => Int
527 This seems unacceptable
529 (B) Monomorphism restriction "wins"
530 Bindings that fall under the monomorphism restriction can't
532 Always generalise over implicit parameters *except* for bindings
533 that fall under the monomorphism restriction
536 * Inlining isn't valid in general
537 * No unexpected loss of sharing
538 * Simple bindings like
540 accepted (get value of ?y from binding site)
542 (C) Always generalise over implicit parameters
543 Bindings that fall under the monomorphism restriction can't
544 be generalised, EXCEPT for implicit parameters
546 * Inlining remains valid
547 * Unexpected loss of sharing (from the extra generalisation)
548 * Simple bindings like
550 accepted (get value of ?y from occurrence sites)
555 None of these choices seems very satisfactory. But at least we should
556 decide which we want to do.
558 It's really not clear what is the Right Thing To Do. If you see
562 would you expect the value of ?y to be got from the *occurrence sites*
563 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
564 case of function definitions, the answer is clearly the former, but
565 less so in the case of non-fucntion definitions. On the other hand,
566 if we say that we get the value of ?y from the definition site of 'z',
567 then inlining 'z' might change the semantics of the program.
569 Choice (C) really says "the monomorphism restriction doesn't apply
570 to implicit parameters". Which is fine, but remember that every
571 innocent binding 'x = ...' that mentions an implicit parameter in
572 the RHS becomes a *function* of that parameter, called at each
573 use of 'x'. Now, the chances are that there are no intervening 'with'
574 clauses that bind ?y, so a decent compiler should common up all
575 those function calls. So I think I strongly favour (C). Indeed,
576 one could make a similar argument for abolishing the monomorphism
577 restriction altogether.
579 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
583 %************************************************************************
585 \subsection{tcSimplifyInfer}
587 %************************************************************************
589 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
591 1. Compute Q = grow( fvs(T), C )
593 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
594 predicates will end up in Ct; we deal with them at the top level
596 3. Try improvement, using functional dependencies
598 4. If Step 3 did any unification, repeat from step 1
599 (Unification can change the result of 'grow'.)
601 Note: we don't reduce dictionaries in step 2. For example, if we have
602 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
603 after step 2. However note that we may therefore quantify over more
604 type variables than we absolutely have to.
606 For the guts, we need a loop, that alternates context reduction and
607 improvement with unification. E.g. Suppose we have
609 class C x y | x->y where ...
611 and tcSimplify is called with:
613 Then improvement unifies a with b, giving
616 If we need to unify anything, we rattle round the whole thing all over
623 -> TcTyVarSet -- fv(T); type vars
625 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
626 TcDictBinds, -- Bindings
627 [TcId]) -- Dict Ids that must be bound here (zonked)
628 -- Any free (escaping) Insts are tossed into the environment
633 tcSimplifyInfer doc tau_tvs wanted_lie
634 = inferLoop doc (varSetElems tau_tvs)
635 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
637 extendLIEs frees `thenM_`
638 returnM (qtvs, binds, map instToId irreds)
640 inferLoop doc tau_tvs wanteds
642 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
643 mappM zonkInst wanteds `thenM` \ wanteds' ->
644 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
646 preds = fdPredsOfInsts wanteds'
647 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
650 | isFreeWhenInferring qtvs inst = Free
651 | isClassDict inst = DontReduceUnlessConstant -- Dicts
652 | otherwise = ReduceMe -- Lits and Methods
654 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
655 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
657 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
660 if no_improvement then
661 returnM (varSetElems qtvs, frees, binds, irreds)
663 -- If improvement did some unification, we go round again. There
664 -- are two subtleties:
665 -- a) We start again with irreds, not wanteds
666 -- Using an instance decl might have introduced a fresh type variable
667 -- which might have been unified, so we'd get an infinite loop
668 -- if we started again with wanteds! See example [LOOP]
670 -- b) It's also essential to re-process frees, because unification
671 -- might mean that a type variable that looked free isn't now.
673 -- Hence the (irreds ++ frees)
675 -- However, NOTICE that when we are done, we might have some bindings, but
676 -- the final qtvs might be empty. See [NO TYVARS] below.
678 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
679 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
684 class If b t e r | b t e -> r
687 class Lte a b c | a b -> c where lte :: a -> b -> c
689 instance (Lte a b l,If l b a c) => Max a b c
691 Wanted: Max Z (S x) y
693 Then we'll reduce using the Max instance to:
694 (Lte Z (S x) l, If l (S x) Z y)
695 and improve by binding l->T, after which we can do some reduction
696 on both the Lte and If constraints. What we *can't* do is start again
697 with (Max Z (S x) y)!
701 class Y a b | a -> b where
704 instance Y [[a]] a where
707 k :: X a -> X a -> X a
709 g :: Num a => [X a] -> [X a]
712 h ys = ys ++ map (k (y [[0]])) xs
714 The excitement comes when simplifying the bindings for h. Initially
715 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
716 From this we get t1:=:t2, but also various bindings. We can't forget
717 the bindings (because of [LOOP]), but in fact t1 is what g is
720 The net effect of [NO TYVARS]
723 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
724 isFreeWhenInferring qtvs inst
725 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
726 && isInheritableInst inst -- And no implicit parameter involved
727 -- (see "Notes on implicit parameters")
729 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
730 -> NameSet -- Quantified implicit parameters
732 isFreeWhenChecking qtvs ips inst
733 = isFreeWrtTyVars qtvs inst
734 && isFreeWrtIPs ips inst
736 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
737 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
741 %************************************************************************
743 \subsection{tcSimplifyCheck}
745 %************************************************************************
747 @tcSimplifyCheck@ is used when we know exactly the set of variables
748 we are going to quantify over. For example, a class or instance declaration.
753 -> [TcTyVar] -- Quantify over these
756 -> TcM TcDictBinds -- Bindings
758 -- tcSimplifyCheck is used when checking expression type signatures,
759 -- class decls, instance decls etc.
761 -- NB: tcSimplifyCheck does not consult the
762 -- global type variables in the environment; so you don't
763 -- need to worry about setting them before calling tcSimplifyCheck
764 tcSimplifyCheck doc qtvs givens wanted_lie
765 = tcSimplCheck doc get_qtvs
766 givens wanted_lie `thenM` \ (qtvs', binds) ->
769 -- get_qtvs = zonkTcTyVarsAndFV qtvs
770 get_qtvs = return (mkVarSet qtvs)
773 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
774 -- against, but we don't know the type variables over which we are going to quantify.
775 -- This happens when we have a type signature for a mutually recursive group
778 -> TcTyVarSet -- fv(T)
781 -> TcM ([TcTyVar], -- Variables over which to quantify
782 TcDictBinds) -- Bindings
784 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
785 = tcSimplCheck doc get_qtvs givens wanted_lie
787 -- Figure out which type variables to quantify over
788 -- You might think it should just be the signature tyvars,
789 -- but in bizarre cases you can get extra ones
790 -- f :: forall a. Num a => a -> a
791 -- f x = fst (g (x, head [])) + 1
793 -- Here we infer g :: forall a b. a -> b -> (b,a)
794 -- We don't want g to be monomorphic in b just because
795 -- f isn't quantified over b.
796 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
798 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
799 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
801 qtvs = all_tvs' `minusVarSet` gbl_tvs
802 -- We could close gbl_tvs, but its not necessary for
803 -- soundness, and it'll only affect which tyvars, not which
804 -- dictionaries, we quantify over
809 Here is the workhorse function for all three wrappers.
812 tcSimplCheck doc get_qtvs givens wanted_lie
813 = check_loop givens wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
815 -- Complain about any irreducible ones
816 mappM zonkInst given_dicts_and_ips `thenM` \ givens' ->
817 groupErrs (addNoInstanceErrs (Just doc) givens') irreds `thenM_`
820 extendLIEs frees `thenM_`
821 returnM (qtvs, binds)
824 given_dicts_and_ips = filter (not . isMethod) givens
825 -- For error reporting, filter out methods, which are
826 -- only added to the given set as an optimisation
828 ip_set = mkNameSet (ipNamesOfInsts givens)
830 check_loop givens wanteds
832 mappM zonkInst givens `thenM` \ givens' ->
833 mappM zonkInst wanteds `thenM` \ wanteds' ->
834 get_qtvs `thenM` \ qtvs' ->
838 -- When checking against a given signature we always reduce
839 -- until we find a match against something given, or can't reduce
840 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
841 | otherwise = ReduceMe
843 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
846 if no_improvement then
847 returnM (varSetElems qtvs', frees, binds, irreds)
849 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
850 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
854 %************************************************************************
856 \subsection{tcSimplifyRestricted}
858 %************************************************************************
860 tcSimplifyRestricted infers which type variables to quantify for a
861 group of restricted bindings. This isn't trivial.
864 We want to quantify over a to get id :: forall a. a->a
867 We do not want to quantify over a, because there's an Eq a
868 constraint, so we get eq :: a->a->Bool (notice no forall)
871 RHS has type 'tau', whose free tyvars are tau_tvs
872 RHS has constraints 'wanteds'
875 Quantify over (tau_tvs \ ftvs(wanteds))
876 This is bad. The constraints may contain (Monad (ST s))
877 where we have instance Monad (ST s) where...
878 so there's no need to be monomorphic in s!
880 Also the constraint might be a method constraint,
881 whose type mentions a perfectly innocent tyvar:
882 op :: Num a => a -> b -> a
883 Here, b is unconstrained. A good example would be
885 We want to infer the polymorphic type
886 foo :: forall b. b -> b
889 Plan B (cunning, used for a long time up to and including GHC 6.2)
890 Step 1: Simplify the constraints as much as possible (to deal
891 with Plan A's problem). Then set
892 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
894 Step 2: Now simplify again, treating the constraint as 'free' if
895 it does not mention qtvs, and trying to reduce it otherwise.
896 The reasons for this is to maximise sharing.
898 This fails for a very subtle reason. Suppose that in the Step 2
899 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
900 In the Step 1 this constraint might have been simplified, perhaps to
901 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
902 This won't happen in Step 2... but that in turn might prevent some other
903 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
904 and that in turn breaks the invariant that no constraints are quantified over.
906 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
911 Step 1: Simplify the constraints as much as possible (to deal
912 with Plan A's problem). Then set
913 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
914 Return the bindings from Step 1.
917 A note about Plan C (arising from "bug" reported by George Russel March 2004)
920 instance (HasBinary ty IO) => HasCodedValue ty
922 foo :: HasCodedValue a => String -> IO a
924 doDecodeIO :: HasCodedValue a => () -> () -> IO a
925 doDecodeIO codedValue view
926 = let { act = foo "foo" } in act
928 You might think this should work becuase the call to foo gives rise to a constraint
929 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
930 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
931 constraint using the (rather bogus) instance declaration, and now we are stuffed.
933 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
937 Plan D (a variant of plan B)
938 Step 1: Simplify the constraints as much as possible (to deal
939 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
940 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
942 Step 2: Now simplify again, treating the constraint as 'free' if
943 it does not mention qtvs, and trying to reduce it otherwise.
945 The point here is that it's generally OK to have too few qtvs; that is,
946 to make the thing more monomorphic than it could be. We don't want to
947 do that in the common cases, but in wierd cases it's ok: the programmer
948 can always add a signature.
950 Too few qtvs => too many wanteds, which is what happens if you do less
955 tcSimplifyRestricted -- Used for restricted binding groups
956 -- i.e. ones subject to the monomorphism restriction
958 -> TcTyVarSet -- Free in the type of the RHSs
959 -> [Inst] -- Free in the RHSs
960 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
961 TcDictBinds) -- Bindings
962 -- tcSimpifyRestricted returns no constraints to
963 -- quantify over; by definition there are none.
964 -- They are all thrown back in the LIE
966 tcSimplifyRestricted doc tau_tvs wanteds
967 -- Zonk everything in sight
968 = mappM zonkInst wanteds `thenM` \ wanteds' ->
969 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
970 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
972 -- 'reduceMe': Reduce as far as we can. Don't stop at
973 -- dicts; the idea is to get rid of as many type
974 -- variables as possible, and we don't want to stop
975 -- at (say) Monad (ST s), because that reduces
976 -- immediately, with no constraint on s.
978 -- BUT do no improvement! See Plan D above
979 reduceContextWithoutImprovement
980 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
982 -- Next, figure out the tyvars we will quantify over
984 constrained_tvs = tyVarsOfInsts constrained_dicts
985 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
986 `minusVarSet` constrained_tvs
987 try_me inst | isFreeWrtTyVars qtvs inst = Free
988 | otherwise = ReduceMe
990 traceTc (text "tcSimplifyRestricted" <+> vcat [
991 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
993 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
995 -- The first step may have squashed more methods than
996 -- necessary, so try again, this time more gently, knowing the exact
997 -- set of type variables to quantify over.
999 -- We quantify only over constraints that are captured by qtvs;
1000 -- these will just be a subset of non-dicts. This in contrast
1001 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1002 -- all *non-inheritable* constraints too. This implements choice
1003 -- (B) under "implicit parameter and monomorphism" above.
1005 -- Remember that we may need to do *some* simplification, to
1006 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1007 -- just to float all constraints
1008 reduceContextWithoutImprovement
1009 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1010 ASSERT( null irreds )
1011 extendLIEs frees `thenM_`
1012 returnM (varSetElems qtvs, binds)
1016 %************************************************************************
1018 \subsection{tcSimplifyToDicts}
1020 %************************************************************************
1022 On the LHS of transformation rules we only simplify methods and constants,
1023 getting dictionaries. We want to keep all of them unsimplified, to serve
1024 as the available stuff for the RHS of the rule.
1026 The same thing is used for specialise pragmas. Consider
1028 f :: Num a => a -> a
1029 {-# SPECIALISE f :: Int -> Int #-}
1032 The type checker generates a binding like:
1034 f_spec = (f :: Int -> Int)
1036 and we want to end up with
1038 f_spec = _inline_me_ (f Int dNumInt)
1040 But that means that we must simplify the Method for f to (f Int dNumInt)!
1041 So tcSimplifyToDicts squeezes out all Methods.
1043 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
1045 fromIntegral :: (Integral a, Num b) => a -> b
1046 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1048 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
1051 forall dIntegralInt.
1052 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1054 because the scsel will mess up matching. Instead we want
1056 forall dIntegralInt, dNumInt.
1057 fromIntegral Int Int dIntegralInt dNumInt = id Int
1062 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
1063 tcSimplifyToDicts wanteds
1064 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1065 -- Since try_me doesn't look at types, we don't need to
1066 -- do any zonking, so it's safe to call reduceContext directly
1067 ASSERT( null frees )
1068 extendLIEs irreds `thenM_`
1072 doc = text "tcSimplifyToDicts"
1074 -- Reduce methods and lits only; stop as soon as we get a dictionary
1075 try_me inst | isDict inst = KeepDictWithoutSCs -- See notes above re "WithoutSCs"
1076 | otherwise = ReduceMe
1081 tcSimplifyBracket is used when simplifying the constraints arising from
1082 a Template Haskell bracket [| ... |]. We want to check that there aren't
1083 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1084 Show instance), but we aren't otherwise interested in the results.
1085 Nor do we care about ambiguous dictionaries etc. We will type check
1086 this bracket again at its usage site.
1089 tcSimplifyBracket :: [Inst] -> TcM ()
1090 tcSimplifyBracket wanteds
1091 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1094 doc = text "tcSimplifyBracket"
1098 %************************************************************************
1100 \subsection{Filtering at a dynamic binding}
1102 %************************************************************************
1107 we must discharge all the ?x constraints from B. We also do an improvement
1108 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1110 Actually, the constraints from B might improve the types in ?x. For example
1112 f :: (?x::Int) => Char -> Char
1115 then the constraint (?x::Int) arising from the call to f will
1116 force the binding for ?x to be of type Int.
1119 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1122 tcSimplifyIPs given_ips wanteds
1123 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1124 extendLIEs frees `thenM_`
1127 doc = text "tcSimplifyIPs" <+> ppr given_ips
1128 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1130 -- Simplify any methods that mention the implicit parameter
1131 try_me inst | isFreeWrtIPs ip_set inst = Free
1132 | otherwise = ReduceMe
1134 simpl_loop givens wanteds
1135 = mappM zonkInst givens `thenM` \ givens' ->
1136 mappM zonkInst wanteds `thenM` \ wanteds' ->
1138 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1140 if no_improvement then
1141 ASSERT( null irreds )
1142 returnM (frees, binds)
1144 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1145 returnM (frees1, binds `unionBags` binds1)
1149 %************************************************************************
1151 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1153 %************************************************************************
1155 When doing a binding group, we may have @Insts@ of local functions.
1156 For example, we might have...
1158 let f x = x + 1 -- orig local function (overloaded)
1159 f.1 = f Int -- two instances of f
1164 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1165 where @f@ is in scope; those @Insts@ must certainly not be passed
1166 upwards towards the top-level. If the @Insts@ were binding-ified up
1167 there, they would have unresolvable references to @f@.
1169 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1170 For each method @Inst@ in the @init_lie@ that mentions one of the
1171 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1172 @LIE@), as well as the @HsBinds@ generated.
1175 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1176 -- Simlifies only MethodInsts, and generate only bindings of form
1178 -- We're careful not to even generate bindings of the form
1180 -- You'd think that'd be fine, but it interacts with what is
1181 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1183 bindInstsOfLocalFuns wanteds local_ids
1184 | null overloaded_ids
1186 = extendLIEs wanteds `thenM_`
1187 returnM emptyLHsBinds
1190 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1191 ASSERT( null irreds )
1192 extendLIEs not_for_me `thenM_`
1193 extendLIEs frees `thenM_`
1196 doc = text "bindInsts" <+> ppr local_ids
1197 overloaded_ids = filter is_overloaded local_ids
1198 is_overloaded id = isOverloadedTy (idType id)
1199 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1201 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1202 -- so it's worth building a set, so that
1203 -- lookup (in isMethodFor) is faster
1204 try_me inst | isMethod inst = ReduceMe
1209 %************************************************************************
1211 \subsection{Data types for the reduction mechanism}
1213 %************************************************************************
1215 The main control over context reduction is here
1219 = ReduceMe -- Try to reduce this
1220 -- If there's no instance, behave exactly like
1221 -- DontReduce: add the inst to
1222 -- the irreductible ones, but don't
1223 -- produce an error message of any kind.
1224 -- It might be quite legitimate such as (Eq a)!
1226 | KeepDictWithoutSCs -- Return as irreducible; don't add its superclasses
1227 -- Rather specialised: see notes with tcSimplifyToDicts
1229 | DontReduceUnlessConstant -- Return as irreducible unless it can
1230 -- be reduced to a constant in one step
1232 | Free -- Return as free
1234 reduceMe :: Inst -> WhatToDo
1235 reduceMe inst = ReduceMe
1237 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1238 -- of a predicate when adding it to the avails
1244 type Avails = FiniteMap Inst Avail
1245 emptyAvails = emptyFM
1248 = IsFree -- Used for free Insts
1249 | Irred -- Used for irreducible dictionaries,
1250 -- which are going to be lambda bound
1252 | Given TcId -- Used for dictionaries for which we have a binding
1253 -- e.g. those "given" in a signature
1254 Bool -- True <=> actually consumed (splittable IPs only)
1256 | NoRhs -- Used for Insts like (CCallable f)
1257 -- where no witness is required.
1260 | Rhs -- Used when there is a RHS
1261 (LHsExpr TcId) -- The RHS
1262 [Inst] -- Insts free in the RHS; we need these too
1264 | Linear -- Splittable Insts only.
1265 Int -- The Int is always 2 or more; indicates how
1266 -- many copies are required
1267 Inst -- The splitter
1268 Avail -- Where the "master copy" is
1270 | LinRhss -- Splittable Insts only; this is used only internally
1271 -- by extractResults, where a Linear
1272 -- is turned into an LinRhss
1273 [LHsExpr TcId] -- A supply of suitable RHSs
1275 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1276 | (inst,avail) <- fmToList avails ]
1278 instance Outputable Avail where
1281 pprAvail NoRhs = text "<no rhs>"
1282 pprAvail IsFree = text "Free"
1283 pprAvail Irred = text "Irred"
1284 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1285 if b then text "(used)" else empty
1286 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1287 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1288 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1291 Extracting the bindings from a bunch of Avails.
1292 The bindings do *not* come back sorted in dependency order.
1293 We assume that they'll be wrapped in a big Rec, so that the
1294 dependency analyser can sort them out later
1298 extractResults :: Avails
1300 -> TcM (TcDictBinds, -- Bindings
1301 [Inst], -- Irreducible ones
1302 [Inst]) -- Free ones
1304 extractResults avails wanteds
1305 = go avails emptyBag [] [] wanteds
1307 go avails binds irreds frees []
1308 = returnM (binds, irreds, frees)
1310 go avails binds irreds frees (w:ws)
1311 = case lookupFM avails w of
1312 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1313 go avails binds irreds frees ws
1315 Just NoRhs -> go avails binds irreds frees ws
1316 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1317 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1319 Just (Given id _) -> go avails new_binds irreds frees ws
1321 new_binds | id == instToId w = binds
1322 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1323 -- The sought Id can be one of the givens, via a superclass chain
1324 -- and then we definitely don't want to generate an x=x binding!
1326 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1328 new_binds = addBind binds w rhs
1330 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1331 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1332 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1333 go (addToFM avails w (LinRhss rhss))
1334 (binds `unionBags` binds')
1335 irreds' frees' (split_inst : w : ws)
1337 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1338 -> go new_avails new_binds irreds frees ws
1340 new_binds = addBind binds w rhs
1341 new_avails = addToFM avails w (LinRhss rhss)
1343 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1344 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1345 returnM (w':irreds, frees, instToId w')
1346 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1347 returnM (irreds, w':frees, instToId w')
1350 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1351 | otherwise = addToFM avails w NoRhs
1352 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1353 -- than Given, else we end up with bogus bindings.
1355 add_free avails w | isMethod w = avails
1356 | otherwise = add_given avails w
1358 -- Do *not* replace Free by Given if it's a method.
1359 -- The following situation shows why this is bad:
1360 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1361 -- From an application (truncate f i) we get
1362 -- t1 = truncate at f
1364 -- If we have also have a second occurrence of truncate, we get
1365 -- t3 = truncate at f
1367 -- When simplifying with i,f free, we might still notice that
1368 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1369 -- will continue to float out!
1370 -- (split n i a) returns: n rhss
1371 -- auxiliary bindings
1372 -- 1 or 0 insts to add to irreds
1375 split :: Int -> TcId -> TcId -> Inst
1376 -> TcM (TcDictBinds, [LHsExpr TcId])
1377 -- (split n split_id root_id wanted) returns
1378 -- * a list of 'n' expressions, all of which witness 'avail'
1379 -- * a bunch of auxiliary bindings to support these expressions
1380 -- * one or zero insts needed to witness the whole lot
1381 -- (maybe be zero if the initial Inst is a Given)
1383 -- NB: 'wanted' is just a template
1385 split n split_id root_id wanted
1388 ty = linearInstType wanted
1389 pair_ty = mkTyConApp pairTyCon [ty,ty]
1390 id = instToId wanted
1393 span = instSpan wanted
1395 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1397 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1398 expand n rhss `thenM` \ (binds2, rhss') ->
1399 returnM (binds1 `unionBags` binds2, rhss')
1402 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1403 -- e.g. expand 3 [rhs1, rhs2]
1404 -- = ( { x = split rhs1 },
1405 -- [fst x, snd x, rhs2] )
1407 | n `rem` 2 == 0 = go rhss -- n is even
1408 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1409 returnM (binds', head rhss : rhss')
1411 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1412 returnM (listToBag binds', concat rhss')
1414 do_one rhs = newUnique `thenM` \ uniq ->
1415 tcLookupId fstName `thenM` \ fst_id ->
1416 tcLookupId sndName `thenM` \ snd_id ->
1418 x = mkUserLocal occ uniq pair_ty loc
1420 returnM (L span (VarBind x (mk_app span split_id rhs)),
1421 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1423 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1425 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1427 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1428 (VarBind (instToId inst) rhs))
1429 instSpan wanted = instLocSrcSpan (instLoc wanted)
1433 %************************************************************************
1435 \subsection[reduce]{@reduce@}
1437 %************************************************************************
1439 When the "what to do" predicate doesn't depend on the quantified type variables,
1440 matters are easier. We don't need to do any zonking, unless the improvement step
1441 does something, in which case we zonk before iterating.
1443 The "given" set is always empty.
1446 simpleReduceLoop :: SDoc
1447 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1449 -> TcM ([Inst], -- Free
1451 [Inst]) -- Irreducible
1453 simpleReduceLoop doc try_me wanteds
1454 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1455 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1456 if no_improvement then
1457 returnM (frees, binds, irreds)
1459 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1460 returnM (frees1, binds `unionBags` binds1, irreds1)
1466 reduceContext :: SDoc
1467 -> (Inst -> WhatToDo)
1470 -> TcM (Bool, -- True <=> improve step did no unification
1472 TcDictBinds, -- Dictionary bindings
1473 [Inst]) -- Irreducible
1475 reduceContext doc try_me givens wanteds
1477 traceTc (text "reduceContext" <+> (vcat [
1478 text "----------------------",
1480 text "given" <+> ppr givens,
1481 text "wanted" <+> ppr wanteds,
1482 text "----------------------"
1485 -- Build the Avail mapping from "givens"
1486 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1489 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1491 -- Do improvement, using everything in avails
1492 -- In particular, avails includes all superclasses of everything
1493 tcImprove avails `thenM` \ no_improvement ->
1495 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1497 traceTc (text "reduceContext end" <+> (vcat [
1498 text "----------------------",
1500 text "given" <+> ppr givens,
1501 text "wanted" <+> ppr wanteds,
1503 text "avails" <+> pprAvails avails,
1504 text "frees" <+> ppr frees,
1505 text "no_improvement =" <+> ppr no_improvement,
1506 text "----------------------"
1509 returnM (no_improvement, frees, binds, irreds)
1511 -- reduceContextWithoutImprovement differs from reduceContext
1512 -- (a) no improvement
1513 -- (b) 'givens' is assumed empty
1514 reduceContextWithoutImprovement doc try_me wanteds
1516 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1517 text "----------------------",
1519 text "wanted" <+> ppr wanteds,
1520 text "----------------------"
1524 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1525 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1527 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1528 text "----------------------",
1530 text "wanted" <+> ppr wanteds,
1532 text "avails" <+> pprAvails avails,
1533 text "frees" <+> ppr frees,
1534 text "----------------------"
1537 returnM (frees, binds, irreds)
1539 tcImprove :: Avails -> TcM Bool -- False <=> no change
1540 -- Perform improvement using all the predicates in Avails
1542 = tcGetInstEnvs `thenM` \ inst_envs ->
1544 preds = [ (pred, pp_loc)
1545 | (inst, avail) <- fmToList avails,
1546 pred <- get_preds inst avail,
1547 let pp_loc = pprInstLoc (instLoc inst)
1549 -- Avails has all the superclasses etc (good)
1550 -- It also has all the intermediates of the deduction (good)
1551 -- It does not have duplicates (good)
1552 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1553 -- so that improve will see them separate
1555 -- For free Methods, we want to take predicates from their context,
1556 -- but for Methods that have been squished their context will already
1557 -- be in Avails, and we don't want duplicates. Hence this rather
1558 -- horrid get_preds function
1559 get_preds inst IsFree = fdPredsOfInst inst
1560 get_preds inst other | isDict inst = [dictPred inst]
1563 eqns = improve get_insts preds
1564 get_insts clas = classInstances inst_envs clas
1569 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1570 mappM_ unify eqns `thenM_`
1573 unify ((qtvs, pairs), doc)
1575 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1576 mapM_ (unif_pr tenv) pairs
1577 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1580 The main context-reduction function is @reduce@. Here's its game plan.
1583 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1584 -- along with its depth
1585 -> (Inst -> WhatToDo)
1592 try_me: given an inst, this function returns
1594 DontReduce return this in "irreds"
1595 Free return this in "frees"
1597 wanteds: The list of insts to reduce
1598 state: An accumulating parameter of type Avails
1599 that contains the state of the algorithm
1601 It returns a Avails.
1603 The (n,stack) pair is just used for error reporting.
1604 n is always the depth of the stack.
1605 The stack is the stack of Insts being reduced: to produce X
1606 I had to produce Y, to produce Y I had to produce Z, and so on.
1609 reduceList (n,stack) try_me wanteds state
1610 | n > opt_MaxContextReductionDepth
1611 = failWithTc (reduceDepthErr n stack)
1617 pprTrace "Interesting! Context reduction stack deeper than 8:"
1618 (nest 2 (pprStack stack))
1623 go [] state = returnM state
1624 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1627 -- Base case: we're done!
1628 reduce stack try_me wanted avails
1629 -- It's the same as an existing inst, or a superclass thereof
1630 | Just avail <- isAvailable avails wanted
1631 = if isLinearInst wanted then
1632 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1633 reduceList stack try_me wanteds' avails'
1635 returnM avails -- No op for non-linear things
1638 = case try_me wanted of {
1640 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1642 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1643 -- First, see if the inst can be reduced to a constant in one step
1644 try_simple (addIrred AddSCs) -- Assume want superclasses
1646 ; Free -> -- It's free so just chuck it upstairs
1647 -- First, see if the inst can be reduced to a constant in one step
1650 ; ReduceMe -> -- It should be reduced
1651 lookupInst wanted `thenM` \ lookup_result ->
1652 case lookup_result of
1653 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1654 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1655 addWanted avails2 wanted rhs wanteds'
1656 -- Experiment with temporarily doing addIrred *before* the reduceList,
1657 -- which has the effect of adding the thing we are trying
1658 -- to prove to the database before trying to prove the things it
1659 -- needs. See note [RECURSIVE DICTIONARIES]
1660 -- NB: we must not do an addWanted before, because that adds the
1661 -- superclasses too, and thaat can lead to a spurious loop; see
1662 -- the examples in [SUPERCLASS-LOOP]
1663 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1665 SimpleInst rhs -> addWanted avails wanted rhs []
1667 NoInstance -> -- No such instance!
1668 -- Add it and its superclasses
1669 addIrred AddSCs avails wanted
1672 try_simple do_this_otherwise
1673 = lookupInst wanted `thenM` \ lookup_result ->
1674 case lookup_result of
1675 SimpleInst rhs -> addWanted avails wanted rhs []
1676 other -> do_this_otherwise avails wanted
1681 -------------------------
1682 isAvailable :: Avails -> Inst -> Maybe Avail
1683 isAvailable avails wanted = lookupFM avails wanted
1684 -- NB 1: the Ord instance of Inst compares by the class/type info
1685 -- *not* by unique. So
1686 -- d1::C Int == d2::C Int
1688 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1689 addLinearAvailable avails avail wanted
1690 -- avails currently maps [wanted -> avail]
1691 -- Extend avails to reflect a neeed for an extra copy of avail
1693 | Just avail' <- split_avail avail
1694 = returnM (addToFM avails wanted avail', [])
1697 = tcLookupId splitName `thenM` \ split_id ->
1698 tcInstClassOp (instLoc wanted) split_id
1699 [linearInstType wanted] `thenM` \ split_inst ->
1700 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1703 split_avail :: Avail -> Maybe Avail
1704 -- (Just av) if there's a modified version of avail that
1705 -- we can use to replace avail in avails
1706 -- Nothing if there isn't, so we need to create a Linear
1707 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1708 split_avail (Given id used) | not used = Just (Given id True)
1709 | otherwise = Nothing
1710 split_avail Irred = Nothing
1711 split_avail IsFree = Nothing
1712 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1714 -------------------------
1715 addFree :: Avails -> Inst -> TcM Avails
1716 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1717 -- to avails, so that any other equal Insts will be commoned up right
1718 -- here rather than also being tossed upstairs. This is really just
1719 -- an optimisation, and perhaps it is more trouble that it is worth,
1720 -- as the following comments show!
1722 -- NB: do *not* add superclasses. If we have
1725 -- but a is not bound here, then we *don't* want to derive
1726 -- dn from df here lest we lose sharing.
1728 addFree avails free = returnM (addToFM avails free IsFree)
1730 addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1731 addWanted avails wanted rhs_expr wanteds
1732 = addAvailAndSCs avails wanted avail
1734 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1735 | otherwise = ASSERT( null wanteds ) NoRhs
1737 addGiven :: Avails -> Inst -> TcM Avails
1738 addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
1739 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1740 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1741 -- so the assert isn't true
1743 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1744 addIrred NoSCs avails irred = returnM (addToFM avails irred Irred)
1745 addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1746 addAvailAndSCs avails irred Irred
1748 addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
1749 addAvailAndSCs avails inst avail
1750 | not (isClassDict inst) = returnM avails1
1751 | otherwise = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
1752 addSCs is_loop avails1 inst
1754 avails1 = addToFM avails inst avail
1755 is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
1756 -- Note: this compares by *type*, not by Unique
1757 deps = findAllDeps emptyVarSet avail
1758 dep_tys = map idType (varSetElems deps)
1760 findAllDeps :: IdSet -> Avail -> IdSet
1761 -- Find all the Insts that this one depends on
1762 -- See Note [SUPERCLASS-LOOP]
1763 -- Watch out, though. Since the avails may contain loops
1764 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1765 findAllDeps so_far (Rhs _ kids)
1767 (extendVarSetList so_far (map instToId kids)) -- Add the kids to so_far
1768 [a | Just a <- map (lookupFM avails) kids] -- Find the kids' Avail
1769 findAllDeps so_far other = so_far
1772 addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
1773 -- Add all the superclasses of the Inst to Avails
1774 -- The first param says "dont do this because the original thing
1775 -- depends on this one, so you'd build a loop"
1776 -- Invariant: the Inst is already in Avails.
1778 addSCs is_loop avails dict
1779 = newDictsFromOld dict sc_theta' `thenM` \ sc_dicts ->
1780 foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1782 (clas, tys) = getDictClassTys dict
1783 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1784 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1786 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1787 | add_me sc_dict = addSCs is_loop avails' sc_dict
1788 | otherwise = returnM avails
1790 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1791 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1793 add_me :: Inst -> Bool
1795 | is_loop sc_dict = False -- See Note [SUPERCLASS-LOOP]
1796 | otherwise = case lookupFM avails sc_dict of
1797 Just (Given _ _) -> False -- Given is cheaper than superclass selection
1801 Note [SUPERCLASS-LOOP]: Checking for loops
1802 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1803 We have to be careful here. If we are *given* d1:Ord a,
1804 and want to deduce (d2:C [a]) where
1806 class Ord a => C a where
1807 instance Ord a => C [a] where ...
1809 Then we'll use the instance decl to deduce C [a] and then add the
1810 superclasses of C [a] to avails. But we must not overwrite the binding
1811 for d1:Ord a (which is given) with a superclass selection or we'll just
1814 Here's another variant, immortalised in tcrun020
1815 class Monad m => C1 m
1816 class C1 m => C2 m x
1817 instance C2 Maybe Bool
1818 For the instance decl we need to build (C1 Maybe), and it's no good if
1819 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1820 before we search for C1 Maybe.
1822 Here's another example
1823 class Eq b => Foo a b
1824 instance Eq a => Foo [a] a
1828 we'll first deduce that it holds (via the instance decl). We must not
1829 then overwrite the Eq t constraint with a superclass selection!
1831 At first I had a gross hack, whereby I simply did not add superclass constraints
1832 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1833 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1834 I found a very obscure program (now tcrun021) in which improvement meant the
1835 simplifier got two bites a the cherry... so something seemed to be an Irred
1836 first time, but reducible next time.
1838 Now we implement the Right Solution, which is to check for loops directly
1839 when adding superclasses. It's a bit like the occurs check in unification.
1842 Note [RECURSIVE DICTIONARIES]
1843 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1845 data D r = ZeroD | SuccD (r (D r));
1847 instance (Eq (r (D r))) => Eq (D r) where
1848 ZeroD == ZeroD = True
1849 (SuccD a) == (SuccD b) = a == b
1852 equalDC :: D [] -> D [] -> Bool;
1855 We need to prove (Eq (D [])). Here's how we go:
1859 by instance decl, holds if
1863 by instance decl of Eq, holds if
1865 where d2 = dfEqList d3
1868 But now we can "tie the knot" to give
1874 and it'll even run! The trick is to put the thing we are trying to prove
1875 (in this case Eq (D []) into the database before trying to prove its
1876 contributing clauses.
1879 %************************************************************************
1881 \section{tcSimplifyTop: defaulting}
1883 %************************************************************************
1886 @tcSimplifyTop@ is called once per module to simplify all the constant
1887 and ambiguous Insts.
1889 We need to be careful of one case. Suppose we have
1891 instance Num a => Num (Foo a b) where ...
1893 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1894 to (Num x), and default x to Int. But what about y??
1896 It's OK: the final zonking stage should zap y to (), which is fine.
1900 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
1901 tcSimplifyTop wanteds = tc_simplify_top False {- Not interactive loop -} wanteds
1902 tcSimplifyInteractive wanteds = tc_simplify_top True {- Interactive loop -} wanteds
1905 -- The TcLclEnv should be valid here, solely to improve
1906 -- error message generation for the monomorphism restriction
1907 tc_simplify_top is_interactive wanteds
1908 = getLclEnv `thenM` \ lcl_env ->
1909 traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env)) `thenM_`
1910 simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenM` \ (frees, binds, irreds) ->
1911 ASSERT( null frees )
1914 -- All the non-std ones are definite errors
1915 (stds, non_stds) = partition isStdClassTyVarDict irreds
1917 -- Group by type variable
1918 std_groups = equivClasses cmp_by_tyvar stds
1920 -- Pick the ones which its worth trying to disambiguate
1921 -- namely, the onese whose type variable isn't bound
1922 -- up with one of the non-standard classes
1923 (std_oks, std_bads) = partition worth_a_try std_groups
1924 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1925 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1927 -- Collect together all the bad guys
1928 bad_guys = non_stds ++ concat std_bads
1929 (bad_ips, non_ips) = partition isIPDict bad_guys
1930 (no_insts, ambigs) = partition no_inst non_ips
1931 no_inst d = not (isTyVarDict d)
1932 -- Previously, there was a more elaborate no_inst definition:
1933 -- no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1934 -- fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
1935 -- But that seems over-elaborate to me; it only bites for class decls with
1936 -- fundeps like this: class C a b | -> b where ...
1939 -- Report definite errors
1940 groupErrs (addNoInstanceErrs Nothing []) no_insts `thenM_`
1941 addTopIPErrs bad_ips `thenM_`
1943 -- Deal with ambiguity errors, but only if
1944 -- if there has not been an error so far; errors often
1945 -- give rise to spurious ambiguous Insts
1946 ifErrsM (returnM []) (
1948 -- Complain about the ones that don't fall under
1949 -- the Haskell rules for disambiguation
1950 -- This group includes both non-existent instances
1951 -- e.g. Num (IO a) and Eq (Int -> Int)
1952 -- and ambiguous dictionaries
1954 addTopAmbigErrs ambigs `thenM_`
1956 -- Disambiguate the ones that look feasible
1957 mappM (disambigGroup is_interactive) std_oks
1958 ) `thenM` \ binds_ambig ->
1960 returnM (binds `unionBags` unionManyBags binds_ambig)
1962 ----------------------------------
1963 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1965 get_tv d = case getDictClassTys d of
1966 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1967 get_clas d = case getDictClassTys d of
1968 (clas, [ty]) -> clas
1971 If a dictionary constrains a type variable which is
1972 * not mentioned in the environment
1973 * and not mentioned in the type of the expression
1974 then it is ambiguous. No further information will arise to instantiate
1975 the type variable; nor will it be generalised and turned into an extra
1976 parameter to a function.
1978 It is an error for this to occur, except that Haskell provided for
1979 certain rules to be applied in the special case of numeric types.
1981 * at least one of its classes is a numeric class, and
1982 * all of its classes are numeric or standard
1983 then the type variable can be defaulted to the first type in the
1984 default-type list which is an instance of all the offending classes.
1986 So here is the function which does the work. It takes the ambiguous
1987 dictionaries and either resolves them (producing bindings) or
1988 complains. It works by splitting the dictionary list by type
1989 variable, and using @disambigOne@ to do the real business.
1991 @disambigOne@ assumes that its arguments dictionaries constrain all
1992 the same type variable.
1994 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1995 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1996 the most common use of defaulting is code like:
1998 _ccall_ foo `seqPrimIO` bar
2000 Since we're not using the result of @foo@, the result if (presumably)
2004 disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
2005 -> [Inst] -- All standard classes of form (C a)
2008 disambigGroup is_interactive dicts
2009 | any std_default_class classes -- Guaranteed all standard classes
2010 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2011 -- SO, TRY DEFAULT TYPES IN ORDER
2013 -- Failure here is caused by there being no type in the
2014 -- default list which can satisfy all the ambiguous classes.
2015 -- For example, if Real a is reqd, but the only type in the
2016 -- default list is Int.
2017 get_default_tys `thenM` \ default_tys ->
2019 try_default [] -- No defaults work, so fail
2022 try_default (default_ty : default_tys)
2023 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2024 -- default_tys instead
2025 tcSimplifyDefault theta `thenM` \ _ ->
2028 theta = [mkClassPred clas [default_ty] | clas <- classes]
2030 -- See if any default works
2031 tryM (try_default default_tys) `thenM` \ mb_ty ->
2034 Right chosen_default_ty -> choose_default chosen_default_ty
2036 | otherwise -- No defaults
2040 tyvar = get_tv (head dicts) -- Should be non-empty
2041 classes = map get_clas dicts
2043 std_default_class cls
2044 = isNumericClass cls
2045 || (is_interactive &&
2046 classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2047 -- In interactive mode, we default Show a to Show ()
2048 -- to avoid graututious errors on "show []"
2050 choose_default default_ty -- Commit to tyvar = default_ty
2051 = -- Bind the type variable
2052 unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
2053 -- and reduce the context, for real this time
2054 simpleReduceLoop (text "disambig" <+> ppr dicts)
2055 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2056 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2057 warnDefault dicts default_ty `thenM_`
2060 bomb_out = addTopAmbigErrs dicts `thenM_`
2064 = do { mb_defaults <- getDefaultTys
2065 ; case mb_defaults of
2066 Just tys -> return tys
2067 Nothing -> -- No use-supplied default;
2068 -- use [Integer, Double]
2069 do { integer_ty <- tcMetaTy integerTyConName
2070 ; return [integer_ty, doubleTy] } }
2073 [Aside - why the defaulting mechanism is turned off when
2074 dealing with arguments and results to ccalls.
2076 When typechecking _ccall_s, TcExpr ensures that the external
2077 function is only passed arguments (and in the other direction,
2078 results) of a restricted set of 'native' types. This is
2079 implemented via the help of the pseudo-type classes,
2080 @CReturnable@ (CR) and @CCallable@ (CC.)
2082 The interaction between the defaulting mechanism for numeric
2083 values and CC & CR can be a bit puzzling to the user at times.
2092 What type has 'x' got here? That depends on the default list
2093 in operation, if it is equal to Haskell 98's default-default
2094 of (Integer, Double), 'x' has type Double, since Integer
2095 is not an instance of CR. If the default list is equal to
2096 Haskell 1.4's default-default of (Int, Double), 'x' has type
2099 To try to minimise the potential for surprises here, the
2100 defaulting mechanism is turned off in the presence of
2101 CCallable and CReturnable.
2106 %************************************************************************
2108 \subsection[simple]{@Simple@ versions}
2110 %************************************************************************
2112 Much simpler versions when there are no bindings to make!
2114 @tcSimplifyThetas@ simplifies class-type constraints formed by
2115 @deriving@ declarations and when specialising instances. We are
2116 only interested in the simplified bunch of class/type constraints.
2118 It simplifies to constraints of the form (C a b c) where
2119 a,b,c are type variables. This is required for the context of
2120 instance declarations.
2123 tcSimplifyDeriv :: [TyVar]
2124 -> ThetaType -- Wanted
2125 -> TcM ThetaType -- Needed
2127 tcSimplifyDeriv tyvars theta
2128 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2129 -- The main loop may do unification, and that may crash if
2130 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2131 -- ToDo: what if two of them do get unified?
2132 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2133 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2134 ASSERT( null frees ) -- reduceMe never returns Free
2136 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2138 tv_set = mkVarSet tvs
2140 (bad_insts, ok_insts) = partition is_bad_inst irreds
2142 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2143 in isEmptyVarSet (tyVarsOfPred pred)
2144 -- Things like (Eq T) are bad
2145 || (not undecidable_ok && not (isTyVarClassPred pred))
2146 -- The returned dictionaries should be of form (C a b)
2147 -- (where a, b are type variables).
2148 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
2149 -- but note that risks non-termination in the 'deriving' context-inference
2150 -- fixpoint loop. It is useful for situations like
2151 -- data Min h a = E | M a (h a)
2152 -- which gives the instance decl
2153 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
2155 simpl_theta = map dictPred ok_insts
2156 weird_preds = [pred | pred <- simpl_theta
2157 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2158 -- Check for a bizarre corner case, when the derived instance decl should
2159 -- have form instance C a b => D (T a) where ...
2160 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2161 -- of problems; in particular, it's hard to compare solutions for
2162 -- equality when finding the fixpoint. So I just rule it out for now.
2164 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2165 -- This reverse-mapping is a Royal Pain,
2166 -- but the result should mention TyVars not TcTyVars
2169 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2170 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2171 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2172 returnM (substTheta rev_env simpl_theta)
2174 doc = ptext SLIT("deriving classes for a data type")
2177 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2178 used with \tr{default} declarations. We are only interested in
2179 whether it worked or not.
2182 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2185 tcSimplifyDefault theta
2186 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2187 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2188 ASSERT( null frees ) -- try_me never returns Free
2189 addNoInstanceErrs Nothing [] irreds `thenM_`
2195 doc = ptext SLIT("default declaration")
2199 %************************************************************************
2201 \section{Errors and contexts}
2203 %************************************************************************
2205 ToDo: for these error messages, should we note the location as coming
2206 from the insts, or just whatever seems to be around in the monad just
2210 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2211 -> [Inst] -- The offending Insts
2213 -- Group together insts with the same origin
2214 -- We want to report them together in error messages
2216 groupErrs report_err []
2218 groupErrs report_err (inst:insts)
2219 = do_one (inst:friends) `thenM_`
2220 groupErrs report_err others
2223 -- (It may seem a bit crude to compare the error messages,
2224 -- but it makes sure that we combine just what the user sees,
2225 -- and it avoids need equality on InstLocs.)
2226 (friends, others) = partition is_friend insts
2227 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2228 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2229 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2230 -- Add location and context information derived from the Insts
2232 -- Add the "arising from..." part to a message about bunch of dicts
2233 addInstLoc :: [Inst] -> Message -> Message
2234 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2237 plural xs = char 's'
2240 = groupErrs report tidy_dicts
2242 (tidy_env, tidy_dicts) = tidyInsts dicts
2243 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2244 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2245 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2247 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2248 -- Just d => d describes the construct
2249 -> [Inst] -- What is given by the context or type sig
2250 -> [Inst] -- What is wanted
2252 addNoInstanceErrs mb_what givens []
2254 addNoInstanceErrs mb_what givens dicts
2255 = -- Some of the dicts are here because there is no instances
2256 -- and some because there are too many instances (overlap)
2257 -- The first thing we do is separate them
2258 getDOpts `thenM` \ dflags ->
2259 tcGetInstEnvs `thenM` \ inst_envs ->
2261 (tidy_env1, tidy_givens) = tidyInsts givens
2262 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2264 -- Run through the dicts, generating a message for each
2265 -- overlapping one, but simply accumulating all the
2266 -- no-instance ones so they can be reported as a group
2267 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2268 check_overlap (overlap_doc, no_inst_dicts) dict
2269 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2271 = case lookupInstEnv dflags inst_envs clas tys of
2272 -- The case of exactly one match and no unifiers means
2273 -- a successful lookup. That can't happen here.
2275 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2277 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2278 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2280 (clas,tys) = getDictClassTys dict
2283 -- Now generate a good message for the no-instance bunch
2284 mk_probable_fix tidy_env2 mb_what no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2286 no_inst_doc | null no_inst_dicts = empty
2287 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2288 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2289 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2290 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2291 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2293 -- And emit both the non-instance and overlap messages
2294 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2296 mk_overlap_msg dict (matches, unifiers)
2297 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2298 <+> pprPred (dictPred dict))),
2299 sep [ptext SLIT("Matching instances") <> colon,
2300 nest 2 (pprDFuns (dfuns ++ unifiers))],
2301 ASSERT( not (null matches) )
2302 if not (isSingleton matches)
2303 then -- Two or more matches
2305 else -- One match, plus some unifiers
2306 ASSERT( not (null unifiers) )
2307 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2308 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2309 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2311 dfuns = [df | (_, (_,_,df)) <- matches]
2313 mk_probable_fix tidy_env Nothing dicts -- Top level
2314 = mkMonomorphismMsg tidy_env dicts
2315 mk_probable_fix tidy_env (Just what) dicts -- Nested (type signatures, instance decls)
2316 = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 fix1, nest 2 fix2])
2318 fix1 = sep [ptext SLIT("Add") <+> pprDictsTheta dicts,
2319 ptext SLIT("to the") <+> what]
2321 fix2 | null instance_dicts = empty
2322 | otherwise = ptext SLIT("Or add an instance declaration for")
2323 <+> pprDictsTheta instance_dicts
2324 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2325 -- Insts for which it is worth suggesting an adding an instance declaration
2326 -- Exclude implicit parameters, and tyvar dicts
2329 addTopAmbigErrs dicts
2330 -- Divide into groups that share a common set of ambiguous tyvars
2331 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2333 (tidy_env, tidy_dicts) = tidyInsts dicts
2335 tvs_of :: Inst -> [TcTyVar]
2336 tvs_of d = varSetElems (tyVarsOfInst d)
2337 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2339 report :: [(Inst,[TcTyVar])] -> TcM ()
2340 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2341 = mkMonomorphismMsg tidy_env dicts `thenM` \ (tidy_env, mono_msg) ->
2342 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2343 -- the location of the first one will do for the err message
2344 addErrTcM (tidy_env, msg $$ mono_msg)
2346 dicts = map fst pairs
2347 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2348 pprQuotedList tvs <+> in_msg,
2349 nest 2 (pprDictsInFull dicts)]
2350 in_msg | isSingleton dicts = text "in the top-level constraint:"
2351 | otherwise = text "in these top-level constraints:"
2354 mkMonomorphismMsg :: TidyEnv -> [Inst] -> TcM (TidyEnv, Message)
2355 -- There's an error with these Insts; if they have free type variables
2356 -- it's probably caused by the monomorphism restriction.
2357 -- Try to identify the offending variable
2358 -- ASSUMPTION: the Insts are fully zonked
2359 mkMonomorphismMsg tidy_env insts
2360 | isEmptyVarSet inst_tvs
2361 = returnM (tidy_env, empty)
2363 = findGlobals inst_tvs tidy_env `thenM` \ (tidy_env, docs) ->
2364 returnM (tidy_env, mk_msg docs)
2367 inst_tvs = tyVarsOfInsts insts
2369 mk_msg [] = empty -- This happens in things like
2370 -- f x = show (read "foo")
2371 -- whre monomorphism doesn't play any role
2372 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2374 ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
2376 warnDefault dicts default_ty
2377 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2378 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2381 (_, tidy_dicts) = tidyInsts dicts
2382 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2383 quotes (ppr default_ty),
2384 pprDictsInFull tidy_dicts]
2386 -- Used for the ...Thetas variants; all top level
2388 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2389 ptext SLIT("type variables that are not data type parameters"),
2390 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2392 reduceDepthErr n stack
2393 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2394 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2395 nest 4 (pprStack stack)]
2397 pprStack stack = vcat (map pprInstInFull stack)