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 ( 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,
35 newDictsAtLoc, tcInstClassOp,
36 getDictClassTys, isTyVarDict, instLoc,
37 zonkInst, tidyInsts, tidyMoreInsts,
38 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, tcIsTyVarTy )
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 | Rhs -- Used when there is a RHS
1354 (LHsExpr TcId) -- The RHS
1355 [Inst] -- Insts free in the RHS; we need these too
1357 | Linear -- Splittable Insts only.
1358 Int -- The Int is always 2 or more; indicates how
1359 -- many copies are required
1360 Inst -- The splitter
1361 Avail -- Where the "master copy" is
1363 | LinRhss -- Splittable Insts only; this is used only internally
1364 -- by extractResults, where a Linear
1365 -- is turned into an LinRhss
1366 [LHsExpr TcId] -- A supply of suitable RHSs
1368 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1369 | (inst,avail) <- fmToList avails ]
1371 instance Outputable Avail where
1374 pprAvail IsFree = text "Free"
1375 pprAvail Irred = text "Irred"
1376 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1377 if b then text "(used)" else empty
1378 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1379 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1380 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1383 Extracting the bindings from a bunch of Avails.
1384 The bindings do *not* come back sorted in dependency order.
1385 We assume that they'll be wrapped in a big Rec, so that the
1386 dependency analyser can sort them out later
1390 extractResults :: Avails
1392 -> TcM (TcDictBinds, -- Bindings
1393 [Inst], -- Irreducible ones
1394 [Inst]) -- Free ones
1396 extractResults avails wanteds
1397 = go avails emptyBag [] [] wanteds
1399 go avails binds irreds frees []
1400 = returnM (binds, irreds, frees)
1402 go avails binds irreds frees (w:ws)
1403 = case lookupFM avails w of
1404 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1405 go avails binds irreds frees ws
1407 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1408 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1410 Just (Given id _) -> go avails new_binds irreds frees ws
1412 new_binds | id == instToId w = binds
1413 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1414 -- The sought Id can be one of the givens, via a superclass chain
1415 -- and then we definitely don't want to generate an x=x binding!
1417 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1419 new_binds = addBind binds w rhs
1421 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1422 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1423 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1424 go (addToFM avails w (LinRhss rhss))
1425 (binds `unionBags` binds')
1426 irreds' frees' (split_inst : w : ws)
1428 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1429 -> go new_avails new_binds irreds frees ws
1431 new_binds = addBind binds w rhs
1432 new_avails = addToFM avails w (LinRhss rhss)
1434 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1435 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1436 returnM (w':irreds, frees, instToId w')
1437 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1438 returnM (irreds, w':frees, instToId w')
1440 add_given avails w = addToFM avails w (Given (instToId w) True)
1442 add_free avails w | isMethod w = avails
1443 | otherwise = add_given avails w
1445 -- Do *not* replace Free by Given if it's a method.
1446 -- The following situation shows why this is bad:
1447 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1448 -- From an application (truncate f i) we get
1449 -- t1 = truncate at f
1451 -- If we have also have a second occurrence of truncate, we get
1452 -- t3 = truncate at f
1454 -- When simplifying with i,f free, we might still notice that
1455 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1456 -- will continue to float out!
1457 -- (split n i a) returns: n rhss
1458 -- auxiliary bindings
1459 -- 1 or 0 insts to add to irreds
1462 split :: Int -> TcId -> TcId -> Inst
1463 -> TcM (TcDictBinds, [LHsExpr TcId])
1464 -- (split n split_id root_id wanted) returns
1465 -- * a list of 'n' expressions, all of which witness 'avail'
1466 -- * a bunch of auxiliary bindings to support these expressions
1467 -- * one or zero insts needed to witness the whole lot
1468 -- (maybe be zero if the initial Inst is a Given)
1470 -- NB: 'wanted' is just a template
1472 split n split_id root_id wanted
1475 ty = linearInstType wanted
1476 pair_ty = mkTyConApp pairTyCon [ty,ty]
1477 id = instToId wanted
1480 span = instSpan wanted
1482 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1484 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1485 expand n rhss `thenM` \ (binds2, rhss') ->
1486 returnM (binds1 `unionBags` binds2, rhss')
1489 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1490 -- e.g. expand 3 [rhs1, rhs2]
1491 -- = ( { x = split rhs1 },
1492 -- [fst x, snd x, rhs2] )
1494 | n `rem` 2 == 0 = go rhss -- n is even
1495 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1496 returnM (binds', head rhss : rhss')
1498 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1499 returnM (listToBag binds', concat rhss')
1501 do_one rhs = newUnique `thenM` \ uniq ->
1502 tcLookupId fstName `thenM` \ fst_id ->
1503 tcLookupId sndName `thenM` \ snd_id ->
1505 x = mkUserLocal occ uniq pair_ty loc
1507 returnM (L span (VarBind x (mk_app span split_id rhs)),
1508 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1510 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1512 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1514 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1515 (VarBind (instToId inst) rhs))
1516 instSpan wanted = instLocSrcSpan (instLoc wanted)
1520 %************************************************************************
1522 \subsection[reduce]{@reduce@}
1524 %************************************************************************
1526 When the "what to do" predicate doesn't depend on the quantified type variables,
1527 matters are easier. We don't need to do any zonking, unless the improvement step
1528 does something, in which case we zonk before iterating.
1530 The "given" set is always empty.
1533 simpleReduceLoop :: SDoc
1534 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1536 -> TcM ([Inst], -- Free
1538 [Inst]) -- Irreducible
1540 simpleReduceLoop doc try_me wanteds
1541 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1542 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1543 if no_improvement then
1544 returnM (frees, binds, irreds)
1546 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1547 returnM (frees1, binds `unionBags` binds1, irreds1)
1553 reduceContext :: SDoc
1554 -> (Inst -> WhatToDo)
1557 -> TcM (Bool, -- True <=> improve step did no unification
1559 TcDictBinds, -- Dictionary bindings
1560 [Inst]) -- Irreducible
1562 reduceContext doc try_me givens wanteds
1564 traceTc (text "reduceContext" <+> (vcat [
1565 text "----------------------",
1567 text "given" <+> ppr givens,
1568 text "wanted" <+> ppr wanteds,
1569 text "----------------------"
1572 -- Build the Avail mapping from "givens"
1573 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1576 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1578 -- Do improvement, using everything in avails
1579 -- In particular, avails includes all superclasses of everything
1580 tcImprove avails `thenM` \ no_improvement ->
1582 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1584 traceTc (text "reduceContext end" <+> (vcat [
1585 text "----------------------",
1587 text "given" <+> ppr givens,
1588 text "wanted" <+> ppr wanteds,
1590 text "avails" <+> pprAvails avails,
1591 text "frees" <+> ppr frees,
1592 text "no_improvement =" <+> ppr no_improvement,
1593 text "----------------------"
1596 returnM (no_improvement, frees, binds, irreds)
1598 -- reduceContextWithoutImprovement differs from reduceContext
1599 -- (a) no improvement
1600 -- (b) 'givens' is assumed empty
1601 reduceContextWithoutImprovement doc try_me wanteds
1603 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1604 text "----------------------",
1606 text "wanted" <+> ppr wanteds,
1607 text "----------------------"
1611 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1612 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1614 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1615 text "----------------------",
1617 text "wanted" <+> ppr wanteds,
1619 text "avails" <+> pprAvails avails,
1620 text "frees" <+> ppr frees,
1621 text "----------------------"
1624 returnM (frees, binds, irreds)
1626 tcImprove :: Avails -> TcM Bool -- False <=> no change
1627 -- Perform improvement using all the predicates in Avails
1629 = tcGetInstEnvs `thenM` \ inst_envs ->
1631 preds = [ (pred, pp_loc)
1632 | (inst, avail) <- fmToList avails,
1633 pred <- get_preds inst avail,
1634 let pp_loc = pprInstLoc (instLoc inst)
1636 -- Avails has all the superclasses etc (good)
1637 -- It also has all the intermediates of the deduction (good)
1638 -- It does not have duplicates (good)
1639 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1640 -- so that improve will see them separate
1642 -- For free Methods, we want to take predicates from their context,
1643 -- but for Methods that have been squished their context will already
1644 -- be in Avails, and we don't want duplicates. Hence this rather
1645 -- horrid get_preds function
1646 get_preds inst IsFree = fdPredsOfInst inst
1647 get_preds inst other | isDict inst = [dictPred inst]
1650 eqns = improve get_insts preds
1651 get_insts clas = classInstances inst_envs clas
1656 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1657 mappM_ unify eqns `thenM_`
1660 unify ((qtvs, pairs), doc)
1662 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1663 mapM_ (unif_pr tenv) pairs
1664 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1667 The main context-reduction function is @reduce@. Here's its game plan.
1670 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1671 -- along with its depth
1672 -> (Inst -> WhatToDo)
1679 try_me: given an inst, this function returns
1681 DontReduce return this in "irreds"
1682 Free return this in "frees"
1684 wanteds: The list of insts to reduce
1685 state: An accumulating parameter of type Avails
1686 that contains the state of the algorithm
1688 It returns a Avails.
1690 The (n,stack) pair is just used for error reporting.
1691 n is always the depth of the stack.
1692 The stack is the stack of Insts being reduced: to produce X
1693 I had to produce Y, to produce Y I had to produce Z, and so on.
1696 reduceList (n,stack) try_me wanteds state
1697 | n > opt_MaxContextReductionDepth
1698 = failWithTc (reduceDepthErr n stack)
1704 pprTrace "Interesting! Context reduction stack deeper than 8:"
1705 (int n $$ ifPprDebug (nest 2 (pprStack stack)))
1710 go [] state = returnM state
1711 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1714 -- Base case: we're done!
1715 reduce stack try_me wanted avails
1716 -- It's the same as an existing inst, or a superclass thereof
1717 | Just avail <- isAvailable avails wanted
1718 = if isLinearInst wanted then
1719 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1720 reduceList stack try_me wanteds' avails'
1722 returnM avails -- No op for non-linear things
1725 = case try_me wanted of {
1727 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1729 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1730 -- First, see if the inst can be reduced to a constant in one step
1731 try_simple (addIrred AddSCs) -- Assume want superclasses
1733 ; Free -> -- It's free so just chuck it upstairs
1734 -- First, see if the inst can be reduced to a constant in one step
1737 ; ReduceMe want_scs -> -- It should be reduced
1738 lookupInst wanted `thenM` \ lookup_result ->
1739 case lookup_result of
1740 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1741 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1742 addWanted want_scs avails2 wanted rhs wanteds'
1743 -- Experiment with temporarily doing addIrred *before* the reduceList,
1744 -- which has the effect of adding the thing we are trying
1745 -- to prove to the database before trying to prove the things it
1746 -- needs. See note [RECURSIVE DICTIONARIES]
1747 -- NB: we must not do an addWanted before, because that adds the
1748 -- superclasses too, and thaat can lead to a spurious loop; see
1749 -- the examples in [SUPERCLASS-LOOP]
1750 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1752 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1754 NoInstance -> -- No such instance!
1755 -- Add it and its superclasses
1756 addIrred want_scs avails wanted
1759 try_simple do_this_otherwise
1760 = lookupInst wanted `thenM` \ lookup_result ->
1761 case lookup_result of
1762 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1763 other -> do_this_otherwise avails wanted
1768 -------------------------
1769 isAvailable :: Avails -> Inst -> Maybe Avail
1770 isAvailable avails wanted = lookupFM avails wanted
1771 -- NB 1: the Ord instance of Inst compares by the class/type info
1772 -- *not* by unique. So
1773 -- d1::C Int == d2::C Int
1775 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1776 addLinearAvailable avails avail wanted
1777 -- avails currently maps [wanted -> avail]
1778 -- Extend avails to reflect a neeed for an extra copy of avail
1780 | Just avail' <- split_avail avail
1781 = returnM (addToFM avails wanted avail', [])
1784 = tcLookupId splitName `thenM` \ split_id ->
1785 tcInstClassOp (instLoc wanted) split_id
1786 [linearInstType wanted] `thenM` \ split_inst ->
1787 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1790 split_avail :: Avail -> Maybe Avail
1791 -- (Just av) if there's a modified version of avail that
1792 -- we can use to replace avail in avails
1793 -- Nothing if there isn't, so we need to create a Linear
1794 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1795 split_avail (Given id used) | not used = Just (Given id True)
1796 | otherwise = Nothing
1797 split_avail Irred = Nothing
1798 split_avail IsFree = Nothing
1799 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1801 -------------------------
1802 addFree :: Avails -> Inst -> TcM Avails
1803 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1804 -- to avails, so that any other equal Insts will be commoned up right
1805 -- here rather than also being tossed upstairs. This is really just
1806 -- an optimisation, and perhaps it is more trouble that it is worth,
1807 -- as the following comments show!
1809 -- NB: do *not* add superclasses. If we have
1812 -- but a is not bound here, then we *don't* want to derive
1813 -- dn from df here lest we lose sharing.
1815 addFree avails free = returnM (addToFM avails free IsFree)
1817 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1818 addWanted want_scs avails wanted rhs_expr wanteds
1819 = addAvailAndSCs want_scs avails wanted avail
1821 avail = Rhs rhs_expr wanteds
1823 addGiven :: Avails -> Inst -> TcM Avails
1824 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1825 -- Always add superclasses for 'givens'
1827 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1828 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1829 -- so the assert isn't true
1831 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1832 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1833 addAvailAndSCs want_scs avails irred Irred
1835 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1836 addAvailAndSCs want_scs avails inst avail
1837 | not (isClassDict inst) = return avails_with_inst
1838 | NoSCs <- want_scs = return avails_with_inst
1839 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1840 ; addSCs is_loop avails_with_inst inst }
1842 avails_with_inst = addToFM avails inst avail
1844 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1845 -- Note: this compares by *type*, not by Unique
1846 deps = findAllDeps (unitVarSet (instToId inst)) avail
1847 dep_tys = map idType (varSetElems deps)
1849 findAllDeps :: IdSet -> Avail -> IdSet
1850 -- Find all the Insts that this one depends on
1851 -- See Note [SUPERCLASS-LOOP 2]
1852 -- Watch out, though. Since the avails may contain loops
1853 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1854 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1855 findAllDeps so_far other = so_far
1857 find_all :: IdSet -> Inst -> IdSet
1859 | kid_id `elemVarSet` so_far = so_far
1860 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1861 | otherwise = so_far'
1863 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1864 kid_id = instToId kid
1866 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1867 -- Add all the superclasses of the Inst to Avails
1868 -- The first param says "dont do this because the original thing
1869 -- depends on this one, so you'd build a loop"
1870 -- Invariant: the Inst is already in Avails.
1872 addSCs is_loop avails dict
1873 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1874 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1876 (clas, tys) = getDictClassTys dict
1877 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1878 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1880 add_sc avails (sc_dict, sc_sel)
1881 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1882 | is_given sc_dict = return avails
1883 | otherwise = addSCs is_loop avails' sc_dict
1885 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1886 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1888 is_given :: Inst -> Bool
1889 is_given sc_dict = case lookupFM avails sc_dict of
1890 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1894 Note [SUPERCLASS-LOOP 2]
1895 ~~~~~~~~~~~~~~~~~~~~~~~~
1896 But the above isn't enough. Suppose we are *given* d1:Ord a,
1897 and want to deduce (d2:C [a]) where
1899 class Ord a => C a where
1900 instance Ord [a] => C [a] where ...
1902 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1903 superclasses of C [a] to avails. But we must not overwrite the binding
1904 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1907 Here's another variant, immortalised in tcrun020
1908 class Monad m => C1 m
1909 class C1 m => C2 m x
1910 instance C2 Maybe Bool
1911 For the instance decl we need to build (C1 Maybe), and it's no good if
1912 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1913 before we search for C1 Maybe.
1915 Here's another example
1916 class Eq b => Foo a b
1917 instance Eq a => Foo [a] a
1921 we'll first deduce that it holds (via the instance decl). We must not
1922 then overwrite the Eq t constraint with a superclass selection!
1924 At first I had a gross hack, whereby I simply did not add superclass constraints
1925 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1926 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1927 I found a very obscure program (now tcrun021) in which improvement meant the
1928 simplifier got two bites a the cherry... so something seemed to be an Irred
1929 first time, but reducible next time.
1931 Now we implement the Right Solution, which is to check for loops directly
1932 when adding superclasses. It's a bit like the occurs check in unification.
1935 Note [RECURSIVE DICTIONARIES]
1936 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1938 data D r = ZeroD | SuccD (r (D r));
1940 instance (Eq (r (D r))) => Eq (D r) where
1941 ZeroD == ZeroD = True
1942 (SuccD a) == (SuccD b) = a == b
1945 equalDC :: D [] -> D [] -> Bool;
1948 We need to prove (Eq (D [])). Here's how we go:
1952 by instance decl, holds if
1956 by instance decl of Eq, holds if
1958 where d2 = dfEqList d3
1961 But now we can "tie the knot" to give
1967 and it'll even run! The trick is to put the thing we are trying to prove
1968 (in this case Eq (D []) into the database before trying to prove its
1969 contributing clauses.
1972 %************************************************************************
1974 \section{tcSimplifyTop: defaulting}
1976 %************************************************************************
1979 @tcSimplifyTop@ is called once per module to simplify all the constant
1980 and ambiguous Insts.
1982 We need to be careful of one case. Suppose we have
1984 instance Num a => Num (Foo a b) where ...
1986 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1987 to (Num x), and default x to Int. But what about y??
1989 It's OK: the final zonking stage should zap y to (), which is fine.
1993 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
1994 tcSimplifyTop wanteds
1995 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
1997 doc = text "tcSimplifyTop"
1999 tcSimplifyInteractive wanteds
2000 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2002 doc = text "tcSimplifyTop"
2004 -- The TcLclEnv should be valid here, solely to improve
2005 -- error message generation for the monomorphism restriction
2006 tc_simplify_top doc is_interactive want_scs wanteds
2007 = do { lcl_env <- getLclEnv
2008 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2010 ; let try_me inst = ReduceMe want_scs
2011 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2014 -- First get rid of implicit parameters
2015 (non_ips, bad_ips) = partition isClassDict irreds
2017 -- All the non-tv or multi-param ones are definite errors
2018 (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
2019 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2021 -- Group by type variable
2022 tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
2024 -- Pick the ones which its worth trying to disambiguate
2025 -- namely, the ones whose type variable isn't bound
2026 -- up with one of the non-tyvar classes
2027 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2028 defaultable_group ds
2029 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
2030 && defaultable_classes (map get_clas ds)
2031 defaultable_classes clss
2032 | is_interactive = any isInteractiveClass clss
2033 | otherwise = all isStandardClass clss && any isNumericClass clss
2035 isInteractiveClass cls = isNumericClass cls
2036 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2037 -- In interactive mode, we default Show a to Show ()
2038 -- to avoid graututious errors on "show []"
2041 -- Collect together all the bad guys
2042 bad_guys = non_tvs ++ concat non_default_gps
2043 (ambigs, no_insts) = partition isTyVarDict bad_guys
2044 -- If the dict has no type constructors involved, it must be ambiguous,
2045 -- except I suppose that another error with fundeps maybe should have
2046 -- constrained those type variables
2048 -- Report definite errors
2049 ; ASSERT( null frees )
2050 groupErrs (addNoInstanceErrs Nothing []) no_insts
2051 ; strangeTopIPErrs bad_ips
2053 -- Deal with ambiguity errors, but only if
2054 -- if there has not been an error so far:
2055 -- errors often give rise to spurious ambiguous Insts.
2057 -- f = (*) -- Monomorphic
2058 -- g :: Num a => a -> a
2060 -- Here, we get a complaint when checking the type signature for g,
2061 -- that g isn't polymorphic enough; but then we get another one when
2062 -- dealing with the (Num a) context arising from f's definition;
2063 -- we try to unify a with Int (to default it), but find that it's
2064 -- already been unified with the rigid variable from g's type sig
2065 ; binds_ambig <- ifErrsM (returnM []) $
2066 do { -- Complain about the ones that don't fall under
2067 -- the Haskell rules for disambiguation
2068 -- This group includes both non-existent instances
2069 -- e.g. Num (IO a) and Eq (Int -> Int)
2070 -- and ambiguous dictionaries
2072 addTopAmbigErrs ambigs
2074 -- Disambiguate the ones that look feasible
2075 ; mappM disambigGroup default_gps }
2077 ; return (binds `unionBags` unionManyBags binds_ambig) }
2079 ----------------------------------
2080 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2082 is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
2083 -- Invariant: argument is a ClassDict, not IP or method
2084 is_unary_tyvar_dict d = case getDictClassTys d of
2085 (_, [ty]) -> tcIsTyVarTy ty
2088 get_tv d = case getDictClassTys d of
2089 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2090 get_clas d = case getDictClassTys d of
2094 If a dictionary constrains a type variable which is
2095 * not mentioned in the environment
2096 * and not mentioned in the type of the expression
2097 then it is ambiguous. No further information will arise to instantiate
2098 the type variable; nor will it be generalised and turned into an extra
2099 parameter to a function.
2101 It is an error for this to occur, except that Haskell provided for
2102 certain rules to be applied in the special case of numeric types.
2104 * at least one of its classes is a numeric class, and
2105 * all of its classes are numeric or standard
2106 then the type variable can be defaulted to the first type in the
2107 default-type list which is an instance of all the offending classes.
2109 So here is the function which does the work. It takes the ambiguous
2110 dictionaries and either resolves them (producing bindings) or
2111 complains. It works by splitting the dictionary list by type
2112 variable, and using @disambigOne@ to do the real business.
2114 @disambigOne@ assumes that its arguments dictionaries constrain all
2115 the same type variable.
2117 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2118 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2119 the most common use of defaulting is code like:
2121 _ccall_ foo `seqPrimIO` bar
2123 Since we're not using the result of @foo@, the result if (presumably)
2127 disambigGroup :: [Inst] -- All standard classes of form (C a)
2131 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2132 -- SO, TRY DEFAULT TYPES IN ORDER
2134 -- Failure here is caused by there being no type in the
2135 -- default list which can satisfy all the ambiguous classes.
2136 -- For example, if Real a is reqd, but the only type in the
2137 -- default list is Int.
2138 get_default_tys `thenM` \ default_tys ->
2140 try_default [] -- No defaults work, so fail
2143 try_default (default_ty : default_tys)
2144 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2145 -- default_tys instead
2146 tcSimplifyDefault theta `thenM` \ _ ->
2149 theta = [mkClassPred clas [default_ty] | clas <- classes]
2151 -- See if any default works
2152 tryM (try_default default_tys) `thenM` \ mb_ty ->
2155 Right chosen_default_ty -> choose_default chosen_default_ty
2157 tyvar = get_tv (head dicts) -- Should be non-empty
2158 classes = map get_clas dicts
2160 choose_default default_ty -- Commit to tyvar = default_ty
2161 = -- Bind the type variable
2162 unifyTauTy default_ty (mkTyVarTy tyvar) `thenM_`
2163 -- and reduce the context, for real this time
2164 simpleReduceLoop (text "disambig" <+> ppr dicts)
2165 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2166 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2167 warnDefault dicts default_ty `thenM_`
2170 bomb_out = addTopAmbigErrs dicts `thenM_`
2174 = do { mb_defaults <- getDefaultTys
2175 ; case mb_defaults of
2176 Just tys -> return tys
2177 Nothing -> -- No use-supplied default;
2178 -- use [Integer, Double]
2179 do { integer_ty <- tcMetaTy integerTyConName
2180 ; checkWiredInTyCon doubleTyCon
2181 ; return [integer_ty, doubleTy] } }
2184 [Aside - why the defaulting mechanism is turned off when
2185 dealing with arguments and results to ccalls.
2187 When typechecking _ccall_s, TcExpr ensures that the external
2188 function is only passed arguments (and in the other direction,
2189 results) of a restricted set of 'native' types.
2191 The interaction between the defaulting mechanism for numeric
2192 values and CC & CR can be a bit puzzling to the user at times.
2201 What type has 'x' got here? That depends on the default list
2202 in operation, if it is equal to Haskell 98's default-default
2203 of (Integer, Double), 'x' has type Double, since Integer
2204 is not an instance of CR. If the default list is equal to
2205 Haskell 1.4's default-default of (Int, Double), 'x' has type
2211 %************************************************************************
2213 \subsection[simple]{@Simple@ versions}
2215 %************************************************************************
2217 Much simpler versions when there are no bindings to make!
2219 @tcSimplifyThetas@ simplifies class-type constraints formed by
2220 @deriving@ declarations and when specialising instances. We are
2221 only interested in the simplified bunch of class/type constraints.
2223 It simplifies to constraints of the form (C a b c) where
2224 a,b,c are type variables. This is required for the context of
2225 instance declarations.
2228 tcSimplifyDeriv :: [TyVar]
2229 -> ThetaType -- Wanted
2230 -> TcM ThetaType -- Needed
2232 tcSimplifyDeriv tyvars theta
2233 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2234 -- The main loop may do unification, and that may crash if
2235 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2236 -- ToDo: what if two of them do get unified?
2237 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2238 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2239 ASSERT( null frees ) -- reduceMe never returns Free
2241 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2243 tv_set = mkVarSet tvs
2245 (bad_insts, ok_insts) = partition is_bad_inst irreds
2247 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2248 in isEmptyVarSet (tyVarsOfPred pred)
2249 -- Things like (Eq T) are bad
2250 || (not undecidable_ok && not (isTyVarClassPred pred))
2251 -- The returned dictionaries should be of form (C a b)
2252 -- (where a, b are type variables).
2253 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
2254 -- but note that risks non-termination in the 'deriving' context-inference
2255 -- fixpoint loop. It is useful for situations like
2256 -- data Min h a = E | M a (h a)
2257 -- which gives the instance decl
2258 -- instance (Eq a, Eq (h a)) => Eq (Min h a)
2260 simpl_theta = map dictPred ok_insts
2261 weird_preds = [pred | pred <- simpl_theta
2262 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2263 -- Check for a bizarre corner case, when the derived instance decl should
2264 -- have form instance C a b => D (T a) where ...
2265 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2266 -- of problems; in particular, it's hard to compare solutions for
2267 -- equality when finding the fixpoint. So I just rule it out for now.
2269 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2270 -- This reverse-mapping is a Royal Pain,
2271 -- but the result should mention TyVars not TcTyVars
2274 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2275 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2276 checkAmbiguity tvs simpl_theta tv_set `thenM_`
2277 returnM (substTheta rev_env simpl_theta)
2279 doc = ptext SLIT("deriving classes for a data type")
2282 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2283 used with \tr{default} declarations. We are only interested in
2284 whether it worked or not.
2287 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2290 tcSimplifyDefault theta
2291 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2292 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2293 ASSERT( null frees ) -- try_me never returns Free
2294 addNoInstanceErrs Nothing [] irreds `thenM_`
2300 doc = ptext SLIT("default declaration")
2304 %************************************************************************
2306 \section{Errors and contexts}
2308 %************************************************************************
2310 ToDo: for these error messages, should we note the location as coming
2311 from the insts, or just whatever seems to be around in the monad just
2315 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2316 -> [Inst] -- The offending Insts
2318 -- Group together insts with the same origin
2319 -- We want to report them together in error messages
2321 groupErrs report_err []
2323 groupErrs report_err (inst:insts)
2324 = do_one (inst:friends) `thenM_`
2325 groupErrs report_err others
2328 -- (It may seem a bit crude to compare the error messages,
2329 -- but it makes sure that we combine just what the user sees,
2330 -- and it avoids need equality on InstLocs.)
2331 (friends, others) = partition is_friend insts
2332 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2333 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2334 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2335 -- Add location and context information derived from the Insts
2337 -- Add the "arising from..." part to a message about bunch of dicts
2338 addInstLoc :: [Inst] -> Message -> Message
2339 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2341 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2342 addTopIPErrs bndrs []
2344 addTopIPErrs bndrs ips
2345 = addErrTcM (tidy_env, mk_msg tidy_ips)
2347 (tidy_env, tidy_ips) = tidyInsts ips
2348 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
2349 pprBinders bndrs <> colon],
2350 nest 2 (vcat (map ppr_ip ips)),
2352 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2354 strangeTopIPErrs :: [Inst] -> TcM ()
2355 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2356 = groupErrs report tidy_dicts
2358 (tidy_env, tidy_dicts) = tidyInsts dicts
2359 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2360 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2361 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2363 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2364 -- Just d => d describes the construct
2365 -> [Inst] -- What is given by the context or type sig
2366 -> [Inst] -- What is wanted
2368 addNoInstanceErrs mb_what givens []
2370 addNoInstanceErrs mb_what givens dicts
2371 = -- Some of the dicts are here because there is no instances
2372 -- and some because there are too many instances (overlap)
2373 tcGetInstEnvs `thenM` \ inst_envs ->
2375 (tidy_env1, tidy_givens) = tidyInsts givens
2376 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2378 -- Run through the dicts, generating a message for each
2379 -- overlapping one, but simply accumulating all the
2380 -- no-instance ones so they can be reported as a group
2381 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2382 check_overlap (overlap_doc, no_inst_dicts) dict
2383 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2385 = case lookupInstEnv inst_envs clas tys of
2386 -- The case of exactly one match and no unifiers means
2387 -- a successful lookup. That can't happen here, becuase
2388 -- dicts only end up here if they didn't match in Inst.lookupInst
2390 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2392 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2393 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2395 (clas,tys) = getDictClassTys dict
2398 -- Now generate a good message for the no-instance bunch
2399 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2401 no_inst_doc | null no_inst_dicts = empty
2402 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2403 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2404 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2405 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2406 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2408 -- And emit both the non-instance and overlap messages
2409 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2411 mk_overlap_msg dict (matches, unifiers)
2412 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2413 <+> pprPred (dictPred dict))),
2414 sep [ptext SLIT("Matching instances") <> colon,
2415 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2416 ASSERT( not (null matches) )
2417 if not (isSingleton matches)
2418 then -- Two or more matches
2420 else -- One match, plus some unifiers
2421 ASSERT( not (null unifiers) )
2422 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2423 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2424 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2426 ispecs = [ispec | (_, ispec) <- matches]
2428 mk_probable_fix tidy_env dicts
2429 = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
2431 fixes = add_ors (fix1 ++ fix2)
2433 fix1 = case mb_what of
2434 Nothing -> [] -- Top level
2435 Just what -> -- Nested (type signatures, instance decls)
2436 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2437 ptext SLIT("to the") <+> what] ]
2439 fix2 | null instance_dicts = []
2440 | otherwise = [ ptext SLIT("add an instance declaration for")
2441 <+> pprDictsTheta instance_dicts ]
2442 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2443 -- Insts for which it is worth suggesting an adding an instance declaration
2444 -- Exclude implicit parameters, and tyvar dicts
2446 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2447 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2448 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2450 addTopAmbigErrs dicts
2451 -- Divide into groups that share a common set of ambiguous tyvars
2452 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2454 (tidy_env, tidy_dicts) = tidyInsts dicts
2456 tvs_of :: Inst -> [TcTyVar]
2457 tvs_of d = varSetElems (tyVarsOfInst d)
2458 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2460 report :: [(Inst,[TcTyVar])] -> TcM ()
2461 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2462 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2463 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2464 -- the location of the first one will do for the err message
2465 addErrTcM (tidy_env, msg $$ mono_msg)
2467 dicts = map fst pairs
2468 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2469 pprQuotedList tvs <+> in_msg,
2470 nest 2 (pprDictsInFull dicts)]
2471 in_msg = text "in the constraint" <> plural dicts <> colon
2474 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2475 -- There's an error with these Insts; if they have free type variables
2476 -- it's probably caused by the monomorphism restriction.
2477 -- Try to identify the offending variable
2478 -- ASSUMPTION: the Insts are fully zonked
2479 mkMonomorphismMsg tidy_env inst_tvs
2480 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2481 returnM (tidy_env, mk_msg docs)
2483 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2484 -- This happens in things like
2485 -- f x = show (read "foo")
2486 -- whre monomorphism doesn't play any role
2487 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2491 monomorphism_fix :: SDoc
2492 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2493 (ptext SLIT("give these definition(s) an explicit type signature")
2494 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2496 warnDefault dicts default_ty
2497 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2498 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2501 (_, tidy_dicts) = tidyInsts dicts
2502 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2503 quotes (ppr default_ty),
2504 pprDictsInFull tidy_dicts]
2506 -- Used for the ...Thetas variants; all top level
2508 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2509 ptext SLIT("type variables that are not data type parameters"),
2510 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2512 reduceDepthErr n stack
2513 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2514 ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2515 nest 4 (pprStack stack)]
2517 pprStack stack = vcat (map pprInstInFull stack)