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 HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
25 import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp )
28 import Inst ( lookupInst, LookupInstResult(..),
29 tyVarsOfInst, fdPredsOfInsts, newDicts,
30 isDict, isClassDict, isLinearInst, linearInstType,
31 isMethodFor, isMethod,
32 instToId, tyVarsOfInsts, cloneDict,
33 ipNamesOfInsts, ipNamesOfInst, dictPred,
35 newDictsAtLoc, tcInstClassOp,
36 getDictClassTys, isTyVarDict, instLoc,
37 zonkInst, tidyInsts, tidyMoreInsts,
38 pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
39 isInheritableInst, pprDictsTheta
41 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
42 lclEnvElts, tcMetaTy )
43 import InstEnv ( lookupInstEnv, classInstances, pprInstances )
44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType )
45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
46 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
47 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
48 tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
49 import TcIface ( checkWiredInTyCon )
50 import Id ( idType, mkUserLocal )
52 import TyCon ( TyCon )
53 import Name ( Name, getOccName, getSrcLoc )
54 import NameSet ( NameSet, mkNameSet, elemNameSet )
55 import Class ( classBigSig, classKey )
56 import FunDeps ( oclose, grow, improve, pprEquation )
57 import PrelInfo ( isNumericClass, isStandardClass )
58 import PrelNames ( splitName, fstName, sndName, integerTyConName,
59 showClassKey, eqClassKey, ordClassKey )
60 import Type ( zipTopTvSubst, substTheta, substTy )
61 import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
62 import ErrUtils ( Message )
63 import BasicTypes ( TopLevelFlag, isNotTopLevel )
65 import VarEnv ( TidyEnv )
69 import ListSetOps ( equivClasses )
70 import Util ( zipEqual, isSingleton )
71 import List ( partition )
72 import SrcLoc ( Located(..) )
73 import DynFlags ( DynFlags(ctxtStkDepth),
74 DynFlag( Opt_GlasgowExts, Opt_AllowUndecidableInstances, Opt_WarnTypeDefaults ) )
78 %************************************************************************
82 %************************************************************************
84 --------------------------------------
85 Notes on functional dependencies (a bug)
86 --------------------------------------
88 | > class Foo a b | a->b
90 | > class Bar a b | a->b
94 | > instance Bar Obj Obj
96 | > instance (Bar a b) => Foo a b
98 | > foo:: (Foo a b) => a -> String
101 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
107 | Could not deduce (Bar a b) from the context (Foo a b)
108 | arising from use of `foo' at <interactive>:1
110 | Add (Bar a b) to the expected type of an expression
111 | In the first argument of `runFoo', namely `foo'
112 | In the definition of `it': it = runFoo foo
114 | Why all of the sudden does GHC need the constraint Bar a b? The
115 | function foo didn't ask for that...
117 The trouble is that to type (runFoo foo), GHC has to solve the problem:
119 Given constraint Foo a b
120 Solve constraint Foo a b'
122 Notice that b and b' aren't the same. To solve this, just do
123 improvement and then they are the same. But GHC currently does
128 That is usually fine, but it isn't here, because it sees that Foo a b is
129 not the same as Foo a b', and so instead applies the instance decl for
130 instance Bar a b => Foo a b. And that's where the Bar constraint comes
133 The Right Thing is to improve whenever the constraint set changes at
134 all. Not hard in principle, but it'll take a bit of fiddling to do.
138 --------------------------------------
139 Notes on quantification
140 --------------------------------------
142 Suppose we are about to do a generalisation step.
146 T the type of the RHS
147 C the constraints from that RHS
149 The game is to figure out
151 Q the set of type variables over which to quantify
152 Ct the constraints we will *not* quantify over
153 Cq the constraints we will quantify over
155 So we're going to infer the type
159 and float the constraints Ct further outwards.
161 Here are the things that *must* be true:
163 (A) Q intersect fv(G) = EMPTY limits how big Q can be
164 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
166 (A) says we can't quantify over a variable that's free in the
167 environment. (B) says we must quantify over all the truly free
168 variables in T, else we won't get a sufficiently general type. We do
169 not *need* to quantify over any variable that is fixed by the free
170 vars of the environment G.
172 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
174 Example: class H x y | x->y where ...
176 fv(G) = {a} C = {H a b, H c d}
179 (A) Q intersect {a} is empty
180 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
182 So Q can be {c,d}, {b,c,d}
184 Other things being equal, however, we'd like to quantify over as few
185 variables as possible: smaller types, fewer type applications, more
186 constraints can get into Ct instead of Cq.
189 -----------------------------------------
192 fv(T) the free type vars of T
194 oclose(vs,C) The result of extending the set of tyvars vs
195 using the functional dependencies from C
197 grow(vs,C) The result of extend the set of tyvars vs
198 using all conceivable links from C.
200 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
201 Then grow(vs,C) = {a,b,c}
203 Note that grow(vs,C) `superset` grow(vs,simplify(C))
204 That is, simplfication can only shrink the result of grow.
207 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
208 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
211 -----------------------------------------
215 Here's a good way to choose Q:
217 Q = grow( fv(T), C ) \ oclose( fv(G), C )
219 That is, quantify over all variable that that MIGHT be fixed by the
220 call site (which influences T), but which aren't DEFINITELY fixed by
221 G. This choice definitely quantifies over enough type variables,
222 albeit perhaps too many.
224 Why grow( fv(T), C ) rather than fv(T)? Consider
226 class H x y | x->y where ...
231 If we used fv(T) = {c} we'd get the type
233 forall c. H c d => c -> b
235 And then if the fn was called at several different c's, each of
236 which fixed d differently, we'd get a unification error, because
237 d isn't quantified. Solution: quantify d. So we must quantify
238 everything that might be influenced by c.
240 Why not oclose( fv(T), C )? Because we might not be able to see
241 all the functional dependencies yet:
243 class H x y | x->y where ...
244 instance H x y => Eq (T x y) where ...
249 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
250 apparent yet, and that's wrong. We must really quantify over d too.
253 There really isn't any point in quantifying over any more than
254 grow( fv(T), C ), because the call sites can't possibly influence
255 any other type variables.
259 --------------------------------------
261 --------------------------------------
263 It's very hard to be certain when a type is ambiguous. Consider
267 instance H x y => K (x,y)
269 Is this type ambiguous?
270 forall a b. (K (a,b), Eq b) => a -> a
272 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
273 now we see that a fixes b. So we can't tell about ambiguity for sure
274 without doing a full simplification. And even that isn't possible if
275 the context has some free vars that may get unified. Urgle!
277 Here's another example: is this ambiguous?
278 forall a b. Eq (T b) => a -> a
279 Not if there's an insance decl (with no context)
280 instance Eq (T b) where ...
282 You may say of this example that we should use the instance decl right
283 away, but you can't always do that:
285 class J a b where ...
286 instance J Int b where ...
288 f :: forall a b. J a b => a -> a
290 (Notice: no functional dependency in J's class decl.)
291 Here f's type is perfectly fine, provided f is only called at Int.
292 It's premature to complain when meeting f's signature, or even
293 when inferring a type for f.
297 However, we don't *need* to report ambiguity right away. It'll always
298 show up at the call site.... and eventually at main, which needs special
299 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
301 So here's the plan. We WARN about probable ambiguity if
303 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
305 (all tested before quantification).
306 That is, all the type variables in Cq must be fixed by the the variables
307 in the environment, or by the variables in the type.
309 Notice that we union before calling oclose. Here's an example:
311 class J a b c | a b -> c
315 forall b c. (J a b c) => b -> b
317 Only if we union {a} from G with {b} from T before using oclose,
318 do we see that c is fixed.
320 It's a bit vague exactly which C we should use for this oclose call. If we
321 don't fix enough variables we might complain when we shouldn't (see
322 the above nasty example). Nothing will be perfect. That's why we can
323 only issue a warning.
326 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
328 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
330 then c is a "bubble"; there's no way it can ever improve, and it's
331 certainly ambiguous. UNLESS it is a constant (sigh). And what about
336 instance H x y => K (x,y)
338 Is this type ambiguous?
339 forall a b. (K (a,b), Eq b) => a -> a
341 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
342 is a "bubble" that's a set of constraints
344 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
346 Hence another idea. To decide Q start with fv(T) and grow it
347 by transitive closure in Cq (no functional dependencies involved).
348 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
349 The definitely-ambiguous can then float out, and get smashed at top level
350 (which squashes out the constants, like Eq (T a) above)
353 --------------------------------------
354 Notes on principal types
355 --------------------------------------
360 f x = let g y = op (y::Int) in True
362 Here the principal type of f is (forall a. a->a)
363 but we'll produce the non-principal type
364 f :: forall a. C Int => a -> a
367 --------------------------------------
368 The need for forall's in constraints
369 --------------------------------------
371 [Exchange on Haskell Cafe 5/6 Dec 2000]
373 class C t where op :: t -> Bool
374 instance C [t] where op x = True
376 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
377 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
379 The definitions of p and q differ only in the order of the components in
380 the pair on their right-hand sides. And yet:
382 ghc and "Typing Haskell in Haskell" reject p, but accept q;
383 Hugs rejects q, but accepts p;
384 hbc rejects both p and q;
385 nhc98 ... (Malcolm, can you fill in the blank for us!).
387 The type signature for f forces context reduction to take place, and
388 the results of this depend on whether or not the type of y is known,
389 which in turn depends on which component of the pair the type checker
392 Solution: if y::m a, float out the constraints
393 Monad m, forall c. C (m c)
394 When m is later unified with [], we can solve both constraints.
397 --------------------------------------
398 Notes on implicit parameters
399 --------------------------------------
401 Question 1: can we "inherit" implicit parameters
402 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
407 where f is *not* a top-level binding.
408 From the RHS of f we'll get the constraint (?y::Int).
409 There are two types we might infer for f:
413 (so we get ?y from the context of f's definition), or
415 f :: (?y::Int) => Int -> Int
417 At first you might think the first was better, becuase then
418 ?y behaves like a free variable of the definition, rather than
419 having to be passed at each call site. But of course, the WHOLE
420 IDEA is that ?y should be passed at each call site (that's what
421 dynamic binding means) so we'd better infer the second.
423 BOTTOM LINE: when *inferring types* you *must* quantify
424 over implicit parameters. See the predicate isFreeWhenInferring.
427 Question 2: type signatures
428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
429 BUT WATCH OUT: When you supply a type signature, we can't force you
430 to quantify over implicit parameters. For example:
434 This is perfectly reasonable. We do not want to insist on
436 (?x + 1) :: (?x::Int => Int)
438 That would be silly. Here, the definition site *is* the occurrence site,
439 so the above strictures don't apply. Hence the difference between
440 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
441 and tcSimplifyCheckBind (which does not).
443 What about when you supply a type signature for a binding?
444 Is it legal to give the following explicit, user type
445 signature to f, thus:
450 At first sight this seems reasonable, but it has the nasty property
451 that adding a type signature changes the dynamic semantics.
454 (let f x = (x::Int) + ?y
455 in (f 3, f 3 with ?y=5)) with ?y = 6
461 in (f 3, f 3 with ?y=5)) with ?y = 6
465 Indeed, simply inlining f (at the Haskell source level) would change the
468 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
469 semantics for a Haskell program without knowing its typing, so if you
470 change the typing you may change the semantics.
472 To make things consistent in all cases where we are *checking* against
473 a supplied signature (as opposed to inferring a type), we adopt the
476 a signature does not need to quantify over implicit params.
478 [This represents a (rather marginal) change of policy since GHC 5.02,
479 which *required* an explicit signature to quantify over all implicit
480 params for the reasons mentioned above.]
482 But that raises a new question. Consider
484 Given (signature) ?x::Int
485 Wanted (inferred) ?x::Int, ?y::Bool
487 Clearly we want to discharge the ?x and float the ?y out. But
488 what is the criterion that distinguishes them? Clearly it isn't
489 what free type variables they have. The Right Thing seems to be
490 to float a constraint that
491 neither mentions any of the quantified type variables
492 nor any of the quantified implicit parameters
494 See the predicate isFreeWhenChecking.
497 Question 3: monomorphism
498 ~~~~~~~~~~~~~~~~~~~~~~~~
499 There's a nasty corner case when the monomorphism restriction bites:
503 The argument above suggests that we *must* generalise
504 over the ?y parameter, to get
505 z :: (?y::Int) => Int,
506 but the monomorphism restriction says that we *must not*, giving
508 Why does the momomorphism restriction say this? Because if you have
510 let z = x + ?y in z+z
512 you might not expect the addition to be done twice --- but it will if
513 we follow the argument of Question 2 and generalise over ?y.
516 Question 4: top level
517 ~~~~~~~~~~~~~~~~~~~~~
518 At the top level, monomorhism makes no sense at all.
521 main = let ?x = 5 in print foo
525 woggle :: (?x :: Int) => Int -> Int
528 We definitely don't want (foo :: Int) with a top-level implicit parameter
529 (?x::Int) becuase there is no way to bind it.
534 (A) Always generalise over implicit parameters
535 Bindings that fall under the monomorphism restriction can't
539 * Inlining remains valid
540 * No unexpected loss of sharing
541 * But simple bindings like
543 will be rejected, unless you add an explicit type signature
544 (to avoid the monomorphism restriction)
545 z :: (?y::Int) => Int
547 This seems unacceptable
549 (B) Monomorphism restriction "wins"
550 Bindings that fall under the monomorphism restriction can't
552 Always generalise over implicit parameters *except* for bindings
553 that fall under the monomorphism restriction
556 * Inlining isn't valid in general
557 * No unexpected loss of sharing
558 * Simple bindings like
560 accepted (get value of ?y from binding site)
562 (C) Always generalise over implicit parameters
563 Bindings that fall under the monomorphism restriction can't
564 be generalised, EXCEPT for implicit parameters
566 * Inlining remains valid
567 * Unexpected loss of sharing (from the extra generalisation)
568 * Simple bindings like
570 accepted (get value of ?y from occurrence sites)
575 None of these choices seems very satisfactory. But at least we should
576 decide which we want to do.
578 It's really not clear what is the Right Thing To Do. If you see
582 would you expect the value of ?y to be got from the *occurrence sites*
583 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
584 case of function definitions, the answer is clearly the former, but
585 less so in the case of non-fucntion definitions. On the other hand,
586 if we say that we get the value of ?y from the definition site of 'z',
587 then inlining 'z' might change the semantics of the program.
589 Choice (C) really says "the monomorphism restriction doesn't apply
590 to implicit parameters". Which is fine, but remember that every
591 innocent binding 'x = ...' that mentions an implicit parameter in
592 the RHS becomes a *function* of that parameter, called at each
593 use of 'x'. Now, the chances are that there are no intervening 'with'
594 clauses that bind ?y, so a decent compiler should common up all
595 those function calls. So I think I strongly favour (C). Indeed,
596 one could make a similar argument for abolishing the monomorphism
597 restriction altogether.
599 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
603 %************************************************************************
605 \subsection{tcSimplifyInfer}
607 %************************************************************************
609 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
611 1. Compute Q = grow( fvs(T), C )
613 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
614 predicates will end up in Ct; we deal with them at the top level
616 3. Try improvement, using functional dependencies
618 4. If Step 3 did any unification, repeat from step 1
619 (Unification can change the result of 'grow'.)
621 Note: we don't reduce dictionaries in step 2. For example, if we have
622 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
623 after step 2. However note that we may therefore quantify over more
624 type variables than we absolutely have to.
626 For the guts, we need a loop, that alternates context reduction and
627 improvement with unification. E.g. Suppose we have
629 class C x y | x->y where ...
631 and tcSimplify is called with:
633 Then improvement unifies a with b, giving
636 If we need to unify anything, we rattle round the whole thing all over
643 -> TcTyVarSet -- fv(T); type vars
645 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
646 TcDictBinds, -- Bindings
647 [TcId]) -- Dict Ids that must be bound here (zonked)
648 -- Any free (escaping) Insts are tossed into the environment
653 tcSimplifyInfer doc tau_tvs wanted_lie
654 = inferLoop doc (varSetElems tau_tvs)
655 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
657 extendLIEs frees `thenM_`
658 returnM (qtvs, binds, map instToId irreds)
660 inferLoop doc tau_tvs wanteds
662 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
663 mappM zonkInst wanteds `thenM` \ wanteds' ->
664 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
666 preds = fdPredsOfInsts wanteds'
667 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
670 | isFreeWhenInferring qtvs inst = Free
671 | isClassDict inst = DontReduceUnlessConstant -- Dicts
672 | otherwise = ReduceMe NoSCs -- Lits and Methods
674 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
675 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
677 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
680 if no_improvement then
681 returnM (varSetElems qtvs, frees, binds, irreds)
683 -- If improvement did some unification, we go round again. There
684 -- are two subtleties:
685 -- a) We start again with irreds, not wanteds
686 -- Using an instance decl might have introduced a fresh type variable
687 -- which might have been unified, so we'd get an infinite loop
688 -- if we started again with wanteds! See example [LOOP]
690 -- b) It's also essential to re-process frees, because unification
691 -- might mean that a type variable that looked free isn't now.
693 -- Hence the (irreds ++ frees)
695 -- However, NOTICE that when we are done, we might have some bindings, but
696 -- the final qtvs might be empty. See [NO TYVARS] below.
698 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
699 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
704 class If b t e r | b t e -> r
707 class Lte a b c | a b -> c where lte :: a -> b -> c
709 instance (Lte a b l,If l b a c) => Max a b c
711 Wanted: Max Z (S x) y
713 Then we'll reduce using the Max instance to:
714 (Lte Z (S x) l, If l (S x) Z y)
715 and improve by binding l->T, after which we can do some reduction
716 on both the Lte and If constraints. What we *can't* do is start again
717 with (Max Z (S x) y)!
721 class Y a b | a -> b where
724 instance Y [[a]] a where
727 k :: X a -> X a -> X a
729 g :: Num a => [X a] -> [X a]
732 h ys = ys ++ map (k (y [[0]])) xs
734 The excitement comes when simplifying the bindings for h. Initially
735 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
736 From this we get t1:=:t2, but also various bindings. We can't forget
737 the bindings (because of [LOOP]), but in fact t1 is what g is
740 The net effect of [NO TYVARS]
743 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
744 isFreeWhenInferring qtvs inst
745 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
746 && isInheritableInst inst -- And no implicit parameter involved
747 -- (see "Notes on implicit parameters")
749 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
750 -> NameSet -- Quantified implicit parameters
752 isFreeWhenChecking qtvs ips inst
753 = isFreeWrtTyVars qtvs inst
754 && isFreeWrtIPs ips inst
756 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
757 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
761 %************************************************************************
763 \subsection{tcSimplifyCheck}
765 %************************************************************************
767 @tcSimplifyCheck@ is used when we know exactly the set of variables
768 we are going to quantify over. For example, a class or instance declaration.
773 -> [TcTyVar] -- Quantify over these
776 -> TcM TcDictBinds -- Bindings
778 -- tcSimplifyCheck is used when checking expression type signatures,
779 -- class decls, instance decls etc.
781 -- NB: tcSimplifyCheck does not consult the
782 -- global type variables in the environment; so you don't
783 -- need to worry about setting them before calling tcSimplifyCheck
784 tcSimplifyCheck doc qtvs givens wanted_lie
785 = ASSERT( all isSkolemTyVar qtvs )
786 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
790 -- get_qtvs = zonkTcTyVarsAndFV qtvs
791 get_qtvs = return (mkVarSet qtvs) -- All skolems
794 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
795 -- against, but we don't know the type variables over which we are going to quantify.
796 -- This happens when we have a type signature for a mutually recursive group
799 -> TcTyVarSet -- fv(T)
802 -> TcM ([TcTyVar], -- Variables over which to quantify
803 TcDictBinds) -- Bindings
805 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
806 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
808 ; return (qtvs', binds) }
810 -- Figure out which type variables to quantify over
811 -- You might think it should just be the signature tyvars,
812 -- but in bizarre cases you can get extra ones
813 -- f :: forall a. Num a => a -> a
814 -- f x = fst (g (x, head [])) + 1
816 -- Here we infer g :: forall a b. a -> b -> (b,a)
817 -- We don't want g to be monomorphic in b just because
818 -- f isn't quantified over b.
819 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
821 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
822 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
824 qtvs = all_tvs' `minusVarSet` gbl_tvs
825 -- We could close gbl_tvs, but its not necessary for
826 -- soundness, and it'll only affect which tyvars, not which
827 -- dictionaries, we quantify over
832 Here is the workhorse function for all three wrappers.
835 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
836 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
838 -- Complain about any irreducible ones
839 ; if not (null irreds)
840 then do { givens' <- mappM zonkInst given_dicts_and_ips
841 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
844 ; returnM (qtvs, frees, binds) }
846 given_dicts_and_ips = filter (not . isMethod) givens
847 -- For error reporting, filter out methods, which are
848 -- only added to the given set as an optimisation
850 ip_set = mkNameSet (ipNamesOfInsts givens)
852 check_loop givens wanteds
854 mappM zonkInst givens `thenM` \ givens' ->
855 mappM zonkInst wanteds `thenM` \ wanteds' ->
856 get_qtvs `thenM` \ qtvs' ->
860 -- When checking against a given signature we always reduce
861 -- until we find a match against something given, or can't reduce
862 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
863 | otherwise = ReduceMe want_scs
865 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
868 if no_improvement then
869 returnM (varSetElems qtvs', frees, binds, irreds)
871 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
872 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
876 %************************************************************************
878 tcSimplifySuperClasses
880 %************************************************************************
882 Note [SUPERCLASS-LOOP 1]
883 ~~~~~~~~~~~~~~~~~~~~~~~~
884 We have to be very, very careful when generating superclasses, lest we
885 accidentally build a loop. Here's an example:
889 class S a => C a where { opc :: a -> a }
890 class S b => D b where { opd :: b -> b }
898 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
899 Simplifying, we may well get:
900 $dfCInt = :C ds1 (opd dd)
903 Notice that we spot that we can extract ds1 from dd.
905 Alas! Alack! We can do the same for (instance D Int):
907 $dfDInt = :D ds2 (opc dc)
911 And now we've defined the superclass in terms of itself.
913 Solution: never generate a superclass selectors at all when
914 satisfying the superclass context of an instance declaration.
916 Two more nasty cases are in
921 tcSimplifySuperClasses qtvs givens sc_wanteds
922 = ASSERT( all isSkolemTyVar qtvs )
923 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
924 ; binds2 <- tc_simplify_top doc False NoSCs frees
925 ; return (binds1 `unionBags` binds2) }
927 get_qtvs = return (mkVarSet qtvs)
928 doc = ptext SLIT("instance declaration superclass context")
932 %************************************************************************
934 \subsection{tcSimplifyRestricted}
936 %************************************************************************
938 tcSimplifyRestricted infers which type variables to quantify for a
939 group of restricted bindings. This isn't trivial.
942 We want to quantify over a to get id :: forall a. a->a
945 We do not want to quantify over a, because there's an Eq a
946 constraint, so we get eq :: a->a->Bool (notice no forall)
949 RHS has type 'tau', whose free tyvars are tau_tvs
950 RHS has constraints 'wanteds'
953 Quantify over (tau_tvs \ ftvs(wanteds))
954 This is bad. The constraints may contain (Monad (ST s))
955 where we have instance Monad (ST s) where...
956 so there's no need to be monomorphic in s!
958 Also the constraint might be a method constraint,
959 whose type mentions a perfectly innocent tyvar:
960 op :: Num a => a -> b -> a
961 Here, b is unconstrained. A good example would be
963 We want to infer the polymorphic type
964 foo :: forall b. b -> b
967 Plan B (cunning, used for a long time up to and including GHC 6.2)
968 Step 1: Simplify the constraints as much as possible (to deal
969 with Plan A's problem). Then set
970 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
972 Step 2: Now simplify again, treating the constraint as 'free' if
973 it does not mention qtvs, and trying to reduce it otherwise.
974 The reasons for this is to maximise sharing.
976 This fails for a very subtle reason. Suppose that in the Step 2
977 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
978 In the Step 1 this constraint might have been simplified, perhaps to
979 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
980 This won't happen in Step 2... but that in turn might prevent some other
981 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
982 and that in turn breaks the invariant that no constraints are quantified over.
984 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
989 Step 1: Simplify the constraints as much as possible (to deal
990 with Plan A's problem). Then set
991 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
992 Return the bindings from Step 1.
995 A note about Plan C (arising from "bug" reported by George Russel March 2004)
998 instance (HasBinary ty IO) => HasCodedValue ty
1000 foo :: HasCodedValue a => String -> IO a
1002 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1003 doDecodeIO codedValue view
1004 = let { act = foo "foo" } in act
1006 You might think this should work becuase the call to foo gives rise to a constraint
1007 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1008 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1009 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1011 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1015 Plan D (a variant of plan B)
1016 Step 1: Simplify the constraints as much as possible (to deal
1017 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1018 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1020 Step 2: Now simplify again, treating the constraint as 'free' if
1021 it does not mention qtvs, and trying to reduce it otherwise.
1023 The point here is that it's generally OK to have too few qtvs; that is,
1024 to make the thing more monomorphic than it could be. We don't want to
1025 do that in the common cases, but in wierd cases it's ok: the programmer
1026 can always add a signature.
1028 Too few qtvs => too many wanteds, which is what happens if you do less
1033 tcSimplifyRestricted -- Used for restricted binding groups
1034 -- i.e. ones subject to the monomorphism restriction
1037 -> [Name] -- Things bound in this group
1038 -> TcTyVarSet -- Free in the type of the RHSs
1039 -> [Inst] -- Free in the RHSs
1040 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1041 TcDictBinds) -- Bindings
1042 -- tcSimpifyRestricted returns no constraints to
1043 -- quantify over; by definition there are none.
1044 -- They are all thrown back in the LIE
1046 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1047 -- Zonk everything in sight
1048 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1049 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1050 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1052 -- 'reduceMe': Reduce as far as we can. Don't stop at
1053 -- dicts; the idea is to get rid of as many type
1054 -- variables as possible, and we don't want to stop
1055 -- at (say) Monad (ST s), because that reduces
1056 -- immediately, with no constraint on s.
1058 -- BUT do no improvement! See Plan D above
1059 reduceContextWithoutImprovement
1060 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1062 -- Next, figure out the tyvars we will quantify over
1064 constrained_tvs = tyVarsOfInsts constrained_dicts
1065 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1066 `minusVarSet` constrained_tvs
1068 traceTc (text "tcSimplifyRestricted" <+> vcat [
1069 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1071 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1073 -- The first step may have squashed more methods than
1074 -- necessary, so try again, this time more gently, knowing the exact
1075 -- set of type variables to quantify over.
1077 -- We quantify only over constraints that are captured by qtvs;
1078 -- these will just be a subset of non-dicts. This in contrast
1079 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1080 -- all *non-inheritable* constraints too. This implements choice
1081 -- (B) under "implicit parameter and monomorphism" above.
1083 -- Remember that we may need to do *some* simplification, to
1084 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1085 -- just to float all constraints
1087 -- At top level, we *do* squash methods becuase we want to
1088 -- expose implicit parameters to the test that follows
1090 is_nested_group = isNotTopLevel top_lvl
1091 try_me inst | isFreeWrtTyVars qtvs inst,
1092 (is_nested_group || isDict inst) = Free
1093 | otherwise = ReduceMe AddSCs
1095 reduceContextWithoutImprovement
1096 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1097 ASSERT( null irreds )
1099 -- See "Notes on implicit parameters, Question 4: top level"
1100 if is_nested_group then
1101 extendLIEs frees `thenM_`
1102 returnM (varSetElems qtvs, binds)
1105 (non_ips, bad_ips) = partition isClassDict frees
1107 addTopIPErrs bndrs bad_ips `thenM_`
1108 extendLIEs non_ips `thenM_`
1109 returnM (varSetElems qtvs, binds)
1113 %************************************************************************
1117 %************************************************************************
1119 On the LHS of transformation rules we only simplify methods and constants,
1120 getting dictionaries. We want to keep all of them unsimplified, to serve
1121 as the available stuff for the RHS of the rule.
1123 Example. Consider the following left-hand side of a rule
1125 f (x == y) (y > z) = ...
1127 If we typecheck this expression we get constraints
1129 d1 :: Ord a, d2 :: Eq a
1131 We do NOT want to "simplify" to the LHS
1133 forall x::a, y::a, z::a, d1::Ord a.
1134 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1138 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1139 f ((==) d2 x y) ((>) d1 y z) = ...
1141 Here is another example:
1143 fromIntegral :: (Integral a, Num b) => a -> b
1144 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1146 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1147 we *dont* want to get
1149 forall dIntegralInt.
1150 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1152 because the scsel will mess up RULE matching. Instead we want
1154 forall dIntegralInt, dNumInt.
1155 fromIntegral Int Int dIntegralInt dNumInt = id Int
1159 g (x == y) (y == z) = ..
1161 where the two dictionaries are *identical*, we do NOT WANT
1163 forall x::a, y::a, z::a, d1::Eq a
1164 f ((==) d1 x y) ((>) d1 y z) = ...
1166 because that will only match if the dict args are (visibly) equal.
1167 Instead we want to quantify over the dictionaries separately.
1169 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1170 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1171 from scratch, rather than further parameterise simpleReduceLoop etc
1174 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1175 tcSimplifyRuleLhs wanteds
1176 = go [] emptyBag wanteds
1179 = return (dicts, binds)
1180 go dicts binds (w:ws)
1182 = go (w:dicts) binds ws
1184 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1185 -- to fromInteger; this looks fragile to me
1186 ; lookup_result <- lookupInst w'
1187 ; case lookup_result of
1188 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
1189 SimpleInst rhs -> go dicts (addBind binds w rhs) ws
1190 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1194 tcSimplifyBracket is used when simplifying the constraints arising from
1195 a Template Haskell bracket [| ... |]. We want to check that there aren't
1196 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1197 Show instance), but we aren't otherwise interested in the results.
1198 Nor do we care about ambiguous dictionaries etc. We will type check
1199 this bracket again at its usage site.
1202 tcSimplifyBracket :: [Inst] -> TcM ()
1203 tcSimplifyBracket wanteds
1204 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1207 doc = text "tcSimplifyBracket"
1211 %************************************************************************
1213 \subsection{Filtering at a dynamic binding}
1215 %************************************************************************
1220 we must discharge all the ?x constraints from B. We also do an improvement
1221 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1223 Actually, the constraints from B might improve the types in ?x. For example
1225 f :: (?x::Int) => Char -> Char
1228 then the constraint (?x::Int) arising from the call to f will
1229 force the binding for ?x to be of type Int.
1232 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1235 tcSimplifyIPs given_ips wanteds
1236 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1237 extendLIEs frees `thenM_`
1240 doc = text "tcSimplifyIPs" <+> ppr given_ips
1241 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1243 -- Simplify any methods that mention the implicit parameter
1244 try_me inst | isFreeWrtIPs ip_set inst = Free
1245 | otherwise = ReduceMe NoSCs
1247 simpl_loop givens wanteds
1248 = mappM zonkInst givens `thenM` \ givens' ->
1249 mappM zonkInst wanteds `thenM` \ wanteds' ->
1251 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1253 if no_improvement then
1254 ASSERT( null irreds )
1255 returnM (frees, binds)
1257 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1258 returnM (frees1, binds `unionBags` binds1)
1262 %************************************************************************
1264 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1266 %************************************************************************
1268 When doing a binding group, we may have @Insts@ of local functions.
1269 For example, we might have...
1271 let f x = x + 1 -- orig local function (overloaded)
1272 f.1 = f Int -- two instances of f
1277 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1278 where @f@ is in scope; those @Insts@ must certainly not be passed
1279 upwards towards the top-level. If the @Insts@ were binding-ified up
1280 there, they would have unresolvable references to @f@.
1282 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1283 For each method @Inst@ in the @init_lie@ that mentions one of the
1284 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1285 @LIE@), as well as the @HsBinds@ generated.
1288 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1289 -- Simlifies only MethodInsts, and generate only bindings of form
1291 -- We're careful not to even generate bindings of the form
1293 -- You'd think that'd be fine, but it interacts with what is
1294 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1296 bindInstsOfLocalFuns wanteds local_ids
1297 | null overloaded_ids
1299 = extendLIEs wanteds `thenM_`
1300 returnM emptyLHsBinds
1303 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1304 ASSERT( null irreds )
1305 extendLIEs not_for_me `thenM_`
1306 extendLIEs frees `thenM_`
1309 doc = text "bindInsts" <+> ppr local_ids
1310 overloaded_ids = filter is_overloaded local_ids
1311 is_overloaded id = isOverloadedTy (idType id)
1312 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1314 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1315 -- so it's worth building a set, so that
1316 -- lookup (in isMethodFor) is faster
1317 try_me inst | isMethod inst = ReduceMe NoSCs
1322 %************************************************************************
1324 \subsection{Data types for the reduction mechanism}
1326 %************************************************************************
1328 The main control over context reduction is here
1332 = ReduceMe WantSCs -- Try to reduce this
1333 -- If there's no instance, behave exactly like
1334 -- DontReduce: add the inst to the irreductible ones,
1335 -- but don't produce an error message of any kind.
1336 -- It might be quite legitimate such as (Eq a)!
1338 | DontReduceUnlessConstant -- Return as irreducible unless it can
1339 -- be reduced to a constant in one step
1341 | Free -- Return as free
1343 reduceMe :: Inst -> WhatToDo
1344 reduceMe inst = ReduceMe AddSCs
1346 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1347 -- of a predicate when adding it to the avails
1348 -- The reason for this flag is entirely the super-class loop problem
1349 -- Note [SUPER-CLASS LOOP 1]
1355 type Avails = FiniteMap Inst Avail
1356 emptyAvails = emptyFM
1359 = IsFree -- Used for free Insts
1360 | Irred -- Used for irreducible dictionaries,
1361 -- which are going to be lambda bound
1363 | Given TcId -- Used for dictionaries for which we have a binding
1364 -- e.g. those "given" in a signature
1365 Bool -- True <=> actually consumed (splittable IPs only)
1367 | Rhs -- Used when there is a RHS
1368 (LHsExpr TcId) -- The RHS
1369 [Inst] -- Insts free in the RHS; we need these too
1371 | Linear -- Splittable Insts only.
1372 Int -- The Int is always 2 or more; indicates how
1373 -- many copies are required
1374 Inst -- The splitter
1375 Avail -- Where the "master copy" is
1377 | LinRhss -- Splittable Insts only; this is used only internally
1378 -- by extractResults, where a Linear
1379 -- is turned into an LinRhss
1380 [LHsExpr TcId] -- A supply of suitable RHSs
1382 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1383 | (inst,avail) <- fmToList avails ]
1385 instance Outputable Avail where
1388 pprAvail IsFree = text "Free"
1389 pprAvail Irred = text "Irred"
1390 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1391 if b then text "(used)" else empty
1392 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1393 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1394 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1397 Extracting the bindings from a bunch of Avails.
1398 The bindings do *not* come back sorted in dependency order.
1399 We assume that they'll be wrapped in a big Rec, so that the
1400 dependency analyser can sort them out later
1404 extractResults :: Avails
1406 -> TcM (TcDictBinds, -- Bindings
1407 [Inst], -- Irreducible ones
1408 [Inst]) -- Free ones
1410 extractResults avails wanteds
1411 = go avails emptyBag [] [] wanteds
1413 go avails binds irreds frees []
1414 = returnM (binds, irreds, frees)
1416 go avails binds irreds frees (w:ws)
1417 = case lookupFM avails w of
1418 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1419 go avails binds irreds frees ws
1421 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1422 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1424 Just (Given id _) -> go avails new_binds irreds frees ws
1426 new_binds | id == instToId w = binds
1427 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1428 -- The sought Id can be one of the givens, via a superclass chain
1429 -- and then we definitely don't want to generate an x=x binding!
1431 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1433 new_binds = addBind binds w rhs
1435 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1436 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1437 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1438 go (addToFM avails w (LinRhss rhss))
1439 (binds `unionBags` binds')
1440 irreds' frees' (split_inst : w : ws)
1442 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1443 -> go new_avails new_binds irreds frees ws
1445 new_binds = addBind binds w rhs
1446 new_avails = addToFM avails w (LinRhss rhss)
1448 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1449 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1450 returnM (w':irreds, frees, instToId w')
1451 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1452 returnM (irreds, w':frees, instToId w')
1454 add_given avails w = addToFM avails w (Given (instToId w) True)
1456 add_free avails w | isMethod w = avails
1457 | otherwise = add_given avails w
1459 -- Do *not* replace Free by Given if it's a method.
1460 -- The following situation shows why this is bad:
1461 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1462 -- From an application (truncate f i) we get
1463 -- t1 = truncate at f
1465 -- If we have also have a second occurrence of truncate, we get
1466 -- t3 = truncate at f
1468 -- When simplifying with i,f free, we might still notice that
1469 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1470 -- will continue to float out!
1472 split :: Int -> TcId -> TcId -> Inst
1473 -> TcM (TcDictBinds, [LHsExpr TcId])
1474 -- (split n split_id root_id wanted) returns
1475 -- * a list of 'n' expressions, all of which witness 'avail'
1476 -- * a bunch of auxiliary bindings to support these expressions
1477 -- * one or zero insts needed to witness the whole lot
1478 -- (maybe be zero if the initial Inst is a Given)
1480 -- NB: 'wanted' is just a template
1482 split n split_id root_id wanted
1485 ty = linearInstType wanted
1486 pair_ty = mkTyConApp pairTyCon [ty,ty]
1487 id = instToId wanted
1490 span = instSpan wanted
1492 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1494 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1495 expand n rhss `thenM` \ (binds2, rhss') ->
1496 returnM (binds1 `unionBags` binds2, rhss')
1499 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1500 -- e.g. expand 3 [rhs1, rhs2]
1501 -- = ( { x = split rhs1 },
1502 -- [fst x, snd x, rhs2] )
1504 | n `rem` 2 == 0 = go rhss -- n is even
1505 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1506 returnM (binds', head rhss : rhss')
1508 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1509 returnM (listToBag binds', concat rhss')
1511 do_one rhs = newUnique `thenM` \ uniq ->
1512 tcLookupId fstName `thenM` \ fst_id ->
1513 tcLookupId sndName `thenM` \ snd_id ->
1515 x = mkUserLocal occ uniq pair_ty loc
1517 returnM (L span (VarBind x (mk_app span split_id rhs)),
1518 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1520 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1522 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1524 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1525 (VarBind (instToId inst) rhs))
1526 instSpan wanted = instLocSrcSpan (instLoc wanted)
1530 %************************************************************************
1532 \subsection[reduce]{@reduce@}
1534 %************************************************************************
1536 When the "what to do" predicate doesn't depend on the quantified type variables,
1537 matters are easier. We don't need to do any zonking, unless the improvement step
1538 does something, in which case we zonk before iterating.
1540 The "given" set is always empty.
1543 simpleReduceLoop :: SDoc
1544 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1546 -> TcM ([Inst], -- Free
1548 [Inst]) -- Irreducible
1550 simpleReduceLoop doc try_me wanteds
1551 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1552 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1553 if no_improvement then
1554 returnM (frees, binds, irreds)
1556 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1557 returnM (frees1, binds `unionBags` binds1, irreds1)
1563 reduceContext :: SDoc
1564 -> (Inst -> WhatToDo)
1567 -> TcM (Bool, -- True <=> improve step did no unification
1569 TcDictBinds, -- Dictionary bindings
1570 [Inst]) -- Irreducible
1572 reduceContext doc try_me givens wanteds
1574 traceTc (text "reduceContext" <+> (vcat [
1575 text "----------------------",
1577 text "given" <+> ppr givens,
1578 text "wanted" <+> ppr wanteds,
1579 text "----------------------"
1582 -- Build the Avail mapping from "givens"
1583 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1586 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1588 -- Do improvement, using everything in avails
1589 -- In particular, avails includes all superclasses of everything
1590 tcImprove avails `thenM` \ no_improvement ->
1592 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1594 traceTc (text "reduceContext end" <+> (vcat [
1595 text "----------------------",
1597 text "given" <+> ppr givens,
1598 text "wanted" <+> ppr wanteds,
1600 text "avails" <+> pprAvails avails,
1601 text "frees" <+> ppr frees,
1602 text "no_improvement =" <+> ppr no_improvement,
1603 text "----------------------"
1606 returnM (no_improvement, frees, binds, irreds)
1608 -- reduceContextWithoutImprovement differs from reduceContext
1609 -- (a) no improvement
1610 -- (b) 'givens' is assumed empty
1611 reduceContextWithoutImprovement doc try_me wanteds
1613 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1614 text "----------------------",
1616 text "wanted" <+> ppr wanteds,
1617 text "----------------------"
1621 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1622 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1624 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1625 text "----------------------",
1627 text "wanted" <+> ppr wanteds,
1629 text "avails" <+> pprAvails avails,
1630 text "frees" <+> ppr frees,
1631 text "----------------------"
1634 returnM (frees, binds, irreds)
1636 tcImprove :: Avails -> TcM Bool -- False <=> no change
1637 -- Perform improvement using all the predicates in Avails
1639 = tcGetInstEnvs `thenM` \ inst_envs ->
1641 preds = [ (pred, pp_loc)
1642 | (inst, avail) <- fmToList avails,
1643 pred <- get_preds inst avail,
1644 let pp_loc = pprInstLoc (instLoc inst)
1646 -- Avails has all the superclasses etc (good)
1647 -- It also has all the intermediates of the deduction (good)
1648 -- It does not have duplicates (good)
1649 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1650 -- so that improve will see them separate
1652 -- For free Methods, we want to take predicates from their context,
1653 -- but for Methods that have been squished their context will already
1654 -- be in Avails, and we don't want duplicates. Hence this rather
1655 -- horrid get_preds function
1656 get_preds inst IsFree = fdPredsOfInst inst
1657 get_preds inst other | isDict inst = [dictPred inst]
1660 eqns = improve get_insts preds
1661 get_insts clas = classInstances inst_envs clas
1666 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1667 mappM_ unify eqns `thenM_`
1670 unify ((qtvs, pairs), what1, what2)
1671 = addErrCtxtM (mkEqnMsg what1 what2) $
1672 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1673 mapM_ (unif_pr tenv) pairs
1674 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1676 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1678 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1679 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1680 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1681 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1682 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1683 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1684 ; return (tidy_env, msg) }
1687 The main context-reduction function is @reduce@. Here's its game plan.
1690 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1691 -- along with its depth
1692 -> (Inst -> WhatToDo)
1699 try_me: given an inst, this function returns
1701 DontReduce return this in "irreds"
1702 Free return this in "frees"
1704 wanteds: The list of insts to reduce
1705 state: An accumulating parameter of type Avails
1706 that contains the state of the algorithm
1708 It returns a Avails.
1710 The (n,stack) pair is just used for error reporting.
1711 n is always the depth of the stack.
1712 The stack is the stack of Insts being reduced: to produce X
1713 I had to produce Y, to produce Y I had to produce Z, and so on.
1716 reduceList (n,stack) try_me wanteds state
1717 = do { dopts <- getDOpts
1720 dumpTcRn (text "Interesting! Context reduction stack deeper than 8:"
1721 <+> (int n $$ ifPprDebug (nest 2 (pprStack stack))))
1724 ; if n >= ctxtStkDepth dopts then
1725 failWithTc (reduceDepthErr n stack)
1729 go [] state = return state
1730 go (w:ws) state = do { state' <- reduce (n+1, w:stack) try_me w state
1733 -- Base case: we're done!
1734 reduce stack try_me wanted avails
1735 -- It's the same as an existing inst, or a superclass thereof
1736 | Just avail <- isAvailable avails wanted
1737 = if isLinearInst wanted then
1738 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1739 reduceList stack try_me wanteds' avails'
1741 returnM avails -- No op for non-linear things
1744 = case try_me wanted of {
1746 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1747 -- First, see if the inst can be reduced to a constant in one step
1748 try_simple (addIrred AddSCs) -- Assume want superclasses
1750 ; Free -> -- It's free so just chuck it upstairs
1751 -- First, see if the inst can be reduced to a constant in one step
1754 ; ReduceMe want_scs -> -- It should be reduced
1755 lookupInst wanted `thenM` \ lookup_result ->
1756 case lookup_result of
1757 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1758 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1759 addWanted want_scs avails2 wanted rhs wanteds'
1760 -- Experiment with temporarily doing addIrred *before* the reduceList,
1761 -- which has the effect of adding the thing we are trying
1762 -- to prove to the database before trying to prove the things it
1763 -- needs. See note [RECURSIVE DICTIONARIES]
1764 -- NB: we must not do an addWanted before, because that adds the
1765 -- superclasses too, and thaat can lead to a spurious loop; see
1766 -- the examples in [SUPERCLASS-LOOP]
1767 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1769 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1771 NoInstance -> -- No such instance!
1772 -- Add it and its superclasses
1773 addIrred want_scs avails wanted
1776 try_simple do_this_otherwise
1777 = lookupInst wanted `thenM` \ lookup_result ->
1778 case lookup_result of
1779 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1780 other -> do_this_otherwise avails wanted
1785 -------------------------
1786 isAvailable :: Avails -> Inst -> Maybe Avail
1787 isAvailable avails wanted = lookupFM avails wanted
1788 -- NB 1: the Ord instance of Inst compares by the class/type info
1789 -- *not* by unique. So
1790 -- d1::C Int == d2::C Int
1792 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1793 addLinearAvailable avails avail wanted
1794 -- avails currently maps [wanted -> avail]
1795 -- Extend avails to reflect a neeed for an extra copy of avail
1797 | Just avail' <- split_avail avail
1798 = returnM (addToFM avails wanted avail', [])
1801 = tcLookupId splitName `thenM` \ split_id ->
1802 tcInstClassOp (instLoc wanted) split_id
1803 [linearInstType wanted] `thenM` \ split_inst ->
1804 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1807 split_avail :: Avail -> Maybe Avail
1808 -- (Just av) if there's a modified version of avail that
1809 -- we can use to replace avail in avails
1810 -- Nothing if there isn't, so we need to create a Linear
1811 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1812 split_avail (Given id used) | not used = Just (Given id True)
1813 | otherwise = Nothing
1814 split_avail Irred = Nothing
1815 split_avail IsFree = Nothing
1816 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1818 -------------------------
1819 addFree :: Avails -> Inst -> TcM Avails
1820 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1821 -- to avails, so that any other equal Insts will be commoned up right
1822 -- here rather than also being tossed upstairs. This is really just
1823 -- an optimisation, and perhaps it is more trouble that it is worth,
1824 -- as the following comments show!
1826 -- NB: do *not* add superclasses. If we have
1829 -- but a is not bound here, then we *don't* want to derive
1830 -- dn from df here lest we lose sharing.
1832 addFree avails free = returnM (addToFM avails free IsFree)
1834 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1835 addWanted want_scs avails wanted rhs_expr wanteds
1836 = addAvailAndSCs want_scs avails wanted avail
1838 avail = Rhs rhs_expr wanteds
1840 addGiven :: Avails -> Inst -> TcM Avails
1841 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1842 -- Always add superclasses for 'givens'
1844 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1845 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1846 -- so the assert isn't true
1848 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1849 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1850 addAvailAndSCs want_scs avails irred Irred
1852 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1853 addAvailAndSCs want_scs avails inst avail
1854 | not (isClassDict inst) = return avails_with_inst
1855 | NoSCs <- want_scs = return avails_with_inst
1856 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1857 ; addSCs is_loop avails_with_inst inst }
1859 avails_with_inst = addToFM avails inst avail
1861 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1862 -- Note: this compares by *type*, not by Unique
1863 deps = findAllDeps (unitVarSet (instToId inst)) avail
1864 dep_tys = map idType (varSetElems deps)
1866 findAllDeps :: IdSet -> Avail -> IdSet
1867 -- Find all the Insts that this one depends on
1868 -- See Note [SUPERCLASS-LOOP 2]
1869 -- Watch out, though. Since the avails may contain loops
1870 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1871 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1872 findAllDeps so_far other = so_far
1874 find_all :: IdSet -> Inst -> IdSet
1876 | kid_id `elemVarSet` so_far = so_far
1877 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1878 | otherwise = so_far'
1880 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1881 kid_id = instToId kid
1883 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1884 -- Add all the superclasses of the Inst to Avails
1885 -- The first param says "dont do this because the original thing
1886 -- depends on this one, so you'd build a loop"
1887 -- Invariant: the Inst is already in Avails.
1889 addSCs is_loop avails dict
1890 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1891 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1893 (clas, tys) = getDictClassTys dict
1894 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1895 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1897 add_sc avails (sc_dict, sc_sel)
1898 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1899 | is_given sc_dict = return avails
1900 | otherwise = addSCs is_loop avails' sc_dict
1902 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1903 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1905 is_given :: Inst -> Bool
1906 is_given sc_dict = case lookupFM avails sc_dict of
1907 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1911 Note [SUPERCLASS-LOOP 2]
1912 ~~~~~~~~~~~~~~~~~~~~~~~~
1913 But the above isn't enough. Suppose we are *given* d1:Ord a,
1914 and want to deduce (d2:C [a]) where
1916 class Ord a => C a where
1917 instance Ord [a] => C [a] where ...
1919 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1920 superclasses of C [a] to avails. But we must not overwrite the binding
1921 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1924 Here's another variant, immortalised in tcrun020
1925 class Monad m => C1 m
1926 class C1 m => C2 m x
1927 instance C2 Maybe Bool
1928 For the instance decl we need to build (C1 Maybe), and it's no good if
1929 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1930 before we search for C1 Maybe.
1932 Here's another example
1933 class Eq b => Foo a b
1934 instance Eq a => Foo [a] a
1938 we'll first deduce that it holds (via the instance decl). We must not
1939 then overwrite the Eq t constraint with a superclass selection!
1941 At first I had a gross hack, whereby I simply did not add superclass constraints
1942 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1943 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1944 I found a very obscure program (now tcrun021) in which improvement meant the
1945 simplifier got two bites a the cherry... so something seemed to be an Irred
1946 first time, but reducible next time.
1948 Now we implement the Right Solution, which is to check for loops directly
1949 when adding superclasses. It's a bit like the occurs check in unification.
1952 Note [RECURSIVE DICTIONARIES]
1953 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1955 data D r = ZeroD | SuccD (r (D r));
1957 instance (Eq (r (D r))) => Eq (D r) where
1958 ZeroD == ZeroD = True
1959 (SuccD a) == (SuccD b) = a == b
1962 equalDC :: D [] -> D [] -> Bool;
1965 We need to prove (Eq (D [])). Here's how we go:
1969 by instance decl, holds if
1973 by instance decl of Eq, holds if
1975 where d2 = dfEqList d3
1978 But now we can "tie the knot" to give
1984 and it'll even run! The trick is to put the thing we are trying to prove
1985 (in this case Eq (D []) into the database before trying to prove its
1986 contributing clauses.
1989 %************************************************************************
1991 \section{tcSimplifyTop: defaulting}
1993 %************************************************************************
1996 @tcSimplifyTop@ is called once per module to simplify all the constant
1997 and ambiguous Insts.
1999 We need to be careful of one case. Suppose we have
2001 instance Num a => Num (Foo a b) where ...
2003 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2004 to (Num x), and default x to Int. But what about y??
2006 It's OK: the final zonking stage should zap y to (), which is fine.
2010 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2011 tcSimplifyTop wanteds
2012 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2014 doc = text "tcSimplifyTop"
2016 tcSimplifyInteractive wanteds
2017 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2019 doc = text "tcSimplifyTop"
2021 -- The TcLclEnv should be valid here, solely to improve
2022 -- error message generation for the monomorphism restriction
2023 tc_simplify_top doc is_interactive want_scs wanteds
2024 = do { lcl_env <- getLclEnv
2025 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2027 ; let try_me inst = ReduceMe want_scs
2028 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2031 -- First get rid of implicit parameters
2032 (non_ips, bad_ips) = partition isClassDict irreds
2034 -- All the non-tv or multi-param ones are definite errors
2035 (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
2036 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2038 -- Group by type variable
2039 tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
2041 -- Pick the ones which its worth trying to disambiguate
2042 -- namely, the ones whose type variable isn't bound
2043 -- up with one of the non-tyvar classes
2044 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2045 defaultable_group ds
2046 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
2047 && defaultable_classes (map get_clas ds)
2048 defaultable_classes clss
2049 | is_interactive = any isInteractiveClass clss
2050 | otherwise = all isStandardClass clss && any isNumericClass clss
2052 isInteractiveClass cls = isNumericClass cls
2053 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2054 -- In interactive mode, we default Show a to Show ()
2055 -- to avoid graututious errors on "show []"
2058 -- Collect together all the bad guys
2059 bad_guys = non_tvs ++ concat non_default_gps
2060 (ambigs, no_insts) = partition isTyVarDict bad_guys
2061 -- If the dict has no type constructors involved, it must be ambiguous,
2062 -- except I suppose that another error with fundeps maybe should have
2063 -- constrained those type variables
2065 -- Report definite errors
2066 ; ASSERT( null frees )
2067 groupErrs (addNoInstanceErrs Nothing []) no_insts
2068 ; strangeTopIPErrs bad_ips
2070 -- Deal with ambiguity errors, but only if
2071 -- if there has not been an error so far:
2072 -- errors often give rise to spurious ambiguous Insts.
2074 -- f = (*) -- Monomorphic
2075 -- g :: Num a => a -> a
2077 -- Here, we get a complaint when checking the type signature for g,
2078 -- that g isn't polymorphic enough; but then we get another one when
2079 -- dealing with the (Num a) context arising from f's definition;
2080 -- we try to unify a with Int (to default it), but find that it's
2081 -- already been unified with the rigid variable from g's type sig
2082 ; binds_ambig <- ifErrsM (returnM []) $
2083 do { -- Complain about the ones that don't fall under
2084 -- the Haskell rules for disambiguation
2085 -- This group includes both non-existent instances
2086 -- e.g. Num (IO a) and Eq (Int -> Int)
2087 -- and ambiguous dictionaries
2089 addTopAmbigErrs ambigs
2091 -- Disambiguate the ones that look feasible
2092 ; mappM disambigGroup default_gps }
2094 ; return (binds `unionBags` unionManyBags binds_ambig) }
2096 ----------------------------------
2097 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2099 is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
2100 -- Invariant: argument is a ClassDict, not IP or method
2101 is_unary_tyvar_dict d = case getDictClassTys d of
2102 (_, [ty]) -> tcIsTyVarTy ty
2105 get_tv d = case getDictClassTys d of
2106 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2107 get_clas d = case getDictClassTys d of
2111 If a dictionary constrains a type variable which is
2112 * not mentioned in the environment
2113 * and not mentioned in the type of the expression
2114 then it is ambiguous. No further information will arise to instantiate
2115 the type variable; nor will it be generalised and turned into an extra
2116 parameter to a function.
2118 It is an error for this to occur, except that Haskell provided for
2119 certain rules to be applied in the special case of numeric types.
2121 * at least one of its classes is a numeric class, and
2122 * all of its classes are numeric or standard
2123 then the type variable can be defaulted to the first type in the
2124 default-type list which is an instance of all the offending classes.
2126 So here is the function which does the work. It takes the ambiguous
2127 dictionaries and either resolves them (producing bindings) or
2128 complains. It works by splitting the dictionary list by type
2129 variable, and using @disambigOne@ to do the real business.
2131 @disambigOne@ assumes that its arguments dictionaries constrain all
2132 the same type variable.
2134 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2135 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2136 the most common use of defaulting is code like:
2138 _ccall_ foo `seqPrimIO` bar
2140 Since we're not using the result of @foo@, the result if (presumably)
2144 disambigGroup :: [Inst] -- All standard classes of form (C a)
2148 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2149 -- SO, TRY DEFAULT TYPES IN ORDER
2151 -- Failure here is caused by there being no type in the
2152 -- default list which can satisfy all the ambiguous classes.
2153 -- For example, if Real a is reqd, but the only type in the
2154 -- default list is Int.
2155 get_default_tys `thenM` \ default_tys ->
2157 try_default [] -- No defaults work, so fail
2160 try_default (default_ty : default_tys)
2161 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2162 -- default_tys instead
2163 tcSimplifyDefault theta `thenM` \ _ ->
2166 theta = [mkClassPred clas [default_ty] | clas <- classes]
2168 -- See if any default works
2169 tryM (try_default default_tys) `thenM` \ mb_ty ->
2172 Right chosen_default_ty -> choose_default chosen_default_ty
2174 tyvar = get_tv (head dicts) -- Should be non-empty
2175 classes = map get_clas dicts
2177 choose_default default_ty -- Commit to tyvar = default_ty
2178 = -- Bind the type variable
2179 unifyType default_ty (mkTyVarTy tyvar) `thenM_`
2180 -- and reduce the context, for real this time
2181 simpleReduceLoop (text "disambig" <+> ppr dicts)
2182 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2183 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2184 warnDefault dicts default_ty `thenM_`
2187 bomb_out = addTopAmbigErrs dicts `thenM_`
2191 = do { mb_defaults <- getDefaultTys
2192 ; case mb_defaults of
2193 Just tys -> return tys
2194 Nothing -> -- No use-supplied default;
2195 -- use [Integer, Double]
2196 do { integer_ty <- tcMetaTy integerTyConName
2197 ; checkWiredInTyCon doubleTyCon
2198 ; return [integer_ty, doubleTy] } }
2201 [Aside - why the defaulting mechanism is turned off when
2202 dealing with arguments and results to ccalls.
2204 When typechecking _ccall_s, TcExpr ensures that the external
2205 function is only passed arguments (and in the other direction,
2206 results) of a restricted set of 'native' types.
2208 The interaction between the defaulting mechanism for numeric
2209 values and CC & CR can be a bit puzzling to the user at times.
2218 What type has 'x' got here? That depends on the default list
2219 in operation, if it is equal to Haskell 98's default-default
2220 of (Integer, Double), 'x' has type Double, since Integer
2221 is not an instance of CR. If the default list is equal to
2222 Haskell 1.4's default-default of (Int, Double), 'x' has type
2228 %************************************************************************
2230 \subsection[simple]{@Simple@ versions}
2232 %************************************************************************
2234 Much simpler versions when there are no bindings to make!
2236 @tcSimplifyThetas@ simplifies class-type constraints formed by
2237 @deriving@ declarations and when specialising instances. We are
2238 only interested in the simplified bunch of class/type constraints.
2240 It simplifies to constraints of the form (C a b c) where
2241 a,b,c are type variables. This is required for the context of
2242 instance declarations.
2245 tcSimplifyDeriv :: TyCon
2247 -> ThetaType -- Wanted
2248 -> TcM ThetaType -- Needed
2250 tcSimplifyDeriv tc tyvars theta
2251 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2252 -- The main loop may do unification, and that may crash if
2253 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2254 -- ToDo: what if two of them do get unified?
2255 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2256 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2257 ASSERT( null frees ) -- reduceMe never returns Free
2259 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
2260 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2262 tv_set = mkVarSet tvs
2264 (bad_insts, ok_insts) = partition is_bad_inst irreds
2266 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2267 in isEmptyVarSet (tyVarsOfPred pred)
2268 -- Things like (Eq T) are bad
2269 || (not gla_exts && not (isTyVarClassPred pred))
2271 simpl_theta = map dictPred ok_insts
2272 weird_preds = [pred | pred <- simpl_theta
2273 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2274 -- Check for a bizarre corner case, when the derived instance decl should
2275 -- have form instance C a b => D (T a) where ...
2276 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2277 -- of problems; in particular, it's hard to compare solutions for
2278 -- equality when finding the fixpoint. So I just rule it out for now.
2280 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2281 -- This reverse-mapping is a Royal Pain,
2282 -- but the result should mention TyVars not TcTyVars
2285 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2286 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2287 returnM (substTheta rev_env simpl_theta)
2289 doc = ptext SLIT("deriving classes for a data type")
2292 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2293 used with \tr{default} declarations. We are only interested in
2294 whether it worked or not.
2297 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2300 tcSimplifyDefault theta
2301 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2302 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2303 ASSERT( null frees ) -- try_me never returns Free
2304 addNoInstanceErrs Nothing [] irreds `thenM_`
2310 doc = ptext SLIT("default declaration")
2314 %************************************************************************
2316 \section{Errors and contexts}
2318 %************************************************************************
2320 ToDo: for these error messages, should we note the location as coming
2321 from the insts, or just whatever seems to be around in the monad just
2325 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2326 -> [Inst] -- The offending Insts
2328 -- Group together insts with the same origin
2329 -- We want to report them together in error messages
2331 groupErrs report_err []
2333 groupErrs report_err (inst:insts)
2334 = do_one (inst:friends) `thenM_`
2335 groupErrs report_err others
2338 -- (It may seem a bit crude to compare the error messages,
2339 -- but it makes sure that we combine just what the user sees,
2340 -- and it avoids need equality on InstLocs.)
2341 (friends, others) = partition is_friend insts
2342 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2343 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2344 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2345 -- Add location and context information derived from the Insts
2347 -- Add the "arising from..." part to a message about bunch of dicts
2348 addInstLoc :: [Inst] -> Message -> Message
2349 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2351 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2352 addTopIPErrs bndrs []
2354 addTopIPErrs bndrs ips
2355 = addErrTcM (tidy_env, mk_msg tidy_ips)
2357 (tidy_env, tidy_ips) = tidyInsts ips
2358 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2359 nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
2360 <+> pprBinders bndrs <> colon)],
2361 nest 2 (vcat (map ppr_ip ips)),
2363 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2365 strangeTopIPErrs :: [Inst] -> TcM ()
2366 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2367 = groupErrs report tidy_dicts
2369 (tidy_env, tidy_dicts) = tidyInsts dicts
2370 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2371 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2372 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2374 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2375 -- Just d => d describes the construct
2376 -> [Inst] -- What is given by the context or type sig
2377 -> [Inst] -- What is wanted
2379 addNoInstanceErrs mb_what givens []
2381 addNoInstanceErrs mb_what givens dicts
2382 = -- Some of the dicts are here because there is no instances
2383 -- and some because there are too many instances (overlap)
2384 tcGetInstEnvs `thenM` \ inst_envs ->
2386 (tidy_env1, tidy_givens) = tidyInsts givens
2387 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2389 -- Run through the dicts, generating a message for each
2390 -- overlapping one, but simply accumulating all the
2391 -- no-instance ones so they can be reported as a group
2392 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2393 check_overlap (overlap_doc, no_inst_dicts) dict
2394 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2396 = case lookupInstEnv inst_envs clas tys of
2397 -- The case of exactly one match and no unifiers means
2398 -- a successful lookup. That can't happen here, becuase
2399 -- dicts only end up here if they didn't match in Inst.lookupInst
2401 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2403 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2404 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2406 (clas,tys) = getDictClassTys dict
2409 -- Now generate a good message for the no-instance bunch
2410 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2412 no_inst_doc | null no_inst_dicts = empty
2413 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2414 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2415 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2416 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2417 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2419 -- And emit both the non-instance and overlap messages
2420 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2422 mk_overlap_msg dict (matches, unifiers)
2423 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2424 <+> pprPred (dictPred dict))),
2425 sep [ptext SLIT("Matching instances") <> colon,
2426 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2427 ASSERT( not (null matches) )
2428 if not (isSingleton matches)
2429 then -- Two or more matches
2431 else -- One match, plus some unifiers
2432 ASSERT( not (null unifiers) )
2433 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2434 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2435 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2437 ispecs = [ispec | (_, ispec) <- matches]
2439 mk_probable_fix tidy_env dicts
2440 = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
2442 fixes = add_ors (fix1 ++ fix2)
2444 fix1 = case mb_what of
2445 Nothing -> [] -- Top level
2446 Just what -> -- Nested (type signatures, instance decls)
2447 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2448 ptext SLIT("to the") <+> what] ]
2450 fix2 | null instance_dicts = []
2451 | otherwise = [ ptext SLIT("add an instance declaration for")
2452 <+> pprDictsTheta instance_dicts ]
2453 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2454 -- Insts for which it is worth suggesting an adding an instance declaration
2455 -- Exclude implicit parameters, and tyvar dicts
2457 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2458 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2459 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2461 addTopAmbigErrs dicts
2462 -- Divide into groups that share a common set of ambiguous tyvars
2463 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2465 (tidy_env, tidy_dicts) = tidyInsts dicts
2467 tvs_of :: Inst -> [TcTyVar]
2468 tvs_of d = varSetElems (tyVarsOfInst d)
2469 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2471 report :: [(Inst,[TcTyVar])] -> TcM ()
2472 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2473 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2474 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2475 -- the location of the first one will do for the err message
2476 addErrTcM (tidy_env, msg $$ mono_msg)
2478 dicts = map fst pairs
2479 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2480 pprQuotedList tvs <+> in_msg,
2481 nest 2 (pprDictsInFull dicts)]
2482 in_msg = text "in the constraint" <> plural dicts <> colon
2485 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2486 -- There's an error with these Insts; if they have free type variables
2487 -- it's probably caused by the monomorphism restriction.
2488 -- Try to identify the offending variable
2489 -- ASSUMPTION: the Insts are fully zonked
2490 mkMonomorphismMsg tidy_env inst_tvs
2491 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2492 returnM (tidy_env, mk_msg docs)
2494 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2495 -- This happens in things like
2496 -- f x = show (read "foo")
2497 -- whre monomorphism doesn't play any role
2498 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2502 monomorphism_fix :: SDoc
2503 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2504 (ptext SLIT("give these definition(s) an explicit type signature")
2505 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2507 warnDefault dicts default_ty
2508 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2509 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2512 (_, tidy_dicts) = tidyInsts dicts
2513 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2514 quotes (ppr default_ty),
2515 pprDictsInFull tidy_dicts]
2517 -- Used for the ...Thetas variants; all top level
2519 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2520 ptext SLIT("type variables that are not data type parameters"),
2521 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2523 reduceDepthErr n stack
2524 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2525 ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
2526 nest 4 (pprStack stack)]
2528 pprStack stack = vcat (map pprInstInFull stack)