2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyToDicts, tcSimplifyIPs,
13 tcSimplifySuperClasses,
14 tcSimplifyTop, tcSimplifyInteractive,
17 tcSimplifyDeriv, tcSimplifyDefault,
21 #include "HsVersions.h"
23 import {-# SOURCE #-} TcUnify( unifyTauTy )
24 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
25 import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
28 import Inst ( lookupInst, LookupInstResult(..),
29 tyVarsOfInst, fdPredsOfInsts, newDicts,
30 isDict, isClassDict, isLinearInst, linearInstType,
31 isMethodFor, isMethod,
32 instToId, tyVarsOfInsts, cloneDict,
33 ipNamesOfInsts, ipNamesOfInst, dictPred,
34 instBindingRequired, fdPredsOfInst,
35 newDictsAtLoc, tcInstClassOp,
36 getDictClassTys, isTyVarDict, instLoc,
37 zonkInst, tidyInsts, tidyMoreInsts,
38 Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
39 isInheritableInst, pprDictsTheta
41 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
42 lclEnvElts, tcMetaTy )
43 import InstEnv ( lookupInstEnv, classInstances, pprInstances )
44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType,
46 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
47 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
48 tyVarsOfPred, tcEqType, pprPred, mkPredTy )
49 import TcIface ( checkWiredInTyCon )
50 import Id ( idType, mkUserLocal )
52 import Name ( Name, getOccName, getSrcLoc )
53 import NameSet ( NameSet, mkNameSet, elemNameSet )
54 import Class ( classBigSig, classKey )
55 import FunDeps ( oclose, grow, improve, pprEquationDoc )
56 import PrelInfo ( isNumericClass, isStandardClass )
57 import PrelNames ( splitName, fstName, sndName, integerTyConName,
58 showClassKey, eqClassKey, ordClassKey )
59 import Type ( zipTopTvSubst, substTheta, substTy )
60 import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
61 import ErrUtils ( Message )
62 import BasicTypes ( TopLevelFlag, isNotTopLevel )
64 import VarEnv ( TidyEnv )
68 import ListSetOps ( equivClasses )
69 import Util ( zipEqual, isSingleton )
70 import List ( partition )
71 import SrcLoc ( Located(..) )
72 import DynFlags ( DynFlag(..) )
77 %************************************************************************
81 %************************************************************************
83 --------------------------------------
84 Notes on functional dependencies (a bug)
85 --------------------------------------
87 | > class Foo a b | a->b
89 | > class Bar a b | a->b
93 | > instance Bar Obj Obj
95 | > instance (Bar a b) => Foo a b
97 | > foo:: (Foo a b) => a -> String
100 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
106 | Could not deduce (Bar a b) from the context (Foo a b)
107 | arising from use of `foo' at <interactive>:1
109 | Add (Bar a b) to the expected type of an expression
110 | In the first argument of `runFoo', namely `foo'
111 | In the definition of `it': it = runFoo foo
113 | Why all of the sudden does GHC need the constraint Bar a b? The
114 | function foo didn't ask for that...
116 The trouble is that to type (runFoo foo), GHC has to solve the problem:
118 Given constraint Foo a b
119 Solve constraint Foo a b'
121 Notice that b and b' aren't the same. To solve this, just do
122 improvement and then they are the same. But GHC currently does
127 That is usually fine, but it isn't here, because it sees that Foo a b is
128 not the same as Foo a b', and so instead applies the instance decl for
129 instance Bar a b => Foo a b. And that's where the Bar constraint comes
132 The Right Thing is to improve whenever the constraint set changes at
133 all. Not hard in principle, but it'll take a bit of fiddling to do.
137 --------------------------------------
138 Notes on quantification
139 --------------------------------------
141 Suppose we are about to do a generalisation step.
145 T the type of the RHS
146 C the constraints from that RHS
148 The game is to figure out
150 Q the set of type variables over which to quantify
151 Ct the constraints we will *not* quantify over
152 Cq the constraints we will quantify over
154 So we're going to infer the type
158 and float the constraints Ct further outwards.
160 Here are the things that *must* be true:
162 (A) Q intersect fv(G) = EMPTY limits how big Q can be
163 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
165 (A) says we can't quantify over a variable that's free in the
166 environment. (B) says we must quantify over all the truly free
167 variables in T, else we won't get a sufficiently general type. We do
168 not *need* to quantify over any variable that is fixed by the free
169 vars of the environment G.
171 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
173 Example: class H x y | x->y where ...
175 fv(G) = {a} C = {H a b, H c d}
178 (A) Q intersect {a} is empty
179 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
181 So Q can be {c,d}, {b,c,d}
183 Other things being equal, however, we'd like to quantify over as few
184 variables as possible: smaller types, fewer type applications, more
185 constraints can get into Ct instead of Cq.
188 -----------------------------------------
191 fv(T) the free type vars of T
193 oclose(vs,C) The result of extending the set of tyvars vs
194 using the functional dependencies from C
196 grow(vs,C) The result of extend the set of tyvars vs
197 using all conceivable links from C.
199 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
200 Then grow(vs,C) = {a,b,c}
202 Note that grow(vs,C) `superset` grow(vs,simplify(C))
203 That is, simplfication can only shrink the result of grow.
206 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
207 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
210 -----------------------------------------
214 Here's a good way to choose Q:
216 Q = grow( fv(T), C ) \ oclose( fv(G), C )
218 That is, quantify over all variable that that MIGHT be fixed by the
219 call site (which influences T), but which aren't DEFINITELY fixed by
220 G. This choice definitely quantifies over enough type variables,
221 albeit perhaps too many.
223 Why grow( fv(T), C ) rather than fv(T)? Consider
225 class H x y | x->y where ...
230 If we used fv(T) = {c} we'd get the type
232 forall c. H c d => c -> b
234 And then if the fn was called at several different c's, each of
235 which fixed d differently, we'd get a unification error, because
236 d isn't quantified. Solution: quantify d. So we must quantify
237 everything that might be influenced by c.
239 Why not oclose( fv(T), C )? Because we might not be able to see
240 all the functional dependencies yet:
242 class H x y | x->y where ...
243 instance H x y => Eq (T x y) where ...
248 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
249 apparent yet, and that's wrong. We must really quantify over d too.
252 There really isn't any point in quantifying over any more than
253 grow( fv(T), C ), because the call sites can't possibly influence
254 any other type variables.
258 --------------------------------------
260 --------------------------------------
262 It's very hard to be certain when a type is ambiguous. Consider
266 instance H x y => K (x,y)
268 Is this type ambiguous?
269 forall a b. (K (a,b), Eq b) => a -> a
271 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
272 now we see that a fixes b. So we can't tell about ambiguity for sure
273 without doing a full simplification. And even that isn't possible if
274 the context has some free vars that may get unified. Urgle!
276 Here's another example: is this ambiguous?
277 forall a b. Eq (T b) => a -> a
278 Not if there's an insance decl (with no context)
279 instance Eq (T b) where ...
281 You may say of this example that we should use the instance decl right
282 away, but you can't always do that:
284 class J a b where ...
285 instance J Int b where ...
287 f :: forall a b. J a b => a -> a
289 (Notice: no functional dependency in J's class decl.)
290 Here f's type is perfectly fine, provided f is only called at Int.
291 It's premature to complain when meeting f's signature, or even
292 when inferring a type for f.
296 However, we don't *need* to report ambiguity right away. It'll always
297 show up at the call site.... and eventually at main, which needs special
298 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
300 So here's the plan. We WARN about probable ambiguity if
302 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
304 (all tested before quantification).
305 That is, all the type variables in Cq must be fixed by the the variables
306 in the environment, or by the variables in the type.
308 Notice that we union before calling oclose. Here's an example:
310 class J a b c | a b -> c
314 forall b c. (J a b c) => b -> b
316 Only if we union {a} from G with {b} from T before using oclose,
317 do we see that c is fixed.
319 It's a bit vague exactly which C we should use for this oclose call. If we
320 don't fix enough variables we might complain when we shouldn't (see
321 the above nasty example). Nothing will be perfect. That's why we can
322 only issue a warning.
325 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
327 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
329 then c is a "bubble"; there's no way it can ever improve, and it's
330 certainly ambiguous. UNLESS it is a constant (sigh). And what about
335 instance H x y => K (x,y)
337 Is this type ambiguous?
338 forall a b. (K (a,b), Eq b) => a -> a
340 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
341 is a "bubble" that's a set of constraints
343 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
345 Hence another idea. To decide Q start with fv(T) and grow it
346 by transitive closure in Cq (no functional dependencies involved).
347 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
348 The definitely-ambiguous can then float out, and get smashed at top level
349 (which squashes out the constants, like Eq (T a) above)
352 --------------------------------------
353 Notes on principal types
354 --------------------------------------
359 f x = let g y = op (y::Int) in True
361 Here the principal type of f is (forall a. a->a)
362 but we'll produce the non-principal type
363 f :: forall a. C Int => a -> a
366 --------------------------------------
367 The need for forall's in constraints
368 --------------------------------------
370 [Exchange on Haskell Cafe 5/6 Dec 2000]
372 class C t where op :: t -> Bool
373 instance C [t] where op x = True
375 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
376 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
378 The definitions of p and q differ only in the order of the components in
379 the pair on their right-hand sides. And yet:
381 ghc and "Typing Haskell in Haskell" reject p, but accept q;
382 Hugs rejects q, but accepts p;
383 hbc rejects both p and q;
384 nhc98 ... (Malcolm, can you fill in the blank for us!).
386 The type signature for f forces context reduction to take place, and
387 the results of this depend on whether or not the type of y is known,
388 which in turn depends on which component of the pair the type checker
391 Solution: if y::m a, float out the constraints
392 Monad m, forall c. C (m c)
393 When m is later unified with [], we can solve both constraints.
396 --------------------------------------
397 Notes on implicit parameters
398 --------------------------------------
400 Question 1: can we "inherit" implicit parameters
401 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
406 where f is *not* a top-level binding.
407 From the RHS of f we'll get the constraint (?y::Int).
408 There are two types we might infer for f:
412 (so we get ?y from the context of f's definition), or
414 f :: (?y::Int) => Int -> Int
416 At first you might think the first was better, becuase then
417 ?y behaves like a free variable of the definition, rather than
418 having to be passed at each call site. But of course, the WHOLE
419 IDEA is that ?y should be passed at each call site (that's what
420 dynamic binding means) so we'd better infer the second.
422 BOTTOM LINE: when *inferring types* you *must* quantify
423 over implicit parameters. See the predicate isFreeWhenInferring.
426 Question 2: type signatures
427 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
428 BUT WATCH OUT: When you supply a type signature, we can't force you
429 to quantify over implicit parameters. For example:
433 This is perfectly reasonable. We do not want to insist on
435 (?x + 1) :: (?x::Int => Int)
437 That would be silly. Here, the definition site *is* the occurrence site,
438 so the above strictures don't apply. Hence the difference between
439 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
440 and tcSimplifyCheckBind (which does not).
442 What about when you supply a type signature for a binding?
443 Is it legal to give the following explicit, user type
444 signature to f, thus:
449 At first sight this seems reasonable, but it has the nasty property
450 that adding a type signature changes the dynamic semantics.
453 (let f x = (x::Int) + ?y
454 in (f 3, f 3 with ?y=5)) with ?y = 6
460 in (f 3, f 3 with ?y=5)) with ?y = 6
464 Indeed, simply inlining f (at the Haskell source level) would change the
467 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
468 semantics for a Haskell program without knowing its typing, so if you
469 change the typing you may change the semantics.
471 To make things consistent in all cases where we are *checking* against
472 a supplied signature (as opposed to inferring a type), we adopt the
475 a signature does not need to quantify over implicit params.
477 [This represents a (rather marginal) change of policy since GHC 5.02,
478 which *required* an explicit signature to quantify over all implicit
479 params for the reasons mentioned above.]
481 But that raises a new question. Consider
483 Given (signature) ?x::Int
484 Wanted (inferred) ?x::Int, ?y::Bool
486 Clearly we want to discharge the ?x and float the ?y out. But
487 what is the criterion that distinguishes them? Clearly it isn't
488 what free type variables they have. The Right Thing seems to be
489 to float a constraint that
490 neither mentions any of the quantified type variables
491 nor any of the quantified implicit parameters
493 See the predicate isFreeWhenChecking.
496 Question 3: monomorphism
497 ~~~~~~~~~~~~~~~~~~~~~~~~
498 There's a nasty corner case when the monomorphism restriction bites:
502 The argument above suggests that we *must* generalise
503 over the ?y parameter, to get
504 z :: (?y::Int) => Int,
505 but the monomorphism restriction says that we *must not*, giving
507 Why does the momomorphism restriction say this? Because if you have
509 let z = x + ?y in z+z
511 you might not expect the addition to be done twice --- but it will if
512 we follow the argument of Question 2 and generalise over ?y.
515 Question 4: top level
516 ~~~~~~~~~~~~~~~~~~~~~
517 At the top level, monomorhism makes no sense at all.
520 main = let ?x = 5 in print foo
524 woggle :: (?x :: Int) => Int -> Int
527 We definitely don't want (foo :: Int) with a top-level implicit parameter
528 (?x::Int) becuase there is no way to bind it.
533 (A) Always generalise over implicit parameters
534 Bindings that fall under the monomorphism restriction can't
538 * Inlining remains valid
539 * No unexpected loss of sharing
540 * But simple bindings like
542 will be rejected, unless you add an explicit type signature
543 (to avoid the monomorphism restriction)
544 z :: (?y::Int) => Int
546 This seems unacceptable
548 (B) Monomorphism restriction "wins"
549 Bindings that fall under the monomorphism restriction can't
551 Always generalise over implicit parameters *except* for bindings
552 that fall under the monomorphism restriction
555 * Inlining isn't valid in general
556 * No unexpected loss of sharing
557 * Simple bindings like
559 accepted (get value of ?y from binding site)
561 (C) Always generalise over implicit parameters
562 Bindings that fall under the monomorphism restriction can't
563 be generalised, EXCEPT for implicit parameters
565 * Inlining remains valid
566 * Unexpected loss of sharing (from the extra generalisation)
567 * Simple bindings like
569 accepted (get value of ?y from occurrence sites)
574 None of these choices seems very satisfactory. But at least we should
575 decide which we want to do.
577 It's really not clear what is the Right Thing To Do. If you see
581 would you expect the value of ?y to be got from the *occurrence sites*
582 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
583 case of function definitions, the answer is clearly the former, but
584 less so in the case of non-fucntion definitions. On the other hand,
585 if we say that we get the value of ?y from the definition site of 'z',
586 then inlining 'z' might change the semantics of the program.
588 Choice (C) really says "the monomorphism restriction doesn't apply
589 to implicit parameters". Which is fine, but remember that every
590 innocent binding 'x = ...' that mentions an implicit parameter in
591 the RHS becomes a *function* of that parameter, called at each
592 use of 'x'. Now, the chances are that there are no intervening 'with'
593 clauses that bind ?y, so a decent compiler should common up all
594 those function calls. So I think I strongly favour (C). Indeed,
595 one could make a similar argument for abolishing the monomorphism
596 restriction altogether.
598 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
602 %************************************************************************
604 \subsection{tcSimplifyInfer}
606 %************************************************************************
608 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
610 1. Compute Q = grow( fvs(T), C )
612 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
613 predicates will end up in Ct; we deal with them at the top level
615 3. Try improvement, using functional dependencies
617 4. If Step 3 did any unification, repeat from step 1
618 (Unification can change the result of 'grow'.)
620 Note: we don't reduce dictionaries in step 2. For example, if we have
621 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
622 after step 2. However note that we may therefore quantify over more
623 type variables than we absolutely have to.
625 For the guts, we need a loop, that alternates context reduction and
626 improvement with unification. E.g. Suppose we have
628 class C x y | x->y where ...
630 and tcSimplify is called with:
632 Then improvement unifies a with b, giving
635 If we need to unify anything, we rattle round the whole thing all over
642 -> TcTyVarSet -- fv(T); type vars
644 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
645 TcDictBinds, -- Bindings
646 [TcId]) -- Dict Ids that must be bound here (zonked)
647 -- Any free (escaping) Insts are tossed into the environment
652 tcSimplifyInfer doc tau_tvs wanted_lie
653 = inferLoop doc (varSetElems tau_tvs)
654 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
656 extendLIEs frees `thenM_`
657 returnM (qtvs, binds, map instToId irreds)
659 inferLoop doc tau_tvs wanteds
661 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
662 mappM zonkInst wanteds `thenM` \ wanteds' ->
663 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
665 preds = fdPredsOfInsts wanteds'
666 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
669 | isFreeWhenInferring qtvs inst = Free
670 | isClassDict inst = DontReduceUnlessConstant -- Dicts
671 | otherwise = ReduceMe NoSCs -- Lits and Methods
673 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
674 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
676 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
679 if no_improvement then
680 returnM (varSetElems qtvs, frees, binds, irreds)
682 -- If improvement did some unification, we go round again. There
683 -- are two subtleties:
684 -- a) We start again with irreds, not wanteds
685 -- Using an instance decl might have introduced a fresh type variable
686 -- which might have been unified, so we'd get an infinite loop
687 -- if we started again with wanteds! See example [LOOP]
689 -- b) It's also essential to re-process frees, because unification
690 -- might mean that a type variable that looked free isn't now.
692 -- Hence the (irreds ++ frees)
694 -- However, NOTICE that when we are done, we might have some bindings, but
695 -- the final qtvs might be empty. See [NO TYVARS] below.
697 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
698 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
703 class If b t e r | b t e -> r
706 class Lte a b c | a b -> c where lte :: a -> b -> c
708 instance (Lte a b l,If l b a c) => Max a b c
710 Wanted: Max Z (S x) y
712 Then we'll reduce using the Max instance to:
713 (Lte Z (S x) l, If l (S x) Z y)
714 and improve by binding l->T, after which we can do some reduction
715 on both the Lte and If constraints. What we *can't* do is start again
716 with (Max Z (S x) y)!
720 class Y a b | a -> b where
723 instance Y [[a]] a where
726 k :: X a -> X a -> X a
728 g :: Num a => [X a] -> [X a]
731 h ys = ys ++ map (k (y [[0]])) xs
733 The excitement comes when simplifying the bindings for h. Initially
734 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
735 From this we get t1:=:t2, but also various bindings. We can't forget
736 the bindings (because of [LOOP]), but in fact t1 is what g is
739 The net effect of [NO TYVARS]
742 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
743 isFreeWhenInferring qtvs inst
744 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
745 && isInheritableInst inst -- And no implicit parameter involved
746 -- (see "Notes on implicit parameters")
748 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
749 -> NameSet -- Quantified implicit parameters
751 isFreeWhenChecking qtvs ips inst
752 = isFreeWrtTyVars qtvs inst
753 && isFreeWrtIPs ips inst
755 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
756 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
760 %************************************************************************
762 \subsection{tcSimplifyCheck}
764 %************************************************************************
766 @tcSimplifyCheck@ is used when we know exactly the set of variables
767 we are going to quantify over. For example, a class or instance declaration.
772 -> [TcTyVar] -- Quantify over these
775 -> TcM TcDictBinds -- Bindings
777 -- tcSimplifyCheck is used when checking expression type signatures,
778 -- class decls, instance decls etc.
780 -- NB: tcSimplifyCheck does not consult the
781 -- global type variables in the environment; so you don't
782 -- need to worry about setting them before calling tcSimplifyCheck
783 tcSimplifyCheck doc qtvs givens wanted_lie
784 = ASSERT( all isSkolemTyVar qtvs )
785 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
789 -- get_qtvs = zonkTcTyVarsAndFV qtvs
790 get_qtvs = return (mkVarSet qtvs) -- All skolems
793 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
794 -- against, but we don't know the type variables over which we are going to quantify.
795 -- This happens when we have a type signature for a mutually recursive group
798 -> TcTyVarSet -- fv(T)
801 -> TcM ([TcTyVar], -- Variables over which to quantify
802 TcDictBinds) -- Bindings
804 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
805 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
807 ; return (qtvs', binds) }
809 -- Figure out which type variables to quantify over
810 -- You might think it should just be the signature tyvars,
811 -- but in bizarre cases you can get extra ones
812 -- f :: forall a. Num a => a -> a
813 -- f x = fst (g (x, head [])) + 1
815 -- Here we infer g :: forall a b. a -> b -> (b,a)
816 -- We don't want g to be monomorphic in b just because
817 -- f isn't quantified over b.
818 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
820 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
821 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
823 qtvs = all_tvs' `minusVarSet` gbl_tvs
824 -- We could close gbl_tvs, but its not necessary for
825 -- soundness, and it'll only affect which tyvars, not which
826 -- dictionaries, we quantify over
831 Here is the workhorse function for all three wrappers.
834 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
835 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
837 -- Complain about any irreducible ones
838 ; if not (null irreds)
839 then do { givens' <- mappM zonkInst given_dicts_and_ips
840 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
843 ; returnM (qtvs, frees, binds) }
845 given_dicts_and_ips = filter (not . isMethod) givens
846 -- For error reporting, filter out methods, which are
847 -- only added to the given set as an optimisation
849 ip_set = mkNameSet (ipNamesOfInsts givens)
851 check_loop givens wanteds
853 mappM zonkInst givens `thenM` \ givens' ->
854 mappM zonkInst wanteds `thenM` \ wanteds' ->
855 get_qtvs `thenM` \ qtvs' ->
859 -- When checking against a given signature we always reduce
860 -- until we find a match against something given, or can't reduce
861 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
862 | otherwise = ReduceMe want_scs
864 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
867 if no_improvement then
868 returnM (varSetElems qtvs', frees, binds, irreds)
870 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
871 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
875 %************************************************************************
877 tcSimplifySuperClasses
879 %************************************************************************
881 Note [SUPERCLASS-LOOP 1]
882 ~~~~~~~~~~~~~~~~~~~~~~~~
883 We have to be very, very careful when generating superclasses, lest we
884 accidentally build a loop. Here's an example:
888 class S a => C a where { opc :: a -> a }
889 class S b => D b where { opd :: b -> b }
897 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
898 Simplifying, we may well get:
899 $dfCInt = :C ds1 (opd dd)
902 Notice that we spot that we can extract ds1 from dd.
904 Alas! Alack! We can do the same for (instance D Int):
906 $dfDInt = :D ds2 (opc dc)
910 And now we've defined the superclass in terms of itself.
912 Solution: never generate a superclass selectors at all when
913 satisfying the superclass context of an instance declaration.
915 Two more nasty cases are in
920 tcSimplifySuperClasses qtvs givens sc_wanteds
921 = ASSERT( all isSkolemTyVar qtvs )
922 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
923 ; binds2 <- tc_simplify_top doc False NoSCs frees
924 ; return (binds1 `unionBags` binds2) }
926 get_qtvs = return (mkVarSet qtvs)
927 doc = ptext SLIT("instance declaration superclass context")
931 %************************************************************************
933 \subsection{tcSimplifyRestricted}
935 %************************************************************************
937 tcSimplifyRestricted infers which type variables to quantify for a
938 group of restricted bindings. This isn't trivial.
941 We want to quantify over a to get id :: forall a. a->a
944 We do not want to quantify over a, because there's an Eq a
945 constraint, so we get eq :: a->a->Bool (notice no forall)
948 RHS has type 'tau', whose free tyvars are tau_tvs
949 RHS has constraints 'wanteds'
952 Quantify over (tau_tvs \ ftvs(wanteds))
953 This is bad. The constraints may contain (Monad (ST s))
954 where we have instance Monad (ST s) where...
955 so there's no need to be monomorphic in s!
957 Also the constraint might be a method constraint,
958 whose type mentions a perfectly innocent tyvar:
959 op :: Num a => a -> b -> a
960 Here, b is unconstrained. A good example would be
962 We want to infer the polymorphic type
963 foo :: forall b. b -> b
966 Plan B (cunning, used for a long time up to and including GHC 6.2)
967 Step 1: Simplify the constraints as much as possible (to deal
968 with Plan A's problem). Then set
969 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
971 Step 2: Now simplify again, treating the constraint as 'free' if
972 it does not mention qtvs, and trying to reduce it otherwise.
973 The reasons for this is to maximise sharing.
975 This fails for a very subtle reason. Suppose that in the Step 2
976 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
977 In the Step 1 this constraint might have been simplified, perhaps to
978 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
979 This won't happen in Step 2... but that in turn might prevent some other
980 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
981 and that in turn breaks the invariant that no constraints are quantified over.
983 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
988 Step 1: Simplify the constraints as much as possible (to deal
989 with Plan A's problem). Then set
990 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
991 Return the bindings from Step 1.
994 A note about Plan C (arising from "bug" reported by George Russel March 2004)
997 instance (HasBinary ty IO) => HasCodedValue ty
999 foo :: HasCodedValue a => String -> IO a
1001 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1002 doDecodeIO codedValue view
1003 = let { act = foo "foo" } in act
1005 You might think this should work becuase the call to foo gives rise to a constraint
1006 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1007 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1008 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1010 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1014 Plan D (a variant of plan B)
1015 Step 1: Simplify the constraints as much as possible (to deal
1016 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1017 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1019 Step 2: Now simplify again, treating the constraint as 'free' if
1020 it does not mention qtvs, and trying to reduce it otherwise.
1022 The point here is that it's generally OK to have too few qtvs; that is,
1023 to make the thing more monomorphic than it could be. We don't want to
1024 do that in the common cases, but in wierd cases it's ok: the programmer
1025 can always add a signature.
1027 Too few qtvs => too many wanteds, which is what happens if you do less
1032 tcSimplifyRestricted -- Used for restricted binding groups
1033 -- i.e. ones subject to the monomorphism restriction
1036 -> [Name] -- Things bound in this group
1037 -> TcTyVarSet -- Free in the type of the RHSs
1038 -> [Inst] -- Free in the RHSs
1039 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1040 TcDictBinds) -- Bindings
1041 -- tcSimpifyRestricted returns no constraints to
1042 -- quantify over; by definition there are none.
1043 -- They are all thrown back in the LIE
1045 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1046 -- Zonk everything in sight
1047 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1048 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1049 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1051 -- 'reduceMe': Reduce as far as we can. Don't stop at
1052 -- dicts; the idea is to get rid of as many type
1053 -- variables as possible, and we don't want to stop
1054 -- at (say) Monad (ST s), because that reduces
1055 -- immediately, with no constraint on s.
1057 -- BUT do no improvement! See Plan D above
1058 reduceContextWithoutImprovement
1059 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1061 -- Next, figure out the tyvars we will quantify over
1063 constrained_tvs = tyVarsOfInsts constrained_dicts
1064 qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1065 `minusVarSet` constrained_tvs
1067 traceTc (text "tcSimplifyRestricted" <+> vcat [
1068 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
1070 ppr constrained_tvs, ppr tau_tvs', ppr qtvs ]) `thenM_`
1072 -- The first step may have squashed more methods than
1073 -- necessary, so try again, this time more gently, knowing the exact
1074 -- set of type variables to quantify over.
1076 -- We quantify only over constraints that are captured by qtvs;
1077 -- these will just be a subset of non-dicts. This in contrast
1078 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1079 -- all *non-inheritable* constraints too. This implements choice
1080 -- (B) under "implicit parameter and monomorphism" above.
1082 -- Remember that we may need to do *some* simplification, to
1083 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1084 -- just to float all constraints
1086 -- At top level, we *do* squash methods becuase we want to
1087 -- expose implicit parameters to the test that follows
1089 is_nested_group = isNotTopLevel top_lvl
1090 try_me inst | isFreeWrtTyVars qtvs inst,
1091 (is_nested_group || isDict inst) = Free
1092 | otherwise = ReduceMe AddSCs
1094 reduceContextWithoutImprovement
1095 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1096 ASSERT( null irreds )
1098 -- See "Notes on implicit parameters, Question 4: top level"
1099 if is_nested_group then
1100 extendLIEs frees `thenM_`
1101 returnM (varSetElems qtvs, binds)
1104 (non_ips, bad_ips) = partition isClassDict frees
1106 addTopIPErrs bndrs bad_ips `thenM_`
1107 extendLIEs non_ips `thenM_`
1108 returnM (varSetElems qtvs, binds)
1112 %************************************************************************
1114 \subsection{tcSimplifyToDicts}
1116 %************************************************************************
1118 On the LHS of transformation rules we only simplify methods and constants,
1119 getting dictionaries. We want to keep all of them unsimplified, to serve
1120 as the available stuff for the RHS of the rule.
1122 The same thing is used for specialise pragmas. Consider
1124 f :: Num a => a -> a
1125 {-# SPECIALISE f :: Int -> Int #-}
1128 The type checker generates a binding like:
1130 f_spec = (f :: Int -> Int)
1132 and we want to end up with
1134 f_spec = _inline_me_ (f Int dNumInt)
1136 But that means that we must simplify the Method for f to (f Int dNumInt)!
1137 So tcSimplifyToDicts squeezes out all Methods.
1139 IMPORTANT NOTE: we *don't* want to do superclass commoning up. Consider
1141 fromIntegral :: (Integral a, Num b) => a -> b
1142 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1144 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
1147 forall dIntegralInt.
1148 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1150 because the scsel will mess up RULE matching. Instead we want
1152 forall dIntegralInt, dNumInt.
1153 fromIntegral Int Int dIntegralInt dNumInt = id Int
1158 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
1159 tcSimplifyToDicts wanteds
1160 = simpleReduceLoop doc try_me wanteds `thenM` \ (frees, binds, irreds) ->
1161 -- Since try_me doesn't look at types, we don't need to
1162 -- do any zonking, so it's safe to call reduceContext directly
1163 ASSERT( null frees )
1164 extendLIEs irreds `thenM_`
1168 doc = text "tcSimplifyToDicts"
1170 -- Reduce methods and lits only; stop as soon as we get a dictionary
1171 try_me inst | isDict inst = KeepDictWithoutSCs -- See notes above re "WithoutSCs"
1172 | otherwise = ReduceMe NoSCs
1177 tcSimplifyBracket is used when simplifying the constraints arising from
1178 a Template Haskell bracket [| ... |]. We want to check that there aren't
1179 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1180 Show instance), but we aren't otherwise interested in the results.
1181 Nor do we care about ambiguous dictionaries etc. We will type check
1182 this bracket again at its usage site.
1185 tcSimplifyBracket :: [Inst] -> TcM ()
1186 tcSimplifyBracket wanteds
1187 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1190 doc = text "tcSimplifyBracket"
1194 %************************************************************************
1196 \subsection{Filtering at a dynamic binding}
1198 %************************************************************************
1203 we must discharge all the ?x constraints from B. We also do an improvement
1204 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1206 Actually, the constraints from B might improve the types in ?x. For example
1208 f :: (?x::Int) => Char -> Char
1211 then the constraint (?x::Int) arising from the call to f will
1212 force the binding for ?x to be of type Int.
1215 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1218 tcSimplifyIPs given_ips wanteds
1219 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1220 extendLIEs frees `thenM_`
1223 doc = text "tcSimplifyIPs" <+> ppr given_ips
1224 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1226 -- Simplify any methods that mention the implicit parameter
1227 try_me inst | isFreeWrtIPs ip_set inst = Free
1228 | otherwise = ReduceMe NoSCs
1230 simpl_loop givens wanteds
1231 = mappM zonkInst givens `thenM` \ givens' ->
1232 mappM zonkInst wanteds `thenM` \ wanteds' ->
1234 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1236 if no_improvement then
1237 ASSERT( null irreds )
1238 returnM (frees, binds)
1240 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1241 returnM (frees1, binds `unionBags` binds1)
1245 %************************************************************************
1247 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1249 %************************************************************************
1251 When doing a binding group, we may have @Insts@ of local functions.
1252 For example, we might have...
1254 let f x = x + 1 -- orig local function (overloaded)
1255 f.1 = f Int -- two instances of f
1260 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1261 where @f@ is in scope; those @Insts@ must certainly not be passed
1262 upwards towards the top-level. If the @Insts@ were binding-ified up
1263 there, they would have unresolvable references to @f@.
1265 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1266 For each method @Inst@ in the @init_lie@ that mentions one of the
1267 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1268 @LIE@), as well as the @HsBinds@ generated.
1271 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1272 -- Simlifies only MethodInsts, and generate only bindings of form
1274 -- We're careful not to even generate bindings of the form
1276 -- You'd think that'd be fine, but it interacts with what is
1277 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1279 bindInstsOfLocalFuns wanteds local_ids
1280 | null overloaded_ids
1282 = extendLIEs wanteds `thenM_`
1283 returnM emptyLHsBinds
1286 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1287 ASSERT( null irreds )
1288 extendLIEs not_for_me `thenM_`
1289 extendLIEs frees `thenM_`
1292 doc = text "bindInsts" <+> ppr local_ids
1293 overloaded_ids = filter is_overloaded local_ids
1294 is_overloaded id = isOverloadedTy (idType id)
1295 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1297 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1298 -- so it's worth building a set, so that
1299 -- lookup (in isMethodFor) is faster
1300 try_me inst | isMethod inst = ReduceMe NoSCs
1305 %************************************************************************
1307 \subsection{Data types for the reduction mechanism}
1309 %************************************************************************
1311 The main control over context reduction is here
1315 = ReduceMe WantSCs -- Try to reduce this
1316 -- If there's no instance, behave exactly like
1317 -- DontReduce: add the inst to the irreductible ones,
1318 -- but don't produce an error message of any kind.
1319 -- It might be quite legitimate such as (Eq a)!
1321 | KeepDictWithoutSCs -- Return as irreducible; don't add its superclasses
1322 -- Rather specialised: see notes with tcSimplifyToDicts
1324 | DontReduceUnlessConstant -- Return as irreducible unless it can
1325 -- be reduced to a constant in one step
1327 | Free -- Return as free
1329 reduceMe :: Inst -> WhatToDo
1330 reduceMe inst = ReduceMe AddSCs
1332 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1333 -- of a predicate when adding it to the avails
1334 -- The reason for this flag is entirely the super-class loop problem
1335 -- Note [SUPER-CLASS LOOP 1]
1341 type Avails = FiniteMap Inst Avail
1342 emptyAvails = emptyFM
1345 = IsFree -- Used for free Insts
1346 | Irred -- Used for irreducible dictionaries,
1347 -- which are going to be lambda bound
1349 | Given TcId -- Used for dictionaries for which we have a binding
1350 -- e.g. those "given" in a signature
1351 Bool -- True <=> actually consumed (splittable IPs only)
1353 | NoRhs -- Used for Insts like (CCallable f)
1354 -- where no witness is required.
1357 | Rhs -- Used when there is a RHS
1358 (LHsExpr TcId) -- The RHS
1359 [Inst] -- Insts free in the RHS; we need these too
1361 | Linear -- Splittable Insts only.
1362 Int -- The Int is always 2 or more; indicates how
1363 -- many copies are required
1364 Inst -- The splitter
1365 Avail -- Where the "master copy" is
1367 | LinRhss -- Splittable Insts only; this is used only internally
1368 -- by extractResults, where a Linear
1369 -- is turned into an LinRhss
1370 [LHsExpr TcId] -- A supply of suitable RHSs
1372 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1373 | (inst,avail) <- fmToList avails ]
1375 instance Outputable Avail where
1378 pprAvail NoRhs = text "<no rhs>"
1379 pprAvail IsFree = text "Free"
1380 pprAvail Irred = text "Irred"
1381 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1382 if b then text "(used)" else empty
1383 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1384 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1385 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1388 Extracting the bindings from a bunch of Avails.
1389 The bindings do *not* come back sorted in dependency order.
1390 We assume that they'll be wrapped in a big Rec, so that the
1391 dependency analyser can sort them out later
1395 extractResults :: Avails
1397 -> TcM (TcDictBinds, -- Bindings
1398 [Inst], -- Irreducible ones
1399 [Inst]) -- Free ones
1401 extractResults avails wanteds
1402 = go avails emptyBag [] [] wanteds
1404 go avails binds irreds frees []
1405 = returnM (binds, irreds, frees)
1407 go avails binds irreds frees (w:ws)
1408 = case lookupFM avails w of
1409 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1410 go avails binds irreds frees ws
1412 Just NoRhs -> go avails binds irreds frees ws
1413 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1414 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1416 Just (Given id _) -> go avails new_binds irreds frees ws
1418 new_binds | id == instToId w = binds
1419 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1420 -- The sought Id can be one of the givens, via a superclass chain
1421 -- and then we definitely don't want to generate an x=x binding!
1423 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1425 new_binds = addBind binds w rhs
1427 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1428 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1429 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1430 go (addToFM avails w (LinRhss rhss))
1431 (binds `unionBags` binds')
1432 irreds' frees' (split_inst : w : ws)
1434 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1435 -> go new_avails new_binds irreds frees ws
1437 new_binds = addBind binds w rhs
1438 new_avails = addToFM avails w (LinRhss rhss)
1440 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1441 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1442 returnM (w':irreds, frees, instToId w')
1443 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1444 returnM (irreds, w':frees, instToId w')
1447 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1448 | otherwise = addToFM avails w NoRhs
1449 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1450 -- than Given, else we end up with bogus bindings.
1452 add_free avails w | isMethod w = avails
1453 | otherwise = add_given avails w
1455 -- Do *not* replace Free by Given if it's a method.
1456 -- The following situation shows why this is bad:
1457 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1458 -- From an application (truncate f i) we get
1459 -- t1 = truncate at f
1461 -- If we have also have a second occurrence of truncate, we get
1462 -- t3 = truncate at f
1464 -- When simplifying with i,f free, we might still notice that
1465 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1466 -- will continue to float out!
1467 -- (split n i a) returns: n rhss
1468 -- auxiliary bindings
1469 -- 1 or 0 insts to add to irreds
1472 split :: Int -> TcId -> TcId -> Inst
1473 -> TcM (TcDictBinds, [LHsExpr TcId])
1474 -- (split n split_id root_id wanted) returns
1475 -- * a list of 'n' expressions, all of which witness 'avail'
1476 -- * a bunch of auxiliary bindings to support these expressions
1477 -- * one or zero insts needed to witness the whole lot
1478 -- (maybe be zero if the initial Inst is a Given)
1480 -- NB: 'wanted' is just a template
1482 split n split_id root_id wanted
1485 ty = linearInstType wanted
1486 pair_ty = mkTyConApp pairTyCon [ty,ty]
1487 id = instToId wanted
1490 span = instSpan wanted
1492 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1494 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1495 expand n rhss `thenM` \ (binds2, rhss') ->
1496 returnM (binds1 `unionBags` binds2, rhss')
1499 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1500 -- e.g. expand 3 [rhs1, rhs2]
1501 -- = ( { x = split rhs1 },
1502 -- [fst x, snd x, rhs2] )
1504 | n `rem` 2 == 0 = go rhss -- n is even
1505 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1506 returnM (binds', head rhss : rhss')
1508 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1509 returnM (listToBag binds', concat rhss')
1511 do_one rhs = newUnique `thenM` \ uniq ->
1512 tcLookupId fstName `thenM` \ fst_id ->
1513 tcLookupId sndName `thenM` \ snd_id ->
1515 x = mkUserLocal occ uniq pair_ty loc
1517 returnM (L span (VarBind x (mk_app span split_id rhs)),
1518 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1520 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1522 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1524 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1525 (VarBind (instToId inst) rhs))
1526 instSpan wanted = instLocSrcSpan (instLoc wanted)
1530 %************************************************************************
1532 \subsection[reduce]{@reduce@}
1534 %************************************************************************
1536 When the "what to do" predicate doesn't depend on the quantified type variables,
1537 matters are easier. We don't need to do any zonking, unless the improvement step
1538 does something, in which case we zonk before iterating.
1540 The "given" set is always empty.
1543 simpleReduceLoop :: SDoc
1544 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1546 -> TcM ([Inst], -- Free
1548 [Inst]) -- Irreducible
1550 simpleReduceLoop doc try_me wanteds
1551 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1552 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1553 if no_improvement then
1554 returnM (frees, binds, irreds)
1556 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1557 returnM (frees1, binds `unionBags` binds1, irreds1)
1563 reduceContext :: SDoc
1564 -> (Inst -> WhatToDo)
1567 -> TcM (Bool, -- True <=> improve step did no unification
1569 TcDictBinds, -- Dictionary bindings
1570 [Inst]) -- Irreducible
1572 reduceContext doc try_me givens wanteds
1574 traceTc (text "reduceContext" <+> (vcat [
1575 text "----------------------",
1577 text "given" <+> ppr givens,
1578 text "wanted" <+> ppr wanteds,
1579 text "----------------------"
1582 -- Build the Avail mapping from "givens"
1583 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1586 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1588 -- Do improvement, using everything in avails
1589 -- In particular, avails includes all superclasses of everything
1590 tcImprove avails `thenM` \ no_improvement ->
1592 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1594 traceTc (text "reduceContext end" <+> (vcat [
1595 text "----------------------",
1597 text "given" <+> ppr givens,
1598 text "wanted" <+> ppr wanteds,
1600 text "avails" <+> pprAvails avails,
1601 text "frees" <+> ppr frees,
1602 text "no_improvement =" <+> ppr no_improvement,
1603 text "----------------------"
1606 returnM (no_improvement, frees, binds, irreds)
1608 -- reduceContextWithoutImprovement differs from reduceContext
1609 -- (a) no improvement
1610 -- (b) 'givens' is assumed empty
1611 reduceContextWithoutImprovement doc try_me wanteds
1613 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1614 text "----------------------",
1616 text "wanted" <+> ppr wanteds,
1617 text "----------------------"
1621 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1622 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1624 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1625 text "----------------------",
1627 text "wanted" <+> ppr wanteds,
1629 text "avails" <+> pprAvails avails,
1630 text "frees" <+> ppr frees,
1631 text "----------------------"
1634 returnM (frees, binds, irreds)
1636 tcImprove :: Avails -> TcM Bool -- False <=> no change
1637 -- Perform improvement using all the predicates in Avails
1639 = tcGetInstEnvs `thenM` \ inst_envs ->
1641 preds = [ (pred, pp_loc)
1642 | (inst, avail) <- fmToList avails,
1643 pred <- get_preds inst avail,
1644 let pp_loc = pprInstLoc (instLoc inst)
1646 -- Avails has all the superclasses etc (good)
1647 -- It also has all the intermediates of the deduction (good)
1648 -- It does not have duplicates (good)
1649 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1650 -- so that improve will see them separate
1652 -- For free Methods, we want to take predicates from their context,
1653 -- but for Methods that have been squished their context will already
1654 -- be in Avails, and we don't want duplicates. Hence this rather
1655 -- horrid get_preds function
1656 get_preds inst IsFree = fdPredsOfInst inst
1657 get_preds inst other | isDict inst = [dictPred inst]
1660 eqns = improve get_insts preds
1661 get_insts clas = classInstances inst_envs clas
1666 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1667 mappM_ unify eqns `thenM_`
1670 unify ((qtvs, pairs), doc)
1672 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1673 mapM_ (unif_pr tenv) pairs
1674 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1677 The main context-reduction function is @reduce@. Here's its game plan.
1680 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1681 -- along with its depth
1682 -> (Inst -> WhatToDo)
1689 try_me: given an inst, this function returns
1691 DontReduce return this in "irreds"
1692 Free return this in "frees"
1694 wanteds: The list of insts to reduce
1695 state: An accumulating parameter of type Avails
1696 that contains the state of the algorithm
1698 It returns a Avails.
1700 The (n,stack) pair is just used for error reporting.
1701 n is always the depth of the stack.
1702 The stack is the stack of Insts being reduced: to produce X
1703 I had to produce Y, to produce Y I had to produce Z, and so on.
1706 reduceList (n,stack) try_me wanteds state
1707 | n > opt_MaxContextReductionDepth
1708 = failWithTc (reduceDepthErr n stack)
1714 pprTrace "Interesting! Context reduction stack deeper than 8:"
1715 (nest 2 (pprStack stack))
1720 go [] state = returnM state
1721 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1724 -- Base case: we're done!
1725 reduce stack try_me wanted avails
1726 -- It's the same as an existing inst, or a superclass thereof
1727 | Just avail <- isAvailable avails wanted
1728 = if isLinearInst wanted then
1729 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1730 reduceList stack try_me wanteds' avails'
1732 returnM avails -- No op for non-linear things
1735 = case try_me wanted of {
1737 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1739 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1740 -- First, see if the inst can be reduced to a constant in one step
1741 try_simple (addIrred AddSCs) -- Assume want superclasses
1743 ; Free -> -- It's free so just chuck it upstairs
1744 -- First, see if the inst can be reduced to a constant in one step
1747 ; ReduceMe want_scs -> -- It should be reduced
1748 lookupInst wanted `thenM` \ lookup_result ->
1749 case lookup_result of
1750 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1751 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1752 addWanted want_scs avails2 wanted rhs wanteds'
1753 -- Experiment with temporarily doing addIrred *before* the reduceList,
1754 -- which has the effect of adding the thing we are trying
1755 -- to prove to the database before trying to prove the things it
1756 -- needs. See note [RECURSIVE DICTIONARIES]
1757 -- NB: we must not do an addWanted before, because that adds the
1758 -- superclasses too, and thaat can lead to a spurious loop; see
1759 -- the examples in [SUPERCLASS-LOOP]
1760 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1762 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1764 NoInstance -> -- No such instance!
1765 -- Add it and its superclasses
1766 addIrred want_scs avails wanted
1769 try_simple do_this_otherwise
1770 = lookupInst wanted `thenM` \ lookup_result ->
1771 case lookup_result of
1772 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1773 other -> do_this_otherwise avails wanted
1778 -------------------------
1779 isAvailable :: Avails -> Inst -> Maybe Avail
1780 isAvailable avails wanted = lookupFM avails wanted
1781 -- NB 1: the Ord instance of Inst compares by the class/type info
1782 -- *not* by unique. So
1783 -- d1::C Int == d2::C Int
1785 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1786 addLinearAvailable avails avail wanted
1787 -- avails currently maps [wanted -> avail]
1788 -- Extend avails to reflect a neeed for an extra copy of avail
1790 | Just avail' <- split_avail avail
1791 = returnM (addToFM avails wanted avail', [])
1794 = tcLookupId splitName `thenM` \ split_id ->
1795 tcInstClassOp (instLoc wanted) split_id
1796 [linearInstType wanted] `thenM` \ split_inst ->
1797 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1800 split_avail :: Avail -> Maybe Avail
1801 -- (Just av) if there's a modified version of avail that
1802 -- we can use to replace avail in avails
1803 -- Nothing if there isn't, so we need to create a Linear
1804 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1805 split_avail (Given id used) | not used = Just (Given id True)
1806 | otherwise = Nothing
1807 split_avail Irred = Nothing
1808 split_avail IsFree = Nothing
1809 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1811 -------------------------
1812 addFree :: Avails -> Inst -> TcM Avails
1813 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1814 -- to avails, so that any other equal Insts will be commoned up right
1815 -- here rather than also being tossed upstairs. This is really just
1816 -- an optimisation, and perhaps it is more trouble that it is worth,
1817 -- as the following comments show!
1819 -- NB: do *not* add superclasses. If we have
1822 -- but a is not bound here, then we *don't* want to derive
1823 -- dn from df here lest we lose sharing.
1825 addFree avails free = returnM (addToFM avails free IsFree)
1827 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1828 addWanted want_scs avails wanted rhs_expr wanteds
1829 = addAvailAndSCs want_scs avails wanted avail
1831 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1832 | otherwise = ASSERT( null wanteds ) NoRhs
1834 addGiven :: Avails -> Inst -> TcM Avails
1835 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1836 -- Always add superclasses for 'givens'
1838 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1839 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1840 -- so the assert isn't true
1842 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1843 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1844 addAvailAndSCs want_scs avails irred Irred
1846 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1847 addAvailAndSCs want_scs avails inst avail
1848 | not (isClassDict inst) = return avails_with_inst
1849 | NoSCs <- want_scs = return avails_with_inst
1850 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1851 ; addSCs is_loop avails_with_inst inst }
1853 avails_with_inst = addToFM avails inst avail
1855 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1856 -- Note: this compares by *type*, not by Unique
1857 deps = findAllDeps (unitVarSet (instToId inst)) avail
1858 dep_tys = map idType (varSetElems deps)
1860 findAllDeps :: IdSet -> Avail -> IdSet
1861 -- Find all the Insts that this one depends on
1862 -- See Note [SUPERCLASS-LOOP 2]
1863 -- Watch out, though. Since the avails may contain loops
1864 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1865 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1866 findAllDeps so_far other = so_far
1868 find_all :: IdSet -> Inst -> IdSet
1870 | kid_id `elemVarSet` so_far = so_far
1871 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1872 | otherwise = so_far'
1874 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1875 kid_id = instToId kid
1877 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1878 -- Add all the superclasses of the Inst to Avails
1879 -- The first param says "dont do this because the original thing
1880 -- depends on this one, so you'd build a loop"
1881 -- Invariant: the Inst is already in Avails.
1883 addSCs is_loop avails dict
1884 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1885 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1887 (clas, tys) = getDictClassTys dict
1888 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1889 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1891 add_sc avails (sc_dict, sc_sel)
1892 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1893 | is_given sc_dict = return avails
1894 | otherwise = addSCs is_loop avails' sc_dict
1896 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1897 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1899 is_given :: Inst -> Bool
1900 is_given sc_dict = case lookupFM avails sc_dict of
1901 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1905 Note [SUPERCLASS-LOOP 2]
1906 ~~~~~~~~~~~~~~~~~~~~~~~~
1907 But the above isn't enough. Suppose we are *given* d1:Ord a,
1908 and want to deduce (d2:C [a]) where
1910 class Ord a => C a where
1911 instance Ord [a] => C [a] where ...
1913 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1914 superclasses of C [a] to avails. But we must not overwrite the binding
1915 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1918 Here's another variant, immortalised in tcrun020
1919 class Monad m => C1 m
1920 class C1 m => C2 m x
1921 instance C2 Maybe Bool
1922 For the instance decl we need to build (C1 Maybe), and it's no good if
1923 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1924 before we search for C1 Maybe.
1926 Here's another example
1927 class Eq b => Foo a b
1928 instance Eq a => Foo [a] a
1932 we'll first deduce that it holds (via the instance decl). We must not
1933 then overwrite the Eq t constraint with a superclass selection!
1935 At first I had a gross hack, whereby I simply did not add superclass constraints
1936 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1937 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1938 I found a very obscure program (now tcrun021) in which improvement meant the
1939 simplifier got two bites a the cherry... so something seemed to be an Irred
1940 first time, but reducible next time.
1942 Now we implement the Right Solution, which is to check for loops directly
1943 when adding superclasses. It's a bit like the occurs check in unification.
1946 Note [RECURSIVE DICTIONARIES]
1947 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1949 data D r = ZeroD | SuccD (r (D r));
1951 instance (Eq (r (D r))) => Eq (D r) where
1952 ZeroD == ZeroD = True
1953 (SuccD a) == (SuccD b) = a == b
1956 equalDC :: D [] -> D [] -> Bool;
1959 We need to prove (Eq (D [])). Here's how we go:
1963 by instance decl, holds if
1967 by instance decl of Eq, holds if
1969 where d2 = dfEqList d3
1972 But now we can "tie the knot" to give
1978 and it'll even run! The trick is to put the thing we are trying to prove
1979 (in this case Eq (D []) into the database before trying to prove its
1980 contributing clauses.
1983 %************************************************************************
1985 \section{tcSimplifyTop: defaulting}
1987 %************************************************************************
1990 @tcSimplifyTop@ is called once per module to simplify all the constant
1991 and ambiguous Insts.
1993 We need to be careful of one case. Suppose we have
1995 instance Num a => Num (Foo a b) where ...
1997 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1998 to (Num x), and default x to Int. But what about y??
2000 It's OK: the final zonking stage should zap y to (), which is fine.
2004 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2005 tcSimplifyTop wanteds
2006 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2008 doc = text "tcSimplifyTop"
2010 tcSimplifyInteractive wanteds
2011 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2013 doc = text "tcSimplifyTop"
2015 -- The TcLclEnv should be valid here, solely to improve
2016 -- error message generation for the monomorphism restriction
2017 tc_simplify_top doc is_interactive want_scs wanteds
2018 = do { lcl_env <- getLclEnv
2019 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2021 ; let try_me inst = ReduceMe want_scs
2022 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2025 -- All the non-tv ones are definite errors
2026 (tv_dicts, non_tvs) = partition isTyVarDict irreds
2027 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2029 -- Group by type variable
2030 tv_groups = equivClasses cmp_by_tyvar tv_dicts
2032 -- Pick the ones which its worth trying to disambiguate
2033 -- namely, the ones whose type variable isn't bound
2034 -- up with one of the non-tyvar classes
2035 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2036 defaultable_group ds@(d:_)
2037 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst d)
2038 && defaultable_classes (map get_clas ds)
2039 defaultable_classes clss
2040 | is_interactive = any isInteractiveClass clss
2041 | otherwise = all isStandardClass clss && any isNumericClass clss
2043 isInteractiveClass cls = isNumericClass cls
2044 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2045 -- In interactive mode, we default Show a to Show ()
2046 -- to avoid graututious errors on "show []"
2049 -- Collect together all the bad guys
2050 bad_guys = non_tvs ++ concat non_default_gps
2051 (non_ips, bad_ips) = partition isClassDict bad_guys
2052 (ambigs, no_insts) = partition isTyVarDict non_ips
2053 -- If the dict has no type constructors involved, it must be ambiguous,
2054 -- except I suppose that another error with fundeps maybe should have
2055 -- constrained those type variables
2057 -- Report definite errors
2058 ; ASSERT( null frees )
2059 groupErrs (addNoInstanceErrs Nothing []) no_insts
2060 ; strangeTopIPErrs bad_ips
2062 -- Deal with ambiguity errors, but only if
2063 -- if there has not been an error so far:
2064 -- errors often give rise to spurious ambiguous Insts.
2066 -- f = (*) -- Monomorphic
2067 -- g :: Num a => a -> a
2069 -- Here, we get a complaint when checking the type signature for g,
2070 -- that g isn't polymorphic enough; but then we get another one when
2071 -- dealing with the (Num a) context arising from f's definition;
2072 -- we try to unify a with Int (to default it), but find that it's
2073 -- already been unified with the rigid variable from g's type sig
2074 ; binds_ambig <- ifErrsM (returnM []) $
2075 do { -- Complain about the ones that don't fall under
2076 -- the Haskell rules for disambiguation
2077 -- This group includes both non-existent instances
2078 -- e.g. Num (IO a) and Eq (Int -> Int)
2079 -- and ambiguous dictionaries
2081 addTopAmbigErrs ambigs
2083 -- Disambiguate the ones that look feasible
2084 ; mappM (disambigGroup is_interactive) default_gps }
2086 ; return (binds `unionBags` unionManyBags binds_ambig) }
2088 ----------------------------------
2089 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2091 get_tv d = case getDictClassTys d of
2092 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2093 get_clas d = case getDictClassTys d of
2094 (clas, [ty]) -> clas
2097 If a dictionary constrains a type variable which is
2098 * not mentioned in the environment
2099 * and not mentioned in the type of the expression
2100 then it is ambiguous. No further information will arise to instantiate
2101 the type variable; nor will it be generalised and turned into an extra
2102 parameter to a function.
2104 It is an error for this to occur, except that Haskell provided for
2105 certain rules to be applied in the special case of numeric types.
2107 * at least one of its classes is a numeric class, and
2108 * all of its classes are numeric or standard
2109 then the type variable can be defaulted to the first type in the
2110 default-type list which is an instance of all the offending classes.
2112 So here is the function which does the work. It takes the ambiguous
2113 dictionaries and either resolves them (producing bindings) or
2114 complains. It works by splitting the dictionary list by type
2115 variable, and using @disambigOne@ to do the real business.
2117 @disambigOne@ assumes that its arguments dictionaries constrain all
2118 the same type variable.
2120 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2121 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2122 the most common use of defaulting is code like:
2124 _ccall_ foo `seqPrimIO` bar
2126 Since we're not using the result of @foo@, the result if (presumably)
2130 disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
2131 -> [Inst] -- All standard classes of form (C a)
2134 disambigGroup is_interactive dicts
2135 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2136 -- SO, TRY DEFAULT TYPES IN ORDER
2138 -- Failure here is caused by there being no type in the
2139 -- default list which can satisfy all the ambiguous classes.
2140 -- For example, if Real a is reqd, but the only type in the
2141 -- default list is Int.
2142 get_default_tys `thenM` \ default_tys ->
2144 try_default [] -- No defaults work, so fail
2147 try_default (default_ty : default_tys)
2148 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2149 -- default_tys instead
2150 tcSimplifyDefault theta `thenM` \ _ ->
2153 theta = [mkClassPred clas [default_ty] | clas <- classes]
2155 -- See if any default works
2156 tryM (try_default default_tys) `thenM` \ mb_ty ->
2159 Right chosen_default_ty -> choose_default chosen_default_ty
2161 tyvar = get_tv (head dicts) -- Should be non-empty
2162 classes = map get_clas dicts
2164 choose_default default_ty -- Commit to tyvar = default_ty
2165 = -- Bind the type variable
2166 unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
2167 -- and reduce the context, for real this time
2168 simpleReduceLoop (text "disambig" <+> ppr dicts)
2169 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2170 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2171 warnDefault dicts default_ty `thenM_`
2174 bomb_out = addTopAmbigErrs dicts `thenM_`
2178 = do { mb_defaults <- getDefaultTys
2179 ; case mb_defaults of
2180 Just tys -> return tys
2181 Nothing -> -- No use-supplied default;
2182 -- use [Integer, Double]
2183 do { integer_ty <- tcMetaTy integerTyConName
2184 ; checkWiredInTyCon doubleTyCon
2185 ; return [integer_ty, doubleTy] } }
2188 [Aside - why the defaulting mechanism is turned off when
2189 dealing with arguments and results to ccalls.
2191 When typechecking _ccall_s, TcExpr ensures that the external
2192 function is only passed arguments (and in the other direction,
2193 results) of a restricted set of 'native' types. This is
2194 implemented via the help of the pseudo-type classes,
2195 @CReturnable@ (CR) and @CCallable@ (CC.)
2197 The interaction between the defaulting mechanism for numeric
2198 values and CC & CR can be a bit puzzling to the user at times.
2207 What type has 'x' got here? That depends on the default list
2208 in operation, if it is equal to Haskell 98's default-default
2209 of (Integer, Double), 'x' has type Double, since Integer
2210 is not an instance of CR. If the default list is equal to
2211 Haskell 1.4's default-default of (Int, Double), 'x' has type
2214 To try to minimise the potential for surprises here, the
2215 defaulting mechanism is turned off in the presence of
2216 CCallable and CReturnable.
2221 %************************************************************************
2223 \subsection[simple]{@Simple@ versions}
2225 %************************************************************************
2227 Much simpler versions when there are no bindings to make!
2229 @tcSimplifyThetas@ simplifies class-type constraints formed by
2230 @deriving@ declarations and when specialising instances. We are
2231 only interested in the simplified bunch of class/type constraints.
2233 It simplifies to constraints of the form (C a b c) where
2234 a,b,c are type variables. This is required for the context of
2235 instance declarations.
2238 tcSimplifyDeriv :: [TyVar]
2239 -> ThetaType -- Wanted
2240 -> TcM ThetaType -- Needed
2242 tcSimplifyDeriv tyvars theta
2243 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2244 -- The main loop may do unification, and that may crash if
2245 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2246 -- ToDo: what if two of them do get unified?
2247 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2248 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2249 ASSERT( null frees ) -- reduceMe never returns Free
2251 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2253 tv_set = mkVarSet tvs
2255 (bad_insts, ok_insts) = partition is_bad_inst irreds
2257 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2258 in isEmptyVarSet (tyVarsOfPred pred)
2259 -- Things like (Eq T) are bad
2260 || (not undecidable_ok && not (isTyVarClassPred pred))
2261 -- The returned dictionaries should be of form (C a b)
2262 -- (where a, b are type variables).
2263 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
2264 -- but note that risks non-termination in the 'deriving' context-inference
2265 -- fixpoint loop. It is useful for situations like
2266 -- data Min h a = E | M a (h a)
2267 -- which gives the instance decl
2268 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
2270 simpl_theta = map dictPred ok_insts
2271 weird_preds = [pred | pred <- simpl_theta
2272 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2273 -- Check for a bizarre corner case, when the derived instance decl should
2274 -- have form instance C a b => D (T a) where ...
2275 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2276 -- of problems; in particular, it's hard to compare solutions for
2277 -- equality when finding the fixpoint. So I just rule it out for now.
2279 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2280 -- This reverse-mapping is a Royal Pain,
2281 -- but the result should mention TyVars not TcTyVars
2284 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2285 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2286 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2287 returnM (substTheta rev_env simpl_theta)
2289 doc = ptext SLIT("deriving classes for a data type")
2292 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2293 used with \tr{default} declarations. We are only interested in
2294 whether it worked or not.
2297 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2300 tcSimplifyDefault theta
2301 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2302 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2303 ASSERT( null frees ) -- try_me never returns Free
2304 addNoInstanceErrs Nothing [] irreds `thenM_`
2310 doc = ptext SLIT("default declaration")
2314 %************************************************************************
2316 \section{Errors and contexts}
2318 %************************************************************************
2320 ToDo: for these error messages, should we note the location as coming
2321 from the insts, or just whatever seems to be around in the monad just
2325 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2326 -> [Inst] -- The offending Insts
2328 -- Group together insts with the same origin
2329 -- We want to report them together in error messages
2331 groupErrs report_err []
2333 groupErrs report_err (inst:insts)
2334 = do_one (inst:friends) `thenM_`
2335 groupErrs report_err others
2338 -- (It may seem a bit crude to compare the error messages,
2339 -- but it makes sure that we combine just what the user sees,
2340 -- and it avoids need equality on InstLocs.)
2341 (friends, others) = partition is_friend insts
2342 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2343 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2344 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2345 -- Add location and context information derived from the Insts
2347 -- Add the "arising from..." part to a message about bunch of dicts
2348 addInstLoc :: [Inst] -> Message -> Message
2349 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2352 plural xs = char 's'
2354 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2355 addTopIPErrs bndrs []
2357 addTopIPErrs bndrs ips
2358 = addErrTcM (tidy_env, mk_msg tidy_ips)
2360 (tidy_env, tidy_ips) = tidyInsts ips
2361 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
2362 pprBinders bndrs <> colon],
2363 nest 2 (vcat (map ppr_ip ips)),
2365 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2367 strangeTopIPErrs :: [Inst] -> TcM ()
2368 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2369 = groupErrs report tidy_dicts
2371 (tidy_env, tidy_dicts) = tidyInsts dicts
2372 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2373 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2374 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2376 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2377 -- Just d => d describes the construct
2378 -> [Inst] -- What is given by the context or type sig
2379 -> [Inst] -- What is wanted
2381 addNoInstanceErrs mb_what givens []
2383 addNoInstanceErrs mb_what givens dicts
2384 = -- Some of the dicts are here because there is no instances
2385 -- and some because there are too many instances (overlap)
2386 tcGetInstEnvs `thenM` \ inst_envs ->
2388 (tidy_env1, tidy_givens) = tidyInsts givens
2389 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2391 -- Run through the dicts, generating a message for each
2392 -- overlapping one, but simply accumulating all the
2393 -- no-instance ones so they can be reported as a group
2394 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2395 check_overlap (overlap_doc, no_inst_dicts) dict
2396 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2398 = case lookupInstEnv inst_envs clas tys of
2399 -- The case of exactly one match and no unifiers means
2400 -- a successful lookup. That can't happen here, becuase
2401 -- dicts only end up here if they didn't match in Inst.lookupInst
2403 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2405 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2406 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2408 (clas,tys) = getDictClassTys dict
2411 -- Now generate a good message for the no-instance bunch
2412 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2414 no_inst_doc | null no_inst_dicts = empty
2415 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2416 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2417 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2418 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2419 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2421 -- And emit both the non-instance and overlap messages
2422 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2424 mk_overlap_msg dict (matches, unifiers)
2425 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2426 <+> pprPred (dictPred dict))),
2427 sep [ptext SLIT("Matching instances") <> colon,
2428 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2429 ASSERT( not (null matches) )
2430 if not (isSingleton matches)
2431 then -- Two or more matches
2433 else -- One match, plus some unifiers
2434 ASSERT( not (null unifiers) )
2435 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2436 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2437 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2439 ispecs = [ispec | (_, ispec) <- matches]
2441 mk_probable_fix tidy_env dicts
2442 = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
2444 fixes = add_ors (fix1 ++ fix2)
2446 fix1 = case mb_what of
2447 Nothing -> [] -- Top level
2448 Just what -> -- Nested (type signatures, instance decls)
2449 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2450 ptext SLIT("to the") <+> what] ]
2452 fix2 | null instance_dicts = []
2453 | otherwise = [ ptext SLIT("add an instance declaration for")
2454 <+> pprDictsTheta instance_dicts ]
2455 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2456 -- Insts for which it is worth suggesting an adding an instance declaration
2457 -- Exclude implicit parameters, and tyvar dicts
2459 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2460 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2461 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2463 addTopAmbigErrs dicts
2464 -- Divide into groups that share a common set of ambiguous tyvars
2465 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2467 (tidy_env, tidy_dicts) = tidyInsts dicts
2469 tvs_of :: Inst -> [TcTyVar]
2470 tvs_of d = varSetElems (tyVarsOfInst d)
2471 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2473 report :: [(Inst,[TcTyVar])] -> TcM ()
2474 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2475 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2476 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2477 -- the location of the first one will do for the err message
2478 addErrTcM (tidy_env, msg $$ mono_msg)
2480 dicts = map fst pairs
2481 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2482 pprQuotedList tvs <+> in_msg,
2483 nest 2 (pprDictsInFull dicts)]
2484 in_msg = text "in the constraint" <> plural dicts <> colon
2487 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2488 -- There's an error with these Insts; if they have free type variables
2489 -- it's probably caused by the monomorphism restriction.
2490 -- Try to identify the offending variable
2491 -- ASSUMPTION: the Insts are fully zonked
2492 mkMonomorphismMsg tidy_env inst_tvs
2493 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2494 returnM (tidy_env, mk_msg docs)
2496 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2497 -- This happens in things like
2498 -- f x = show (read "foo")
2499 -- whre monomorphism doesn't play any role
2500 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2504 monomorphism_fix :: SDoc
2505 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2506 (ptext SLIT("give these definition(s) an explicit type signature")
2507 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2509 warnDefault dicts default_ty
2510 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2511 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2514 (_, tidy_dicts) = tidyInsts dicts
2515 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2516 quotes (ppr default_ty),
2517 pprDictsInFull tidy_dicts]
2519 -- Used for the ...Thetas variants; all top level
2521 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2522 ptext SLIT("type variables that are not data type parameters"),
2523 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2525 reduceDepthErr n stack
2526 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2527 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2528 nest 4 (pprStack stack)]
2530 pprStack stack = vcat (map pprInstInFull stack)