2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck,
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,
28 isDict, isClassDict, instName,
29 isStdClassTyVarDict, isMethodFor,
30 instToId, tyVarsOfInsts,
31 instBindingRequired, instCanBeGeneralised,
32 newDictsFromOld, instMentionsIPs,
33 getDictClassTys, isTyVarDict,
34 instLoc, pprInst, zonkInst, tidyInsts,
35 Inst, LIE, pprInsts, pprInstsInFull,
38 import TcEnv ( tcGetGlobalTyVars, tcGetInstEnv )
39 import InstEnv ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
41 import TcType ( zonkTcTyVarsAndFV, tcInstTyVars )
42 import TcUnify ( unifyTauTy )
44 import NameSet ( mkNameSet )
45 import Class ( classBigSig )
46 import FunDeps ( oclose, grow, improve )
47 import PrelInfo ( isNumericClass, isCreturnableClass, isCcallishClass )
49 import Type ( ThetaType, PredType, mkClassPred,
50 mkTyVarTy, getTyVar, isTyVarClassPred,
51 splitSigmaTy, tyVarsOfPred,
52 getClassPredTys_maybe, isClassPred, isIPPred,
53 inheritablePred, predHasFDs
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: you *must* quantify over implicit parameters.
331 Question 2: type signatures
332 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
333 OK, so it it legal to give an explicit, user type signature to f, thus:
338 At first sight this seems reasonable, but it has the nasty property
339 that adding a type signature changes the dynamic semantics.=20
342 (let f x = (x::Int) + ?y
343 in (f 3, f 3 with ?y=5)) with ?y = 6
347 (let f :: Int -> Int=20
349 in (f 3, f 3 with ?y=5)) with ?y = 6
353 Indeed, simply inlining f (at the Haskell source level) would change the
356 Conclusion: the above type signature is illegal. You'll get a message
357 of the form "could not deduce (?y::Int) from ()".
360 Question 3: monomorphism
361 ~~~~~~~~~~~~~~~~~~~~~~~~
362 There's a nasty corner case when the monomorphism restriction bites:
366 The argument above suggests that we *must* generalise=20
367 over the ?y parameter, to get=20
368 z :: (?y::Int) => Int,
369 but the monomorphism restriction says that we *must not*, giving
371 Why does the momomorphism restriction say this? Because if you have
373 let z = x + ?y in z+z
375 you might not expect the addition to be done twice --- but it will if
376 we follow the argument of Question 2 and generalise over ?y.
382 (A) Always generalise over implicit parameters
383 Bindings that fall under the monomorphism restriction can't
387 * Inlning remains valid
388 * No unexpected loss of sharing
389 * But simple bindings like
391 will be rejected, unless you add an explicit type signature
392 (to avoid the monomorphism restriction)
393 z :: (?y::Int) => Int
395 This seems unacceptable
397 (B) Monomorphism restriction "wins"
398 Bindings that fall under the monomorphism restriction can't
400 Always generalise over implicit parameters *except* for bindings
401 that fall under the monomorphism restriction
404 * Inlining isn't valid in general
405 * No unexpected loss of sharing
406 * Simple bindings like
408 accepted (get value of ?y from binding site)
410 (C) Always generalise over implicit parameters
411 Bindings that fall under the monomorphism restriction can't
412 be generalised, EXCEPT for implicit parameters
414 * Inlining remains valid
415 * Unexpected loss of sharing (from the extra generalisation)
416 * Simple bindings like
418 accepted (get value of ?y from occurrence sites)
423 None of these choices seems very satisfactory. But at least we should
424 decide which we want to do.
426 It's really not clear what is the Right Thing To Do. If you see
430 would you expect the value of ?y to be got from the *occurrence sites*
431 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
432 case of function definitions, the answer is clearly the former, but
433 less so in the case of non-fucntion definitions. On the other hand,
434 if we say that we get the value of ?y from the definition site of 'z',
435 then inlining 'z' might change the semantics of the program.
437 Choice (C) really says "the monomorphism restriction doesn't apply
438 to implicit parameters". Which is fine, but remember that every=20
439 innocent binding 'x = ...' that mentions an implicit parameter in
440 the RHS becomes a *function* of that parameter, called at each
441 use of 'x'. Now, the chances are that there are no intervening 'with'
442 clauses that bind ?y, so a decent compiler should common up all=20
443 those function calls. So I think I strongly favour (C). Indeed,
444 one could make a similar argument for abolishing the monomorphism
445 restriction altogether.
447 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
451 %************************************************************************
453 \subsection{tcSimplifyInfer}
455 %************************************************************************
457 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
459 1. Compute Q = grow( fvs(T), C )
461 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
462 predicates will end up in Ct; we deal with them at the top level
464 3. Try improvement, using functional dependencies
466 4. If Step 3 did any unification, repeat from step 1
467 (Unification can change the result of 'grow'.)
469 Note: we don't reduce dictionaries in step 2. For example, if we have
470 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
471 after step 2. However note that we may therefore quantify over more
472 type variables than we absolutely have to.
474 For the guts, we need a loop, that alternates context reduction and
475 improvement with unification. E.g. Suppose we have
477 class C x y | x->y where ...
479 and tcSimplify is called with:
481 Then improvement unifies a with b, giving
484 If we need to unify anything, we rattle round the whole thing all over
491 -> [TcTyVar] -- fv(T); type vars
493 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
495 TcDictBinds, -- Bindings
496 [TcId]) -- Dict Ids that must be bound here (zonked)
501 tcSimplifyInfer doc tau_tvs wanted_lie
502 = inferLoop doc tau_tvs (lieToList wanted_lie) `thenTc` \ (qtvs, frees, binds, irreds) ->
504 -- Check for non-generalisable insts
505 mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds) `thenTc_`
507 returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
509 inferLoop doc tau_tvs wanteds
511 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
512 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
513 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
515 preds = predsOfInsts wanteds'
516 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
519 | isFreeAndInheritable qtvs inst = Free
520 | isClassDict inst = DontReduceUnlessConstant -- Dicts
521 | otherwise = ReduceMe -- Lits and Methods
524 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
527 if no_improvement then
528 returnTc (varSetElems qtvs, frees, binds, irreds)
530 -- If improvement did some unification, we go round again. There
531 -- are two subtleties:
532 -- a) We start again with irreds, not wanteds
533 -- Using an instance decl might have introduced a fresh type variable
534 -- which might have been unified, so we'd get an infinite loop
535 -- if we started again with wanteds! See example [LOOP]
537 -- b) It's also essential to re-process frees, because unification
538 -- might mean that a type variable that looked free isn't now.
540 -- Hence the (irreds ++ frees)
542 inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
543 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
548 class If b t e r | b t e -> r
551 class Lte a b c | a b -> c where lte :: a -> b -> c
553 instance (Lte a b l,If l b a c) => Max a b c
555 Wanted: Max Z (S x) y
557 Then we'll reduce using the Max instance to:
558 (Lte Z (S x) l, If l (S x) Z y)
559 and improve by binding l->T, after which we can do some reduction
560 on both the Lte and If constraints. What we *can't* do is start again
561 with (Max Z (S x) y)!
564 isFreeAndInheritable qtvs inst
565 = isFree qtvs inst -- Constrains no quantified vars
566 && all inheritablePred (predsOfInst inst) -- And no implicit parameter involved
567 -- (see "Notes on implicit parameters")
569 isFree qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
573 %************************************************************************
575 \subsection{tcSimplifyCheck}
577 %************************************************************************
579 @tcSimplifyCheck@ is used when we know exactly the set of variables
580 we are going to quantify over. For example, a class or instance declaration.
585 -> [TcTyVar] -- Quantify over these
589 TcDictBinds) -- Bindings
591 tcSimplifyCheck doc qtvs givens wanted_lie
592 = checkLoop doc qtvs givens (lieToList wanted_lie) `thenTc` \ (frees, binds, irreds) ->
594 -- Complain about any irreducible ones
595 complainCheck doc givens irreds `thenNF_Tc_`
598 returnTc (mkLIE frees, binds)
600 checkLoop doc qtvs givens wanteds
602 zonkTcTyVarsAndFV qtvs `thenNF_Tc` \ qtvs' ->
603 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
604 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
608 -- When checking against a given signature we always reduce
609 -- until we find a match against something given, or can't reduce
610 try_me inst | isFreeAndInheritable qtvs' inst = Free
611 | otherwise = ReduceMe
613 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
616 if no_improvement then
617 returnTc (frees, binds, irreds)
619 checkLoop doc qtvs givens' (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
620 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
622 complainCheck doc givens irreds
623 = mapNF_Tc zonkInst given_dicts `thenNF_Tc` \ givens' ->
624 mapNF_Tc (addNoInstanceErr doc given_dicts) irreds `thenNF_Tc_`
627 given_dicts = filter isDict givens
628 -- Filter out methods, which are only added to
629 -- the given set as an optimisation
633 %************************************************************************
635 \subsection{tcSimplifyRestricted}
637 %************************************************************************
640 tcSimplifyRestricted -- Used for restricted binding groups
642 -> [TcTyVar] -- Free in the type of the RHSs
643 -> LIE -- Free in the RHSs
644 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
646 TcDictBinds) -- Bindings
648 tcSimplifyRestricted doc tau_tvs wanted_lie
649 = -- First squash out all methods, to find the constrained tyvars
650 -- We can't just take the free vars of wanted_lie because that'll
651 -- have methods that may incidentally mention entirely unconstrained variables
652 -- e.g. a call to f :: Eq a => a -> b -> b
653 -- Here, b is unconstrained. A good example would be
655 -- We want to infer the polymorphic type
656 -- foo :: forall b. b -> b
657 tcSimplifyToDicts wanted_lie `thenTc` \ (dicts, _) ->
659 constrained_tvs = tyVarsOfInsts dicts
662 -- Next, figure out the tyvars we will quantify over
663 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
664 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
666 qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts dicts) gbl_tvs)
667 `minusVarSet` constrained_tvs
670 -- The first step may have squashed more methods than
671 -- necessary, so try again, this time knowing the exact
672 -- set of type variables to quantify over.
674 -- We quantify only over constraints that are captured by qtvs;
675 -- these will just be a subset of non-dicts. This in contrast
676 -- to normal inference (using isFreeAndInheritable) in which we quantify over
677 -- all *non-inheritable* constraints too. This implements choice
678 -- (B) under "implicit parameter and monomorphism" above.
679 mapNF_Tc zonkInst (lieToList wanted_lie) `thenNF_Tc` \ wanteds' ->
681 try_me inst | isFree qtvs inst = Free
682 | otherwise = ReduceMe
684 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
685 ASSERT( no_improvement )
686 ASSERT( null irreds )
687 -- No need to loop because tcSimplifyToDicts will have
688 -- already done any improvement necessary
690 returnTc (varSetElems qtvs, mkLIE frees, binds)
694 %************************************************************************
696 \subsection{tcSimplifyAndCheck}
698 %************************************************************************
700 @tcSimplifyInferCheck@ is used when we know the constraints we are to simplify
701 against, but we don't know the type variables over which we are going to quantify.
702 This happens when we have a type signature for a mutually recursive
708 -> [TcTyVar] -- fv(T)
711 -> TcM ([TcTyVar], -- Variables over which to quantify
713 TcDictBinds) -- Bindings
715 tcSimplifyInferCheck doc tau_tvs givens wanted
716 = inferCheckLoop doc tau_tvs givens (lieToList wanted) `thenTc` \ (qtvs, frees, binds, irreds) ->
718 -- Complain about any irreducible ones
719 complainCheck doc givens irreds `thenNF_Tc_`
722 returnTc (qtvs, mkLIE frees, binds)
724 inferCheckLoop doc tau_tvs givens wanteds
726 zonkTcTyVarsAndFV tau_tvs `thenNF_Tc` \ tau_tvs' ->
727 mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
728 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
729 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
732 -- Figure out what we are going to generalise over
733 -- You might think it should just be the signature tyvars,
734 -- but in bizarre cases you can get extra ones
735 -- f :: forall a. Num a => a -> a
736 -- f x = fst (g (x, head [])) + 1
738 -- Here we infer g :: forall a b. a -> b -> (b,a)
739 -- We don't want g to be monomorphic in b just because
740 -- f isn't quantified over b.
741 qtvs = (tau_tvs' `unionVarSet` tyVarsOfInsts givens') `minusVarSet` gbl_tvs
742 -- We could close gbl_tvs, but its not necessary for
743 -- soundness, and it'll only affect which tyvars, not which
744 -- dictionaries, we quantify over
746 -- When checking against a given signature we always reduce
747 -- until we find a match against something given, or can't reduce
748 try_me inst | isFreeAndInheritable qtvs inst = Free
749 | otherwise = ReduceMe
752 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
755 if no_improvement then
756 returnTc (varSetElems qtvs, frees, binds, irreds)
758 inferCheckLoop doc tau_tvs givens' (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
759 returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
763 %************************************************************************
765 \subsection{tcSimplifyToDicts}
767 %************************************************************************
769 On the LHS of transformation rules we only simplify methods and constants,
770 getting dictionaries. We want to keep all of them unsimplified, to serve
771 as the available stuff for the RHS of the rule.
773 The same thing is used for specialise pragmas. Consider
776 {-# SPECIALISE f :: Int -> Int #-}
779 The type checker generates a binding like:
781 f_spec = (f :: Int -> Int)
783 and we want to end up with
785 f_spec = _inline_me_ (f Int dNumInt)
787 But that means that we must simplify the Method for f to (f Int dNumInt)!
788 So tcSimplifyToDicts squeezes out all Methods.
790 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
792 fromIntegral :: (Integral a, Num b) => a -> b
793 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
795 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
799 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
801 because the scsel will mess up matching. Instead we want
803 forall dIntegralInt, dNumInt.
804 fromIntegral Int Int dIntegralInt dNumInt = id Int
806 Hence "DontReduce NoSCs"
809 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
810 tcSimplifyToDicts wanted_lie
811 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
812 -- Since try_me doesn't look at types, we don't need to
813 -- do any zonking, so it's safe to call reduceContext directly
815 returnTc (irreds, binds)
818 doc = text "tcSimplifyToDicts"
819 wanteds = lieToList wanted_lie
821 -- Reduce methods and lits only; stop as soon as we get a dictionary
822 try_me inst | isDict inst = DontReduce NoSCs
823 | otherwise = ReduceMe
827 %************************************************************************
829 \subsection{Filtering at a dynamic binding}
831 %************************************************************************
836 we must discharge all the ?x constraints from B. We also do an improvement
837 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
839 Actually, the constraints from B might improve the types in ?x. For example
841 f :: (?x::Int) => Char -> Char
844 then the constraint (?x::Int) arising from the call to f will
845 force the binding for ?x to be of type Int.
848 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
850 -> TcM (LIE, TcDictBinds)
851 tcSimplifyIPs given_ips wanted_lie
852 = simpl_loop given_ips wanteds `thenTc` \ (frees, binds) ->
853 returnTc (mkLIE frees, binds)
855 doc = text "tcSimplifyIPs" <+> ppr ip_names
856 wanteds = lieToList wanted_lie
857 ip_names = map instName given_ips
858 ip_set = mkNameSet ip_names
860 -- Simplify any methods that mention the implicit parameter
861 try_me inst | inst `instMentionsIPs` ip_set = ReduceMe
864 simpl_loop givens wanteds
865 = mapNF_Tc zonkInst givens `thenNF_Tc` \ givens' ->
866 mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
868 reduceContext doc try_me givens' wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
870 if no_improvement then
871 ASSERT( null irreds )
872 returnTc (frees, binds)
874 simpl_loop givens' (irreds ++ frees) `thenTc` \ (frees1, binds1) ->
875 returnTc (frees1, binds `AndMonoBinds` binds1)
879 %************************************************************************
881 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
883 %************************************************************************
885 When doing a binding group, we may have @Insts@ of local functions.
886 For example, we might have...
888 let f x = x + 1 -- orig local function (overloaded)
889 f.1 = f Int -- two instances of f
894 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
895 where @f@ is in scope; those @Insts@ must certainly not be passed
896 upwards towards the top-level. If the @Insts@ were binding-ified up
897 there, they would have unresolvable references to @f@.
899 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
900 For each method @Inst@ in the @init_lie@ that mentions one of the
901 @Ids@, we create a binding. We return the remaining @Insts@ (in an
902 @LIE@), as well as the @HsBinds@ generated.
905 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
907 bindInstsOfLocalFuns init_lie local_ids
908 | null overloaded_ids
910 = returnTc (init_lie, EmptyMonoBinds)
913 = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
914 ASSERT( null irreds )
915 returnTc (mkLIE frees, binds)
917 doc = text "bindInsts" <+> ppr local_ids
918 wanteds = lieToList init_lie
919 overloaded_ids = filter is_overloaded local_ids
920 is_overloaded id = case splitSigmaTy (idType id) of
921 (_, theta, _) -> not (null theta)
923 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
924 -- so it's worth building a set, so that
925 -- lookup (in isMethodFor) is faster
927 try_me inst | isMethodFor overloaded_set inst = ReduceMe
932 %************************************************************************
934 \subsection{Data types for the reduction mechanism}
936 %************************************************************************
938 The main control over context reduction is here
942 = ReduceMe -- Try to reduce this
943 -- If there's no instance, behave exactly like
944 -- DontReduce: add the inst to
945 -- the irreductible ones, but don't
946 -- produce an error message of any kind.
947 -- It might be quite legitimate such as (Eq a)!
949 | DontReduce WantSCs -- Return as irreducible
951 | DontReduceUnlessConstant -- Return as irreducible unless it can
952 -- be reduced to a constant in one step
954 | Free -- Return as free
956 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
957 -- of a predicate when adding it to the avails
963 type RedState = (Avails, -- What's available
964 [Inst]) -- Insts for which try_me returned Free
966 type Avails = FiniteMap Inst Avail
969 = Irred -- Used for irreducible dictionaries,
970 -- which are going to be lambda bound
972 | BoundTo TcId -- Used for dictionaries for which we have a binding
973 -- e.g. those "given" in a signature
975 | NoRhs -- Used for Insts like (CCallable f)
976 -- where no witness is required.
978 | Rhs -- Used when there is a RHS
980 [Inst] -- Insts free in the RHS; we need these too
982 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
983 | (inst,avail) <- fmToList avails ]
985 instance Outputable Avail where
988 pprAvail NoRhs = text "<no rhs>"
989 pprAvail Irred = text "Irred"
990 pprAvail (BoundTo x) = text "Bound to" <+> ppr x
991 pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
994 Extracting the bindings from a bunch of Avails.
995 The bindings do *not* come back sorted in dependency order.
996 We assume that they'll be wrapped in a big Rec, so that the
997 dependency analyser can sort them out later
1001 bindsAndIrreds :: Avails
1003 -> (TcDictBinds, -- Bindings
1004 [Inst]) -- Irreducible ones
1006 bindsAndIrreds avails wanteds
1007 = go avails EmptyMonoBinds [] wanteds
1009 go avails binds irreds [] = (binds, irreds)
1011 go avails binds irreds (w:ws)
1012 = case lookupFM avails w of
1013 Nothing -> -- Free guys come out here
1014 -- (If we didn't do addFree we could use this as the
1015 -- criterion for free-ness, and pick up the free ones here too)
1016 go avails binds irreds ws
1018 Just NoRhs -> go avails binds irreds ws
1020 Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
1022 Just (BoundTo id) -> go avails new_binds irreds ws
1024 -- For implicit parameters, all occurrences share the same
1025 -- Id, so there is no need for synonym bindings
1026 new_binds | new_id == id = binds
1027 | otherwise = addBind binds new_id (HsVar id)
1030 Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
1033 avails' = addToFM avails w (BoundTo id)
1035 addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
1039 %************************************************************************
1041 \subsection[reduce]{@reduce@}
1043 %************************************************************************
1045 When the "what to do" predicate doesn't depend on the quantified type variables,
1046 matters are easier. We don't need to do any zonking, unless the improvement step
1047 does something, in which case we zonk before iterating.
1049 The "given" set is always empty.
1052 simpleReduceLoop :: SDoc
1053 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1055 -> TcM ([Inst], -- Free
1057 [Inst]) -- Irreducible
1059 simpleReduceLoop doc try_me wanteds
1060 = mapNF_Tc zonkInst wanteds `thenNF_Tc` \ wanteds' ->
1061 reduceContext doc try_me [] wanteds' `thenTc` \ (no_improvement, frees, binds, irreds) ->
1062 if no_improvement then
1063 returnTc (frees, binds, irreds)
1065 simpleReduceLoop doc try_me (irreds ++ frees) `thenTc` \ (frees1, binds1, irreds1) ->
1066 returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1072 reduceContext :: SDoc
1073 -> (Inst -> WhatToDo)
1076 -> NF_TcM (Bool, -- True <=> improve step did no unification
1078 TcDictBinds, -- Dictionary bindings
1079 [Inst]) -- Irreducible
1081 reduceContext doc try_me givens wanteds
1083 traceTc (text "reduceContext" <+> (vcat [
1084 text "----------------------",
1086 text "given" <+> ppr givens,
1087 text "wanted" <+> ppr wanteds,
1088 text "----------------------"
1091 -- Build the Avail mapping from "givens"
1092 foldlNF_Tc addGiven (emptyFM, []) givens `thenNF_Tc` \ init_state ->
1095 reduceList (0,[]) try_me wanteds init_state `thenNF_Tc` \ state@(avails, frees) ->
1097 -- Do improvement, using everything in avails
1098 -- In particular, avails includes all superclasses of everything
1099 tcImprove avails `thenTc` \ no_improvement ->
1101 traceTc (text "reduceContext end" <+> (vcat [
1102 text "----------------------",
1104 text "given" <+> ppr givens,
1105 text "wanted" <+> ppr wanteds,
1107 text "avails" <+> pprAvails avails,
1108 text "frees" <+> ppr frees,
1109 text "no_improvement =" <+> ppr no_improvement,
1110 text "----------------------"
1113 (binds, irreds) = bindsAndIrreds avails wanteds
1115 returnTc (no_improvement, frees, binds, irreds)
1118 = tcGetInstEnv `thenTc` \ inst_env ->
1120 preds = [ (pred, pp_loc)
1121 | inst <- keysFM avails,
1122 let pp_loc = pprInstLoc (instLoc inst),
1123 pred <- predsOfInst inst,
1126 -- Avails has all the superclasses etc (good)
1127 -- It also has all the intermediates of the deduction (good)
1128 -- It does not have duplicates (good)
1129 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1130 -- so that improve will see them separate
1131 eqns = improve (classInstEnv inst_env) preds
1136 traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns)) `thenNF_Tc_`
1137 mapTc_ unify eqns `thenTc_`
1140 unify ((qtvs, t1, t2), doc)
1141 = tcAddErrCtxt doc $
1142 tcInstTyVars (varSetElems qtvs) `thenNF_Tc` \ (_, _, tenv) ->
1143 unifyTauTy (substTy tenv t1) (substTy tenv t2)
1144 ppr_eqn ((qtvs, t1, t2), doc)
1145 = vcat [ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs))
1146 <+> ppr t1 <+> equals <+> ppr t2,
1150 The main context-reduction function is @reduce@. Here's its game plan.
1153 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1154 -- along with its depth
1155 -> (Inst -> WhatToDo)
1162 try_me: given an inst, this function returns
1164 DontReduce return this in "irreds"
1165 Free return this in "frees"
1167 wanteds: The list of insts to reduce
1168 state: An accumulating parameter of type RedState
1169 that contains the state of the algorithm
1171 It returns a RedState.
1173 The (n,stack) pair is just used for error reporting.
1174 n is always the depth of the stack.
1175 The stack is the stack of Insts being reduced: to produce X
1176 I had to produce Y, to produce Y I had to produce Z, and so on.
1179 reduceList (n,stack) try_me wanteds state
1180 | n > opt_MaxContextReductionDepth
1181 = failWithTc (reduceDepthErr n stack)
1187 pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1192 go [] state = returnTc state
1193 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenTc` \ state' ->
1196 -- Base case: we're done!
1197 reduce stack try_me wanted state
1198 -- It's the same as an existing inst, or a superclass thereof
1199 | isAvailable state wanted
1203 = case try_me wanted of {
1205 DontReduce want_scs -> addIrred want_scs state wanted
1207 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1208 -- First, see if the inst can be reduced to a constant in one step
1209 try_simple (addIrred AddSCs) -- Assume want superclasses
1211 ; Free -> -- It's free so just chuck it upstairs
1212 -- First, see if the inst can be reduced to a constant in one step
1215 ; ReduceMe -> -- It should be reduced
1216 lookupInst wanted `thenNF_Tc` \ lookup_result ->
1217 case lookup_result of
1218 GenInst wanteds' rhs -> reduceList stack try_me wanteds' state `thenTc` \ state' ->
1219 addWanted state' wanted rhs wanteds'
1220 SimpleInst rhs -> addWanted state wanted rhs []
1222 NoInstance -> -- No such instance!
1223 -- Add it and its superclasses
1224 addIrred AddSCs state wanted
1228 try_simple do_this_otherwise
1229 = lookupInst wanted `thenNF_Tc` \ lookup_result ->
1230 case lookup_result of
1231 SimpleInst rhs -> addWanted state wanted rhs []
1232 other -> do_this_otherwise state wanted
1237 isAvailable :: RedState -> Inst -> Bool
1238 isAvailable (avails, _) wanted = wanted `elemFM` avails
1239 -- NB: the Ord instance of Inst compares by the class/type info
1240 -- *not* by unique. So
1241 -- d1::C Int == d2::C Int
1243 -------------------------
1244 addFree :: RedState -> Inst -> NF_TcM RedState
1245 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1246 -- to avails, so that any other equal Insts will be commoned up right
1247 -- here rather than also being tossed upstairs. This is really just
1248 -- an optimisation, and perhaps it is more trouble that it is worth,
1249 -- as the following comments show!
1251 -- NB1: do *not* add superclasses. If we have
1254 -- but a is not bound here, then we *don't* want to derive
1255 -- dn from df here lest we lose sharing.
1257 -- NB2: do *not* add the Inst to avails at all if it's a method.
1258 -- The following situation shows why this is bad:
1259 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1260 -- From an application (truncate f i) we get
1261 -- t1 = truncate at f
1263 -- If we have also have a second occurrence of truncate, we get
1264 -- t3 = truncate at f
1266 -- When simplifying with i,f free, we might still notice that
1267 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1268 -- will continue to float out!
1269 -- Solution: never put methods in avail till they are captured
1270 -- in which case addFree isn't used
1272 -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1273 -- than BoundTo, else we end up with bogus bindings.
1274 -- c.f. instBindingRequired in addWanted
1275 addFree (avails, frees) free
1276 | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1277 | otherwise = returnNF_Tc (avails, free:frees)
1279 avail | instBindingRequired free = BoundTo (instToId free)
1282 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1283 addWanted state@(avails, frees) wanted rhs_expr wanteds
1284 -- Do *not* add superclasses as well. Here's an example of why not
1285 -- class Eq a => Foo a b
1286 -- instance Eq a => Foo [a] a
1287 -- If we are reducing
1289 -- we'll first deduce that it holds (via the instance decl). We
1290 -- must not then overwrite the Eq t constraint with a superclass selection!
1291 -- ToDo: this isn't entirely unsatisfactory, because
1292 -- we may also lose some entirely-legitimate sharing this way
1294 = ASSERT( not (isAvailable state wanted) )
1295 returnNF_Tc (addToFM avails wanted avail, frees)
1297 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1298 | otherwise = ASSERT( null wanteds ) NoRhs
1300 addGiven :: RedState -> Inst -> NF_TcM RedState
1301 addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
1303 addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
1304 addIrred NoSCs (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
1305 addIrred AddSCs state irred = addAvailAndSCs state irred Irred
1307 addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
1308 addAvailAndSCs (avails, frees) wanted avail
1309 = add_avail_and_scs avails wanted avail `thenNF_Tc` \ avails' ->
1310 returnNF_Tc (avails', frees)
1312 ---------------------
1313 add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
1314 add_avail_and_scs avails wanted avail
1315 = add_scs (addToFM avails wanted avail) wanted
1317 add_scs :: Avails -> Inst -> NF_TcM Avails
1318 -- Add all the superclasses of the Inst to Avails
1319 -- Invariant: the Inst is already in Avails.
1322 | not (isClassDict dict)
1323 = returnNF_Tc avails
1325 | otherwise -- It is a dictionary
1326 = newDictsFromOld dict sc_theta' `thenNF_Tc` \ sc_dicts ->
1327 foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1329 (clas, tys) = getDictClassTys dict
1330 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1331 sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1333 add_sc avails (sc_dict, sc_sel) -- Add it, and its superclasses
1334 = case lookupFM avails sc_dict of
1335 Just (BoundTo _) -> returnNF_Tc avails -- See Note [SUPER] below
1336 other -> add_avail_and_scs avails sc_dict avail
1338 sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1339 avail = Rhs sc_sel_rhs [dict]
1342 Note [SUPER]. We have to be careful here. If we are *given* d1:Ord a,
1343 and want to deduce (d2:C [a]) where
1345 class Ord a => C a where
1346 instance Ord a => C [a] where ...
1348 Then we'll use the instance decl to deduce C [a] and then add the
1349 superclasses of C [a] to avails. But we must not overwrite the binding
1350 for d1:Ord a (which is given) with a superclass selection or we'll just
1351 build a loop! Hence looking for BoundTo. Crudely, BoundTo is cheaper
1355 %************************************************************************
1357 \section{tcSimplifyTop: defaulting}
1359 %************************************************************************
1362 If a dictionary constrains a type variable which is
1363 * not mentioned in the environment
1364 * and not mentioned in the type of the expression
1365 then it is ambiguous. No further information will arise to instantiate
1366 the type variable; nor will it be generalised and turned into an extra
1367 parameter to a function.
1369 It is an error for this to occur, except that Haskell provided for
1370 certain rules to be applied in the special case of numeric types.
1372 * at least one of its classes is a numeric class, and
1373 * all of its classes are numeric or standard
1374 then the type variable can be defaulted to the first type in the
1375 default-type list which is an instance of all the offending classes.
1377 So here is the function which does the work. It takes the ambiguous
1378 dictionaries and either resolves them (producing bindings) or
1379 complains. It works by splitting the dictionary list by type
1380 variable, and using @disambigOne@ to do the real business.
1382 @tcSimplifyTop@ is called once per module to simplify all the constant
1383 and ambiguous Insts.
1385 We need to be careful of one case. Suppose we have
1387 instance Num a => Num (Foo a b) where ...
1389 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1390 to (Num x), and default x to Int. But what about y??
1392 It's OK: the final zonking stage should zap y to (), which is fine.
1396 tcSimplifyTop :: LIE -> TcM TcDictBinds
1397 tcSimplifyTop wanted_lie
1398 = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1399 ASSERT( null frees )
1402 -- All the non-std ones are definite errors
1403 (stds, non_stds) = partition isStdClassTyVarDict irreds
1405 -- Group by type variable
1406 std_groups = equivClasses cmp_by_tyvar stds
1408 -- Pick the ones which its worth trying to disambiguate
1409 (std_oks, std_bads) = partition worth_a_try std_groups
1411 -- Have a try at disambiguation
1412 -- if the type variable isn't bound
1413 -- up with one of the non-standard classes
1414 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1415 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
1417 -- Collect together all the bad guys
1418 bad_guys = non_stds ++ concat std_bads
1420 -- Disambiguate the ones that look feasible
1421 mapTc disambigGroup std_oks `thenTc` \ binds_ambig ->
1423 -- And complain about the ones that don't
1424 -- This group includes both non-existent instances
1425 -- e.g. Num (IO a) and Eq (Int -> Int)
1426 -- and ambiguous dictionaries
1428 addTopAmbigErrs bad_guys `thenNF_Tc_`
1430 returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1432 wanteds = lieToList wanted_lie
1433 try_me inst = ReduceMe
1435 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1437 get_tv d = case getDictClassTys d of
1438 (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
1439 get_clas d = case getDictClassTys d of
1440 (clas, [ty]) -> clas
1443 @disambigOne@ assumes that its arguments dictionaries constrain all
1444 the same type variable.
1446 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1447 @()@ instead of @Int@. I reckon this is the Right Thing to do since
1448 the most common use of defaulting is code like:
1450 _ccall_ foo `seqPrimIO` bar
1452 Since we're not using the result of @foo@, the result if (presumably)
1456 disambigGroup :: [Inst] -- All standard classes of form (C a)
1460 | any isNumericClass classes -- Guaranteed all standard classes
1461 -- see comment at the end of function for reasons as to
1462 -- why the defaulting mechanism doesn't apply to groups that
1463 -- include CCallable or CReturnable dicts.
1464 && not (any isCcallishClass classes)
1465 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1466 -- SO, TRY DEFAULT TYPES IN ORDER
1468 -- Failure here is caused by there being no type in the
1469 -- default list which can satisfy all the ambiguous classes.
1470 -- For example, if Real a is reqd, but the only type in the
1471 -- default list is Int.
1472 tcGetDefaultTys `thenNF_Tc` \ default_tys ->
1474 try_default [] -- No defaults work, so fail
1477 try_default (default_ty : default_tys)
1478 = tryTc_ (try_default default_tys) $ -- If default_ty fails, we try
1479 -- default_tys instead
1480 tcSimplifyCheckThetas [] theta `thenTc` \ _ ->
1483 theta = [mkClassPred clas [default_ty] | clas <- classes]
1485 -- See if any default works, and if so bind the type variable to it
1486 -- If not, add an AmbigErr
1487 recoverTc (addAmbigErrs dicts `thenNF_Tc_`
1488 returnTc EmptyMonoBinds) $
1490 try_default default_tys `thenTc` \ chosen_default_ty ->
1492 -- Bind the type variable and reduce the context, for real this time
1493 unifyTauTy chosen_default_ty (mkTyVarTy tyvar) `thenTc_`
1494 simpleReduceLoop (text "disambig" <+> ppr dicts)
1495 try_me dicts `thenTc` \ (frees, binds, ambigs) ->
1496 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1497 warnDefault dicts chosen_default_ty `thenTc_`
1500 | all isCreturnableClass classes
1501 = -- Default CCall stuff to (); we don't even both to check that () is an
1502 -- instance of CReturnable, because we know it is.
1503 unifyTauTy (mkTyVarTy tyvar) unitTy `thenTc_`
1504 returnTc EmptyMonoBinds
1506 | otherwise -- No defaults
1507 = addAmbigErrs dicts `thenNF_Tc_`
1508 returnTc EmptyMonoBinds
1511 try_me inst = ReduceMe -- This reduce should not fail
1512 tyvar = get_tv (head dicts) -- Should be non-empty
1513 classes = map get_clas dicts
1516 [Aside - why the defaulting mechanism is turned off when
1517 dealing with arguments and results to ccalls.
1519 When typechecking _ccall_s, TcExpr ensures that the external
1520 function is only passed arguments (and in the other direction,
1521 results) of a restricted set of 'native' types. This is
1522 implemented via the help of the pseudo-type classes,
1523 @CReturnable@ (CR) and @CCallable@ (CC.)
1525 The interaction between the defaulting mechanism for numeric
1526 values and CC & CR can be a bit puzzling to the user at times.
1535 What type has 'x' got here? That depends on the default list
1536 in operation, if it is equal to Haskell 98's default-default
1537 of (Integer, Double), 'x' has type Double, since Integer
1538 is not an instance of CR. If the default list is equal to
1539 Haskell 1.4's default-default of (Int, Double), 'x' has type
1542 To try to minimise the potential for surprises here, the
1543 defaulting mechanism is turned off in the presence of
1544 CCallable and CReturnable.
1549 %************************************************************************
1551 \subsection[simple]{@Simple@ versions}
1553 %************************************************************************
1555 Much simpler versions when there are no bindings to make!
1557 @tcSimplifyThetas@ simplifies class-type constraints formed by
1558 @deriving@ declarations and when specialising instances. We are
1559 only interested in the simplified bunch of class/type constraints.
1561 It simplifies to constraints of the form (C a b c) where
1562 a,b,c are type variables. This is required for the context of
1563 instance declarations.
1566 tcSimplifyThetas :: ThetaType -- Wanted
1567 -> TcM ThetaType -- Needed
1569 tcSimplifyThetas wanteds
1570 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ glaExts ->
1571 reduceSimple [] wanteds `thenNF_Tc` \ irreds ->
1573 -- For multi-param Haskell, check that the returned dictionaries
1574 -- don't have any of the form (C Int Bool) for which
1575 -- we expect an instance here
1576 -- For Haskell 98, check that all the constraints are of the form C a,
1577 -- where a is a type variable
1578 bad_guys | glaExts = [pred | pred <- irreds,
1579 isEmptyVarSet (tyVarsOfPred pred)]
1580 | otherwise = [pred | pred <- irreds,
1581 not (isTyVarClassPred pred)]
1583 if null bad_guys then
1586 mapNF_Tc addNoInstErr bad_guys `thenNF_Tc_`
1590 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1591 used with \tr{default} declarations. We are only interested in
1592 whether it worked or not.
1595 tcSimplifyCheckThetas :: ThetaType -- Given
1596 -> ThetaType -- Wanted
1599 tcSimplifyCheckThetas givens wanteds
1600 = reduceSimple givens wanteds `thenNF_Tc` \ irreds ->
1604 mapNF_Tc addNoInstErr irreds `thenNF_Tc_`
1610 type AvailsSimple = FiniteMap PredType Bool
1611 -- True => irreducible
1612 -- False => given, or can be derived from a given or from an irreducible
1614 reduceSimple :: ThetaType -- Given
1615 -> ThetaType -- Wanted
1616 -> NF_TcM ThetaType -- Irreducible
1618 reduceSimple givens wanteds
1619 = reduce_simple (0,[]) givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
1620 returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
1622 givens_fm = foldl addNonIrred emptyFM givens
1624 reduce_simple :: (Int,ThetaType) -- Stack
1627 -> NF_TcM AvailsSimple
1629 reduce_simple (n,stack) avails wanteds
1632 go avails [] = returnNF_Tc avails
1633 go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w `thenNF_Tc` \ avails' ->
1636 reduce_simple_help stack givens wanted
1637 | wanted `elemFM` givens
1638 = returnNF_Tc givens
1640 | Just (clas, tys) <- getClassPredTys_maybe wanted
1641 = lookupSimpleInst clas tys `thenNF_Tc` \ maybe_theta ->
1643 Nothing -> returnNF_Tc (addSimpleIrred givens wanted)
1644 Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1647 = returnNF_Tc (addSimpleIrred givens wanted)
1649 addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
1650 addSimpleIrred givens pred
1651 = addSCs (addToFM givens pred True) pred
1653 addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
1654 addNonIrred givens pred
1655 = addSCs (addToFM givens pred False) pred
1658 | not (isClassPred pred) = givens
1659 | otherwise = foldl add givens sc_theta
1661 Just (clas,tys) = getClassPredTys_maybe pred
1662 (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1663 sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1666 = case lookupFM givens ct of
1667 Nothing -> -- Add it and its superclasses
1668 addSCs (addToFM givens ct False) ct
1670 Just True -> -- Set its flag to False; superclasses already done
1671 addToFM givens ct False
1673 Just False -> -- Already done
1679 %************************************************************************
1681 \section{Errors and contexts}
1683 %************************************************************************
1685 ToDo: for these error messages, should we note the location as coming
1686 from the insts, or just whatever seems to be around in the monad just
1690 addTopAmbigErrs dicts
1691 = mapNF_Tc complain tidy_dicts
1693 fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1694 (tidy_env, tidy_dicts) = tidyInsts dicts
1695 complain d | any isIPPred (predsOfInst d) = addTopIPErr tidy_env d
1696 | not (isTyVarDict d) ||
1697 tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
1698 | otherwise = addAmbigErr tidy_env d
1700 addTopIPErr tidy_env tidy_dict
1701 = addInstErrTcM (instLoc tidy_dict)
1703 ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
1705 -- Used for top-level irreducibles
1706 addTopInstanceErr tidy_env tidy_dict
1707 = addInstErrTcM (instLoc tidy_dict)
1709 ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
1712 = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1714 (tidy_env, tidy_dicts) = tidyInsts dicts
1716 addAmbigErr tidy_env tidy_dict
1717 = addInstErrTcM (instLoc tidy_dict)
1719 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1720 nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1722 ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1724 warnDefault dicts default_ty
1725 = doptsTc Opt_WarnTypeDefaults `thenTc` \ warn_flag ->
1726 tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1729 (_, tidy_dicts) = tidyInsts dicts
1730 get_loc i = case instLoc i of { (_,loc,_) -> loc }
1731 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1732 quotes (ppr default_ty),
1733 pprInstsInFull tidy_dicts]
1735 -- The error message when we don't find a suitable instance
1736 -- is complicated by the fact that sometimes this is because
1737 -- there is no instance, and sometimes it's because there are
1738 -- too many instances (overlap). See the comments in TcEnv.lhs
1739 -- with the InstEnv stuff.
1740 addNoInstanceErr what_doc givens dict
1741 = tcGetInstEnv `thenNF_Tc` \ inst_env ->
1743 doc = vcat [sep [herald <+> quotes (pprInst tidy_dict),
1744 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1746 ptext SLIT("Probable fix:"),
1750 herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1751 unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1755 | not ambig_overlap = empty
1757 = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1758 nest 4 (ptext SLIT("depends on the instantiation of") <+>
1759 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
1761 fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
1762 ptext SLIT("to the") <+> what_doc]
1764 fix2 | isTyVarDict dict
1765 || not (isClassDict dict) -- Don't suggest adding instance declarations for implicit parameters
1769 = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
1771 (tidy_env, tidy_dict:tidy_givens) = tidyInsts (dict:givens)
1773 -- Checks for the ambiguous case when we have overlapping instances
1774 ambig_overlap | isClassDict dict
1775 = case lookupInstEnv inst_env clas tys of
1776 NoMatch ambig -> ambig
1780 (clas,tys) = getDictClassTys dict
1782 addInstErrTcM (instLoc dict) (tidy_env, doc)
1784 -- Used for the ...Thetas variants; all top level
1786 = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
1788 reduceDepthErr n stack
1789 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1790 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1791 nest 4 (pprInstsInFull stack)]
1793 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1795 -----------------------------------------------
1797 = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1798 nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])