2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
15 tcSimplifyDeriv, tcSimplifyDefault,
19 #include "HsVersions.h"
21 import {-# SOURCE #-} TcUnify( unifyTauTy )
23 import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
24 import TcHsSyn ( TcExpr, TcId,
25 TcMonoBinds, TcDictBinds
29 import Inst ( lookupInst, LookupInstResult(..),
30 tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
31 isDict, isClassDict, isLinearInst, linearInstType,
32 isStdClassTyVarDict, isMethodFor, isMethod,
33 instToId, tyVarsOfInsts, cloneDict,
34 ipNamesOfInsts, ipNamesOfInst, dictPred,
35 instBindingRequired, instCanBeGeneralised,
36 newDictsFromOld, tcInstClassOp,
37 getDictClassTys, isTyVarDict,
38 instLoc, zonkInst, tidyInsts, tidyMoreInsts,
39 Inst, pprInsts, pprInstsInFull,
40 isIPDict, isInheritableInst
42 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv, tcLookupId, findGlobals )
43 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
46 mkClassPred, isOverloadedTy, mkTyConApp,
47 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
49 import Id ( idType, mkUserLocal )
51 import Name ( getOccName, getSrcLoc )
52 import NameSet ( NameSet, mkNameSet, elemNameSet )
53 import Class ( classBigSig )
54 import FunDeps ( oclose, grow, improve, pprEquationDoc )
55 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
56 import PrelNames ( splitName, fstName, sndName )
58 import Subst ( mkTopTyVarSubst, substTheta, substTy )
59 import TysWiredIn ( unitTy, pairTyCon )
60 import ErrUtils ( Message )
62 import VarEnv ( TidyEnv )
65 import ListSetOps ( equivClasses )
66 import Util ( zipEqual, isSingleton )
67 import List ( partition )
72 %************************************************************************
76 %************************************************************************
78 --------------------------------------
79 Notes on quantification
80 --------------------------------------
82 Suppose we are about to do a generalisation step.
87 C the constraints from that RHS
89 The game is to figure out
91 Q the set of type variables over which to quantify
92 Ct the constraints we will *not* quantify over
93 Cq the constraints we will quantify over
95 So we're going to infer the type
99 and float the constraints Ct further outwards.
101 Here are the things that *must* be true:
103 (A) Q intersect fv(G) = EMPTY limits how big Q can be
104 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
106 (A) says we can't quantify over a variable that's free in the
107 environment. (B) says we must quantify over all the truly free
108 variables in T, else we won't get a sufficiently general type. We do
109 not *need* to quantify over any variable that is fixed by the free
110 vars of the environment G.
112 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
114 Example: class H x y | x->y where ...
116 fv(G) = {a} C = {H a b, H c d}
119 (A) Q intersect {a} is empty
120 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
122 So Q can be {c,d}, {b,c,d}
124 Other things being equal, however, we'd like to quantify over as few
125 variables as possible: smaller types, fewer type applications, more
126 constraints can get into Ct instead of Cq.
129 -----------------------------------------
132 fv(T) the free type vars of T
134 oclose(vs,C) The result of extending the set of tyvars vs
135 using the functional dependencies from C
137 grow(vs,C) The result of extend the set of tyvars vs
138 using all conceivable links from C.
140 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
141 Then grow(vs,C) = {a,b,c}
143 Note that grow(vs,C) `superset` grow(vs,simplify(C))
144 That is, simplfication can only shrink the result of grow.
147 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
148 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
151 -----------------------------------------
155 Here's a good way to choose Q:
157 Q = grow( fv(T), C ) \ oclose( fv(G), C )
159 That is, quantify over all variable that that MIGHT be fixed by the
160 call site (which influences T), but which aren't DEFINITELY fixed by
161 G. This choice definitely quantifies over enough type variables,
162 albeit perhaps too many.
164 Why grow( fv(T), C ) rather than fv(T)? Consider
166 class H x y | x->y where ...
171 If we used fv(T) = {c} we'd get the type
173 forall c. H c d => c -> b
175 And then if the fn was called at several different c's, each of
176 which fixed d differently, we'd get a unification error, because
177 d isn't quantified. Solution: quantify d. So we must quantify
178 everything that might be influenced by c.
180 Why not oclose( fv(T), C )? Because we might not be able to see
181 all the functional dependencies yet:
183 class H x y | x->y where ...
184 instance H x y => Eq (T x y) where ...
189 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
190 apparent yet, and that's wrong. We must really quantify over d too.
193 There really isn't any point in quantifying over any more than
194 grow( fv(T), C ), because the call sites can't possibly influence
195 any other type variables.
199 --------------------------------------
201 --------------------------------------
203 It's very hard to be certain when a type is ambiguous. Consider
207 instance H x y => K (x,y)
209 Is this type ambiguous?
210 forall a b. (K (a,b), Eq b) => a -> a
212 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
213 now we see that a fixes b. So we can't tell about ambiguity for sure
214 without doing a full simplification. And even that isn't possible if
215 the context has some free vars that may get unified. Urgle!
217 Here's another example: is this ambiguous?
218 forall a b. Eq (T b) => a -> a
219 Not if there's an insance decl (with no context)
220 instance Eq (T b) where ...
222 You may say of this example that we should use the instance decl right
223 away, but you can't always do that:
225 class J a b where ...
226 instance J Int b where ...
228 f :: forall a b. J a b => a -> a
230 (Notice: no functional dependency in J's class decl.)
231 Here f's type is perfectly fine, provided f is only called at Int.
232 It's premature to complain when meeting f's signature, or even
233 when inferring a type for f.
237 However, we don't *need* to report ambiguity right away. It'll always
238 show up at the call site.... and eventually at main, which needs special
239 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
241 So here's the plan. We WARN about probable ambiguity if
243 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
245 (all tested before quantification).
246 That is, all the type variables in Cq must be fixed by the the variables
247 in the environment, or by the variables in the type.
249 Notice that we union before calling oclose. Here's an example:
251 class J a b c | a b -> c
255 forall b c. (J a b c) => b -> b
257 Only if we union {a} from G with {b} from T before using oclose,
258 do we see that c is fixed.
260 It's a bit vague exactly which C we should use for this oclose call. If we
261 don't fix enough variables we might complain when we shouldn't (see
262 the above nasty example). Nothing will be perfect. That's why we can
263 only issue a warning.
266 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
268 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
270 then c is a "bubble"; there's no way it can ever improve, and it's
271 certainly ambiguous. UNLESS it is a constant (sigh). And what about
276 instance H x y => K (x,y)
278 Is this type ambiguous?
279 forall a b. (K (a,b), Eq b) => a -> a
281 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
282 is a "bubble" that's a set of constraints
284 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
286 Hence another idea. To decide Q start with fv(T) and grow it
287 by transitive closure in Cq (no functional dependencies involved).
288 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
289 The definitely-ambiguous can then float out, and get smashed at top level
290 (which squashes out the constants, like Eq (T a) above)
293 --------------------------------------
294 Notes on principal types
295 --------------------------------------
300 f x = let g y = op (y::Int) in True
302 Here the principal type of f is (forall a. a->a)
303 but we'll produce the non-principal type
304 f :: forall a. C Int => a -> a
307 --------------------------------------
308 Notes on implicit parameters
309 --------------------------------------
311 Question 1: can we "inherit" implicit parameters
312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
317 where f is *not* a top-level binding.
318 From the RHS of f we'll get the constraint (?y::Int).
319 There are two types we might infer for f:
323 (so we get ?y from the context of f's definition), or
325 f :: (?y::Int) => Int -> Int
327 At first you might think the first was better, becuase then
328 ?y behaves like a free variable of the definition, rather than
329 having to be passed at each call site. But of course, the WHOLE
330 IDEA is that ?y should be passed at each call site (that's what
331 dynamic binding means) so we'd better infer the second.
333 BOTTOM LINE: when *inferring types* you *must* quantify
334 over implicit parameters. See the predicate isFreeWhenInferring.
337 Question 2: type signatures
338 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
339 BUT WATCH OUT: When you supply a type signature, we can't force you
340 to quantify over implicit parameters. For example:
344 This is perfectly reasonable. We do not want to insist on
346 (?x + 1) :: (?x::Int => Int)
348 That would be silly. Here, the definition site *is* the occurrence site,
349 so the above strictures don't apply. Hence the difference between
350 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
351 and tcSimplifyCheckBind (which does not).
353 What about when you supply a type signature for a binding?
354 Is it legal to give the following explicit, user type
355 signature to f, thus:
360 At first sight this seems reasonable, but it has the nasty property
361 that adding a type signature changes the dynamic semantics.
364 (let f x = (x::Int) + ?y
365 in (f 3, f 3 with ?y=5)) with ?y = 6
371 in (f 3, f 3 with ?y=5)) with ?y = 6
375 Indeed, simply inlining f (at the Haskell source level) would change the
378 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
379 semantics for a Haskell program without knowing its typing, so if you
380 change the typing you may change the semantics.
382 To make things consistent in all cases where we are *checking* against
383 a supplied signature (as opposed to inferring a type), we adopt the
386 a signature does not need to quantify over implicit params.
388 [This represents a (rather marginal) change of policy since GHC 5.02,
389 which *required* an explicit signature to quantify over all implicit
390 params for the reasons mentioned above.]
392 But that raises a new question. Consider
394 Given (signature) ?x::Int
395 Wanted (inferred) ?x::Int, ?y::Bool
397 Clearly we want to discharge the ?x and float the ?y out. But
398 what is the criterion that distinguishes them? Clearly it isn't
399 what free type variables they have. The Right Thing seems to be
400 to float a constraint that
401 neither mentions any of the quantified type variables
402 nor any of the quantified implicit parameters
404 See the predicate isFreeWhenChecking.
407 Question 3: monomorphism
408 ~~~~~~~~~~~~~~~~~~~~~~~~
409 There's a nasty corner case when the monomorphism restriction bites:
413 The argument above suggests that we *must* generalise
414 over the ?y parameter, to get
415 z :: (?y::Int) => Int,
416 but the monomorphism restriction says that we *must not*, giving
418 Why does the momomorphism restriction say this? Because if you have
420 let z = x + ?y in z+z
422 you might not expect the addition to be done twice --- but it will if
423 we follow the argument of Question 2 and generalise over ?y.
429 (A) Always generalise over implicit parameters
430 Bindings that fall under the monomorphism restriction can't
434 * Inlining remains valid
435 * No unexpected loss of sharing
436 * But simple bindings like
438 will be rejected, unless you add an explicit type signature
439 (to avoid the monomorphism restriction)
440 z :: (?y::Int) => Int
442 This seems unacceptable
444 (B) Monomorphism restriction "wins"
445 Bindings that fall under the monomorphism restriction can't
447 Always generalise over implicit parameters *except* for bindings
448 that fall under the monomorphism restriction
451 * Inlining isn't valid in general
452 * No unexpected loss of sharing
453 * Simple bindings like
455 accepted (get value of ?y from binding site)
457 (C) Always generalise over implicit parameters
458 Bindings that fall under the monomorphism restriction can't
459 be generalised, EXCEPT for implicit parameters
461 * Inlining remains valid
462 * Unexpected loss of sharing (from the extra generalisation)
463 * Simple bindings like
465 accepted (get value of ?y from occurrence sites)
470 None of these choices seems very satisfactory. But at least we should
471 decide which we want to do.
473 It's really not clear what is the Right Thing To Do. If you see
477 would you expect the value of ?y to be got from the *occurrence sites*
478 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
479 case of function definitions, the answer is clearly the former, but
480 less so in the case of non-fucntion definitions. On the other hand,
481 if we say that we get the value of ?y from the definition site of 'z',
482 then inlining 'z' might change the semantics of the program.
484 Choice (C) really says "the monomorphism restriction doesn't apply
485 to implicit parameters". Which is fine, but remember that every
486 innocent binding 'x = ...' that mentions an implicit parameter in
487 the RHS becomes a *function* of that parameter, called at each
488 use of 'x'. Now, the chances are that there are no intervening 'with'
489 clauses that bind ?y, so a decent compiler should common up all
490 those function calls. So I think I strongly favour (C). Indeed,
491 one could make a similar argument for abolishing the monomorphism
492 restriction altogether.
494 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
498 %************************************************************************
500 \subsection{tcSimplifyInfer}
502 %************************************************************************
504 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
506 1. Compute Q = grow( fvs(T), C )
508 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
509 predicates will end up in Ct; we deal with them at the top level
511 3. Try improvement, using functional dependencies
513 4. If Step 3 did any unification, repeat from step 1
514 (Unification can change the result of 'grow'.)
516 Note: we don't reduce dictionaries in step 2. For example, if we have
517 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
518 after step 2. However note that we may therefore quantify over more
519 type variables than we absolutely have to.
521 For the guts, we need a loop, that alternates context reduction and
522 improvement with unification. E.g. Suppose we have
524 class C x y | x->y where ...
526 and tcSimplify is called with:
528 Then improvement unifies a with b, giving
531 If we need to unify anything, we rattle round the whole thing all over
538 -> TcTyVarSet -- fv(T); type vars
540 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
541 TcDictBinds, -- Bindings
542 [TcId]) -- Dict Ids that must be bound here (zonked)
543 -- Any free (escaping) Insts are tossed into the environment
548 tcSimplifyInfer doc tau_tvs wanted_lie
549 = inferLoop doc (varSetElems tau_tvs)
550 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
552 -- Check for non-generalisable insts
553 mappM_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenM_`
555 extendLIEs frees `thenM_`
556 returnM (qtvs, binds, map instToId irreds)
558 inferLoop doc tau_tvs wanteds
560 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
561 mappM zonkInst wanteds `thenM` \ wanteds' ->
562 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
564 preds = fdPredsOfInsts wanteds'
565 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
568 | isFreeWhenInferring qtvs inst = Free
569 | isClassDict inst = DontReduceUnlessConstant -- Dicts
570 | otherwise = ReduceMe -- Lits and Methods
573 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
576 if no_improvement then
577 returnM (varSetElems qtvs, frees, binds, irreds)
579 -- If improvement did some unification, we go round again. There
580 -- are two subtleties:
581 -- a) We start again with irreds, not wanteds
582 -- Using an instance decl might have introduced a fresh type variable
583 -- which might have been unified, so we'd get an infinite loop
584 -- if we started again with wanteds! See example [LOOP]
586 -- b) It's also essential to re-process frees, because unification
587 -- might mean that a type variable that looked free isn't now.
589 -- Hence the (irreds ++ frees)
591 -- However, NOTICE that when we are done, we might have some bindings, but
592 -- the final qtvs might be empty. See [NO TYVARS] below.
594 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
595 returnM (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
600 class If b t e r | b t e -> r
603 class Lte a b c | a b -> c where lte :: a -> b -> c
605 instance (Lte a b l,If l b a c) => Max a b c
607 Wanted: Max Z (S x) y
609 Then we'll reduce using the Max instance to:
610 (Lte Z (S x) l, If l (S x) Z y)
611 and improve by binding l->T, after which we can do some reduction
612 on both the Lte and If constraints. What we *can't* do is start again
613 with (Max Z (S x) y)!
617 class Y a b | a -> b where
620 instance Y [[a]] a where
623 k :: X a -> X a -> X a
625 g :: Num a => [X a] -> [X a]
628 h ys = ys ++ map (k (y [[0]])) xs
630 The excitement comes when simplifying the bindings for h. Initially
631 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
632 From this we get t1:=:t2, but also various bindings. We can't forget
633 the bindings (because of [LOOP]), but in fact t1 is what g is
636 The net effect of [NO TYVARS]
639 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
640 isFreeWhenInferring qtvs inst
641 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
642 && isInheritableInst inst -- And no implicit parameter involved
643 -- (see "Notes on implicit parameters")
645 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
646 -> NameSet -- Quantified implicit parameters
648 isFreeWhenChecking qtvs ips inst
649 = isFreeWrtTyVars qtvs inst
650 && isFreeWrtIPs ips inst
652 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
653 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
657 %************************************************************************
659 \subsection{tcSimplifyCheck}
661 %************************************************************************
663 @tcSimplifyCheck@ is used when we know exactly the set of variables
664 we are going to quantify over. For example, a class or instance declaration.
669 -> [TcTyVar] -- Quantify over these
672 -> TcM TcDictBinds -- Bindings
674 -- tcSimplifyCheck is used when checking expression type signatures,
675 -- class decls, instance decls etc.
677 -- NB: tcSimplifyCheck does not consult the
678 -- global type variables in the environment; so you don't
679 -- need to worry about setting them before calling tcSimplifyCheck
680 tcSimplifyCheck doc qtvs givens wanted_lie
681 = tcSimplCheck doc get_qtvs
682 givens wanted_lie `thenM` \ (qtvs', binds) ->
685 get_qtvs = zonkTcTyVarsAndFV qtvs
688 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
689 -- against, but we don't know the type variables over which we are going to quantify.
690 -- This happens when we have a type signature for a mutually recursive group
693 -> TcTyVarSet -- fv(T)
696 -> TcM ([TcTyVar], -- Variables over which to quantify
697 TcDictBinds) -- Bindings
699 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
700 = tcSimplCheck doc get_qtvs givens wanted_lie
702 -- Figure out which type variables to quantify over
703 -- You might think it should just be the signature tyvars,
704 -- but in bizarre cases you can get extra ones
705 -- f :: forall a. Num a => a -> a
706 -- f x = fst (g (x, head [])) + 1
708 -- Here we infer g :: forall a b. a -> b -> (b,a)
709 -- We don't want g to be monomorphic in b just because
710 -- f isn't quantified over b.
711 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
713 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
714 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
716 qtvs = all_tvs' `minusVarSet` gbl_tvs
717 -- We could close gbl_tvs, but its not necessary for
718 -- soundness, and it'll only affect which tyvars, not which
719 -- dictionaries, we quantify over
724 Here is the workhorse function for all three wrappers.
727 tcSimplCheck doc get_qtvs givens wanted_lie
728 = check_loop givens wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
730 -- Complain about any irreducible ones
731 complainCheck doc givens irreds `thenM_`
734 extendLIEs frees `thenM_`
735 returnM (qtvs, binds)
738 ip_set = mkNameSet (ipNamesOfInsts givens)
740 check_loop givens wanteds
742 mappM zonkInst givens `thenM` \ givens' ->
743 mappM zonkInst wanteds `thenM` \ wanteds' ->
744 get_qtvs `thenM` \ qtvs' ->
748 -- When checking against a given signature we always reduce
749 -- until we find a match against something given, or can't reduce
750 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
751 | otherwise = ReduceMe
753 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
756 if no_improvement then
757 returnM (varSetElems qtvs', frees, binds, irreds)
759 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
760 returnM (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
764 %************************************************************************
766 \subsection{tcSimplifyRestricted}
768 %************************************************************************
771 tcSimplifyRestricted -- Used for restricted binding groups
772 -- i.e. ones subject to the monomorphism restriction
774 -> TcTyVarSet -- Free in the type of the RHSs
775 -> [Inst] -- Free in the RHSs
776 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
777 TcDictBinds) -- Bindings
779 tcSimplifyRestricted doc tau_tvs wanteds
780 = -- First squash out all methods, to find the constrained tyvars
781 -- We can't just take the free vars of wanted_lie because that'll
782 -- have methods that may incidentally mention entirely unconstrained variables
783 -- e.g. a call to f :: Eq a => a -> b -> b
784 -- Here, b is unconstrained. A good example would be
786 -- We want to infer the polymorphic type
787 -- foo :: forall b. b -> b
789 -- 'reduceMe': Reduce as far as we can. Don't stop at
790 -- dicts; the idea is to get rid of as many type
791 -- variables as possible, and we don't want to stop
792 -- at (say) Monad (ST s), because that reduces
793 -- immediately, with no constraint on s.
794 simpleReduceLoop doc reduceMe wanteds `thenM` \ (foo_frees, foo_binds, constrained_dicts) ->
796 -- Next, figure out the tyvars we will quantify over
797 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
798 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
800 constrained_tvs = tyVarsOfInsts constrained_dicts
801 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs)
802 `minusVarSet` constrained_tvs
804 traceTc (text "tcSimplifyRestricted" <+> vcat [
805 pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts,
807 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
809 -- The first step may have squashed more methods than
810 -- necessary, so try again, this time knowing the exact
811 -- set of type variables to quantify over.
813 -- We quantify only over constraints that are captured by qtvs;
814 -- these will just be a subset of non-dicts. This in contrast
815 -- to normal inference (using isFreeWhenInferring) in which we quantify over
816 -- all *non-inheritable* constraints too. This implements choice
817 -- (B) under "implicit parameter and monomorphism" above.
819 -- Remember that we may need to do *some* simplification, to
820 -- (for example) squash {Monad (ST s)} into {}. It's not enough
821 -- just to float all constraints
822 restrict_loop doc qtvs wanteds
823 -- We still need a loop because improvement can take place
824 -- E.g. if we have (C (T a)) and the instance decl
825 -- instance D Int b => C (T a) where ...
826 -- and there's a functional dependency for D. Then we may improve
827 -- the tyep variable 'b'.
829 restrict_loop doc qtvs wanteds
830 = mappM zonkInst wanteds `thenM` \ wanteds' ->
831 zonkTcTyVarsAndFV (varSetElems qtvs) `thenM` \ qtvs' ->
833 try_me inst | isFreeWrtTyVars qtvs' inst = Free
834 | otherwise = ReduceMe
836 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
837 if no_improvement then
838 ASSERT( null irreds )
839 extendLIEs frees `thenM_`
840 returnM (varSetElems qtvs', binds)
842 restrict_loop doc qtvs' (irreds ++ frees) `thenM` \ (qtvs1, binds1) ->
843 returnM (qtvs1, binds `AndMonoBinds` binds1)
847 %************************************************************************
849 \subsection{tcSimplifyToDicts}
851 %************************************************************************
853 On the LHS of transformation rules we only simplify methods and constants,
854 getting dictionaries. We want to keep all of them unsimplified, to serve
855 as the available stuff for the RHS of the rule.
857 The same thing is used for specialise pragmas. Consider
860 {-# SPECIALISE f :: Int -> Int #-}
863 The type checker generates a binding like:
865 f_spec = (f :: Int -> Int)
867 and we want to end up with
869 f_spec = _inline_me_ (f Int dNumInt)
871 But that means that we must simplify the Method for f to (f Int dNumInt)!
872 So tcSimplifyToDicts squeezes out all Methods.
874 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
876 fromIntegral :: (Integral a, Num b) => a -> b
877 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
879 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
883 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
885 because the scsel will mess up matching. Instead we want
887 forall dIntegralInt, dNumInt.
888 fromIntegral Int Int dIntegralInt dNumInt = id Int
890 Hence "DontReduce NoSCs"
893 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
894 tcSimplifyToDicts wanteds
895 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
896 -- Since try_me doesn't look at types, we don't need to
897 -- do any zonking, so it's safe to call reduceContext directly
899 extendLIEs irreds `thenM_`
903 doc = text "tcSimplifyToDicts"
905 -- Reduce methods and lits only; stop as soon as we get a dictionary
906 try_me inst | isDict inst = DontReduce NoSCs
907 | otherwise = ReduceMe
912 tcSimplifyBracket is used when simplifying the constraints arising from
913 a Template Haskell bracket [| ... |]. We want to check that there aren't
914 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
915 Show instance), but we aren't otherwise interested in the results.
916 Nor do we care about ambiguous dictionaries etc. We will type check
917 this bracket again at its usage site.
920 tcSimplifyBracket :: [Inst] -> TcM ()
921 tcSimplifyBracket wanteds
922 = simpleReduceLoop doc reduceMe wanteds `thenM_`
925 doc = text "tcSimplifyBracket"
929 %************************************************************************
931 \subsection{Filtering at a dynamic binding}
933 %************************************************************************
938 we must discharge all the ?x constraints from B. We also do an improvement
939 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
941 Actually, the constraints from B might improve the types in ?x. For example
943 f :: (?x::Int) => Char -> Char
946 then the constraint (?x::Int) arising from the call to f will
947 force the binding for ?x to be of type Int.
950 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
953 tcSimplifyIPs given_ips wanteds
954 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
955 extendLIEs frees `thenM_`
958 doc = text "tcSimplifyIPs" <+> ppr given_ips
959 ip_set = mkNameSet (ipNamesOfInsts given_ips)
961 -- Simplify any methods that mention the implicit parameter
962 try_me inst | isFreeWrtIPs ip_set inst = Free
963 | otherwise = ReduceMe
965 simpl_loop givens wanteds
966 = mappM zonkInst givens `thenM` \ givens' ->
967 mappM zonkInst wanteds `thenM` \ wanteds' ->
969 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
971 if no_improvement then
972 ASSERT( null irreds )
973 returnM (frees, binds)
975 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
976 returnM (frees1, binds `AndMonoBinds` binds1)
980 %************************************************************************
982 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
984 %************************************************************************
986 When doing a binding group, we may have @Insts@ of local functions.
987 For example, we might have...
989 let f x = x + 1 -- orig local function (overloaded)
990 f.1 = f Int -- two instances of f
995 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
996 where @f@ is in scope; those @Insts@ must certainly not be passed
997 upwards towards the top-level. If the @Insts@ were binding-ified up
998 there, they would have unresolvable references to @f@.
1000 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1001 For each method @Inst@ in the @init_lie@ that mentions one of the
1002 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1003 @LIE@), as well as the @HsBinds@ generated.
1006 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcMonoBinds
1008 bindInstsOfLocalFuns wanteds local_ids
1009 | null overloaded_ids
1011 = extendLIEs wanteds `thenM_`
1012 returnM EmptyMonoBinds
1015 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1016 ASSERT( null irreds )
1017 extendLIEs frees `thenM_`
1020 doc = text "bindInsts" <+> ppr local_ids
1021 overloaded_ids = filter is_overloaded local_ids
1022 is_overloaded id = isOverloadedTy (idType id)
1024 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1025 -- so it's worth building a set, so that
1026 -- lookup (in isMethodFor) is faster
1028 try_me inst | isMethodFor overloaded_set inst = ReduceMe
1033 %************************************************************************
1035 \subsection{Data types for the reduction mechanism}
1037 %************************************************************************
1039 The main control over context reduction is here
1043 = ReduceMe -- Try to reduce this
1044 -- If there's no instance, behave exactly like
1045 -- DontReduce: add the inst to
1046 -- the irreductible ones, but don't
1047 -- produce an error message of any kind.
1048 -- It might be quite legitimate such as (Eq a)!
1050 | DontReduce WantSCs -- Return as irreducible
1052 | DontReduceUnlessConstant -- Return as irreducible unless it can
1053 -- be reduced to a constant in one step
1055 | Free -- Return as free
1057 reduceMe :: Inst -> WhatToDo
1058 reduceMe inst = ReduceMe
1060 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1061 -- of a predicate when adding it to the avails
1067 type Avails = FiniteMap Inst Avail
1070 = IsFree -- Used for free Insts
1071 | Irred -- Used for irreducible dictionaries,
1072 -- which are going to be lambda bound
1074 | Given TcId -- Used for dictionaries for which we have a binding
1075 -- e.g. those "given" in a signature
1076 Bool -- True <=> actually consumed (splittable IPs only)
1078 | NoRhs -- Used for Insts like (CCallable f)
1079 -- where no witness is required.
1081 | Rhs -- Used when there is a RHS
1083 [Inst] -- Insts free in the RHS; we need these too
1085 | Linear -- Splittable Insts only.
1086 Int -- The Int is always 2 or more; indicates how
1087 -- many copies are required
1088 Inst -- The splitter
1089 Avail -- Where the "master copy" is
1091 | LinRhss -- Splittable Insts only; this is used only internally
1092 -- by extractResults, where a Linear
1093 -- is turned into an LinRhss
1094 [TcExpr] -- A supply of suitable RHSs
1096 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1097 | (inst,avail) <- fmToList avails ]
1099 instance Outputable Avail where
1102 pprAvail NoRhs = text "<no rhs>"
1103 pprAvail IsFree = text "Free"
1104 pprAvail Irred = text "Irred"
1105 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1106 if b then text "(used)" else empty
1107 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1108 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1109 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1112 Extracting the bindings from a bunch of Avails.
1113 The bindings do *not* come back sorted in dependency order.
1114 We assume that they'll be wrapped in a big Rec, so that the
1115 dependency analyser can sort them out later
1119 extractResults :: Avails
1121 -> TcM (TcDictBinds, -- Bindings
1122 [Inst], -- Irreducible ones
1123 [Inst]) -- Free ones
1125 extractResults avails wanteds
1126 = go avails EmptyMonoBinds [] [] wanteds
1128 go avails binds irreds frees []
1129 = returnM (binds, irreds, frees)
1131 go avails binds irreds frees (w:ws)
1132 = case lookupFM avails w of
1133 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1134 go avails binds irreds frees ws
1136 Just NoRhs -> go avails binds irreds frees ws
1137 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1138 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1140 Just (Given id _) -> go avails new_binds irreds frees ws
1142 new_binds | id == instToId w = binds
1143 | otherwise = addBind binds w (HsVar id)
1144 -- The sought Id can be one of the givens, via a superclass chain
1145 -- and then we definitely don't want to generate an x=x binding!
1147 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1149 new_binds = addBind binds w rhs
1151 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1152 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1153 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1154 go (addToFM avails w (LinRhss rhss))
1155 (binds `AndMonoBinds` binds')
1156 irreds' frees' (split_inst : w : ws)
1158 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1159 -> go new_avails new_binds irreds frees ws
1161 new_binds = addBind binds w rhs
1162 new_avails = addToFM avails w (LinRhss rhss)
1164 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1165 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1166 returnM (w':irreds, frees, instToId w')
1167 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1168 returnM (irreds, w':frees, instToId w')
1171 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1172 | otherwise = addToFM avails w NoRhs
1173 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1174 -- than Given, else we end up with bogus bindings.
1176 add_free avails w | isMethod w = avails
1177 | otherwise = add_given avails w
1179 -- Do *not* replace Free by Given if it's a method.
1180 -- The following situation shows why this is bad:
1181 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1182 -- From an application (truncate f i) we get
1183 -- t1 = truncate at f
1185 -- If we have also have a second occurrence of truncate, we get
1186 -- t3 = truncate at f
1188 -- When simplifying with i,f free, we might still notice that
1189 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1190 -- will continue to float out!
1191 -- (split n i a) returns: n rhss
1192 -- auxiliary bindings
1193 -- 1 or 0 insts to add to irreds
1196 split :: Int -> TcId -> TcId -> Inst
1197 -> TcM (TcDictBinds, [TcExpr])
1198 -- (split n split_id root_id wanted) returns
1199 -- * a list of 'n' expressions, all of which witness 'avail'
1200 -- * a bunch of auxiliary bindings to support these expressions
1201 -- * one or zero insts needed to witness the whole lot
1202 -- (maybe be zero if the initial Inst is a Given)
1204 -- NB: 'wanted' is just a template
1206 split n split_id root_id wanted
1209 ty = linearInstType wanted
1210 pair_ty = mkTyConApp pairTyCon [ty,ty]
1211 id = instToId wanted
1215 go 1 = returnM (EmptyMonoBinds, [HsVar root_id])
1217 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1218 expand n rhss `thenM` \ (binds2, rhss') ->
1219 returnM (binds1 `AndMonoBinds` binds2, rhss')
1222 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1223 -- e.g. expand 3 [rhs1, rhs2]
1224 -- = ( { x = split rhs1 },
1225 -- [fst x, snd x, rhs2] )
1227 | n `rem` 2 == 0 = go rhss -- n is even
1228 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1229 returnM (binds', head rhss : rhss')
1231 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1232 returnM (andMonoBindList binds', concat rhss')
1234 do_one rhs = newUnique `thenM` \ uniq ->
1235 tcLookupId fstName `thenM` \ fst_id ->
1236 tcLookupId sndName `thenM` \ snd_id ->
1238 x = mkUserLocal occ uniq pair_ty loc
1240 returnM (VarMonoBind x (mk_app split_id rhs),
1241 [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
1243 mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
1245 mk_app id rhs = HsApp (HsVar id) rhs
1247 addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
1251 %************************************************************************
1253 \subsection[reduce]{@reduce@}
1255 %************************************************************************
1257 When the "what to do" predicate doesn't depend on the quantified type variables,
1258 matters are easier. We don't need to do any zonking, unless the improvement step
1259 does something, in which case we zonk before iterating.
1261 The "given" set is always empty.
1264 simpleReduceLoop :: SDoc
1265 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1267 -> TcM ([Inst], -- Free
1269 [Inst]) -- Irreducible
1271 simpleReduceLoop doc try_me wanteds
1272 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1273 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1274 if no_improvement then
1275 returnM (frees, binds, irreds)
1277 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1278 returnM (frees1, binds `AndMonoBinds` binds1, irreds1)
1284 reduceContext :: SDoc
1285 -> (Inst -> WhatToDo)
1288 -> TcM (Bool, -- True <=> improve step did no unification
1290 TcDictBinds, -- Dictionary bindings
1291 [Inst]) -- Irreducible
1293 reduceContext doc try_me givens wanteds
1295 traceTc (text "reduceContext" <+> (vcat [
1296 text "----------------------",
1298 text "given" <+> ppr givens,
1299 text "wanted" <+> ppr wanteds,
1300 text "----------------------"
1303 -- Build the Avail mapping from "givens"
1304 foldlM addGiven emptyFM givens `thenM` \ init_state ->
1307 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1309 -- Do improvement, using everything in avails
1310 -- In particular, avails includes all superclasses of everything
1311 tcImprove avails `thenM` \ no_improvement ->
1313 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1315 traceTc (text "reduceContext end" <+> (vcat [
1316 text "----------------------",
1318 text "given" <+> ppr givens,
1319 text "wanted" <+> ppr wanteds,
1321 text "avails" <+> pprAvails avails,
1322 text "frees" <+> ppr frees,
1323 text "no_improvement =" <+> ppr no_improvement,
1324 text "----------------------"
1327 returnM (no_improvement, frees, binds, irreds)
1330 = tcGetInstEnv `thenM` \ inst_env ->
1332 preds = [ (pred, pp_loc)
1333 | inst <- keysFM avails,
1334 let pp_loc = pprInstLoc (instLoc inst),
1335 pred <- fdPredsOfInst inst
1337 -- Avails has all the superclasses etc (good)
1338 -- It also has all the intermediates of the deduction (good)
1339 -- It does not have duplicates (good)
1340 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1341 -- so that improve will see them separate
1342 eqns = improve (classInstEnv inst_env) preds
1347 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1348 mappM_ unify eqns `thenM_`
1351 unify ((qtvs, t1, t2), doc)
1353 tcInstTyVars VanillaTv (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1354 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1357 The main context-reduction function is @reduce@. Here's its game plan.
1360 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1361 -- along with its depth
1362 -> (Inst -> WhatToDo)
1369 try_me: given an inst, this function returns
1371 DontReduce return this in "irreds"
1372 Free return this in "frees"
1374 wanteds: The list of insts to reduce
1375 state: An accumulating parameter of type Avails
1376 that contains the state of the algorithm
1378 It returns a Avails.
1380 The (n,stack) pair is just used for error reporting.
1381 n is always the depth of the stack.
1382 The stack is the stack of Insts being reduced: to produce X
1383 I had to produce Y, to produce Y I had to produce Z, and so on.
1386 reduceList (n,stack) try_me wanteds state
1387 | n > opt_MaxContextReductionDepth
1388 = failWithTc (reduceDepthErr n stack)
1394 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1399 go [] state = returnM state
1400 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1403 -- Base case: we're done!
1404 reduce stack try_me wanted state
1405 -- It's the same as an existing inst, or a superclass thereof
1406 | Just avail <- isAvailable state wanted
1407 = if isLinearInst wanted then
1408 addLinearAvailable state avail wanted `thenM` \ (state', wanteds') ->
1409 reduceList stack try_me wanteds' state'
1411 returnM state -- No op for non-linear things
1414 = case try_me wanted of {
1416 DontReduce want_scs -> addIrred want_scs state wanted
1418 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1419 -- First, see if the inst can be reduced to a constant in one step
1420 try_simple (addIrred AddSCs) -- Assume want superclasses
1422 ; Free -> -- It's free so just chuck it upstairs
1423 -- First, see if the inst can be reduced to a constant in one step
1426 ; ReduceMe -> -- It should be reduced
1427 lookupInst wanted `thenM` \ lookup_result ->
1428 case lookup_result of
1429 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenM` \ state' ->
1430 addWanted state' wanted rhs wanteds'
1431 SimpleInst rhs -> addWanted state wanted rhs []
1433 NoInstance -> -- No such instance!
1434 -- Add it and its superclasses
1435 addIrred AddSCs state wanted
1439 try_simple do_this_otherwise
1440 = lookupInst wanted `thenM` \ lookup_result ->
1441 case lookup_result of
1442 SimpleInst rhs -> addWanted state wanted rhs []
1443 other -> do_this_otherwise state wanted
1448 -------------------------
1449 isAvailable :: Avails -> Inst -> Maybe Avail
1450 isAvailable avails wanted = lookupFM avails wanted
1451 -- NB 1: the Ord instance of Inst compares by the class/type info
1452 -- *not* by unique. So
1453 -- d1::C Int == d2::C Int
1455 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1456 addLinearAvailable avails avail wanted
1457 -- avails currently maps [wanted -> avail]
1458 -- Extend avails to reflect a neeed for an extra copy of avail
1460 | Just avail' <- split_avail avail
1461 = returnM (addToFM avails wanted avail', [])
1464 = tcLookupId splitName `thenM` \ split_id ->
1465 tcInstClassOp (instLoc wanted) split_id
1466 [linearInstType wanted] `thenM` \ split_inst ->
1467 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1470 split_avail :: Avail -> Maybe Avail
1471 -- (Just av) if there's a modified version of avail that
1472 -- we can use to replace avail in avails
1473 -- Nothing if there isn't, so we need to create a Linear
1474 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1475 split_avail (Given id used) | not used = Just (Given id True)
1476 | otherwise = Nothing
1477 split_avail Irred = Nothing
1478 split_avail IsFree = Nothing
1479 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1481 -------------------------
1482 addFree :: Avails -> Inst -> TcM Avails
1483 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1484 -- to avails, so that any other equal Insts will be commoned up right
1485 -- here rather than also being tossed upstairs. This is really just
1486 -- an optimisation, and perhaps it is more trouble that it is worth,
1487 -- as the following comments show!
1489 -- NB: do *not* add superclasses. If we have
1492 -- but a is not bound here, then we *don't* want to derive
1493 -- dn from df here lest we lose sharing.
1495 addFree avails free = returnM (addToFM avails free IsFree)
1497 addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> TcM Avails
1498 addWanted avails wanted rhs_expr wanteds
1499 = ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
1500 addAvailAndSCs avails wanted avail
1502 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1503 | otherwise = ASSERT( null wanteds ) NoRhs
1505 addGiven :: Avails -> Inst -> TcM Avails
1506 addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
1507 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1508 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1509 -- so the assert isn't true
1511 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1512 addIrred NoSCs avails irred = returnM (addToFM avails irred Irred)
1513 addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1514 addAvailAndSCs avails irred Irred
1516 addAvailAndSCs :: Avails -> Inst -> Avail -> TcM Avails
1517 addAvailAndSCs avails inst avail
1518 | not (isClassDict inst) = returnM avails1
1519 | otherwise = addSCs is_loop avails1 inst
1521 avails1 = addToFM avails inst avail
1522 is_loop inst = inst `elem` deps -- Note: this compares by *type*, not by Unique
1523 deps = findAllDeps avails avail
1525 findAllDeps :: Avails -> Avail -> [Inst]
1526 -- Find all the Insts that this one depends on
1527 -- See Note [SUPERCLASS-LOOP]
1528 findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
1529 findAllDeps avails other = []
1531 find_all_deps_help :: Avails -> Inst -> [Inst]
1532 find_all_deps_help avails inst
1533 = case lookupFM avails inst of
1534 Just avail -> findAllDeps avails avail
1537 addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
1538 -- Add all the superclasses of the Inst to Avails
1539 -- The first param says "dont do this because the original thing
1540 -- depends on this one, so you'd build a loop"
1541 -- Invariant: the Inst is already in Avails.
1543 addSCs is_loop avails dict
1544 = newDictsFromOld dict sc_theta' `thenM` \ sc_dicts ->
1545 foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1547 (clas, tys) = getDictClassTys dict
1548 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1549 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1551 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1552 = case lookupFM avails sc_dict of
1553 Just (Given _ _) -> returnM avails -- Given is cheaper than
1554 -- a superclass selection
1555 Just other | is_loop sc_dict -> returnM avails -- See Note [SUPERCLASS-LOOP]
1556 | otherwise -> returnM avails' -- SCs already added
1558 Nothing -> addSCs is_loop avails' sc_dict
1560 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1561 avail = Rhs sc_sel_rhs [dict]
1562 avails' = addToFM avails sc_dict avail
1565 Note [SUPERCLASS-LOOP]: Checking for loops
1566 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1567 We have to be careful here. If we are *given* d1:Ord a,
1568 and want to deduce (d2:C [a]) where
1570 class Ord a => C a where
1571 instance Ord a => C [a] where ...
1573 Then we'll use the instance decl to deduce C [a] and then add the
1574 superclasses of C [a] to avails. But we must not overwrite the binding
1575 for d1:Ord a (which is given) with a superclass selection or we'll just
1578 Here's another example
1579 class Eq b => Foo a b
1580 instance Eq a => Foo [a] a
1584 we'll first deduce that it holds (via the instance decl). We must not
1585 then overwrite the Eq t constraint with a superclass selection!
1587 At first I had a gross hack, whereby I simply did not add superclass constraints
1588 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1589 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1590 I found a very obscure program (now tcrun021) in which improvement meant the
1591 simplifier got two bites a the cherry... so something seemed to be an Irred
1592 first time, but reducible next time.
1594 Now we implement the Right Solution, which is to check for loops directly
1595 when adding superclasses. It's a bit like the occurs check in unification.
1599 %************************************************************************
1601 \section{tcSimplifyTop: defaulting}
1603 %************************************************************************
1606 @tcSimplifyTop@ is called once per module to simplify all the constant
1607 and ambiguous Insts.
1609 We need to be careful of one case. Suppose we have
1611 instance Num a => Num (Foo a b) where ...
1613 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1614 to (Num x), and default x to Int. But what about y??
1616 It's OK: the final zonking stage should zap y to (), which is fine.
1620 tcSimplifyTop :: [Inst] -> TcM TcDictBinds
1621 -- The TcLclEnv should be valid here, solely to improve
1622 -- error message generation for the monomorphism restriction
1623 tcSimplifyTop wanteds
1624 = getLclEnv `thenM` \ lcl_env ->
1625 traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env)) `thenM_`
1626 simpleReduceLoop (text "tcSimplTop") reduceMe wanteds `thenM` \ (frees, binds, irreds) ->
1627 ASSERT( null frees )
1630 -- All the non-std ones are definite errors
1631 (stds, non_stds) = partition isStdClassTyVarDict irreds
1633 -- Group by type variable
1634 std_groups = equivClasses cmp_by_tyvar stds
1636 -- Pick the ones which its worth trying to disambiguate
1637 -- namely, the onese whose type variable isn't bound
1638 -- up with one of the non-standard classes
1639 (std_oks, std_bads) = partition worth_a_try std_groups
1640 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1641 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1643 -- Collect together all the bad guys
1644 bad_guys = non_stds ++ concat std_bads
1645 (tidy_env, tidy_dicts) = tidyInsts bad_guys
1646 (bad_ips, non_ips) = partition isIPDict tidy_dicts
1647 (no_insts, ambigs) = partition no_inst non_ips
1648 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1649 fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
1652 -- Report definite errors
1653 addTopInstanceErrs tidy_env no_insts `thenM_`
1654 addTopIPErrs tidy_env bad_ips `thenM_`
1656 -- Deal with ambiguity errors, but only if
1657 -- if there has not been an error so far; errors often
1658 -- give rise to spurious ambiguous Insts
1659 ifErrsM (returnM []) (
1661 -- Complain about the ones that don't fall under
1662 -- the Haskell rules for disambiguation
1663 -- This group includes both non-existent instances
1664 -- e.g. Num (IO a) and Eq (Int -> Int)
1665 -- and ambiguous dictionaries
1667 addTopAmbigErrs (tidy_env, ambigs) `thenM_`
1669 -- Disambiguate the ones that look feasible
1670 mappM disambigGroup std_oks
1671 ) `thenM` \ binds_ambig ->
1673 returnM (binds `andMonoBinds` andMonoBindList binds_ambig)
1675 ----------------------------------
1676 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1678 get_tv d = case getDictClassTys d of
1679 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1680 get_clas d = case getDictClassTys d of
1681 (clas, [ty]) -> clas
1684 If a dictionary constrains a type variable which is
1685 * not mentioned in the environment
1686 * and not mentioned in the type of the expression
1687 then it is ambiguous. No further information will arise to instantiate
1688 the type variable; nor will it be generalised and turned into an extra
1689 parameter to a function.
1691 It is an error for this to occur, except that Haskell provided for
1692 certain rules to be applied in the special case of numeric types.
1694 * at least one of its classes is a numeric class, and
1695 * all of its classes are numeric or standard
1696 then the type variable can be defaulted to the first type in the
1697 default-type list which is an instance of all the offending classes.
1699 So here is the function which does the work. It takes the ambiguous
1700 dictionaries and either resolves them (producing bindings) or
1701 complains. It works by splitting the dictionary list by type
1702 variable, and using @disambigOne@ to do the real business.
1704 @disambigOne@ assumes that its arguments dictionaries constrain all
1705 the same type variable.
1707 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1708 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1709 the most common use of defaulting is code like:
1711 _ccall_ foo `seqPrimIO` bar
1713 Since we're not using the result of @foo@, the result if (presumably)
1717 disambigGroup :: [Inst] -- All standard classes of form (C a)
1721 | any isNumericClass classes -- Guaranteed all standard classes
1722 -- see comment at the end of function for reasons as to
1723 -- why the defaulting mechanism doesn't apply to groups that
1724 -- include CCallable or CReturnable dicts.
1725 && not (any isCcallishClass classes)
1726 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1727 -- SO, TRY DEFAULT TYPES IN ORDER
1729 -- Failure here is caused by there being no type in the
1730 -- default list which can satisfy all the ambiguous classes.
1731 -- For example, if Real a is reqd, but the only type in the
1732 -- default list is Int.
1733 getDefaultTys `thenM` \ default_tys ->
1735 try_default [] -- No defaults work, so fail
1738 try_default (default_ty : default_tys)
1739 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
1740 -- default_tys instead
1741 tcSimplifyDefault theta `thenM` \ _ ->
1744 theta = [mkClassPred clas [default_ty] | clas <- classes]
1746 -- See if any default works
1747 tryM (try_default default_tys) `thenM` \ mb_ty ->
1749 Left _ -> -- If not, add an AmbigErr
1750 addTopAmbigErrs (tidyInsts dicts) `thenM_`
1751 returnM EmptyMonoBinds ;
1753 Right chosen_default_ty ->
1755 -- If so, bind the type variable
1756 -- and reduce the context, for real this time
1757 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenM_`
1758 simpleReduceLoop (text "disambig" <+> ppr dicts)
1759 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
1760 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1761 warnDefault dicts chosen_default_ty `thenM_`
1764 | all isCreturnableClass classes
1765 = -- Default CCall stuff to (); we don't even both to check that () is an
1766 -- instance of CReturnable, because we know it is.
1767 unifyTauTy (mkTyVarTy tyvar) unitTy `thenM_`
1768 returnM EmptyMonoBinds
1770 | otherwise -- No defaults
1771 = addTopAmbigErrs (tidyInsts dicts) `thenM_`
1772 returnM EmptyMonoBinds
1775 tyvar = get_tv (head dicts) -- Should be non-empty
1776 classes = map get_clas dicts
1779 [Aside - why the defaulting mechanism is turned off when
1780 dealing with arguments and results to ccalls.
1782 When typechecking _ccall_s, TcExpr ensures that the external
1783 function is only passed arguments (and in the other direction,
1784 results) of a restricted set of 'native' types. This is
1785 implemented via the help of the pseudo-type classes,
1786 @CReturnable@ (CR) and @CCallable@ (CC.)
1788 The interaction between the defaulting mechanism for numeric
1789 values and CC & CR can be a bit puzzling to the user at times.
1798 What type has 'x' got here? That depends on the default list
1799 in operation, if it is equal to Haskell 98's default-default
1800 of (Integer, Double), 'x' has type Double, since Integer
1801 is not an instance of CR. If the default list is equal to
1802 Haskell 1.4's default-default of (Int, Double), 'x' has type
1805 To try to minimise the potential for surprises here, the
1806 defaulting mechanism is turned off in the presence of
1807 CCallable and CReturnable.
1812 %************************************************************************
1814 \subsection[simple]{@Simple@ versions}
1816 %************************************************************************
1818 Much simpler versions when there are no bindings to make!
1820 @tcSimplifyThetas@ simplifies class-type constraints formed by
1821 @deriving@ declarations and when specialising instances. We are
1822 only interested in the simplified bunch of class/type constraints.
1824 It simplifies to constraints of the form (C a b c) where
1825 a,b,c are type variables. This is required for the context of
1826 instance declarations.
1829 tcSimplifyDeriv :: [TyVar]
1830 -> ThetaType -- Wanted
1831 -> TcM ThetaType -- Needed
1833 tcSimplifyDeriv tyvars theta
1834 = tcInstTyVars VanillaTv tyvars `thenM` \ (tvs, _, tenv) ->
1835 -- The main loop may do unification, and that may crash if
1836 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
1837 -- ToDo: what if two of them do get unified?
1838 newDicts DataDeclOrigin (substTheta tenv theta) `thenM` \ wanteds ->
1839 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
1840 ASSERT( null frees ) -- reduceMe never returns Free
1842 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
1844 tv_set = mkVarSet tvs
1845 simpl_theta = map dictPred irreds -- reduceMe squashes all non-dicts
1848 | isEmptyVarSet pred_tyvars -- Things like (Eq T) should be rejected
1849 = addErrTc (noInstErr pred)
1851 | not undecidable_ok && not (isTyVarClassPred pred)
1852 -- Check that the returned dictionaries are all of form (C a b)
1853 -- (where a, b are type variables).
1854 -- We allow this if we had -fallow-undecidable-instances,
1855 -- but note that risks non-termination in the 'deriving' context-inference
1856 -- fixpoint loop. It is useful for situations like
1857 -- data Min h a = E | M a (h a)
1858 -- which gives the instance decl
1859 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
1860 = addErrTc (noInstErr pred)
1862 | not (pred_tyvars `subVarSet` tv_set)
1863 -- Check for a bizarre corner case, when the derived instance decl should
1864 -- have form instance C a b => D (T a) where ...
1865 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
1866 -- of problems; in particular, it's hard to compare solutions for
1867 -- equality when finding the fixpoint. So I just rule it out for now.
1868 = addErrTc (badDerivedPred pred)
1873 pred_tyvars = tyVarsOfPred pred
1875 rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
1876 -- This reverse-mapping is a Royal Pain,
1877 -- but the result should mention TyVars not TcTyVars
1880 mappM check_pred simpl_theta `thenM_`
1881 checkAmbiguity tvs simpl_theta tv_set `thenM_`
1882 returnM (substTheta rev_env simpl_theta)
1884 doc = ptext SLIT("deriving classes for a data type")
1887 @tcSimplifyDefault@ just checks class-type constraints, essentially;
1888 used with \tr{default} declarations. We are only interested in
1889 whether it worked or not.
1892 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
1895 tcSimplifyDefault theta
1896 = newDicts DataDeclOrigin theta `thenM` \ wanteds ->
1897 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
1898 ASSERT( null frees ) -- try_me never returns Free
1899 mappM (addErrTc . noInstErr) irreds `thenM_`
1905 doc = ptext SLIT("default declaration")
1909 %************************************************************************
1911 \section{Errors and contexts}
1913 %************************************************************************
1915 ToDo: for these error messages, should we note the location as coming
1916 from the insts, or just whatever seems to be around in the monad just
1920 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
1921 -> [Inst] -- The offending Insts
1923 -- Group together insts with the same origin
1924 -- We want to report them together in error messages
1926 groupErrs report_err []
1928 groupErrs report_err (inst:insts)
1929 = do_one (inst:friends) `thenM_`
1930 groupErrs report_err others
1933 -- (It may seem a bit crude to compare the error messages,
1934 -- but it makes sure that we combine just what the user sees,
1935 -- and it avoids need equality on InstLocs.)
1936 (friends, others) = partition is_friend insts
1937 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1938 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1939 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
1940 -- Add location and context information derived from the Insts
1942 -- Add the "arising from..." part to a message about bunch of dicts
1943 addInstLoc :: [Inst] -> Message -> Message
1944 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
1947 plural xs = char 's'
1950 addTopIPErrs tidy_env tidy_dicts
1951 = groupErrs report tidy_dicts
1953 report dicts = addErrTcM (tidy_env, mk_msg dicts)
1954 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
1955 plural tidy_dicts <+> pprInsts tidy_dicts)
1957 -- Used for top-level irreducibles
1958 addTopInstanceErrs tidy_env tidy_dicts
1959 = groupErrs report tidy_dicts
1961 report dicts = mkMonomorphismMsg tidy_env dicts `thenM` \ (tidy_env, mono_msg) ->
1962 addErrTcM (tidy_env, mk_msg dicts $$ mono_msg)
1963 mk_msg dicts = addInstLoc dicts (ptext SLIT("No instance") <> plural tidy_dicts <+>
1964 ptext SLIT("for") <+> pprInsts tidy_dicts)
1967 addTopAmbigErrs (tidy_env, tidy_dicts)
1968 -- Divide into groups that share a common set of ambiguous tyvars
1969 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
1971 tvs_of :: Inst -> [TcTyVar]
1972 tvs_of d = varSetElems (tyVarsOfInst d)
1973 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
1975 report :: [(Inst,[TcTyVar])] -> TcM ()
1976 report pairs@((_,tvs) : _) -- The pairs share a common set of ambiguous tyvars
1977 = mkMonomorphismMsg tidy_env dicts `thenM` \ (tidy_env, mono_msg) ->
1978 addErrTcM (tidy_env, msg $$ mono_msg)
1980 dicts = map fst pairs
1981 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
1982 pprQuotedList tvs <+> in_msg,
1983 nest 2 (pprInstsInFull dicts)]
1984 in_msg | isSingleton dicts = text "in the top-level constraint:"
1985 | otherwise = text "in these top-level constraints:"
1988 mkMonomorphismMsg :: TidyEnv -> [Inst] -> TcM (TidyEnv, Message)
1989 -- There's an error with these Insts; if they have free type variables
1990 -- it's probably caused by the monomorphism restriction.
1991 -- Try to identify the offending variable
1992 -- ASSUMPTION: the Insts are fully zonked
1993 mkMonomorphismMsg tidy_env insts
1994 | isEmptyVarSet inst_tvs
1995 = returnM (tidy_env, empty)
1997 = findGlobals inst_tvs tidy_env `thenM` \ (tidy_env, docs) ->
1998 returnM (tidy_env, mk_msg docs)
2001 inst_tvs = tyVarsOfInsts insts
2003 mk_msg [] = empty -- This happens in things like
2004 -- f x = show (read "foo")
2005 -- whre monomorphism doesn't play any role
2006 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2008 ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
2010 warnDefault dicts default_ty
2011 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2012 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2015 (_, tidy_dicts) = tidyInsts dicts
2016 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2017 quotes (ppr default_ty),
2018 pprInstsInFull tidy_dicts]
2020 complainCheck doc givens irreds
2021 = mappM zonkInst given_dicts_and_ips `thenM` \ givens' ->
2022 groupErrs (addNoInstanceErrs doc givens') irreds `thenM_`
2025 given_dicts_and_ips = filter (not . isMethod) givens
2026 -- Filter out methods, which are only added to
2027 -- the given set as an optimisation
2029 addNoInstanceErrs what_doc givens dicts
2030 = getDOpts `thenM` \ dflags ->
2031 tcGetInstEnv `thenM` \ inst_env ->
2033 (tidy_env1, tidy_givens) = tidyInsts givens
2034 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2036 doc = vcat [addInstLoc dicts $
2037 sep [herald <+> pprInsts tidy_dicts,
2038 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
2040 ptext SLIT("Probable fix:"),
2044 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
2045 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
2048 -- The error message when we don't find a suitable instance
2049 -- is complicated by the fact that sometimes this is because
2050 -- there is no instance, and sometimes it's because there are
2051 -- too many instances (overlap). See the comments in TcEnv.lhs
2052 -- with the InstEnv stuff.
2055 | not ambig_overlap = empty
2057 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
2058 nest 4 (ptext SLIT("depends on the instantiation of") <+>
2059 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
2061 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
2062 ptext SLIT("to the") <+> what_doc]
2064 fix2 | null instance_dicts
2067 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
2069 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
2070 -- Insts for which it is worth suggesting an adding an instance declaration
2071 -- Exclude implicit parameters, and tyvar dicts
2073 -- Checks for the ambiguous case when we have overlapping instances
2074 ambig_overlap = any ambig_overlap1 dicts
2077 = case lookupInstEnv dflags inst_env clas tys of
2078 NoMatch ambig -> ambig
2082 (clas,tys) = getDictClassTys dict
2084 addErrTcM (tidy_env2, doc)
2086 -- Used for the ...Thetas variants; all top level
2087 noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
2090 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2091 ptext SLIT("type variables that are not data type parameters"),
2092 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2094 reduceDepthErr n stack
2095 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2096 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2097 nest 4 (pprInstsInFull stack)]
2099 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
2101 -----------------------------------------------
2103 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
2104 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])