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 checkAmbiguity, checkInstTermination )
47 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
48 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
49 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
50 tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
51 import TcIface ( checkWiredInTyCon )
52 import Id ( idType, mkUserLocal )
54 import TyCon ( TyCon )
55 import Name ( Name, getOccName, getSrcLoc )
56 import NameSet ( NameSet, mkNameSet, elemNameSet )
57 import Class ( classBigSig, classKey )
58 import FunDeps ( oclose, grow, improve, pprEquation )
59 import PrelInfo ( isNumericClass, isStandardClass )
60 import PrelNames ( splitName, fstName, sndName, integerTyConName,
61 showClassKey, eqClassKey, ordClassKey )
62 import Type ( zipTopTvSubst, substTheta, substTy )
63 import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
64 import ErrUtils ( Message )
65 import BasicTypes ( TopLevelFlag, isNotTopLevel )
67 import VarEnv ( TidyEnv )
71 import ListSetOps ( equivClasses )
72 import Util ( zipEqual, isSingleton )
73 import List ( partition )
74 import SrcLoc ( Located(..) )
75 import DynFlags ( DynFlag(..) )
80 %************************************************************************
84 %************************************************************************
86 --------------------------------------
87 Notes on functional dependencies (a bug)
88 --------------------------------------
90 | > class Foo a b | a->b
92 | > class Bar a b | a->b
96 | > instance Bar Obj Obj
98 | > instance (Bar a b) => Foo a b
100 | > foo:: (Foo a b) => a -> String
103 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
109 | Could not deduce (Bar a b) from the context (Foo a b)
110 | arising from use of `foo' at <interactive>:1
112 | Add (Bar a b) to the expected type of an expression
113 | In the first argument of `runFoo', namely `foo'
114 | In the definition of `it': it = runFoo foo
116 | Why all of the sudden does GHC need the constraint Bar a b? The
117 | function foo didn't ask for that...
119 The trouble is that to type (runFoo foo), GHC has to solve the problem:
121 Given constraint Foo a b
122 Solve constraint Foo a b'
124 Notice that b and b' aren't the same. To solve this, just do
125 improvement and then they are the same. But GHC currently does
130 That is usually fine, but it isn't here, because it sees that Foo a b is
131 not the same as Foo a b', and so instead applies the instance decl for
132 instance Bar a b => Foo a b. And that's where the Bar constraint comes
135 The Right Thing is to improve whenever the constraint set changes at
136 all. Not hard in principle, but it'll take a bit of fiddling to do.
140 --------------------------------------
141 Notes on quantification
142 --------------------------------------
144 Suppose we are about to do a generalisation step.
148 T the type of the RHS
149 C the constraints from that RHS
151 The game is to figure out
153 Q the set of type variables over which to quantify
154 Ct the constraints we will *not* quantify over
155 Cq the constraints we will quantify over
157 So we're going to infer the type
161 and float the constraints Ct further outwards.
163 Here are the things that *must* be true:
165 (A) Q intersect fv(G) = EMPTY limits how big Q can be
166 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
168 (A) says we can't quantify over a variable that's free in the
169 environment. (B) says we must quantify over all the truly free
170 variables in T, else we won't get a sufficiently general type. We do
171 not *need* to quantify over any variable that is fixed by the free
172 vars of the environment G.
174 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
176 Example: class H x y | x->y where ...
178 fv(G) = {a} C = {H a b, H c d}
181 (A) Q intersect {a} is empty
182 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
184 So Q can be {c,d}, {b,c,d}
186 Other things being equal, however, we'd like to quantify over as few
187 variables as possible: smaller types, fewer type applications, more
188 constraints can get into Ct instead of Cq.
191 -----------------------------------------
194 fv(T) the free type vars of T
196 oclose(vs,C) The result of extending the set of tyvars vs
197 using the functional dependencies from C
199 grow(vs,C) The result of extend the set of tyvars vs
200 using all conceivable links from C.
202 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
203 Then grow(vs,C) = {a,b,c}
205 Note that grow(vs,C) `superset` grow(vs,simplify(C))
206 That is, simplfication can only shrink the result of grow.
209 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
210 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
213 -----------------------------------------
217 Here's a good way to choose Q:
219 Q = grow( fv(T), C ) \ oclose( fv(G), C )
221 That is, quantify over all variable that that MIGHT be fixed by the
222 call site (which influences T), but which aren't DEFINITELY fixed by
223 G. This choice definitely quantifies over enough type variables,
224 albeit perhaps too many.
226 Why grow( fv(T), C ) rather than fv(T)? Consider
228 class H x y | x->y where ...
233 If we used fv(T) = {c} we'd get the type
235 forall c. H c d => c -> b
237 And then if the fn was called at several different c's, each of
238 which fixed d differently, we'd get a unification error, because
239 d isn't quantified. Solution: quantify d. So we must quantify
240 everything that might be influenced by c.
242 Why not oclose( fv(T), C )? Because we might not be able to see
243 all the functional dependencies yet:
245 class H x y | x->y where ...
246 instance H x y => Eq (T x y) where ...
251 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
252 apparent yet, and that's wrong. We must really quantify over d too.
255 There really isn't any point in quantifying over any more than
256 grow( fv(T), C ), because the call sites can't possibly influence
257 any other type variables.
261 --------------------------------------
263 --------------------------------------
265 It's very hard to be certain when a type is ambiguous. Consider
269 instance H x y => K (x,y)
271 Is this type ambiguous?
272 forall a b. (K (a,b), Eq b) => a -> a
274 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
275 now we see that a fixes b. So we can't tell about ambiguity for sure
276 without doing a full simplification. And even that isn't possible if
277 the context has some free vars that may get unified. Urgle!
279 Here's another example: is this ambiguous?
280 forall a b. Eq (T b) => a -> a
281 Not if there's an insance decl (with no context)
282 instance Eq (T b) where ...
284 You may say of this example that we should use the instance decl right
285 away, but you can't always do that:
287 class J a b where ...
288 instance J Int b where ...
290 f :: forall a b. J a b => a -> a
292 (Notice: no functional dependency in J's class decl.)
293 Here f's type is perfectly fine, provided f is only called at Int.
294 It's premature to complain when meeting f's signature, or even
295 when inferring a type for f.
299 However, we don't *need* to report ambiguity right away. It'll always
300 show up at the call site.... and eventually at main, which needs special
301 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
303 So here's the plan. We WARN about probable ambiguity if
305 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
307 (all tested before quantification).
308 That is, all the type variables in Cq must be fixed by the the variables
309 in the environment, or by the variables in the type.
311 Notice that we union before calling oclose. Here's an example:
313 class J a b c | a b -> c
317 forall b c. (J a b c) => b -> b
319 Only if we union {a} from G with {b} from T before using oclose,
320 do we see that c is fixed.
322 It's a bit vague exactly which C we should use for this oclose call. If we
323 don't fix enough variables we might complain when we shouldn't (see
324 the above nasty example). Nothing will be perfect. That's why we can
325 only issue a warning.
328 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
330 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
332 then c is a "bubble"; there's no way it can ever improve, and it's
333 certainly ambiguous. UNLESS it is a constant (sigh). And what about
338 instance H x y => K (x,y)
340 Is this type ambiguous?
341 forall a b. (K (a,b), Eq b) => a -> a
343 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
344 is a "bubble" that's a set of constraints
346 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
348 Hence another idea. To decide Q start with fv(T) and grow it
349 by transitive closure in Cq (no functional dependencies involved).
350 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
351 The definitely-ambiguous can then float out, and get smashed at top level
352 (which squashes out the constants, like Eq (T a) above)
355 --------------------------------------
356 Notes on principal types
357 --------------------------------------
362 f x = let g y = op (y::Int) in True
364 Here the principal type of f is (forall a. a->a)
365 but we'll produce the non-principal type
366 f :: forall a. C Int => a -> a
369 --------------------------------------
370 The need for forall's in constraints
371 --------------------------------------
373 [Exchange on Haskell Cafe 5/6 Dec 2000]
375 class C t where op :: t -> Bool
376 instance C [t] where op x = True
378 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
379 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
381 The definitions of p and q differ only in the order of the components in
382 the pair on their right-hand sides. And yet:
384 ghc and "Typing Haskell in Haskell" reject p, but accept q;
385 Hugs rejects q, but accepts p;
386 hbc rejects both p and q;
387 nhc98 ... (Malcolm, can you fill in the blank for us!).
389 The type signature for f forces context reduction to take place, and
390 the results of this depend on whether or not the type of y is known,
391 which in turn depends on which component of the pair the type checker
394 Solution: if y::m a, float out the constraints
395 Monad m, forall c. C (m c)
396 When m is later unified with [], we can solve both constraints.
399 --------------------------------------
400 Notes on implicit parameters
401 --------------------------------------
403 Question 1: can we "inherit" implicit parameters
404 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
409 where f is *not* a top-level binding.
410 From the RHS of f we'll get the constraint (?y::Int).
411 There are two types we might infer for f:
415 (so we get ?y from the context of f's definition), or
417 f :: (?y::Int) => Int -> Int
419 At first you might think the first was better, becuase then
420 ?y behaves like a free variable of the definition, rather than
421 having to be passed at each call site. But of course, the WHOLE
422 IDEA is that ?y should be passed at each call site (that's what
423 dynamic binding means) so we'd better infer the second.
425 BOTTOM LINE: when *inferring types* you *must* quantify
426 over implicit parameters. See the predicate isFreeWhenInferring.
429 Question 2: type signatures
430 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
431 BUT WATCH OUT: When you supply a type signature, we can't force you
432 to quantify over implicit parameters. For example:
436 This is perfectly reasonable. We do not want to insist on
438 (?x + 1) :: (?x::Int => Int)
440 That would be silly. Here, the definition site *is* the occurrence site,
441 so the above strictures don't apply. Hence the difference between
442 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
443 and tcSimplifyCheckBind (which does not).
445 What about when you supply a type signature for a binding?
446 Is it legal to give the following explicit, user type
447 signature to f, thus:
452 At first sight this seems reasonable, but it has the nasty property
453 that adding a type signature changes the dynamic semantics.
456 (let f x = (x::Int) + ?y
457 in (f 3, f 3 with ?y=5)) with ?y = 6
463 in (f 3, f 3 with ?y=5)) with ?y = 6
467 Indeed, simply inlining f (at the Haskell source level) would change the
470 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
471 semantics for a Haskell program without knowing its typing, so if you
472 change the typing you may change the semantics.
474 To make things consistent in all cases where we are *checking* against
475 a supplied signature (as opposed to inferring a type), we adopt the
478 a signature does not need to quantify over implicit params.
480 [This represents a (rather marginal) change of policy since GHC 5.02,
481 which *required* an explicit signature to quantify over all implicit
482 params for the reasons mentioned above.]
484 But that raises a new question. Consider
486 Given (signature) ?x::Int
487 Wanted (inferred) ?x::Int, ?y::Bool
489 Clearly we want to discharge the ?x and float the ?y out. But
490 what is the criterion that distinguishes them? Clearly it isn't
491 what free type variables they have. The Right Thing seems to be
492 to float a constraint that
493 neither mentions any of the quantified type variables
494 nor any of the quantified implicit parameters
496 See the predicate isFreeWhenChecking.
499 Question 3: monomorphism
500 ~~~~~~~~~~~~~~~~~~~~~~~~
501 There's a nasty corner case when the monomorphism restriction bites:
505 The argument above suggests that we *must* generalise
506 over the ?y parameter, to get
507 z :: (?y::Int) => Int,
508 but the monomorphism restriction says that we *must not*, giving
510 Why does the momomorphism restriction say this? Because if you have
512 let z = x + ?y in z+z
514 you might not expect the addition to be done twice --- but it will if
515 we follow the argument of Question 2 and generalise over ?y.
518 Question 4: top level
519 ~~~~~~~~~~~~~~~~~~~~~
520 At the top level, monomorhism makes no sense at all.
523 main = let ?x = 5 in print foo
527 woggle :: (?x :: Int) => Int -> Int
530 We definitely don't want (foo :: Int) with a top-level implicit parameter
531 (?x::Int) becuase there is no way to bind it.
536 (A) Always generalise over implicit parameters
537 Bindings that fall under the monomorphism restriction can't
541 * Inlining remains valid
542 * No unexpected loss of sharing
543 * But simple bindings like
545 will be rejected, unless you add an explicit type signature
546 (to avoid the monomorphism restriction)
547 z :: (?y::Int) => Int
549 This seems unacceptable
551 (B) Monomorphism restriction "wins"
552 Bindings that fall under the monomorphism restriction can't
554 Always generalise over implicit parameters *except* for bindings
555 that fall under the monomorphism restriction
558 * Inlining isn't valid in general
559 * No unexpected loss of sharing
560 * Simple bindings like
562 accepted (get value of ?y from binding site)
564 (C) Always generalise over implicit parameters
565 Bindings that fall under the monomorphism restriction can't
566 be generalised, EXCEPT for implicit parameters
568 * Inlining remains valid
569 * Unexpected loss of sharing (from the extra generalisation)
570 * Simple bindings like
572 accepted (get value of ?y from occurrence sites)
577 None of these choices seems very satisfactory. But at least we should
578 decide which we want to do.
580 It's really not clear what is the Right Thing To Do. If you see
584 would you expect the value of ?y to be got from the *occurrence sites*
585 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
586 case of function definitions, the answer is clearly the former, but
587 less so in the case of non-fucntion definitions. On the other hand,
588 if we say that we get the value of ?y from the definition site of 'z',
589 then inlining 'z' might change the semantics of the program.
591 Choice (C) really says "the monomorphism restriction doesn't apply
592 to implicit parameters". Which is fine, but remember that every
593 innocent binding 'x = ...' that mentions an implicit parameter in
594 the RHS becomes a *function* of that parameter, called at each
595 use of 'x'. Now, the chances are that there are no intervening 'with'
596 clauses that bind ?y, so a decent compiler should common up all
597 those function calls. So I think I strongly favour (C). Indeed,
598 one could make a similar argument for abolishing the monomorphism
599 restriction altogether.
601 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
605 %************************************************************************
607 \subsection{tcSimplifyInfer}
609 %************************************************************************
611 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
613 1. Compute Q = grow( fvs(T), C )
615 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
616 predicates will end up in Ct; we deal with them at the top level
618 3. Try improvement, using functional dependencies
620 4. If Step 3 did any unification, repeat from step 1
621 (Unification can change the result of 'grow'.)
623 Note: we don't reduce dictionaries in step 2. For example, if we have
624 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
625 after step 2. However note that we may therefore quantify over more
626 type variables than we absolutely have to.
628 For the guts, we need a loop, that alternates context reduction and
629 improvement with unification. E.g. Suppose we have
631 class C x y | x->y where ...
633 and tcSimplify is called with:
635 Then improvement unifies a with b, giving
638 If we need to unify anything, we rattle round the whole thing all over
645 -> TcTyVarSet -- fv(T); type vars
647 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
648 TcDictBinds, -- Bindings
649 [TcId]) -- Dict Ids that must be bound here (zonked)
650 -- Any free (escaping) Insts are tossed into the environment
655 tcSimplifyInfer doc tau_tvs wanted_lie
656 = inferLoop doc (varSetElems tau_tvs)
657 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
659 extendLIEs frees `thenM_`
660 returnM (qtvs, binds, map instToId irreds)
662 inferLoop doc tau_tvs wanteds
664 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
665 mappM zonkInst wanteds `thenM` \ wanteds' ->
666 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
668 preds = fdPredsOfInsts wanteds'
669 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
672 | isFreeWhenInferring qtvs inst = Free
673 | isClassDict inst = DontReduceUnlessConstant -- Dicts
674 | otherwise = ReduceMe NoSCs -- Lits and Methods
676 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
677 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
679 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
682 if no_improvement then
683 returnM (varSetElems qtvs, frees, binds, irreds)
685 -- If improvement did some unification, we go round again. There
686 -- are two subtleties:
687 -- a) We start again with irreds, not wanteds
688 -- Using an instance decl might have introduced a fresh type variable
689 -- which might have been unified, so we'd get an infinite loop
690 -- if we started again with wanteds! See example [LOOP]
692 -- b) It's also essential to re-process frees, because unification
693 -- might mean that a type variable that looked free isn't now.
695 -- Hence the (irreds ++ frees)
697 -- However, NOTICE that when we are done, we might have some bindings, but
698 -- the final qtvs might be empty. See [NO TYVARS] below.
700 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
701 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
706 class If b t e r | b t e -> r
709 class Lte a b c | a b -> c where lte :: a -> b -> c
711 instance (Lte a b l,If l b a c) => Max a b c
713 Wanted: Max Z (S x) y
715 Then we'll reduce using the Max instance to:
716 (Lte Z (S x) l, If l (S x) Z y)
717 and improve by binding l->T, after which we can do some reduction
718 on both the Lte and If constraints. What we *can't* do is start again
719 with (Max Z (S x) y)!
723 class Y a b | a -> b where
726 instance Y [[a]] a where
729 k :: X a -> X a -> X a
731 g :: Num a => [X a] -> [X a]
734 h ys = ys ++ map (k (y [[0]])) xs
736 The excitement comes when simplifying the bindings for h. Initially
737 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
738 From this we get t1:=:t2, but also various bindings. We can't forget
739 the bindings (because of [LOOP]), but in fact t1 is what g is
742 The net effect of [NO TYVARS]
745 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
746 isFreeWhenInferring qtvs inst
747 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
748 && isInheritableInst inst -- And no implicit parameter involved
749 -- (see "Notes on implicit parameters")
751 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
752 -> NameSet -- Quantified implicit parameters
754 isFreeWhenChecking qtvs ips inst
755 = isFreeWrtTyVars qtvs inst
756 && isFreeWrtIPs ips inst
758 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
759 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
763 %************************************************************************
765 \subsection{tcSimplifyCheck}
767 %************************************************************************
769 @tcSimplifyCheck@ is used when we know exactly the set of variables
770 we are going to quantify over. For example, a class or instance declaration.
775 -> [TcTyVar] -- Quantify over these
778 -> TcM TcDictBinds -- Bindings
780 -- tcSimplifyCheck is used when checking expression type signatures,
781 -- class decls, instance decls etc.
783 -- NB: tcSimplifyCheck does not consult the
784 -- global type variables in the environment; so you don't
785 -- need to worry about setting them before calling tcSimplifyCheck
786 tcSimplifyCheck doc qtvs givens wanted_lie
787 = ASSERT( all isSkolemTyVar qtvs )
788 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
792 -- get_qtvs = zonkTcTyVarsAndFV qtvs
793 get_qtvs = return (mkVarSet qtvs) -- All skolems
796 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
797 -- against, but we don't know the type variables over which we are going to quantify.
798 -- This happens when we have a type signature for a mutually recursive group
801 -> TcTyVarSet -- fv(T)
804 -> TcM ([TcTyVar], -- Variables over which to quantify
805 TcDictBinds) -- Bindings
807 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
808 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
810 ; return (qtvs', binds) }
812 -- Figure out which type variables to quantify over
813 -- You might think it should just be the signature tyvars,
814 -- but in bizarre cases you can get extra ones
815 -- f :: forall a. Num a => a -> a
816 -- f x = fst (g (x, head [])) + 1
818 -- Here we infer g :: forall a b. a -> b -> (b,a)
819 -- We don't want g to be monomorphic in b just because
820 -- f isn't quantified over b.
821 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
823 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
824 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
826 qtvs = all_tvs' `minusVarSet` gbl_tvs
827 -- We could close gbl_tvs, but its not necessary for
828 -- soundness, and it'll only affect which tyvars, not which
829 -- dictionaries, we quantify over
834 Here is the workhorse function for all three wrappers.
837 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
838 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
840 -- Complain about any irreducible ones
841 ; if not (null irreds)
842 then do { givens' <- mappM zonkInst given_dicts_and_ips
843 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
846 ; returnM (qtvs, frees, binds) }
848 given_dicts_and_ips = filter (not . isMethod) givens
849 -- For error reporting, filter out methods, which are
850 -- only added to the given set as an optimisation
852 ip_set = mkNameSet (ipNamesOfInsts givens)
854 check_loop givens wanteds
856 mappM zonkInst givens `thenM` \ givens' ->
857 mappM zonkInst wanteds `thenM` \ wanteds' ->
858 get_qtvs `thenM` \ qtvs' ->
862 -- When checking against a given signature we always reduce
863 -- until we find a match against something given, or can't reduce
864 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
865 | otherwise = ReduceMe want_scs
867 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
870 if no_improvement then
871 returnM (varSetElems qtvs', frees, binds, irreds)
873 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
874 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
878 %************************************************************************
880 tcSimplifySuperClasses
882 %************************************************************************
884 Note [SUPERCLASS-LOOP 1]
885 ~~~~~~~~~~~~~~~~~~~~~~~~
886 We have to be very, very careful when generating superclasses, lest we
887 accidentally build a loop. Here's an example:
891 class S a => C a where { opc :: a -> a }
892 class S b => D b where { opd :: b -> b }
900 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
901 Simplifying, we may well get:
902 $dfCInt = :C ds1 (opd dd)
905 Notice that we spot that we can extract ds1 from dd.
907 Alas! Alack! We can do the same for (instance D Int):
909 $dfDInt = :D ds2 (opc dc)
913 And now we've defined the superclass in terms of itself.
915 Solution: never generate a superclass selectors at all when
916 satisfying the superclass context of an instance declaration.
918 Two more nasty cases are in
923 tcSimplifySuperClasses qtvs givens sc_wanteds
924 = ASSERT( all isSkolemTyVar qtvs )
925 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
926 ; binds2 <- tc_simplify_top doc False NoSCs frees
927 ; return (binds1 `unionBags` binds2) }
929 get_qtvs = return (mkVarSet qtvs)
930 doc = ptext SLIT("instance declaration superclass context")
934 %************************************************************************
936 \subsection{tcSimplifyRestricted}
938 %************************************************************************
940 tcSimplifyRestricted infers which type variables to quantify for a
941 group of restricted bindings. This isn't trivial.
944 We want to quantify over a to get id :: forall a. a->a
947 We do not want to quantify over a, because there's an Eq a
948 constraint, so we get eq :: a->a->Bool (notice no forall)
951 RHS has type 'tau', whose free tyvars are tau_tvs
952 RHS has constraints 'wanteds'
955 Quantify over (tau_tvs \ ftvs(wanteds))
956 This is bad. The constraints may contain (Monad (ST s))
957 where we have instance Monad (ST s) where...
958 so there's no need to be monomorphic in s!
960 Also the constraint might be a method constraint,
961 whose type mentions a perfectly innocent tyvar:
962 op :: Num a => a -> b -> a
963 Here, b is unconstrained. A good example would be
965 We want to infer the polymorphic type
966 foo :: forall b. b -> b
969 Plan B (cunning, used for a long time up to and including GHC 6.2)
970 Step 1: Simplify the constraints as much as possible (to deal
971 with Plan A's problem). Then set
972 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
974 Step 2: Now simplify again, treating the constraint as 'free' if
975 it does not mention qtvs, and trying to reduce it otherwise.
976 The reasons for this is to maximise sharing.
978 This fails for a very subtle reason. Suppose that in the Step 2
979 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
980 In the Step 1 this constraint might have been simplified, perhaps to
981 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
982 This won't happen in Step 2... but that in turn might prevent some other
983 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
984 and that in turn breaks the invariant that no constraints are quantified over.
986 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
991 Step 1: Simplify the constraints as much as possible (to deal
992 with Plan A's problem). Then set
993 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
994 Return the bindings from Step 1.
997 A note about Plan C (arising from "bug" reported by George Russel March 2004)
1000 instance (HasBinary ty IO) => HasCodedValue ty
1002 foo :: HasCodedValue a => String -> IO a
1004 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1005 doDecodeIO codedValue view
1006 = let { act = foo "foo" } in act
1008 You might think this should work becuase the call to foo gives rise to a constraint
1009 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1010 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1011 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1013 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1017 Plan D (a variant of plan B)
1018 Step 1: Simplify the constraints as much as possible (to deal
1019 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1020 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1022 Step 2: Now simplify again, treating the constraint as 'free' if
1023 it does not mention qtvs, and trying to reduce it otherwise.
1025 The point here is that it's generally OK to have too few qtvs; that is,
1026 to make the thing more monomorphic than it could be. We don't want to
1027 do that in the common cases, but in wierd cases it's ok: the programmer
1028 can always add a signature.
1030 Too few qtvs => too many wanteds, which is what happens if you do less
1035 tcSimplifyRestricted -- Used for restricted binding groups
1036 -- i.e. ones subject to the monomorphism restriction
1039 -> [Name] -- Things bound in this group
1040 -> TcTyVarSet -- Free in the type of the RHSs
1041 -> [Inst] -- Free in the RHSs
1042 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1043 TcDictBinds) -- Bindings
1044 -- tcSimpifyRestricted returns no constraints to
1045 -- quantify over; by definition there are none.
1046 -- They are all thrown back in the LIE
1048 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1049 -- Zonk everything in sight
1050 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1051 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1052 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1054 -- 'reduceMe': Reduce as far as we can. Don't stop at
1055 -- dicts; the idea is to get rid of as many type
1056 -- variables as possible, and we don't want to stop
1057 -- at (say) Monad (ST s), because that reduces
1058 -- immediately, with no constraint on s.
1060 -- BUT do no improvement! See Plan D above
1061 reduceContextWithoutImprovement
1062 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1064 -- Next, figure out the tyvars we will quantify over
1066 constrained_tvs = tyVarsOfInsts constrained_dicts
1067 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1068 `minusVarSet` constrained_tvs
1070 traceTc (text "tcSimplifyRestricted" <+> vcat [
1071 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1073 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1075 -- The first step may have squashed more methods than
1076 -- necessary, so try again, this time more gently, knowing the exact
1077 -- set of type variables to quantify over.
1079 -- We quantify only over constraints that are captured by qtvs;
1080 -- these will just be a subset of non-dicts. This in contrast
1081 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1082 -- all *non-inheritable* constraints too. This implements choice
1083 -- (B) under "implicit parameter and monomorphism" above.
1085 -- Remember that we may need to do *some* simplification, to
1086 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1087 -- just to float all constraints
1089 -- At top level, we *do* squash methods becuase we want to
1090 -- expose implicit parameters to the test that follows
1092 is_nested_group = isNotTopLevel top_lvl
1093 try_me inst | isFreeWrtTyVars qtvs inst,
1094 (is_nested_group || isDict inst) = Free
1095 | otherwise = ReduceMe AddSCs
1097 reduceContextWithoutImprovement
1098 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1099 ASSERT( null irreds )
1101 -- See "Notes on implicit parameters, Question 4: top level"
1102 if is_nested_group then
1103 extendLIEs frees `thenM_`
1104 returnM (varSetElems qtvs, binds)
1107 (non_ips, bad_ips) = partition isClassDict frees
1109 addTopIPErrs bndrs bad_ips `thenM_`
1110 extendLIEs non_ips `thenM_`
1111 returnM (varSetElems qtvs, binds)
1115 %************************************************************************
1119 %************************************************************************
1121 On the LHS of transformation rules we only simplify methods and constants,
1122 getting dictionaries. We want to keep all of them unsimplified, to serve
1123 as the available stuff for the RHS of the rule.
1125 Example. Consider the following left-hand side of a rule
1127 f (x == y) (y > z) = ...
1129 If we typecheck this expression we get constraints
1131 d1 :: Ord a, d2 :: Eq a
1133 We do NOT want to "simplify" to the LHS
1135 forall x::a, y::a, z::a, d1::Ord a.
1136 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1140 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1141 f ((==) d2 x y) ((>) d1 y z) = ...
1143 Here is another example:
1145 fromIntegral :: (Integral a, Num b) => a -> b
1146 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1148 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1149 we *dont* want to get
1151 forall dIntegralInt.
1152 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1154 because the scsel will mess up RULE matching. Instead we want
1156 forall dIntegralInt, dNumInt.
1157 fromIntegral Int Int dIntegralInt dNumInt = id Int
1161 g (x == y) (y == z) = ..
1163 where the two dictionaries are *identical*, we do NOT WANT
1165 forall x::a, y::a, z::a, d1::Eq a
1166 f ((==) d1 x y) ((>) d1 y z) = ...
1168 because that will only match if the dict args are (visibly) equal.
1169 Instead we want to quantify over the dictionaries separately.
1171 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1172 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1173 from scratch, rather than further parameterise simpleReduceLoop etc
1176 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1177 tcSimplifyRuleLhs wanteds
1178 = go [] emptyBag wanteds
1181 = return (dicts, binds)
1182 go dicts binds (w:ws)
1184 = go (w:dicts) binds ws
1186 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1187 -- to fromInteger; this looks fragile to me
1188 ; lookup_result <- lookupInst w'
1189 ; case lookup_result of
1190 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
1191 SimpleInst rhs -> go dicts (addBind binds w rhs) ws
1192 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1196 tcSimplifyBracket is used when simplifying the constraints arising from
1197 a Template Haskell bracket [| ... |]. We want to check that there aren't
1198 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1199 Show instance), but we aren't otherwise interested in the results.
1200 Nor do we care about ambiguous dictionaries etc. We will type check
1201 this bracket again at its usage site.
1204 tcSimplifyBracket :: [Inst] -> TcM ()
1205 tcSimplifyBracket wanteds
1206 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1209 doc = text "tcSimplifyBracket"
1213 %************************************************************************
1215 \subsection{Filtering at a dynamic binding}
1217 %************************************************************************
1222 we must discharge all the ?x constraints from B. We also do an improvement
1223 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1225 Actually, the constraints from B might improve the types in ?x. For example
1227 f :: (?x::Int) => Char -> Char
1230 then the constraint (?x::Int) arising from the call to f will
1231 force the binding for ?x to be of type Int.
1234 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1237 tcSimplifyIPs given_ips wanteds
1238 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1239 extendLIEs frees `thenM_`
1242 doc = text "tcSimplifyIPs" <+> ppr given_ips
1243 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1245 -- Simplify any methods that mention the implicit parameter
1246 try_me inst | isFreeWrtIPs ip_set inst = Free
1247 | otherwise = ReduceMe NoSCs
1249 simpl_loop givens wanteds
1250 = mappM zonkInst givens `thenM` \ givens' ->
1251 mappM zonkInst wanteds `thenM` \ wanteds' ->
1253 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1255 if no_improvement then
1256 ASSERT( null irreds )
1257 returnM (frees, binds)
1259 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1260 returnM (frees1, binds `unionBags` binds1)
1264 %************************************************************************
1266 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1268 %************************************************************************
1270 When doing a binding group, we may have @Insts@ of local functions.
1271 For example, we might have...
1273 let f x = x + 1 -- orig local function (overloaded)
1274 f.1 = f Int -- two instances of f
1279 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1280 where @f@ is in scope; those @Insts@ must certainly not be passed
1281 upwards towards the top-level. If the @Insts@ were binding-ified up
1282 there, they would have unresolvable references to @f@.
1284 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1285 For each method @Inst@ in the @init_lie@ that mentions one of the
1286 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1287 @LIE@), as well as the @HsBinds@ generated.
1290 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1291 -- Simlifies only MethodInsts, and generate only bindings of form
1293 -- We're careful not to even generate bindings of the form
1295 -- You'd think that'd be fine, but it interacts with what is
1296 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1298 bindInstsOfLocalFuns wanteds local_ids
1299 | null overloaded_ids
1301 = extendLIEs wanteds `thenM_`
1302 returnM emptyLHsBinds
1305 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1306 ASSERT( null irreds )
1307 extendLIEs not_for_me `thenM_`
1308 extendLIEs frees `thenM_`
1311 doc = text "bindInsts" <+> ppr local_ids
1312 overloaded_ids = filter is_overloaded local_ids
1313 is_overloaded id = isOverloadedTy (idType id)
1314 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1316 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1317 -- so it's worth building a set, so that
1318 -- lookup (in isMethodFor) is faster
1319 try_me inst | isMethod inst = ReduceMe NoSCs
1324 %************************************************************************
1326 \subsection{Data types for the reduction mechanism}
1328 %************************************************************************
1330 The main control over context reduction is here
1334 = ReduceMe WantSCs -- Try to reduce this
1335 -- If there's no instance, behave exactly like
1336 -- DontReduce: add the inst to the irreductible ones,
1337 -- but don't produce an error message of any kind.
1338 -- It might be quite legitimate such as (Eq a)!
1340 | DontReduceUnlessConstant -- Return as irreducible unless it can
1341 -- be reduced to a constant in one step
1343 | Free -- Return as free
1345 reduceMe :: Inst -> WhatToDo
1346 reduceMe inst = ReduceMe AddSCs
1348 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1349 -- of a predicate when adding it to the avails
1350 -- The reason for this flag is entirely the super-class loop problem
1351 -- Note [SUPER-CLASS LOOP 1]
1357 type Avails = FiniteMap Inst Avail
1358 emptyAvails = emptyFM
1361 = IsFree -- Used for free Insts
1362 | Irred -- Used for irreducible dictionaries,
1363 -- which are going to be lambda bound
1365 | Given TcId -- Used for dictionaries for which we have a binding
1366 -- e.g. those "given" in a signature
1367 Bool -- True <=> actually consumed (splittable IPs only)
1369 | Rhs -- Used when there is a RHS
1370 (LHsExpr TcId) -- The RHS
1371 [Inst] -- Insts free in the RHS; we need these too
1373 | Linear -- Splittable Insts only.
1374 Int -- The Int is always 2 or more; indicates how
1375 -- many copies are required
1376 Inst -- The splitter
1377 Avail -- Where the "master copy" is
1379 | LinRhss -- Splittable Insts only; this is used only internally
1380 -- by extractResults, where a Linear
1381 -- is turned into an LinRhss
1382 [LHsExpr TcId] -- A supply of suitable RHSs
1384 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1385 | (inst,avail) <- fmToList avails ]
1387 instance Outputable Avail where
1390 pprAvail IsFree = text "Free"
1391 pprAvail Irred = text "Irred"
1392 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1393 if b then text "(used)" else empty
1394 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1395 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1396 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1399 Extracting the bindings from a bunch of Avails.
1400 The bindings do *not* come back sorted in dependency order.
1401 We assume that they'll be wrapped in a big Rec, so that the
1402 dependency analyser can sort them out later
1406 extractResults :: Avails
1408 -> TcM (TcDictBinds, -- Bindings
1409 [Inst], -- Irreducible ones
1410 [Inst]) -- Free ones
1412 extractResults avails wanteds
1413 = go avails emptyBag [] [] wanteds
1415 go avails binds irreds frees []
1416 = returnM (binds, irreds, frees)
1418 go avails binds irreds frees (w:ws)
1419 = case lookupFM avails w of
1420 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1421 go avails binds irreds frees ws
1423 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1424 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1426 Just (Given id _) -> go avails new_binds irreds frees ws
1428 new_binds | id == instToId w = binds
1429 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1430 -- The sought Id can be one of the givens, via a superclass chain
1431 -- and then we definitely don't want to generate an x=x binding!
1433 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1435 new_binds = addBind binds w rhs
1437 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1438 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1439 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1440 go (addToFM avails w (LinRhss rhss))
1441 (binds `unionBags` binds')
1442 irreds' frees' (split_inst : w : ws)
1444 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1445 -> go new_avails new_binds irreds frees ws
1447 new_binds = addBind binds w rhs
1448 new_avails = addToFM avails w (LinRhss rhss)
1450 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1451 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1452 returnM (w':irreds, frees, instToId w')
1453 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1454 returnM (irreds, w':frees, instToId w')
1456 add_given avails w = addToFM avails w (Given (instToId w) True)
1458 add_free avails w | isMethod w = avails
1459 | otherwise = add_given avails w
1461 -- Do *not* replace Free by Given if it's a method.
1462 -- The following situation shows why this is bad:
1463 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1464 -- From an application (truncate f i) we get
1465 -- t1 = truncate at f
1467 -- If we have also have a second occurrence of truncate, we get
1468 -- t3 = truncate at f
1470 -- When simplifying with i,f free, we might still notice that
1471 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1472 -- will continue to float out!
1474 split :: Int -> TcId -> TcId -> Inst
1475 -> TcM (TcDictBinds, [LHsExpr TcId])
1476 -- (split n split_id root_id wanted) returns
1477 -- * a list of 'n' expressions, all of which witness 'avail'
1478 -- * a bunch of auxiliary bindings to support these expressions
1479 -- * one or zero insts needed to witness the whole lot
1480 -- (maybe be zero if the initial Inst is a Given)
1482 -- NB: 'wanted' is just a template
1484 split n split_id root_id wanted
1487 ty = linearInstType wanted
1488 pair_ty = mkTyConApp pairTyCon [ty,ty]
1489 id = instToId wanted
1492 span = instSpan wanted
1494 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1496 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1497 expand n rhss `thenM` \ (binds2, rhss') ->
1498 returnM (binds1 `unionBags` binds2, rhss')
1501 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1502 -- e.g. expand 3 [rhs1, rhs2]
1503 -- = ( { x = split rhs1 },
1504 -- [fst x, snd x, rhs2] )
1506 | n `rem` 2 == 0 = go rhss -- n is even
1507 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1508 returnM (binds', head rhss : rhss')
1510 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1511 returnM (listToBag binds', concat rhss')
1513 do_one rhs = newUnique `thenM` \ uniq ->
1514 tcLookupId fstName `thenM` \ fst_id ->
1515 tcLookupId sndName `thenM` \ snd_id ->
1517 x = mkUserLocal occ uniq pair_ty loc
1519 returnM (L span (VarBind x (mk_app span split_id rhs)),
1520 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1522 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1524 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1526 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1527 (VarBind (instToId inst) rhs))
1528 instSpan wanted = instLocSrcSpan (instLoc wanted)
1532 %************************************************************************
1534 \subsection[reduce]{@reduce@}
1536 %************************************************************************
1538 When the "what to do" predicate doesn't depend on the quantified type variables,
1539 matters are easier. We don't need to do any zonking, unless the improvement step
1540 does something, in which case we zonk before iterating.
1542 The "given" set is always empty.
1545 simpleReduceLoop :: SDoc
1546 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1548 -> TcM ([Inst], -- Free
1550 [Inst]) -- Irreducible
1552 simpleReduceLoop doc try_me wanteds
1553 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1554 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1555 if no_improvement then
1556 returnM (frees, binds, irreds)
1558 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1559 returnM (frees1, binds `unionBags` binds1, irreds1)
1565 reduceContext :: SDoc
1566 -> (Inst -> WhatToDo)
1569 -> TcM (Bool, -- True <=> improve step did no unification
1571 TcDictBinds, -- Dictionary bindings
1572 [Inst]) -- Irreducible
1574 reduceContext doc try_me givens wanteds
1576 traceTc (text "reduceContext" <+> (vcat [
1577 text "----------------------",
1579 text "given" <+> ppr givens,
1580 text "wanted" <+> ppr wanteds,
1581 text "----------------------"
1584 -- Build the Avail mapping from "givens"
1585 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1588 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1590 -- Do improvement, using everything in avails
1591 -- In particular, avails includes all superclasses of everything
1592 tcImprove avails `thenM` \ no_improvement ->
1594 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1596 traceTc (text "reduceContext end" <+> (vcat [
1597 text "----------------------",
1599 text "given" <+> ppr givens,
1600 text "wanted" <+> ppr wanteds,
1602 text "avails" <+> pprAvails avails,
1603 text "frees" <+> ppr frees,
1604 text "no_improvement =" <+> ppr no_improvement,
1605 text "----------------------"
1608 returnM (no_improvement, frees, binds, irreds)
1610 -- reduceContextWithoutImprovement differs from reduceContext
1611 -- (a) no improvement
1612 -- (b) 'givens' is assumed empty
1613 reduceContextWithoutImprovement doc try_me wanteds
1615 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1616 text "----------------------",
1618 text "wanted" <+> ppr wanteds,
1619 text "----------------------"
1623 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1624 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1626 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1627 text "----------------------",
1629 text "wanted" <+> ppr wanteds,
1631 text "avails" <+> pprAvails avails,
1632 text "frees" <+> ppr frees,
1633 text "----------------------"
1636 returnM (frees, binds, irreds)
1638 tcImprove :: Avails -> TcM Bool -- False <=> no change
1639 -- Perform improvement using all the predicates in Avails
1641 = tcGetInstEnvs `thenM` \ inst_envs ->
1643 preds = [ (pred, pp_loc)
1644 | (inst, avail) <- fmToList avails,
1645 pred <- get_preds inst avail,
1646 let pp_loc = pprInstLoc (instLoc inst)
1648 -- Avails has all the superclasses etc (good)
1649 -- It also has all the intermediates of the deduction (good)
1650 -- It does not have duplicates (good)
1651 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1652 -- so that improve will see them separate
1654 -- For free Methods, we want to take predicates from their context,
1655 -- but for Methods that have been squished their context will already
1656 -- be in Avails, and we don't want duplicates. Hence this rather
1657 -- horrid get_preds function
1658 get_preds inst IsFree = fdPredsOfInst inst
1659 get_preds inst other | isDict inst = [dictPred inst]
1662 eqns = improve get_insts preds
1663 get_insts clas = classInstances inst_envs clas
1668 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1669 mappM_ unify eqns `thenM_`
1672 unify ((qtvs, pairs), what1, what2)
1673 = addErrCtxtM (mkEqnMsg what1 what2) $
1674 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1675 mapM_ (unif_pr tenv) pairs
1676 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1678 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1680 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1681 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1682 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1683 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1684 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1685 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1686 ; return (tidy_env, msg) }
1689 The main context-reduction function is @reduce@. Here's its game plan.
1692 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1693 -- along with its depth
1694 -> (Inst -> WhatToDo)
1701 try_me: given an inst, this function returns
1703 DontReduce return this in "irreds"
1704 Free return this in "frees"
1706 wanteds: The list of insts to reduce
1707 state: An accumulating parameter of type Avails
1708 that contains the state of the algorithm
1710 It returns a Avails.
1712 The (n,stack) pair is just used for error reporting.
1713 n is always the depth of the stack.
1714 The stack is the stack of Insts being reduced: to produce X
1715 I had to produce Y, to produce Y I had to produce Z, and so on.
1718 reduceList (n,stack) try_me wanteds state
1719 | n > opt_MaxContextReductionDepth
1720 = failWithTc (reduceDepthErr n stack)
1726 pprTrace "Interesting! Context reduction stack deeper than 8:"
1727 (int n $$ ifPprDebug (nest 2 (pprStack stack)))
1732 go [] state = returnM state
1733 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1736 -- Base case: we're done!
1737 reduce stack try_me wanted avails
1738 -- It's the same as an existing inst, or a superclass thereof
1739 | Just avail <- isAvailable avails wanted
1740 = if isLinearInst wanted then
1741 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1742 reduceList stack try_me wanteds' avails'
1744 returnM avails -- No op for non-linear things
1747 = case try_me wanted of {
1749 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1750 -- First, see if the inst can be reduced to a constant in one step
1751 try_simple (addIrred AddSCs) -- Assume want superclasses
1753 ; Free -> -- It's free so just chuck it upstairs
1754 -- First, see if the inst can be reduced to a constant in one step
1757 ; ReduceMe want_scs -> -- It should be reduced
1758 lookupInst wanted `thenM` \ lookup_result ->
1759 case lookup_result of
1760 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1761 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1762 addWanted want_scs avails2 wanted rhs wanteds'
1763 -- Experiment with temporarily doing addIrred *before* the reduceList,
1764 -- which has the effect of adding the thing we are trying
1765 -- to prove to the database before trying to prove the things it
1766 -- needs. See note [RECURSIVE DICTIONARIES]
1767 -- NB: we must not do an addWanted before, because that adds the
1768 -- superclasses too, and thaat can lead to a spurious loop; see
1769 -- the examples in [SUPERCLASS-LOOP]
1770 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1772 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1774 NoInstance -> -- No such instance!
1775 -- Add it and its superclasses
1776 addIrred want_scs avails wanted
1779 try_simple do_this_otherwise
1780 = lookupInst wanted `thenM` \ lookup_result ->
1781 case lookup_result of
1782 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1783 other -> do_this_otherwise avails wanted
1788 -------------------------
1789 isAvailable :: Avails -> Inst -> Maybe Avail
1790 isAvailable avails wanted = lookupFM avails wanted
1791 -- NB 1: the Ord instance of Inst compares by the class/type info
1792 -- *not* by unique. So
1793 -- d1::C Int == d2::C Int
1795 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1796 addLinearAvailable avails avail wanted
1797 -- avails currently maps [wanted -> avail]
1798 -- Extend avails to reflect a neeed for an extra copy of avail
1800 | Just avail' <- split_avail avail
1801 = returnM (addToFM avails wanted avail', [])
1804 = tcLookupId splitName `thenM` \ split_id ->
1805 tcInstClassOp (instLoc wanted) split_id
1806 [linearInstType wanted] `thenM` \ split_inst ->
1807 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1810 split_avail :: Avail -> Maybe Avail
1811 -- (Just av) if there's a modified version of avail that
1812 -- we can use to replace avail in avails
1813 -- Nothing if there isn't, so we need to create a Linear
1814 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1815 split_avail (Given id used) | not used = Just (Given id True)
1816 | otherwise = Nothing
1817 split_avail Irred = Nothing
1818 split_avail IsFree = Nothing
1819 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1821 -------------------------
1822 addFree :: Avails -> Inst -> TcM Avails
1823 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1824 -- to avails, so that any other equal Insts will be commoned up right
1825 -- here rather than also being tossed upstairs. This is really just
1826 -- an optimisation, and perhaps it is more trouble that it is worth,
1827 -- as the following comments show!
1829 -- NB: do *not* add superclasses. If we have
1832 -- but a is not bound here, then we *don't* want to derive
1833 -- dn from df here lest we lose sharing.
1835 addFree avails free = returnM (addToFM avails free IsFree)
1837 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1838 addWanted want_scs avails wanted rhs_expr wanteds
1839 = addAvailAndSCs want_scs avails wanted avail
1841 avail = Rhs rhs_expr wanteds
1843 addGiven :: Avails -> Inst -> TcM Avails
1844 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1845 -- Always add superclasses for 'givens'
1847 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1848 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1849 -- so the assert isn't true
1851 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1852 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1853 addAvailAndSCs want_scs avails irred Irred
1855 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1856 addAvailAndSCs want_scs avails inst avail
1857 | not (isClassDict inst) = return avails_with_inst
1858 | NoSCs <- want_scs = return avails_with_inst
1859 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1860 ; addSCs is_loop avails_with_inst inst }
1862 avails_with_inst = addToFM avails inst avail
1864 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1865 -- Note: this compares by *type*, not by Unique
1866 deps = findAllDeps (unitVarSet (instToId inst)) avail
1867 dep_tys = map idType (varSetElems deps)
1869 findAllDeps :: IdSet -> Avail -> IdSet
1870 -- Find all the Insts that this one depends on
1871 -- See Note [SUPERCLASS-LOOP 2]
1872 -- Watch out, though. Since the avails may contain loops
1873 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1874 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1875 findAllDeps so_far other = so_far
1877 find_all :: IdSet -> Inst -> IdSet
1879 | kid_id `elemVarSet` so_far = so_far
1880 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1881 | otherwise = so_far'
1883 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1884 kid_id = instToId kid
1886 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1887 -- Add all the superclasses of the Inst to Avails
1888 -- The first param says "dont do this because the original thing
1889 -- depends on this one, so you'd build a loop"
1890 -- Invariant: the Inst is already in Avails.
1892 addSCs is_loop avails dict
1893 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1894 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1896 (clas, tys) = getDictClassTys dict
1897 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1898 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1900 add_sc avails (sc_dict, sc_sel)
1901 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1902 | is_given sc_dict = return avails
1903 | otherwise = addSCs is_loop avails' sc_dict
1905 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1906 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1908 is_given :: Inst -> Bool
1909 is_given sc_dict = case lookupFM avails sc_dict of
1910 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1914 Note [SUPERCLASS-LOOP 2]
1915 ~~~~~~~~~~~~~~~~~~~~~~~~
1916 But the above isn't enough. Suppose we are *given* d1:Ord a,
1917 and want to deduce (d2:C [a]) where
1919 class Ord a => C a where
1920 instance Ord [a] => C [a] where ...
1922 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1923 superclasses of C [a] to avails. But we must not overwrite the binding
1924 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1927 Here's another variant, immortalised in tcrun020
1928 class Monad m => C1 m
1929 class C1 m => C2 m x
1930 instance C2 Maybe Bool
1931 For the instance decl we need to build (C1 Maybe), and it's no good if
1932 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1933 before we search for C1 Maybe.
1935 Here's another example
1936 class Eq b => Foo a b
1937 instance Eq a => Foo [a] a
1941 we'll first deduce that it holds (via the instance decl). We must not
1942 then overwrite the Eq t constraint with a superclass selection!
1944 At first I had a gross hack, whereby I simply did not add superclass constraints
1945 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1946 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1947 I found a very obscure program (now tcrun021) in which improvement meant the
1948 simplifier got two bites a the cherry... so something seemed to be an Irred
1949 first time, but reducible next time.
1951 Now we implement the Right Solution, which is to check for loops directly
1952 when adding superclasses. It's a bit like the occurs check in unification.
1955 Note [RECURSIVE DICTIONARIES]
1956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1958 data D r = ZeroD | SuccD (r (D r));
1960 instance (Eq (r (D r))) => Eq (D r) where
1961 ZeroD == ZeroD = True
1962 (SuccD a) == (SuccD b) = a == b
1965 equalDC :: D [] -> D [] -> Bool;
1968 We need to prove (Eq (D [])). Here's how we go:
1972 by instance decl, holds if
1976 by instance decl of Eq, holds if
1978 where d2 = dfEqList d3
1981 But now we can "tie the knot" to give
1987 and it'll even run! The trick is to put the thing we are trying to prove
1988 (in this case Eq (D []) into the database before trying to prove its
1989 contributing clauses.
1992 %************************************************************************
1994 \section{tcSimplifyTop: defaulting}
1996 %************************************************************************
1999 @tcSimplifyTop@ is called once per module to simplify all the constant
2000 and ambiguous Insts.
2002 We need to be careful of one case. Suppose we have
2004 instance Num a => Num (Foo a b) where ...
2006 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2007 to (Num x), and default x to Int. But what about y??
2009 It's OK: the final zonking stage should zap y to (), which is fine.
2013 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2014 tcSimplifyTop wanteds
2015 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2017 doc = text "tcSimplifyTop"
2019 tcSimplifyInteractive wanteds
2020 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2022 doc = text "tcSimplifyTop"
2024 -- The TcLclEnv should be valid here, solely to improve
2025 -- error message generation for the monomorphism restriction
2026 tc_simplify_top doc is_interactive want_scs wanteds
2027 = do { lcl_env <- getLclEnv
2028 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2030 ; let try_me inst = ReduceMe want_scs
2031 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2034 -- First get rid of implicit parameters
2035 (non_ips, bad_ips) = partition isClassDict irreds
2037 -- All the non-tv or multi-param ones are definite errors
2038 (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
2039 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2041 -- Group by type variable
2042 tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
2044 -- Pick the ones which its worth trying to disambiguate
2045 -- namely, the ones whose type variable isn't bound
2046 -- up with one of the non-tyvar classes
2047 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2048 defaultable_group ds
2049 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
2050 && defaultable_classes (map get_clas ds)
2051 defaultable_classes clss
2052 | is_interactive = any isInteractiveClass clss
2053 | otherwise = all isStandardClass clss && any isNumericClass clss
2055 isInteractiveClass cls = isNumericClass cls
2056 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2057 -- In interactive mode, we default Show a to Show ()
2058 -- to avoid graututious errors on "show []"
2061 -- Collect together all the bad guys
2062 bad_guys = non_tvs ++ concat non_default_gps
2063 (ambigs, no_insts) = partition isTyVarDict bad_guys
2064 -- If the dict has no type constructors involved, it must be ambiguous,
2065 -- except I suppose that another error with fundeps maybe should have
2066 -- constrained those type variables
2068 -- Report definite errors
2069 ; ASSERT( null frees )
2070 groupErrs (addNoInstanceErrs Nothing []) no_insts
2071 ; strangeTopIPErrs bad_ips
2073 -- Deal with ambiguity errors, but only if
2074 -- if there has not been an error so far:
2075 -- errors often give rise to spurious ambiguous Insts.
2077 -- f = (*) -- Monomorphic
2078 -- g :: Num a => a -> a
2080 -- Here, we get a complaint when checking the type signature for g,
2081 -- that g isn't polymorphic enough; but then we get another one when
2082 -- dealing with the (Num a) context arising from f's definition;
2083 -- we try to unify a with Int (to default it), but find that it's
2084 -- already been unified with the rigid variable from g's type sig
2085 ; binds_ambig <- ifErrsM (returnM []) $
2086 do { -- Complain about the ones that don't fall under
2087 -- the Haskell rules for disambiguation
2088 -- This group includes both non-existent instances
2089 -- e.g. Num (IO a) and Eq (Int -> Int)
2090 -- and ambiguous dictionaries
2092 addTopAmbigErrs ambigs
2094 -- Disambiguate the ones that look feasible
2095 ; mappM disambigGroup default_gps }
2097 ; return (binds `unionBags` unionManyBags binds_ambig) }
2099 ----------------------------------
2100 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2102 is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
2103 -- Invariant: argument is a ClassDict, not IP or method
2104 is_unary_tyvar_dict d = case getDictClassTys d of
2105 (_, [ty]) -> tcIsTyVarTy ty
2108 get_tv d = case getDictClassTys d of
2109 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2110 get_clas d = case getDictClassTys d of
2114 If a dictionary constrains a type variable which is
2115 * not mentioned in the environment
2116 * and not mentioned in the type of the expression
2117 then it is ambiguous. No further information will arise to instantiate
2118 the type variable; nor will it be generalised and turned into an extra
2119 parameter to a function.
2121 It is an error for this to occur, except that Haskell provided for
2122 certain rules to be applied in the special case of numeric types.
2124 * at least one of its classes is a numeric class, and
2125 * all of its classes are numeric or standard
2126 then the type variable can be defaulted to the first type in the
2127 default-type list which is an instance of all the offending classes.
2129 So here is the function which does the work. It takes the ambiguous
2130 dictionaries and either resolves them (producing bindings) or
2131 complains. It works by splitting the dictionary list by type
2132 variable, and using @disambigOne@ to do the real business.
2134 @disambigOne@ assumes that its arguments dictionaries constrain all
2135 the same type variable.
2137 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2138 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2139 the most common use of defaulting is code like:
2141 _ccall_ foo `seqPrimIO` bar
2143 Since we're not using the result of @foo@, the result if (presumably)
2147 disambigGroup :: [Inst] -- All standard classes of form (C a)
2151 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2152 -- SO, TRY DEFAULT TYPES IN ORDER
2154 -- Failure here is caused by there being no type in the
2155 -- default list which can satisfy all the ambiguous classes.
2156 -- For example, if Real a is reqd, but the only type in the
2157 -- default list is Int.
2158 get_default_tys `thenM` \ default_tys ->
2160 try_default [] -- No defaults work, so fail
2163 try_default (default_ty : default_tys)
2164 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2165 -- default_tys instead
2166 tcSimplifyDefault theta `thenM` \ _ ->
2169 theta = [mkClassPred clas [default_ty] | clas <- classes]
2171 -- See if any default works
2172 tryM (try_default default_tys) `thenM` \ mb_ty ->
2175 Right chosen_default_ty -> choose_default chosen_default_ty
2177 tyvar = get_tv (head dicts) -- Should be non-empty
2178 classes = map get_clas dicts
2180 choose_default default_ty -- Commit to tyvar = default_ty
2181 = -- Bind the type variable
2182 unifyType default_ty (mkTyVarTy tyvar) `thenM_`
2183 -- and reduce the context, for real this time
2184 simpleReduceLoop (text "disambig" <+> ppr dicts)
2185 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2186 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2187 warnDefault dicts default_ty `thenM_`
2190 bomb_out = addTopAmbigErrs dicts `thenM_`
2194 = do { mb_defaults <- getDefaultTys
2195 ; case mb_defaults of
2196 Just tys -> return tys
2197 Nothing -> -- No use-supplied default;
2198 -- use [Integer, Double]
2199 do { integer_ty <- tcMetaTy integerTyConName
2200 ; checkWiredInTyCon doubleTyCon
2201 ; return [integer_ty, doubleTy] } }
2204 [Aside - why the defaulting mechanism is turned off when
2205 dealing with arguments and results to ccalls.
2207 When typechecking _ccall_s, TcExpr ensures that the external
2208 function is only passed arguments (and in the other direction,
2209 results) of a restricted set of 'native' types.
2211 The interaction between the defaulting mechanism for numeric
2212 values and CC & CR can be a bit puzzling to the user at times.
2221 What type has 'x' got here? That depends on the default list
2222 in operation, if it is equal to Haskell 98's default-default
2223 of (Integer, Double), 'x' has type Double, since Integer
2224 is not an instance of CR. If the default list is equal to
2225 Haskell 1.4's default-default of (Int, Double), 'x' has type
2231 %************************************************************************
2233 \subsection[simple]{@Simple@ versions}
2235 %************************************************************************
2237 Much simpler versions when there are no bindings to make!
2239 @tcSimplifyThetas@ simplifies class-type constraints formed by
2240 @deriving@ declarations and when specialising instances. We are
2241 only interested in the simplified bunch of class/type constraints.
2243 It simplifies to constraints of the form (C a b c) where
2244 a,b,c are type variables. This is required for the context of
2245 instance declarations.
2248 tcSimplifyDeriv :: TyCon
2250 -> ThetaType -- Wanted
2251 -> TcM ThetaType -- Needed
2253 tcSimplifyDeriv tc tyvars theta
2254 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2255 -- The main loop may do unification, and that may crash if
2256 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2257 -- ToDo: what if two of them do get unified?
2258 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2259 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2260 ASSERT( null frees ) -- reduceMe never returns Free
2262 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
2263 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2265 tv_set = mkVarSet tvs
2267 (bad_insts, ok_insts) = partition is_bad_inst irreds
2269 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2270 in isEmptyVarSet (tyVarsOfPred pred)
2271 -- Things like (Eq T) are bad
2272 || (not gla_exts && not (isTyVarClassPred pred))
2274 simpl_theta = map dictPred ok_insts
2275 weird_preds = [pred | pred <- simpl_theta
2276 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2277 -- Check for a bizarre corner case, when the derived instance decl should
2278 -- have form instance C a b => D (T a) where ...
2279 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2280 -- of problems; in particular, it's hard to compare solutions for
2281 -- equality when finding the fixpoint. So I just rule it out for now.
2283 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2284 -- This reverse-mapping is a Royal Pain,
2285 -- but the result should mention TyVars not TcTyVars
2287 head_ty = TyConApp tc (map TyVarTy tvs)
2290 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2291 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2292 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2293 -- Check instance termination as for user-declared instances.
2294 -- unless we had -fallow-undecidable-instances (which risks
2295 -- non-termination in the 'deriving' context-inference fixpoint
2297 ifM (gla_exts && not undecidable_ok)
2298 (checkInstTermination simpl_theta [head_ty]) `thenM_`
2299 returnM (substTheta rev_env simpl_theta)
2301 doc = ptext SLIT("deriving classes for a data type")
2304 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2305 used with \tr{default} declarations. We are only interested in
2306 whether it worked or not.
2309 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2312 tcSimplifyDefault theta
2313 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2314 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2315 ASSERT( null frees ) -- try_me never returns Free
2316 addNoInstanceErrs Nothing [] irreds `thenM_`
2322 doc = ptext SLIT("default declaration")
2326 %************************************************************************
2328 \section{Errors and contexts}
2330 %************************************************************************
2332 ToDo: for these error messages, should we note the location as coming
2333 from the insts, or just whatever seems to be around in the monad just
2337 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2338 -> [Inst] -- The offending Insts
2340 -- Group together insts with the same origin
2341 -- We want to report them together in error messages
2343 groupErrs report_err []
2345 groupErrs report_err (inst:insts)
2346 = do_one (inst:friends) `thenM_`
2347 groupErrs report_err others
2350 -- (It may seem a bit crude to compare the error messages,
2351 -- but it makes sure that we combine just what the user sees,
2352 -- and it avoids need equality on InstLocs.)
2353 (friends, others) = partition is_friend insts
2354 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2355 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2356 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2357 -- Add location and context information derived from the Insts
2359 -- Add the "arising from..." part to a message about bunch of dicts
2360 addInstLoc :: [Inst] -> Message -> Message
2361 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2363 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2364 addTopIPErrs bndrs []
2366 addTopIPErrs bndrs ips
2367 = addErrTcM (tidy_env, mk_msg tidy_ips)
2369 (tidy_env, tidy_ips) = tidyInsts ips
2370 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2371 nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
2372 <+> pprBinders bndrs <> colon)],
2373 nest 2 (vcat (map ppr_ip ips)),
2375 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2377 strangeTopIPErrs :: [Inst] -> TcM ()
2378 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2379 = groupErrs report tidy_dicts
2381 (tidy_env, tidy_dicts) = tidyInsts dicts
2382 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2383 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2384 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2386 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2387 -- Just d => d describes the construct
2388 -> [Inst] -- What is given by the context or type sig
2389 -> [Inst] -- What is wanted
2391 addNoInstanceErrs mb_what givens []
2393 addNoInstanceErrs mb_what givens dicts
2394 = -- Some of the dicts are here because there is no instances
2395 -- and some because there are too many instances (overlap)
2396 tcGetInstEnvs `thenM` \ inst_envs ->
2398 (tidy_env1, tidy_givens) = tidyInsts givens
2399 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2401 -- Run through the dicts, generating a message for each
2402 -- overlapping one, but simply accumulating all the
2403 -- no-instance ones so they can be reported as a group
2404 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2405 check_overlap (overlap_doc, no_inst_dicts) dict
2406 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2408 = case lookupInstEnv inst_envs clas tys of
2409 -- The case of exactly one match and no unifiers means
2410 -- a successful lookup. That can't happen here, becuase
2411 -- dicts only end up here if they didn't match in Inst.lookupInst
2413 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2415 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2416 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2418 (clas,tys) = getDictClassTys dict
2421 -- Now generate a good message for the no-instance bunch
2422 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2424 no_inst_doc | null no_inst_dicts = empty
2425 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2426 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2427 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2428 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2429 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2431 -- And emit both the non-instance and overlap messages
2432 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2434 mk_overlap_msg dict (matches, unifiers)
2435 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2436 <+> pprPred (dictPred dict))),
2437 sep [ptext SLIT("Matching instances") <> colon,
2438 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2439 ASSERT( not (null matches) )
2440 if not (isSingleton matches)
2441 then -- Two or more matches
2443 else -- One match, plus some unifiers
2444 ASSERT( not (null unifiers) )
2445 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2446 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2447 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2449 ispecs = [ispec | (_, ispec) <- matches]
2451 mk_probable_fix tidy_env dicts
2452 = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
2454 fixes = add_ors (fix1 ++ fix2)
2456 fix1 = case mb_what of
2457 Nothing -> [] -- Top level
2458 Just what -> -- Nested (type signatures, instance decls)
2459 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2460 ptext SLIT("to the") <+> what] ]
2462 fix2 | null instance_dicts = []
2463 | otherwise = [ ptext SLIT("add an instance declaration for")
2464 <+> pprDictsTheta instance_dicts ]
2465 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2466 -- Insts for which it is worth suggesting an adding an instance declaration
2467 -- Exclude implicit parameters, and tyvar dicts
2469 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2470 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2471 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2473 addTopAmbigErrs dicts
2474 -- Divide into groups that share a common set of ambiguous tyvars
2475 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2477 (tidy_env, tidy_dicts) = tidyInsts dicts
2479 tvs_of :: Inst -> [TcTyVar]
2480 tvs_of d = varSetElems (tyVarsOfInst d)
2481 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2483 report :: [(Inst,[TcTyVar])] -> TcM ()
2484 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2485 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2486 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2487 -- the location of the first one will do for the err message
2488 addErrTcM (tidy_env, msg $$ mono_msg)
2490 dicts = map fst pairs
2491 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2492 pprQuotedList tvs <+> in_msg,
2493 nest 2 (pprDictsInFull dicts)]
2494 in_msg = text "in the constraint" <> plural dicts <> colon
2497 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2498 -- There's an error with these Insts; if they have free type variables
2499 -- it's probably caused by the monomorphism restriction.
2500 -- Try to identify the offending variable
2501 -- ASSUMPTION: the Insts are fully zonked
2502 mkMonomorphismMsg tidy_env inst_tvs
2503 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2504 returnM (tidy_env, mk_msg docs)
2506 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2507 -- This happens in things like
2508 -- f x = show (read "foo")
2509 -- whre monomorphism doesn't play any role
2510 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2514 monomorphism_fix :: SDoc
2515 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2516 (ptext SLIT("give these definition(s) an explicit type signature")
2517 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2519 warnDefault dicts default_ty
2520 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2521 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2524 (_, tidy_dicts) = tidyInsts dicts
2525 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2526 quotes (ppr default_ty),
2527 pprDictsInFull tidy_dicts]
2529 -- Used for the ...Thetas variants; all top level
2531 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2532 ptext SLIT("type variables that are not data type parameters"),
2533 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2535 reduceDepthErr n stack
2536 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2537 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2538 nest 4 (pprStack stack)]
2540 pprStack stack = vcat (map pprInstInFull stack)