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 HsSyn ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
21 import TcHsSyn ( TcExpr, TcId,
22 TcMonoBinds, TcDictBinds
26 import Inst ( lookupInst, lookupSimpleInst, LookupInstResult(..),
27 tyVarsOfInst, predsOfInsts, predsOfInst,
29 isStdClassTyVarDict, isMethodFor,
30 instToId, tyVarsOfInsts,
31 ipNamesOfInsts, ipNamesOfInst,
32 instBindingRequired, instCanBeGeneralised,
34 getDictClassTys, isTyVarDict,
35 instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
36 Inst, LIE, pprInsts, pprInstsInFull,
39 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
40 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
42 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
43 import TcType ( TcTyVar, TcTyVarSet, ThetaType, PredType,
44 mkClassPred, isOverloadedTy,
45 mkTyVarTy, tcGetTyVar, isTyVarClassPred,
46 tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
47 inheritablePred, predHasFDs )
49 import NameSet ( NameSet, mkNameSet, elemNameSet )
50 import Class ( classBigSig )
51 import FunDeps ( oclose, grow, improve, pprEquationDoc )
52 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
54 import Subst ( mkTopTyVarSubst, substTheta, substTy )
55 import TysWiredIn ( unitTy )
59 import ListSetOps ( equivClasses )
60 import Util ( zipEqual )
61 import List ( partition )
66 %************************************************************************
70 %************************************************************************
72 --------------------------------------
73 Notes on quantification
74 --------------------------------------
76 Suppose we are about to do a generalisation step.
81 C the constraints from that RHS
83 The game is to figure out
85 Q the set of type variables over which to quantify
86 Ct the constraints we will *not* quantify over
87 Cq the constraints we will quantify over
89 So we're going to infer the type
93 and float the constraints Ct further outwards.
95 Here are the things that *must* be true:
97 (A) Q intersect fv(G) = EMPTY limits how big Q can be
98 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
100 (A) says we can't quantify over a variable that's free in the
101 environment. (B) says we must quantify over all the truly free
102 variables in T, else we won't get a sufficiently general type. We do
103 not *need* to quantify over any variable that is fixed by the free
104 vars of the environment G.
106 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
108 Example: class H x y | x->y where ...
110 fv(G) = {a} C = {H a b, H c d}
113 (A) Q intersect {a} is empty
114 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
116 So Q can be {c,d}, {b,c,d}
118 Other things being equal, however, we'd like to quantify over as few
119 variables as possible: smaller types, fewer type applications, more
120 constraints can get into Ct instead of Cq.
123 -----------------------------------------
126 fv(T) the free type vars of T
128 oclose(vs,C) The result of extending the set of tyvars vs
129 using the functional dependencies from C
131 grow(vs,C) The result of extend the set of tyvars vs
132 using all conceivable links from C.
134 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
135 Then grow(vs,C) = {a,b,c}
137 Note that grow(vs,C) `superset` grow(vs,simplify(C))
138 That is, simplfication can only shrink the result of grow.
141 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
142 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
145 -----------------------------------------
149 Here's a good way to choose Q:
151 Q = grow( fv(T), C ) \ oclose( fv(G), C )
153 That is, quantify over all variable that that MIGHT be fixed by the
154 call site (which influences T), but which aren't DEFINITELY fixed by
155 G. This choice definitely quantifies over enough type variables,
156 albeit perhaps too many.
158 Why grow( fv(T), C ) rather than fv(T)? Consider
160 class H x y | x->y where ...
165 If we used fv(T) = {c} we'd get the type
167 forall c. H c d => c -> b
169 And then if the fn was called at several different c's, each of
170 which fixed d differently, we'd get a unification error, because
171 d isn't quantified. Solution: quantify d. So we must quantify
172 everything that might be influenced by c.
174 Why not oclose( fv(T), C )? Because we might not be able to see
175 all the functional dependencies yet:
177 class H x y | x->y where ...
178 instance H x y => Eq (T x y) where ...
183 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
184 apparent yet, and that's wrong. We must really quantify over d too.
187 There really isn't any point in quantifying over any more than
188 grow( fv(T), C ), because the call sites can't possibly influence
189 any other type variables.
193 --------------------------------------
195 --------------------------------------
197 It's very hard to be certain when a type is ambiguous. Consider
201 instance H x y => K (x,y)
203 Is this type ambiguous?
204 forall a b. (K (a,b), Eq b) => a -> a
206 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
207 now we see that a fixes b. So we can't tell about ambiguity for sure
208 without doing a full simplification. And even that isn't possible if
209 the context has some free vars that may get unified. Urgle!
211 Here's another example: is this ambiguous?
212 forall a b. Eq (T b) => a -> a
213 Not if there's an insance decl (with no context)
214 instance Eq (T b) where ...
216 You may say of this example that we should use the instance decl right
217 away, but you can't always do that:
219 class J a b where ...
220 instance J Int b where ...
222 f :: forall a b. J a b => a -> a
224 (Notice: no functional dependency in J's class decl.)
225 Here f's type is perfectly fine, provided f is only called at Int.
226 It's premature to complain when meeting f's signature, or even
227 when inferring a type for f.
231 However, we don't *need* to report ambiguity right away. It'll always
232 show up at the call site.... and eventually at main, which needs special
233 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
235 So here's the plan. We WARN about probable ambiguity if
237 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
239 (all tested before quantification).
240 That is, all the type variables in Cq must be fixed by the the variables
241 in the environment, or by the variables in the type.
243 Notice that we union before calling oclose. Here's an example:
245 class J a b c | a b -> c
249 forall b c. (J a b c) => b -> b
251 Only if we union {a} from G with {b} from T before using oclose,
252 do we see that c is fixed.
254 It's a bit vague exactly which C we should use for this oclose call. If we
255 don't fix enough variables we might complain when we shouldn't (see
256 the above nasty example). Nothing will be perfect. That's why we can
257 only issue a warning.
260 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
262 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
264 then c is a "bubble"; there's no way it can ever improve, and it's
265 certainly ambiguous. UNLESS it is a constant (sigh). And what about
270 instance H x y => K (x,y)
272 Is this type ambiguous?
273 forall a b. (K (a,b), Eq b) => a -> a
275 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
276 is a "bubble" that's a set of constraints
278 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
280 Hence another idea. To decide Q start with fv(T) and grow it
281 by transitive closure in Cq (no functional dependencies involved).
282 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
283 The definitely-ambiguous can then float out, and get smashed at top level
284 (which squashes out the constants, like Eq (T a) above)
287 --------------------------------------
288 Notes on principal types
289 --------------------------------------
294 f x = let g y = op (y::Int) in True
296 Here the principal type of f is (forall a. a->a)
297 but we'll produce the non-principal type
298 f :: forall a. C Int => a -> a
301 --------------------------------------
302 Notes on implicit parameters
303 --------------------------------------
305 Question 1: can we "inherit" implicit parameters
306 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
311 where f is *not* a top-level binding.
312 From the RHS of f we'll get the constraint (?y::Int).
313 There are two types we might infer for f:
317 (so we get ?y from the context of f's definition), or
319 f :: (?y::Int) => Int -> Int
321 At first you might think the first was better, becuase then
322 ?y behaves like a free variable of the definition, rather than
323 having to be passed at each call site. But of course, the WHOLE
324 IDEA is that ?y should be passed at each call site (that's what
325 dynamic binding means) so we'd better infer the second.
327 BOTTOM LINE: when *inferring types* you *must* quantify
328 over implicit parameters. See the predicate isFreeWhenInferring.
331 Question 2: type signatures
332 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
333 BUT WATCH OUT: When you supply a type signature, we can't force you
334 to quantify over implicit parameters. For example:
338 This is perfectly reasonable. We do not want to insist on
340 (?x + 1) :: (?x::Int => Int)
342 That would be silly. Here, the definition site *is* the occurrence site,
343 so the above strictures don't apply. Hence the difference between
344 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
345 and tcSimplifyCheckBind (which does not).
347 What about when you supply a type signature for a binding?
348 Is it legal to give the following explicit, user type
349 signature to f, thus:
354 At first sight this seems reasonable, but it has the nasty property
355 that adding a type signature changes the dynamic semantics.
358 (let f x = (x::Int) + ?y
359 in (f 3, f 3 with ?y=5)) with ?y = 6
365 in (f 3, f 3 with ?y=5)) with ?y = 6
369 Indeed, simply inlining f (at the Haskell source level) would change the
372 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
373 semantics for a Haskell program without knowing its typing, so if you
374 change the typing you may change the semantics.
376 To make things consistent in all cases where we are *checking* against
377 a supplied signature (as opposed to inferring a type), we adopt the
380 a signature does not need to quantify over implicit params.
382 [This represents a (rather marginal) change of policy since GHC 5.02,
383 which *required* an explicit signature to quantify over all implicit
384 params for the reasons mentioned above.]
386 But that raises a new question. Consider
388 Given (signature) ?x::Int
389 Wanted (inferred) ?x::Int, ?y::Bool
391 Clearly we want to discharge the ?x and float the ?y out. But
392 what is the criterion that distinguishes them? Clearly it isn't
393 what free type variables they have. The Right Thing seems to be
394 to float a constraint that
395 neither mentions any of the quantified type variables
396 nor any of the quantified implicit parameters
398 See the predicate isFreeWhenChecking.
401 Question 3: monomorphism
402 ~~~~~~~~~~~~~~~~~~~~~~~~
403 There's a nasty corner case when the monomorphism restriction bites:
407 The argument above suggests that we *must* generalise
408 over the ?y parameter, to get
409 z :: (?y::Int) => Int,
410 but the monomorphism restriction says that we *must not*, giving
412 Why does the momomorphism restriction say this? Because if you have
414 let z = x + ?y in z+z
416 you might not expect the addition to be done twice --- but it will if
417 we follow the argument of Question 2 and generalise over ?y.
423 (A) Always generalise over implicit parameters
424 Bindings that fall under the monomorphism restriction can't
428 * Inlining remains valid
429 * No unexpected loss of sharing
430 * But simple bindings like
432 will be rejected, unless you add an explicit type signature
433 (to avoid the monomorphism restriction)
434 z :: (?y::Int) => Int
436 This seems unacceptable
438 (B) Monomorphism restriction "wins"
439 Bindings that fall under the monomorphism restriction can't
441 Always generalise over implicit parameters *except* for bindings
442 that fall under the monomorphism restriction
445 * Inlining isn't valid in general
446 * No unexpected loss of sharing
447 * Simple bindings like
449 accepted (get value of ?y from binding site)
451 (C) Always generalise over implicit parameters
452 Bindings that fall under the monomorphism restriction can't
453 be generalised, EXCEPT for implicit parameters
455 * Inlining remains valid
456 * Unexpected loss of sharing (from the extra generalisation)
457 * Simple bindings like
459 accepted (get value of ?y from occurrence sites)
464 None of these choices seems very satisfactory. But at least we should
465 decide which we want to do.
467 It's really not clear what is the Right Thing To Do. If you see
471 would you expect the value of ?y to be got from the *occurrence sites*
472 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
473 case of function definitions, the answer is clearly the former, but
474 less so in the case of non-fucntion definitions. On the other hand,
475 if we say that we get the value of ?y from the definition site of 'z',
476 then inlining 'z' might change the semantics of the program.
478 Choice (C) really says "the monomorphism restriction doesn't apply
479 to implicit parameters". Which is fine, but remember that every
480 innocent binding 'x = ...' that mentions an implicit parameter in
481 the RHS becomes a *function* of that parameter, called at each
482 use of 'x'. Now, the chances are that there are no intervening 'with'
483 clauses that bind ?y, so a decent compiler should common up all
484 those function calls. So I think I strongly favour (C). Indeed,
485 one could make a similar argument for abolishing the monomorphism
486 restriction altogether.
488 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
492 %************************************************************************
494 \subsection{tcSimplifyInfer}
496 %************************************************************************
498 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
500 1. Compute Q = grow( fvs(T), C )
502 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
503 predicates will end up in Ct; we deal with them at the top level
505 3. Try improvement, using functional dependencies
507 4. If Step 3 did any unification, repeat from step 1
508 (Unification can change the result of 'grow'.)
510 Note: we don't reduce dictionaries in step 2. For example, if we have
511 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
512 after step 2. However note that we may therefore quantify over more
513 type variables than we absolutely have to.
515 For the guts, we need a loop, that alternates context reduction and
516 improvement with unification. E.g. Suppose we have
518 class C x y | x->y where ...
520 and tcSimplify is called with:
522 Then improvement unifies a with b, giving
525 If we need to unify anything, we rattle round the whole thing all over
532 -> TcTyVarSet -- fv(T); type vars
534 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
536 TcDictBinds, -- Bindings
537 [TcId]) -- Dict Ids that must be bound here (zonked)
542 tcSimplifyInfer doc tau_tvs wanted_lie
543 = inferLoop doc (varSetElems tau_tvs)
544 (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
546 -- Check for non-generalisable insts
547 mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
549 returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
551 inferLoop doc tau_tvs wanteds
553 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
554 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
555 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
557 preds = predsOfInsts wanteds'
558 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
561 | isFreeWhenInferring qtvs inst = Free
562 | isClassDict inst = DontReduceUnlessConstant -- Dicts
563 | otherwise = ReduceMe -- Lits and Methods
566 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
569 if no_improvement then
570 returnTc (varSetElems qtvs, frees, binds, irreds)
572 -- If improvement did some unification, we go round again. There
573 -- are two subtleties:
574 -- a) We start again with irreds, not wanteds
575 -- Using an instance decl might have introduced a fresh type variable
576 -- which might have been unified, so we'd get an infinite loop
577 -- if we started again with wanteds! See example [LOOP]
579 -- b) It's also essential to re-process frees, because unification
580 -- might mean that a type variable that looked free isn't now.
582 -- Hence the (irreds ++ frees)
584 -- However, NOTICE that when we are done, we might have some bindings, but
585 -- the final qtvs might be empty. See [NO TYVARS] below.
587 inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
588 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
593 class If b t e r | b t e -> r
596 class Lte a b c | a b -> c where lte :: a -> b -> c
598 instance (Lte a b l,If l b a c) => Max a b c
600 Wanted: Max Z (S x) y
602 Then we'll reduce using the Max instance to:
603 (Lte Z (S x) l, If l (S x) Z y)
604 and improve by binding l->T, after which we can do some reduction
605 on both the Lte and If constraints. What we *can't* do is start again
606 with (Max Z (S x) y)!
610 class Y a b | a -> b where
613 instance Y [[a]] a where
616 k :: X a -> X a -> X a
618 g :: Num a => [X a] -> [X a]
621 h ys = ys ++ map (k (y [[0]])) xs
623 The excitement comes when simplifying the bindings for h. Initially
624 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
625 From this we get t1:=:t2, but also various bindings. We can't forget
626 the bindings (because of [LOOP]), but in fact t1 is what g is
629 The net effect of [NO TYVARS]
632 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
633 isFreeWhenInferring qtvs inst
634 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
635 && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
636 -- (see "Notes on implicit parameters")
638 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
639 -> NameSet -- Quantified implicit parameters
641 isFreeWhenChecking qtvs ips inst
642 = isFreeWrtTyVars qtvs inst
643 && isFreeWrtIPs ips inst
645 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
646 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
650 %************************************************************************
652 \subsection{tcSimplifyCheck}
654 %************************************************************************
656 @tcSimplifyCheck@ is used when we know exactly the set of variables
657 we are going to quantify over. For example, a class or instance declaration.
662 -> [TcTyVar] -- Quantify over these
666 TcDictBinds) -- Bindings
668 -- tcSimplifyCheck is used when checking expression type signatures,
669 -- class decls, instance decls etc.
670 -- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
671 -- It's important that we can float out non-inheritable predicates
672 -- Example: (?x :: Int) is ok!
673 tcSimplifyCheck doc qtvs givens wanted_lie
674 = tcSimplCheck doc get_qtvs
675 givens wanted_lie `thenTc` \ (qtvs', frees, binds) ->
676 returnTc (frees, binds)
678 get_qtvs = zonkTcTyVarsAndFV qtvs
681 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
682 -- against, but we don't know the type variables over which we are going to quantify.
683 -- This happens when we have a type signature for a mutually recursive group
686 -> TcTyVarSet -- fv(T)
689 -> TcM ([TcTyVar], -- Variables over which to quantify
691 TcDictBinds) -- Bindings
693 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
694 = tcSimplCheck doc get_qtvs givens wanted_lie
696 -- Figure out which type variables to quantify over
697 -- You might think it should just be the signature tyvars,
698 -- but in bizarre cases you can get extra ones
699 -- f :: forall a. Num a => a -> a
700 -- f x = fst (g (x, head [])) + 1
702 -- Here we infer g :: forall a b. a -> b -> (b,a)
703 -- We don't want g to be monomorphic in b just because
704 -- f isn't quantified over b.
705 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
707 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenNF_Tc` \ all_tvs' ->
708 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
710 qtvs = all_tvs' `minusVarSet` gbl_tvs
711 -- We could close gbl_tvs, but its not necessary for
712 -- soundness, and it'll only affect which tyvars, not which
713 -- dictionaries, we quantify over
718 Here is the workhorse function for all three wrappers.
721 tcSimplCheck doc get_qtvs givens wanted_lie
722 = check_loop givens (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
724 -- Complain about any irreducible ones
725 complainCheck doc givens irreds `thenNF_Tc_`
728 returnTc (qtvs, mkLIE frees, binds)
731 ip_set = mkNameSet (ipNamesOfInsts givens)
733 check_loop givens wanteds
735 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
736 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
737 get_qtvs `thenNF_Tc` \ qtvs' ->
741 -- When checking against a given signature we always reduce
742 -- until we find a match against something given, or can't reduce
743 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
744 | otherwise = ReduceMe
746 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
749 if no_improvement then
750 returnTc (varSetElems qtvs', frees, binds, irreds)
752 check_loop givens' (irreds ++ frees) `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
753 returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
757 %************************************************************************
759 \subsection{tcSimplifyRestricted}
761 %************************************************************************
764 tcSimplifyRestricted -- Used for restricted binding groups
765 -- i.e. ones subject to the monomorphism restriction
767 -> TcTyVarSet -- Free in the type of the RHSs
768 -> LIE -- Free in the RHSs
769 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
771 TcDictBinds) -- Bindings
773 tcSimplifyRestricted doc tau_tvs wanted_lie
774 = -- First squash out all methods, to find the constrained tyvars
775 -- We can't just take the free vars of wanted_lie because that'll
776 -- have methods that may incidentally mention entirely unconstrained variables
777 -- e.g. a call to f :: Eq a => a -> b -> b
778 -- Here, b is unconstrained. A good example would be
780 -- We want to infer the polymorphic type
781 -- foo :: forall b. b -> b
783 wanteds = lieToList wanted_lie
784 try_me inst = ReduceMe -- Reduce as far as we can. Don't stop at
785 -- dicts; the idea is to get rid of as many type
786 -- variables as possible, and we don't want to stop
787 -- at (say) Monad (ST s), because that reduces
788 -- immediately, with no constraint on s.
790 simpleReduceLoop doc try_me wanteds `thenTc` \ (_, _, constrained_dicts) ->
792 -- Next, figure out the tyvars we will quantify over
793 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenNF_Tc` \ tau_tvs' ->
794 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
796 constrained_tvs = tyVarsOfInsts constrained_dicts
797 qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
798 `minusVarSet` constrained_tvs
801 -- The first step may have squashed more methods than
802 -- necessary, so try again, this time knowing the exact
803 -- set of type variables to quantify over.
805 -- We quantify only over constraints that are captured by qtvs;
806 -- these will just be a subset of non-dicts. This in contrast
807 -- to normal inference (using isFreeWhenInferring) in which we quantify over
808 -- all *non-inheritable* constraints too. This implements choice
809 -- (B) under "implicit parameter and monomorphism" above.
811 -- Remember that we may need to do *some* simplification, to
812 -- (for example) squash {Monad (ST s)} into {}. It's not enough
813 -- just to float all constraints
814 mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
816 try_me inst | isFreeWrtTyVars qtvs inst = Free
817 | otherwise = ReduceMe
819 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
820 ASSERT( no_improvement )
821 ASSERT( null irreds )
822 -- No need to loop because simpleReduceLoop will have
823 -- already done any improvement necessary
825 returnTc (varSetElems qtvs, mkLIE frees, binds)
829 %************************************************************************
831 \subsection{tcSimplifyToDicts}
833 %************************************************************************
835 On the LHS of transformation rules we only simplify methods and constants,
836 getting dictionaries. We want to keep all of them unsimplified, to serve
837 as the available stuff for the RHS of the rule.
839 The same thing is used for specialise pragmas. Consider
842 {-# SPECIALISE f :: Int -> Int #-}
845 The type checker generates a binding like:
847 f_spec = (f :: Int -> Int)
849 and we want to end up with
851 f_spec = _inline_me_ (f Int dNumInt)
853 But that means that we must simplify the Method for f to (f Int dNumInt)!
854 So tcSimplifyToDicts squeezes out all Methods.
856 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
858 fromIntegral :: (Integral a, Num b) => a -> b
859 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
861 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
865 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
867 because the scsel will mess up matching. Instead we want
869 forall dIntegralInt, dNumInt.
870 fromIntegral Int Int dIntegralInt dNumInt = id Int
872 Hence "DontReduce NoSCs"
875 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
876 tcSimplifyToDicts wanted_lie
877 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
878 -- Since try_me doesn't look at types, we don't need to
879 -- do any zonking, so it's safe to call reduceContext directly
881 returnTc (irreds, binds)
884 doc = text "tcSimplifyToDicts"
885 wanteds = lieToList wanted_lie
887 -- Reduce methods and lits only; stop as soon as we get a dictionary
888 try_me inst | isDict inst = DontReduce NoSCs
889 | otherwise = ReduceMe
893 %************************************************************************
895 \subsection{Filtering at a dynamic binding}
897 %************************************************************************
902 we must discharge all the ?x constraints from B. We also do an improvement
903 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
905 Actually, the constraints from B might improve the types in ?x. For example
907 f :: (?x::Int) => Char -> Char
910 then the constraint (?x::Int) arising from the call to f will
911 force the binding for ?x to be of type Int.
914 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
916 -> TcM (LIE, TcDictBinds)
917 tcSimplifyIPs given_ips wanted_lie
918 = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
919 returnTc (mkLIE frees, binds)
921 doc = text "tcSimplifyIPs" <+> ppr given_ips
922 wanteds = lieToList wanted_lie
923 ip_set = mkNameSet (ipNamesOfInsts given_ips)
925 -- Simplify any methods that mention the implicit parameter
926 try_me inst | isFreeWrtIPs ip_set inst = Free
927 | otherwise = ReduceMe
929 simpl_loop givens wanteds
930 = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
931 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
933 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
935 if no_improvement then
936 ASSERT( null irreds )
937 returnTc (frees, binds)
939 simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
940 returnTc (frees1, binds `AndMonoBinds` binds1)
944 %************************************************************************
946 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
948 %************************************************************************
950 When doing a binding group, we may have @Insts@ of local functions.
951 For example, we might have...
953 let f x = x + 1 -- orig local function (overloaded)
954 f.1 = f Int -- two instances of f
959 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
960 where @f@ is in scope; those @Insts@ must certainly not be passed
961 upwards towards the top-level. If the @Insts@ were binding-ified up
962 there, they would have unresolvable references to @f@.
964 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
965 For each method @Inst@ in the @init_lie@ that mentions one of the
966 @Ids@, we create a binding. We return the remaining @Insts@ (in an
967 @LIE@), as well as the @HsBinds@ generated.
970 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
972 bindInstsOfLocalFuns init_lie local_ids
973 | null overloaded_ids
975 = returnTc (init_lie, EmptyMonoBinds)
978 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
979 ASSERT( null irreds )
980 returnTc (mkLIE frees, binds)
982 doc = text "bindInsts" <+> ppr local_ids
983 wanteds = lieToList init_lie
984 overloaded_ids = filter is_overloaded local_ids
985 is_overloaded id = isOverloadedTy (idType id)
987 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
988 -- so it's worth building a set, so that
989 -- lookup (in isMethodFor) is faster
991 try_me inst | isMethodFor overloaded_set inst = ReduceMe
996 %************************************************************************
998 \subsection{Data types for the reduction mechanism}
1000 %************************************************************************
1002 The main control over context reduction is here
1006 = ReduceMe -- Try to reduce this
1007 -- If there's no instance, behave exactly like
1008 -- DontReduce: add the inst to
1009 -- the irreductible ones, but don't
1010 -- produce an error message of any kind.
1011 -- It might be quite legitimate such as (Eq a)!
1013 | DontReduce WantSCs -- Return as irreducible
1015 | DontReduceUnlessConstant -- Return as irreducible unless it can
1016 -- be reduced to a constant in one step
1018 | Free -- Return as free
1020 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1021 -- of a predicate when adding it to the avails
1027 type RedState = (Avails, -- What's available
1028 [Inst]) -- Insts for which try_me returned Free
1030 type Avails = FiniteMap Inst Avail
1033 = Irred -- Used for irreducible dictionaries,
1034 -- which are going to be lambda bound
1036 | BoundTo TcId -- Used for dictionaries for which we have a binding
1037 -- e.g. those "given" in a signature
1039 | NoRhs -- Used for Insts like (CCallable f)
1040 -- where no witness is required.
1042 | Rhs -- Used when there is a RHS
1044 [Inst] -- Insts free in the RHS; we need these too
1046 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
1047 | (inst,avail) <- fmToList avails ]
1049 instance Outputable Avail where
1052 pprAvail NoRhs = text "<no rhs>"
1053 pprAvail Irred = text "Irred"
1054 pprAvail (BoundTo x) = text "Bound to" <+> ppr x
1055 pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
1058 Extracting the bindings from a bunch of Avails.
1059 The bindings do *not* come back sorted in dependency order.
1060 We assume that they'll be wrapped in a big Rec, so that the
1061 dependency analyser can sort them out later
1065 bindsAndIrreds :: Avails
1067 -> (TcDictBinds, -- Bindings
1068 [Inst]) -- Irreducible ones
1070 bindsAndIrreds avails wanteds
1071 = go avails EmptyMonoBinds [] wanteds
1073 go avails binds irreds [] = (binds, irreds)
1075 go avails binds irreds (w:ws)
1076 = case lookupFM avails w of
1077 Nothing -> -- Free guys come out here
1078 -- (If we didn't do addFree we could use this as the
1079 -- criterion for free-ness, and pick up the free ones here too)
1080 go avails binds irreds ws
1082 Just NoRhs -> go avails binds irreds ws
1084 Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
1086 Just (BoundTo id) -> go avails new_binds irreds ws
1088 -- For implicit parameters, all occurrences share the same
1089 -- Id, so there is no need for synonym bindings
1090 new_binds | new_id == id = binds
1091 | otherwise = addBind binds new_id (HsVar id)
1094 Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
1097 avails' = addToFM avails w (BoundTo id)
1099 addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
1103 %************************************************************************
1105 \subsection[reduce]{@reduce@}
1107 %************************************************************************
1109 When the "what to do" predicate doesn't depend on the quantified type variables,
1110 matters are easier. We don't need to do any zonking, unless the improvement step
1111 does something, in which case we zonk before iterating.
1113 The "given" set is always empty.
1116 simpleReduceLoop :: SDoc
1117 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1119 -> TcM ([Inst], -- Free
1121 [Inst]) -- Irreducible
1123 simpleReduceLoop doc try_me wanteds
1124 = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
1125 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
1126 if no_improvement then
1127 returnTc (frees, binds, irreds)
1129 simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
1130 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1136 reduceContext :: SDoc
1137 -> (Inst -> WhatToDo)
1140 -> NF_TcM (Bool, -- True <=> improve step did no unification
1142 TcDictBinds, -- Dictionary bindings
1143 [Inst]) -- Irreducible
1145 reduceContext doc try_me givens wanteds
1147 traceTc (text "reduceContext" <+> (vcat [
1148 text "----------------------",
1150 text "given" <+> ppr givens,
1151 text "wanted" <+> ppr wanteds,
1152 text "----------------------"
1155 -- Build the Avail mapping from "givens"
1156 foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
1159 reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
1161 -- Do improvement, using everything in avails
1162 -- In particular, avails includes all superclasses of everything
1163 tcImprove avails `thenTc` \ no_improvement ->
1165 traceTc (text "reduceContext end" <+> (vcat [
1166 text "----------------------",
1168 text "given" <+> ppr givens,
1169 text "wanted" <+> ppr wanteds,
1171 text "avails" <+> pprAvails avails,
1172 text "frees" <+> ppr frees,
1173 text "no_improvement =" <+> ppr no_improvement,
1174 text "----------------------"
1177 (binds, irreds) = bindsAndIrreds avails wanteds
1179 returnTc (no_improvement, frees, binds, irreds)
1182 = tcGetInstEnv `thenTc` \ inst_env ->
1184 preds = [ (pred, pp_loc)
1185 | inst <- keysFM avails,
1186 let pp_loc = pprInstLoc (instLoc inst),
1187 pred <- predsOfInst inst,
1190 -- Avails has all the superclasses etc (good)
1191 -- It also has all the intermediates of the deduction (good)
1192 -- It does not have duplicates (good)
1193 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1194 -- so that improve will see them separate
1195 eqns = improve (classInstEnv inst_env) preds
1200 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenNF_Tc_`
1201 mapTc_ unify eqns `thenTc_`
1204 unify ((qtvs, t1, t2), doc)
1205 = tcAddErrCtxt doc $
1206 tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
1207 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1210 The main context-reduction function is @reduce@. Here's its game plan.
1213 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1214 -- along with its depth
1215 -> (Inst -> WhatToDo)
1222 try_me: given an inst, this function returns
1224 DontReduce return this in "irreds"
1225 Free return this in "frees"
1227 wanteds: The list of insts to reduce
1228 state: An accumulating parameter of type RedState
1229 that contains the state of the algorithm
1231 It returns a RedState.
1233 The (n,stack) pair is just used for error reporting.
1234 n is always the depth of the stack.
1235 The stack is the stack of Insts being reduced: to produce X
1236 I had to produce Y, to produce Y I had to produce Z, and so on.
1239 reduceList (n,stack) try_me wanteds state
1240 | n > opt_MaxContextReductionDepth
1241 = failWithTc (reduceDepthErr n stack)
1247 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1252 go [] state = returnTc state
1253 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
1256 -- Base case: we're done!
1257 reduce stack try_me wanted state
1258 -- It's the same as an existing inst, or a superclass thereof
1259 | isAvailable state wanted
1263 = case try_me wanted of {
1265 DontReduce want_scs -> addIrred want_scs state wanted
1267 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1268 -- First, see if the inst can be reduced to a constant in one step
1269 try_simple (addIrred AddSCs) -- Assume want superclasses
1271 ; Free -> -- It's free so just chuck it upstairs
1272 -- First, see if the inst can be reduced to a constant in one step
1275 ; ReduceMe -> -- It should be reduced
1276 lookupInst wanted `thenNF_Tc` \ lookup_result ->
1277 case lookup_result of
1278 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
1279 addWanted state' wanted rhs wanteds'
1280 SimpleInst rhs -> addWanted state wanted rhs []
1282 NoInstance -> -- No such instance!
1283 -- Add it and its superclasses
1284 addIrred AddSCs state wanted
1288 try_simple do_this_otherwise
1289 = lookupInst wanted `thenNF_Tc` \ lookup_result ->
1290 case lookup_result of
1291 SimpleInst rhs -> addWanted state wanted rhs []
1292 other -> do_this_otherwise state wanted
1297 isAvailable :: RedState -> Inst -> Bool
1298 isAvailable (avails, _) wanted = wanted `elemFM` avails
1299 -- NB: the Ord instance of Inst compares by the class/type info
1300 -- *not* by unique. So
1301 -- d1::C Int == d2::C Int
1303 -------------------------
1304 addFree :: RedState -> Inst -> NF_TcM RedState
1305 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1306 -- to avails, so that any other equal Insts will be commoned up right
1307 -- here rather than also being tossed upstairs. This is really just
1308 -- an optimisation, and perhaps it is more trouble that it is worth,
1309 -- as the following comments show!
1311 -- NB1: do *not* add superclasses. If we have
1314 -- but a is not bound here, then we *don't* want to derive
1315 -- dn from df here lest we lose sharing.
1317 -- NB2: do *not* add the Inst to avails at all if it's a method.
1318 -- The following situation shows why this is bad:
1319 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1320 -- From an application (truncate f i) we get
1321 -- t1 = truncate at f
1323 -- If we have also have a second occurrence of truncate, we get
1324 -- t3 = truncate at f
1326 -- When simplifying with i,f free, we might still notice that
1327 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1328 -- will continue to float out!
1329 -- Solution: never put methods in avail till they are captured
1330 -- in which case addFree isn't used
1332 -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1333 -- than BoundTo, else we end up with bogus bindings.
1334 -- c.f. instBindingRequired in addWanted
1335 addFree (avails, frees) free
1336 | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1337 | otherwise = returnNF_Tc (avails, free:frees)
1339 avail | instBindingRequired free = BoundTo (instToId free)
1342 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1343 addWanted state@(avails, frees) wanted rhs_expr wanteds
1344 -- Do *not* add superclasses as well. Here's an example of why not
1345 -- class Eq a => Foo a b
1346 -- instance Eq a => Foo [a] a
1347 -- If we are reducing
1349 -- we'll first deduce that it holds (via the instance decl). We
1350 -- must not then overwrite the Eq t constraint with a superclass selection!
1351 -- ToDo: this isn't entirely unsatisfactory, because
1352 -- we may also lose some entirely-legitimate sharing this way
1354 = ASSERT( not (isAvailable state wanted) )
1355 returnNF_Tc (addToFM avails wanted avail, frees)
1357 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1358 | otherwise = ASSERT( null wanteds ) NoRhs
1360 addGiven :: RedState -> Inst -> NF_TcM RedState
1361 addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
1363 addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
1364 addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
1365 addIrred AddSCs state irred = addAvailAndSCs state irred Irred
1367 addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
1368 addAvailAndSCs (avails, frees) wanted avail
1369 = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
1370 returnNF_Tc (avails', frees)
1372 ---------------------
1373 add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
1374 add_avail_and_scs avails wanted avail
1375 = add_scs (addToFM avails wanted avail) wanted
1377 add_scs :: Avails -> Inst -> NF_TcM Avails
1378 -- Add all the superclasses of the Inst to Avails
1379 -- Invariant: the Inst is already in Avails.
1382 | not (isClassDict dict)
1383 = returnNF_Tc avails
1385 | otherwise -- It is a dictionary
1386 = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
1387 foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1389 (clas, tys) = getDictClassTys dict
1390 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1391 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1393 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1394 = case lookupFM avails sc_dict of
1395 Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
1396 other -> add_avail_and_scs avails sc_dict avail
1398 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1399 avail = Rhs sc_sel_rhs [dict]
1402 Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
1403 and want to deduce (d2:C [a]) where
1405 class Ord a => C a where
1406 instance Ord a => C [a] where ...
1408 Then we'll use the instance decl to deduce C [a] and then add the
1409 superclasses of C [a] to avails. But we must not overwrite the binding
1410 for d1:Ord a (which is given) with a superclass selection or we'll just
1411 build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
1415 %************************************************************************
1417 \section{tcSimplifyTop: defaulting}
1419 %************************************************************************
1422 If a dictionary constrains a type variable which is
1423 * not mentioned in the environment
1424 * and not mentioned in the type of the expression
1425 then it is ambiguous. No further information will arise to instantiate
1426 the type variable; nor will it be generalised and turned into an extra
1427 parameter to a function.
1429 It is an error for this to occur, except that Haskell provided for
1430 certain rules to be applied in the special case of numeric types.
1432 * at least one of its classes is a numeric class, and
1433 * all of its classes are numeric or standard
1434 then the type variable can be defaulted to the first type in the
1435 default-type list which is an instance of all the offending classes.
1437 So here is the function which does the work. It takes the ambiguous
1438 dictionaries and either resolves them (producing bindings) or
1439 complains. It works by splitting the dictionary list by type
1440 variable, and using @disambigOne@ to do the real business.
1442 @tcSimplifyTop@ is called once per module to simplify all the constant
1443 and ambiguous Insts.
1445 We need to be careful of one case. Suppose we have
1447 instance Num a => Num (Foo a b) where ...
1449 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1450 to (Num x), and default x to Int. But what about y??
1452 It's OK: the final zonking stage should zap y to (), which is fine.
1456 tcSimplifyTop :: LIE -> TcM TcDictBinds
1457 tcSimplifyTop wanted_lie
1458 = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1459 ASSERT( null frees )
1462 -- All the non-std ones are definite errors
1463 (stds, non_stds) = partition isStdClassTyVarDict irreds
1465 -- Group by type variable
1466 std_groups = equivClasses cmp_by_tyvar stds
1468 -- Pick the ones which its worth trying to disambiguate
1469 (std_oks, std_bads) = partition worth_a_try std_groups
1471 -- Have a try at disambiguation
1472 -- if the type variable isn't bound
1473 -- up with one of the non-standard classes
1474 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1475 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1477 -- Collect together all the bad guys
1478 bad_guys = non_stds ++ concat std_bads
1480 -- Disambiguate the ones that look feasible
1481 mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
1483 -- And complain about the ones that don't
1484 -- This group includes both non-existent instances
1485 -- e.g. Num (IO a) and Eq (Int -> Int)
1486 -- and ambiguous dictionaries
1488 addTopAmbigErrs bad_guys `thenNF_Tc_`
1490 returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1492 wanteds = lieToList wanted_lie
1493 try_me inst = ReduceMe
1495 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1497 get_tv d = case getDictClassTys d of
1498 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1499 get_clas d = case getDictClassTys d of
1500 (clas, [ty]) -> clas
1503 @disambigOne@ assumes that its arguments dictionaries constrain all
1504 the same type variable.
1506 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1507 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1508 the most common use of defaulting is code like:
1510 _ccall_ foo `seqPrimIO` bar
1512 Since we're not using the result of @foo@, the result if (presumably)
1516 disambigGroup :: [Inst] -- All standard classes of form (C a)
1520 | any isNumericClass classes -- Guaranteed all standard classes
1521 -- see comment at the end of function for reasons as to
1522 -- why the defaulting mechanism doesn't apply to groups that
1523 -- include CCallable or CReturnable dicts.
1524 && not (any isCcallishClass classes)
1525 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1526 -- SO, TRY DEFAULT TYPES IN ORDER
1528 -- Failure here is caused by there being no type in the
1529 -- default list which can satisfy all the ambiguous classes.
1530 -- For example, if Real a is reqd, but the only type in the
1531 -- default list is Int.
1532 tcGetDefaultTys `thenNF_Tc` \ default_tys ->
1534 try_default [] -- No defaults work, so fail
1537 try_default (default_ty : default_tys)
1538 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1539 -- default_tys instead
1540 tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
1543 theta = [mkClassPred clas [default_ty] | clas <- classes]
1545 -- See if any default works, and if so bind the type variable to it
1546 -- If not, add an AmbigErr
1547 recoverTc (addAmbigErrs dicts `thenNF_Tc_`
1548 returnTc EmptyMonoBinds) $
1550 try_default default_tys `thenTc` \ chosen_default_ty ->
1552 -- Bind the type variable and reduce the context, for real this time
1553 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
1554 simpleReduceLoop (text "disambig" <+> ppr dicts)
1555 try_me dicts `thenTc` \ (frees, binds, ambigs) ->
1556 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1557 warnDefault dicts chosen_default_ty `thenTc_`
1560 | all isCreturnableClass classes
1561 = -- Default CCall stuff to (); we don't even both to check that () is an
1562 -- instance of CReturnable, because we know it is.
1563 unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
1564 returnTc EmptyMonoBinds
1566 | otherwise -- No defaults
1567 = addAmbigErrs dicts `thenNF_Tc_`
1568 returnTc EmptyMonoBinds
1571 try_me inst = ReduceMe -- This reduce should not fail
1572 tyvar = get_tv (head dicts) -- Should be non-empty
1573 classes = map get_clas dicts
1576 [Aside - why the defaulting mechanism is turned off when
1577 dealing with arguments and results to ccalls.
1579 When typechecking _ccall_s, TcExpr ensures that the external
1580 function is only passed arguments (and in the other direction,
1581 results) of a restricted set of 'native' types. This is
1582 implemented via the help of the pseudo-type classes,
1583 @CReturnable@ (CR) and @CCallable@ (CC.)
1585 The interaction between the defaulting mechanism for numeric
1586 values and CC & CR can be a bit puzzling to the user at times.
1595 What type has 'x' got here? That depends on the default list
1596 in operation, if it is equal to Haskell 98's default-default
1597 of (Integer, Double), 'x' has type Double, since Integer
1598 is not an instance of CR. If the default list is equal to
1599 Haskell 1.4's default-default of (Int, Double), 'x' has type
1602 To try to minimise the potential for surprises here, the
1603 defaulting mechanism is turned off in the presence of
1604 CCallable and CReturnable.
1609 %************************************************************************
1611 \subsection[simple]{@Simple@ versions}
1613 %************************************************************************
1615 Much simpler versions when there are no bindings to make!
1617 @tcSimplifyThetas@ simplifies class-type constraints formed by
1618 @deriving@ declarations and when specialising instances. We are
1619 only interested in the simplified bunch of class/type constraints.
1621 It simplifies to constraints of the form (C a b c) where
1622 a,b,c are type variables. This is required for the context of
1623 instance declarations.
1626 tcSimplifyThetas :: ThetaType -- Wanted
1627 -> TcM ThetaType -- Needed
1629 tcSimplifyThetas wanteds
1630 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
1631 reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
1633 -- For multi-param Haskell, check that the returned dictionaries
1634 -- don't have any of the form (C Int Bool) for which
1635 -- we expect an instance here
1636 -- For Haskell 98, check that all the constraints are of the form C a,
1637 -- where a is a type variable
1638 bad_guys | glaExts = [pred | pred <- irreds,
1639 isEmptyVarSet (tyVarsOfPred pred)]
1640 | otherwise = [pred | pred <- irreds,
1641 not (isTyVarClassPred pred)]
1643 if null bad_guys then
1646 mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
1650 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1651 used with \tr{default} declarations. We are only interested in
1652 whether it worked or not.
1655 tcSimplifyCheckThetas :: ThetaType -- Given
1656 -> ThetaType -- Wanted
1659 tcSimplifyCheckThetas givens wanteds
1660 = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
1664 mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
1670 type AvailsSimple = FiniteMap PredType Bool
1671 -- True => irreducible
1672 -- False => given, or can be derived from a given or from an irreducible
1674 reduceSimple :: ThetaType -- Given
1675 -> ThetaType -- Wanted
1676 -> NF_TcM ThetaType -- Irreducible
1678 reduceSimple givens wanteds
1679 = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
1680 returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
1682 givens_fm = foldl addNonIrred emptyFM givens
1684 reduce_simple :: (Int,ThetaType) -- Stack
1687 -> NF_TcM AvailsSimple
1689 reduce_simple (n,stack) avails wanteds
1692 go avails [] = returnNF_Tc avails
1693 go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
1696 reduce_simple_help stack givens wanted
1697 | wanted `elemFM` givens
1698 = returnNF_Tc givens
1700 | Just (clas, tys) <- getClassPredTys_maybe wanted
1701 = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
1703 Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
1704 Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1707 = returnNF_Tc (addSimpleIrred givens wanted)
1709 addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
1710 addSimpleIrred givens pred
1711 = addSCs (addToFM givens pred True) pred
1713 addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
1714 addNonIrred givens pred
1715 = addSCs (addToFM givens pred False) pred
1718 | not (isClassPred pred) = givens
1719 | otherwise = foldl add givens sc_theta
1721 Just (clas,tys) = getClassPredTys_maybe pred
1722 (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1723 sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1726 = case lookupFM givens ct of
1727 Nothing -> -- Add it and its superclasses
1728 addSCs (addToFM givens ct False) ct
1730 Just True -> -- Set its flag to False; superclasses already done
1731 addToFM givens ct False
1733 Just False -> -- Already done
1739 %************************************************************************
1741 \section{Errors and contexts}
1743 %************************************************************************
1745 ToDo: for these error messages, should we note the location as coming
1746 from the insts, or just whatever seems to be around in the monad just
1750 groupInsts :: [Inst] -> [[Inst]]
1751 -- Group together insts with the same origin
1752 -- We want to report them together in error messages
1754 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1756 -- (It may seem a bit crude to compare the error messages,
1757 -- but it makes sure that we combine just what the user sees,
1758 -- and it avoids need equality on InstLocs.)
1759 (friends, others) = partition is_friend insts
1760 loc_msg = showSDoc (pprInstLoc (instLoc inst))
1761 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1764 addTopAmbigErrs dicts
1765 = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts) `thenNF_Tc_`
1766 mapNF_Tc (addTopIPErrs tidy_env) (groupInsts bad_ips) `thenNF_Tc_`
1767 mapNF_Tc (addAmbigErr tidy_env) ambigs `thenNF_Tc_`
1770 fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1771 (tidy_env, tidy_dicts) = tidyInsts dicts
1772 (bad_ips, non_ips) = partition is_ip tidy_dicts
1773 (no_insts, ambigs) = partition no_inst non_ips
1774 is_ip d = any isIPPred (predsOfInst d)
1775 no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1778 plural xs = char 's'
1780 addTopIPErrs tidy_env tidy_dicts
1781 = addInstErrTcM (instLoc (head tidy_dicts))
1783 ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1785 -- Used for top-level irreducibles
1786 addTopInstanceErrs tidy_env tidy_dicts
1787 = addInstErrTcM (instLoc (head tidy_dicts))
1789 ptext SLIT("No instance") <> plural tidy_dicts <+>
1790 ptext SLIT("for") <+> pprInsts tidy_dicts)
1793 = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1795 (tidy_env, tidy_dicts) = tidyInsts dicts
1797 addAmbigErr tidy_env tidy_dict
1798 = addInstErrTcM (instLoc tidy_dict)
1800 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1801 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1803 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1805 warnDefault dicts default_ty
1806 = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
1807 tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1810 (_, tidy_dicts) = tidyInsts dicts
1811 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1812 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1813 quotes (ppr default_ty),
1814 pprInstsInFull tidy_dicts]
1816 complainCheck doc givens irreds
1817 = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
1818 mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds) `thenNF_Tc_`
1821 given_dicts = filter isDict givens
1822 -- Filter out methods, which are only added to
1823 -- the given set as an optimisation
1825 addNoInstanceErrs what_doc givens dicts
1826 = tcGetInstEnv `thenNF_Tc` \ inst_env ->
1828 (tidy_env1, tidy_givens) = tidyInsts givens
1829 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
1831 doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1832 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1834 ptext SLIT("Probable fix:"),
1838 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1839 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1842 -- The error message when we don't find a suitable instance
1843 -- is complicated by the fact that sometimes this is because
1844 -- there is no instance, and sometimes it's because there are
1845 -- too many instances (overlap). See the comments in TcEnv.lhs
1846 -- with the InstEnv stuff.
1849 | not ambig_overlap = empty
1851 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1852 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1853 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1855 fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1856 ptext SLIT("to the") <+> what_doc]
1858 fix2 | null instance_dicts
1861 = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1863 instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1864 -- Insts for which it is worth suggesting an adding an instance declaration
1865 -- Exclude implicit parameters, and tyvar dicts
1867 -- Checks for the ambiguous case when we have overlapping instances
1868 ambig_overlap = any ambig_overlap1 dicts
1871 = case lookupInstEnv inst_env clas tys of
1872 NoMatch ambig -> ambig
1876 (clas,tys) = getDictClassTys dict
1878 addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
1880 -- Used for the ...Thetas variants; all top level
1882 = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
1884 reduceDepthErr n stack
1885 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1886 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1887 nest 4 (pprInstsInFull stack)]
1889 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1891 -----------------------------------------------
1893 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1894 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])