2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyRuleLhs, tcSimplifyIPs,
13 tcSimplifySuperClasses,
14 tcSimplifyTop, tcSimplifyInteractive,
17 tcSimplifyDeriv, tcSimplifyDefault,
21 #include "HsVersions.h"
23 import {-# SOURCE #-} TcUnify( unifyType )
24 import TypeRep ( Type(..) )
25 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
26 import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp )
29 import Inst ( lookupInst, LookupInstResult(..),
30 tyVarsOfInst, fdPredsOfInsts, newDicts,
31 isDict, isClassDict, isLinearInst, linearInstType,
32 isMethodFor, isMethod,
33 instToId, tyVarsOfInsts, cloneDict,
34 ipNamesOfInsts, ipNamesOfInst, dictPred,
36 newDictsAtLoc, tcInstClassOp,
37 getDictClassTys, isTyVarDict, instLoc,
38 zonkInst, tidyInsts, tidyMoreInsts,
39 pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
40 isInheritableInst, pprDictsTheta
42 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
43 lclEnvElts, tcMetaTy )
44 import InstEnv ( lookupInstEnv, classInstances, pprInstances )
45 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType )
46 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
47 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
48 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
49 tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
50 import TcIface ( checkWiredInTyCon )
51 import Id ( idType, mkUserLocal )
53 import TyCon ( TyCon )
54 import Name ( Name, getOccName, getSrcLoc )
55 import NameSet ( NameSet, mkNameSet, elemNameSet )
56 import Class ( classBigSig, classKey )
57 import FunDeps ( oclose, grow, improve, pprEquation )
58 import PrelInfo ( isNumericClass, isStandardClass )
59 import PrelNames ( splitName, fstName, sndName, integerTyConName,
60 showClassKey, eqClassKey, ordClassKey )
61 import Type ( zipTopTvSubst, substTheta, substTy )
62 import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
63 import ErrUtils ( Message )
64 import BasicTypes ( TopLevelFlag, isNotTopLevel )
66 import VarEnv ( TidyEnv )
70 import ListSetOps ( equivClasses )
71 import Util ( zipEqual, isSingleton )
72 import List ( partition )
73 import SrcLoc ( Located(..) )
74 import DynFlags ( DynFlag(..) )
79 %************************************************************************
83 %************************************************************************
85 --------------------------------------
86 Notes on functional dependencies (a bug)
87 --------------------------------------
89 | > class Foo a b | a->b
91 | > class Bar a b | a->b
95 | > instance Bar Obj Obj
97 | > instance (Bar a b) => Foo a b
99 | > foo:: (Foo a b) => a -> String
102 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
108 | Could not deduce (Bar a b) from the context (Foo a b)
109 | arising from use of `foo' at <interactive>:1
111 | Add (Bar a b) to the expected type of an expression
112 | In the first argument of `runFoo', namely `foo'
113 | In the definition of `it': it = runFoo foo
115 | Why all of the sudden does GHC need the constraint Bar a b? The
116 | function foo didn't ask for that...
118 The trouble is that to type (runFoo foo), GHC has to solve the problem:
120 Given constraint Foo a b
121 Solve constraint Foo a b'
123 Notice that b and b' aren't the same. To solve this, just do
124 improvement and then they are the same. But GHC currently does
129 That is usually fine, but it isn't here, because it sees that Foo a b is
130 not the same as Foo a b', and so instead applies the instance decl for
131 instance Bar a b => Foo a b. And that's where the Bar constraint comes
134 The Right Thing is to improve whenever the constraint set changes at
135 all. Not hard in principle, but it'll take a bit of fiddling to do.
139 --------------------------------------
140 Notes on quantification
141 --------------------------------------
143 Suppose we are about to do a generalisation step.
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
168 environment. (B) says we must quantify over all the truly free
169 variables in T, else we won't get a sufficiently general type. We do
170 not *need* to quantify over any variable that is fixed by the free
171 vars of the environment G.
173 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
175 Example: class H x y | x->y where ...
177 fv(G) = {a} C = {H a b, H c d}
180 (A) Q intersect {a} is empty
181 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
183 So Q can be {c,d}, {b,c,d}
185 Other things being equal, however, we'd like to quantify over as few
186 variables as possible: smaller types, fewer type applications, more
187 constraints can get into Ct instead of Cq.
190 -----------------------------------------
193 fv(T) the free type vars of T
195 oclose(vs,C) The result of extending the set of tyvars vs
196 using the functional dependencies from C
198 grow(vs,C) The result of extend the set of tyvars vs
199 using all conceivable links from C.
201 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
202 Then grow(vs,C) = {a,b,c}
204 Note that grow(vs,C) `superset` grow(vs,simplify(C))
205 That is, simplfication can only shrink the result of grow.
208 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
209 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
212 -----------------------------------------
216 Here's a good way to choose Q:
218 Q = grow( fv(T), C ) \ oclose( fv(G), C )
220 That is, quantify over all variable that that MIGHT be fixed by the
221 call site (which influences T), but which aren't DEFINITELY fixed by
222 G. This choice definitely quantifies over enough type variables,
223 albeit perhaps too many.
225 Why grow( fv(T), C ) rather than fv(T)? Consider
227 class H x y | x->y where ...
232 If we used fv(T) = {c} we'd get the type
234 forall c. H c d => c -> b
236 And then if the fn was called at several different c's, each of
237 which fixed d differently, we'd get a unification error, because
238 d isn't quantified. Solution: quantify d. So we must quantify
239 everything that might be influenced by c.
241 Why not oclose( fv(T), C )? Because we might not be able to see
242 all the functional dependencies yet:
244 class H x y | x->y where ...
245 instance H x y => Eq (T x y) where ...
250 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
251 apparent yet, and that's wrong. We must really quantify over d too.
254 There really isn't any point in quantifying over any more than
255 grow( fv(T), C ), because the call sites can't possibly influence
256 any other type variables.
260 --------------------------------------
262 --------------------------------------
264 It's very hard to be certain when a type is ambiguous. Consider
268 instance H x y => K (x,y)
270 Is this type ambiguous?
271 forall a b. (K (a,b), Eq b) => a -> a
273 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
274 now we see that a fixes b. So we can't tell about ambiguity for sure
275 without doing a full simplification. And even that isn't possible if
276 the context has some free vars that may get unified. Urgle!
278 Here's another example: is this ambiguous?
279 forall a b. Eq (T b) => a -> a
280 Not if there's an insance decl (with no context)
281 instance Eq (T b) where ...
283 You may say of this example that we should use the instance decl right
284 away, but you can't always do that:
286 class J a b where ...
287 instance J Int b where ...
289 f :: forall a b. J a b => a -> a
291 (Notice: no functional dependency in J's class decl.)
292 Here f's type is perfectly fine, provided f is only called at Int.
293 It's premature to complain when meeting f's signature, or even
294 when inferring a type for f.
298 However, we don't *need* to report ambiguity right away. It'll always
299 show up at the call site.... and eventually at main, which needs special
300 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
302 So here's the plan. We WARN about probable ambiguity if
304 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
306 (all tested before quantification).
307 That is, all the type variables in Cq must be fixed by the the variables
308 in the environment, or by the variables in the type.
310 Notice that we union before calling oclose. Here's an example:
312 class J a b c | a b -> c
316 forall b c. (J a b c) => b -> b
318 Only if we union {a} from G with {b} from T before using oclose,
319 do we see that c is fixed.
321 It's a bit vague exactly which C we should use for this oclose call. If we
322 don't fix enough variables we might complain when we shouldn't (see
323 the above nasty example). Nothing will be perfect. That's why we can
324 only issue a warning.
327 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
329 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
331 then c is a "bubble"; there's no way it can ever improve, and it's
332 certainly ambiguous. UNLESS it is a constant (sigh). And what about
337 instance H x y => K (x,y)
339 Is this type ambiguous?
340 forall a b. (K (a,b), Eq b) => a -> a
342 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
343 is a "bubble" that's a set of constraints
345 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
347 Hence another idea. To decide Q start with fv(T) and grow it
348 by transitive closure in Cq (no functional dependencies involved).
349 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
350 The definitely-ambiguous can then float out, and get smashed at top level
351 (which squashes out the constants, like Eq (T a) above)
354 --------------------------------------
355 Notes on principal types
356 --------------------------------------
361 f x = let g y = op (y::Int) in True
363 Here the principal type of f is (forall a. a->a)
364 but we'll produce the non-principal type
365 f :: forall a. C Int => a -> a
368 --------------------------------------
369 The need for forall's in constraints
370 --------------------------------------
372 [Exchange on Haskell Cafe 5/6 Dec 2000]
374 class C t where op :: t -> Bool
375 instance C [t] where op x = True
377 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
378 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
380 The definitions of p and q differ only in the order of the components in
381 the pair on their right-hand sides. And yet:
383 ghc and "Typing Haskell in Haskell" reject p, but accept q;
384 Hugs rejects q, but accepts p;
385 hbc rejects both p and q;
386 nhc98 ... (Malcolm, can you fill in the blank for us!).
388 The type signature for f forces context reduction to take place, and
389 the results of this depend on whether or not the type of y is known,
390 which in turn depends on which component of the pair the type checker
393 Solution: if y::m a, float out the constraints
394 Monad m, forall c. C (m c)
395 When m is later unified with [], we can solve both constraints.
398 --------------------------------------
399 Notes on implicit parameters
400 --------------------------------------
402 Question 1: can we "inherit" implicit parameters
403 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
408 where f is *not* a top-level binding.
409 From the RHS of f we'll get the constraint (?y::Int).
410 There are two types we might infer for f:
414 (so we get ?y from the context of f's definition), or
416 f :: (?y::Int) => Int -> Int
418 At first you might think the first was better, becuase then
419 ?y behaves like a free variable of the definition, rather than
420 having to be passed at each call site. But of course, the WHOLE
421 IDEA is that ?y should be passed at each call site (that's what
422 dynamic binding means) so we'd better infer the second.
424 BOTTOM LINE: when *inferring types* you *must* quantify
425 over implicit parameters. See the predicate isFreeWhenInferring.
428 Question 2: type signatures
429 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
430 BUT WATCH OUT: When you supply a type signature, we can't force you
431 to quantify over implicit parameters. For example:
435 This is perfectly reasonable. We do not want to insist on
437 (?x + 1) :: (?x::Int => Int)
439 That would be silly. Here, the definition site *is* the occurrence site,
440 so the above strictures don't apply. Hence the difference between
441 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
442 and tcSimplifyCheckBind (which does not).
444 What about when you supply a type signature for a binding?
445 Is it legal to give the following explicit, user type
446 signature to f, thus:
451 At first sight this seems reasonable, but it has the nasty property
452 that adding a type signature changes the dynamic semantics.
455 (let f x = (x::Int) + ?y
456 in (f 3, f 3 with ?y=5)) with ?y = 6
462 in (f 3, f 3 with ?y=5)) with ?y = 6
466 Indeed, simply inlining f (at the Haskell source level) would change the
469 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
470 semantics for a Haskell program without knowing its typing, so if you
471 change the typing you may change the semantics.
473 To make things consistent in all cases where we are *checking* against
474 a supplied signature (as opposed to inferring a type), we adopt the
477 a signature does not need to quantify over implicit params.
479 [This represents a (rather marginal) change of policy since GHC 5.02,
480 which *required* an explicit signature to quantify over all implicit
481 params for the reasons mentioned above.]
483 But that raises a new question. Consider
485 Given (signature) ?x::Int
486 Wanted (inferred) ?x::Int, ?y::Bool
488 Clearly we want to discharge the ?x and float the ?y out. But
489 what is the criterion that distinguishes them? Clearly it isn't
490 what free type variables they have. The Right Thing seems to be
491 to float a constraint that
492 neither mentions any of the quantified type variables
493 nor any of the quantified implicit parameters
495 See the predicate isFreeWhenChecking.
498 Question 3: monomorphism
499 ~~~~~~~~~~~~~~~~~~~~~~~~
500 There's a nasty corner case when the monomorphism restriction bites:
504 The argument above suggests that we *must* generalise
505 over the ?y parameter, to get
506 z :: (?y::Int) => Int,
507 but the monomorphism restriction says that we *must not*, giving
509 Why does the momomorphism restriction say this? Because if you have
511 let z = x + ?y in z+z
513 you might not expect the addition to be done twice --- but it will if
514 we follow the argument of Question 2 and generalise over ?y.
517 Question 4: top level
518 ~~~~~~~~~~~~~~~~~~~~~
519 At the top level, monomorhism makes no sense at all.
522 main = let ?x = 5 in print foo
526 woggle :: (?x :: Int) => Int -> Int
529 We definitely don't want (foo :: Int) with a top-level implicit parameter
530 (?x::Int) becuase there is no way to bind it.
535 (A) Always generalise over implicit parameters
536 Bindings that fall under the monomorphism restriction can't
540 * Inlining remains valid
541 * No unexpected loss of sharing
542 * But simple bindings like
544 will be rejected, unless you add an explicit type signature
545 (to avoid the monomorphism restriction)
546 z :: (?y::Int) => Int
548 This seems unacceptable
550 (B) Monomorphism restriction "wins"
551 Bindings that fall under the monomorphism restriction can't
553 Always generalise over implicit parameters *except* for bindings
554 that fall under the monomorphism restriction
557 * Inlining isn't valid in general
558 * No unexpected loss of sharing
559 * Simple bindings like
561 accepted (get value of ?y from binding site)
563 (C) Always generalise over implicit parameters
564 Bindings that fall under the monomorphism restriction can't
565 be generalised, EXCEPT for implicit parameters
567 * Inlining remains valid
568 * Unexpected loss of sharing (from the extra generalisation)
569 * Simple bindings like
571 accepted (get value of ?y from occurrence sites)
576 None of these choices seems very satisfactory. But at least we should
577 decide which we want to do.
579 It's really not clear what is the Right Thing To Do. If you see
583 would you expect the value of ?y to be got from the *occurrence sites*
584 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
585 case of function definitions, the answer is clearly the former, but
586 less so in the case of non-fucntion definitions. On the other hand,
587 if we say that we get the value of ?y from the definition site of 'z',
588 then inlining 'z' might change the semantics of the program.
590 Choice (C) really says "the monomorphism restriction doesn't apply
591 to implicit parameters". Which is fine, but remember that every
592 innocent binding 'x = ...' that mentions an implicit parameter in
593 the RHS becomes a *function* of that parameter, called at each
594 use of 'x'. Now, the chances are that there are no intervening 'with'
595 clauses that bind ?y, so a decent compiler should common up all
596 those function calls. So I think I strongly favour (C). Indeed,
597 one could make a similar argument for abolishing the monomorphism
598 restriction altogether.
600 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
604 %************************************************************************
606 \subsection{tcSimplifyInfer}
608 %************************************************************************
610 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
612 1. Compute Q = grow( fvs(T), C )
614 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
615 predicates will end up in Ct; we deal with them at the top level
617 3. Try improvement, using functional dependencies
619 4. If Step 3 did any unification, repeat from step 1
620 (Unification can change the result of 'grow'.)
622 Note: we don't reduce dictionaries in step 2. For example, if we have
623 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
624 after step 2. However note that we may therefore quantify over more
625 type variables than we absolutely have to.
627 For the guts, we need a loop, that alternates context reduction and
628 improvement with unification. E.g. Suppose we have
630 class C x y | x->y where ...
632 and tcSimplify is called with:
634 Then improvement unifies a with b, giving
637 If we need to unify anything, we rattle round the whole thing all over
644 -> TcTyVarSet -- fv(T); type vars
646 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
647 TcDictBinds, -- Bindings
648 [TcId]) -- Dict Ids that must be bound here (zonked)
649 -- Any free (escaping) Insts are tossed into the environment
654 tcSimplifyInfer doc tau_tvs wanted_lie
655 = inferLoop doc (varSetElems tau_tvs)
656 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
658 extendLIEs frees `thenM_`
659 returnM (qtvs, binds, map instToId irreds)
661 inferLoop doc tau_tvs wanteds
663 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
664 mappM zonkInst wanteds `thenM` \ wanteds' ->
665 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
667 preds = fdPredsOfInsts wanteds'
668 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
671 | isFreeWhenInferring qtvs inst = Free
672 | isClassDict inst = DontReduceUnlessConstant -- Dicts
673 | otherwise = ReduceMe NoSCs -- Lits and Methods
675 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
676 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
678 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
681 if no_improvement then
682 returnM (varSetElems qtvs, frees, binds, irreds)
684 -- If improvement did some unification, we go round again. There
685 -- are two subtleties:
686 -- a) We start again with irreds, not wanteds
687 -- Using an instance decl might have introduced a fresh type variable
688 -- which might have been unified, so we'd get an infinite loop
689 -- if we started again with wanteds! See example [LOOP]
691 -- b) It's also essential to re-process frees, because unification
692 -- might mean that a type variable that looked free isn't now.
694 -- Hence the (irreds ++ frees)
696 -- However, NOTICE that when we are done, we might have some bindings, but
697 -- the final qtvs might be empty. See [NO TYVARS] below.
699 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
700 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
705 class If b t e r | b t e -> r
708 class Lte a b c | a b -> c where lte :: a -> b -> c
710 instance (Lte a b l,If l b a c) => Max a b c
712 Wanted: Max Z (S x) y
714 Then we'll reduce using the Max instance to:
715 (Lte Z (S x) l, If l (S x) Z y)
716 and improve by binding l->T, after which we can do some reduction
717 on both the Lte and If constraints. What we *can't* do is start again
718 with (Max Z (S x) y)!
722 class Y a b | a -> b where
725 instance Y [[a]] a where
728 k :: X a -> X a -> X a
730 g :: Num a => [X a] -> [X a]
733 h ys = ys ++ map (k (y [[0]])) xs
735 The excitement comes when simplifying the bindings for h. Initially
736 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
737 From this we get t1:=:t2, but also various bindings. We can't forget
738 the bindings (because of [LOOP]), but in fact t1 is what g is
741 The net effect of [NO TYVARS]
744 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
745 isFreeWhenInferring qtvs inst
746 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
747 && isInheritableInst inst -- And no implicit parameter involved
748 -- (see "Notes on implicit parameters")
750 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
751 -> NameSet -- Quantified implicit parameters
753 isFreeWhenChecking qtvs ips inst
754 = isFreeWrtTyVars qtvs inst
755 && isFreeWrtIPs ips inst
757 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
758 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
762 %************************************************************************
764 \subsection{tcSimplifyCheck}
766 %************************************************************************
768 @tcSimplifyCheck@ is used when we know exactly the set of variables
769 we are going to quantify over. For example, a class or instance declaration.
774 -> [TcTyVar] -- Quantify over these
777 -> TcM TcDictBinds -- Bindings
779 -- tcSimplifyCheck is used when checking expression type signatures,
780 -- class decls, instance decls etc.
782 -- NB: tcSimplifyCheck does not consult the
783 -- global type variables in the environment; so you don't
784 -- need to worry about setting them before calling tcSimplifyCheck
785 tcSimplifyCheck doc qtvs givens wanted_lie
786 = ASSERT( all isSkolemTyVar qtvs )
787 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
791 -- get_qtvs = zonkTcTyVarsAndFV qtvs
792 get_qtvs = return (mkVarSet qtvs) -- All skolems
795 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
796 -- against, but we don't know the type variables over which we are going to quantify.
797 -- This happens when we have a type signature for a mutually recursive group
800 -> TcTyVarSet -- fv(T)
803 -> TcM ([TcTyVar], -- Variables over which to quantify
804 TcDictBinds) -- Bindings
806 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
807 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
809 ; return (qtvs', binds) }
811 -- Figure out which type variables to quantify over
812 -- You might think it should just be the signature tyvars,
813 -- but in bizarre cases you can get extra ones
814 -- f :: forall a. Num a => a -> a
815 -- f x = fst (g (x, head [])) + 1
817 -- Here we infer g :: forall a b. a -> b -> (b,a)
818 -- We don't want g to be monomorphic in b just because
819 -- f isn't quantified over b.
820 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
822 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
823 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
825 qtvs = all_tvs' `minusVarSet` gbl_tvs
826 -- We could close gbl_tvs, but its not necessary for
827 -- soundness, and it'll only affect which tyvars, not which
828 -- dictionaries, we quantify over
833 Here is the workhorse function for all three wrappers.
836 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
837 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
839 -- Complain about any irreducible ones
840 ; if not (null irreds)
841 then do { givens' <- mappM zonkInst given_dicts_and_ips
842 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
845 ; returnM (qtvs, frees, binds) }
847 given_dicts_and_ips = filter (not . isMethod) givens
848 -- For error reporting, filter out methods, which are
849 -- only added to the given set as an optimisation
851 ip_set = mkNameSet (ipNamesOfInsts givens)
853 check_loop givens wanteds
855 mappM zonkInst givens `thenM` \ givens' ->
856 mappM zonkInst wanteds `thenM` \ wanteds' ->
857 get_qtvs `thenM` \ qtvs' ->
861 -- When checking against a given signature we always reduce
862 -- until we find a match against something given, or can't reduce
863 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
864 | otherwise = ReduceMe want_scs
866 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
869 if no_improvement then
870 returnM (varSetElems qtvs', frees, binds, irreds)
872 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
873 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
877 %************************************************************************
879 tcSimplifySuperClasses
881 %************************************************************************
883 Note [SUPERCLASS-LOOP 1]
884 ~~~~~~~~~~~~~~~~~~~~~~~~
885 We have to be very, very careful when generating superclasses, lest we
886 accidentally build a loop. Here's an example:
890 class S a => C a where { opc :: a -> a }
891 class S b => D b where { opd :: b -> b }
899 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
900 Simplifying, we may well get:
901 $dfCInt = :C ds1 (opd dd)
904 Notice that we spot that we can extract ds1 from dd.
906 Alas! Alack! We can do the same for (instance D Int):
908 $dfDInt = :D ds2 (opc dc)
912 And now we've defined the superclass in terms of itself.
914 Solution: never generate a superclass selectors at all when
915 satisfying the superclass context of an instance declaration.
917 Two more nasty cases are in
922 tcSimplifySuperClasses qtvs givens sc_wanteds
923 = ASSERT( all isSkolemTyVar qtvs )
924 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
925 ; binds2 <- tc_simplify_top doc False NoSCs frees
926 ; return (binds1 `unionBags` binds2) }
928 get_qtvs = return (mkVarSet qtvs)
929 doc = ptext SLIT("instance declaration superclass context")
933 %************************************************************************
935 \subsection{tcSimplifyRestricted}
937 %************************************************************************
939 tcSimplifyRestricted infers which type variables to quantify for a
940 group of restricted bindings. This isn't trivial.
943 We want to quantify over a to get id :: forall a. a->a
946 We do not want to quantify over a, because there's an Eq a
947 constraint, so we get eq :: a->a->Bool (notice no forall)
950 RHS has type 'tau', whose free tyvars are tau_tvs
951 RHS has constraints 'wanteds'
954 Quantify over (tau_tvs \ ftvs(wanteds))
955 This is bad. The constraints may contain (Monad (ST s))
956 where we have instance Monad (ST s) where...
957 so there's no need to be monomorphic in s!
959 Also the constraint might be a method constraint,
960 whose type mentions a perfectly innocent tyvar:
961 op :: Num a => a -> b -> a
962 Here, b is unconstrained. A good example would be
964 We want to infer the polymorphic type
965 foo :: forall b. b -> b
968 Plan B (cunning, used for a long time up to and including GHC 6.2)
969 Step 1: Simplify the constraints as much as possible (to deal
970 with Plan A's problem). Then set
971 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
973 Step 2: Now simplify again, treating the constraint as 'free' if
974 it does not mention qtvs, and trying to reduce it otherwise.
975 The reasons for this is to maximise sharing.
977 This fails for a very subtle reason. Suppose that in the Step 2
978 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
979 In the Step 1 this constraint might have been simplified, perhaps to
980 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
981 This won't happen in Step 2... but that in turn might prevent some other
982 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
983 and that in turn breaks the invariant that no constraints are quantified over.
985 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
990 Step 1: Simplify the constraints as much as possible (to deal
991 with Plan A's problem). Then set
992 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
993 Return the bindings from Step 1.
996 A note about Plan C (arising from "bug" reported by George Russel March 2004)
999 instance (HasBinary ty IO) => HasCodedValue ty
1001 foo :: HasCodedValue a => String -> IO a
1003 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1004 doDecodeIO codedValue view
1005 = let { act = foo "foo" } in act
1007 You might think this should work becuase the call to foo gives rise to a constraint
1008 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1009 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1010 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1012 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1016 Plan D (a variant of plan B)
1017 Step 1: Simplify the constraints as much as possible (to deal
1018 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1019 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1021 Step 2: Now simplify again, treating the constraint as 'free' if
1022 it does not mention qtvs, and trying to reduce it otherwise.
1024 The point here is that it's generally OK to have too few qtvs; that is,
1025 to make the thing more monomorphic than it could be. We don't want to
1026 do that in the common cases, but in wierd cases it's ok: the programmer
1027 can always add a signature.
1029 Too few qtvs => too many wanteds, which is what happens if you do less
1034 tcSimplifyRestricted -- Used for restricted binding groups
1035 -- i.e. ones subject to the monomorphism restriction
1038 -> [Name] -- Things bound in this group
1039 -> TcTyVarSet -- Free in the type of the RHSs
1040 -> [Inst] -- Free in the RHSs
1041 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1042 TcDictBinds) -- Bindings
1043 -- tcSimpifyRestricted returns no constraints to
1044 -- quantify over; by definition there are none.
1045 -- They are all thrown back in the LIE
1047 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1048 -- Zonk everything in sight
1049 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1050 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1051 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1053 -- 'reduceMe': Reduce as far as we can. Don't stop at
1054 -- dicts; the idea is to get rid of as many type
1055 -- variables as possible, and we don't want to stop
1056 -- at (say) Monad (ST s), because that reduces
1057 -- immediately, with no constraint on s.
1059 -- BUT do no improvement! See Plan D above
1060 reduceContextWithoutImprovement
1061 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1063 -- Next, figure out the tyvars we will quantify over
1065 constrained_tvs = tyVarsOfInsts constrained_dicts
1066 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1067 `minusVarSet` constrained_tvs
1069 traceTc (text "tcSimplifyRestricted" <+> vcat [
1070 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1072 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1074 -- The first step may have squashed more methods than
1075 -- necessary, so try again, this time more gently, knowing the exact
1076 -- set of type variables to quantify over.
1078 -- We quantify only over constraints that are captured by qtvs;
1079 -- these will just be a subset of non-dicts. This in contrast
1080 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1081 -- all *non-inheritable* constraints too. This implements choice
1082 -- (B) under "implicit parameter and monomorphism" above.
1084 -- Remember that we may need to do *some* simplification, to
1085 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1086 -- just to float all constraints
1088 -- At top level, we *do* squash methods becuase we want to
1089 -- expose implicit parameters to the test that follows
1091 is_nested_group = isNotTopLevel top_lvl
1092 try_me inst | isFreeWrtTyVars qtvs inst,
1093 (is_nested_group || isDict inst) = Free
1094 | otherwise = ReduceMe AddSCs
1096 reduceContextWithoutImprovement
1097 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1098 ASSERT( null irreds )
1100 -- See "Notes on implicit parameters, Question 4: top level"
1101 if is_nested_group then
1102 extendLIEs frees `thenM_`
1103 returnM (varSetElems qtvs, binds)
1106 (non_ips, bad_ips) = partition isClassDict frees
1108 addTopIPErrs bndrs bad_ips `thenM_`
1109 extendLIEs non_ips `thenM_`
1110 returnM (varSetElems qtvs, binds)
1114 %************************************************************************
1118 %************************************************************************
1120 On the LHS of transformation rules we only simplify methods and constants,
1121 getting dictionaries. We want to keep all of them unsimplified, to serve
1122 as the available stuff for the RHS of the rule.
1124 Example. Consider the following left-hand side of a rule
1126 f (x == y) (y > z) = ...
1128 If we typecheck this expression we get constraints
1130 d1 :: Ord a, d2 :: Eq a
1132 We do NOT want to "simplify" to the LHS
1134 forall x::a, y::a, z::a, d1::Ord a.
1135 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1139 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1140 f ((==) d2 x y) ((>) d1 y z) = ...
1142 Here is another example:
1144 fromIntegral :: (Integral a, Num b) => a -> b
1145 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1147 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1148 we *dont* want to get
1150 forall dIntegralInt.
1151 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1153 because the scsel will mess up RULE matching. Instead we want
1155 forall dIntegralInt, dNumInt.
1156 fromIntegral Int Int dIntegralInt dNumInt = id Int
1160 g (x == y) (y == z) = ..
1162 where the two dictionaries are *identical*, we do NOT WANT
1164 forall x::a, y::a, z::a, d1::Eq a
1165 f ((==) d1 x y) ((>) d1 y z) = ...
1167 because that will only match if the dict args are (visibly) equal.
1168 Instead we want to quantify over the dictionaries separately.
1170 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1171 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1172 from scratch, rather than further parameterise simpleReduceLoop etc
1175 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1176 tcSimplifyRuleLhs wanteds
1177 = go [] emptyBag wanteds
1180 = return (dicts, binds)
1181 go dicts binds (w:ws)
1183 = go (w:dicts) binds ws
1185 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1186 -- to fromInteger; this looks fragile to me
1187 ; lookup_result <- lookupInst w'
1188 ; case lookup_result of
1189 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
1190 SimpleInst rhs -> go dicts (addBind binds w rhs) ws
1191 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1195 tcSimplifyBracket is used when simplifying the constraints arising from
1196 a Template Haskell bracket [| ... |]. We want to check that there aren't
1197 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1198 Show instance), but we aren't otherwise interested in the results.
1199 Nor do we care about ambiguous dictionaries etc. We will type check
1200 this bracket again at its usage site.
1203 tcSimplifyBracket :: [Inst] -> TcM ()
1204 tcSimplifyBracket wanteds
1205 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1208 doc = text "tcSimplifyBracket"
1212 %************************************************************************
1214 \subsection{Filtering at a dynamic binding}
1216 %************************************************************************
1221 we must discharge all the ?x constraints from B. We also do an improvement
1222 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1224 Actually, the constraints from B might improve the types in ?x. For example
1226 f :: (?x::Int) => Char -> Char
1229 then the constraint (?x::Int) arising from the call to f will
1230 force the binding for ?x to be of type Int.
1233 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1236 tcSimplifyIPs given_ips wanteds
1237 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1238 extendLIEs frees `thenM_`
1241 doc = text "tcSimplifyIPs" <+> ppr given_ips
1242 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1244 -- Simplify any methods that mention the implicit parameter
1245 try_me inst | isFreeWrtIPs ip_set inst = Free
1246 | otherwise = ReduceMe NoSCs
1248 simpl_loop givens wanteds
1249 = mappM zonkInst givens `thenM` \ givens' ->
1250 mappM zonkInst wanteds `thenM` \ wanteds' ->
1252 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1254 if no_improvement then
1255 ASSERT( null irreds )
1256 returnM (frees, binds)
1258 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1259 returnM (frees1, binds `unionBags` binds1)
1263 %************************************************************************
1265 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1267 %************************************************************************
1269 When doing a binding group, we may have @Insts@ of local functions.
1270 For example, we might have...
1272 let f x = x + 1 -- orig local function (overloaded)
1273 f.1 = f Int -- two instances of f
1278 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1279 where @f@ is in scope; those @Insts@ must certainly not be passed
1280 upwards towards the top-level. If the @Insts@ were binding-ified up
1281 there, they would have unresolvable references to @f@.
1283 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1284 For each method @Inst@ in the @init_lie@ that mentions one of the
1285 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1286 @LIE@), as well as the @HsBinds@ generated.
1289 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1290 -- Simlifies only MethodInsts, and generate only bindings of form
1292 -- We're careful not to even generate bindings of the form
1294 -- You'd think that'd be fine, but it interacts with what is
1295 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1297 bindInstsOfLocalFuns wanteds local_ids
1298 | null overloaded_ids
1300 = extendLIEs wanteds `thenM_`
1301 returnM emptyLHsBinds
1304 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1305 ASSERT( null irreds )
1306 extendLIEs not_for_me `thenM_`
1307 extendLIEs frees `thenM_`
1310 doc = text "bindInsts" <+> ppr local_ids
1311 overloaded_ids = filter is_overloaded local_ids
1312 is_overloaded id = isOverloadedTy (idType id)
1313 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1315 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1316 -- so it's worth building a set, so that
1317 -- lookup (in isMethodFor) is faster
1318 try_me inst | isMethod inst = ReduceMe NoSCs
1323 %************************************************************************
1325 \subsection{Data types for the reduction mechanism}
1327 %************************************************************************
1329 The main control over context reduction is here
1333 = ReduceMe WantSCs -- Try to reduce this
1334 -- If there's no instance, behave exactly like
1335 -- DontReduce: add the inst to the irreductible ones,
1336 -- but don't produce an error message of any kind.
1337 -- It might be quite legitimate such as (Eq a)!
1339 | DontReduceUnlessConstant -- Return as irreducible unless it can
1340 -- be reduced to a constant in one step
1342 | Free -- Return as free
1344 reduceMe :: Inst -> WhatToDo
1345 reduceMe inst = ReduceMe AddSCs
1347 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1348 -- of a predicate when adding it to the avails
1349 -- The reason for this flag is entirely the super-class loop problem
1350 -- Note [SUPER-CLASS LOOP 1]
1356 type Avails = FiniteMap Inst Avail
1357 emptyAvails = emptyFM
1360 = IsFree -- Used for free Insts
1361 | Irred -- Used for irreducible dictionaries,
1362 -- which are going to be lambda bound
1364 | Given TcId -- Used for dictionaries for which we have a binding
1365 -- e.g. those "given" in a signature
1366 Bool -- True <=> actually consumed (splittable IPs only)
1368 | Rhs -- Used when there is a RHS
1369 (LHsExpr TcId) -- The RHS
1370 [Inst] -- Insts free in the RHS; we need these too
1372 | Linear -- Splittable Insts only.
1373 Int -- The Int is always 2 or more; indicates how
1374 -- many copies are required
1375 Inst -- The splitter
1376 Avail -- Where the "master copy" is
1378 | LinRhss -- Splittable Insts only; this is used only internally
1379 -- by extractResults, where a Linear
1380 -- is turned into an LinRhss
1381 [LHsExpr TcId] -- A supply of suitable RHSs
1383 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1384 | (inst,avail) <- fmToList avails ]
1386 instance Outputable Avail where
1389 pprAvail IsFree = text "Free"
1390 pprAvail Irred = text "Irred"
1391 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1392 if b then text "(used)" else empty
1393 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1394 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1395 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1398 Extracting the bindings from a bunch of Avails.
1399 The bindings do *not* come back sorted in dependency order.
1400 We assume that they'll be wrapped in a big Rec, so that the
1401 dependency analyser can sort them out later
1405 extractResults :: Avails
1407 -> TcM (TcDictBinds, -- Bindings
1408 [Inst], -- Irreducible ones
1409 [Inst]) -- Free ones
1411 extractResults avails wanteds
1412 = go avails emptyBag [] [] wanteds
1414 go avails binds irreds frees []
1415 = returnM (binds, irreds, frees)
1417 go avails binds irreds frees (w:ws)
1418 = case lookupFM avails w of
1419 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1420 go avails binds irreds frees ws
1422 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1423 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1425 Just (Given id _) -> go avails new_binds irreds frees ws
1427 new_binds | id == instToId w = binds
1428 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1429 -- The sought Id can be one of the givens, via a superclass chain
1430 -- and then we definitely don't want to generate an x=x binding!
1432 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1434 new_binds = addBind binds w rhs
1436 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1437 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1438 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1439 go (addToFM avails w (LinRhss rhss))
1440 (binds `unionBags` binds')
1441 irreds' frees' (split_inst : w : ws)
1443 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1444 -> go new_avails new_binds irreds frees ws
1446 new_binds = addBind binds w rhs
1447 new_avails = addToFM avails w (LinRhss rhss)
1449 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1450 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1451 returnM (w':irreds, frees, instToId w')
1452 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1453 returnM (irreds, w':frees, instToId w')
1455 add_given avails w = addToFM avails w (Given (instToId w) True)
1457 add_free avails w | isMethod w = avails
1458 | otherwise = add_given avails w
1460 -- Do *not* replace Free by Given if it's a method.
1461 -- The following situation shows why this is bad:
1462 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1463 -- From an application (truncate f i) we get
1464 -- t1 = truncate at f
1466 -- If we have also have a second occurrence of truncate, we get
1467 -- t3 = truncate at f
1469 -- When simplifying with i,f free, we might still notice that
1470 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1471 -- will continue to float out!
1473 split :: Int -> TcId -> TcId -> Inst
1474 -> TcM (TcDictBinds, [LHsExpr TcId])
1475 -- (split n split_id root_id wanted) returns
1476 -- * a list of 'n' expressions, all of which witness 'avail'
1477 -- * a bunch of auxiliary bindings to support these expressions
1478 -- * one or zero insts needed to witness the whole lot
1479 -- (maybe be zero if the initial Inst is a Given)
1481 -- NB: 'wanted' is just a template
1483 split n split_id root_id wanted
1486 ty = linearInstType wanted
1487 pair_ty = mkTyConApp pairTyCon [ty,ty]
1488 id = instToId wanted
1491 span = instSpan wanted
1493 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1495 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1496 expand n rhss `thenM` \ (binds2, rhss') ->
1497 returnM (binds1 `unionBags` binds2, rhss')
1500 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1501 -- e.g. expand 3 [rhs1, rhs2]
1502 -- = ( { x = split rhs1 },
1503 -- [fst x, snd x, rhs2] )
1505 | n `rem` 2 == 0 = go rhss -- n is even
1506 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1507 returnM (binds', head rhss : rhss')
1509 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1510 returnM (listToBag binds', concat rhss')
1512 do_one rhs = newUnique `thenM` \ uniq ->
1513 tcLookupId fstName `thenM` \ fst_id ->
1514 tcLookupId sndName `thenM` \ snd_id ->
1516 x = mkUserLocal occ uniq pair_ty loc
1518 returnM (L span (VarBind x (mk_app span split_id rhs)),
1519 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1521 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1523 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1525 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1526 (VarBind (instToId inst) rhs))
1527 instSpan wanted = instLocSrcSpan (instLoc wanted)
1531 %************************************************************************
1533 \subsection[reduce]{@reduce@}
1535 %************************************************************************
1537 When the "what to do" predicate doesn't depend on the quantified type variables,
1538 matters are easier. We don't need to do any zonking, unless the improvement step
1539 does something, in which case we zonk before iterating.
1541 The "given" set is always empty.
1544 simpleReduceLoop :: SDoc
1545 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1547 -> TcM ([Inst], -- Free
1549 [Inst]) -- Irreducible
1551 simpleReduceLoop doc try_me wanteds
1552 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1553 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1554 if no_improvement then
1555 returnM (frees, binds, irreds)
1557 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1558 returnM (frees1, binds `unionBags` binds1, irreds1)
1564 reduceContext :: SDoc
1565 -> (Inst -> WhatToDo)
1568 -> TcM (Bool, -- True <=> improve step did no unification
1570 TcDictBinds, -- Dictionary bindings
1571 [Inst]) -- Irreducible
1573 reduceContext doc try_me givens wanteds
1575 traceTc (text "reduceContext" <+> (vcat [
1576 text "----------------------",
1578 text "given" <+> ppr givens,
1579 text "wanted" <+> ppr wanteds,
1580 text "----------------------"
1583 -- Build the Avail mapping from "givens"
1584 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1587 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1589 -- Do improvement, using everything in avails
1590 -- In particular, avails includes all superclasses of everything
1591 tcImprove avails `thenM` \ no_improvement ->
1593 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1595 traceTc (text "reduceContext end" <+> (vcat [
1596 text "----------------------",
1598 text "given" <+> ppr givens,
1599 text "wanted" <+> ppr wanteds,
1601 text "avails" <+> pprAvails avails,
1602 text "frees" <+> ppr frees,
1603 text "no_improvement =" <+> ppr no_improvement,
1604 text "----------------------"
1607 returnM (no_improvement, frees, binds, irreds)
1609 -- reduceContextWithoutImprovement differs from reduceContext
1610 -- (a) no improvement
1611 -- (b) 'givens' is assumed empty
1612 reduceContextWithoutImprovement doc try_me wanteds
1614 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1615 text "----------------------",
1617 text "wanted" <+> ppr wanteds,
1618 text "----------------------"
1622 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1623 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1625 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1626 text "----------------------",
1628 text "wanted" <+> ppr wanteds,
1630 text "avails" <+> pprAvails avails,
1631 text "frees" <+> ppr frees,
1632 text "----------------------"
1635 returnM (frees, binds, irreds)
1637 tcImprove :: Avails -> TcM Bool -- False <=> no change
1638 -- Perform improvement using all the predicates in Avails
1640 = tcGetInstEnvs `thenM` \ inst_envs ->
1642 preds = [ (pred, pp_loc)
1643 | (inst, avail) <- fmToList avails,
1644 pred <- get_preds inst avail,
1645 let pp_loc = pprInstLoc (instLoc inst)
1647 -- Avails has all the superclasses etc (good)
1648 -- It also has all the intermediates of the deduction (good)
1649 -- It does not have duplicates (good)
1650 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1651 -- so that improve will see them separate
1653 -- For free Methods, we want to take predicates from their context,
1654 -- but for Methods that have been squished their context will already
1655 -- be in Avails, and we don't want duplicates. Hence this rather
1656 -- horrid get_preds function
1657 get_preds inst IsFree = fdPredsOfInst inst
1658 get_preds inst other | isDict inst = [dictPred inst]
1661 eqns = improve get_insts preds
1662 get_insts clas = classInstances inst_envs clas
1667 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1668 mappM_ unify eqns `thenM_`
1671 unify ((qtvs, pairs), what1, what2)
1672 = addErrCtxtM (mkEqnMsg what1 what2) $
1673 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1674 mapM_ (unif_pr tenv) pairs
1675 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1677 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1679 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1680 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1681 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1682 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1683 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1684 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1685 ; return (tidy_env, msg) }
1688 The main context-reduction function is @reduce@. Here's its game plan.
1691 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1692 -- along with its depth
1693 -> (Inst -> WhatToDo)
1700 try_me: given an inst, this function returns
1702 DontReduce return this in "irreds"
1703 Free return this in "frees"
1705 wanteds: The list of insts to reduce
1706 state: An accumulating parameter of type Avails
1707 that contains the state of the algorithm
1709 It returns a Avails.
1711 The (n,stack) pair is just used for error reporting.
1712 n is always the depth of the stack.
1713 The stack is the stack of Insts being reduced: to produce X
1714 I had to produce Y, to produce Y I had to produce Z, and so on.
1717 reduceList (n,stack) try_me wanteds state
1718 | n > opt_MaxContextReductionDepth
1719 = failWithTc (reduceDepthErr n stack)
1725 pprTrace "Interesting! Context reduction stack deeper than 8:"
1726 (int n $$ ifPprDebug (nest 2 (pprStack stack)))
1731 go [] state = returnM state
1732 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1735 -- Base case: we're done!
1736 reduce stack try_me wanted avails
1737 -- It's the same as an existing inst, or a superclass thereof
1738 | Just avail <- isAvailable avails wanted
1739 = if isLinearInst wanted then
1740 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1741 reduceList stack try_me wanteds' avails'
1743 returnM avails -- No op for non-linear things
1746 = case try_me wanted of {
1748 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1749 -- First, see if the inst can be reduced to a constant in one step
1750 try_simple (addIrred AddSCs) -- Assume want superclasses
1752 ; Free -> -- It's free so just chuck it upstairs
1753 -- First, see if the inst can be reduced to a constant in one step
1756 ; ReduceMe want_scs -> -- It should be reduced
1757 lookupInst wanted `thenM` \ lookup_result ->
1758 case lookup_result of
1759 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1760 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1761 addWanted want_scs avails2 wanted rhs wanteds'
1762 -- Experiment with temporarily doing addIrred *before* the reduceList,
1763 -- which has the effect of adding the thing we are trying
1764 -- to prove to the database before trying to prove the things it
1765 -- needs. See note [RECURSIVE DICTIONARIES]
1766 -- NB: we must not do an addWanted before, because that adds the
1767 -- superclasses too, and thaat can lead to a spurious loop; see
1768 -- the examples in [SUPERCLASS-LOOP]
1769 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1771 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1773 NoInstance -> -- No such instance!
1774 -- Add it and its superclasses
1775 addIrred want_scs avails wanted
1778 try_simple do_this_otherwise
1779 = lookupInst wanted `thenM` \ lookup_result ->
1780 case lookup_result of
1781 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1782 other -> do_this_otherwise avails wanted
1787 -------------------------
1788 isAvailable :: Avails -> Inst -> Maybe Avail
1789 isAvailable avails wanted = lookupFM avails wanted
1790 -- NB 1: the Ord instance of Inst compares by the class/type info
1791 -- *not* by unique. So
1792 -- d1::C Int == d2::C Int
1794 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1795 addLinearAvailable avails avail wanted
1796 -- avails currently maps [wanted -> avail]
1797 -- Extend avails to reflect a neeed for an extra copy of avail
1799 | Just avail' <- split_avail avail
1800 = returnM (addToFM avails wanted avail', [])
1803 = tcLookupId splitName `thenM` \ split_id ->
1804 tcInstClassOp (instLoc wanted) split_id
1805 [linearInstType wanted] `thenM` \ split_inst ->
1806 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1809 split_avail :: Avail -> Maybe Avail
1810 -- (Just av) if there's a modified version of avail that
1811 -- we can use to replace avail in avails
1812 -- Nothing if there isn't, so we need to create a Linear
1813 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1814 split_avail (Given id used) | not used = Just (Given id True)
1815 | otherwise = Nothing
1816 split_avail Irred = Nothing
1817 split_avail IsFree = Nothing
1818 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1820 -------------------------
1821 addFree :: Avails -> Inst -> TcM Avails
1822 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1823 -- to avails, so that any other equal Insts will be commoned up right
1824 -- here rather than also being tossed upstairs. This is really just
1825 -- an optimisation, and perhaps it is more trouble that it is worth,
1826 -- as the following comments show!
1828 -- NB: do *not* add superclasses. If we have
1831 -- but a is not bound here, then we *don't* want to derive
1832 -- dn from df here lest we lose sharing.
1834 addFree avails free = returnM (addToFM avails free IsFree)
1836 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1837 addWanted want_scs avails wanted rhs_expr wanteds
1838 = addAvailAndSCs want_scs avails wanted avail
1840 avail = Rhs rhs_expr wanteds
1842 addGiven :: Avails -> Inst -> TcM Avails
1843 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1844 -- Always add superclasses for 'givens'
1846 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1847 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1848 -- so the assert isn't true
1850 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1851 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1852 addAvailAndSCs want_scs avails irred Irred
1854 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1855 addAvailAndSCs want_scs avails inst avail
1856 | not (isClassDict inst) = return avails_with_inst
1857 | NoSCs <- want_scs = return avails_with_inst
1858 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1859 ; addSCs is_loop avails_with_inst inst }
1861 avails_with_inst = addToFM avails inst avail
1863 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1864 -- Note: this compares by *type*, not by Unique
1865 deps = findAllDeps (unitVarSet (instToId inst)) avail
1866 dep_tys = map idType (varSetElems deps)
1868 findAllDeps :: IdSet -> Avail -> IdSet
1869 -- Find all the Insts that this one depends on
1870 -- See Note [SUPERCLASS-LOOP 2]
1871 -- Watch out, though. Since the avails may contain loops
1872 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1873 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1874 findAllDeps so_far other = so_far
1876 find_all :: IdSet -> Inst -> IdSet
1878 | kid_id `elemVarSet` so_far = so_far
1879 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1880 | otherwise = so_far'
1882 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1883 kid_id = instToId kid
1885 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1886 -- Add all the superclasses of the Inst to Avails
1887 -- The first param says "dont do this because the original thing
1888 -- depends on this one, so you'd build a loop"
1889 -- Invariant: the Inst is already in Avails.
1891 addSCs is_loop avails dict
1892 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1893 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1895 (clas, tys) = getDictClassTys dict
1896 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1897 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1899 add_sc avails (sc_dict, sc_sel)
1900 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1901 | is_given sc_dict = return avails
1902 | otherwise = addSCs is_loop avails' sc_dict
1904 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1905 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1907 is_given :: Inst -> Bool
1908 is_given sc_dict = case lookupFM avails sc_dict of
1909 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1913 Note [SUPERCLASS-LOOP 2]
1914 ~~~~~~~~~~~~~~~~~~~~~~~~
1915 But the above isn't enough. Suppose we are *given* d1:Ord a,
1916 and want to deduce (d2:C [a]) where
1918 class Ord a => C a where
1919 instance Ord [a] => C [a] where ...
1921 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1922 superclasses of C [a] to avails. But we must not overwrite the binding
1923 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1926 Here's another variant, immortalised in tcrun020
1927 class Monad m => C1 m
1928 class C1 m => C2 m x
1929 instance C2 Maybe Bool
1930 For the instance decl we need to build (C1 Maybe), and it's no good if
1931 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1932 before we search for C1 Maybe.
1934 Here's another example
1935 class Eq b => Foo a b
1936 instance Eq a => Foo [a] a
1940 we'll first deduce that it holds (via the instance decl). We must not
1941 then overwrite the Eq t constraint with a superclass selection!
1943 At first I had a gross hack, whereby I simply did not add superclass constraints
1944 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1945 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1946 I found a very obscure program (now tcrun021) in which improvement meant the
1947 simplifier got two bites a the cherry... so something seemed to be an Irred
1948 first time, but reducible next time.
1950 Now we implement the Right Solution, which is to check for loops directly
1951 when adding superclasses. It's a bit like the occurs check in unification.
1954 Note [RECURSIVE DICTIONARIES]
1955 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1957 data D r = ZeroD | SuccD (r (D r));
1959 instance (Eq (r (D r))) => Eq (D r) where
1960 ZeroD == ZeroD = True
1961 (SuccD a) == (SuccD b) = a == b
1964 equalDC :: D [] -> D [] -> Bool;
1967 We need to prove (Eq (D [])). Here's how we go:
1971 by instance decl, holds if
1975 by instance decl of Eq, holds if
1977 where d2 = dfEqList d3
1980 But now we can "tie the knot" to give
1986 and it'll even run! The trick is to put the thing we are trying to prove
1987 (in this case Eq (D []) into the database before trying to prove its
1988 contributing clauses.
1991 %************************************************************************
1993 \section{tcSimplifyTop: defaulting}
1995 %************************************************************************
1998 @tcSimplifyTop@ is called once per module to simplify all the constant
1999 and ambiguous Insts.
2001 We need to be careful of one case. Suppose we have
2003 instance Num a => Num (Foo a b) where ...
2005 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2006 to (Num x), and default x to Int. But what about y??
2008 It's OK: the final zonking stage should zap y to (), which is fine.
2012 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2013 tcSimplifyTop wanteds
2014 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2016 doc = text "tcSimplifyTop"
2018 tcSimplifyInteractive wanteds
2019 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2021 doc = text "tcSimplifyTop"
2023 -- The TcLclEnv should be valid here, solely to improve
2024 -- error message generation for the monomorphism restriction
2025 tc_simplify_top doc is_interactive want_scs wanteds
2026 = do { lcl_env <- getLclEnv
2027 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2029 ; let try_me inst = ReduceMe want_scs
2030 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2033 -- First get rid of implicit parameters
2034 (non_ips, bad_ips) = partition isClassDict irreds
2036 -- All the non-tv or multi-param ones are definite errors
2037 (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
2038 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2040 -- Group by type variable
2041 tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
2043 -- Pick the ones which its worth trying to disambiguate
2044 -- namely, the ones whose type variable isn't bound
2045 -- up with one of the non-tyvar classes
2046 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2047 defaultable_group ds
2048 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
2049 && defaultable_classes (map get_clas ds)
2050 defaultable_classes clss
2051 | is_interactive = any isInteractiveClass clss
2052 | otherwise = all isStandardClass clss && any isNumericClass clss
2054 isInteractiveClass cls = isNumericClass cls
2055 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2056 -- In interactive mode, we default Show a to Show ()
2057 -- to avoid graututious errors on "show []"
2060 -- Collect together all the bad guys
2061 bad_guys = non_tvs ++ concat non_default_gps
2062 (ambigs, no_insts) = partition isTyVarDict bad_guys
2063 -- If the dict has no type constructors involved, it must be ambiguous,
2064 -- except I suppose that another error with fundeps maybe should have
2065 -- constrained those type variables
2067 -- Report definite errors
2068 ; ASSERT( null frees )
2069 groupErrs (addNoInstanceErrs Nothing []) no_insts
2070 ; strangeTopIPErrs bad_ips
2072 -- Deal with ambiguity errors, but only if
2073 -- if there has not been an error so far:
2074 -- errors often give rise to spurious ambiguous Insts.
2076 -- f = (*) -- Monomorphic
2077 -- g :: Num a => a -> a
2079 -- Here, we get a complaint when checking the type signature for g,
2080 -- that g isn't polymorphic enough; but then we get another one when
2081 -- dealing with the (Num a) context arising from f's definition;
2082 -- we try to unify a with Int (to default it), but find that it's
2083 -- already been unified with the rigid variable from g's type sig
2084 ; binds_ambig <- ifErrsM (returnM []) $
2085 do { -- Complain about the ones that don't fall under
2086 -- the Haskell rules for disambiguation
2087 -- This group includes both non-existent instances
2088 -- e.g. Num (IO a) and Eq (Int -> Int)
2089 -- and ambiguous dictionaries
2091 addTopAmbigErrs ambigs
2093 -- Disambiguate the ones that look feasible
2094 ; mappM disambigGroup default_gps }
2096 ; return (binds `unionBags` unionManyBags binds_ambig) }
2098 ----------------------------------
2099 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2101 is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
2102 -- Invariant: argument is a ClassDict, not IP or method
2103 is_unary_tyvar_dict d = case getDictClassTys d of
2104 (_, [ty]) -> tcIsTyVarTy ty
2107 get_tv d = case getDictClassTys d of
2108 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2109 get_clas d = case getDictClassTys d of
2113 If a dictionary constrains a type variable which is
2114 * not mentioned in the environment
2115 * and not mentioned in the type of the expression
2116 then it is ambiguous. No further information will arise to instantiate
2117 the type variable; nor will it be generalised and turned into an extra
2118 parameter to a function.
2120 It is an error for this to occur, except that Haskell provided for
2121 certain rules to be applied in the special case of numeric types.
2123 * at least one of its classes is a numeric class, and
2124 * all of its classes are numeric or standard
2125 then the type variable can be defaulted to the first type in the
2126 default-type list which is an instance of all the offending classes.
2128 So here is the function which does the work. It takes the ambiguous
2129 dictionaries and either resolves them (producing bindings) or
2130 complains. It works by splitting the dictionary list by type
2131 variable, and using @disambigOne@ to do the real business.
2133 @disambigOne@ assumes that its arguments dictionaries constrain all
2134 the same type variable.
2136 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2137 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2138 the most common use of defaulting is code like:
2140 _ccall_ foo `seqPrimIO` bar
2142 Since we're not using the result of @foo@, the result if (presumably)
2146 disambigGroup :: [Inst] -- All standard classes of form (C a)
2150 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2151 -- SO, TRY DEFAULT TYPES IN ORDER
2153 -- Failure here is caused by there being no type in the
2154 -- default list which can satisfy all the ambiguous classes.
2155 -- For example, if Real a is reqd, but the only type in the
2156 -- default list is Int.
2157 get_default_tys `thenM` \ default_tys ->
2159 try_default [] -- No defaults work, so fail
2162 try_default (default_ty : default_tys)
2163 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2164 -- default_tys instead
2165 tcSimplifyDefault theta `thenM` \ _ ->
2168 theta = [mkClassPred clas [default_ty] | clas <- classes]
2170 -- See if any default works
2171 tryM (try_default default_tys) `thenM` \ mb_ty ->
2174 Right chosen_default_ty -> choose_default chosen_default_ty
2176 tyvar = get_tv (head dicts) -- Should be non-empty
2177 classes = map get_clas dicts
2179 choose_default default_ty -- Commit to tyvar = default_ty
2180 = -- Bind the type variable
2181 unifyType default_ty (mkTyVarTy tyvar) `thenM_`
2182 -- and reduce the context, for real this time
2183 simpleReduceLoop (text "disambig" <+> ppr dicts)
2184 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2185 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2186 warnDefault dicts default_ty `thenM_`
2189 bomb_out = addTopAmbigErrs dicts `thenM_`
2193 = do { mb_defaults <- getDefaultTys
2194 ; case mb_defaults of
2195 Just tys -> return tys
2196 Nothing -> -- No use-supplied default;
2197 -- use [Integer, Double]
2198 do { integer_ty <- tcMetaTy integerTyConName
2199 ; checkWiredInTyCon doubleTyCon
2200 ; return [integer_ty, doubleTy] } }
2203 [Aside - why the defaulting mechanism is turned off when
2204 dealing with arguments and results to ccalls.
2206 When typechecking _ccall_s, TcExpr ensures that the external
2207 function is only passed arguments (and in the other direction,
2208 results) of a restricted set of 'native' types.
2210 The interaction between the defaulting mechanism for numeric
2211 values and CC & CR can be a bit puzzling to the user at times.
2220 What type has 'x' got here? That depends on the default list
2221 in operation, if it is equal to Haskell 98's default-default
2222 of (Integer, Double), 'x' has type Double, since Integer
2223 is not an instance of CR. If the default list is equal to
2224 Haskell 1.4's default-default of (Int, Double), 'x' has type
2230 %************************************************************************
2232 \subsection[simple]{@Simple@ versions}
2234 %************************************************************************
2236 Much simpler versions when there are no bindings to make!
2238 @tcSimplifyThetas@ simplifies class-type constraints formed by
2239 @deriving@ declarations and when specialising instances. We are
2240 only interested in the simplified bunch of class/type constraints.
2242 It simplifies to constraints of the form (C a b c) where
2243 a,b,c are type variables. This is required for the context of
2244 instance declarations.
2247 tcSimplifyDeriv :: TyCon
2249 -> ThetaType -- Wanted
2250 -> TcM ThetaType -- Needed
2252 tcSimplifyDeriv tc tyvars theta
2253 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2254 -- The main loop may do unification, and that may crash if
2255 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2256 -- ToDo: what if two of them do get unified?
2257 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2258 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2259 ASSERT( null frees ) -- reduceMe never returns Free
2261 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
2262 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2264 tv_set = mkVarSet tvs
2266 (bad_insts, ok_insts) = partition is_bad_inst irreds
2268 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2269 in isEmptyVarSet (tyVarsOfPred pred)
2270 -- Things like (Eq T) are bad
2271 || (not gla_exts && not (isTyVarClassPred pred))
2273 simpl_theta = map dictPred ok_insts
2274 weird_preds = [pred | pred <- simpl_theta
2275 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2276 -- Check for a bizarre corner case, when the derived instance decl should
2277 -- have form instance C a b => D (T a) where ...
2278 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2279 -- of problems; in particular, it's hard to compare solutions for
2280 -- equality when finding the fixpoint. So I just rule it out for now.
2282 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2283 -- This reverse-mapping is a Royal Pain,
2284 -- but the result should mention TyVars not TcTyVars
2287 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2288 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2289 returnM (substTheta rev_env simpl_theta)
2291 doc = ptext SLIT("deriving classes for a data type")
2294 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2295 used with \tr{default} declarations. We are only interested in
2296 whether it worked or not.
2299 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2302 tcSimplifyDefault theta
2303 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2304 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2305 ASSERT( null frees ) -- try_me never returns Free
2306 addNoInstanceErrs Nothing [] irreds `thenM_`
2312 doc = ptext SLIT("default declaration")
2316 %************************************************************************
2318 \section{Errors and contexts}
2320 %************************************************************************
2322 ToDo: for these error messages, should we note the location as coming
2323 from the insts, or just whatever seems to be around in the monad just
2327 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2328 -> [Inst] -- The offending Insts
2330 -- Group together insts with the same origin
2331 -- We want to report them together in error messages
2333 groupErrs report_err []
2335 groupErrs report_err (inst:insts)
2336 = do_one (inst:friends) `thenM_`
2337 groupErrs report_err others
2340 -- (It may seem a bit crude to compare the error messages,
2341 -- but it makes sure that we combine just what the user sees,
2342 -- and it avoids need equality on InstLocs.)
2343 (friends, others) = partition is_friend insts
2344 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2345 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2346 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2347 -- Add location and context information derived from the Insts
2349 -- Add the "arising from..." part to a message about bunch of dicts
2350 addInstLoc :: [Inst] -> Message -> Message
2351 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2353 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2354 addTopIPErrs bndrs []
2356 addTopIPErrs bndrs ips
2357 = addErrTcM (tidy_env, mk_msg tidy_ips)
2359 (tidy_env, tidy_ips) = tidyInsts ips
2360 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2361 nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
2362 <+> pprBinders bndrs <> colon)],
2363 nest 2 (vcat (map ppr_ip ips)),
2365 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2367 strangeTopIPErrs :: [Inst] -> TcM ()
2368 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2369 = groupErrs report tidy_dicts
2371 (tidy_env, tidy_dicts) = tidyInsts dicts
2372 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2373 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2374 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2376 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2377 -- Just d => d describes the construct
2378 -> [Inst] -- What is given by the context or type sig
2379 -> [Inst] -- What is wanted
2381 addNoInstanceErrs mb_what givens []
2383 addNoInstanceErrs mb_what givens dicts
2384 = -- Some of the dicts are here because there is no instances
2385 -- and some because there are too many instances (overlap)
2386 tcGetInstEnvs `thenM` \ inst_envs ->
2388 (tidy_env1, tidy_givens) = tidyInsts givens
2389 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2391 -- Run through the dicts, generating a message for each
2392 -- overlapping one, but simply accumulating all the
2393 -- no-instance ones so they can be reported as a group
2394 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2395 check_overlap (overlap_doc, no_inst_dicts) dict
2396 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2398 = case lookupInstEnv inst_envs clas tys of
2399 -- The case of exactly one match and no unifiers means
2400 -- a successful lookup. That can't happen here, becuase
2401 -- dicts only end up here if they didn't match in Inst.lookupInst
2403 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2405 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2406 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2408 (clas,tys) = getDictClassTys dict
2411 -- Now generate a good message for the no-instance bunch
2412 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2414 no_inst_doc | null no_inst_dicts = empty
2415 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2416 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2417 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2418 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2419 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2421 -- And emit both the non-instance and overlap messages
2422 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2424 mk_overlap_msg dict (matches, unifiers)
2425 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2426 <+> pprPred (dictPred dict))),
2427 sep [ptext SLIT("Matching instances") <> colon,
2428 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2429 ASSERT( not (null matches) )
2430 if not (isSingleton matches)
2431 then -- Two or more matches
2433 else -- One match, plus some unifiers
2434 ASSERT( not (null unifiers) )
2435 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2436 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2437 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2439 ispecs = [ispec | (_, ispec) <- matches]
2441 mk_probable_fix tidy_env dicts
2442 = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
2444 fixes = add_ors (fix1 ++ fix2)
2446 fix1 = case mb_what of
2447 Nothing -> [] -- Top level
2448 Just what -> -- Nested (type signatures, instance decls)
2449 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2450 ptext SLIT("to the") <+> what] ]
2452 fix2 | null instance_dicts = []
2453 | otherwise = [ ptext SLIT("add an instance declaration for")
2454 <+> pprDictsTheta instance_dicts ]
2455 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2456 -- Insts for which it is worth suggesting an adding an instance declaration
2457 -- Exclude implicit parameters, and tyvar dicts
2459 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2460 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2461 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2463 addTopAmbigErrs dicts
2464 -- Divide into groups that share a common set of ambiguous tyvars
2465 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2467 (tidy_env, tidy_dicts) = tidyInsts dicts
2469 tvs_of :: Inst -> [TcTyVar]
2470 tvs_of d = varSetElems (tyVarsOfInst d)
2471 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2473 report :: [(Inst,[TcTyVar])] -> TcM ()
2474 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2475 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2476 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2477 -- the location of the first one will do for the err message
2478 addErrTcM (tidy_env, msg $$ mono_msg)
2480 dicts = map fst pairs
2481 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2482 pprQuotedList tvs <+> in_msg,
2483 nest 2 (pprDictsInFull dicts)]
2484 in_msg = text "in the constraint" <> plural dicts <> colon
2487 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2488 -- There's an error with these Insts; if they have free type variables
2489 -- it's probably caused by the monomorphism restriction.
2490 -- Try to identify the offending variable
2491 -- ASSUMPTION: the Insts are fully zonked
2492 mkMonomorphismMsg tidy_env inst_tvs
2493 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2494 returnM (tidy_env, mk_msg docs)
2496 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2497 -- This happens in things like
2498 -- f x = show (read "foo")
2499 -- whre monomorphism doesn't play any role
2500 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2504 monomorphism_fix :: SDoc
2505 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2506 (ptext SLIT("give these definition(s) an explicit type signature")
2507 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2509 warnDefault dicts default_ty
2510 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2511 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2514 (_, tidy_dicts) = tidyInsts dicts
2515 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2516 quotes (ppr default_ty),
2517 pprDictsInFull tidy_dicts]
2519 -- Used for the ...Thetas variants; all top level
2521 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2522 ptext SLIT("type variables that are not data type parameters"),
2523 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2525 reduceDepthErr n stack
2526 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2527 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2528 nest 4 (pprStack stack)]
2530 pprStack stack = vcat (map pprInstInFull stack)