2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs,
13 tcSimplifySuperClasses,
14 tcSimplifyTop, tcSimplifyInteractive,
17 tcSimplifyDeriv, tcSimplifyDefault,
21 #include "HsVersions.h"
23 import {-# SOURCE #-} TcUnify( unifyTauTy )
25 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
26 import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
29 import Inst ( lookupInst, LookupInstResult(..),
30 tyVarsOfInst, fdPredsOfInsts, newDicts,
31 isDict, isClassDict, isLinearInst, linearInstType,
32 isStdClassTyVarDict, isMethodFor, isMethod,
33 instToId, tyVarsOfInsts, cloneDict,
34 ipNamesOfInsts, ipNamesOfInst, dictPred,
35 instBindingRequired, fdPredsOfInst,
36 newDictsAtLoc, tcInstClassOp,
37 getDictClassTys, isTyVarDict, instLoc,
38 zonkInst, tidyInsts, tidyMoreInsts,
39 Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
40 isInheritableInst, pprDFuns, pprDictsTheta
42 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
43 import InstEnv ( lookupInstEnv, classInstances )
44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType,
46 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
47 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
48 tyVarsOfPred, tcEqType, pprPred, mkPredTy )
49 import Id ( idType, mkUserLocal )
51 import Name ( Name, getOccName, getSrcLoc )
52 import NameSet ( NameSet, mkNameSet, elemNameSet )
53 import Class ( classBigSig, classKey )
54 import FunDeps ( oclose, grow, improve, pprEquationDoc )
55 import PrelInfo ( isNumericClass )
56 import PrelNames ( splitName, fstName, sndName, integerTyConName,
57 showClassKey, eqClassKey, ordClassKey )
58 import Type ( zipTopTvSubst, substTheta, substTy )
59 import TysWiredIn ( pairTyCon, doubleTy )
60 import ErrUtils ( Message )
61 import BasicTypes ( TopLevelFlag, isNotTopLevel )
63 import VarEnv ( TidyEnv )
67 import ListSetOps ( equivClasses )
68 import Util ( zipEqual, isSingleton )
69 import List ( partition )
70 import SrcLoc ( Located(..) )
75 %************************************************************************
79 %************************************************************************
81 --------------------------------------
82 Notes on functional dependencies (a bug)
83 --------------------------------------
85 | > class Foo a b | a->b
87 | > class Bar a b | a->b
91 | > instance Bar Obj Obj
93 | > instance (Bar a b) => Foo a b
95 | > foo:: (Foo a b) => a -> String
98 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
104 | Could not deduce (Bar a b) from the context (Foo a b)
105 | arising from use of `foo' at <interactive>:1
107 | Add (Bar a b) to the expected type of an expression
108 | In the first argument of `runFoo', namely `foo'
109 | In the definition of `it': it = runFoo foo
111 | Why all of the sudden does GHC need the constraint Bar a b? The
112 | function foo didn't ask for that...
114 The trouble is that to type (runFoo foo), GHC has to solve the problem:
116 Given constraint Foo a b
117 Solve constraint Foo a b'
119 Notice that b and b' aren't the same. To solve this, just do
120 improvement and then they are the same. But GHC currently does
125 That is usually fine, but it isn't here, because it sees that Foo a b is
126 not the same as Foo a b', and so instead applies the instance decl for
127 instance Bar a b => Foo a b. And that's where the Bar constraint comes
130 The Right Thing is to improve whenever the constraint set changes at
131 all. Not hard in principle, but it'll take a bit of fiddling to do.
135 --------------------------------------
136 Notes on quantification
137 --------------------------------------
139 Suppose we are about to do a generalisation step.
143 T the type of the RHS
144 C the constraints from that RHS
146 The game is to figure out
148 Q the set of type variables over which to quantify
149 Ct the constraints we will *not* quantify over
150 Cq the constraints we will quantify over
152 So we're going to infer the type
156 and float the constraints Ct further outwards.
158 Here are the things that *must* be true:
160 (A) Q intersect fv(G) = EMPTY limits how big Q can be
161 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
163 (A) says we can't quantify over a variable that's free in the
164 environment. (B) says we must quantify over all the truly free
165 variables in T, else we won't get a sufficiently general type. We do
166 not *need* to quantify over any variable that is fixed by the free
167 vars of the environment G.
169 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
171 Example: class H x y | x->y where ...
173 fv(G) = {a} C = {H a b, H c d}
176 (A) Q intersect {a} is empty
177 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
179 So Q can be {c,d}, {b,c,d}
181 Other things being equal, however, we'd like to quantify over as few
182 variables as possible: smaller types, fewer type applications, more
183 constraints can get into Ct instead of Cq.
186 -----------------------------------------
189 fv(T) the free type vars of T
191 oclose(vs,C) The result of extending the set of tyvars vs
192 using the functional dependencies from C
194 grow(vs,C) The result of extend the set of tyvars vs
195 using all conceivable links from C.
197 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
198 Then grow(vs,C) = {a,b,c}
200 Note that grow(vs,C) `superset` grow(vs,simplify(C))
201 That is, simplfication can only shrink the result of grow.
204 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
205 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
208 -----------------------------------------
212 Here's a good way to choose Q:
214 Q = grow( fv(T), C ) \ oclose( fv(G), C )
216 That is, quantify over all variable that that MIGHT be fixed by the
217 call site (which influences T), but which aren't DEFINITELY fixed by
218 G. This choice definitely quantifies over enough type variables,
219 albeit perhaps too many.
221 Why grow( fv(T), C ) rather than fv(T)? Consider
223 class H x y | x->y where ...
228 If we used fv(T) = {c} we'd get the type
230 forall c. H c d => c -> b
232 And then if the fn was called at several different c's, each of
233 which fixed d differently, we'd get a unification error, because
234 d isn't quantified. Solution: quantify d. So we must quantify
235 everything that might be influenced by c.
237 Why not oclose( fv(T), C )? Because we might not be able to see
238 all the functional dependencies yet:
240 class H x y | x->y where ...
241 instance H x y => Eq (T x y) where ...
246 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
247 apparent yet, and that's wrong. We must really quantify over d too.
250 There really isn't any point in quantifying over any more than
251 grow( fv(T), C ), because the call sites can't possibly influence
252 any other type variables.
256 --------------------------------------
258 --------------------------------------
260 It's very hard to be certain when a type is ambiguous. Consider
264 instance H x y => K (x,y)
266 Is this type ambiguous?
267 forall a b. (K (a,b), Eq b) => a -> a
269 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
270 now we see that a fixes b. So we can't tell about ambiguity for sure
271 without doing a full simplification. And even that isn't possible if
272 the context has some free vars that may get unified. Urgle!
274 Here's another example: is this ambiguous?
275 forall a b. Eq (T b) => a -> a
276 Not if there's an insance decl (with no context)
277 instance Eq (T b) where ...
279 You may say of this example that we should use the instance decl right
280 away, but you can't always do that:
282 class J a b where ...
283 instance J Int b where ...
285 f :: forall a b. J a b => a -> a
287 (Notice: no functional dependency in J's class decl.)
288 Here f's type is perfectly fine, provided f is only called at Int.
289 It's premature to complain when meeting f's signature, or even
290 when inferring a type for f.
294 However, we don't *need* to report ambiguity right away. It'll always
295 show up at the call site.... and eventually at main, which needs special
296 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
298 So here's the plan. We WARN about probable ambiguity if
300 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
302 (all tested before quantification).
303 That is, all the type variables in Cq must be fixed by the the variables
304 in the environment, or by the variables in the type.
306 Notice that we union before calling oclose. Here's an example:
308 class J a b c | a b -> c
312 forall b c. (J a b c) => b -> b
314 Only if we union {a} from G with {b} from T before using oclose,
315 do we see that c is fixed.
317 It's a bit vague exactly which C we should use for this oclose call. If we
318 don't fix enough variables we might complain when we shouldn't (see
319 the above nasty example). Nothing will be perfect. That's why we can
320 only issue a warning.
323 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
325 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
327 then c is a "bubble"; there's no way it can ever improve, and it's
328 certainly ambiguous. UNLESS it is a constant (sigh). And what about
333 instance H x y => K (x,y)
335 Is this type ambiguous?
336 forall a b. (K (a,b), Eq b) => a -> a
338 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
339 is a "bubble" that's a set of constraints
341 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
343 Hence another idea. To decide Q start with fv(T) and grow it
344 by transitive closure in Cq (no functional dependencies involved).
345 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
346 The definitely-ambiguous can then float out, and get smashed at top level
347 (which squashes out the constants, like Eq (T a) above)
350 --------------------------------------
351 Notes on principal types
352 --------------------------------------
357 f x = let g y = op (y::Int) in True
359 Here the principal type of f is (forall a. a->a)
360 but we'll produce the non-principal type
361 f :: forall a. C Int => a -> a
364 --------------------------------------
365 The need for forall's in constraints
366 --------------------------------------
368 [Exchange on Haskell Cafe 5/6 Dec 2000]
370 class C t where op :: t -> Bool
371 instance C [t] where op x = True
373 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
374 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
376 The definitions of p and q differ only in the order of the components in
377 the pair on their right-hand sides. And yet:
379 ghc and "Typing Haskell in Haskell" reject p, but accept q;
380 Hugs rejects q, but accepts p;
381 hbc rejects both p and q;
382 nhc98 ... (Malcolm, can you fill in the blank for us!).
384 The type signature for f forces context reduction to take place, and
385 the results of this depend on whether or not the type of y is known,
386 which in turn depends on which component of the pair the type checker
389 Solution: if y::m a, float out the constraints
390 Monad m, forall c. C (m c)
391 When m is later unified with [], we can solve both constraints.
394 --------------------------------------
395 Notes on implicit parameters
396 --------------------------------------
398 Question 1: can we "inherit" implicit parameters
399 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
404 where f is *not* a top-level binding.
405 From the RHS of f we'll get the constraint (?y::Int).
406 There are two types we might infer for f:
410 (so we get ?y from the context of f's definition), or
412 f :: (?y::Int) => Int -> Int
414 At first you might think the first was better, becuase then
415 ?y behaves like a free variable of the definition, rather than
416 having to be passed at each call site. But of course, the WHOLE
417 IDEA is that ?y should be passed at each call site (that's what
418 dynamic binding means) so we'd better infer the second.
420 BOTTOM LINE: when *inferring types* you *must* quantify
421 over implicit parameters. See the predicate isFreeWhenInferring.
424 Question 2: type signatures
425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
426 BUT WATCH OUT: When you supply a type signature, we can't force you
427 to quantify over implicit parameters. For example:
431 This is perfectly reasonable. We do not want to insist on
433 (?x + 1) :: (?x::Int => Int)
435 That would be silly. Here, the definition site *is* the occurrence site,
436 so the above strictures don't apply. Hence the difference between
437 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
438 and tcSimplifyCheckBind (which does not).
440 What about when you supply a type signature for a binding?
441 Is it legal to give the following explicit, user type
442 signature to f, thus:
447 At first sight this seems reasonable, but it has the nasty property
448 that adding a type signature changes the dynamic semantics.
451 (let f x = (x::Int) + ?y
452 in (f 3, f 3 with ?y=5)) with ?y = 6
458 in (f 3, f 3 with ?y=5)) with ?y = 6
462 Indeed, simply inlining f (at the Haskell source level) would change the
465 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
466 semantics for a Haskell program without knowing its typing, so if you
467 change the typing you may change the semantics.
469 To make things consistent in all cases where we are *checking* against
470 a supplied signature (as opposed to inferring a type), we adopt the
473 a signature does not need to quantify over implicit params.
475 [This represents a (rather marginal) change of policy since GHC 5.02,
476 which *required* an explicit signature to quantify over all implicit
477 params for the reasons mentioned above.]
479 But that raises a new question. Consider
481 Given (signature) ?x::Int
482 Wanted (inferred) ?x::Int, ?y::Bool
484 Clearly we want to discharge the ?x and float the ?y out. But
485 what is the criterion that distinguishes them? Clearly it isn't
486 what free type variables they have. The Right Thing seems to be
487 to float a constraint that
488 neither mentions any of the quantified type variables
489 nor any of the quantified implicit parameters
491 See the predicate isFreeWhenChecking.
494 Question 3: monomorphism
495 ~~~~~~~~~~~~~~~~~~~~~~~~
496 There's a nasty corner case when the monomorphism restriction bites:
500 The argument above suggests that we *must* generalise
501 over the ?y parameter, to get
502 z :: (?y::Int) => Int,
503 but the monomorphism restriction says that we *must not*, giving
505 Why does the momomorphism restriction say this? Because if you have
507 let z = x + ?y in z+z
509 you might not expect the addition to be done twice --- but it will if
510 we follow the argument of Question 2 and generalise over ?y.
513 Question 4: top level
514 ~~~~~~~~~~~~~~~~~~~~~
515 At the top level, monomorhism makes no sense at all.
518 main = let ?x = 5 in print foo
522 woggle :: (?x :: Int) => Int -> Int
525 We definitely don't want (foo :: Int) with a top-level implicit parameter
526 (?x::Int) becuase there is no way to bind it.
531 (A) Always generalise over implicit parameters
532 Bindings that fall under the monomorphism restriction can't
536 * Inlining remains valid
537 * No unexpected loss of sharing
538 * But simple bindings like
540 will be rejected, unless you add an explicit type signature
541 (to avoid the monomorphism restriction)
542 z :: (?y::Int) => Int
544 This seems unacceptable
546 (B) Monomorphism restriction "wins"
547 Bindings that fall under the monomorphism restriction can't
549 Always generalise over implicit parameters *except* for bindings
550 that fall under the monomorphism restriction
553 * Inlining isn't valid in general
554 * No unexpected loss of sharing
555 * Simple bindings like
557 accepted (get value of ?y from binding site)
559 (C) Always generalise over implicit parameters
560 Bindings that fall under the monomorphism restriction can't
561 be generalised, EXCEPT for implicit parameters
563 * Inlining remains valid
564 * Unexpected loss of sharing (from the extra generalisation)
565 * Simple bindings like
567 accepted (get value of ?y from occurrence sites)
572 None of these choices seems very satisfactory. But at least we should
573 decide which we want to do.
575 It's really not clear what is the Right Thing To Do. If you see
579 would you expect the value of ?y to be got from the *occurrence sites*
580 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
581 case of function definitions, the answer is clearly the former, but
582 less so in the case of non-fucntion definitions. On the other hand,
583 if we say that we get the value of ?y from the definition site of 'z',
584 then inlining 'z' might change the semantics of the program.
586 Choice (C) really says "the monomorphism restriction doesn't apply
587 to implicit parameters". Which is fine, but remember that every
588 innocent binding 'x = ...' that mentions an implicit parameter in
589 the RHS becomes a *function* of that parameter, called at each
590 use of 'x'. Now, the chances are that there are no intervening 'with'
591 clauses that bind ?y, so a decent compiler should common up all
592 those function calls. So I think I strongly favour (C). Indeed,
593 one could make a similar argument for abolishing the monomorphism
594 restriction altogether.
596 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
600 %************************************************************************
602 \subsection{tcSimplifyInfer}
604 %************************************************************************
606 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
608 1. Compute Q = grow( fvs(T), C )
610 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
611 predicates will end up in Ct; we deal with them at the top level
613 3. Try improvement, using functional dependencies
615 4. If Step 3 did any unification, repeat from step 1
616 (Unification can change the result of 'grow'.)
618 Note: we don't reduce dictionaries in step 2. For example, if we have
619 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
620 after step 2. However note that we may therefore quantify over more
621 type variables than we absolutely have to.
623 For the guts, we need a loop, that alternates context reduction and
624 improvement with unification. E.g. Suppose we have
626 class C x y | x->y where ...
628 and tcSimplify is called with:
630 Then improvement unifies a with b, giving
633 If we need to unify anything, we rattle round the whole thing all over
640 -> TcTyVarSet -- fv(T); type vars
642 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
643 TcDictBinds, -- Bindings
644 [TcId]) -- Dict Ids that must be bound here (zonked)
645 -- Any free (escaping) Insts are tossed into the environment
650 tcSimplifyInfer doc tau_tvs wanted_lie
651 = inferLoop doc (varSetElems tau_tvs)
652 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
654 extendLIEs frees `thenM_`
655 returnM (qtvs, binds, map instToId irreds)
657 inferLoop doc tau_tvs wanteds
659 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
660 mappM zonkInst wanteds `thenM` \ wanteds' ->
661 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
663 preds = fdPredsOfInsts wanteds'
664 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
667 | isFreeWhenInferring qtvs inst = Free
668 | isClassDict inst = DontReduceUnlessConstant -- Dicts
669 | otherwise = ReduceMe NoSCs -- Lits and Methods
671 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
672 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
674 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
677 if no_improvement then
678 returnM (varSetElems qtvs, frees, binds, irreds)
680 -- If improvement did some unification, we go round again. There
681 -- are two subtleties:
682 -- a) We start again with irreds, not wanteds
683 -- Using an instance decl might have introduced a fresh type variable
684 -- which might have been unified, so we'd get an infinite loop
685 -- if we started again with wanteds! See example [LOOP]
687 -- b) It's also essential to re-process frees, because unification
688 -- might mean that a type variable that looked free isn't now.
690 -- Hence the (irreds ++ frees)
692 -- However, NOTICE that when we are done, we might have some bindings, but
693 -- the final qtvs might be empty. See [NO TYVARS] below.
695 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
696 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
701 class If b t e r | b t e -> r
704 class Lte a b c | a b -> c where lte :: a -> b -> c
706 instance (Lte a b l,If l b a c) => Max a b c
708 Wanted: Max Z (S x) y
710 Then we'll reduce using the Max instance to:
711 (Lte Z (S x) l, If l (S x) Z y)
712 and improve by binding l->T, after which we can do some reduction
713 on both the Lte and If constraints. What we *can't* do is start again
714 with (Max Z (S x) y)!
718 class Y a b | a -> b where
721 instance Y [[a]] a where
724 k :: X a -> X a -> X a
726 g :: Num a => [X a] -> [X a]
729 h ys = ys ++ map (k (y [[0]])) xs
731 The excitement comes when simplifying the bindings for h. Initially
732 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
733 From this we get t1:=:t2, but also various bindings. We can't forget
734 the bindings (because of [LOOP]), but in fact t1 is what g is
737 The net effect of [NO TYVARS]
740 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
741 isFreeWhenInferring qtvs inst
742 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
743 && isInheritableInst inst -- And no implicit parameter involved
744 -- (see "Notes on implicit parameters")
746 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
747 -> NameSet -- Quantified implicit parameters
749 isFreeWhenChecking qtvs ips inst
750 = isFreeWrtTyVars qtvs inst
751 && isFreeWrtIPs ips inst
753 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
754 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
758 %************************************************************************
760 \subsection{tcSimplifyCheck}
762 %************************************************************************
764 @tcSimplifyCheck@ is used when we know exactly the set of variables
765 we are going to quantify over. For example, a class or instance declaration.
770 -> [TcTyVar] -- Quantify over these
773 -> TcM TcDictBinds -- Bindings
775 -- tcSimplifyCheck is used when checking expression type signatures,
776 -- class decls, instance decls etc.
778 -- NB: tcSimplifyCheck does not consult the
779 -- global type variables in the environment; so you don't
780 -- need to worry about setting them before calling tcSimplifyCheck
781 tcSimplifyCheck doc qtvs givens wanted_lie
782 = ASSERT( all isSkolemTyVar qtvs )
783 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
787 -- get_qtvs = zonkTcTyVarsAndFV qtvs
788 get_qtvs = return (mkVarSet qtvs) -- All skolems
791 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
792 -- against, but we don't know the type variables over which we are going to quantify.
793 -- This happens when we have a type signature for a mutually recursive group
796 -> TcTyVarSet -- fv(T)
799 -> TcM ([TcTyVar], -- Variables over which to quantify
800 TcDictBinds) -- Bindings
802 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
803 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
805 ; return (qtvs', binds) }
807 -- Figure out which type variables to quantify over
808 -- You might think it should just be the signature tyvars,
809 -- but in bizarre cases you can get extra ones
810 -- f :: forall a. Num a => a -> a
811 -- f x = fst (g (x, head [])) + 1
813 -- Here we infer g :: forall a b. a -> b -> (b,a)
814 -- We don't want g to be monomorphic in b just because
815 -- f isn't quantified over b.
816 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
818 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
819 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
821 qtvs = all_tvs' `minusVarSet` gbl_tvs
822 -- We could close gbl_tvs, but its not necessary for
823 -- soundness, and it'll only affect which tyvars, not which
824 -- dictionaries, we quantify over
829 Here is the workhorse function for all three wrappers.
832 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
833 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
835 -- Complain about any irreducible ones
836 ; if not (null irreds)
837 then do { givens' <- mappM zonkInst given_dicts_and_ips
838 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
841 ; returnM (qtvs, frees, binds) }
843 given_dicts_and_ips = filter (not . isMethod) givens
844 -- For error reporting, filter out methods, which are
845 -- only added to the given set as an optimisation
847 ip_set = mkNameSet (ipNamesOfInsts givens)
849 check_loop givens wanteds
851 mappM zonkInst givens `thenM` \ givens' ->
852 mappM zonkInst wanteds `thenM` \ wanteds' ->
853 get_qtvs `thenM` \ qtvs' ->
857 -- When checking against a given signature we always reduce
858 -- until we find a match against something given, or can't reduce
859 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
860 | otherwise = ReduceMe want_scs
862 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
865 if no_improvement then
866 returnM (varSetElems qtvs', frees, binds, irreds)
868 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
869 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
873 %************************************************************************
875 tcSimplifySuperClasses
877 %************************************************************************
879 Note [SUPERCLASS-LOOP 1]
880 ~~~~~~~~~~~~~~~~~~~~~~~~
881 We have to be very, very careful when generating superclasses, lest we
882 accidentally build a loop. Here's an example:
886 class S a => C a where { opc :: a -> a }
887 class S b => D b where { opd :: b -> b }
895 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
896 Simplifying, we may well get:
897 $dfCInt = :C ds1 (opd dd)
900 Notice that we spot that we can extract ds1 from dd.
902 Alas! Alack! We can do the same for (instance D Int):
904 $dfDInt = :D ds2 (opc dc)
908 And now we've defined the superclass in terms of itself.
910 Solution: never generate a superclass selectors at all when
911 satisfying the superclass context of an instance declaration.
913 Two more nasty cases are in
918 tcSimplifySuperClasses qtvs givens sc_wanteds
919 = ASSERT( all isSkolemTyVar qtvs )
920 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
921 ; binds2 <- tc_simplify_top doc False NoSCs frees
922 ; return (binds1 `unionBags` binds2) }
924 get_qtvs = return (mkVarSet qtvs)
925 doc = ptext SLIT("instance declaration superclass context")
929 %************************************************************************
931 \subsection{tcSimplifyRestricted}
933 %************************************************************************
935 tcSimplifyRestricted infers which type variables to quantify for a
936 group of restricted bindings. This isn't trivial.
939 We want to quantify over a to get id :: forall a. a->a
942 We do not want to quantify over a, because there's an Eq a
943 constraint, so we get eq :: a->a->Bool (notice no forall)
946 RHS has type 'tau', whose free tyvars are tau_tvs
947 RHS has constraints 'wanteds'
950 Quantify over (tau_tvs \ ftvs(wanteds))
951 This is bad. The constraints may contain (Monad (ST s))
952 where we have instance Monad (ST s) where...
953 so there's no need to be monomorphic in s!
955 Also the constraint might be a method constraint,
956 whose type mentions a perfectly innocent tyvar:
957 op :: Num a => a -> b -> a
958 Here, b is unconstrained. A good example would be
960 We want to infer the polymorphic type
961 foo :: forall b. b -> b
964 Plan B (cunning, used for a long time up to and including GHC 6.2)
965 Step 1: Simplify the constraints as much as possible (to deal
966 with Plan A's problem). Then set
967 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
969 Step 2: Now simplify again, treating the constraint as 'free' if
970 it does not mention qtvs, and trying to reduce it otherwise.
971 The reasons for this is to maximise sharing.
973 This fails for a very subtle reason. Suppose that in the Step 2
974 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
975 In the Step 1 this constraint might have been simplified, perhaps to
976 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
977 This won't happen in Step 2... but that in turn might prevent some other
978 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
979 and that in turn breaks the invariant that no constraints are quantified over.
981 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
986 Step 1: Simplify the constraints as much as possible (to deal
987 with Plan A's problem). Then set
988 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
989 Return the bindings from Step 1.
992 A note about Plan C (arising from "bug" reported by George Russel March 2004)
995 instance (HasBinary ty IO) => HasCodedValue ty
997 foo :: HasCodedValue a => String -> IO a
999 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1000 doDecodeIO codedValue view
1001 = let { act = foo "foo" } in act
1003 You might think this should work becuase the call to foo gives rise to a constraint
1004 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1005 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1006 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1008 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1012 Plan D (a variant of plan B)
1013 Step 1: Simplify the constraints as much as possible (to deal
1014 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1015 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1017 Step 2: Now simplify again, treating the constraint as 'free' if
1018 it does not mention qtvs, and trying to reduce it otherwise.
1020 The point here is that it's generally OK to have too few qtvs; that is,
1021 to make the thing more monomorphic than it could be. We don't want to
1022 do that in the common cases, but in wierd cases it's ok: the programmer
1023 can always add a signature.
1025 Too few qtvs => too many wanteds, which is what happens if you do less
1030 tcSimplifyRestricted -- Used for restricted binding groups
1031 -- i.e. ones subject to the monomorphism restriction
1034 -> [Name] -- Things bound in this group
1035 -> TcTyVarSet -- Free in the type of the RHSs
1036 -> [Inst] -- Free in the RHSs
1037 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1038 TcDictBinds) -- Bindings
1039 -- tcSimpifyRestricted returns no constraints to
1040 -- quantify over; by definition there are none.
1041 -- They are all thrown back in the LIE
1043 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1044 -- Zonk everything in sight
1045 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1046 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1047 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1049 -- 'reduceMe': Reduce as far as we can. Don't stop at
1050 -- dicts; the idea is to get rid of as many type
1051 -- variables as possible, and we don't want to stop
1052 -- at (say) Monad (ST s), because that reduces
1053 -- immediately, with no constraint on s.
1055 -- BUT do no improvement! See Plan D above
1056 reduceContextWithoutImprovement
1057 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1059 -- Next, figure out the tyvars we will quantify over
1061 constrained_tvs = tyVarsOfInsts constrained_dicts
1062 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1063 `minusVarSet` constrained_tvs
1065 traceTc (text "tcSimplifyRestricted" <+> vcat [
1066 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1068 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1070 -- The first step may have squashed more methods than
1071 -- necessary, so try again, this time more gently, knowing the exact
1072 -- set of type variables to quantify over.
1074 -- We quantify only over constraints that are captured by qtvs;
1075 -- these will just be a subset of non-dicts. This in contrast
1076 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1077 -- all *non-inheritable* constraints too. This implements choice
1078 -- (B) under "implicit parameter and monomorphism" above.
1080 -- Remember that we may need to do *some* simplification, to
1081 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1082 -- just to float all constraints
1084 -- At top level, we *do* squash methods becuase we want to
1085 -- expose implicit parameters to the test that follows
1087 is_nested_group = isNotTopLevel top_lvl
1088 try_me inst | isFreeWrtTyVars qtvs inst,
1089 (is_nested_group || isDict inst) = Free
1090 | otherwise = ReduceMe AddSCs
1092 reduceContextWithoutImprovement
1093 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1094 ASSERT( null irreds )
1096 -- See "Notes on implicit parameters, Question 4: top level"
1097 if is_nested_group then
1098 extendLIEs frees `thenM_`
1099 returnM (varSetElems qtvs, binds)
1102 (non_ips, bad_ips) = partition isClassDict frees
1104 addTopIPErrs bndrs bad_ips `thenM_`
1105 extendLIEs non_ips `thenM_`
1106 returnM (varSetElems qtvs, binds)
1110 %************************************************************************
1112 \subsection{tcSimplifyToDicts}
1114 %************************************************************************
1116 On the LHS of transformation rules we only simplify methods and constants,
1117 getting dictionaries. We want to keep all of them unsimplified, to serve
1118 as the available stuff for the RHS of the rule.
1120 The same thing is used for specialise pragmas. Consider
1122 f :: Num a => a -> a
1123 {-# SPECIALISE f :: Int -> Int #-}
1126 The type checker generates a binding like:
1128 f_spec = (f :: Int -> Int)
1130 and we want to end up with
1132 f_spec = _inline_me_ (f Int dNumInt)
1134 But that means that we must simplify the Method for f to (f Int dNumInt)!
1135 So tcSimplifyToDicts squeezes out all Methods.
1137 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
1139 fromIntegral :: (Integral a, Num b) => a -> b
1140 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1142 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
1145 forall dIntegralInt.
1146 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1148 because the scsel will mess up RULE matching. Instead we want
1150 forall dIntegralInt, dNumInt.
1151 fromIntegral Int Int dIntegralInt dNumInt = id Int
1156 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
1157 tcSimplifyToDicts wanteds
1158 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1159 -- Since try_me doesn't look at types, we don't need to
1160 -- do any zonking, so it's safe to call reduceContext directly
1161 ASSERT( null frees )
1162 extendLIEs irreds `thenM_`
1166 doc = text "tcSimplifyToDicts"
1168 -- Reduce methods and lits only; stop as soon as we get a dictionary
1169 try_me inst | isDict inst = KeepDictWithoutSCs -- See notes above re "WithoutSCs"
1170 | otherwise = ReduceMe NoSCs
1175 tcSimplifyBracket is used when simplifying the constraints arising from
1176 a Template Haskell bracket [| ... |]. We want to check that there aren't
1177 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1178 Show instance), but we aren't otherwise interested in the results.
1179 Nor do we care about ambiguous dictionaries etc. We will type check
1180 this bracket again at its usage site.
1183 tcSimplifyBracket :: [Inst] -> TcM ()
1184 tcSimplifyBracket wanteds
1185 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1188 doc = text "tcSimplifyBracket"
1192 %************************************************************************
1194 \subsection{Filtering at a dynamic binding}
1196 %************************************************************************
1201 we must discharge all the ?x constraints from B. We also do an improvement
1202 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1204 Actually, the constraints from B might improve the types in ?x. For example
1206 f :: (?x::Int) => Char -> Char
1209 then the constraint (?x::Int) arising from the call to f will
1210 force the binding for ?x to be of type Int.
1213 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1216 tcSimplifyIPs given_ips wanteds
1217 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1218 extendLIEs frees `thenM_`
1221 doc = text "tcSimplifyIPs" <+> ppr given_ips
1222 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1224 -- Simplify any methods that mention the implicit parameter
1225 try_me inst | isFreeWrtIPs ip_set inst = Free
1226 | otherwise = ReduceMe NoSCs
1228 simpl_loop givens wanteds
1229 = mappM zonkInst givens `thenM` \ givens' ->
1230 mappM zonkInst wanteds `thenM` \ wanteds' ->
1232 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1234 if no_improvement then
1235 ASSERT( null irreds )
1236 returnM (frees, binds)
1238 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1239 returnM (frees1, binds `unionBags` binds1)
1243 %************************************************************************
1245 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1247 %************************************************************************
1249 When doing a binding group, we may have @Insts@ of local functions.
1250 For example, we might have...
1252 let f x = x + 1 -- orig local function (overloaded)
1253 f.1 = f Int -- two instances of f
1258 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1259 where @f@ is in scope; those @Insts@ must certainly not be passed
1260 upwards towards the top-level. If the @Insts@ were binding-ified up
1261 there, they would have unresolvable references to @f@.
1263 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1264 For each method @Inst@ in the @init_lie@ that mentions one of the
1265 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1266 @LIE@), as well as the @HsBinds@ generated.
1269 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1270 -- Simlifies only MethodInsts, and generate only bindings of form
1272 -- We're careful not to even generate bindings of the form
1274 -- You'd think that'd be fine, but it interacts with what is
1275 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1277 bindInstsOfLocalFuns wanteds local_ids
1278 | null overloaded_ids
1280 = extendLIEs wanteds `thenM_`
1281 returnM emptyLHsBinds
1284 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1285 ASSERT( null irreds )
1286 extendLIEs not_for_me `thenM_`
1287 extendLIEs frees `thenM_`
1290 doc = text "bindInsts" <+> ppr local_ids
1291 overloaded_ids = filter is_overloaded local_ids
1292 is_overloaded id = isOverloadedTy (idType id)
1293 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1295 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1296 -- so it's worth building a set, so that
1297 -- lookup (in isMethodFor) is faster
1298 try_me inst | isMethod inst = ReduceMe NoSCs
1303 %************************************************************************
1305 \subsection{Data types for the reduction mechanism}
1307 %************************************************************************
1309 The main control over context reduction is here
1313 = ReduceMe WantSCs -- Try to reduce this
1314 -- If there's no instance, behave exactly like
1315 -- DontReduce: add the inst to
1316 -- the irreductible ones, but don't
1317 -- produce an error message of any kind.
1318 -- It might be quite legitimate such as (Eq a)!
1320 | KeepDictWithoutSCs -- Return as irreducible; don't add its superclasses
1321 -- Rather specialised: see notes with tcSimplifyToDicts
1323 | DontReduceUnlessConstant -- Return as irreducible unless it can
1324 -- be reduced to a constant in one step
1326 | Free -- Return as free
1328 reduceMe :: Inst -> WhatToDo
1329 reduceMe inst = ReduceMe AddSCs
1331 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1332 -- of a predicate when adding it to the avails
1338 type Avails = FiniteMap Inst Avail
1339 emptyAvails = emptyFM
1342 = IsFree -- Used for free Insts
1343 | Irred -- Used for irreducible dictionaries,
1344 -- which are going to be lambda bound
1346 | Given TcId -- Used for dictionaries for which we have a binding
1347 -- e.g. those "given" in a signature
1348 Bool -- True <=> actually consumed (splittable IPs only)
1350 | NoRhs -- Used for Insts like (CCallable f)
1351 -- where no witness is required.
1354 | Rhs -- Used when there is a RHS
1355 (LHsExpr TcId) -- The RHS
1356 [Inst] -- Insts free in the RHS; we need these too
1358 | Linear -- Splittable Insts only.
1359 Int -- The Int is always 2 or more; indicates how
1360 -- many copies are required
1361 Inst -- The splitter
1362 Avail -- Where the "master copy" is
1364 | LinRhss -- Splittable Insts only; this is used only internally
1365 -- by extractResults, where a Linear
1366 -- is turned into an LinRhss
1367 [LHsExpr TcId] -- A supply of suitable RHSs
1369 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1370 | (inst,avail) <- fmToList avails ]
1372 instance Outputable Avail where
1375 pprAvail NoRhs = text "<no rhs>"
1376 pprAvail IsFree = text "Free"
1377 pprAvail Irred = text "Irred"
1378 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1379 if b then text "(used)" else empty
1380 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1381 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1382 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1385 Extracting the bindings from a bunch of Avails.
1386 The bindings do *not* come back sorted in dependency order.
1387 We assume that they'll be wrapped in a big Rec, so that the
1388 dependency analyser can sort them out later
1392 extractResults :: Avails
1394 -> TcM (TcDictBinds, -- Bindings
1395 [Inst], -- Irreducible ones
1396 [Inst]) -- Free ones
1398 extractResults avails wanteds
1399 = go avails emptyBag [] [] wanteds
1401 go avails binds irreds frees []
1402 = returnM (binds, irreds, frees)
1404 go avails binds irreds frees (w:ws)
1405 = case lookupFM avails w of
1406 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1407 go avails binds irreds frees ws
1409 Just NoRhs -> go avails binds irreds frees ws
1410 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1411 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1413 Just (Given id _) -> go avails new_binds irreds frees ws
1415 new_binds | id == instToId w = binds
1416 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1417 -- The sought Id can be one of the givens, via a superclass chain
1418 -- and then we definitely don't want to generate an x=x binding!
1420 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1422 new_binds = addBind binds w rhs
1424 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1425 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1426 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1427 go (addToFM avails w (LinRhss rhss))
1428 (binds `unionBags` binds')
1429 irreds' frees' (split_inst : w : ws)
1431 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1432 -> go new_avails new_binds irreds frees ws
1434 new_binds = addBind binds w rhs
1435 new_avails = addToFM avails w (LinRhss rhss)
1437 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1438 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1439 returnM (w':irreds, frees, instToId w')
1440 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1441 returnM (irreds, w':frees, instToId w')
1444 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1445 | otherwise = addToFM avails w NoRhs
1446 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1447 -- than Given, else we end up with bogus bindings.
1449 add_free avails w | isMethod w = avails
1450 | otherwise = add_given avails w
1452 -- Do *not* replace Free by Given if it's a method.
1453 -- The following situation shows why this is bad:
1454 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1455 -- From an application (truncate f i) we get
1456 -- t1 = truncate at f
1458 -- If we have also have a second occurrence of truncate, we get
1459 -- t3 = truncate at f
1461 -- When simplifying with i,f free, we might still notice that
1462 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1463 -- will continue to float out!
1464 -- (split n i a) returns: n rhss
1465 -- auxiliary bindings
1466 -- 1 or 0 insts to add to irreds
1469 split :: Int -> TcId -> TcId -> Inst
1470 -> TcM (TcDictBinds, [LHsExpr TcId])
1471 -- (split n split_id root_id wanted) returns
1472 -- * a list of 'n' expressions, all of which witness 'avail'
1473 -- * a bunch of auxiliary bindings to support these expressions
1474 -- * one or zero insts needed to witness the whole lot
1475 -- (maybe be zero if the initial Inst is a Given)
1477 -- NB: 'wanted' is just a template
1479 split n split_id root_id wanted
1482 ty = linearInstType wanted
1483 pair_ty = mkTyConApp pairTyCon [ty,ty]
1484 id = instToId wanted
1487 span = instSpan wanted
1489 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1491 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1492 expand n rhss `thenM` \ (binds2, rhss') ->
1493 returnM (binds1 `unionBags` binds2, rhss')
1496 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1497 -- e.g. expand 3 [rhs1, rhs2]
1498 -- = ( { x = split rhs1 },
1499 -- [fst x, snd x, rhs2] )
1501 | n `rem` 2 == 0 = go rhss -- n is even
1502 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1503 returnM (binds', head rhss : rhss')
1505 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1506 returnM (listToBag binds', concat rhss')
1508 do_one rhs = newUnique `thenM` \ uniq ->
1509 tcLookupId fstName `thenM` \ fst_id ->
1510 tcLookupId sndName `thenM` \ snd_id ->
1512 x = mkUserLocal occ uniq pair_ty loc
1514 returnM (L span (VarBind x (mk_app span split_id rhs)),
1515 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1517 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1519 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1521 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1522 (VarBind (instToId inst) rhs))
1523 instSpan wanted = instLocSrcSpan (instLoc wanted)
1527 %************************************************************************
1529 \subsection[reduce]{@reduce@}
1531 %************************************************************************
1533 When the "what to do" predicate doesn't depend on the quantified type variables,
1534 matters are easier. We don't need to do any zonking, unless the improvement step
1535 does something, in which case we zonk before iterating.
1537 The "given" set is always empty.
1540 simpleReduceLoop :: SDoc
1541 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1543 -> TcM ([Inst], -- Free
1545 [Inst]) -- Irreducible
1547 simpleReduceLoop doc try_me wanteds
1548 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1549 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1550 if no_improvement then
1551 returnM (frees, binds, irreds)
1553 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1554 returnM (frees1, binds `unionBags` binds1, irreds1)
1560 reduceContext :: SDoc
1561 -> (Inst -> WhatToDo)
1564 -> TcM (Bool, -- True <=> improve step did no unification
1566 TcDictBinds, -- Dictionary bindings
1567 [Inst]) -- Irreducible
1569 reduceContext doc try_me givens wanteds
1571 traceTc (text "reduceContext" <+> (vcat [
1572 text "----------------------",
1574 text "given" <+> ppr givens,
1575 text "wanted" <+> ppr wanteds,
1576 text "----------------------"
1579 -- Build the Avail mapping from "givens"
1580 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1583 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1585 -- Do improvement, using everything in avails
1586 -- In particular, avails includes all superclasses of everything
1587 tcImprove avails `thenM` \ no_improvement ->
1589 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1591 traceTc (text "reduceContext end" <+> (vcat [
1592 text "----------------------",
1594 text "given" <+> ppr givens,
1595 text "wanted" <+> ppr wanteds,
1597 text "avails" <+> pprAvails avails,
1598 text "frees" <+> ppr frees,
1599 text "no_improvement =" <+> ppr no_improvement,
1600 text "----------------------"
1603 returnM (no_improvement, frees, binds, irreds)
1605 -- reduceContextWithoutImprovement differs from reduceContext
1606 -- (a) no improvement
1607 -- (b) 'givens' is assumed empty
1608 reduceContextWithoutImprovement doc try_me wanteds
1610 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1611 text "----------------------",
1613 text "wanted" <+> ppr wanteds,
1614 text "----------------------"
1618 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1619 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1621 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1622 text "----------------------",
1624 text "wanted" <+> ppr wanteds,
1626 text "avails" <+> pprAvails avails,
1627 text "frees" <+> ppr frees,
1628 text "----------------------"
1631 returnM (frees, binds, irreds)
1633 tcImprove :: Avails -> TcM Bool -- False <=> no change
1634 -- Perform improvement using all the predicates in Avails
1636 = tcGetInstEnvs `thenM` \ inst_envs ->
1638 preds = [ (pred, pp_loc)
1639 | (inst, avail) <- fmToList avails,
1640 pred <- get_preds inst avail,
1641 let pp_loc = pprInstLoc (instLoc inst)
1643 -- Avails has all the superclasses etc (good)
1644 -- It also has all the intermediates of the deduction (good)
1645 -- It does not have duplicates (good)
1646 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1647 -- so that improve will see them separate
1649 -- For free Methods, we want to take predicates from their context,
1650 -- but for Methods that have been squished their context will already
1651 -- be in Avails, and we don't want duplicates. Hence this rather
1652 -- horrid get_preds function
1653 get_preds inst IsFree = fdPredsOfInst inst
1654 get_preds inst other | isDict inst = [dictPred inst]
1657 eqns = improve get_insts preds
1658 get_insts clas = classInstances inst_envs clas
1663 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1664 mappM_ unify eqns `thenM_`
1667 unify ((qtvs, pairs), doc)
1669 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1670 mapM_ (unif_pr tenv) pairs
1671 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1674 The main context-reduction function is @reduce@. Here's its game plan.
1677 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1678 -- along with its depth
1679 -> (Inst -> WhatToDo)
1686 try_me: given an inst, this function returns
1688 DontReduce return this in "irreds"
1689 Free return this in "frees"
1691 wanteds: The list of insts to reduce
1692 state: An accumulating parameter of type Avails
1693 that contains the state of the algorithm
1695 It returns a Avails.
1697 The (n,stack) pair is just used for error reporting.
1698 n is always the depth of the stack.
1699 The stack is the stack of Insts being reduced: to produce X
1700 I had to produce Y, to produce Y I had to produce Z, and so on.
1703 reduceList (n,stack) try_me wanteds state
1704 | n > opt_MaxContextReductionDepth
1705 = failWithTc (reduceDepthErr n stack)
1711 pprTrace "Interesting! Context reduction stack deeper than 8:"
1712 (nest 2 (pprStack stack))
1717 go [] state = returnM state
1718 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1721 -- Base case: we're done!
1722 reduce stack try_me wanted avails
1723 -- It's the same as an existing inst, or a superclass thereof
1724 | Just avail <- isAvailable avails wanted
1725 = if isLinearInst wanted then
1726 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1727 reduceList stack try_me wanteds' avails'
1729 returnM avails -- No op for non-linear things
1732 = case try_me wanted of {
1734 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1736 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1737 -- First, see if the inst can be reduced to a constant in one step
1738 try_simple (addIrred AddSCs) -- Assume want superclasses
1740 ; Free -> -- It's free so just chuck it upstairs
1741 -- First, see if the inst can be reduced to a constant in one step
1744 ; ReduceMe want_scs -> -- It should be reduced
1745 lookupInst wanted `thenM` \ lookup_result ->
1746 case lookup_result of
1747 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1748 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1749 addWanted want_scs avails2 wanted rhs wanteds'
1750 -- Experiment with temporarily doing addIrred *before* the reduceList,
1751 -- which has the effect of adding the thing we are trying
1752 -- to prove to the database before trying to prove the things it
1753 -- needs. See note [RECURSIVE DICTIONARIES]
1754 -- NB: we must not do an addWanted before, because that adds the
1755 -- superclasses too, and thaat can lead to a spurious loop; see
1756 -- the examples in [SUPERCLASS-LOOP]
1757 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1759 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1761 NoInstance -> -- No such instance!
1762 -- Add it and its superclasses
1763 addIrred want_scs avails wanted
1766 try_simple do_this_otherwise
1767 = lookupInst wanted `thenM` \ lookup_result ->
1768 case lookup_result of
1769 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1770 other -> do_this_otherwise avails wanted
1775 -------------------------
1776 isAvailable :: Avails -> Inst -> Maybe Avail
1777 isAvailable avails wanted = lookupFM avails wanted
1778 -- NB 1: the Ord instance of Inst compares by the class/type info
1779 -- *not* by unique. So
1780 -- d1::C Int == d2::C Int
1782 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1783 addLinearAvailable avails avail wanted
1784 -- avails currently maps [wanted -> avail]
1785 -- Extend avails to reflect a neeed for an extra copy of avail
1787 | Just avail' <- split_avail avail
1788 = returnM (addToFM avails wanted avail', [])
1791 = tcLookupId splitName `thenM` \ split_id ->
1792 tcInstClassOp (instLoc wanted) split_id
1793 [linearInstType wanted] `thenM` \ split_inst ->
1794 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1797 split_avail :: Avail -> Maybe Avail
1798 -- (Just av) if there's a modified version of avail that
1799 -- we can use to replace avail in avails
1800 -- Nothing if there isn't, so we need to create a Linear
1801 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1802 split_avail (Given id used) | not used = Just (Given id True)
1803 | otherwise = Nothing
1804 split_avail Irred = Nothing
1805 split_avail IsFree = Nothing
1806 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1808 -------------------------
1809 addFree :: Avails -> Inst -> TcM Avails
1810 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1811 -- to avails, so that any other equal Insts will be commoned up right
1812 -- here rather than also being tossed upstairs. This is really just
1813 -- an optimisation, and perhaps it is more trouble that it is worth,
1814 -- as the following comments show!
1816 -- NB: do *not* add superclasses. If we have
1819 -- but a is not bound here, then we *don't* want to derive
1820 -- dn from df here lest we lose sharing.
1822 addFree avails free = returnM (addToFM avails free IsFree)
1824 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1825 addWanted want_scs avails wanted rhs_expr wanteds
1826 = addAvailAndSCs want_scs avails wanted avail
1828 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1829 | otherwise = ASSERT( null wanteds ) NoRhs
1831 addGiven :: Avails -> Inst -> TcM Avails
1832 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1833 -- Always add superclasses for 'givens'
1835 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1836 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1837 -- so the assert isn't true
1839 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1840 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1841 addAvailAndSCs want_scs avails irred Irred
1843 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1844 addAvailAndSCs want_scs avails inst avail
1845 | not (isClassDict inst) = return avails_with_inst
1846 | NoSCs <- want_scs = return avails_with_inst
1847 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1848 ; addSCs is_loop avails_with_inst inst }
1850 avails_with_inst = addToFM avails inst avail
1852 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1853 -- Note: this compares by *type*, not by Unique
1854 deps = findAllDeps (unitVarSet (instToId inst)) avail
1855 dep_tys = map idType (varSetElems deps)
1857 findAllDeps :: IdSet -> Avail -> IdSet
1858 -- Find all the Insts that this one depends on
1859 -- See Note [SUPERCLASS-LOOP]
1860 -- Watch out, though. Since the avails may contain loops
1861 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1862 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1863 findAllDeps so_far other = so_far
1865 find_all :: IdSet -> Inst -> IdSet
1867 | kid_id `elemVarSet` so_far = so_far
1868 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1869 | otherwise = so_far'
1871 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1872 kid_id = instToId kid
1874 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1875 -- Add all the superclasses of the Inst to Avails
1876 -- The first param says "dont do this because the original thing
1877 -- depends on this one, so you'd build a loop"
1878 -- Invariant: the Inst is already in Avails.
1880 addSCs is_loop avails dict
1881 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1882 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1884 (clas, tys) = getDictClassTys dict
1885 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1886 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1888 add_sc avails (sc_dict, sc_sel)
1889 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1890 | is_given sc_dict = return avails
1891 | otherwise = addSCs is_loop avails' sc_dict
1893 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1894 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1896 is_given :: Inst -> Bool
1897 is_given sc_dict = case lookupFM avails sc_dict of
1898 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1902 Note [SUPERCLASS-LOOP 2]
1903 ~~~~~~~~~~~~~~~~~~~~~~~~
1904 But the above isn't enough. Suppose we are *given* d1:Ord a,
1905 and want to deduce (d2:C [a]) where
1907 class Ord a => C a where
1908 instance Ord [a] => C [a] where ...
1910 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1911 superclasses of C [a] to avails. But we must not overwrite the binding
1912 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1915 Here's another variant, immortalised in tcrun020
1916 class Monad m => C1 m
1917 class C1 m => C2 m x
1918 instance C2 Maybe Bool
1919 For the instance decl we need to build (C1 Maybe), and it's no good if
1920 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1921 before we search for C1 Maybe.
1923 Here's another example
1924 class Eq b => Foo a b
1925 instance Eq a => Foo [a] a
1929 we'll first deduce that it holds (via the instance decl). We must not
1930 then overwrite the Eq t constraint with a superclass selection!
1932 At first I had a gross hack, whereby I simply did not add superclass constraints
1933 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1934 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1935 I found a very obscure program (now tcrun021) in which improvement meant the
1936 simplifier got two bites a the cherry... so something seemed to be an Irred
1937 first time, but reducible next time.
1939 Now we implement the Right Solution, which is to check for loops directly
1940 when adding superclasses. It's a bit like the occurs check in unification.
1943 Note [RECURSIVE DICTIONARIES]
1944 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1946 data D r = ZeroD | SuccD (r (D r));
1948 instance (Eq (r (D r))) => Eq (D r) where
1949 ZeroD == ZeroD = True
1950 (SuccD a) == (SuccD b) = a == b
1953 equalDC :: D [] -> D [] -> Bool;
1956 We need to prove (Eq (D [])). Here's how we go:
1960 by instance decl, holds if
1964 by instance decl of Eq, holds if
1966 where d2 = dfEqList d3
1969 But now we can "tie the knot" to give
1975 and it'll even run! The trick is to put the thing we are trying to prove
1976 (in this case Eq (D []) into the database before trying to prove its
1977 contributing clauses.
1980 %************************************************************************
1982 \section{tcSimplifyTop: defaulting}
1984 %************************************************************************
1987 @tcSimplifyTop@ is called once per module to simplify all the constant
1988 and ambiguous Insts.
1990 We need to be careful of one case. Suppose we have
1992 instance Num a => Num (Foo a b) where ...
1994 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1995 to (Num x), and default x to Int. But what about y??
1997 It's OK: the final zonking stage should zap y to (), which is fine.
2001 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2002 tcSimplifyTop wanteds
2003 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2005 doc = text "tcSimplifyTop"
2007 tcSimplifyInteractive wanteds
2008 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2010 doc = text "tcSimplifyTop"
2012 -- The TcLclEnv should be valid here, solely to improve
2013 -- error message generation for the monomorphism restriction
2014 tc_simplify_top doc is_interactive want_scs wanteds
2015 = do { lcl_env <- getLclEnv
2016 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2018 ; let try_me inst = ReduceMe want_scs
2019 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2022 -- All the non-std ones are definite errors
2023 (stds, non_stds) = partition isStdClassTyVarDict irreds
2025 -- Group by type variable
2026 std_groups = equivClasses cmp_by_tyvar stds
2028 -- Pick the ones which its worth trying to disambiguate
2029 -- namely, the onese whose type variable isn't bound
2030 -- up with one of the non-standard classes
2031 (std_oks, std_bads) = partition worth_a_try std_groups
2032 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
2033 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
2035 -- Collect together all the bad guys
2036 bad_guys = non_stds ++ concat std_bads
2037 (non_ips, bad_ips) = partition isClassDict bad_guys
2038 (ambigs, no_insts) = partition isTyVarDict non_ips
2039 -- If the dict has no type constructors involved, it must be ambiguous,
2040 -- except I suppose that another error with fundeps maybe should have
2041 -- constrained those type variables
2043 -- Report definite errors
2044 ; ASSERT( null frees )
2045 groupErrs (addNoInstanceErrs Nothing []) no_insts
2046 ; strangeTopIPErrs bad_ips
2048 -- Deal with ambiguity errors, but only if
2049 -- if there has not been an error so far:
2050 -- errors often give rise to spurious ambiguous Insts.
2052 -- f = (*) -- Monomorphic
2053 -- g :: Num a => a -> a
2055 -- Here, we get a complaint when checking the type signature for g,
2056 -- that g isn't polymorphic enough; but then we get another one when
2057 -- dealing with the (Num a) context arising from f's definition;
2058 -- we try to unify a with Int (to default it), but find that it's
2059 -- already been unified with the rigid variable from g's type sig
2060 ; binds_ambig <- ifErrsM (returnM []) $
2061 do { -- Complain about the ones that don't fall under
2062 -- the Haskell rules for disambiguation
2063 -- This group includes both non-existent instances
2064 -- e.g. Num (IO a) and Eq (Int -> Int)
2065 -- and ambiguous dictionaries
2067 addTopAmbigErrs ambigs
2069 -- Disambiguate the ones that look feasible
2070 ; mappM (disambigGroup is_interactive) std_oks }
2072 ; return (binds `unionBags` unionManyBags binds_ambig) }
2074 ----------------------------------
2075 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2077 get_tv d = case getDictClassTys d of
2078 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2079 get_clas d = case getDictClassTys d of
2080 (clas, [ty]) -> clas
2083 If a dictionary constrains a type variable which is
2084 * not mentioned in the environment
2085 * and not mentioned in the type of the expression
2086 then it is ambiguous. No further information will arise to instantiate
2087 the type variable; nor will it be generalised and turned into an extra
2088 parameter to a function.
2090 It is an error for this to occur, except that Haskell provided for
2091 certain rules to be applied in the special case of numeric types.
2093 * at least one of its classes is a numeric class, and
2094 * all of its classes are numeric or standard
2095 then the type variable can be defaulted to the first type in the
2096 default-type list which is an instance of all the offending classes.
2098 So here is the function which does the work. It takes the ambiguous
2099 dictionaries and either resolves them (producing bindings) or
2100 complains. It works by splitting the dictionary list by type
2101 variable, and using @disambigOne@ to do the real business.
2103 @disambigOne@ assumes that its arguments dictionaries constrain all
2104 the same type variable.
2106 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2107 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2108 the most common use of defaulting is code like:
2110 _ccall_ foo `seqPrimIO` bar
2112 Since we're not using the result of @foo@, the result if (presumably)
2116 disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
2117 -> [Inst] -- All standard classes of form (C a)
2120 disambigGroup is_interactive dicts
2121 | any std_default_class classes -- Guaranteed all standard classes
2122 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2123 -- SO, TRY DEFAULT TYPES IN ORDER
2125 -- Failure here is caused by there being no type in the
2126 -- default list which can satisfy all the ambiguous classes.
2127 -- For example, if Real a is reqd, but the only type in the
2128 -- default list is Int.
2129 get_default_tys `thenM` \ default_tys ->
2131 try_default [] -- No defaults work, so fail
2134 try_default (default_ty : default_tys)
2135 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2136 -- default_tys instead
2137 tcSimplifyDefault theta `thenM` \ _ ->
2140 theta = [mkClassPred clas [default_ty] | clas <- classes]
2142 -- See if any default works
2143 tryM (try_default default_tys) `thenM` \ mb_ty ->
2146 Right chosen_default_ty -> choose_default chosen_default_ty
2148 | otherwise -- No defaults
2152 tyvar = get_tv (head dicts) -- Should be non-empty
2153 classes = map get_clas dicts
2155 std_default_class cls
2156 = isNumericClass cls
2157 || (is_interactive &&
2158 classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2159 -- In interactive mode, we default Show a to Show ()
2160 -- to avoid graututious errors on "show []"
2162 choose_default default_ty -- Commit to tyvar = default_ty
2163 = -- Bind the type variable
2164 unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
2165 -- and reduce the context, for real this time
2166 simpleReduceLoop (text "disambig" <+> ppr dicts)
2167 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2168 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2169 warnDefault dicts default_ty `thenM_`
2172 bomb_out = addTopAmbigErrs dicts `thenM_`
2176 = do { mb_defaults <- getDefaultTys
2177 ; case mb_defaults of
2178 Just tys -> return tys
2179 Nothing -> -- No use-supplied default;
2180 -- use [Integer, Double]
2181 do { integer_ty <- tcMetaTy integerTyConName
2182 ; return [integer_ty, doubleTy] } }
2185 [Aside - why the defaulting mechanism is turned off when
2186 dealing with arguments and results to ccalls.
2188 When typechecking _ccall_s, TcExpr ensures that the external
2189 function is only passed arguments (and in the other direction,
2190 results) of a restricted set of 'native' types. This is
2191 implemented via the help of the pseudo-type classes,
2192 @CReturnable@ (CR) and @CCallable@ (CC.)
2194 The interaction between the defaulting mechanism for numeric
2195 values and CC & CR can be a bit puzzling to the user at times.
2204 What type has 'x' got here? That depends on the default list
2205 in operation, if it is equal to Haskell 98's default-default
2206 of (Integer, Double), 'x' has type Double, since Integer
2207 is not an instance of CR. If the default list is equal to
2208 Haskell 1.4's default-default of (Int, Double), 'x' has type
2211 To try to minimise the potential for surprises here, the
2212 defaulting mechanism is turned off in the presence of
2213 CCallable and CReturnable.
2218 %************************************************************************
2220 \subsection[simple]{@Simple@ versions}
2222 %************************************************************************
2224 Much simpler versions when there are no bindings to make!
2226 @tcSimplifyThetas@ simplifies class-type constraints formed by
2227 @deriving@ declarations and when specialising instances. We are
2228 only interested in the simplified bunch of class/type constraints.
2230 It simplifies to constraints of the form (C a b c) where
2231 a,b,c are type variables. This is required for the context of
2232 instance declarations.
2235 tcSimplifyDeriv :: [TyVar]
2236 -> ThetaType -- Wanted
2237 -> TcM ThetaType -- Needed
2239 tcSimplifyDeriv tyvars theta
2240 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2241 -- The main loop may do unification, and that may crash if
2242 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2243 -- ToDo: what if two of them do get unified?
2244 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2245 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2246 ASSERT( null frees ) -- reduceMe never returns Free
2248 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2250 tv_set = mkVarSet tvs
2252 (bad_insts, ok_insts) = partition is_bad_inst irreds
2254 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2255 in isEmptyVarSet (tyVarsOfPred pred)
2256 -- Things like (Eq T) are bad
2257 || (not undecidable_ok && not (isTyVarClassPred pred))
2258 -- The returned dictionaries should be of form (C a b)
2259 -- (where a, b are type variables).
2260 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
2261 -- but note that risks non-termination in the 'deriving' context-inference
2262 -- fixpoint loop. It is useful for situations like
2263 -- data Min h a = E | M a (h a)
2264 -- which gives the instance decl
2265 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
2267 simpl_theta = map dictPred ok_insts
2268 weird_preds = [pred | pred <- simpl_theta
2269 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2270 -- Check for a bizarre corner case, when the derived instance decl should
2271 -- have form instance C a b => D (T a) where ...
2272 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2273 -- of problems; in particular, it's hard to compare solutions for
2274 -- equality when finding the fixpoint. So I just rule it out for now.
2276 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2277 -- This reverse-mapping is a Royal Pain,
2278 -- but the result should mention TyVars not TcTyVars
2281 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2282 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2283 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2284 returnM (substTheta rev_env simpl_theta)
2286 doc = ptext SLIT("deriving classes for a data type")
2289 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2290 used with \tr{default} declarations. We are only interested in
2291 whether it worked or not.
2294 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2297 tcSimplifyDefault theta
2298 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2299 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2300 ASSERT( null frees ) -- try_me never returns Free
2301 addNoInstanceErrs Nothing [] irreds `thenM_`
2307 doc = ptext SLIT("default declaration")
2311 %************************************************************************
2313 \section{Errors and contexts}
2315 %************************************************************************
2317 ToDo: for these error messages, should we note the location as coming
2318 from the insts, or just whatever seems to be around in the monad just
2322 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2323 -> [Inst] -- The offending Insts
2325 -- Group together insts with the same origin
2326 -- We want to report them together in error messages
2328 groupErrs report_err []
2330 groupErrs report_err (inst:insts)
2331 = do_one (inst:friends) `thenM_`
2332 groupErrs report_err others
2335 -- (It may seem a bit crude to compare the error messages,
2336 -- but it makes sure that we combine just what the user sees,
2337 -- and it avoids need equality on InstLocs.)
2338 (friends, others) = partition is_friend insts
2339 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2340 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2341 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2342 -- Add location and context information derived from the Insts
2344 -- Add the "arising from..." part to a message about bunch of dicts
2345 addInstLoc :: [Inst] -> Message -> Message
2346 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2349 plural xs = char 's'
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 the monomorphic top-level binding(s) of"),
2359 pprBinders bndrs <> colon],
2360 nest 2 (vcat (map ppr_ip ips)),
2362 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2364 strangeTopIPErrs :: [Inst] -> TcM ()
2365 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2366 = groupErrs report tidy_dicts
2368 (tidy_env, tidy_dicts) = tidyInsts dicts
2369 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2370 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2371 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2373 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2374 -- Just d => d describes the construct
2375 -> [Inst] -- What is given by the context or type sig
2376 -> [Inst] -- What is wanted
2378 addNoInstanceErrs mb_what givens []
2380 addNoInstanceErrs mb_what givens dicts
2381 = -- Some of the dicts are here because there is no instances
2382 -- and some because there are too many instances (overlap)
2383 getDOpts `thenM` \ dflags ->
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 dflags 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 [pprDFuns dfuns, pprDFuns 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 dfuns = [df | (_, (_,_,df)) <- matches]
2439 mk_probable_fix tidy_env dicts
2440 = returnM (tidy_env, sep [ptext SLIT("Probable 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-stack20 to increase stack size to (e.g.) 20"),
2526 nest 4 (pprStack stack)]
2528 pprStack stack = vcat (map pprInstInFull stack)