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(..) )
71 import DynFlags ( DynFlag(..) )
76 %************************************************************************
80 %************************************************************************
82 --------------------------------------
83 Notes on functional dependencies (a bug)
84 --------------------------------------
86 | > class Foo a b | a->b
88 | > class Bar a b | a->b
92 | > instance Bar Obj Obj
94 | > instance (Bar a b) => Foo a b
96 | > foo:: (Foo a b) => a -> String
99 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
105 | Could not deduce (Bar a b) from the context (Foo a b)
106 | arising from use of `foo' at <interactive>:1
108 | Add (Bar a b) to the expected type of an expression
109 | In the first argument of `runFoo', namely `foo'
110 | In the definition of `it': it = runFoo foo
112 | Why all of the sudden does GHC need the constraint Bar a b? The
113 | function foo didn't ask for that...
115 The trouble is that to type (runFoo foo), GHC has to solve the problem:
117 Given constraint Foo a b
118 Solve constraint Foo a b'
120 Notice that b and b' aren't the same. To solve this, just do
121 improvement and then they are the same. But GHC currently does
126 That is usually fine, but it isn't here, because it sees that Foo a b is
127 not the same as Foo a b', and so instead applies the instance decl for
128 instance Bar a b => Foo a b. And that's where the Bar constraint comes
131 The Right Thing is to improve whenever the constraint set changes at
132 all. Not hard in principle, but it'll take a bit of fiddling to do.
136 --------------------------------------
137 Notes on quantification
138 --------------------------------------
140 Suppose we are about to do a generalisation step.
144 T the type of the RHS
145 C the constraints from that RHS
147 The game is to figure out
149 Q the set of type variables over which to quantify
150 Ct the constraints we will *not* quantify over
151 Cq the constraints we will quantify over
153 So we're going to infer the type
157 and float the constraints Ct further outwards.
159 Here are the things that *must* be true:
161 (A) Q intersect fv(G) = EMPTY limits how big Q can be
162 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
164 (A) says we can't quantify over a variable that's free in the
165 environment. (B) says we must quantify over all the truly free
166 variables in T, else we won't get a sufficiently general type. We do
167 not *need* to quantify over any variable that is fixed by the free
168 vars of the environment G.
170 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
172 Example: class H x y | x->y where ...
174 fv(G) = {a} C = {H a b, H c d}
177 (A) Q intersect {a} is empty
178 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
180 So Q can be {c,d}, {b,c,d}
182 Other things being equal, however, we'd like to quantify over as few
183 variables as possible: smaller types, fewer type applications, more
184 constraints can get into Ct instead of Cq.
187 -----------------------------------------
190 fv(T) the free type vars of T
192 oclose(vs,C) The result of extending the set of tyvars vs
193 using the functional dependencies from C
195 grow(vs,C) The result of extend the set of tyvars vs
196 using all conceivable links from C.
198 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
199 Then grow(vs,C) = {a,b,c}
201 Note that grow(vs,C) `superset` grow(vs,simplify(C))
202 That is, simplfication can only shrink the result of grow.
205 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
206 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
209 -----------------------------------------
213 Here's a good way to choose Q:
215 Q = grow( fv(T), C ) \ oclose( fv(G), C )
217 That is, quantify over all variable that that MIGHT be fixed by the
218 call site (which influences T), but which aren't DEFINITELY fixed by
219 G. This choice definitely quantifies over enough type variables,
220 albeit perhaps too many.
222 Why grow( fv(T), C ) rather than fv(T)? Consider
224 class H x y | x->y where ...
229 If we used fv(T) = {c} we'd get the type
231 forall c. H c d => c -> b
233 And then if the fn was called at several different c's, each of
234 which fixed d differently, we'd get a unification error, because
235 d isn't quantified. Solution: quantify d. So we must quantify
236 everything that might be influenced by c.
238 Why not oclose( fv(T), C )? Because we might not be able to see
239 all the functional dependencies yet:
241 class H x y | x->y where ...
242 instance H x y => Eq (T x y) where ...
247 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
248 apparent yet, and that's wrong. We must really quantify over d too.
251 There really isn't any point in quantifying over any more than
252 grow( fv(T), C ), because the call sites can't possibly influence
253 any other type variables.
257 --------------------------------------
259 --------------------------------------
261 It's very hard to be certain when a type is ambiguous. Consider
265 instance H x y => K (x,y)
267 Is this type ambiguous?
268 forall a b. (K (a,b), Eq b) => a -> a
270 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
271 now we see that a fixes b. So we can't tell about ambiguity for sure
272 without doing a full simplification. And even that isn't possible if
273 the context has some free vars that may get unified. Urgle!
275 Here's another example: is this ambiguous?
276 forall a b. Eq (T b) => a -> a
277 Not if there's an insance decl (with no context)
278 instance Eq (T b) where ...
280 You may say of this example that we should use the instance decl right
281 away, but you can't always do that:
283 class J a b where ...
284 instance J Int b where ...
286 f :: forall a b. J a b => a -> a
288 (Notice: no functional dependency in J's class decl.)
289 Here f's type is perfectly fine, provided f is only called at Int.
290 It's premature to complain when meeting f's signature, or even
291 when inferring a type for f.
295 However, we don't *need* to report ambiguity right away. It'll always
296 show up at the call site.... and eventually at main, which needs special
297 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
299 So here's the plan. We WARN about probable ambiguity if
301 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
303 (all tested before quantification).
304 That is, all the type variables in Cq must be fixed by the the variables
305 in the environment, or by the variables in the type.
307 Notice that we union before calling oclose. Here's an example:
309 class J a b c | a b -> c
313 forall b c. (J a b c) => b -> b
315 Only if we union {a} from G with {b} from T before using oclose,
316 do we see that c is fixed.
318 It's a bit vague exactly which C we should use for this oclose call. If we
319 don't fix enough variables we might complain when we shouldn't (see
320 the above nasty example). Nothing will be perfect. That's why we can
321 only issue a warning.
324 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
326 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
328 then c is a "bubble"; there's no way it can ever improve, and it's
329 certainly ambiguous. UNLESS it is a constant (sigh). And what about
334 instance H x y => K (x,y)
336 Is this type ambiguous?
337 forall a b. (K (a,b), Eq b) => a -> a
339 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
340 is a "bubble" that's a set of constraints
342 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
344 Hence another idea. To decide Q start with fv(T) and grow it
345 by transitive closure in Cq (no functional dependencies involved).
346 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
347 The definitely-ambiguous can then float out, and get smashed at top level
348 (which squashes out the constants, like Eq (T a) above)
351 --------------------------------------
352 Notes on principal types
353 --------------------------------------
358 f x = let g y = op (y::Int) in True
360 Here the principal type of f is (forall a. a->a)
361 but we'll produce the non-principal type
362 f :: forall a. C Int => a -> a
365 --------------------------------------
366 The need for forall's in constraints
367 --------------------------------------
369 [Exchange on Haskell Cafe 5/6 Dec 2000]
371 class C t where op :: t -> Bool
372 instance C [t] where op x = True
374 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
375 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
377 The definitions of p and q differ only in the order of the components in
378 the pair on their right-hand sides. And yet:
380 ghc and "Typing Haskell in Haskell" reject p, but accept q;
381 Hugs rejects q, but accepts p;
382 hbc rejects both p and q;
383 nhc98 ... (Malcolm, can you fill in the blank for us!).
385 The type signature for f forces context reduction to take place, and
386 the results of this depend on whether or not the type of y is known,
387 which in turn depends on which component of the pair the type checker
390 Solution: if y::m a, float out the constraints
391 Monad m, forall c. C (m c)
392 When m is later unified with [], we can solve both constraints.
395 --------------------------------------
396 Notes on implicit parameters
397 --------------------------------------
399 Question 1: can we "inherit" implicit parameters
400 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
405 where f is *not* a top-level binding.
406 From the RHS of f we'll get the constraint (?y::Int).
407 There are two types we might infer for f:
411 (so we get ?y from the context of f's definition), or
413 f :: (?y::Int) => Int -> Int
415 At first you might think the first was better, becuase then
416 ?y behaves like a free variable of the definition, rather than
417 having to be passed at each call site. But of course, the WHOLE
418 IDEA is that ?y should be passed at each call site (that's what
419 dynamic binding means) so we'd better infer the second.
421 BOTTOM LINE: when *inferring types* you *must* quantify
422 over implicit parameters. See the predicate isFreeWhenInferring.
425 Question 2: type signatures
426 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
427 BUT WATCH OUT: When you supply a type signature, we can't force you
428 to quantify over implicit parameters. For example:
432 This is perfectly reasonable. We do not want to insist on
434 (?x + 1) :: (?x::Int => Int)
436 That would be silly. Here, the definition site *is* the occurrence site,
437 so the above strictures don't apply. Hence the difference between
438 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
439 and tcSimplifyCheckBind (which does not).
441 What about when you supply a type signature for a binding?
442 Is it legal to give the following explicit, user type
443 signature to f, thus:
448 At first sight this seems reasonable, but it has the nasty property
449 that adding a type signature changes the dynamic semantics.
452 (let f x = (x::Int) + ?y
453 in (f 3, f 3 with ?y=5)) with ?y = 6
459 in (f 3, f 3 with ?y=5)) with ?y = 6
463 Indeed, simply inlining f (at the Haskell source level) would change the
466 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
467 semantics for a Haskell program without knowing its typing, so if you
468 change the typing you may change the semantics.
470 To make things consistent in all cases where we are *checking* against
471 a supplied signature (as opposed to inferring a type), we adopt the
474 a signature does not need to quantify over implicit params.
476 [This represents a (rather marginal) change of policy since GHC 5.02,
477 which *required* an explicit signature to quantify over all implicit
478 params for the reasons mentioned above.]
480 But that raises a new question. Consider
482 Given (signature) ?x::Int
483 Wanted (inferred) ?x::Int, ?y::Bool
485 Clearly we want to discharge the ?x and float the ?y out. But
486 what is the criterion that distinguishes them? Clearly it isn't
487 what free type variables they have. The Right Thing seems to be
488 to float a constraint that
489 neither mentions any of the quantified type variables
490 nor any of the quantified implicit parameters
492 See the predicate isFreeWhenChecking.
495 Question 3: monomorphism
496 ~~~~~~~~~~~~~~~~~~~~~~~~
497 There's a nasty corner case when the monomorphism restriction bites:
501 The argument above suggests that we *must* generalise
502 over the ?y parameter, to get
503 z :: (?y::Int) => Int,
504 but the monomorphism restriction says that we *must not*, giving
506 Why does the momomorphism restriction say this? Because if you have
508 let z = x + ?y in z+z
510 you might not expect the addition to be done twice --- but it will if
511 we follow the argument of Question 2 and generalise over ?y.
514 Question 4: top level
515 ~~~~~~~~~~~~~~~~~~~~~
516 At the top level, monomorhism makes no sense at all.
519 main = let ?x = 5 in print foo
523 woggle :: (?x :: Int) => Int -> Int
526 We definitely don't want (foo :: Int) with a top-level implicit parameter
527 (?x::Int) becuase there is no way to bind it.
532 (A) Always generalise over implicit parameters
533 Bindings that fall under the monomorphism restriction can't
537 * Inlining remains valid
538 * No unexpected loss of sharing
539 * But simple bindings like
541 will be rejected, unless you add an explicit type signature
542 (to avoid the monomorphism restriction)
543 z :: (?y::Int) => Int
545 This seems unacceptable
547 (B) Monomorphism restriction "wins"
548 Bindings that fall under the monomorphism restriction can't
550 Always generalise over implicit parameters *except* for bindings
551 that fall under the monomorphism restriction
554 * Inlining isn't valid in general
555 * No unexpected loss of sharing
556 * Simple bindings like
558 accepted (get value of ?y from binding site)
560 (C) Always generalise over implicit parameters
561 Bindings that fall under the monomorphism restriction can't
562 be generalised, EXCEPT for implicit parameters
564 * Inlining remains valid
565 * Unexpected loss of sharing (from the extra generalisation)
566 * Simple bindings like
568 accepted (get value of ?y from occurrence sites)
573 None of these choices seems very satisfactory. But at least we should
574 decide which we want to do.
576 It's really not clear what is the Right Thing To Do. If you see
580 would you expect the value of ?y to be got from the *occurrence sites*
581 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
582 case of function definitions, the answer is clearly the former, but
583 less so in the case of non-fucntion definitions. On the other hand,
584 if we say that we get the value of ?y from the definition site of 'z',
585 then inlining 'z' might change the semantics of the program.
587 Choice (C) really says "the monomorphism restriction doesn't apply
588 to implicit parameters". Which is fine, but remember that every
589 innocent binding 'x = ...' that mentions an implicit parameter in
590 the RHS becomes a *function* of that parameter, called at each
591 use of 'x'. Now, the chances are that there are no intervening 'with'
592 clauses that bind ?y, so a decent compiler should common up all
593 those function calls. So I think I strongly favour (C). Indeed,
594 one could make a similar argument for abolishing the monomorphism
595 restriction altogether.
597 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
601 %************************************************************************
603 \subsection{tcSimplifyInfer}
605 %************************************************************************
607 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
609 1. Compute Q = grow( fvs(T), C )
611 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
612 predicates will end up in Ct; we deal with them at the top level
614 3. Try improvement, using functional dependencies
616 4. If Step 3 did any unification, repeat from step 1
617 (Unification can change the result of 'grow'.)
619 Note: we don't reduce dictionaries in step 2. For example, if we have
620 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
621 after step 2. However note that we may therefore quantify over more
622 type variables than we absolutely have to.
624 For the guts, we need a loop, that alternates context reduction and
625 improvement with unification. E.g. Suppose we have
627 class C x y | x->y where ...
629 and tcSimplify is called with:
631 Then improvement unifies a with b, giving
634 If we need to unify anything, we rattle round the whole thing all over
641 -> TcTyVarSet -- fv(T); type vars
643 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
644 TcDictBinds, -- Bindings
645 [TcId]) -- Dict Ids that must be bound here (zonked)
646 -- Any free (escaping) Insts are tossed into the environment
651 tcSimplifyInfer doc tau_tvs wanted_lie
652 = inferLoop doc (varSetElems tau_tvs)
653 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
655 extendLIEs frees `thenM_`
656 returnM (qtvs, binds, map instToId irreds)
658 inferLoop doc tau_tvs wanteds
660 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
661 mappM zonkInst wanteds `thenM` \ wanteds' ->
662 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
664 preds = fdPredsOfInsts wanteds'
665 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
668 | isFreeWhenInferring qtvs inst = Free
669 | isClassDict inst = DontReduceUnlessConstant -- Dicts
670 | otherwise = ReduceMe NoSCs -- Lits and Methods
672 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
673 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
675 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
678 if no_improvement then
679 returnM (varSetElems qtvs, frees, binds, irreds)
681 -- If improvement did some unification, we go round again. There
682 -- are two subtleties:
683 -- a) We start again with irreds, not wanteds
684 -- Using an instance decl might have introduced a fresh type variable
685 -- which might have been unified, so we'd get an infinite loop
686 -- if we started again with wanteds! See example [LOOP]
688 -- b) It's also essential to re-process frees, because unification
689 -- might mean that a type variable that looked free isn't now.
691 -- Hence the (irreds ++ frees)
693 -- However, NOTICE that when we are done, we might have some bindings, but
694 -- the final qtvs might be empty. See [NO TYVARS] below.
696 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
697 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
702 class If b t e r | b t e -> r
705 class Lte a b c | a b -> c where lte :: a -> b -> c
707 instance (Lte a b l,If l b a c) => Max a b c
709 Wanted: Max Z (S x) y
711 Then we'll reduce using the Max instance to:
712 (Lte Z (S x) l, If l (S x) Z y)
713 and improve by binding l->T, after which we can do some reduction
714 on both the Lte and If constraints. What we *can't* do is start again
715 with (Max Z (S x) y)!
719 class Y a b | a -> b where
722 instance Y [[a]] a where
725 k :: X a -> X a -> X a
727 g :: Num a => [X a] -> [X a]
730 h ys = ys ++ map (k (y [[0]])) xs
732 The excitement comes when simplifying the bindings for h. Initially
733 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
734 From this we get t1:=:t2, but also various bindings. We can't forget
735 the bindings (because of [LOOP]), but in fact t1 is what g is
738 The net effect of [NO TYVARS]
741 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
742 isFreeWhenInferring qtvs inst
743 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
744 && isInheritableInst inst -- And no implicit parameter involved
745 -- (see "Notes on implicit parameters")
747 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
748 -> NameSet -- Quantified implicit parameters
750 isFreeWhenChecking qtvs ips inst
751 = isFreeWrtTyVars qtvs inst
752 && isFreeWrtIPs ips inst
754 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
755 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
759 %************************************************************************
761 \subsection{tcSimplifyCheck}
763 %************************************************************************
765 @tcSimplifyCheck@ is used when we know exactly the set of variables
766 we are going to quantify over. For example, a class or instance declaration.
771 -> [TcTyVar] -- Quantify over these
774 -> TcM TcDictBinds -- Bindings
776 -- tcSimplifyCheck is used when checking expression type signatures,
777 -- class decls, instance decls etc.
779 -- NB: tcSimplifyCheck does not consult the
780 -- global type variables in the environment; so you don't
781 -- need to worry about setting them before calling tcSimplifyCheck
782 tcSimplifyCheck doc qtvs givens wanted_lie
783 = ASSERT( all isSkolemTyVar qtvs )
784 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
788 -- get_qtvs = zonkTcTyVarsAndFV qtvs
789 get_qtvs = return (mkVarSet qtvs) -- All skolems
792 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
793 -- against, but we don't know the type variables over which we are going to quantify.
794 -- This happens when we have a type signature for a mutually recursive group
797 -> TcTyVarSet -- fv(T)
800 -> TcM ([TcTyVar], -- Variables over which to quantify
801 TcDictBinds) -- Bindings
803 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
804 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
806 ; return (qtvs', binds) }
808 -- Figure out which type variables to quantify over
809 -- You might think it should just be the signature tyvars,
810 -- but in bizarre cases you can get extra ones
811 -- f :: forall a. Num a => a -> a
812 -- f x = fst (g (x, head [])) + 1
814 -- Here we infer g :: forall a b. a -> b -> (b,a)
815 -- We don't want g to be monomorphic in b just because
816 -- f isn't quantified over b.
817 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
819 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
820 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
822 qtvs = all_tvs' `minusVarSet` gbl_tvs
823 -- We could close gbl_tvs, but its not necessary for
824 -- soundness, and it'll only affect which tyvars, not which
825 -- dictionaries, we quantify over
830 Here is the workhorse function for all three wrappers.
833 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
834 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
836 -- Complain about any irreducible ones
837 ; if not (null irreds)
838 then do { givens' <- mappM zonkInst given_dicts_and_ips
839 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
842 ; returnM (qtvs, frees, binds) }
844 given_dicts_and_ips = filter (not . isMethod) givens
845 -- For error reporting, filter out methods, which are
846 -- only added to the given set as an optimisation
848 ip_set = mkNameSet (ipNamesOfInsts givens)
850 check_loop givens wanteds
852 mappM zonkInst givens `thenM` \ givens' ->
853 mappM zonkInst wanteds `thenM` \ wanteds' ->
854 get_qtvs `thenM` \ qtvs' ->
858 -- When checking against a given signature we always reduce
859 -- until we find a match against something given, or can't reduce
860 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
861 | otherwise = ReduceMe want_scs
863 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
866 if no_improvement then
867 returnM (varSetElems qtvs', frees, binds, irreds)
869 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
870 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
874 %************************************************************************
876 tcSimplifySuperClasses
878 %************************************************************************
880 Note [SUPERCLASS-LOOP 1]
881 ~~~~~~~~~~~~~~~~~~~~~~~~
882 We have to be very, very careful when generating superclasses, lest we
883 accidentally build a loop. Here's an example:
887 class S a => C a where { opc :: a -> a }
888 class S b => D b where { opd :: b -> b }
896 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
897 Simplifying, we may well get:
898 $dfCInt = :C ds1 (opd dd)
901 Notice that we spot that we can extract ds1 from dd.
903 Alas! Alack! We can do the same for (instance D Int):
905 $dfDInt = :D ds2 (opc dc)
909 And now we've defined the superclass in terms of itself.
911 Solution: never generate a superclass selectors at all when
912 satisfying the superclass context of an instance declaration.
914 Two more nasty cases are in
919 tcSimplifySuperClasses qtvs givens sc_wanteds
920 = ASSERT( all isSkolemTyVar qtvs )
921 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
922 ; binds2 <- tc_simplify_top doc False NoSCs frees
923 ; return (binds1 `unionBags` binds2) }
925 get_qtvs = return (mkVarSet qtvs)
926 doc = ptext SLIT("instance declaration superclass context")
930 %************************************************************************
932 \subsection{tcSimplifyRestricted}
934 %************************************************************************
936 tcSimplifyRestricted infers which type variables to quantify for a
937 group of restricted bindings. This isn't trivial.
940 We want to quantify over a to get id :: forall a. a->a
943 We do not want to quantify over a, because there's an Eq a
944 constraint, so we get eq :: a->a->Bool (notice no forall)
947 RHS has type 'tau', whose free tyvars are tau_tvs
948 RHS has constraints 'wanteds'
951 Quantify over (tau_tvs \ ftvs(wanteds))
952 This is bad. The constraints may contain (Monad (ST s))
953 where we have instance Monad (ST s) where...
954 so there's no need to be monomorphic in s!
956 Also the constraint might be a method constraint,
957 whose type mentions a perfectly innocent tyvar:
958 op :: Num a => a -> b -> a
959 Here, b is unconstrained. A good example would be
961 We want to infer the polymorphic type
962 foo :: forall b. b -> b
965 Plan B (cunning, used for a long time up to and including GHC 6.2)
966 Step 1: Simplify the constraints as much as possible (to deal
967 with Plan A's problem). Then set
968 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
970 Step 2: Now simplify again, treating the constraint as 'free' if
971 it does not mention qtvs, and trying to reduce it otherwise.
972 The reasons for this is to maximise sharing.
974 This fails for a very subtle reason. Suppose that in the Step 2
975 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
976 In the Step 1 this constraint might have been simplified, perhaps to
977 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
978 This won't happen in Step 2... but that in turn might prevent some other
979 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
980 and that in turn breaks the invariant that no constraints are quantified over.
982 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
987 Step 1: Simplify the constraints as much as possible (to deal
988 with Plan A's problem). Then set
989 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
990 Return the bindings from Step 1.
993 A note about Plan C (arising from "bug" reported by George Russel March 2004)
996 instance (HasBinary ty IO) => HasCodedValue ty
998 foo :: HasCodedValue a => String -> IO a
1000 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1001 doDecodeIO codedValue view
1002 = let { act = foo "foo" } in act
1004 You might think this should work becuase the call to foo gives rise to a constraint
1005 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1006 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1007 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1009 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1013 Plan D (a variant of plan B)
1014 Step 1: Simplify the constraints as much as possible (to deal
1015 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1016 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1018 Step 2: Now simplify again, treating the constraint as 'free' if
1019 it does not mention qtvs, and trying to reduce it otherwise.
1021 The point here is that it's generally OK to have too few qtvs; that is,
1022 to make the thing more monomorphic than it could be. We don't want to
1023 do that in the common cases, but in wierd cases it's ok: the programmer
1024 can always add a signature.
1026 Too few qtvs => too many wanteds, which is what happens if you do less
1031 tcSimplifyRestricted -- Used for restricted binding groups
1032 -- i.e. ones subject to the monomorphism restriction
1035 -> [Name] -- Things bound in this group
1036 -> TcTyVarSet -- Free in the type of the RHSs
1037 -> [Inst] -- Free in the RHSs
1038 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1039 TcDictBinds) -- Bindings
1040 -- tcSimpifyRestricted returns no constraints to
1041 -- quantify over; by definition there are none.
1042 -- They are all thrown back in the LIE
1044 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1045 -- Zonk everything in sight
1046 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1047 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1048 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1050 -- 'reduceMe': Reduce as far as we can. Don't stop at
1051 -- dicts; the idea is to get rid of as many type
1052 -- variables as possible, and we don't want to stop
1053 -- at (say) Monad (ST s), because that reduces
1054 -- immediately, with no constraint on s.
1056 -- BUT do no improvement! See Plan D above
1057 reduceContextWithoutImprovement
1058 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1060 -- Next, figure out the tyvars we will quantify over
1062 constrained_tvs = tyVarsOfInsts constrained_dicts
1063 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1064 `minusVarSet` constrained_tvs
1066 traceTc (text "tcSimplifyRestricted" <+> vcat [
1067 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1069 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1071 -- The first step may have squashed more methods than
1072 -- necessary, so try again, this time more gently, knowing the exact
1073 -- set of type variables to quantify over.
1075 -- We quantify only over constraints that are captured by qtvs;
1076 -- these will just be a subset of non-dicts. This in contrast
1077 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1078 -- all *non-inheritable* constraints too. This implements choice
1079 -- (B) under "implicit parameter and monomorphism" above.
1081 -- Remember that we may need to do *some* simplification, to
1082 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1083 -- just to float all constraints
1085 -- At top level, we *do* squash methods becuase we want to
1086 -- expose implicit parameters to the test that follows
1088 is_nested_group = isNotTopLevel top_lvl
1089 try_me inst | isFreeWrtTyVars qtvs inst,
1090 (is_nested_group || isDict inst) = Free
1091 | otherwise = ReduceMe AddSCs
1093 reduceContextWithoutImprovement
1094 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1095 ASSERT( null irreds )
1097 -- See "Notes on implicit parameters, Question 4: top level"
1098 if is_nested_group then
1099 extendLIEs frees `thenM_`
1100 returnM (varSetElems qtvs, binds)
1103 (non_ips, bad_ips) = partition isClassDict frees
1105 addTopIPErrs bndrs bad_ips `thenM_`
1106 extendLIEs non_ips `thenM_`
1107 returnM (varSetElems qtvs, binds)
1111 %************************************************************************
1113 \subsection{tcSimplifyToDicts}
1115 %************************************************************************
1117 On the LHS of transformation rules we only simplify methods and constants,
1118 getting dictionaries. We want to keep all of them unsimplified, to serve
1119 as the available stuff for the RHS of the rule.
1121 The same thing is used for specialise pragmas. Consider
1123 f :: Num a => a -> a
1124 {-# SPECIALISE f :: Int -> Int #-}
1127 The type checker generates a binding like:
1129 f_spec = (f :: Int -> Int)
1131 and we want to end up with
1133 f_spec = _inline_me_ (f Int dNumInt)
1135 But that means that we must simplify the Method for f to (f Int dNumInt)!
1136 So tcSimplifyToDicts squeezes out all Methods.
1138 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
1140 fromIntegral :: (Integral a, Num b) => a -> b
1141 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1143 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
1146 forall dIntegralInt.
1147 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1149 because the scsel will mess up RULE matching. Instead we want
1151 forall dIntegralInt, dNumInt.
1152 fromIntegral Int Int dIntegralInt dNumInt = id Int
1157 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
1158 tcSimplifyToDicts wanteds
1159 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1160 -- Since try_me doesn't look at types, we don't need to
1161 -- do any zonking, so it's safe to call reduceContext directly
1162 ASSERT( null frees )
1163 extendLIEs irreds `thenM_`
1167 doc = text "tcSimplifyToDicts"
1169 -- Reduce methods and lits only; stop as soon as we get a dictionary
1170 try_me inst | isDict inst = KeepDictWithoutSCs -- See notes above re "WithoutSCs"
1171 | otherwise = ReduceMe NoSCs
1176 tcSimplifyBracket is used when simplifying the constraints arising from
1177 a Template Haskell bracket [| ... |]. We want to check that there aren't
1178 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1179 Show instance), but we aren't otherwise interested in the results.
1180 Nor do we care about ambiguous dictionaries etc. We will type check
1181 this bracket again at its usage site.
1184 tcSimplifyBracket :: [Inst] -> TcM ()
1185 tcSimplifyBracket wanteds
1186 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1189 doc = text "tcSimplifyBracket"
1193 %************************************************************************
1195 \subsection{Filtering at a dynamic binding}
1197 %************************************************************************
1202 we must discharge all the ?x constraints from B. We also do an improvement
1203 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1205 Actually, the constraints from B might improve the types in ?x. For example
1207 f :: (?x::Int) => Char -> Char
1210 then the constraint (?x::Int) arising from the call to f will
1211 force the binding for ?x to be of type Int.
1214 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1217 tcSimplifyIPs given_ips wanteds
1218 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1219 extendLIEs frees `thenM_`
1222 doc = text "tcSimplifyIPs" <+> ppr given_ips
1223 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1225 -- Simplify any methods that mention the implicit parameter
1226 try_me inst | isFreeWrtIPs ip_set inst = Free
1227 | otherwise = ReduceMe NoSCs
1229 simpl_loop givens wanteds
1230 = mappM zonkInst givens `thenM` \ givens' ->
1231 mappM zonkInst wanteds `thenM` \ wanteds' ->
1233 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1235 if no_improvement then
1236 ASSERT( null irreds )
1237 returnM (frees, binds)
1239 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1240 returnM (frees1, binds `unionBags` binds1)
1244 %************************************************************************
1246 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1248 %************************************************************************
1250 When doing a binding group, we may have @Insts@ of local functions.
1251 For example, we might have...
1253 let f x = x + 1 -- orig local function (overloaded)
1254 f.1 = f Int -- two instances of f
1259 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1260 where @f@ is in scope; those @Insts@ must certainly not be passed
1261 upwards towards the top-level. If the @Insts@ were binding-ified up
1262 there, they would have unresolvable references to @f@.
1264 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1265 For each method @Inst@ in the @init_lie@ that mentions one of the
1266 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1267 @LIE@), as well as the @HsBinds@ generated.
1270 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1271 -- Simlifies only MethodInsts, and generate only bindings of form
1273 -- We're careful not to even generate bindings of the form
1275 -- You'd think that'd be fine, but it interacts with what is
1276 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1278 bindInstsOfLocalFuns wanteds local_ids
1279 | null overloaded_ids
1281 = extendLIEs wanteds `thenM_`
1282 returnM emptyLHsBinds
1285 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1286 ASSERT( null irreds )
1287 extendLIEs not_for_me `thenM_`
1288 extendLIEs frees `thenM_`
1291 doc = text "bindInsts" <+> ppr local_ids
1292 overloaded_ids = filter is_overloaded local_ids
1293 is_overloaded id = isOverloadedTy (idType id)
1294 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1296 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1297 -- so it's worth building a set, so that
1298 -- lookup (in isMethodFor) is faster
1299 try_me inst | isMethod inst = ReduceMe NoSCs
1304 %************************************************************************
1306 \subsection{Data types for the reduction mechanism}
1308 %************************************************************************
1310 The main control over context reduction is here
1314 = ReduceMe WantSCs -- Try to reduce this
1315 -- If there's no instance, behave exactly like
1316 -- DontReduce: add the inst to
1317 -- the irreductible ones, but don't
1318 -- produce an error message of any kind.
1319 -- It might be quite legitimate such as (Eq a)!
1321 | KeepDictWithoutSCs -- Return as irreducible; don't add its superclasses
1322 -- Rather specialised: see notes with tcSimplifyToDicts
1324 | DontReduceUnlessConstant -- Return as irreducible unless it can
1325 -- be reduced to a constant in one step
1327 | Free -- Return as free
1329 reduceMe :: Inst -> WhatToDo
1330 reduceMe inst = ReduceMe AddSCs
1332 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1333 -- of a predicate when adding it to the avails
1339 type Avails = FiniteMap Inst Avail
1340 emptyAvails = emptyFM
1343 = IsFree -- Used for free Insts
1344 | Irred -- Used for irreducible dictionaries,
1345 -- which are going to be lambda bound
1347 | Given TcId -- Used for dictionaries for which we have a binding
1348 -- e.g. those "given" in a signature
1349 Bool -- True <=> actually consumed (splittable IPs only)
1351 | NoRhs -- Used for Insts like (CCallable f)
1352 -- where no witness is required.
1355 | Rhs -- Used when there is a RHS
1356 (LHsExpr TcId) -- The RHS
1357 [Inst] -- Insts free in the RHS; we need these too
1359 | Linear -- Splittable Insts only.
1360 Int -- The Int is always 2 or more; indicates how
1361 -- many copies are required
1362 Inst -- The splitter
1363 Avail -- Where the "master copy" is
1365 | LinRhss -- Splittable Insts only; this is used only internally
1366 -- by extractResults, where a Linear
1367 -- is turned into an LinRhss
1368 [LHsExpr TcId] -- A supply of suitable RHSs
1370 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1371 | (inst,avail) <- fmToList avails ]
1373 instance Outputable Avail where
1376 pprAvail NoRhs = text "<no rhs>"
1377 pprAvail IsFree = text "Free"
1378 pprAvail Irred = text "Irred"
1379 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1380 if b then text "(used)" else empty
1381 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1382 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1383 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1386 Extracting the bindings from a bunch of Avails.
1387 The bindings do *not* come back sorted in dependency order.
1388 We assume that they'll be wrapped in a big Rec, so that the
1389 dependency analyser can sort them out later
1393 extractResults :: Avails
1395 -> TcM (TcDictBinds, -- Bindings
1396 [Inst], -- Irreducible ones
1397 [Inst]) -- Free ones
1399 extractResults avails wanteds
1400 = go avails emptyBag [] [] wanteds
1402 go avails binds irreds frees []
1403 = returnM (binds, irreds, frees)
1405 go avails binds irreds frees (w:ws)
1406 = case lookupFM avails w of
1407 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1408 go avails binds irreds frees ws
1410 Just NoRhs -> go avails binds irreds frees ws
1411 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1412 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1414 Just (Given id _) -> go avails new_binds irreds frees ws
1416 new_binds | id == instToId w = binds
1417 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1418 -- The sought Id can be one of the givens, via a superclass chain
1419 -- and then we definitely don't want to generate an x=x binding!
1421 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1423 new_binds = addBind binds w rhs
1425 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1426 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1427 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1428 go (addToFM avails w (LinRhss rhss))
1429 (binds `unionBags` binds')
1430 irreds' frees' (split_inst : w : ws)
1432 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1433 -> go new_avails new_binds irreds frees ws
1435 new_binds = addBind binds w rhs
1436 new_avails = addToFM avails w (LinRhss rhss)
1438 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1439 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1440 returnM (w':irreds, frees, instToId w')
1441 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1442 returnM (irreds, w':frees, instToId w')
1445 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1446 | otherwise = addToFM avails w NoRhs
1447 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1448 -- than Given, else we end up with bogus bindings.
1450 add_free avails w | isMethod w = avails
1451 | otherwise = add_given avails w
1453 -- Do *not* replace Free by Given if it's a method.
1454 -- The following situation shows why this is bad:
1455 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1456 -- From an application (truncate f i) we get
1457 -- t1 = truncate at f
1459 -- If we have also have a second occurrence of truncate, we get
1460 -- t3 = truncate at f
1462 -- When simplifying with i,f free, we might still notice that
1463 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1464 -- will continue to float out!
1465 -- (split n i a) returns: n rhss
1466 -- auxiliary bindings
1467 -- 1 or 0 insts to add to irreds
1470 split :: Int -> TcId -> TcId -> Inst
1471 -> TcM (TcDictBinds, [LHsExpr TcId])
1472 -- (split n split_id root_id wanted) returns
1473 -- * a list of 'n' expressions, all of which witness 'avail'
1474 -- * a bunch of auxiliary bindings to support these expressions
1475 -- * one or zero insts needed to witness the whole lot
1476 -- (maybe be zero if the initial Inst is a Given)
1478 -- NB: 'wanted' is just a template
1480 split n split_id root_id wanted
1483 ty = linearInstType wanted
1484 pair_ty = mkTyConApp pairTyCon [ty,ty]
1485 id = instToId wanted
1488 span = instSpan wanted
1490 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1492 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1493 expand n rhss `thenM` \ (binds2, rhss') ->
1494 returnM (binds1 `unionBags` binds2, rhss')
1497 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1498 -- e.g. expand 3 [rhs1, rhs2]
1499 -- = ( { x = split rhs1 },
1500 -- [fst x, snd x, rhs2] )
1502 | n `rem` 2 == 0 = go rhss -- n is even
1503 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1504 returnM (binds', head rhss : rhss')
1506 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1507 returnM (listToBag binds', concat rhss')
1509 do_one rhs = newUnique `thenM` \ uniq ->
1510 tcLookupId fstName `thenM` \ fst_id ->
1511 tcLookupId sndName `thenM` \ snd_id ->
1513 x = mkUserLocal occ uniq pair_ty loc
1515 returnM (L span (VarBind x (mk_app span split_id rhs)),
1516 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1518 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1520 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1522 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1523 (VarBind (instToId inst) rhs))
1524 instSpan wanted = instLocSrcSpan (instLoc wanted)
1528 %************************************************************************
1530 \subsection[reduce]{@reduce@}
1532 %************************************************************************
1534 When the "what to do" predicate doesn't depend on the quantified type variables,
1535 matters are easier. We don't need to do any zonking, unless the improvement step
1536 does something, in which case we zonk before iterating.
1538 The "given" set is always empty.
1541 simpleReduceLoop :: SDoc
1542 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1544 -> TcM ([Inst], -- Free
1546 [Inst]) -- Irreducible
1548 simpleReduceLoop doc try_me wanteds
1549 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1550 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1551 if no_improvement then
1552 returnM (frees, binds, irreds)
1554 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1555 returnM (frees1, binds `unionBags` binds1, irreds1)
1561 reduceContext :: SDoc
1562 -> (Inst -> WhatToDo)
1565 -> TcM (Bool, -- True <=> improve step did no unification
1567 TcDictBinds, -- Dictionary bindings
1568 [Inst]) -- Irreducible
1570 reduceContext doc try_me givens wanteds
1572 traceTc (text "reduceContext" <+> (vcat [
1573 text "----------------------",
1575 text "given" <+> ppr givens,
1576 text "wanted" <+> ppr wanteds,
1577 text "----------------------"
1580 -- Build the Avail mapping from "givens"
1581 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1584 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1586 -- Do improvement, using everything in avails
1587 -- In particular, avails includes all superclasses of everything
1588 tcImprove avails `thenM` \ no_improvement ->
1590 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1592 traceTc (text "reduceContext end" <+> (vcat [
1593 text "----------------------",
1595 text "given" <+> ppr givens,
1596 text "wanted" <+> ppr wanteds,
1598 text "avails" <+> pprAvails avails,
1599 text "frees" <+> ppr frees,
1600 text "no_improvement =" <+> ppr no_improvement,
1601 text "----------------------"
1604 returnM (no_improvement, frees, binds, irreds)
1606 -- reduceContextWithoutImprovement differs from reduceContext
1607 -- (a) no improvement
1608 -- (b) 'givens' is assumed empty
1609 reduceContextWithoutImprovement doc try_me wanteds
1611 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1612 text "----------------------",
1614 text "wanted" <+> ppr wanteds,
1615 text "----------------------"
1619 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1620 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1622 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1623 text "----------------------",
1625 text "wanted" <+> ppr wanteds,
1627 text "avails" <+> pprAvails avails,
1628 text "frees" <+> ppr frees,
1629 text "----------------------"
1632 returnM (frees, binds, irreds)
1634 tcImprove :: Avails -> TcM Bool -- False <=> no change
1635 -- Perform improvement using all the predicates in Avails
1637 = tcGetInstEnvs `thenM` \ inst_envs ->
1639 preds = [ (pred, pp_loc)
1640 | (inst, avail) <- fmToList avails,
1641 pred <- get_preds inst avail,
1642 let pp_loc = pprInstLoc (instLoc inst)
1644 -- Avails has all the superclasses etc (good)
1645 -- It also has all the intermediates of the deduction (good)
1646 -- It does not have duplicates (good)
1647 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1648 -- so that improve will see them separate
1650 -- For free Methods, we want to take predicates from their context,
1651 -- but for Methods that have been squished their context will already
1652 -- be in Avails, and we don't want duplicates. Hence this rather
1653 -- horrid get_preds function
1654 get_preds inst IsFree = fdPredsOfInst inst
1655 get_preds inst other | isDict inst = [dictPred inst]
1658 eqns = improve get_insts preds
1659 get_insts clas = classInstances inst_envs clas
1664 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1665 mappM_ unify eqns `thenM_`
1668 unify ((qtvs, pairs), doc)
1670 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1671 mapM_ (unif_pr tenv) pairs
1672 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1675 The main context-reduction function is @reduce@. Here's its game plan.
1678 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1679 -- along with its depth
1680 -> (Inst -> WhatToDo)
1687 try_me: given an inst, this function returns
1689 DontReduce return this in "irreds"
1690 Free return this in "frees"
1692 wanteds: The list of insts to reduce
1693 state: An accumulating parameter of type Avails
1694 that contains the state of the algorithm
1696 It returns a Avails.
1698 The (n,stack) pair is just used for error reporting.
1699 n is always the depth of the stack.
1700 The stack is the stack of Insts being reduced: to produce X
1701 I had to produce Y, to produce Y I had to produce Z, and so on.
1704 reduceList (n,stack) try_me wanteds state
1705 | n > opt_MaxContextReductionDepth
1706 = failWithTc (reduceDepthErr n stack)
1712 pprTrace "Interesting! Context reduction stack deeper than 8:"
1713 (nest 2 (pprStack stack))
1718 go [] state = returnM state
1719 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1722 -- Base case: we're done!
1723 reduce stack try_me wanted avails
1724 -- It's the same as an existing inst, or a superclass thereof
1725 | Just avail <- isAvailable avails wanted
1726 = if isLinearInst wanted then
1727 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1728 reduceList stack try_me wanteds' avails'
1730 returnM avails -- No op for non-linear things
1733 = case try_me wanted of {
1735 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1737 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1738 -- First, see if the inst can be reduced to a constant in one step
1739 try_simple (addIrred AddSCs) -- Assume want superclasses
1741 ; Free -> -- It's free so just chuck it upstairs
1742 -- First, see if the inst can be reduced to a constant in one step
1745 ; ReduceMe want_scs -> -- It should be reduced
1746 lookupInst wanted `thenM` \ lookup_result ->
1747 case lookup_result of
1748 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1749 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1750 addWanted want_scs avails2 wanted rhs wanteds'
1751 -- Experiment with temporarily doing addIrred *before* the reduceList,
1752 -- which has the effect of adding the thing we are trying
1753 -- to prove to the database before trying to prove the things it
1754 -- needs. See note [RECURSIVE DICTIONARIES]
1755 -- NB: we must not do an addWanted before, because that adds the
1756 -- superclasses too, and thaat can lead to a spurious loop; see
1757 -- the examples in [SUPERCLASS-LOOP]
1758 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1760 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1762 NoInstance -> -- No such instance!
1763 -- Add it and its superclasses
1764 addIrred want_scs avails wanted
1767 try_simple do_this_otherwise
1768 = lookupInst wanted `thenM` \ lookup_result ->
1769 case lookup_result of
1770 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1771 other -> do_this_otherwise avails wanted
1776 -------------------------
1777 isAvailable :: Avails -> Inst -> Maybe Avail
1778 isAvailable avails wanted = lookupFM avails wanted
1779 -- NB 1: the Ord instance of Inst compares by the class/type info
1780 -- *not* by unique. So
1781 -- d1::C Int == d2::C Int
1783 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1784 addLinearAvailable avails avail wanted
1785 -- avails currently maps [wanted -> avail]
1786 -- Extend avails to reflect a neeed for an extra copy of avail
1788 | Just avail' <- split_avail avail
1789 = returnM (addToFM avails wanted avail', [])
1792 = tcLookupId splitName `thenM` \ split_id ->
1793 tcInstClassOp (instLoc wanted) split_id
1794 [linearInstType wanted] `thenM` \ split_inst ->
1795 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1798 split_avail :: Avail -> Maybe Avail
1799 -- (Just av) if there's a modified version of avail that
1800 -- we can use to replace avail in avails
1801 -- Nothing if there isn't, so we need to create a Linear
1802 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1803 split_avail (Given id used) | not used = Just (Given id True)
1804 | otherwise = Nothing
1805 split_avail Irred = Nothing
1806 split_avail IsFree = Nothing
1807 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1809 -------------------------
1810 addFree :: Avails -> Inst -> TcM Avails
1811 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1812 -- to avails, so that any other equal Insts will be commoned up right
1813 -- here rather than also being tossed upstairs. This is really just
1814 -- an optimisation, and perhaps it is more trouble that it is worth,
1815 -- as the following comments show!
1817 -- NB: do *not* add superclasses. If we have
1820 -- but a is not bound here, then we *don't* want to derive
1821 -- dn from df here lest we lose sharing.
1823 addFree avails free = returnM (addToFM avails free IsFree)
1825 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1826 addWanted want_scs avails wanted rhs_expr wanteds
1827 = addAvailAndSCs want_scs avails wanted avail
1829 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1830 | otherwise = ASSERT( null wanteds ) NoRhs
1832 addGiven :: Avails -> Inst -> TcM Avails
1833 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1834 -- Always add superclasses for 'givens'
1836 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1837 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1838 -- so the assert isn't true
1840 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1841 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1842 addAvailAndSCs want_scs avails irred Irred
1844 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1845 addAvailAndSCs want_scs avails inst avail
1846 | not (isClassDict inst) = return avails_with_inst
1847 | NoSCs <- want_scs = return avails_with_inst
1848 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1849 ; addSCs is_loop avails_with_inst inst }
1851 avails_with_inst = addToFM avails inst avail
1853 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1854 -- Note: this compares by *type*, not by Unique
1855 deps = findAllDeps (unitVarSet (instToId inst)) avail
1856 dep_tys = map idType (varSetElems deps)
1858 findAllDeps :: IdSet -> Avail -> IdSet
1859 -- Find all the Insts that this one depends on
1860 -- See Note [SUPERCLASS-LOOP]
1861 -- Watch out, though. Since the avails may contain loops
1862 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1863 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1864 findAllDeps so_far other = so_far
1866 find_all :: IdSet -> Inst -> IdSet
1868 | kid_id `elemVarSet` so_far = so_far
1869 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1870 | otherwise = so_far'
1872 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1873 kid_id = instToId kid
1875 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1876 -- Add all the superclasses of the Inst to Avails
1877 -- The first param says "dont do this because the original thing
1878 -- depends on this one, so you'd build a loop"
1879 -- Invariant: the Inst is already in Avails.
1881 addSCs is_loop avails dict
1882 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1883 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1885 (clas, tys) = getDictClassTys dict
1886 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1887 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1889 add_sc avails (sc_dict, sc_sel)
1890 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1891 | is_given sc_dict = return avails
1892 | otherwise = addSCs is_loop avails' sc_dict
1894 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1895 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1897 is_given :: Inst -> Bool
1898 is_given sc_dict = case lookupFM avails sc_dict of
1899 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1903 Note [SUPERCLASS-LOOP 2]
1904 ~~~~~~~~~~~~~~~~~~~~~~~~
1905 But the above isn't enough. Suppose we are *given* d1:Ord a,
1906 and want to deduce (d2:C [a]) where
1908 class Ord a => C a where
1909 instance Ord [a] => C [a] where ...
1911 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1912 superclasses of C [a] to avails. But we must not overwrite the binding
1913 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1916 Here's another variant, immortalised in tcrun020
1917 class Monad m => C1 m
1918 class C1 m => C2 m x
1919 instance C2 Maybe Bool
1920 For the instance decl we need to build (C1 Maybe), and it's no good if
1921 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1922 before we search for C1 Maybe.
1924 Here's another example
1925 class Eq b => Foo a b
1926 instance Eq a => Foo [a] a
1930 we'll first deduce that it holds (via the instance decl). We must not
1931 then overwrite the Eq t constraint with a superclass selection!
1933 At first I had a gross hack, whereby I simply did not add superclass constraints
1934 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1935 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1936 I found a very obscure program (now tcrun021) in which improvement meant the
1937 simplifier got two bites a the cherry... so something seemed to be an Irred
1938 first time, but reducible next time.
1940 Now we implement the Right Solution, which is to check for loops directly
1941 when adding superclasses. It's a bit like the occurs check in unification.
1944 Note [RECURSIVE DICTIONARIES]
1945 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1947 data D r = ZeroD | SuccD (r (D r));
1949 instance (Eq (r (D r))) => Eq (D r) where
1950 ZeroD == ZeroD = True
1951 (SuccD a) == (SuccD b) = a == b
1954 equalDC :: D [] -> D [] -> Bool;
1957 We need to prove (Eq (D [])). Here's how we go:
1961 by instance decl, holds if
1965 by instance decl of Eq, holds if
1967 where d2 = dfEqList d3
1970 But now we can "tie the knot" to give
1976 and it'll even run! The trick is to put the thing we are trying to prove
1977 (in this case Eq (D []) into the database before trying to prove its
1978 contributing clauses.
1981 %************************************************************************
1983 \section{tcSimplifyTop: defaulting}
1985 %************************************************************************
1988 @tcSimplifyTop@ is called once per module to simplify all the constant
1989 and ambiguous Insts.
1991 We need to be careful of one case. Suppose we have
1993 instance Num a => Num (Foo a b) where ...
1995 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1996 to (Num x), and default x to Int. But what about y??
1998 It's OK: the final zonking stage should zap y to (), which is fine.
2002 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2003 tcSimplifyTop wanteds
2004 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2006 doc = text "tcSimplifyTop"
2008 tcSimplifyInteractive wanteds
2009 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2011 doc = text "tcSimplifyTop"
2013 -- The TcLclEnv should be valid here, solely to improve
2014 -- error message generation for the monomorphism restriction
2015 tc_simplify_top doc is_interactive want_scs wanteds
2016 = do { lcl_env <- getLclEnv
2017 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2019 ; let try_me inst = ReduceMe want_scs
2020 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2023 -- All the non-std ones are definite errors
2024 (stds, non_stds) = partition isStdClassTyVarDict irreds
2026 -- Group by type variable
2027 std_groups = equivClasses cmp_by_tyvar stds
2029 -- Pick the ones which its worth trying to disambiguate
2030 -- namely, the onese whose type variable isn't bound
2031 -- up with one of the non-standard classes
2032 (std_oks, std_bads) = partition worth_a_try std_groups
2033 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
2034 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
2036 -- Collect together all the bad guys
2037 bad_guys = non_stds ++ concat std_bads
2038 (non_ips, bad_ips) = partition isClassDict bad_guys
2039 (ambigs, no_insts) = partition isTyVarDict non_ips
2040 -- If the dict has no type constructors involved, it must be ambiguous,
2041 -- except I suppose that another error with fundeps maybe should have
2042 -- constrained those type variables
2044 -- Report definite errors
2045 ; ASSERT( null frees )
2046 groupErrs (addNoInstanceErrs Nothing []) no_insts
2047 ; strangeTopIPErrs bad_ips
2049 -- Deal with ambiguity errors, but only if
2050 -- if there has not been an error so far:
2051 -- errors often give rise to spurious ambiguous Insts.
2053 -- f = (*) -- Monomorphic
2054 -- g :: Num a => a -> a
2056 -- Here, we get a complaint when checking the type signature for g,
2057 -- that g isn't polymorphic enough; but then we get another one when
2058 -- dealing with the (Num a) context arising from f's definition;
2059 -- we try to unify a with Int (to default it), but find that it's
2060 -- already been unified with the rigid variable from g's type sig
2061 ; binds_ambig <- ifErrsM (returnM []) $
2062 do { -- Complain about the ones that don't fall under
2063 -- the Haskell rules for disambiguation
2064 -- This group includes both non-existent instances
2065 -- e.g. Num (IO a) and Eq (Int -> Int)
2066 -- and ambiguous dictionaries
2068 addTopAmbigErrs ambigs
2070 -- Disambiguate the ones that look feasible
2071 ; mappM (disambigGroup is_interactive) std_oks }
2073 ; return (binds `unionBags` unionManyBags binds_ambig) }
2075 ----------------------------------
2076 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2078 get_tv d = case getDictClassTys d of
2079 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2080 get_clas d = case getDictClassTys d of
2081 (clas, [ty]) -> clas
2084 If a dictionary constrains a type variable which is
2085 * not mentioned in the environment
2086 * and not mentioned in the type of the expression
2087 then it is ambiguous. No further information will arise to instantiate
2088 the type variable; nor will it be generalised and turned into an extra
2089 parameter to a function.
2091 It is an error for this to occur, except that Haskell provided for
2092 certain rules to be applied in the special case of numeric types.
2094 * at least one of its classes is a numeric class, and
2095 * all of its classes are numeric or standard
2096 then the type variable can be defaulted to the first type in the
2097 default-type list which is an instance of all the offending classes.
2099 So here is the function which does the work. It takes the ambiguous
2100 dictionaries and either resolves them (producing bindings) or
2101 complains. It works by splitting the dictionary list by type
2102 variable, and using @disambigOne@ to do the real business.
2104 @disambigOne@ assumes that its arguments dictionaries constrain all
2105 the same type variable.
2107 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2108 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2109 the most common use of defaulting is code like:
2111 _ccall_ foo `seqPrimIO` bar
2113 Since we're not using the result of @foo@, the result if (presumably)
2117 disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
2118 -> [Inst] -- All standard classes of form (C a)
2121 disambigGroup is_interactive dicts
2122 | any std_default_class classes -- Guaranteed all standard classes
2123 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2124 -- SO, TRY DEFAULT TYPES IN ORDER
2126 -- Failure here is caused by there being no type in the
2127 -- default list which can satisfy all the ambiguous classes.
2128 -- For example, if Real a is reqd, but the only type in the
2129 -- default list is Int.
2130 get_default_tys `thenM` \ default_tys ->
2132 try_default [] -- No defaults work, so fail
2135 try_default (default_ty : default_tys)
2136 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2137 -- default_tys instead
2138 tcSimplifyDefault theta `thenM` \ _ ->
2141 theta = [mkClassPred clas [default_ty] | clas <- classes]
2143 -- See if any default works
2144 tryM (try_default default_tys) `thenM` \ mb_ty ->
2147 Right chosen_default_ty -> choose_default chosen_default_ty
2149 | otherwise -- No defaults
2153 tyvar = get_tv (head dicts) -- Should be non-empty
2154 classes = map get_clas dicts
2156 std_default_class cls
2157 = isNumericClass cls
2158 || (is_interactive &&
2159 classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2160 -- In interactive mode, we default Show a to Show ()
2161 -- to avoid graututious errors on "show []"
2163 choose_default default_ty -- Commit to tyvar = default_ty
2164 = -- Bind the type variable
2165 unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
2166 -- and reduce the context, for real this time
2167 simpleReduceLoop (text "disambig" <+> ppr dicts)
2168 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2169 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2170 warnDefault dicts default_ty `thenM_`
2173 bomb_out = addTopAmbigErrs dicts `thenM_`
2177 = do { mb_defaults <- getDefaultTys
2178 ; case mb_defaults of
2179 Just tys -> return tys
2180 Nothing -> -- No use-supplied default;
2181 -- use [Integer, Double]
2182 do { integer_ty <- tcMetaTy integerTyConName
2183 ; return [integer_ty, doubleTy] } }
2186 [Aside - why the defaulting mechanism is turned off when
2187 dealing with arguments and results to ccalls.
2189 When typechecking _ccall_s, TcExpr ensures that the external
2190 function is only passed arguments (and in the other direction,
2191 results) of a restricted set of 'native' types. This is
2192 implemented via the help of the pseudo-type classes,
2193 @CReturnable@ (CR) and @CCallable@ (CC.)
2195 The interaction between the defaulting mechanism for numeric
2196 values and CC & CR can be a bit puzzling to the user at times.
2205 What type has 'x' got here? That depends on the default list
2206 in operation, if it is equal to Haskell 98's default-default
2207 of (Integer, Double), 'x' has type Double, since Integer
2208 is not an instance of CR. If the default list is equal to
2209 Haskell 1.4's default-default of (Int, Double), 'x' has type
2212 To try to minimise the potential for surprises here, the
2213 defaulting mechanism is turned off in the presence of
2214 CCallable and CReturnable.
2219 %************************************************************************
2221 \subsection[simple]{@Simple@ versions}
2223 %************************************************************************
2225 Much simpler versions when there are no bindings to make!
2227 @tcSimplifyThetas@ simplifies class-type constraints formed by
2228 @deriving@ declarations and when specialising instances. We are
2229 only interested in the simplified bunch of class/type constraints.
2231 It simplifies to constraints of the form (C a b c) where
2232 a,b,c are type variables. This is required for the context of
2233 instance declarations.
2236 tcSimplifyDeriv :: [TyVar]
2237 -> ThetaType -- Wanted
2238 -> TcM ThetaType -- Needed
2240 tcSimplifyDeriv tyvars theta
2241 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2242 -- The main loop may do unification, and that may crash if
2243 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2244 -- ToDo: what if two of them do get unified?
2245 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2246 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2247 ASSERT( null frees ) -- reduceMe never returns Free
2249 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2251 tv_set = mkVarSet tvs
2253 (bad_insts, ok_insts) = partition is_bad_inst irreds
2255 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2256 in isEmptyVarSet (tyVarsOfPred pred)
2257 -- Things like (Eq T) are bad
2258 || (not undecidable_ok && not (isTyVarClassPred pred))
2259 -- The returned dictionaries should be of form (C a b)
2260 -- (where a, b are type variables).
2261 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
2262 -- but note that risks non-termination in the 'deriving' context-inference
2263 -- fixpoint loop. It is useful for situations like
2264 -- data Min h a = E | M a (h a)
2265 -- which gives the instance decl
2266 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
2268 simpl_theta = map dictPred ok_insts
2269 weird_preds = [pred | pred <- simpl_theta
2270 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2271 -- Check for a bizarre corner case, when the derived instance decl should
2272 -- have form instance C a b => D (T a) where ...
2273 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2274 -- of problems; in particular, it's hard to compare solutions for
2275 -- equality when finding the fixpoint. So I just rule it out for now.
2277 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2278 -- This reverse-mapping is a Royal Pain,
2279 -- but the result should mention TyVars not TcTyVars
2282 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2283 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2284 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2285 returnM (substTheta rev_env simpl_theta)
2287 doc = ptext SLIT("deriving classes for a data type")
2290 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2291 used with \tr{default} declarations. We are only interested in
2292 whether it worked or not.
2295 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2298 tcSimplifyDefault theta
2299 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2300 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2301 ASSERT( null frees ) -- try_me never returns Free
2302 addNoInstanceErrs Nothing [] irreds `thenM_`
2308 doc = ptext SLIT("default declaration")
2312 %************************************************************************
2314 \section{Errors and contexts}
2316 %************************************************************************
2318 ToDo: for these error messages, should we note the location as coming
2319 from the insts, or just whatever seems to be around in the monad just
2323 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2324 -> [Inst] -- The offending Insts
2326 -- Group together insts with the same origin
2327 -- We want to report them together in error messages
2329 groupErrs report_err []
2331 groupErrs report_err (inst:insts)
2332 = do_one (inst:friends) `thenM_`
2333 groupErrs report_err others
2336 -- (It may seem a bit crude to compare the error messages,
2337 -- but it makes sure that we combine just what the user sees,
2338 -- and it avoids need equality on InstLocs.)
2339 (friends, others) = partition is_friend insts
2340 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2341 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2342 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2343 -- Add location and context information derived from the Insts
2345 -- Add the "arising from..." part to a message about bunch of dicts
2346 addInstLoc :: [Inst] -> Message -> Message
2347 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2350 plural xs = char 's'
2352 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2353 addTopIPErrs bndrs []
2355 addTopIPErrs bndrs ips
2356 = addErrTcM (tidy_env, mk_msg tidy_ips)
2358 (tidy_env, tidy_ips) = tidyInsts ips
2359 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
2360 pprBinders bndrs <> colon],
2361 nest 2 (vcat (map ppr_ip ips)),
2363 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2365 strangeTopIPErrs :: [Inst] -> TcM ()
2366 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2367 = groupErrs report tidy_dicts
2369 (tidy_env, tidy_dicts) = tidyInsts dicts
2370 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2371 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2372 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2374 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2375 -- Just d => d describes the construct
2376 -> [Inst] -- What is given by the context or type sig
2377 -> [Inst] -- What is wanted
2379 addNoInstanceErrs mb_what givens []
2381 addNoInstanceErrs mb_what givens dicts
2382 = -- Some of the dicts are here because there is no instances
2383 -- and some because there are too many instances (overlap)
2384 getDOpts `thenM` \ dflags ->
2385 tcGetInstEnvs `thenM` \ inst_envs ->
2387 (tidy_env1, tidy_givens) = tidyInsts givens
2388 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2390 -- Run through the dicts, generating a message for each
2391 -- overlapping one, but simply accumulating all the
2392 -- no-instance ones so they can be reported as a group
2393 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2394 check_overlap (overlap_doc, no_inst_dicts) dict
2395 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2397 = case lookupInstEnv dflags inst_envs clas tys of
2398 -- The case of exactly one match and no unifiers means
2399 -- a successful lookup. That can't happen here, becuase
2400 -- dicts only end up here if they didn't match in Inst.lookupInst
2402 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2404 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2405 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2407 (clas,tys) = getDictClassTys dict
2410 -- Now generate a good message for the no-instance bunch
2411 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2413 no_inst_doc | null no_inst_dicts = empty
2414 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2415 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2416 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2417 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2418 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2420 -- And emit both the non-instance and overlap messages
2421 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2423 mk_overlap_msg dict (matches, unifiers)
2424 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2425 <+> pprPred (dictPred dict))),
2426 sep [ptext SLIT("Matching instances") <> colon,
2427 nest 2 (vcat [pprDFuns dfuns, pprDFuns unifiers])],
2428 ASSERT( not (null matches) )
2429 if not (isSingleton matches)
2430 then -- Two or more matches
2432 else -- One match, plus some unifiers
2433 ASSERT( not (null unifiers) )
2434 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2435 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2436 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2438 dfuns = [df | (_, (_,_,df)) <- matches]
2440 mk_probable_fix tidy_env dicts
2441 = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
2443 fixes = add_ors (fix1 ++ fix2)
2445 fix1 = case mb_what of
2446 Nothing -> [] -- Top level
2447 Just what -> -- Nested (type signatures, instance decls)
2448 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2449 ptext SLIT("to the") <+> what] ]
2451 fix2 | null instance_dicts = []
2452 | otherwise = [ ptext SLIT("add an instance declaration for")
2453 <+> pprDictsTheta instance_dicts ]
2454 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2455 -- Insts for which it is worth suggesting an adding an instance declaration
2456 -- Exclude implicit parameters, and tyvar dicts
2458 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2459 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2460 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2462 addTopAmbigErrs dicts
2463 -- Divide into groups that share a common set of ambiguous tyvars
2464 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2466 (tidy_env, tidy_dicts) = tidyInsts dicts
2468 tvs_of :: Inst -> [TcTyVar]
2469 tvs_of d = varSetElems (tyVarsOfInst d)
2470 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2472 report :: [(Inst,[TcTyVar])] -> TcM ()
2473 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2474 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2475 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2476 -- the location of the first one will do for the err message
2477 addErrTcM (tidy_env, msg $$ mono_msg)
2479 dicts = map fst pairs
2480 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2481 pprQuotedList tvs <+> in_msg,
2482 nest 2 (pprDictsInFull dicts)]
2483 in_msg = text "in the constraint" <> plural dicts <> colon
2486 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2487 -- There's an error with these Insts; if they have free type variables
2488 -- it's probably caused by the monomorphism restriction.
2489 -- Try to identify the offending variable
2490 -- ASSUMPTION: the Insts are fully zonked
2491 mkMonomorphismMsg tidy_env inst_tvs
2492 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2493 returnM (tidy_env, mk_msg docs)
2495 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2496 -- This happens in things like
2497 -- f x = show (read "foo")
2498 -- whre monomorphism doesn't play any role
2499 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2503 monomorphism_fix :: SDoc
2504 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2505 (ptext SLIT("give these definition(s) an explicit type signature")
2506 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2508 warnDefault dicts default_ty
2509 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2510 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2513 (_, tidy_dicts) = tidyInsts dicts
2514 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2515 quotes (ppr default_ty),
2516 pprDictsInFull tidy_dicts]
2518 -- Used for the ...Thetas variants; all top level
2520 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2521 ptext SLIT("type variables that are not data type parameters"),
2522 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2524 reduceDepthErr n stack
2525 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2526 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2527 nest 4 (pprStack stack)]
2529 pprStack stack = vcat (map pprInstInFull stack)