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 )
25 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
26 import TcHsSyn ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
29 import Inst ( lookupInst, LookupInstResult(..),
30 tyVarsOfInst, fdPredsOfInsts, newDicts,
31 isDict, isClassDict, isLinearInst, linearInstType,
32 isStdClassTyVarDict, isMethodFor, isMethod,
33 instToId, tyVarsOfInsts, cloneDict,
34 ipNamesOfInsts, ipNamesOfInst, dictPred,
35 instBindingRequired, fdPredsOfInst,
36 newDictsAtLoc, tcInstClassOp,
37 getDictClassTys, isTyVarDict, instLoc,
38 zonkInst, tidyInsts, tidyMoreInsts,
39 Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
40 isInheritableInst, pprDictsTheta
42 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
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 )
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
1318 -- the irreductible ones, but don't
1319 -- produce an error message of any kind.
1320 -- It might be quite legitimate such as (Eq a)!
1322 | KeepDictWithoutSCs -- Return as irreducible; don't add its superclasses
1323 -- Rather specialised: see notes with tcSimplifyToDicts
1325 | DontReduceUnlessConstant -- Return as irreducible unless it can
1326 -- be reduced to a constant in one step
1328 | Free -- Return as free
1330 reduceMe :: Inst -> WhatToDo
1331 reduceMe inst = ReduceMe AddSCs
1333 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1334 -- of a predicate when adding it to the avails
1340 type Avails = FiniteMap Inst Avail
1341 emptyAvails = emptyFM
1344 = IsFree -- Used for free Insts
1345 | Irred -- Used for irreducible dictionaries,
1346 -- which are going to be lambda bound
1348 | Given TcId -- Used for dictionaries for which we have a binding
1349 -- e.g. those "given" in a signature
1350 Bool -- True <=> actually consumed (splittable IPs only)
1352 | NoRhs -- Used for Insts like (CCallable f)
1353 -- where no witness is required.
1356 | Rhs -- Used when there is a RHS
1357 (LHsExpr TcId) -- The RHS
1358 [Inst] -- Insts free in the RHS; we need these too
1360 | Linear -- Splittable Insts only.
1361 Int -- The Int is always 2 or more; indicates how
1362 -- many copies are required
1363 Inst -- The splitter
1364 Avail -- Where the "master copy" is
1366 | LinRhss -- Splittable Insts only; this is used only internally
1367 -- by extractResults, where a Linear
1368 -- is turned into an LinRhss
1369 [LHsExpr TcId] -- A supply of suitable RHSs
1371 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1372 | (inst,avail) <- fmToList avails ]
1374 instance Outputable Avail where
1377 pprAvail NoRhs = text "<no rhs>"
1378 pprAvail IsFree = text "Free"
1379 pprAvail Irred = text "Irred"
1380 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1381 if b then text "(used)" else empty
1382 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1383 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1384 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1387 Extracting the bindings from a bunch of Avails.
1388 The bindings do *not* come back sorted in dependency order.
1389 We assume that they'll be wrapped in a big Rec, so that the
1390 dependency analyser can sort them out later
1394 extractResults :: Avails
1396 -> TcM (TcDictBinds, -- Bindings
1397 [Inst], -- Irreducible ones
1398 [Inst]) -- Free ones
1400 extractResults avails wanteds
1401 = go avails emptyBag [] [] wanteds
1403 go avails binds irreds frees []
1404 = returnM (binds, irreds, frees)
1406 go avails binds irreds frees (w:ws)
1407 = case lookupFM avails w of
1408 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1409 go avails binds irreds frees ws
1411 Just NoRhs -> go avails binds irreds frees ws
1412 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1413 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1415 Just (Given id _) -> go avails new_binds irreds frees ws
1417 new_binds | id == instToId w = binds
1418 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1419 -- The sought Id can be one of the givens, via a superclass chain
1420 -- and then we definitely don't want to generate an x=x binding!
1422 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1424 new_binds = addBind binds w rhs
1426 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1427 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1428 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1429 go (addToFM avails w (LinRhss rhss))
1430 (binds `unionBags` binds')
1431 irreds' frees' (split_inst : w : ws)
1433 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1434 -> go new_avails new_binds irreds frees ws
1436 new_binds = addBind binds w rhs
1437 new_avails = addToFM avails w (LinRhss rhss)
1439 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1440 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1441 returnM (w':irreds, frees, instToId w')
1442 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1443 returnM (irreds, w':frees, instToId w')
1446 | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1447 | otherwise = addToFM avails w NoRhs
1448 -- NB: make sure that CCallable/CReturnable use NoRhs rather
1449 -- than Given, else we end up with bogus bindings.
1451 add_free avails w | isMethod w = avails
1452 | otherwise = add_given avails w
1454 -- Do *not* replace Free by Given if it's a method.
1455 -- The following situation shows why this is bad:
1456 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1457 -- From an application (truncate f i) we get
1458 -- t1 = truncate at f
1460 -- If we have also have a second occurrence of truncate, we get
1461 -- t3 = truncate at f
1463 -- When simplifying with i,f free, we might still notice that
1464 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1465 -- will continue to float out!
1466 -- (split n i a) returns: n rhss
1467 -- auxiliary bindings
1468 -- 1 or 0 insts to add to irreds
1471 split :: Int -> TcId -> TcId -> Inst
1472 -> TcM (TcDictBinds, [LHsExpr TcId])
1473 -- (split n split_id root_id wanted) returns
1474 -- * a list of 'n' expressions, all of which witness 'avail'
1475 -- * a bunch of auxiliary bindings to support these expressions
1476 -- * one or zero insts needed to witness the whole lot
1477 -- (maybe be zero if the initial Inst is a Given)
1479 -- NB: 'wanted' is just a template
1481 split n split_id root_id wanted
1484 ty = linearInstType wanted
1485 pair_ty = mkTyConApp pairTyCon [ty,ty]
1486 id = instToId wanted
1489 span = instSpan wanted
1491 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1493 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1494 expand n rhss `thenM` \ (binds2, rhss') ->
1495 returnM (binds1 `unionBags` binds2, rhss')
1498 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1499 -- e.g. expand 3 [rhs1, rhs2]
1500 -- = ( { x = split rhs1 },
1501 -- [fst x, snd x, rhs2] )
1503 | n `rem` 2 == 0 = go rhss -- n is even
1504 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1505 returnM (binds', head rhss : rhss')
1507 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1508 returnM (listToBag binds', concat rhss')
1510 do_one rhs = newUnique `thenM` \ uniq ->
1511 tcLookupId fstName `thenM` \ fst_id ->
1512 tcLookupId sndName `thenM` \ snd_id ->
1514 x = mkUserLocal occ uniq pair_ty loc
1516 returnM (L span (VarBind x (mk_app span split_id rhs)),
1517 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1519 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1521 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1523 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1524 (VarBind (instToId inst) rhs))
1525 instSpan wanted = instLocSrcSpan (instLoc wanted)
1529 %************************************************************************
1531 \subsection[reduce]{@reduce@}
1533 %************************************************************************
1535 When the "what to do" predicate doesn't depend on the quantified type variables,
1536 matters are easier. We don't need to do any zonking, unless the improvement step
1537 does something, in which case we zonk before iterating.
1539 The "given" set is always empty.
1542 simpleReduceLoop :: SDoc
1543 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1545 -> TcM ([Inst], -- Free
1547 [Inst]) -- Irreducible
1549 simpleReduceLoop doc try_me wanteds
1550 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1551 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1552 if no_improvement then
1553 returnM (frees, binds, irreds)
1555 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1556 returnM (frees1, binds `unionBags` binds1, irreds1)
1562 reduceContext :: SDoc
1563 -> (Inst -> WhatToDo)
1566 -> TcM (Bool, -- True <=> improve step did no unification
1568 TcDictBinds, -- Dictionary bindings
1569 [Inst]) -- Irreducible
1571 reduceContext doc try_me givens wanteds
1573 traceTc (text "reduceContext" <+> (vcat [
1574 text "----------------------",
1576 text "given" <+> ppr givens,
1577 text "wanted" <+> ppr wanteds,
1578 text "----------------------"
1581 -- Build the Avail mapping from "givens"
1582 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1585 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1587 -- Do improvement, using everything in avails
1588 -- In particular, avails includes all superclasses of everything
1589 tcImprove avails `thenM` \ no_improvement ->
1591 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1593 traceTc (text "reduceContext end" <+> (vcat [
1594 text "----------------------",
1596 text "given" <+> ppr givens,
1597 text "wanted" <+> ppr wanteds,
1599 text "avails" <+> pprAvails avails,
1600 text "frees" <+> ppr frees,
1601 text "no_improvement =" <+> ppr no_improvement,
1602 text "----------------------"
1605 returnM (no_improvement, frees, binds, irreds)
1607 -- reduceContextWithoutImprovement differs from reduceContext
1608 -- (a) no improvement
1609 -- (b) 'givens' is assumed empty
1610 reduceContextWithoutImprovement doc try_me wanteds
1612 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1613 text "----------------------",
1615 text "wanted" <+> ppr wanteds,
1616 text "----------------------"
1620 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1621 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1623 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1624 text "----------------------",
1626 text "wanted" <+> ppr wanteds,
1628 text "avails" <+> pprAvails avails,
1629 text "frees" <+> ppr frees,
1630 text "----------------------"
1633 returnM (frees, binds, irreds)
1635 tcImprove :: Avails -> TcM Bool -- False <=> no change
1636 -- Perform improvement using all the predicates in Avails
1638 = tcGetInstEnvs `thenM` \ inst_envs ->
1640 preds = [ (pred, pp_loc)
1641 | (inst, avail) <- fmToList avails,
1642 pred <- get_preds inst avail,
1643 let pp_loc = pprInstLoc (instLoc inst)
1645 -- Avails has all the superclasses etc (good)
1646 -- It also has all the intermediates of the deduction (good)
1647 -- It does not have duplicates (good)
1648 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1649 -- so that improve will see them separate
1651 -- For free Methods, we want to take predicates from their context,
1652 -- but for Methods that have been squished their context will already
1653 -- be in Avails, and we don't want duplicates. Hence this rather
1654 -- horrid get_preds function
1655 get_preds inst IsFree = fdPredsOfInst inst
1656 get_preds inst other | isDict inst = [dictPred inst]
1659 eqns = improve get_insts preds
1660 get_insts clas = classInstances inst_envs clas
1665 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1666 mappM_ unify eqns `thenM_`
1669 unify ((qtvs, pairs), doc)
1671 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1672 mapM_ (unif_pr tenv) pairs
1673 unif_pr tenv (ty1,ty2) = unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
1676 The main context-reduction function is @reduce@. Here's its game plan.
1679 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1680 -- along with its depth
1681 -> (Inst -> WhatToDo)
1688 try_me: given an inst, this function returns
1690 DontReduce return this in "irreds"
1691 Free return this in "frees"
1693 wanteds: The list of insts to reduce
1694 state: An accumulating parameter of type Avails
1695 that contains the state of the algorithm
1697 It returns a Avails.
1699 The (n,stack) pair is just used for error reporting.
1700 n is always the depth of the stack.
1701 The stack is the stack of Insts being reduced: to produce X
1702 I had to produce Y, to produce Y I had to produce Z, and so on.
1705 reduceList (n,stack) try_me wanteds state
1706 | n > opt_MaxContextReductionDepth
1707 = failWithTc (reduceDepthErr n stack)
1713 pprTrace "Interesting! Context reduction stack deeper than 8:"
1714 (nest 2 (pprStack stack))
1719 go [] state = returnM state
1720 go (w:ws) state = reduce (n+1, w:stack) try_me w state `thenM` \ state' ->
1723 -- Base case: we're done!
1724 reduce stack try_me wanted avails
1725 -- It's the same as an existing inst, or a superclass thereof
1726 | Just avail <- isAvailable avails wanted
1727 = if isLinearInst wanted then
1728 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1729 reduceList stack try_me wanteds' avails'
1731 returnM avails -- No op for non-linear things
1734 = case try_me wanted of {
1736 KeepDictWithoutSCs -> addIrred NoSCs avails wanted
1738 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1739 -- First, see if the inst can be reduced to a constant in one step
1740 try_simple (addIrred AddSCs) -- Assume want superclasses
1742 ; Free -> -- It's free so just chuck it upstairs
1743 -- First, see if the inst can be reduced to a constant in one step
1746 ; ReduceMe want_scs -> -- It should be reduced
1747 lookupInst wanted `thenM` \ lookup_result ->
1748 case lookup_result of
1749 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1750 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1751 addWanted want_scs avails2 wanted rhs wanteds'
1752 -- Experiment with temporarily doing addIrred *before* the reduceList,
1753 -- which has the effect of adding the thing we are trying
1754 -- to prove to the database before trying to prove the things it
1755 -- needs. See note [RECURSIVE DICTIONARIES]
1756 -- NB: we must not do an addWanted before, because that adds the
1757 -- superclasses too, and thaat can lead to a spurious loop; see
1758 -- the examples in [SUPERCLASS-LOOP]
1759 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1761 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1763 NoInstance -> -- No such instance!
1764 -- Add it and its superclasses
1765 addIrred want_scs avails wanted
1768 try_simple do_this_otherwise
1769 = lookupInst wanted `thenM` \ lookup_result ->
1770 case lookup_result of
1771 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1772 other -> do_this_otherwise avails wanted
1777 -------------------------
1778 isAvailable :: Avails -> Inst -> Maybe Avail
1779 isAvailable avails wanted = lookupFM avails wanted
1780 -- NB 1: the Ord instance of Inst compares by the class/type info
1781 -- *not* by unique. So
1782 -- d1::C Int == d2::C Int
1784 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1785 addLinearAvailable avails avail wanted
1786 -- avails currently maps [wanted -> avail]
1787 -- Extend avails to reflect a neeed for an extra copy of avail
1789 | Just avail' <- split_avail avail
1790 = returnM (addToFM avails wanted avail', [])
1793 = tcLookupId splitName `thenM` \ split_id ->
1794 tcInstClassOp (instLoc wanted) split_id
1795 [linearInstType wanted] `thenM` \ split_inst ->
1796 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1799 split_avail :: Avail -> Maybe Avail
1800 -- (Just av) if there's a modified version of avail that
1801 -- we can use to replace avail in avails
1802 -- Nothing if there isn't, so we need to create a Linear
1803 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1804 split_avail (Given id used) | not used = Just (Given id True)
1805 | otherwise = Nothing
1806 split_avail Irred = Nothing
1807 split_avail IsFree = Nothing
1808 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1810 -------------------------
1811 addFree :: Avails -> Inst -> TcM Avails
1812 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1813 -- to avails, so that any other equal Insts will be commoned up right
1814 -- here rather than also being tossed upstairs. This is really just
1815 -- an optimisation, and perhaps it is more trouble that it is worth,
1816 -- as the following comments show!
1818 -- NB: do *not* add superclasses. If we have
1821 -- but a is not bound here, then we *don't* want to derive
1822 -- dn from df here lest we lose sharing.
1824 addFree avails free = returnM (addToFM avails free IsFree)
1826 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1827 addWanted want_scs avails wanted rhs_expr wanteds
1828 = addAvailAndSCs want_scs avails wanted avail
1830 avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1831 | otherwise = ASSERT( null wanteds ) NoRhs
1833 addGiven :: Avails -> Inst -> TcM Avails
1834 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1835 -- Always add superclasses for 'givens'
1837 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1838 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1839 -- so the assert isn't true
1841 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1842 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1843 addAvailAndSCs want_scs avails irred Irred
1845 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1846 addAvailAndSCs want_scs avails inst avail
1847 | not (isClassDict inst) = return avails_with_inst
1848 | NoSCs <- want_scs = return avails_with_inst
1849 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1850 ; addSCs is_loop avails_with_inst inst }
1852 avails_with_inst = addToFM avails inst avail
1854 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1855 -- Note: this compares by *type*, not by Unique
1856 deps = findAllDeps (unitVarSet (instToId inst)) avail
1857 dep_tys = map idType (varSetElems deps)
1859 findAllDeps :: IdSet -> Avail -> IdSet
1860 -- Find all the Insts that this one depends on
1861 -- See Note [SUPERCLASS-LOOP]
1862 -- Watch out, though. Since the avails may contain loops
1863 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1864 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1865 findAllDeps so_far other = so_far
1867 find_all :: IdSet -> Inst -> IdSet
1869 | kid_id `elemVarSet` so_far = so_far
1870 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1871 | otherwise = so_far'
1873 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1874 kid_id = instToId kid
1876 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1877 -- Add all the superclasses of the Inst to Avails
1878 -- The first param says "dont do this because the original thing
1879 -- depends on this one, so you'd build a loop"
1880 -- Invariant: the Inst is already in Avails.
1882 addSCs is_loop avails dict
1883 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1884 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1886 (clas, tys) = getDictClassTys dict
1887 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1888 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1890 add_sc avails (sc_dict, sc_sel)
1891 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1892 | is_given sc_dict = return avails
1893 | otherwise = addSCs is_loop avails' sc_dict
1895 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1896 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1898 is_given :: Inst -> Bool
1899 is_given sc_dict = case lookupFM avails sc_dict of
1900 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1904 Note [SUPERCLASS-LOOP 2]
1905 ~~~~~~~~~~~~~~~~~~~~~~~~
1906 But the above isn't enough. Suppose we are *given* d1:Ord a,
1907 and want to deduce (d2:C [a]) where
1909 class Ord a => C a where
1910 instance Ord [a] => C [a] where ...
1912 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1913 superclasses of C [a] to avails. But we must not overwrite the binding
1914 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1917 Here's another variant, immortalised in tcrun020
1918 class Monad m => C1 m
1919 class C1 m => C2 m x
1920 instance C2 Maybe Bool
1921 For the instance decl we need to build (C1 Maybe), and it's no good if
1922 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1923 before we search for C1 Maybe.
1925 Here's another example
1926 class Eq b => Foo a b
1927 instance Eq a => Foo [a] a
1931 we'll first deduce that it holds (via the instance decl). We must not
1932 then overwrite the Eq t constraint with a superclass selection!
1934 At first I had a gross hack, whereby I simply did not add superclass constraints
1935 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1936 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1937 I found a very obscure program (now tcrun021) in which improvement meant the
1938 simplifier got two bites a the cherry... so something seemed to be an Irred
1939 first time, but reducible next time.
1941 Now we implement the Right Solution, which is to check for loops directly
1942 when adding superclasses. It's a bit like the occurs check in unification.
1945 Note [RECURSIVE DICTIONARIES]
1946 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1948 data D r = ZeroD | SuccD (r (D r));
1950 instance (Eq (r (D r))) => Eq (D r) where
1951 ZeroD == ZeroD = True
1952 (SuccD a) == (SuccD b) = a == b
1955 equalDC :: D [] -> D [] -> Bool;
1958 We need to prove (Eq (D [])). Here's how we go:
1962 by instance decl, holds if
1966 by instance decl of Eq, holds if
1968 where d2 = dfEqList d3
1971 But now we can "tie the knot" to give
1977 and it'll even run! The trick is to put the thing we are trying to prove
1978 (in this case Eq (D []) into the database before trying to prove its
1979 contributing clauses.
1982 %************************************************************************
1984 \section{tcSimplifyTop: defaulting}
1986 %************************************************************************
1989 @tcSimplifyTop@ is called once per module to simplify all the constant
1990 and ambiguous Insts.
1992 We need to be careful of one case. Suppose we have
1994 instance Num a => Num (Foo a b) where ...
1996 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
1997 to (Num x), and default x to Int. But what about y??
1999 It's OK: the final zonking stage should zap y to (), which is fine.
2003 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2004 tcSimplifyTop wanteds
2005 = tc_simplify_top doc False {- Not interactive loop -} AddSCs wanteds
2007 doc = text "tcSimplifyTop"
2009 tcSimplifyInteractive wanteds
2010 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2012 doc = text "tcSimplifyTop"
2014 -- The TcLclEnv should be valid here, solely to improve
2015 -- error message generation for the monomorphism restriction
2016 tc_simplify_top doc is_interactive want_scs wanteds
2017 = do { lcl_env <- getLclEnv
2018 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2020 ; let try_me inst = ReduceMe want_scs
2021 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2024 -- All the non-std ones are definite errors
2025 (stds, non_stds) = partition isStdClassTyVarDict irreds
2027 -- Group by type variable
2028 std_groups = equivClasses cmp_by_tyvar stds
2030 -- Pick the ones which its worth trying to disambiguate
2031 -- namely, the onese whose type variable isn't bound
2032 -- up with one of the non-standard classes
2033 (std_oks, std_bads) = partition worth_a_try std_groups
2034 worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
2035 non_std_tyvars = unionVarSets (map tyVarsOfInst non_stds)
2037 -- Collect together all the bad guys
2038 bad_guys = non_stds ++ concat std_bads
2039 (non_ips, bad_ips) = partition isClassDict bad_guys
2040 (ambigs, no_insts) = partition isTyVarDict non_ips
2041 -- If the dict has no type constructors involved, it must be ambiguous,
2042 -- except I suppose that another error with fundeps maybe should have
2043 -- constrained those type variables
2045 -- Report definite errors
2046 ; ASSERT( null frees )
2047 groupErrs (addNoInstanceErrs Nothing []) no_insts
2048 ; strangeTopIPErrs bad_ips
2050 -- Deal with ambiguity errors, but only if
2051 -- if there has not been an error so far:
2052 -- errors often give rise to spurious ambiguous Insts.
2054 -- f = (*) -- Monomorphic
2055 -- g :: Num a => a -> a
2057 -- Here, we get a complaint when checking the type signature for g,
2058 -- that g isn't polymorphic enough; but then we get another one when
2059 -- dealing with the (Num a) context arising from f's definition;
2060 -- we try to unify a with Int (to default it), but find that it's
2061 -- already been unified with the rigid variable from g's type sig
2062 ; binds_ambig <- ifErrsM (returnM []) $
2063 do { -- Complain about the ones that don't fall under
2064 -- the Haskell rules for disambiguation
2065 -- This group includes both non-existent instances
2066 -- e.g. Num (IO a) and Eq (Int -> Int)
2067 -- and ambiguous dictionaries
2069 addTopAmbigErrs ambigs
2071 -- Disambiguate the ones that look feasible
2072 ; mappM (disambigGroup is_interactive) std_oks }
2074 ; return (binds `unionBags` unionManyBags binds_ambig) }
2076 ----------------------------------
2077 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2079 get_tv d = case getDictClassTys d of
2080 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2081 get_clas d = case getDictClassTys d of
2082 (clas, [ty]) -> clas
2085 If a dictionary constrains a type variable which is
2086 * not mentioned in the environment
2087 * and not mentioned in the type of the expression
2088 then it is ambiguous. No further information will arise to instantiate
2089 the type variable; nor will it be generalised and turned into an extra
2090 parameter to a function.
2092 It is an error for this to occur, except that Haskell provided for
2093 certain rules to be applied in the special case of numeric types.
2095 * at least one of its classes is a numeric class, and
2096 * all of its classes are numeric or standard
2097 then the type variable can be defaulted to the first type in the
2098 default-type list which is an instance of all the offending classes.
2100 So here is the function which does the work. It takes the ambiguous
2101 dictionaries and either resolves them (producing bindings) or
2102 complains. It works by splitting the dictionary list by type
2103 variable, and using @disambigOne@ to do the real business.
2105 @disambigOne@ assumes that its arguments dictionaries constrain all
2106 the same type variable.
2108 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2109 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2110 the most common use of defaulting is code like:
2112 _ccall_ foo `seqPrimIO` bar
2114 Since we're not using the result of @foo@, the result if (presumably)
2118 disambigGroup :: Bool -- True <=> simplifying at top-level interactive loop
2119 -> [Inst] -- All standard classes of form (C a)
2122 disambigGroup is_interactive dicts
2123 | any std_default_class classes -- Guaranteed all standard classes
2124 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2125 -- SO, TRY DEFAULT TYPES IN ORDER
2127 -- Failure here is caused by there being no type in the
2128 -- default list which can satisfy all the ambiguous classes.
2129 -- For example, if Real a is reqd, but the only type in the
2130 -- default list is Int.
2131 get_default_tys `thenM` \ default_tys ->
2133 try_default [] -- No defaults work, so fail
2136 try_default (default_ty : default_tys)
2137 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2138 -- default_tys instead
2139 tcSimplifyDefault theta `thenM` \ _ ->
2142 theta = [mkClassPred clas [default_ty] | clas <- classes]
2144 -- See if any default works
2145 tryM (try_default default_tys) `thenM` \ mb_ty ->
2148 Right chosen_default_ty -> choose_default chosen_default_ty
2150 | otherwise -- No defaults
2154 tyvar = get_tv (head dicts) -- Should be non-empty
2155 classes = map get_clas dicts
2157 std_default_class cls
2158 = isNumericClass cls
2159 || (is_interactive &&
2160 classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2161 -- In interactive mode, we default Show a to Show ()
2162 -- to avoid graututious errors on "show []"
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)