2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
14 tcSimplifyThetas, tcSimplifyCheckThetas,
18 #include "HsVersions.h"
20 import {-# SOURCE #-} TcUnify( unifyTauTy )
22 import HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
23 import TcHsSyn ( TcExpr, TcId,
24 TcMonoBinds, TcDictBinds
28 import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
29 tyVarsOfInst, predsOfInsts, predsOfInst,
31 isStdClassTyVarDict, isMethodFor,
32 instToId, tyVarsOfInsts,
33 ipNamesOfInsts, ipNamesOfInst,
34 instBindingRequired, instCanBeGeneralised,
36 getDictClassTys, isTyVarDict,
37 instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
38 Inst, LIE, pprInsts, pprInstsInFull,
41 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
42 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
43 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars )
44 import TcType ( TcTyVar, TcTyVarSet, ThetaType, PredType,
45 mkClassPred, isOverloadedTy,
46 mkTyVarTy, tcGetTyVar, isTyVarClassPred,
47 tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
48 inheritablePred, predHasFDs )
50 import NameSet ( NameSet, mkNameSet, elemNameSet )
51 import Class ( classBigSig )
52 import FunDeps ( oclose, grow, improve, pprEquationDoc )
53 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
55 import Subst ( mkTopTyVarSubst, substTheta, substTy )
56 import TysWiredIn ( unitTy )
60 import ListSetOps ( equivClasses )
61 import Util ( zipEqual )
62 import List ( partition )
67 %************************************************************************
71 %************************************************************************
73 --------------------------------------
74 Notes on quantification
75 --------------------------------------
77 Suppose we are about to do a generalisation step.
82 C the constraints from that RHS
84 The game is to figure out
86 Q the set of type variables over which to quantify
87 Ct the constraints we will *not* quantify over
88 Cq the constraints we will quantify over
90 So we're going to infer the type
94 and float the constraints Ct further outwards.
96 Here are the things that *must* be true:
98 (A) Q intersect fv(G) = EMPTY limits how big Q can be
99 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
101 (A) says we can't quantify over a variable that's free in the
102 environment. (B) says we must quantify over all the truly free
103 variables in T, else we won't get a sufficiently general type. We do
104 not *need* to quantify over any variable that is fixed by the free
105 vars of the environment G.
107 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
109 Example: class H x y | x->y where ...
111 fv(G) = {a} C = {H a b, H c d}
114 (A) Q intersect {a} is empty
115 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
117 So Q can be {c,d}, {b,c,d}
119 Other things being equal, however, we'd like to quantify over as few
120 variables as possible: smaller types, fewer type applications, more
121 constraints can get into Ct instead of Cq.
124 -----------------------------------------
127 fv(T) the free type vars of T
129 oclose(vs,C) The result of extending the set of tyvars vs
130 using the functional dependencies from C
132 grow(vs,C) The result of extend the set of tyvars vs
133 using all conceivable links from C.
135 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
136 Then grow(vs,C) = {a,b,c}
138 Note that grow(vs,C) `superset` grow(vs,simplify(C))
139 That is, simplfication can only shrink the result of grow.
142 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
143 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
146 -----------------------------------------
150 Here's a good way to choose Q:
152 Q = grow( fv(T), C ) \ oclose( fv(G), C )
154 That is, quantify over all variable that that MIGHT be fixed by the
155 call site (which influences T), but which aren't DEFINITELY fixed by
156 G. This choice definitely quantifies over enough type variables,
157 albeit perhaps too many.
159 Why grow( fv(T), C ) rather than fv(T)? Consider
161 class H x y | x->y where ...
166 If we used fv(T) = {c} we'd get the type
168 forall c. H c d => c -> b
170 And then if the fn was called at several different c's, each of
171 which fixed d differently, we'd get a unification error, because
172 d isn't quantified. Solution: quantify d. So we must quantify
173 everything that might be influenced by c.
175 Why not oclose( fv(T), C )? Because we might not be able to see
176 all the functional dependencies yet:
178 class H x y | x->y where ...
179 instance H x y => Eq (T x y) where ...
184 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
185 apparent yet, and that's wrong. We must really quantify over d too.
188 There really isn't any point in quantifying over any more than
189 grow( fv(T), C ), because the call sites can't possibly influence
190 any other type variables.
194 --------------------------------------
196 --------------------------------------
198 It's very hard to be certain when a type is ambiguous. Consider
202 instance H x y => K (x,y)
204 Is this type ambiguous?
205 forall a b. (K (a,b), Eq b) => a -> a
207 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
208 now we see that a fixes b. So we can't tell about ambiguity for sure
209 without doing a full simplification. And even that isn't possible if
210 the context has some free vars that may get unified. Urgle!
212 Here's another example: is this ambiguous?
213 forall a b. Eq (T b) => a -> a
214 Not if there's an insance decl (with no context)
215 instance Eq (T b) where ...
217 You may say of this example that we should use the instance decl right
218 away, but you can't always do that:
220 class J a b where ...
221 instance J Int b where ...
223 f :: forall a b. J a b => a -> a
225 (Notice: no functional dependency in J's class decl.)
226 Here f's type is perfectly fine, provided f is only called at Int.
227 It's premature to complain when meeting f's signature, or even
228 when inferring a type for f.
232 However, we don't *need* to report ambiguity right away. It'll always
233 show up at the call site.... and eventually at main, which needs special
234 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
236 So here's the plan. We WARN about probable ambiguity if
238 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
240 (all tested before quantification).
241 That is, all the type variables in Cq must be fixed by the the variables
242 in the environment, or by the variables in the type.
244 Notice that we union before calling oclose. Here's an example:
246 class J a b c | a b -> c
250 forall b c. (J a b c) => b -> b
252 Only if we union {a} from G with {b} from T before using oclose,
253 do we see that c is fixed.
255 It's a bit vague exactly which C we should use for this oclose call. If we
256 don't fix enough variables we might complain when we shouldn't (see
257 the above nasty example). Nothing will be perfect. That's why we can
258 only issue a warning.
261 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
263 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
265 then c is a "bubble"; there's no way it can ever improve, and it's
266 certainly ambiguous. UNLESS it is a constant (sigh). And what about
271 instance H x y => K (x,y)
273 Is this type ambiguous?
274 forall a b. (K (a,b), Eq b) => a -> a
276 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
277 is a "bubble" that's a set of constraints
279 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
281 Hence another idea. To decide Q start with fv(T) and grow it
282 by transitive closure in Cq (no functional dependencies involved).
283 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
284 The definitely-ambiguous can then float out, and get smashed at top level
285 (which squashes out the constants, like Eq (T a) above)
288 --------------------------------------
289 Notes on principal types
290 --------------------------------------
295 f x = let g y = op (y::Int) in True
297 Here the principal type of f is (forall a. a->a)
298 but we'll produce the non-principal type
299 f :: forall a. C Int => a -> a
302 --------------------------------------
303 Notes on implicit parameters
304 --------------------------------------
306 Question 1: can we "inherit" implicit parameters
307 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
312 where f is *not* a top-level binding.
313 From the RHS of f we'll get the constraint (?y::Int).
314 There are two types we might infer for f:
318 (so we get ?y from the context of f's definition), or
320 f :: (?y::Int) => Int -> Int
322 At first you might think the first was better, becuase then
323 ?y behaves like a free variable of the definition, rather than
324 having to be passed at each call site. But of course, the WHOLE
325 IDEA is that ?y should be passed at each call site (that's what
326 dynamic binding means) so we'd better infer the second.
328 BOTTOM LINE: when *inferring types* you *must* quantify
329 over implicit parameters. See the predicate isFreeWhenInferring.
332 Question 2: type signatures
333 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
334 BUT WATCH OUT: When you supply a type signature, we can't force you
335 to quantify over implicit parameters. For example:
339 This is perfectly reasonable. We do not want to insist on
341 (?x + 1) :: (?x::Int => Int)
343 That would be silly. Here, the definition site *is* the occurrence site,
344 so the above strictures don't apply. Hence the difference between
345 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
346 and tcSimplifyCheckBind (which does not).
348 What about when you supply a type signature for a binding?
349 Is it legal to give the following explicit, user type
350 signature to f, thus:
355 At first sight this seems reasonable, but it has the nasty property
356 that adding a type signature changes the dynamic semantics.
359 (let f x = (x::Int) + ?y
360 in (f 3, f 3 with ?y=5)) with ?y = 6
366 in (f 3, f 3 with ?y=5)) with ?y = 6
370 Indeed, simply inlining f (at the Haskell source level) would change the
373 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
374 semantics for a Haskell program without knowing its typing, so if you
375 change the typing you may change the semantics.
377 To make things consistent in all cases where we are *checking* against
378 a supplied signature (as opposed to inferring a type), we adopt the
381 a signature does not need to quantify over implicit params.
383 [This represents a (rather marginal) change of policy since GHC 5.02,
384 which *required* an explicit signature to quantify over all implicit
385 params for the reasons mentioned above.]
387 But that raises a new question. Consider
389 Given (signature) ?x::Int
390 Wanted (inferred) ?x::Int, ?y::Bool
392 Clearly we want to discharge the ?x and float the ?y out. But
393 what is the criterion that distinguishes them? Clearly it isn't
394 what free type variables they have. The Right Thing seems to be
395 to float a constraint that
396 neither mentions any of the quantified type variables
397 nor any of the quantified implicit parameters
399 See the predicate isFreeWhenChecking.
402 Question 3: monomorphism
403 ~~~~~~~~~~~~~~~~~~~~~~~~
404 There's a nasty corner case when the monomorphism restriction bites:
408 The argument above suggests that we *must* generalise
409 over the ?y parameter, to get
410 z :: (?y::Int) => Int,
411 but the monomorphism restriction says that we *must not*, giving
413 Why does the momomorphism restriction say this? Because if you have
415 let z = x + ?y in z+z
417 you might not expect the addition to be done twice --- but it will if
418 we follow the argument of Question 2 and generalise over ?y.
424 (A) Always generalise over implicit parameters
425 Bindings that fall under the monomorphism restriction can't
429 * Inlining remains valid
430 * No unexpected loss of sharing
431 * But simple bindings like
433 will be rejected, unless you add an explicit type signature
434 (to avoid the monomorphism restriction)
435 z :: (?y::Int) => Int
437 This seems unacceptable
439 (B) Monomorphism restriction "wins"
440 Bindings that fall under the monomorphism restriction can't
442 Always generalise over implicit parameters *except* for bindings
443 that fall under the monomorphism restriction
446 * Inlining isn't valid in general
447 * No unexpected loss of sharing
448 * Simple bindings like
450 accepted (get value of ?y from binding site)
452 (C) Always generalise over implicit parameters
453 Bindings that fall under the monomorphism restriction can't
454 be generalised, EXCEPT for implicit parameters
456 * Inlining remains valid
457 * Unexpected loss of sharing (from the extra generalisation)
458 * Simple bindings like
460 accepted (get value of ?y from occurrence sites)
465 None of these choices seems very satisfactory. But at least we should
466 decide which we want to do.
468 It's really not clear what is the Right Thing To Do. If you see
472 would you expect the value of ?y to be got from the *occurrence sites*
473 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
474 case of function definitions, the answer is clearly the former, but
475 less so in the case of non-fucntion definitions. On the other hand,
476 if we say that we get the value of ?y from the definition site of 'z',
477 then inlining 'z' might change the semantics of the program.
479 Choice (C) really says "the monomorphism restriction doesn't apply
480 to implicit parameters". Which is fine, but remember that every
481 innocent binding 'x = ...' that mentions an implicit parameter in
482 the RHS becomes a *function* of that parameter, called at each
483 use of 'x'. Now, the chances are that there are no intervening 'with'
484 clauses that bind ?y, so a decent compiler should common up all
485 those function calls. So I think I strongly favour (C). Indeed,
486 one could make a similar argument for abolishing the monomorphism
487 restriction altogether.
489 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
493 %************************************************************************
495 \subsection{tcSimplifyInfer}
497 %************************************************************************
499 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
501 1. Compute Q = grow( fvs(T), C )
503 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
504 predicates will end up in Ct; we deal with them at the top level
506 3. Try improvement, using functional dependencies
508 4. If Step 3 did any unification, repeat from step 1
509 (Unification can change the result of 'grow'.)
511 Note: we don't reduce dictionaries in step 2. For example, if we have
512 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
513 after step 2. However note that we may therefore quantify over more
514 type variables than we absolutely have to.
516 For the guts, we need a loop, that alternates context reduction and
517 improvement with unification. E.g. Suppose we have
519 class C x y | x->y where ...
521 and tcSimplify is called with:
523 Then improvement unifies a with b, giving
526 If we need to unify anything, we rattle round the whole thing all over
533 -> TcTyVarSet -- fv(T); type vars
535 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
537 TcDictBinds, -- Bindings
538 [TcId]) -- Dict Ids that must be bound here (zonked)
543 tcSimplifyInfer doc tau_tvs wanted_lie
544 = inferLoop doc (varSetElems tau_tvs)
545 (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
547 -- Check for non-generalisable insts
548 mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
550 returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
552 inferLoop doc tau_tvs wanteds
554 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
555 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
556 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
558 preds = predsOfInsts wanteds'
559 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
562 | isFreeWhenInferring qtvs inst = Free
563 | isClassDict inst = DontReduceUnlessConstant -- Dicts
564 | otherwise = ReduceMe -- Lits and Methods
567 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
570 if no_improvement then
571 returnTc (varSetElems qtvs, frees, binds, irreds)
573 -- If improvement did some unification, we go round again. There
574 -- are two subtleties:
575 -- a) We start again with irreds, not wanteds
576 -- Using an instance decl might have introduced a fresh type variable
577 -- which might have been unified, so we'd get an infinite loop
578 -- if we started again with wanteds! See example [LOOP]
580 -- b) It's also essential to re-process frees, because unification
581 -- might mean that a type variable that looked free isn't now.
583 -- Hence the (irreds ++ frees)
585 -- However, NOTICE that when we are done, we might have some bindings, but
586 -- the final qtvs might be empty. See [NO TYVARS] below.
588 inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
589 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
594 class If b t e r | b t e -> r
597 class Lte a b c | a b -> c where lte :: a -> b -> c
599 instance (Lte a b l,If l b a c) => Max a b c
601 Wanted: Max Z (S x) y
603 Then we'll reduce using the Max instance to:
604 (Lte Z (S x) l, If l (S x) Z y)
605 and improve by binding l->T, after which we can do some reduction
606 on both the Lte and If constraints. What we *can't* do is start again
607 with (Max Z (S x) y)!
611 class Y a b | a -> b where
614 instance Y [[a]] a where
617 k :: X a -> X a -> X a
619 g :: Num a => [X a] -> [X a]
622 h ys = ys ++ map (k (y [[0]])) xs
624 The excitement comes when simplifying the bindings for h. Initially
625 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
626 From this we get t1:=:t2, but also various bindings. We can't forget
627 the bindings (because of [LOOP]), but in fact t1 is what g is
630 The net effect of [NO TYVARS]
633 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
634 isFreeWhenInferring qtvs inst
635 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
636 && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
637 -- (see "Notes on implicit parameters")
639 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
640 -> NameSet -- Quantified implicit parameters
642 isFreeWhenChecking qtvs ips inst
643 = isFreeWrtTyVars qtvs inst
644 && isFreeWrtIPs ips inst
646 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
647 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
651 %************************************************************************
653 \subsection{tcSimplifyCheck}
655 %************************************************************************
657 @tcSimplifyCheck@ is used when we know exactly the set of variables
658 we are going to quantify over. For example, a class or instance declaration.
663 -> [TcTyVar] -- Quantify over these
667 TcDictBinds) -- Bindings
669 -- tcSimplifyCheck is used when checking expression type signatures,
670 -- class decls, instance decls etc.
671 -- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
672 -- It's important that we can float out non-inheritable predicates
673 -- Example: (?x :: Int) is ok!
674 tcSimplifyCheck doc qtvs givens wanted_lie
675 = tcSimplCheck doc get_qtvs
676 givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
677 returnTc (frees, binds)
679 get_qtvs = zonkTcTyVarsAndFV qtvs
682 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
683 -- against, but we don't know the type variables over which we are going to quantify.
684 -- This happens when we have a type signature for a mutually recursive group
687 -> TcTyVarSet -- fv(T)
690 -> TcM ([TcTyVar], -- Variables over which to quantify
692 TcDictBinds) -- Bindings
694 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
695 = tcSimplCheck doc get_qtvs givens wanted_lie
697 -- Figure out which type variables to quantify over
698 -- You might think it should just be the signature tyvars,
699 -- but in bizarre cases you can get extra ones
700 -- f :: forall a. Num a => a -> a
701 -- f x = fst (g (x, head [])) + 1
703 -- Here we infer g :: forall a b. a -> b -> (b,a)
704 -- We don't want g to be monomorphic in b just because
705 -- f isn't quantified over b.
706 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
708 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenNF_Tc` \ all_tvs' ->
709 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
711 qtvs = all_tvs' `minusVarSet` gbl_tvs
712 -- We could close gbl_tvs, but its not necessary for
713 -- soundness, and it'll only affect which tyvars, not which
714 -- dictionaries, we quantify over
719 Here is the workhorse function for all three wrappers.
722 tcSimplCheck doc get_qtvs givens wanted_lie
723 = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
725 -- Complain about any irreducible ones
726 complainCheck doc givens irreds `thenNF_Tc_`
729 returnTc (qtvs, mkLIE frees, binds)
732 ip_set = mkNameSet (ipNamesOfInsts givens)
734 check_loop givens wanteds
736 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
737 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
738 get_qtvs `thenNF_Tc` \ qtvs' ->
742 -- When checking against a given signature we always reduce
743 -- until we find a match against something given, or can't reduce
744 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
745 | otherwise = ReduceMe
747 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
750 if no_improvement then
751 returnTc (varSetElems qtvs', frees, binds, irreds)
753 check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
754 returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
758 %************************************************************************
760 \subsection{tcSimplifyRestricted}
762 %************************************************************************
765 tcSimplifyRestricted -- Used for restricted binding groups
766 -- i.e. ones subject to the monomorphism restriction
768 -> TcTyVarSet -- Free in the type of the RHSs
769 -> LIE -- Free in the RHSs
770 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
772 TcDictBinds) -- Bindings
774 tcSimplifyRestricted doc tau_tvs wanted_lie
775 = -- First squash out all methods, to find the constrained tyvars
776 -- We can't just take the free vars of wanted_lie because that'll
777 -- have methods that may incidentally mention entirely unconstrained variables
778 -- e.g. a call to f :: Eq a => a -> b -> b
779 -- Here, b is unconstrained. A good example would be
781 -- We want to infer the polymorphic type
782 -- foo :: forall b. b -> b
784 wanteds = lieToList wanted_lie
785 try_me inst = ReduceMe -- Reduce as far as we can. Don't stop at
786 -- dicts; the idea is to get rid of as many type
787 -- variables as possible, and we don't want to stop
788 -- at (say) Monad (ST s), because that reduces
789 -- immediately, with no constraint on s.
791 simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
793 -- Next, figure out the tyvars we will quantify over
794 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
795 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
797 constrained_tvs = tyVarsOfInsts constrained_dicts
798 qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
799 `minusVarSet` constrained_tvs
802 -- The first step may have squashed more methods than
803 -- necessary, so try again, this time knowing the exact
804 -- set of type variables to quantify over.
806 -- We quantify only over constraints that are captured by qtvs;
807 -- these will just be a subset of non-dicts. This in contrast
808 -- to normal inference (using isFreeWhenInferring) in which we quantify over
809 -- all *non-inheritable* constraints too. This implements choice
810 -- (B) under "implicit parameter and monomorphism" above.
812 -- Remember that we may need to do *some* simplification, to
813 -- (for example) squash {Monad (ST s)} into {}. It's not enough
814 -- just to float all constraints
815 mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
817 try_me inst | isFreeWrtTyVars qtvs inst = Free
818 | otherwise = ReduceMe
820 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
821 ASSERT( no_improvement )
822 ASSERT( null irreds )
823 -- No need to loop because simpleReduceLoop will have
824 -- already done any improvement necessary
826 returnTc (varSetElems qtvs, mkLIE frees, binds)
830 %************************************************************************
832 \subsection{tcSimplifyToDicts}
834 %************************************************************************
836 On the LHS of transformation rules we only simplify methods and constants,
837 getting dictionaries. We want to keep all of them unsimplified, to serve
838 as the available stuff for the RHS of the rule.
840 The same thing is used for specialise pragmas. Consider
843 {-# SPECIALISE f :: Int -> Int #-}
846 The type checker generates a binding like:
848 f_spec = (f :: Int -> Int)
850 and we want to end up with
852 f_spec = _inline_me_ (f Int dNumInt)
854 But that means that we must simplify the Method for f to (f Int dNumInt)!
855 So tcSimplifyToDicts squeezes out all Methods.
857 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
859 fromIntegral :: (Integral a, Num b) => a -> b
860 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
862 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
866 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
868 because the scsel will mess up matching. Instead we want
870 forall dIntegralInt, dNumInt.
871 fromIntegral Int Int dIntegralInt dNumInt = id Int
873 Hence "DontReduce NoSCs"
876 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
877 tcSimplifyToDicts wanted_lie
878 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
879 -- Since try_me doesn't look at types, we don't need to
880 -- do any zonking, so it's safe to call reduceContext directly
882 returnTc (irreds, binds)
885 doc = text "tcSimplifyToDicts"
886 wanteds = lieToList wanted_lie
888 -- Reduce methods and lits only; stop as soon as we get a dictionary
889 try_me inst | isDict inst = DontReduce NoSCs
890 | otherwise = ReduceMe
894 %************************************************************************
896 \subsection{Filtering at a dynamic binding}
898 %************************************************************************
903 we must discharge all the ?x constraints from B. We also do an improvement
904 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
906 Actually, the constraints from B might improve the types in ?x. For example
908 f :: (?x::Int) => Char -> Char
911 then the constraint (?x::Int) arising from the call to f will
912 force the binding for ?x to be of type Int.
915 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
917 -> TcM (LIE, TcDictBinds)
918 tcSimplifyIPs given_ips wanted_lie
919 = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
920 returnTc (mkLIE frees, binds)
922 doc = text "tcSimplifyIPs" <+> ppr given_ips
923 wanteds = lieToList wanted_lie
924 ip_set = mkNameSet (ipNamesOfInsts given_ips)
926 -- Simplify any methods that mention the implicit parameter
927 try_me inst | isFreeWrtIPs ip_set inst = Free
928 | otherwise = ReduceMe
930 simpl_loop givens wanteds
931 = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
932 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
934 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
936 if no_improvement then
937 ASSERT( null irreds )
938 returnTc (frees, binds)
940 simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
941 returnTc (frees1, binds `AndMonoBinds` binds1)
945 %************************************************************************
947 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
949 %************************************************************************
951 When doing a binding group, we may have @Insts@ of local functions.
952 For example, we might have...
954 let f x = x + 1 -- orig local function (overloaded)
955 f.1 = f Int -- two instances of f
960 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
961 where @f@ is in scope; those @Insts@ must certainly not be passed
962 upwards towards the top-level. If the @Insts@ were binding-ified up
963 there, they would have unresolvable references to @f@.
965 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
966 For each method @Inst@ in the @init_lie@ that mentions one of the
967 @Ids@, we create a binding. We return the remaining @Insts@ (in an
968 @LIE@), as well as the @HsBinds@ generated.
971 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
973 bindInstsOfLocalFuns init_lie local_ids
974 | null overloaded_ids
976 = returnTc (init_lie, EmptyMonoBinds)
979 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
980 ASSERT( null irreds )
981 returnTc (mkLIE frees, binds)
983 doc = text "bindInsts" <+> ppr local_ids
984 wanteds = lieToList init_lie
985 overloaded_ids = filter is_overloaded local_ids
986 is_overloaded id = isOverloadedTy (idType id)
988 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
989 -- so it's worth building a set, so that
990 -- lookup (in isMethodFor) is faster
992 try_me inst | isMethodFor overloaded_set inst = ReduceMe
997 %************************************************************************
999 \subsection{Data types for the reduction mechanism}
1001 %************************************************************************
1003 The main control over context reduction is here
1007 = ReduceMe -- Try to reduce this
1008 -- If there's no instance, behave exactly like
1009 -- DontReduce: add the inst to
1010 -- the irreductible ones, but don't
1011 -- produce an error message of any kind.
1012 -- It might be quite legitimate such as (Eq a)!
1014 | DontReduce WantSCs -- Return as irreducible
1016 | DontReduceUnlessConstant -- Return as irreducible unless it can
1017 -- be reduced to a constant in one step
1019 | Free -- Return as free
1021 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1022 -- of a predicate when adding it to the avails
1028 type RedState = (Avails, -- What's available
1029 [Inst]) -- Insts for which try_me returned Free
1031 type Avails = FiniteMap Inst Avail
1034 = Irred -- Used for irreducible dictionaries,
1035 -- which are going to be lambda bound
1037 | BoundTo TcId -- Used for dictionaries for which we have a binding
1038 -- e.g. those "given" in a signature
1040 | NoRhs -- Used for Insts like (CCallable f)
1041 -- where no witness is required.
1043 | Rhs -- Used when there is a RHS
1045 [Inst] -- Insts free in the RHS; we need these too
1047 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
1048 | (inst,avail) <- fmToList avails ]
1050 instance Outputable Avail where
1053 pprAvail NoRhs = text "<no rhs>"
1054 pprAvail Irred = text "Irred"
1055 pprAvail (BoundTo x) = text "Bound to" <+> ppr x
1056 pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
1059 Extracting the bindings from a bunch of Avails.
1060 The bindings do *not* come back sorted in dependency order.
1061 We assume that they'll be wrapped in a big Rec, so that the
1062 dependency analyser can sort them out later
1066 bindsAndIrreds :: Avails
1068 -> (TcDictBinds, -- Bindings
1069 [Inst]) -- Irreducible ones
1071 bindsAndIrreds avails wanteds
1072 = go avails EmptyMonoBinds [] wanteds
1074 go avails binds irreds [] = (binds, irreds)
1076 go avails binds irreds (w:ws)
1077 = case lookupFM avails w of
1078 Nothing -> -- Free guys come out here
1079 -- (If we didn't do addFree we could use this as the
1080 -- criterion for free-ness, and pick up the free ones here too)
1081 go avails binds irreds ws
1083 Just NoRhs -> go avails binds irreds ws
1085 Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
1087 Just (BoundTo id) -> go avails new_binds irreds ws
1089 -- For implicit parameters, all occurrences share the same
1090 -- Id, so there is no need for synonym bindings
1091 -- ** BUT THIS TEST IS NEEDED FOR DICTS TOO ** (not sure why)
1092 new_binds | new_id == id = binds
1093 | otherwise = addBind binds new_id (HsVar id)
1096 Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
1099 avails' = addToFM avails w (BoundTo id)
1101 addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
1105 %************************************************************************
1107 \subsection[reduce]{@reduce@}
1109 %************************************************************************
1111 When the "what to do" predicate doesn't depend on the quantified type variables,
1112 matters are easier. We don't need to do any zonking, unless the improvement step
1113 does something, in which case we zonk before iterating.
1115 The "given" set is always empty.
1118 simpleReduceLoop :: SDoc
1119 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1121 -> TcM ([Inst], -- Free
1123 [Inst]) -- Irreducible
1125 simpleReduceLoop doc try_me wanteds
1126 = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
1127 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
1128 if no_improvement then
1129 returnTc (frees, binds, irreds)
1131 simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
1132 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1138 reduceContext :: SDoc
1139 -> (Inst -> WhatToDo)
1142 -> NF_TcM (Bool, -- True <=> improve step did no unification
1144 TcDictBinds, -- Dictionary bindings
1145 [Inst]) -- Irreducible
1147 reduceContext doc try_me givens wanteds
1149 traceTc (text "reduceContext" <+> (vcat [
1150 text "----------------------",
1152 text "given" <+> ppr givens,
1153 text "wanted" <+> ppr wanteds,
1154 text "----------------------"
1157 -- Build the Avail mapping from "givens"
1158 foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
1161 reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
1163 -- Do improvement, using everything in avails
1164 -- In particular, avails includes all superclasses of everything
1165 tcImprove avails `thenTc` \ no_improvement ->
1167 traceTc (text "reduceContext end" <+> (vcat [
1168 text "----------------------",
1170 text "given" <+> ppr givens,
1171 text "wanted" <+> ppr wanteds,
1173 text "avails" <+> pprAvails avails,
1174 text "frees" <+> ppr frees,
1175 text "no_improvement =" <+> ppr no_improvement,
1176 text "----------------------"
1179 (binds, irreds) = bindsAndIrreds avails wanteds
1181 returnTc (no_improvement, frees, binds, irreds)
1184 = tcGetInstEnv `thenTc` \ inst_env ->
1186 preds = [ (pred, pp_loc)
1187 | inst <- keysFM avails,
1188 let pp_loc = pprInstLoc (instLoc inst),
1189 pred <- predsOfInst inst,
1192 -- Avails has all the superclasses etc (good)
1193 -- It also has all the intermediates of the deduction (good)
1194 -- It does not have duplicates (good)
1195 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1196 -- so that improve will see them separate
1197 eqns = improve (classInstEnv inst_env) preds
1202 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
1203 mapTc_ unify eqns `thenTc_`
1206 unify ((qtvs, t1, t2), doc)
1207 = tcAddErrCtxt doc $
1208 tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
1209 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1212 The main context-reduction function is @reduce@. Here's its game plan.
1215 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1216 -- along with its depth
1217 -> (Inst -> WhatToDo)
1224 try_me: given an inst, this function returns
1226 DontReduce return this in "irreds"
1227 Free return this in "frees"
1229 wanteds: The list of insts to reduce
1230 state: An accumulating parameter of type RedState
1231 that contains the state of the algorithm
1233 It returns a RedState.
1235 The (n,stack) pair is just used for error reporting.
1236 n is always the depth of the stack.
1237 The stack is the stack of Insts being reduced: to produce X
1238 I had to produce Y, to produce Y I had to produce Z, and so on.
1241 reduceList (n,stack) try_me wanteds state
1242 | n > opt_MaxContextReductionDepth
1243 = failWithTc (reduceDepthErr n stack)
1249 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1254 go [] state = returnTc state
1255 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
1258 -- Base case: we're done!
1259 reduce stack try_me wanted state
1260 -- It's the same as an existing inst, or a superclass thereof
1261 | isAvailable state wanted
1265 = case try_me wanted of {
1267 DontReduce want_scs -> addIrred want_scs state wanted
1269 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1270 -- First, see if the inst can be reduced to a constant in one step
1271 try_simple (addIrred AddSCs) -- Assume want superclasses
1273 ; Free -> -- It's free so just chuck it upstairs
1274 -- First, see if the inst can be reduced to a constant in one step
1277 ; ReduceMe -> -- It should be reduced
1278 lookupInst wanted `thenNF_Tc` \ lookup_result ->
1279 case lookup_result of
1280 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
1281 addWanted state' wanted rhs wanteds'
1282 SimpleInst rhs -> addWanted state wanted rhs []
1284 NoInstance -> -- No such instance!
1285 -- Add it and its superclasses
1286 addIrred AddSCs state wanted
1290 try_simple do_this_otherwise
1291 = lookupInst wanted `thenNF_Tc` \ lookup_result ->
1292 case lookup_result of
1293 SimpleInst rhs -> addWanted state wanted rhs []
1294 other -> do_this_otherwise state wanted
1299 isAvailable :: RedState -> Inst -> Bool
1300 isAvailable (avails, _) wanted = wanted `elemFM` avails
1301 -- NB: the Ord instance of Inst compares by the class/type info
1302 -- *not* by unique. So
1303 -- d1::C Int == d2::C Int
1305 -------------------------
1306 addFree :: RedState -> Inst -> NF_TcM RedState
1307 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1308 -- to avails, so that any other equal Insts will be commoned up right
1309 -- here rather than also being tossed upstairs. This is really just
1310 -- an optimisation, and perhaps it is more trouble that it is worth,
1311 -- as the following comments show!
1313 -- NB1: do *not* add superclasses. If we have
1316 -- but a is not bound here, then we *don't* want to derive
1317 -- dn from df here lest we lose sharing.
1319 -- NB2: do *not* add the Inst to avails at all if it's a method.
1320 -- The following situation shows why this is bad:
1321 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1322 -- From an application (truncate f i) we get
1323 -- t1 = truncate at f
1325 -- If we have also have a second occurrence of truncate, we get
1326 -- t3 = truncate at f
1328 -- When simplifying with i,f free, we might still notice that
1329 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1330 -- will continue to float out!
1331 -- Solution: never put methods in avail till they are captured
1332 -- in which case addFree isn't used
1334 -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1335 -- than BoundTo, else we end up with bogus bindings.
1336 -- c.f. instBindingRequired in addWanted
1337 addFree (avails, frees) free
1338 | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1339 | otherwise = returnNF_Tc (avails, free:frees)
1341 avail | instBindingRequired free = BoundTo (instToId free)
1344 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1345 addWanted state@(avails, frees) wanted rhs_expr wanteds
1346 -- Do *not* add superclasses as well. Here's an example of why not
1347 -- class Eq a => Foo a b
1348 -- instance Eq a => Foo [a] a
1349 -- If we are reducing
1351 -- we'll first deduce that it holds (via the instance decl). We
1352 -- must not then overwrite the Eq t constraint with a superclass selection!
1353 -- ToDo: this isn't entirely unsatisfactory, because
1354 -- we may also lose some entirely-legitimate sharing this way
1356 = ASSERT( not (isAvailable state wanted) )
1357 returnNF_Tc (addToFM avails wanted avail, frees)
1359 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1360 | otherwise = ASSERT( null wanteds ) NoRhs
1362 addGiven :: RedState -> Inst -> NF_TcM RedState
1363 addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
1365 addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
1366 addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
1367 addIrred AddSCs state irred = addAvailAndSCs state irred Irred
1369 addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
1370 addAvailAndSCs (avails, frees) wanted avail
1371 = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
1372 returnNF_Tc (avails', frees)
1374 ---------------------
1375 add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
1376 add_avail_and_scs avails wanted avail
1377 = add_scs (addToFM avails wanted avail) wanted
1379 add_scs :: Avails -> Inst -> NF_TcM Avails
1380 -- Add all the superclasses of the Inst to Avails
1381 -- Invariant: the Inst is already in Avails.
1384 | not (isClassDict dict)
1385 = returnNF_Tc avails
1387 | otherwise -- It is a dictionary
1388 = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
1389 foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1391 (clas, tys) = getDictClassTys dict
1392 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1393 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1395 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1396 = case lookupFM avails sc_dict of
1397 Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
1398 other -> add_avail_and_scs avails sc_dict avail
1400 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1401 avail = Rhs sc_sel_rhs [dict]
1404 Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
1405 and want to deduce (d2:C [a]) where
1407 class Ord a => C a where
1408 instance Ord a => C [a] where ...
1410 Then we'll use the instance decl to deduce C [a] and then add the
1411 superclasses of C [a] to avails. But we must not overwrite the binding
1412 for d1:Ord a (which is given) with a superclass selection or we'll just
1413 build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
1417 %************************************************************************
1419 \section{tcSimplifyTop: defaulting}
1421 %************************************************************************
1424 If a dictionary constrains a type variable which is
1425 * not mentioned in the environment
1426 * and not mentioned in the type of the expression
1427 then it is ambiguous. No further information will arise to instantiate
1428 the type variable; nor will it be generalised and turned into an extra
1429 parameter to a function.
1431 It is an error for this to occur, except that Haskell provided for
1432 certain rules to be applied in the special case of numeric types.
1434 * at least one of its classes is a numeric class, and
1435 * all of its classes are numeric or standard
1436 then the type variable can be defaulted to the first type in the
1437 default-type list which is an instance of all the offending classes.
1439 So here is the function which does the work. It takes the ambiguous
1440 dictionaries and either resolves them (producing bindings) or
1441 complains. It works by splitting the dictionary list by type
1442 variable, and using @disambigOne@ to do the real business.
1444 @tcSimplifyTop@ is called once per module to simplify all the constant
1445 and ambiguous Insts.
1447 We need to be careful of one case. Suppose we have
1449 instance Num a => Num (Foo a b) where ...
1451 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1452 to (Num x), and default x to Int. But what about y??
1454 It's OK: the final zonking stage should zap y to (), which is fine.
1458 tcSimplifyTop :: LIE -> TcM TcDictBinds
1459 tcSimplifyTop wanted_lie
1460 = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1461 ASSERT( null frees )
1464 -- All the non-std ones are definite errors
1465 (stds, non_stds) = partition isStdClassTyVarDict irreds
1467 -- Group by type variable
1468 std_groups = equivClasses cmp_by_tyvar stds
1470 -- Pick the ones which its worth trying to disambiguate
1471 (std_oks, std_bads) = partition worth_a_try std_groups
1473 -- Have a try at disambiguation
1474 -- if the type variable isn't bound
1475 -- up with one of the non-standard classes
1476 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1477 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1479 -- Collect together all the bad guys
1480 bad_guys = non_stds ++ concat std_bads
1482 -- Disambiguate the ones that look feasible
1483 mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
1485 -- And complain about the ones that don't
1486 -- This group includes both non-existent instances
1487 -- e.g. Num (IO a) and Eq (Int -> Int)
1488 -- and ambiguous dictionaries
1490 addTopAmbigErrs bad_guys `thenNF_Tc_`
1492 returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1494 wanteds = lieToList wanted_lie
1495 try_me inst = ReduceMe
1497 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1499 get_tv d = case getDictClassTys d of
1500 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1501 get_clas d = case getDictClassTys d of
1502 (clas, [ty]) -> clas
1505 @disambigOne@ assumes that its arguments dictionaries constrain all
1506 the same type variable.
1508 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1509 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1510 the most common use of defaulting is code like:
1512 _ccall_ foo `seqPrimIO` bar
1514 Since we're not using the result of @foo@, the result if (presumably)
1518 disambigGroup :: [Inst] -- All standard classes of form (C a)
1522 | any isNumericClass classes -- Guaranteed all standard classes
1523 -- see comment at the end of function for reasons as to
1524 -- why the defaulting mechanism doesn't apply to groups that
1525 -- include CCallable or CReturnable dicts.
1526 && not (any isCcallishClass classes)
1527 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1528 -- SO, TRY DEFAULT TYPES IN ORDER
1530 -- Failure here is caused by there being no type in the
1531 -- default list which can satisfy all the ambiguous classes.
1532 -- For example, if Real a is reqd, but the only type in the
1533 -- default list is Int.
1534 tcGetDefaultTys `thenNF_Tc` \ default_tys ->
1536 try_default [] -- No defaults work, so fail
1539 try_default (default_ty : default_tys)
1540 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1541 -- default_tys instead
1542 tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
1545 theta = [mkClassPred clas [default_ty] | clas <- classes]
1547 -- See if any default works, and if so bind the type variable to it
1548 -- If not, add an AmbigErr
1549 recoverTc (addAmbigErrs dicts `thenNF_Tc_`
1550 returnTc EmptyMonoBinds) $
1552 try_default default_tys `thenTc` \ chosen_default_ty ->
1554 -- Bind the type variable and reduce the context, for real this time
1555 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
1556 simpleReduceLoop (text "disambig" <+> ppr dicts)
1557 try_me dicts `thenTc` \ (frees, binds, ambigs) ->
1558 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1559 warnDefault dicts chosen_default_ty `thenTc_`
1562 | all isCreturnableClass classes
1563 = -- Default CCall stuff to (); we don't even both to check that () is an
1564 -- instance of CReturnable, because we know it is.
1565 unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
1566 returnTc EmptyMonoBinds
1568 | otherwise -- No defaults
1569 = addAmbigErrs dicts `thenNF_Tc_`
1570 returnTc EmptyMonoBinds
1573 try_me inst = ReduceMe -- This reduce should not fail
1574 tyvar = get_tv (head dicts) -- Should be non-empty
1575 classes = map get_clas dicts
1578 [Aside - why the defaulting mechanism is turned off when
1579 dealing with arguments and results to ccalls.
1581 When typechecking _ccall_s, TcExpr ensures that the external
1582 function is only passed arguments (and in the other direction,
1583 results) of a restricted set of 'native' types. This is
1584 implemented via the help of the pseudo-type classes,
1585 @CReturnable@ (CR) and @CCallable@ (CC.)
1587 The interaction between the defaulting mechanism for numeric
1588 values and CC & CR can be a bit puzzling to the user at times.
1597 What type has 'x' got here? That depends on the default list
1598 in operation, if it is equal to Haskell 98's default-default
1599 of (Integer, Double), 'x' has type Double, since Integer
1600 is not an instance of CR. If the default list is equal to
1601 Haskell 1.4's default-default of (Int, Double), 'x' has type
1604 To try to minimise the potential for surprises here, the
1605 defaulting mechanism is turned off in the presence of
1606 CCallable and CReturnable.
1611 %************************************************************************
1613 \subsection[simple]{@Simple@ versions}
1615 %************************************************************************
1617 Much simpler versions when there are no bindings to make!
1619 @tcSimplifyThetas@ simplifies class-type constraints formed by
1620 @deriving@ declarations and when specialising instances. We are
1621 only interested in the simplified bunch of class/type constraints.
1623 It simplifies to constraints of the form (C a b c) where
1624 a,b,c are type variables. This is required for the context of
1625 instance declarations.
1628 tcSimplifyThetas :: ThetaType -- Wanted
1629 -> TcM ThetaType -- Needed
1631 tcSimplifyThetas wanteds
1632 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
1633 reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
1635 -- For multi-param Haskell, check that the returned dictionaries
1636 -- don't have any of the form (C Int Bool) for which
1637 -- we expect an instance here
1638 -- For Haskell 98, check that all the constraints are of the form C a,
1639 -- where a is a type variable
1640 bad_guys | glaExts = [pred | pred <- irreds,
1641 isEmptyVarSet (tyVarsOfPred pred)]
1642 | otherwise = [pred | pred <- irreds,
1643 not (isTyVarClassPred pred)]
1645 if null bad_guys then
1648 mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
1652 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1653 used with \tr{default} declarations. We are only interested in
1654 whether it worked or not.
1657 tcSimplifyCheckThetas :: ThetaType -- Given
1658 -> ThetaType -- Wanted
1661 tcSimplifyCheckThetas givens wanteds
1662 = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
1666 mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
1672 type AvailsSimple = FiniteMap PredType Bool
1673 -- True => irreducible
1674 -- False => given, or can be derived from a given or from an irreducible
1676 reduceSimple :: ThetaType -- Given
1677 -> ThetaType -- Wanted
1678 -> NF_TcM ThetaType -- Irreducible
1680 reduceSimple givens wanteds
1681 = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
1682 returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
1684 givens_fm = foldl addNonIrred emptyFM givens
1686 reduce_simple :: (Int,ThetaType) -- Stack
1689 -> NF_TcM AvailsSimple
1691 reduce_simple (n,stack) avails wanteds
1694 go avails [] = returnNF_Tc avails
1695 go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
1698 reduce_simple_help stack givens wanted
1699 | wanted `elemFM` givens
1700 = returnNF_Tc givens
1702 | Just (clas, tys) <- getClassPredTys_maybe wanted
1703 = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
1705 Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
1706 Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1709 = returnNF_Tc (addSimpleIrred givens wanted)
1711 addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
1712 addSimpleIrred givens pred
1713 = addSCs (addToFM givens pred True) pred
1715 addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
1716 addNonIrred givens pred
1717 = addSCs (addToFM givens pred False) pred
1720 | not (isClassPred pred) = givens
1721 | otherwise = foldl add givens sc_theta
1723 Just (clas,tys) = getClassPredTys_maybe pred
1724 (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1725 sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1728 = case lookupFM givens ct of
1729 Nothing -> -- Add it and its superclasses
1730 addSCs (addToFM givens ct False) ct
1732 Just True -> -- Set its flag to False; superclasses already done
1733 addToFM givens ct False
1735 Just False -> -- Already done
1741 %************************************************************************
1743 \section{Errors and contexts}
1745 %************************************************************************
1747 ToDo: for these error messages, should we note the location as coming
1748 from the insts, or just whatever seems to be around in the monad just
1752 groupInsts :: [Inst] -> [[Inst]]
1753 -- Group together insts with the same origin
1754 -- We want to report them together in error messages
1756 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1758 -- (It may seem a bit crude to compare the error messages,
1759 -- but it makes sure that we combine just what the user sees,
1760 -- and it avoids need equality on InstLocs.)
1761 (friends, others) = partition is_friend insts
1762 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1763 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1766 addTopAmbigErrs dicts
1767 = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
1768 mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
1769 mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
1772 fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1773 (tidy_env, tidy_dicts) = tidyInsts dicts
1774 (bad_ips, non_ips) = partition is_ip tidy_dicts
1775 (no_insts, ambigs) = partition no_inst non_ips
1776 is_ip d = any isIPPred (predsOfInst d)
1777 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1780 plural xs = char 's'
1782 addTopIPErrs tidy_env tidy_dicts
1783 = addInstErrTcM (instLoc (head tidy_dicts))
1785 ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1787 -- Used for top-level irreducibles
1788 addTopInstanceErrs tidy_env tidy_dicts
1789 = addInstErrTcM (instLoc (head tidy_dicts))
1791 ptext SLIT("No instance") <> plural tidy_dicts <+>
1792 ptext SLIT("for") <+> pprInsts tidy_dicts)
1795 = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1797 (tidy_env, tidy_dicts) = tidyInsts dicts
1799 addAmbigErr tidy_env tidy_dict
1800 = addInstErrTcM (instLoc tidy_dict)
1802 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1803 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1805 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1807 warnDefault dicts default_ty
1808 = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
1809 tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1812 (_, tidy_dicts) = tidyInsts dicts
1813 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1814 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1815 quotes (ppr default_ty),
1816 pprInstsInFull tidy_dicts]
1818 complainCheck doc givens irreds
1819 = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
1820 mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
1823 given_dicts = filter isDict givens
1824 -- Filter out methods, which are only added to
1825 -- the given set as an optimisation
1827 addNoInstanceErrs what_doc givens dicts
1828 = tcGetInstEnv `thenNF_Tc` \ inst_env ->
1830 (tidy_env1, tidy_givens) = tidyInsts givens
1831 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
1833 doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1834 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1836 ptext SLIT("Probable fix:"),
1840 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1841 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1844 -- The error message when we don't find a suitable instance
1845 -- is complicated by the fact that sometimes this is because
1846 -- there is no instance, and sometimes it's because there are
1847 -- too many instances (overlap). See the comments in TcEnv.lhs
1848 -- with the InstEnv stuff.
1851 | not ambig_overlap = empty
1853 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1854 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1855 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1857 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1858 ptext SLIT("to the") <+> what_doc]
1860 fix2 | null instance_dicts
1863 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1865 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1866 -- Insts for which it is worth suggesting an adding an instance declaration
1867 -- Exclude implicit parameters, and tyvar dicts
1869 -- Checks for the ambiguous case when we have overlapping instances
1870 ambig_overlap = any ambig_overlap1 dicts
1873 = case lookupInstEnv inst_env clas tys of
1874 NoMatch ambig -> ambig
1878 (clas,tys) = getDictClassTys dict
1880 addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
1882 -- Used for the ...Thetas variants; all top level
1884 = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
1886 reduceDepthErr n stack
1887 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1888 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1889 nest 4 (pprInstsInFull stack)]
1891 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1893 -----------------------------------------------
1895 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1896 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])