2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs,
13 tcSimplifyTop, tcSimplifyInteractive,
16 tcSimplifyDeriv, tcSimplifyDefault,
20 #include "HsVersions.h"
22 import {-# SOURCE #-} TcUnify( unifyTauTy )
24 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
25 import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
28 import Inst ( lookupInst, LookupInstResult(..),
29 tyVarsOfInst, fdPredsOfInsts, newDicts,
30 isDict, isClassDict, isLinearInst, linearInstType,
31 isStdClassTyVarDict, isMethodFor, isMethod,
32 instToId, tyVarsOfInsts, cloneDict,
33 ipNamesOfInsts, ipNamesOfInst, dictPred,
34 instBindingRequired, fdPredsOfInst,
35 newDictsFromOld, tcInstClassOp,
36 getDictClassTys, isTyVarDict,
37 instLoc, zonkInst, tidyInsts, tidyMoreInsts,
38 Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
39 isInheritableInst, pprDFuns, pprDictsTheta
41 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
42 import InstEnv ( lookupInstEnv, classInstances )
43 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
44 import TcType ( TcTyVar, TcTyVarSet, ThetaType,
45 mkClassPred, isOverloadedTy, mkTyConApp,
46 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
47 tyVarsOfPred, tcEqType, pprPred )
48 import Id ( idType, mkUserLocal )
50 import Name ( Name, getOccName, getSrcLoc )
51 import NameSet ( NameSet, mkNameSet, elemNameSet )
52 import Class ( classBigSig, classKey )
53 import FunDeps ( oclose, grow, improve, pprEquationDoc )
54 import PrelInfo ( isNumericClass )
55 import PrelNames ( splitName, fstName, sndName, integerTyConName,
56 showClassKey, eqClassKey, ordClassKey )
57 import Type ( zipTopTvSubst, substTheta, substTy )
58 import TysWiredIn ( pairTyCon, doubleTy )
59 import ErrUtils ( Message )
60 import BasicTypes ( TopLevelFlag, isNotTopLevel )
62 import VarEnv ( TidyEnv )
66 import ListSetOps ( equivClasses )
67 import Util ( zipEqual, isSingleton )
68 import List ( partition )
69 import SrcLoc ( Located(..) )
74 %************************************************************************
78 %************************************************************************
80 --------------------------------------
81 Notes on functional dependencies (a bug)
82 --------------------------------------
84 | > class Foo a b | a->b
86 | > class Bar a b | a->b
90 | > instance Bar Obj Obj
92 | > instance (Bar a b) => Foo a b
94 | > foo:: (Foo a b) => a -> String
97 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
103 | Could not deduce (Bar a b) from the context (Foo a b)
104 | arising from use of `foo' at <interactive>:1
106 | Add (Bar a b) to the expected type of an expression
107 | In the first argument of `runFoo', namely `foo'
108 | In the definition of `it': it = runFoo foo
110 | Why all of the sudden does GHC need the constraint Bar a b? The
111 | function foo didn't ask for that...
113 The trouble is that to type (runFoo foo), GHC has to solve the problem:
115 Given constraint Foo a b
116 Solve constraint Foo a b'
118 Notice that b and b' aren't the same. To solve this, just do
119 improvement and then they are the same. But GHC currently does
124 That is usually fine, but it isn't here, because it sees that Foo a b is
125 not the same as Foo a b', and so instead applies the instance decl for
126 instance Bar a b => Foo a b. And that's where the Bar constraint comes
129 The Right Thing is to improve whenever the constraint set changes at
130 all. Not hard in principle, but it'll take a bit of fiddling to do.
134 --------------------------------------
135 Notes on quantification
136 --------------------------------------
138 Suppose we are about to do a generalisation step.
142 T the type of the RHS
143 C the constraints from that RHS
145 The game is to figure out
147 Q the set of type variables over which to quantify
148 Ct the constraints we will *not* quantify over
149 Cq the constraints we will quantify over
151 So we're going to infer the type
155 and float the constraints Ct further outwards.
157 Here are the things that *must* be true:
159 (A) Q intersect fv(G) = EMPTY limits how big Q can be
160 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
162 (A) says we can't quantify over a variable that's free in the
163 environment. (B) says we must quantify over all the truly free
164 variables in T, else we won't get a sufficiently general type. We do
165 not *need* to quantify over any variable that is fixed by the free
166 vars of the environment G.
168 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
170 Example: class H x y | x->y where ...
172 fv(G) = {a} C = {H a b, H c d}
175 (A) Q intersect {a} is empty
176 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
178 So Q can be {c,d}, {b,c,d}
180 Other things being equal, however, we'd like to quantify over as few
181 variables as possible: smaller types, fewer type applications, more
182 constraints can get into Ct instead of Cq.
185 -----------------------------------------
188 fv(T) the free type vars of T
190 oclose(vs,C) The result of extending the set of tyvars vs
191 using the functional dependencies from C
193 grow(vs,C) The result of extend the set of tyvars vs
194 using all conceivable links from C.
196 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
197 Then grow(vs,C) = {a,b,c}
199 Note that grow(vs,C) `superset` grow(vs,simplify(C))
200 That is, simplfication can only shrink the result of grow.
203 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
204 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
207 -----------------------------------------
211 Here's a good way to choose Q:
213 Q = grow( fv(T), C ) \ oclose( fv(G), C )
215 That is, quantify over all variable that that MIGHT be fixed by the
216 call site (which influences T), but which aren't DEFINITELY fixed by
217 G. This choice definitely quantifies over enough type variables,
218 albeit perhaps too many.
220 Why grow( fv(T), C ) rather than fv(T)? Consider
222 class H x y | x->y where ...
227 If we used fv(T) = {c} we'd get the type
229 forall c. H c d => c -> b
231 And then if the fn was called at several different c's, each of
232 which fixed d differently, we'd get a unification error, because
233 d isn't quantified. Solution: quantify d. So we must quantify
234 everything that might be influenced by c.
236 Why not oclose( fv(T), C )? Because we might not be able to see
237 all the functional dependencies yet:
239 class H x y | x->y where ...
240 instance H x y => Eq (T x y) where ...
245 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
246 apparent yet, and that's wrong. We must really quantify over d too.
249 There really isn't any point in quantifying over any more than
250 grow( fv(T), C ), because the call sites can't possibly influence
251 any other type variables.
255 --------------------------------------
257 --------------------------------------
259 It's very hard to be certain when a type is ambiguous. Consider
263 instance H x y => K (x,y)
265 Is this type ambiguous?
266 forall a b. (K (a,b), Eq b) => a -> a
268 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
269 now we see that a fixes b. So we can't tell about ambiguity for sure
270 without doing a full simplification. And even that isn't possible if
271 the context has some free vars that may get unified. Urgle!
273 Here's another example: is this ambiguous?
274 forall a b. Eq (T b) => a -> a
275 Not if there's an insance decl (with no context)
276 instance Eq (T b) where ...
278 You may say of this example that we should use the instance decl right
279 away, but you can't always do that:
281 class J a b where ...
282 instance J Int b where ...
284 f :: forall a b. J a b => a -> a
286 (Notice: no functional dependency in J's class decl.)
287 Here f's type is perfectly fine, provided f is only called at Int.
288 It's premature to complain when meeting f's signature, or even
289 when inferring a type for f.
293 However, we don't *need* to report ambiguity right away. It'll always
294 show up at the call site.... and eventually at main, which needs special
295 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
297 So here's the plan. We WARN about probable ambiguity if
299 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
301 (all tested before quantification).
302 That is, all the type variables in Cq must be fixed by the the variables
303 in the environment, or by the variables in the type.
305 Notice that we union before calling oclose. Here's an example:
307 class J a b c | a b -> c
311 forall b c. (J a b c) => b -> b
313 Only if we union {a} from G with {b} from T before using oclose,
314 do we see that c is fixed.
316 It's a bit vague exactly which C we should use for this oclose call. If we
317 don't fix enough variables we might complain when we shouldn't (see
318 the above nasty example). Nothing will be perfect. That's why we can
319 only issue a warning.
322 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
324 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
326 then c is a "bubble"; there's no way it can ever improve, and it's
327 certainly ambiguous. UNLESS it is a constant (sigh). And what about
332 instance H x y => K (x,y)
334 Is this type ambiguous?
335 forall a b. (K (a,b), Eq b) => a -> a
337 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
338 is a "bubble" that's a set of constraints
340 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
342 Hence another idea. To decide Q start with fv(T) and grow it
343 by transitive closure in Cq (no functional dependencies involved).
344 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
345 The definitely-ambiguous can then float out, and get smashed at top level
346 (which squashes out the constants, like Eq (T a) above)
349 --------------------------------------
350 Notes on principal types
351 --------------------------------------
356 f x = let g y = op (y::Int) in True
358 Here the principal type of f is (forall a. a->a)
359 but we'll produce the non-principal type
360 f :: forall a. C Int => a -> a
363 --------------------------------------
364 The need for forall's in constraints
365 --------------------------------------
367 [Exchange on Haskell Cafe 5/6 Dec 2000]
369 class C t where op :: t -> Bool
370 instance C [t] where op x = True
372 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
373 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
375 The definitions of p and q differ only in the order of the components in
376 the pair on their right-hand sides. And yet:
378 ghc and "Typing Haskell in Haskell" reject p, but accept q;
379 Hugs rejects q, but accepts p;
380 hbc rejects both p and q;
381 nhc98 ... (Malcolm, can you fill in the blank for us!).
383 The type signature for f forces context reduction to take place, and
384 the results of this depend on whether or not the type of y is known,
385 which in turn depends on which component of the pair the type checker
388 Solution: if y::m a, float out the constraints
389 Monad m, forall c. C (m c)
390 When m is later unified with [], we can solve both constraints.
393 --------------------------------------
394 Notes on implicit parameters
395 --------------------------------------
397 Question 1: can we "inherit" implicit parameters
398 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
403 where f is *not* a top-level binding.
404 From the RHS of f we'll get the constraint (?y::Int).
405 There are two types we might infer for f:
409 (so we get ?y from the context of f's definition), or
411 f :: (?y::Int) => Int -> Int
413 At first you might think the first was better, becuase then
414 ?y behaves like a free variable of the definition, rather than
415 having to be passed at each call site. But of course, the WHOLE
416 IDEA is that ?y should be passed at each call site (that's what
417 dynamic binding means) so we'd better infer the second.
419 BOTTOM LINE: when *inferring types* you *must* quantify
420 over implicit parameters. See the predicate isFreeWhenInferring.
423 Question 2: type signatures
424 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
425 BUT WATCH OUT: When you supply a type signature, we can't force you
426 to quantify over implicit parameters. For example:
430 This is perfectly reasonable. We do not want to insist on
432 (?x + 1) :: (?x::Int => Int)
434 That would be silly. Here, the definition site *is* the occurrence site,
435 so the above strictures don't apply. Hence the difference between
436 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
437 and tcSimplifyCheckBind (which does not).
439 What about when you supply a type signature for a binding?
440 Is it legal to give the following explicit, user type
441 signature to f, thus:
446 At first sight this seems reasonable, but it has the nasty property
447 that adding a type signature changes the dynamic semantics.
450 (let f x = (x::Int) + ?y
451 in (f 3, f 3 with ?y=5)) with ?y = 6
457 in (f 3, f 3 with ?y=5)) with ?y = 6
461 Indeed, simply inlining f (at the Haskell source level) would change the
464 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
465 semantics for a Haskell program without knowing its typing, so if you
466 change the typing you may change the semantics.
468 To make things consistent in all cases where we are *checking* against
469 a supplied signature (as opposed to inferring a type), we adopt the
472 a signature does not need to quantify over implicit params.
474 [This represents a (rather marginal) change of policy since GHC 5.02,
475 which *required* an explicit signature to quantify over all implicit
476 params for the reasons mentioned above.]
478 But that raises a new question. Consider
480 Given (signature) ?x::Int
481 Wanted (inferred) ?x::Int, ?y::Bool
483 Clearly we want to discharge the ?x and float the ?y out. But
484 what is the criterion that distinguishes them? Clearly it isn't
485 what free type variables they have. The Right Thing seems to be
486 to float a constraint that
487 neither mentions any of the quantified type variables
488 nor any of the quantified implicit parameters
490 See the predicate isFreeWhenChecking.
493 Question 3: monomorphism
494 ~~~~~~~~~~~~~~~~~~~~~~~~
495 There's a nasty corner case when the monomorphism restriction bites:
499 The argument above suggests that we *must* generalise
500 over the ?y parameter, to get
501 z :: (?y::Int) => Int,
502 but the monomorphism restriction says that we *must not*, giving
504 Why does the momomorphism restriction say this? Because if you have
506 let z = x + ?y in z+z
508 you might not expect the addition to be done twice --- but it will if
509 we follow the argument of Question 2 and generalise over ?y.
512 Question 4: top level
513 ~~~~~~~~~~~~~~~~~~~~~
514 At the top level, monomorhism makes no sense at all.
517 main = let ?x = 5 in print foo
521 woggle :: (?x :: Int) => Int -> Int
524 We definitely don't want (foo :: Int) with a top-level implicit parameter
525 (?x::Int) becuase there is no way to bind it.
530 (A) Always generalise over implicit parameters
531 Bindings that fall under the monomorphism restriction can't
535 * Inlining remains valid
536 * No unexpected loss of sharing
537 * But simple bindings like
539 will be rejected, unless you add an explicit type signature
540 (to avoid the monomorphism restriction)
541 z :: (?y::Int) => Int
543 This seems unacceptable
545 (B) Monomorphism restriction "wins"
546 Bindings that fall under the monomorphism restriction can't
548 Always generalise over implicit parameters *except* for bindings
549 that fall under the monomorphism restriction
552 * Inlining isn't valid in general
553 * No unexpected loss of sharing
554 * Simple bindings like
556 accepted (get value of ?y from binding site)
558 (C) Always generalise over implicit parameters
559 Bindings that fall under the monomorphism restriction can't
560 be generalised, EXCEPT for implicit parameters
562 * Inlining remains valid
563 * Unexpected loss of sharing (from the extra generalisation)
564 * Simple bindings like
566 accepted (get value of ?y from occurrence sites)
571 None of these choices seems very satisfactory. But at least we should
572 decide which we want to do.
574 It's really not clear what is the Right Thing To Do. If you see
578 would you expect the value of ?y to be got from the *occurrence sites*
579 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
580 case of function definitions, the answer is clearly the former, but
581 less so in the case of non-fucntion definitions. On the other hand,
582 if we say that we get the value of ?y from the definition site of 'z',
583 then inlining 'z' might change the semantics of the program.
585 Choice (C) really says "the monomorphism restriction doesn't apply
586 to implicit parameters". Which is fine, but remember that every
587 innocent binding 'x = ...' that mentions an implicit parameter in
588 the RHS becomes a *function* of that parameter, called at each
589 use of 'x'. Now, the chances are that there are no intervening 'with'
590 clauses that bind ?y, so a decent compiler should common up all
591 those function calls. So I think I strongly favour (C). Indeed,
592 one could make a similar argument for abolishing the monomorphism
593 restriction altogether.
595 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
599 %************************************************************************
601 \subsection{tcSimplifyInfer}
603 %************************************************************************
605 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
607 1. Compute Q = grow( fvs(T), C )
609 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
610 predicates will end up in Ct; we deal with them at the top level
612 3. Try improvement, using functional dependencies
614 4. If Step 3 did any unification, repeat from step 1
615 (Unification can change the result of 'grow'.)
617 Note: we don't reduce dictionaries in step 2. For example, if we have
618 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
619 after step 2. However note that we may therefore quantify over more
620 type variables than we absolutely have to.
622 For the guts, we need a loop, that alternates context reduction and
623 improvement with unification. E.g. Suppose we have
625 class C x y | x->y where ...
627 and tcSimplify is called with:
629 Then improvement unifies a with b, giving
632 If we need to unify anything, we rattle round the whole thing all over
639 -> TcTyVarSet -- fv(T); type vars
641 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
642 TcDictBinds, -- Bindings
643 [TcId]) -- Dict Ids that must be bound here (zonked)
644 -- Any free (escaping) Insts are tossed into the environment
649 tcSimplifyInfer doc tau_tvs wanted_lie
650 = inferLoop doc (varSetElems tau_tvs)
651 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
653 extendLIEs frees `thenM_`
654 returnM (qtvs, binds, map instToId irreds)
656 inferLoop doc tau_tvs wanteds
658 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
659 mappM zonkInst wanteds `thenM` \ wanteds' ->
660 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
662 preds = fdPredsOfInsts wanteds'
663 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
666 | isFreeWhenInferring qtvs inst = Free
667 | isClassDict inst = DontReduceUnlessConstant -- Dicts
668 | otherwise = ReduceMe -- Lits and Methods
670 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
671 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
673 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
676 if no_improvement then
677 returnM (varSetElems qtvs, frees, binds, irreds)
679 -- If improvement did some unification, we go round again. There
680 -- are two subtleties:
681 -- a) We start again with irreds, not wanteds
682 -- Using an instance decl might have introduced a fresh type variable
683 -- which might have been unified, so we'd get an infinite loop
684 -- if we started again with wanteds! See example [LOOP]
686 -- b) It's also essential to re-process frees, because unification
687 -- might mean that a type variable that looked free isn't now.
689 -- Hence the (irreds ++ frees)
691 -- However, NOTICE that when we are done, we might have some bindings, but
692 -- the final qtvs might be empty. See [NO TYVARS] below.
694 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
695 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
700 class If b t e r | b t e -> r
703 class Lte a b c | a b -> c where lte :: a -> b -> c
705 instance (Lte a b l,If l b a c) => Max a b c
707 Wanted: Max Z (S x) y
709 Then we'll reduce using the Max instance to:
710 (Lte Z (S x) l, If l (S x) Z y)
711 and improve by binding l->T, after which we can do some reduction
712 on both the Lte and If constraints. What we *can't* do is start again
713 with (Max Z (S x) y)!
717 class Y a b | a -> b where
720 instance Y [[a]] a where
723 k :: X a -> X a -> X a
725 g :: Num a => [X a] -> [X a]
728 h ys = ys ++ map (k (y [[0]])) xs
730 The excitement comes when simplifying the bindings for h. Initially
731 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
732 From this we get t1:=:t2, but also various bindings. We can't forget
733 the bindings (because of [LOOP]), but in fact t1 is what g is
736 The net effect of [NO TYVARS]
739 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
740 isFreeWhenInferring qtvs inst
741 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
742 && isInheritableInst inst -- And no implicit parameter involved
743 -- (see "Notes on implicit parameters")
745 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
746 -> NameSet -- Quantified implicit parameters
748 isFreeWhenChecking qtvs ips inst
749 = isFreeWrtTyVars qtvs inst
750 && isFreeWrtIPs ips inst
752 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
753 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
757 %************************************************************************
759 \subsection{tcSimplifyCheck}
761 %************************************************************************
763 @tcSimplifyCheck@ is used when we know exactly the set of variables
764 we are going to quantify over. For example, a class or instance declaration.
769 -> [TcTyVar] -- Quantify over these
772 -> TcM TcDictBinds -- Bindings
774 -- tcSimplifyCheck is used when checking expression type signatures,
775 -- class decls, instance decls etc.
777 -- NB: tcSimplifyCheck does not consult the
778 -- global type variables in the environment; so you don't
779 -- need to worry about setting them before calling tcSimplifyCheck
780 tcSimplifyCheck doc qtvs givens wanted_lie
781 = tcSimplCheck doc get_qtvs
782 givens wanted_lie `thenM` \ (qtvs', binds) ->
785 -- get_qtvs = zonkTcTyVarsAndFV qtvs
786 get_qtvs = return (mkVarSet qtvs)
789 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
790 -- against, but we don't know the type variables over which we are going to quantify.
791 -- This happens when we have a type signature for a mutually recursive group
794 -> TcTyVarSet -- fv(T)
797 -> TcM ([TcTyVar], -- Variables over which to quantify
798 TcDictBinds) -- Bindings
800 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
801 = tcSimplCheck doc get_qtvs givens wanted_lie
803 -- Figure out which type variables to quantify over
804 -- You might think it should just be the signature tyvars,
805 -- but in bizarre cases you can get extra ones
806 -- f :: forall a. Num a => a -> a
807 -- f x = fst (g (x, head [])) + 1
809 -- Here we infer g :: forall a b. a -> b -> (b,a)
810 -- We don't want g to be monomorphic in b just because
811 -- f isn't quantified over b.
812 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
814 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
815 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
817 qtvs = all_tvs' `minusVarSet` gbl_tvs
818 -- We could close gbl_tvs, but its not necessary for
819 -- soundness, and it'll only affect which tyvars, not which
820 -- dictionaries, we quantify over
825 Here is the workhorse function for all three wrappers.
828 tcSimplCheck doc get_qtvs givens wanted_lie
829 = check_loop givens wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
831 -- Complain about any irreducible ones
832 mappM zonkInst given_dicts_and_ips `thenM` \ givens' ->
833 groupErrs (addNoInstanceErrs (Just doc) givens') irreds `thenM_`
836 extendLIEs frees `thenM_`
837 returnM (qtvs, binds)
840 given_dicts_and_ips = filter (not . isMethod) givens
841 -- For error reporting, filter out methods, which are
842 -- only added to the given set as an optimisation
844 ip_set = mkNameSet (ipNamesOfInsts givens)
846 check_loop givens wanteds
848 mappM zonkInst givens `thenM` \ givens' ->
849 mappM zonkInst wanteds `thenM` \ wanteds' ->
850 get_qtvs `thenM` \ qtvs' ->
854 -- When checking against a given signature we always reduce
855 -- until we find a match against something given, or can't reduce
856 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
857 | otherwise = ReduceMe
859 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
862 if no_improvement then
863 returnM (varSetElems qtvs', frees, binds, irreds)
865 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
866 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
870 %************************************************************************
872 \subsection{tcSimplifyRestricted}
874 %************************************************************************
876 tcSimplifyRestricted infers which type variables to quantify for a
877 group of restricted bindings. This isn't trivial.
880 We want to quantify over a to get id :: forall a. a->a
883 We do not want to quantify over a, because there's an Eq a
884 constraint, so we get eq :: a->a->Bool (notice no forall)
887 RHS has type 'tau', whose free tyvars are tau_tvs
888 RHS has constraints 'wanteds'
891 Quantify over (tau_tvs \ ftvs(wanteds))
892 This is bad. The constraints may contain (Monad (ST s))
893 where we have instance Monad (ST s) where...
894 so there's no need to be monomorphic in s!
896 Also the constraint might be a method constraint,
897 whose type mentions a perfectly innocent tyvar:
898 op :: Num a => a -> b -> a
899 Here, b is unconstrained. A good example would be
901 We want to infer the polymorphic type
902 foo :: forall b. b -> b
905 Plan B (cunning, used for a long time up to and including GHC 6.2)
906 Step 1: Simplify the constraints as much as possible (to deal
907 with Plan A's problem). Then set
908 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
910 Step 2: Now simplify again, treating the constraint as 'free' if
911 it does not mention qtvs, and trying to reduce it otherwise.
912 The reasons for this is to maximise sharing.
914 This fails for a very subtle reason. Suppose that in the Step 2
915 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
916 In the Step 1 this constraint might have been simplified, perhaps to
917 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
918 This won't happen in Step 2... but that in turn might prevent some other
919 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
920 and that in turn breaks the invariant that no constraints are quantified over.
922 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
927 Step 1: Simplify the constraints as much as possible (to deal
928 with Plan A's problem). Then set
929 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
930 Return the bindings from Step 1.
933 A note about Plan C (arising from "bug" reported by George Russel March 2004)
936 instance (HasBinary ty IO) => HasCodedValue ty
938 foo :: HasCodedValue a => String -> IO a
940 doDecodeIO :: HasCodedValue a => () -> () -> IO a
941 doDecodeIO codedValue view
942 = let { act = foo "foo" } in act
944 You might think this should work becuase the call to foo gives rise to a constraint
945 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
946 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
947 constraint using the (rather bogus) instance declaration, and now we are stuffed.
949 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
953 Plan D (a variant of plan B)
954 Step 1: Simplify the constraints as much as possible (to deal
955 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
956 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
958 Step 2: Now simplify again, treating the constraint as 'free' if
959 it does not mention qtvs, and trying to reduce it otherwise.
961 The point here is that it's generally OK to have too few qtvs; that is,
962 to make the thing more monomorphic than it could be. We don't want to
963 do that in the common cases, but in wierd cases it's ok: the programmer
964 can always add a signature.
966 Too few qtvs => too many wanteds, which is what happens if you do less
971 tcSimplifyRestricted -- Used for restricted binding groups
972 -- i.e. ones subject to the monomorphism restriction
975 -> [Name] -- Things bound in this group
976 -> TcTyVarSet -- Free in the type of the RHSs
977 -> [Inst] -- Free in the RHSs
978 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
979 TcDictBinds) -- Bindings
980 -- tcSimpifyRestricted returns no constraints to
981 -- quantify over; by definition there are none.
982 -- They are all thrown back in the LIE
984 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
985 -- Zonk everything in sight
986 = mappM zonkInst wanteds `thenM` \ wanteds' ->
987 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
988 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
990 -- 'reduceMe': Reduce as far as we can. Don't stop at
991 -- dicts; the idea is to get rid of as many type
992 -- variables as possible, and we don't want to stop
993 -- at (say) Monad (ST s), because that reduces
994 -- immediately, with no constraint on s.
996 -- BUT do no improvement! See Plan D above
997 reduceContextWithoutImprovement
998 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1000 -- Next, figure out the tyvars we will quantify over
1002 constrained_tvs = tyVarsOfInsts constrained_dicts
1003 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1004 `minusVarSet` constrained_tvs
1006 traceTc (text "tcSimplifyRestricted" <+> vcat [
1007 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1009 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1011 -- The first step may have squashed more methods than
1012 -- necessary, so try again, this time more gently, knowing the exact
1013 -- set of type variables to quantify over.
1015 -- We quantify only over constraints that are captured by qtvs;
1016 -- these will just be a subset of non-dicts. This in contrast
1017 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1018 -- all *non-inheritable* constraints too. This implements choice
1019 -- (B) under "implicit parameter and monomorphism" above.
1021 -- Remember that we may need to do *some* simplification, to
1022 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1023 -- just to float all constraints
1025 -- At top level, we *do* squash methods becuase we want to
1026 -- expose implicit parameters to the test that follows
1028 is_nested_group = isNotTopLevel top_lvl
1029 try_me inst | isFreeWrtTyVars qtvs inst,
1030 (is_nested_group || isDict inst) = Free
1031 | otherwise = ReduceMe
1033 reduceContextWithoutImprovement
1034 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1035 ASSERT( null irreds )
1037 -- See "Notes on implicit parameters, Question 4: top level"
1038 if is_nested_group then
1039 extendLIEs frees `thenM_`
1040 returnM (varSetElems qtvs, binds)
1043 (non_ips, bad_ips) = partition isClassDict frees
1045 addTopIPErrs bndrs bad_ips `thenM_`
1046 extendLIEs non_ips `thenM_`
1047 returnM (varSetElems qtvs, binds)
1051 %************************************************************************
1053 \subsection{tcSimplifyToDicts}
1055 %************************************************************************
1057 On the LHS of transformation rules we only simplify methods and constants,
1058 getting dictionaries. We want to keep all of them unsimplified, to serve
1059 as the available stuff for the RHS of the rule.
1061 The same thing is used for specialise pragmas. Consider
1063 f :: Num a => a -> a
1064 {-# SPECIALISE f :: Int -> Int #-}
1067 The type checker generates a binding like:
1069 f_spec = (f :: Int -> Int)
1071 and we want to end up with
1073 f_spec = _inline_me_ (f Int dNumInt)
1075 But that means that we must simplify the Method for f to (f Int dNumInt)!
1076 So tcSimplifyToDicts squeezes out all Methods.
1078 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
1080 fromIntegral :: (Integral a, Num b) => a -> b
1081 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1083 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
1086 forall dIntegralInt.
1087 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1089 because the scsel will mess up matching. Instead we want
1091 forall dIntegralInt, dNumInt.
1092 fromIntegral Int Int dIntegralInt dNumInt = id Int
1097 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
1098 tcSimplifyToDicts wanteds
1099 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1100 -- Since try_me doesn't look at types, we don't need to
1101 -- do any zonking, so it's safe to call reduceContext directly
1102 ASSERT( null frees )
1103 extendLIEs irreds `thenM_`
1107 doc = text "tcSimplifyToDicts"
1109 -- Reduce methods and lits only; stop as soon as we get a dictionary
1110 try_me inst | isDict inst = KeepDictWithoutSCs -- See notes above re "WithoutSCs"
1111 | otherwise = ReduceMe
1116 tcSimplifyBracket is used when simplifying the constraints arising from
1117 a Template Haskell bracket [| ... |]. We want to check that there aren't
1118 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1119 Show instance), but we aren't otherwise interested in the results.
1120 Nor do we care about ambiguous dictionaries etc. We will type check
1121 this bracket again at its usage site.
1124 tcSimplifyBracket :: [Inst] -> TcM ()
1125 tcSimplifyBracket wanteds
1126 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1129 doc = text "tcSimplifyBracket"
1133 %************************************************************************
1135 \subsection{Filtering at a dynamic binding}
1137 %************************************************************************
1142 we must discharge all the ?x constraints from B. We also do an improvement
1143 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1145 Actually, the constraints from B might improve the types in ?x. For example
1147 f :: (?x::Int) => Char -> Char
1150 then the constraint (?x::Int) arising from the call to f will
1151 force the binding for ?x to be of type Int.
1154 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1157 tcSimplifyIPs given_ips wanteds
1158 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1159 extendLIEs frees `thenM_`
1162 doc = text "tcSimplifyIPs" <+> ppr given_ips
1163 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1165 -- Simplify any methods that mention the implicit parameter
1166 try_me inst | isFreeWrtIPs ip_set inst = Free
1167 | otherwise = ReduceMe
1169 simpl_loop givens wanteds
1170 = mappM zonkInst givens `thenM` \ givens' ->
1171 mappM zonkInst wanteds `thenM` \ wanteds' ->
1173 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1175 if no_improvement then
1176 ASSERT( null irreds )
1177 returnM (frees, binds)
1179 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1180 returnM (frees1, binds `unionBags` binds1)
1184 %************************************************************************
1186 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1188 %************************************************************************
1190 When doing a binding group, we may have @Insts@ of local functions.
1191 For example, we might have...
1193 let f x = x + 1 -- orig local function (overloaded)
1194 f.1 = f Int -- two instances of f
1199 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1200 where @f@ is in scope; those @Insts@ must certainly not be passed
1201 upwards towards the top-level. If the @Insts@ were binding-ified up
1202 there, they would have unresolvable references to @f@.
1204 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1205 For each method @Inst@ in the @init_lie@ that mentions one of the
1206 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1207 @LIE@), as well as the @HsBinds@ generated.
1210 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1211 -- Simlifies only MethodInsts, and generate only bindings of form
1213 -- We're careful not to even generate bindings of the form
1215 -- You'd think that'd be fine, but it interacts with what is
1216 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1218 bindInstsOfLocalFuns wanteds local_ids
1219 | null overloaded_ids
1221 = extendLIEs wanteds `thenM_`
1222 returnM emptyLHsBinds
1225 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1226 ASSERT( null irreds )
1227 extendLIEs not_for_me `thenM_`
1228 extendLIEs frees `thenM_`
1231 doc = text "bindInsts" <+> ppr local_ids
1232 overloaded_ids = filter is_overloaded local_ids
1233 is_overloaded id = isOverloadedTy (idType id)
1234 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1236 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1237 -- so it's worth building a set, so that
1238 -- lookup (in isMethodFor) is faster
1239 try_me inst | isMethod inst = ReduceMe
1244 %************************************************************************
1246 \subsection{Data types for the reduction mechanism}
1248 %************************************************************************
1250 The main control over context reduction is here
1254 = ReduceMe -- Try to reduce this
1255 -- If there's no instance, behave exactly like
1256 -- DontReduce: add the inst to
1257 -- the irreductible ones, but don't
1258 -- produce an error message of any kind.
1259 -- It might be quite legitimate such as (Eq a)!
1261 | KeepDictWithoutSCs -- Return as irreducible; don't add its superclasses
1262 -- Rather specialised: see notes with tcSimplifyToDicts
1264 | DontReduceUnlessConstant -- Return as irreducible unless it can
1265 -- be reduced to a constant in one step
1267 | Free -- Return as free
1269 reduceMe :: Inst -> WhatToDo
1270 reduceMe inst = ReduceMe
1272 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1273 -- of a predicate when adding it to the avails
1279 type Avails = FiniteMap Inst Avail
1280 emptyAvails = emptyFM
1283 = IsFree -- Used for free Insts
1284 | Irred -- Used for irreducible dictionaries,
1285 -- which are going to be lambda bound
1287 | Given TcId -- Used for dictionaries for which we have a binding
1288 -- e.g. those "given" in a signature
1289 Bool -- True <=> actually consumed (splittable IPs only)
1291 | NoRhs -- Used for Insts like (CCallable f)
1292 -- where no witness is required.
1295 | Rhs -- Used when there is a RHS
1296 (LHsExpr TcId) -- The RHS
1297 [Inst] -- Insts free in the RHS; we need these too
1299 | Linear -- Splittable Insts only.
1300 Int -- The Int is always 2 or more; indicates how
1301 -- many copies are required
1302 Inst -- The splitter
1303 Avail -- Where the "master copy" is
1305 | LinRhss -- Splittable Insts only; this is used only internally
1306 -- by extractResults, where a Linear
1307 -- is turned into an LinRhss
1308 [LHsExpr TcId] -- A supply of suitable RHSs
1310 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1311 | (inst,avail) <- fmToList avails ]
1313 instance Outputable Avail where
1316 pprAvail NoRhs = text "<no rhs>"
1317 pprAvail IsFree = text "Free"
1318 pprAvail Irred = text "Irred"
1319 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1320 if b then text "(used)" else empty
1321 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1322 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1323 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1326 Extracting the bindings from a bunch of Avails.
1327 The bindings do *not* come back sorted in dependency order.
1328 We assume that they'll be wrapped in a big Rec, so that the
1329 dependency analyser can sort them out later
1333 extractResults :: Avails
1335 -> TcM (TcDictBinds, -- Bindings
1336 [Inst], -- Irreducible ones
1337 [Inst]) -- Free ones
1339 extractResults avails wanteds
1340 = go avails emptyBag [] [] wanteds
1342 go avails binds irreds frees []
1343 = returnM (binds, irreds, frees)
1345 go avails binds irreds frees (w:ws)
1346 = case lookupFM avails w of
1347 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1348 go avails binds irreds frees ws
1350 Just NoRhs -> go avails binds irreds frees ws
1351 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1352 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1354 Just (Given id _) -> go avails new_binds irreds frees ws
1356 new_binds | id == instToId w = binds
1357 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1358 -- The sought Id can be one of the givens, via a superclass chain
1359 -- and then we definitely don't want to generate an x=x binding!
1361 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1363 new_binds = addBind binds w rhs
1365 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1366 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1367 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1368 go (addToFM avails w (LinRhss rhss))
1369 (binds `unionBags` binds')
1370 irreds' frees' (split_inst : w : ws)
1372 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1373 -> go new_avails new_binds irreds frees ws
1375 new_binds = addBind binds w rhs
1376 new_avails = addToFM avails w (LinRhss rhss)
1378 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1379 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1380 returnM (w':irreds, frees, instToId w')
1381 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1382 returnM (irreds, w':frees, instToId w')
1385 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1386 | otherwise = addToFM avails w NoRhs
1387 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1388 -- than Given, else we end up with bogus bindings.
1390 add_free avails w | isMethod w = avails
1391 | otherwise = add_given avails w
1393 -- Do *not* replace Free by Given if it's a method.
1394 -- The following situation shows why this is bad:
1395 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1396 -- From an application (truncate f i) we get
1397 -- t1 = truncate at f
1399 -- If we have also have a second occurrence of truncate, we get
1400 -- t3 = truncate at f
1402 -- When simplifying with i,f free, we might still notice that
1403 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1404 -- will continue to float out!
1405 -- (split n i a) returns: n rhss
1406 -- auxiliary bindings
1407 -- 1 or 0 insts to add to irreds
1410 split :: Int -> TcId -> TcId -> Inst
1411 -> TcM (TcDictBinds, [LHsExpr TcId])
1412 -- (split n split_id root_id wanted) returns
1413 -- * a list of 'n' expressions, all of which witness 'avail'
1414 -- * a bunch of auxiliary bindings to support these expressions
1415 -- * one or zero insts needed to witness the whole lot
1416 -- (maybe be zero if the initial Inst is a Given)
1418 -- NB: 'wanted' is just a template
1420 split n split_id root_id wanted
1423 ty = linearInstType wanted
1424 pair_ty = mkTyConApp pairTyCon [ty,ty]
1425 id = instToId wanted
1428 span = instSpan wanted
1430 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1432 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1433 expand n rhss `thenM` \ (binds2, rhss') ->
1434 returnM (binds1 `unionBags` binds2, rhss')
1437 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1438 -- e.g. expand 3 [rhs1, rhs2]
1439 -- = ( { x = split rhs1 },
1440 -- [fst x, snd x, rhs2] )
1442 | n `rem` 2 == 0 = go rhss -- n is even
1443 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1444 returnM (binds', head rhss : rhss')
1446 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1447 returnM (listToBag binds', concat rhss')
1449 do_one rhs = newUnique `thenM` \ uniq ->
1450 tcLookupId fstName `thenM` \ fst_id ->
1451 tcLookupId sndName `thenM` \ snd_id ->
1453 x = mkUserLocal occ uniq pair_ty loc
1455 returnM (L span (VarBind x (mk_app span split_id rhs)),
1456 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1458 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1460 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1462 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1463 (VarBind (instToId inst) rhs))
1464 instSpan wanted = instLocSrcSpan (instLoc wanted)
1468 %************************************************************************
1470 \subsection[reduce]{@reduce@}
1472 %************************************************************************
1474 When the "what to do" predicate doesn't depend on the quantified type variables,
1475 matters are easier. We don't need to do any zonking, unless the improvement step
1476 does something, in which case we zonk before iterating.
1478 The "given" set is always empty.
1481 simpleReduceLoop :: SDoc
1482 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1484 -> TcM ([Inst], -- Free
1486 [Inst]) -- Irreducible
1488 simpleReduceLoop doc try_me wanteds
1489 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1490 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1491 if no_improvement then
1492 returnM (frees, binds, irreds)
1494 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1495 returnM (frees1, binds `unionBags` binds1, irreds1)
1501 reduceContext :: SDoc
1502 -> (Inst -> WhatToDo)
1505 -> TcM (Bool, -- True <=> improve step did no unification
1507 TcDictBinds, -- Dictionary bindings
1508 [Inst]) -- Irreducible
1510 reduceContext doc try_me givens wanteds
1512 traceTc (text "reduceContext" <+> (vcat [
1513 text "----------------------",
1515 text "given" <+> ppr givens,
1516 text "wanted" <+> ppr wanteds,
1517 text "----------------------"
1520 -- Build the Avail mapping from "givens"
1521 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1524 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1526 -- Do improvement, using everything in avails
1527 -- In particular, avails includes all superclasses of everything
1528 tcImprove avails `thenM` \ no_improvement ->
1530 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1532 traceTc (text "reduceContext end" <+> (vcat [
1533 text "----------------------",
1535 text "given" <+> ppr givens,
1536 text "wanted" <+> ppr wanteds,
1538 text "avails" <+> pprAvails avails,
1539 text "frees" <+> ppr frees,
1540 text "no_improvement =" <+> ppr no_improvement,
1541 text "----------------------"
1544 returnM (no_improvement, frees, binds, irreds)
1546 -- reduceContextWithoutImprovement differs from reduceContext
1547 -- (a) no improvement
1548 -- (b) 'givens' is assumed empty
1549 reduceContextWithoutImprovement doc try_me wanteds
1551 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1552 text "----------------------",
1554 text "wanted" <+> ppr wanteds,
1555 text "----------------------"
1559 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1560 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1562 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1563 text "----------------------",
1565 text "wanted" <+> ppr wanteds,
1567 text "avails" <+> pprAvails avails,
1568 text "frees" <+> ppr frees,
1569 text "----------------------"
1572 returnM (frees, binds, irreds)
1574 tcImprove :: Avails -> TcM Bool -- False <=> no change
1575 -- Perform improvement using all the predicates in Avails
1577 = tcGetInstEnvs `thenM` \ inst_envs ->
1579 preds = [ (pred, pp_loc)
1580 | (inst, avail) <- fmToList avails,
1581 pred <- get_preds inst avail,
1582 let pp_loc = pprInstLoc (instLoc inst)
1584 -- Avails has all the superclasses etc (good)
1585 -- It also has all the intermediates of the deduction (good)
1586 -- It does not have duplicates (good)
1587 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1588 -- so that improve will see them separate
1590 -- For free Methods, we want to take predicates from their context,
1591 -- but for Methods that have been squished their context will already
1592 -- be in Avails, and we don't want duplicates. Hence this rather
1593 -- horrid get_preds function
1594 get_preds inst IsFree = fdPredsOfInst inst
1595 get_preds inst other | isDict inst = [dictPred inst]
1598 eqns = improve get_insts preds
1599 get_insts clas = classInstances inst_envs clas
1604 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1605 mappM_ unify eqns `thenM_`
1608 unify ((qtvs, pairs), doc)
1610 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1611 mapM_ (unif_pr tenv) pairs
1612 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1615 The main context-reduction function is @reduce@. Here's its game plan.
1618 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1619 -- along with its depth
1620 -> (Inst -> WhatToDo)
1627 try_me: given an inst, this function returns
1629 DontReduce return this in "irreds"
1630 Free return this in "frees"
1632 wanteds: The list of insts to reduce
1633 state: An accumulating parameter of type Avails
1634 that contains the state of the algorithm
1636 It returns a Avails.
1638 The (n,stack) pair is just used for error reporting.
1639 n is always the depth of the stack.
1640 The stack is the stack of Insts being reduced: to produce X
1641 I had to produce Y, to produce Y I had to produce Z, and so on.
1644 reduceList (n,stack) try_me wanteds state
1645 | n > opt_MaxContextReductionDepth
1646 = failWithTc (reduceDepthErr n stack)
1652 pprTrace "Interesting! Context reduction stack deeper than 8:"
1653 (nest 2 (pprStack stack))
1658 go [] state = returnM state
1659 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1662 -- Base case: we're done!
1663 reduce stack try_me wanted avails
1664 -- It's the same as an existing inst, or a superclass thereof
1665 | Just avail <- isAvailable avails wanted
1666 = if isLinearInst wanted then
1667 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1668 reduceList stack try_me wanteds' avails'
1670 returnM avails -- No op for non-linear things
1673 = case try_me wanted of {
1675 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1677 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1678 -- First, see if the inst can be reduced to a constant in one step
1679 try_simple (addIrred AddSCs) -- Assume want superclasses
1681 ; Free -> -- It's free so just chuck it upstairs
1682 -- First, see if the inst can be reduced to a constant in one step
1685 ; ReduceMe -> -- It should be reduced
1686 lookupInst wanted `thenM` \ lookup_result ->
1687 case lookup_result of
1688 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1689 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1690 addWanted avails2 wanted rhs wanteds'
1691 -- Experiment with temporarily doing addIrred *before* the reduceList,
1692 -- which has the effect of adding the thing we are trying
1693 -- to prove to the database before trying to prove the things it
1694 -- needs. See note [RECURSIVE DICTIONARIES]
1695 -- NB: we must not do an addWanted before, because that adds the
1696 -- superclasses too, and thaat can lead to a spurious loop; see
1697 -- the examples in [SUPERCLASS-LOOP]
1698 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1700 SimpleInst rhs -> addWanted avails wanted rhs []
1702 NoInstance -> -- No such instance!
1703 -- Add it and its superclasses
1704 addIrred AddSCs avails wanted
1707 try_simple do_this_otherwise
1708 = lookupInst wanted `thenM` \ lookup_result ->
1709 case lookup_result of
1710 SimpleInst rhs -> addWanted avails wanted rhs []
1711 other -> do_this_otherwise avails wanted
1716 -------------------------
1717 isAvailable :: Avails -> Inst -> Maybe Avail
1718 isAvailable avails wanted = lookupFM avails wanted
1719 -- NB 1: the Ord instance of Inst compares by the class/type info
1720 -- *not* by unique. So
1721 -- d1::C Int == d2::C Int
1723 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1724 addLinearAvailable avails avail wanted
1725 -- avails currently maps [wanted -> avail]
1726 -- Extend avails to reflect a neeed for an extra copy of avail
1728 | Just avail' <- split_avail avail
1729 = returnM (addToFM avails wanted avail', [])
1732 = tcLookupId splitName `thenM` \ split_id ->
1733 tcInstClassOp (instLoc wanted) split_id
1734 [linearInstType wanted] `thenM` \ split_inst ->
1735 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1738 split_avail :: Avail -> Maybe Avail
1739 -- (Just av) if there's a modified version of avail that
1740 -- we can use to replace avail in avails
1741 -- Nothing if there isn't, so we need to create a Linear
1742 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1743 split_avail (Given id used) | not used = Just (Given id True)
1744 | otherwise = Nothing
1745 split_avail Irred = Nothing
1746 split_avail IsFree = Nothing
1747 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1749 -------------------------
1750 addFree :: Avails -> Inst -> TcM Avails
1751 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1752 -- to avails, so that any other equal Insts will be commoned up right
1753 -- here rather than also being tossed upstairs. This is really just
1754 -- an optimisation, and perhaps it is more trouble that it is worth,
1755 -- as the following comments show!
1757 -- NB: do *not* add superclasses. If we have
1760 -- but a is not bound here, then we *don't* want to derive
1761 -- dn from df here lest we lose sharing.
1763 addFree avails free = returnM (addToFM avails free IsFree)
1765 addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1766 addWanted avails wanted rhs_expr wanteds
1767 = addAvailAndSCs avails wanted avail
1769 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1770 | otherwise = ASSERT( null wanteds ) NoRhs
1772 addGiven :: Avails -> Inst -> TcM Avails
1773 addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
1774 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1775 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1776 -- so the assert isn't true
1778 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1779 addIrred NoSCs avails irred = returnM (addToFM avails irred Irred)
1780 addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1781 addAvailAndSCs avails irred Irred
1783 addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
1784 addAvailAndSCs avails inst avail
1785 | not (isClassDict inst) = returnM avails1
1786 | otherwise = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
1787 addSCs is_loop avails1 inst
1789 avails1 = addToFM avails inst avail
1790 is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
1791 -- Note: this compares by *type*, not by Unique
1792 deps = findAllDeps (unitVarSet (instToId inst)) avail
1793 dep_tys = map idType (varSetElems deps)
1795 findAllDeps :: IdSet -> Avail -> IdSet
1796 -- Find all the Insts that this one depends on
1797 -- See Note [SUPERCLASS-LOOP]
1798 -- Watch out, though. Since the avails may contain loops
1799 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1800 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1801 findAllDeps so_far other = so_far
1803 find_all :: IdSet -> Inst -> IdSet
1805 | kid_id `elemVarSet` so_far = so_far
1806 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1807 | otherwise = so_far'
1809 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1810 kid_id = instToId kid
1812 addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
1813 -- Add all the superclasses of the Inst to Avails
1814 -- The first param says "dont do this because the original thing
1815 -- depends on this one, so you'd build a loop"
1816 -- Invariant: the Inst is already in Avails.
1818 addSCs is_loop avails dict
1819 = newDictsFromOld dict sc_theta' `thenM` \ sc_dicts ->
1820 foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1822 (clas, tys) = getDictClassTys dict
1823 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1824 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1826 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1827 | add_me sc_dict = addSCs is_loop avails' sc_dict
1828 | otherwise = returnM avails
1830 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1831 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1833 add_me :: Inst -> Bool
1835 | is_loop sc_dict = False -- See Note [SUPERCLASS-LOOP]
1836 | otherwise = case lookupFM avails sc_dict of
1837 Just (Given _ _) -> False -- Given is cheaper than superclass selection
1841 Note [SUPERCLASS-LOOP]: Checking for loops
1842 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1843 We have to be careful here. If we are *given* d1:Ord a,
1844 and want to deduce (d2:C [a]) where
1846 class Ord a => C a where
1847 instance Ord [a] => C [a] where ...
1849 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1850 superclasses of C [a] to avails. But we must not overwrite the binding
1851 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1854 Here's another variant, immortalised in tcrun020
1855 class Monad m => C1 m
1856 class C1 m => C2 m x
1857 instance C2 Maybe Bool
1858 For the instance decl we need to build (C1 Maybe), and it's no good if
1859 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1860 before we search for C1 Maybe.
1862 Here's another example
1863 class Eq b => Foo a b
1864 instance Eq a => Foo [a] a
1868 we'll first deduce that it holds (via the instance decl). We must not
1869 then overwrite the Eq t constraint with a superclass selection!
1871 At first I had a gross hack, whereby I simply did not add superclass constraints
1872 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1873 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1874 I found a very obscure program (now tcrun021) in which improvement meant the
1875 simplifier got two bites a the cherry... so something seemed to be an Irred
1876 first time, but reducible next time.
1878 Now we implement the Right Solution, which is to check for loops directly
1879 when adding superclasses. It's a bit like the occurs check in unification.
1882 Note [RECURSIVE DICTIONARIES]
1883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1885 data D r = ZeroD | SuccD (r (D r));
1887 instance (Eq (r (D r))) => Eq (D r) where
1888 ZeroD == ZeroD = True
1889 (SuccD a) == (SuccD b) = a == b
1892 equalDC :: D [] -> D [] -> Bool;
1895 We need to prove (Eq (D [])). Here's how we go:
1899 by instance decl, holds if
1903 by instance decl of Eq, holds if
1905 where d2 = dfEqList d3
1908 But now we can "tie the knot" to give
1914 and it'll even run! The trick is to put the thing we are trying to prove
1915 (in this case Eq (D []) into the database before trying to prove its
1916 contributing clauses.
1919 %************************************************************************
1921 \section{tcSimplifyTop: defaulting}
1923 %************************************************************************
1926 @tcSimplifyTop@ is called once per module to simplify all the constant
1927 and ambiguous Insts.
1929 We need to be careful of one case. Suppose we have
1931 instance Num a => Num (Foo a b) where ...
1933 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1934 to (Num x), and default x to Int. But what about y??
1936 It's OK: the final zonking stage should zap y to (), which is fine.
1940 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
1941 tcSimplifyTop wanteds = tc_simplify_top False {- Not interactive loop -} wanteds
1942 tcSimplifyInteractive wanteds = tc_simplify_top True {- Interactive loop -} wanteds
1945 -- The TcLclEnv should be valid here, solely to improve
1946 -- error message generation for the monomorphism restriction
1947 tc_simplify_top is_interactive wanteds
1948 = getLclEnv `thenM` \ lcl_env ->
1949 traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env)) `thenM_`
1950 simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenM` \ (frees, binds, irreds) ->
1951 ASSERT( null frees )
1954 -- All the non-std ones are definite errors
1955 (stds, non_stds) = partition isStdClassTyVarDict irreds
1957 -- Group by type variable
1958 std_groups = equivClasses cmp_by_tyvar stds
1960 -- Pick the ones which its worth trying to disambiguate
1961 -- namely, the onese whose type variable isn't bound
1962 -- up with one of the non-standard classes
1963 (std_oks, std_bads) = partition worth_a_try std_groups
1964 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1965 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1967 -- Collect together all the bad guys
1968 bad_guys = non_stds ++ concat std_bads
1969 (non_ips, bad_ips) = partition isClassDict bad_guys
1970 (ambigs, no_insts) = partition is_ambig non_ips
1971 is_ambig d = not (tyVarsOfInst d `subVarSet` fixed_tvs)
1972 fixed_tvs = oclose (fdPredsOfInsts irreds) emptyVarSet
1973 -- If the dict has free type variables, it's almost certainly ambiguous,
1974 -- and that's the first thing to fix.
1975 -- Otherwise, addNoInstanceErrs does the right thing
1976 -- I say "almost certain" because we might have
1977 -- class C a b | a -> B where ...
1978 -- plus an Inst (C Int x). Then the 'x' isn't ambiguous; it's just that
1979 -- there's no instance decl for (C Int ...). Hence the oclose.
1982 -- Report definite errors
1983 groupErrs (addNoInstanceErrs Nothing []) no_insts `thenM_`
1984 strangeTopIPErrs bad_ips `thenM_`
1986 -- Deal with ambiguity errors, but only if
1987 -- if there has not been an error so far:
1988 -- errors often give rise to spurious ambiguous Insts.
1990 -- f = (*) -- Monomorphic
1991 -- g :: Num a => a -> a
1993 -- Here, we get a complaint when checking the type signature for g,
1994 -- that g isn't polymorphic enough; but then we get another one when
1995 -- dealing with the (Num a) context arising from f's definition;
1996 -- we try to unify a with Int (to default it), but find that it's
1997 -- already been unified with the rigid variable from g's type sig
1998 ifErrsM (returnM []) (
2000 -- Complain about the ones that don't fall under
2001 -- the Haskell rules for disambiguation
2002 -- This group includes both non-existent instances
2003 -- e.g. Num (IO a) and Eq (Int -> Int)
2004 -- and ambiguous dictionaries
2006 addTopAmbigErrs ambigs `thenM_`
2008 -- Disambiguate the ones that look feasible
2009 mappM (disambigGroup is_interactive) std_oks
2010 ) `thenM` \ binds_ambig ->
2012 returnM (binds `unionBags` unionManyBags binds_ambig)
2014 ----------------------------------
2015 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2017 get_tv d = case getDictClassTys d of
2018 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2019 get_clas d = case getDictClassTys d of
2020 (clas, [ty]) -> clas
2023 If a dictionary constrains a type variable which is
2024 * not mentioned in the environment
2025 * and not mentioned in the type of the expression
2026 then it is ambiguous. No further information will arise to instantiate
2027 the type variable; nor will it be generalised and turned into an extra
2028 parameter to a function.
2030 It is an error for this to occur, except that Haskell provided for
2031 certain rules to be applied in the special case of numeric types.
2033 * at least one of its classes is a numeric class, and
2034 * all of its classes are numeric or standard
2035 then the type variable can be defaulted to the first type in the
2036 default-type list which is an instance of all the offending classes.
2038 So here is the function which does the work. It takes the ambiguous
2039 dictionaries and either resolves them (producing bindings) or
2040 complains. It works by splitting the dictionary list by type
2041 variable, and using @disambigOne@ to do the real business.
2043 @disambigOne@ assumes that its arguments dictionaries constrain all
2044 the same type variable.
2046 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2047 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2048 the most common use of defaulting is code like:
2050 _ccall_ foo `seqPrimIO` bar
2052 Since we're not using the result of @foo@, the result if (presumably)
2056 disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
2057 -> [Inst] -- All standard classes of form (C a)
2060 disambigGroup is_interactive dicts
2061 | any std_default_class classes -- Guaranteed all standard classes
2062 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2063 -- SO, TRY DEFAULT TYPES IN ORDER
2065 -- Failure here is caused by there being no type in the
2066 -- default list which can satisfy all the ambiguous classes.
2067 -- For example, if Real a is reqd, but the only type in the
2068 -- default list is Int.
2069 get_default_tys `thenM` \ default_tys ->
2071 try_default [] -- No defaults work, so fail
2074 try_default (default_ty : default_tys)
2075 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2076 -- default_tys instead
2077 tcSimplifyDefault theta `thenM` \ _ ->
2080 theta = [mkClassPred clas [default_ty] | clas <- classes]
2082 -- See if any default works
2083 tryM (try_default default_tys) `thenM` \ mb_ty ->
2086 Right chosen_default_ty -> choose_default chosen_default_ty
2088 | otherwise -- No defaults
2092 tyvar = get_tv (head dicts) -- Should be non-empty
2093 classes = map get_clas dicts
2095 std_default_class cls
2096 = isNumericClass cls
2097 || (is_interactive &&
2098 classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2099 -- In interactive mode, we default Show a to Show ()
2100 -- to avoid graututious errors on "show []"
2102 choose_default default_ty -- Commit to tyvar = default_ty
2103 = -- Bind the type variable
2104 unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
2105 -- and reduce the context, for real this time
2106 simpleReduceLoop (text "disambig" <+> ppr dicts)
2107 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2108 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2109 warnDefault dicts default_ty `thenM_`
2112 bomb_out = addTopAmbigErrs dicts `thenM_`
2116 = do { mb_defaults <- getDefaultTys
2117 ; case mb_defaults of
2118 Just tys -> return tys
2119 Nothing -> -- No use-supplied default;
2120 -- use [Integer, Double]
2121 do { integer_ty <- tcMetaTy integerTyConName
2122 ; return [integer_ty, doubleTy] } }
2125 [Aside - why the defaulting mechanism is turned off when
2126 dealing with arguments and results to ccalls.
2128 When typechecking _ccall_s, TcExpr ensures that the external
2129 function is only passed arguments (and in the other direction,
2130 results) of a restricted set of 'native' types. This is
2131 implemented via the help of the pseudo-type classes,
2132 @CReturnable@ (CR) and @CCallable@ (CC.)
2134 The interaction between the defaulting mechanism for numeric
2135 values and CC & CR can be a bit puzzling to the user at times.
2144 What type has 'x' got here? That depends on the default list
2145 in operation, if it is equal to Haskell 98's default-default
2146 of (Integer, Double), 'x' has type Double, since Integer
2147 is not an instance of CR. If the default list is equal to
2148 Haskell 1.4's default-default of (Int, Double), 'x' has type
2151 To try to minimise the potential for surprises here, the
2152 defaulting mechanism is turned off in the presence of
2153 CCallable and CReturnable.
2158 %************************************************************************
2160 \subsection[simple]{@Simple@ versions}
2162 %************************************************************************
2164 Much simpler versions when there are no bindings to make!
2166 @tcSimplifyThetas@ simplifies class-type constraints formed by
2167 @deriving@ declarations and when specialising instances. We are
2168 only interested in the simplified bunch of class/type constraints.
2170 It simplifies to constraints of the form (C a b c) where
2171 a,b,c are type variables. This is required for the context of
2172 instance declarations.
2175 tcSimplifyDeriv :: [TyVar]
2176 -> ThetaType -- Wanted
2177 -> TcM ThetaType -- Needed
2179 tcSimplifyDeriv tyvars theta
2180 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2181 -- The main loop may do unification, and that may crash if
2182 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2183 -- ToDo: what if two of them do get unified?
2184 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2185 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2186 ASSERT( null frees ) -- reduceMe never returns Free
2188 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2190 tv_set = mkVarSet tvs
2192 (bad_insts, ok_insts) = partition is_bad_inst irreds
2194 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2195 in isEmptyVarSet (tyVarsOfPred pred)
2196 -- Things like (Eq T) are bad
2197 || (not undecidable_ok && not (isTyVarClassPred pred))
2198 -- The returned dictionaries should be of form (C a b)
2199 -- (where a, b are type variables).
2200 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
2201 -- but note that risks non-termination in the 'deriving' context-inference
2202 -- fixpoint loop. It is useful for situations like
2203 -- data Min h a = E | M a (h a)
2204 -- which gives the instance decl
2205 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
2207 simpl_theta = map dictPred ok_insts
2208 weird_preds = [pred | pred <- simpl_theta
2209 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2210 -- Check for a bizarre corner case, when the derived instance decl should
2211 -- have form instance C a b => D (T a) where ...
2212 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2213 -- of problems; in particular, it's hard to compare solutions for
2214 -- equality when finding the fixpoint. So I just rule it out for now.
2216 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2217 -- This reverse-mapping is a Royal Pain,
2218 -- but the result should mention TyVars not TcTyVars
2221 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2222 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2223 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2224 returnM (substTheta rev_env simpl_theta)
2226 doc = ptext SLIT("deriving classes for a data type")
2229 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2230 used with \tr{default} declarations. We are only interested in
2231 whether it worked or not.
2234 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2237 tcSimplifyDefault theta
2238 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2239 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2240 ASSERT( null frees ) -- try_me never returns Free
2241 addNoInstanceErrs Nothing [] irreds `thenM_`
2247 doc = ptext SLIT("default declaration")
2251 %************************************************************************
2253 \section{Errors and contexts}
2255 %************************************************************************
2257 ToDo: for these error messages, should we note the location as coming
2258 from the insts, or just whatever seems to be around in the monad just
2262 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2263 -> [Inst] -- The offending Insts
2265 -- Group together insts with the same origin
2266 -- We want to report them together in error messages
2268 groupErrs report_err []
2270 groupErrs report_err (inst:insts)
2271 = do_one (inst:friends) `thenM_`
2272 groupErrs report_err others
2275 -- (It may seem a bit crude to compare the error messages,
2276 -- but it makes sure that we combine just what the user sees,
2277 -- and it avoids need equality on InstLocs.)
2278 (friends, others) = partition is_friend insts
2279 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2280 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2281 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2282 -- Add location and context information derived from the Insts
2284 -- Add the "arising from..." part to a message about bunch of dicts
2285 addInstLoc :: [Inst] -> Message -> Message
2286 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2289 plural xs = char 's'
2291 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2292 addTopIPErrs bndrs []
2294 addTopIPErrs bndrs ips
2295 = addErrTcM (tidy_env, mk_msg tidy_ips)
2297 (tidy_env, tidy_ips) = tidyInsts ips
2298 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
2299 pprBinders bndrs <> colon],
2300 nest 2 (vcat (map ppr_ip ips)),
2302 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2304 strangeTopIPErrs :: [Inst] -> TcM ()
2305 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2306 = groupErrs report tidy_dicts
2308 (tidy_env, tidy_dicts) = tidyInsts dicts
2309 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2310 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2311 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2313 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2314 -- Just d => d describes the construct
2315 -> [Inst] -- What is given by the context or type sig
2316 -> [Inst] -- What is wanted
2318 addNoInstanceErrs mb_what givens []
2320 addNoInstanceErrs mb_what givens dicts
2321 = -- Some of the dicts are here because there is no instances
2322 -- and some because there are too many instances (overlap)
2323 getDOpts `thenM` \ dflags ->
2324 tcGetInstEnvs `thenM` \ inst_envs ->
2326 (tidy_env1, tidy_givens) = tidyInsts givens
2327 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2329 -- Run through the dicts, generating a message for each
2330 -- overlapping one, but simply accumulating all the
2331 -- no-instance ones so they can be reported as a group
2332 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2333 check_overlap (overlap_doc, no_inst_dicts) dict
2334 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2336 = case lookupInstEnv dflags inst_envs clas tys of
2337 -- The case of exactly one match and no unifiers means
2338 -- a successful lookup. That can't happen here, becuase
2339 -- dicts only end up here if they didn't match in Inst.lookupInst
2341 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2343 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2344 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2346 (clas,tys) = getDictClassTys dict
2349 -- Now generate a good message for the no-instance bunch
2350 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2352 no_inst_doc | null no_inst_dicts = empty
2353 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2354 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2355 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2356 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2357 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2359 -- And emit both the non-instance and overlap messages
2360 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2362 mk_overlap_msg dict (matches, unifiers)
2363 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2364 <+> pprPred (dictPred dict))),
2365 sep [ptext SLIT("Matching instances") <> colon,
2366 nest 2 (vcat [pprDFuns dfuns, pprDFuns unifiers])],
2367 ASSERT( not (null matches) )
2368 if not (isSingleton matches)
2369 then -- Two or more matches
2371 else -- One match, plus some unifiers
2372 ASSERT( not (null unifiers) )
2373 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2374 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2375 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2377 dfuns = [df | (_, (_,_,df)) <- matches]
2379 mk_probable_fix tidy_env dicts
2380 = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
2382 fixes = add_ors (fix1 ++ fix2)
2384 fix1 = case mb_what of
2385 Nothing -> [] -- Top level
2386 Just what -> -- Nested (type signatures, instance decls)
2387 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2388 ptext SLIT("to the") <+> what] ]
2390 fix2 | null instance_dicts = []
2391 | otherwise = [ ptext SLIT("add an instance declaration for")
2392 <+> pprDictsTheta instance_dicts ]
2393 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2394 -- Insts for which it is worth suggesting an adding an instance declaration
2395 -- Exclude implicit parameters, and tyvar dicts
2397 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2398 add_ors [] = ptext SLIT("[No suggested fixes]") -- Strange
2399 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2401 addTopAmbigErrs dicts
2402 -- Divide into groups that share a common set of ambiguous tyvars
2403 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2405 (tidy_env, tidy_dicts) = tidyInsts dicts
2407 tvs_of :: Inst -> [TcTyVar]
2408 tvs_of d = varSetElems (tyVarsOfInst d)
2409 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2411 report :: [(Inst,[TcTyVar])] -> TcM ()
2412 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2413 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2414 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2415 -- the location of the first one will do for the err message
2416 addErrTcM (tidy_env, msg $$ mono_msg)
2418 dicts = map fst pairs
2419 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2420 pprQuotedList tvs <+> in_msg,
2421 nest 2 (pprDictsInFull dicts)]
2422 in_msg = text "in the constraint" <> plural dicts <> colon
2425 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2426 -- There's an error with these Insts; if they have free type variables
2427 -- it's probably caused by the monomorphism restriction.
2428 -- Try to identify the offending variable
2429 -- ASSUMPTION: the Insts are fully zonked
2430 mkMonomorphismMsg tidy_env inst_tvs
2431 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2432 returnM (tidy_env, mk_msg docs)
2434 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2435 -- This happens in things like
2436 -- f x = show (read "foo")
2437 -- whre monomorphism doesn't play any role
2438 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2442 monomorphism_fix :: SDoc
2443 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2444 (ptext SLIT("give these definition(s) an explicit type signature")
2445 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2447 warnDefault dicts default_ty
2448 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2449 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2452 (_, tidy_dicts) = tidyInsts dicts
2453 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2454 quotes (ppr default_ty),
2455 pprDictsInFull tidy_dicts]
2457 -- Used for the ...Thetas variants; all top level
2459 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2460 ptext SLIT("type variables that are not data type parameters"),
2461 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2463 reduceDepthErr n stack
2464 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2465 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2466 nest 4 (pprStack stack)]
2468 pprStack stack = vcat (map pprInstInFull stack)