2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcSimplify]{TcSimplify}
10 tcSimplifyInfer, tcSimplifyInferCheck,
11 tcSimplifyCheck, tcSimplifyRestricted,
12 tcSimplifyRuleLhs, tcSimplifyIPs,
13 tcSimplifySuperClasses,
14 tcSimplifyTop, tcSimplifyInteractive,
17 tcSimplifyDeriv, tcSimplifyDefault,
21 #include "HsVersions.h"
23 import {-# SOURCE #-} TcUnify( unifyType )
24 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, mkCoTyApps,
25 ExprCoFn(..), (<.>), nlHsTyApp, emptyLHsBinds )
26 import TcHsSyn ( mkHsApp )
29 import Inst ( lookupInst, LookupInstResult(..),
30 tyVarsOfInst, fdPredsOfInsts,
31 isDict, isClassDict, isLinearInst, linearInstType,
32 isMethodFor, isMethod,
33 instToId, tyVarsOfInsts, cloneDict,
34 ipNamesOfInsts, ipNamesOfInst, dictPred,
36 newDictBndrs, newDictBndrsO, tcInstClassOp,
37 getDictClassTys, isTyVarDict, instLoc,
38 zonkInst, tidyInsts, tidyMoreInsts,
39 pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
40 isInheritableInst, pprDictsTheta
42 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
43 lclEnvElts, tcMetaTy )
44 import InstEnv ( lookupInstEnv, classInstances, pprInstances )
45 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType )
46 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
47 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
48 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
49 tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
50 import TcIface ( checkWiredInTyCon )
51 import Id ( idType, mkUserLocal )
53 import TyCon ( TyCon )
54 import Name ( Name, getOccName, getSrcLoc )
55 import NameSet ( NameSet, mkNameSet, elemNameSet )
56 import Class ( classBigSig, classKey )
57 import FunDeps ( oclose, grow, improve, pprEquation )
58 import PrelInfo ( isNumericClass, isStandardClass )
59 import PrelNames ( splitName, fstName, sndName, integerTyConName,
60 showClassKey, eqClassKey, ordClassKey )
61 import Type ( zipTopTvSubst, substTheta, substTy )
62 import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
63 import ErrUtils ( Message )
64 import BasicTypes ( TopLevelFlag, isNotTopLevel )
66 import VarEnv ( TidyEnv )
70 import ListSetOps ( equivClasses )
71 import Util ( zipEqual, isSingleton )
72 import List ( partition )
73 import SrcLoc ( Located(..) )
74 import DynFlags ( DynFlags(ctxtStkDepth),
75 DynFlag( Opt_GlasgowExts, Opt_AllowUndecidableInstances,
76 Opt_WarnTypeDefaults, Opt_ExtendedDefaultRules ) )
80 %************************************************************************
84 %************************************************************************
86 --------------------------------------
87 Notes on functional dependencies (a bug)
88 --------------------------------------
95 instance D a b => C a b -- Undecidable
96 -- (Not sure if it's crucial to this eg)
97 f :: C a b => a -> Bool
100 g :: C a b => a -> Bool
103 Here f typechecks, but g does not!! Reason: before doing improvement,
104 we reduce the (C a b1) constraint from the call of f to (D a b1).
106 Here is a more complicated example:
108 | > class Foo a b | a->b
110 | > class Bar a b | a->b
114 | > instance Bar Obj Obj
116 | > instance (Bar a b) => Foo a b
118 | > foo:: (Foo a b) => a -> String
121 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
127 | Could not deduce (Bar a b) from the context (Foo a b)
128 | arising from use of `foo' at <interactive>:1
130 | Add (Bar a b) to the expected type of an expression
131 | In the first argument of `runFoo', namely `foo'
132 | In the definition of `it': it = runFoo foo
134 | Why all of the sudden does GHC need the constraint Bar a b? The
135 | function foo didn't ask for that...
137 The trouble is that to type (runFoo foo), GHC has to solve the problem:
139 Given constraint Foo a b
140 Solve constraint Foo a b'
142 Notice that b and b' aren't the same. To solve this, just do
143 improvement and then they are the same. But GHC currently does
148 That is usually fine, but it isn't here, because it sees that Foo a b is
149 not the same as Foo a b', and so instead applies the instance decl for
150 instance Bar a b => Foo a b. And that's where the Bar constraint comes
153 The Right Thing is to improve whenever the constraint set changes at
154 all. Not hard in principle, but it'll take a bit of fiddling to do.
158 --------------------------------------
159 Notes on quantification
160 --------------------------------------
162 Suppose we are about to do a generalisation step.
166 T the type of the RHS
167 C the constraints from that RHS
169 The game is to figure out
171 Q the set of type variables over which to quantify
172 Ct the constraints we will *not* quantify over
173 Cq the constraints we will quantify over
175 So we're going to infer the type
179 and float the constraints Ct further outwards.
181 Here are the things that *must* be true:
183 (A) Q intersect fv(G) = EMPTY limits how big Q can be
184 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
186 (A) says we can't quantify over a variable that's free in the
187 environment. (B) says we must quantify over all the truly free
188 variables in T, else we won't get a sufficiently general type. We do
189 not *need* to quantify over any variable that is fixed by the free
190 vars of the environment G.
192 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
194 Example: class H x y | x->y where ...
196 fv(G) = {a} C = {H a b, H c d}
199 (A) Q intersect {a} is empty
200 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
202 So Q can be {c,d}, {b,c,d}
204 Other things being equal, however, we'd like to quantify over as few
205 variables as possible: smaller types, fewer type applications, more
206 constraints can get into Ct instead of Cq.
209 -----------------------------------------
212 fv(T) the free type vars of T
214 oclose(vs,C) The result of extending the set of tyvars vs
215 using the functional dependencies from C
217 grow(vs,C) The result of extend the set of tyvars vs
218 using all conceivable links from C.
220 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
221 Then grow(vs,C) = {a,b,c}
223 Note that grow(vs,C) `superset` grow(vs,simplify(C))
224 That is, simplfication can only shrink the result of grow.
227 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
228 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
231 -----------------------------------------
235 Here's a good way to choose Q:
237 Q = grow( fv(T), C ) \ oclose( fv(G), C )
239 That is, quantify over all variable that that MIGHT be fixed by the
240 call site (which influences T), but which aren't DEFINITELY fixed by
241 G. This choice definitely quantifies over enough type variables,
242 albeit perhaps too many.
244 Why grow( fv(T), C ) rather than fv(T)? Consider
246 class H x y | x->y where ...
251 If we used fv(T) = {c} we'd get the type
253 forall c. H c d => c -> b
255 And then if the fn was called at several different c's, each of
256 which fixed d differently, we'd get a unification error, because
257 d isn't quantified. Solution: quantify d. So we must quantify
258 everything that might be influenced by c.
260 Why not oclose( fv(T), C )? Because we might not be able to see
261 all the functional dependencies yet:
263 class H x y | x->y where ...
264 instance H x y => Eq (T x y) where ...
269 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
270 apparent yet, and that's wrong. We must really quantify over d too.
273 There really isn't any point in quantifying over any more than
274 grow( fv(T), C ), because the call sites can't possibly influence
275 any other type variables.
279 -------------------------------------
281 -------------------------------------
283 It's very hard to be certain when a type is ambiguous. Consider
287 instance H x y => K (x,y)
289 Is this type ambiguous?
290 forall a b. (K (a,b), Eq b) => a -> a
292 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
293 now we see that a fixes b. So we can't tell about ambiguity for sure
294 without doing a full simplification. And even that isn't possible if
295 the context has some free vars that may get unified. Urgle!
297 Here's another example: is this ambiguous?
298 forall a b. Eq (T b) => a -> a
299 Not if there's an insance decl (with no context)
300 instance Eq (T b) where ...
302 You may say of this example that we should use the instance decl right
303 away, but you can't always do that:
305 class J a b where ...
306 instance J Int b where ...
308 f :: forall a b. J a b => a -> a
310 (Notice: no functional dependency in J's class decl.)
311 Here f's type is perfectly fine, provided f is only called at Int.
312 It's premature to complain when meeting f's signature, or even
313 when inferring a type for f.
317 However, we don't *need* to report ambiguity right away. It'll always
318 show up at the call site.... and eventually at main, which needs special
319 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
321 So here's the plan. We WARN about probable ambiguity if
323 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
325 (all tested before quantification).
326 That is, all the type variables in Cq must be fixed by the the variables
327 in the environment, or by the variables in the type.
329 Notice that we union before calling oclose. Here's an example:
331 class J a b c | a b -> c
335 forall b c. (J a b c) => b -> b
337 Only if we union {a} from G with {b} from T before using oclose,
338 do we see that c is fixed.
340 It's a bit vague exactly which C we should use for this oclose call. If we
341 don't fix enough variables we might complain when we shouldn't (see
342 the above nasty example). Nothing will be perfect. That's why we can
343 only issue a warning.
346 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
348 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
350 then c is a "bubble"; there's no way it can ever improve, and it's
351 certainly ambiguous. UNLESS it is a constant (sigh). And what about
356 instance H x y => K (x,y)
358 Is this type ambiguous?
359 forall a b. (K (a,b), Eq b) => a -> a
361 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
362 is a "bubble" that's a set of constraints
364 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
366 Hence another idea. To decide Q start with fv(T) and grow it
367 by transitive closure in Cq (no functional dependencies involved).
368 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
369 The definitely-ambiguous can then float out, and get smashed at top level
370 (which squashes out the constants, like Eq (T a) above)
373 --------------------------------------
374 Notes on principal types
375 --------------------------------------
380 f x = let g y = op (y::Int) in True
382 Here the principal type of f is (forall a. a->a)
383 but we'll produce the non-principal type
384 f :: forall a. C Int => a -> a
387 --------------------------------------
388 The need for forall's in constraints
389 --------------------------------------
391 [Exchange on Haskell Cafe 5/6 Dec 2000]
393 class C t where op :: t -> Bool
394 instance C [t] where op x = True
396 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
397 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
399 The definitions of p and q differ only in the order of the components in
400 the pair on their right-hand sides. And yet:
402 ghc and "Typing Haskell in Haskell" reject p, but accept q;
403 Hugs rejects q, but accepts p;
404 hbc rejects both p and q;
405 nhc98 ... (Malcolm, can you fill in the blank for us!).
407 The type signature for f forces context reduction to take place, and
408 the results of this depend on whether or not the type of y is known,
409 which in turn depends on which component of the pair the type checker
412 Solution: if y::m a, float out the constraints
413 Monad m, forall c. C (m c)
414 When m is later unified with [], we can solve both constraints.
417 --------------------------------------
418 Notes on implicit parameters
419 --------------------------------------
421 Question 1: can we "inherit" implicit parameters
422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
427 where f is *not* a top-level binding.
428 From the RHS of f we'll get the constraint (?y::Int).
429 There are two types we might infer for f:
433 (so we get ?y from the context of f's definition), or
435 f :: (?y::Int) => Int -> Int
437 At first you might think the first was better, becuase then
438 ?y behaves like a free variable of the definition, rather than
439 having to be passed at each call site. But of course, the WHOLE
440 IDEA is that ?y should be passed at each call site (that's what
441 dynamic binding means) so we'd better infer the second.
443 BOTTOM LINE: when *inferring types* you *must* quantify
444 over implicit parameters. See the predicate isFreeWhenInferring.
447 Question 2: type signatures
448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
449 BUT WATCH OUT: When you supply a type signature, we can't force you
450 to quantify over implicit parameters. For example:
454 This is perfectly reasonable. We do not want to insist on
456 (?x + 1) :: (?x::Int => Int)
458 That would be silly. Here, the definition site *is* the occurrence site,
459 so the above strictures don't apply. Hence the difference between
460 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
461 and tcSimplifyCheckBind (which does not).
463 What about when you supply a type signature for a binding?
464 Is it legal to give the following explicit, user type
465 signature to f, thus:
470 At first sight this seems reasonable, but it has the nasty property
471 that adding a type signature changes the dynamic semantics.
474 (let f x = (x::Int) + ?y
475 in (f 3, f 3 with ?y=5)) with ?y = 6
481 in (f 3, f 3 with ?y=5)) with ?y = 6
485 Indeed, simply inlining f (at the Haskell source level) would change the
488 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
489 semantics for a Haskell program without knowing its typing, so if you
490 change the typing you may change the semantics.
492 To make things consistent in all cases where we are *checking* against
493 a supplied signature (as opposed to inferring a type), we adopt the
496 a signature does not need to quantify over implicit params.
498 [This represents a (rather marginal) change of policy since GHC 5.02,
499 which *required* an explicit signature to quantify over all implicit
500 params for the reasons mentioned above.]
502 But that raises a new question. Consider
504 Given (signature) ?x::Int
505 Wanted (inferred) ?x::Int, ?y::Bool
507 Clearly we want to discharge the ?x and float the ?y out. But
508 what is the criterion that distinguishes them? Clearly it isn't
509 what free type variables they have. The Right Thing seems to be
510 to float a constraint that
511 neither mentions any of the quantified type variables
512 nor any of the quantified implicit parameters
514 See the predicate isFreeWhenChecking.
517 Question 3: monomorphism
518 ~~~~~~~~~~~~~~~~~~~~~~~~
519 There's a nasty corner case when the monomorphism restriction bites:
523 The argument above suggests that we *must* generalise
524 over the ?y parameter, to get
525 z :: (?y::Int) => Int,
526 but the monomorphism restriction says that we *must not*, giving
528 Why does the momomorphism restriction say this? Because if you have
530 let z = x + ?y in z+z
532 you might not expect the addition to be done twice --- but it will if
533 we follow the argument of Question 2 and generalise over ?y.
536 Question 4: top level
537 ~~~~~~~~~~~~~~~~~~~~~
538 At the top level, monomorhism makes no sense at all.
541 main = let ?x = 5 in print foo
545 woggle :: (?x :: Int) => Int -> Int
548 We definitely don't want (foo :: Int) with a top-level implicit parameter
549 (?x::Int) becuase there is no way to bind it.
554 (A) Always generalise over implicit parameters
555 Bindings that fall under the monomorphism restriction can't
559 * Inlining remains valid
560 * No unexpected loss of sharing
561 * But simple bindings like
563 will be rejected, unless you add an explicit type signature
564 (to avoid the monomorphism restriction)
565 z :: (?y::Int) => Int
567 This seems unacceptable
569 (B) Monomorphism restriction "wins"
570 Bindings that fall under the monomorphism restriction can't
572 Always generalise over implicit parameters *except* for bindings
573 that fall under the monomorphism restriction
576 * Inlining isn't valid in general
577 * No unexpected loss of sharing
578 * Simple bindings like
580 accepted (get value of ?y from binding site)
582 (C) Always generalise over implicit parameters
583 Bindings that fall under the monomorphism restriction can't
584 be generalised, EXCEPT for implicit parameters
586 * Inlining remains valid
587 * Unexpected loss of sharing (from the extra generalisation)
588 * Simple bindings like
590 accepted (get value of ?y from occurrence sites)
595 None of these choices seems very satisfactory. But at least we should
596 decide which we want to do.
598 It's really not clear what is the Right Thing To Do. If you see
602 would you expect the value of ?y to be got from the *occurrence sites*
603 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
604 case of function definitions, the answer is clearly the former, but
605 less so in the case of non-fucntion definitions. On the other hand,
606 if we say that we get the value of ?y from the definition site of 'z',
607 then inlining 'z' might change the semantics of the program.
609 Choice (C) really says "the monomorphism restriction doesn't apply
610 to implicit parameters". Which is fine, but remember that every
611 innocent binding 'x = ...' that mentions an implicit parameter in
612 the RHS becomes a *function* of that parameter, called at each
613 use of 'x'. Now, the chances are that there are no intervening 'with'
614 clauses that bind ?y, so a decent compiler should common up all
615 those function calls. So I think I strongly favour (C). Indeed,
616 one could make a similar argument for abolishing the monomorphism
617 restriction altogether.
619 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
623 %************************************************************************
625 \subsection{tcSimplifyInfer}
627 %************************************************************************
629 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
631 1. Compute Q = grow( fvs(T), C )
633 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
634 predicates will end up in Ct; we deal with them at the top level
636 3. Try improvement, using functional dependencies
638 4. If Step 3 did any unification, repeat from step 1
639 (Unification can change the result of 'grow'.)
641 Note: we don't reduce dictionaries in step 2. For example, if we have
642 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
643 after step 2. However note that we may therefore quantify over more
644 type variables than we absolutely have to.
646 For the guts, we need a loop, that alternates context reduction and
647 improvement with unification. E.g. Suppose we have
649 class C x y | x->y where ...
651 and tcSimplify is called with:
653 Then improvement unifies a with b, giving
656 If we need to unify anything, we rattle round the whole thing all over
663 -> TcTyVarSet -- fv(T); type vars
665 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
666 TcDictBinds, -- Bindings
667 [TcId]) -- Dict Ids that must be bound here (zonked)
668 -- Any free (escaping) Insts are tossed into the environment
673 tcSimplifyInfer doc tau_tvs wanted_lie
674 = inferLoop doc (varSetElems tau_tvs)
675 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
677 extendLIEs frees `thenM_`
678 returnM (qtvs, binds, map instToId irreds)
680 inferLoop doc tau_tvs wanteds
682 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
683 mappM zonkInst wanteds `thenM` \ wanteds' ->
684 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
686 preds = fdPredsOfInsts wanteds'
687 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
690 | isFreeWhenInferring qtvs inst = Free
691 | isClassDict inst = DontReduceUnlessConstant -- Dicts
692 | otherwise = ReduceMe NoSCs -- Lits and Methods
694 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
695 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
697 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
700 if no_improvement then
701 returnM (varSetElems qtvs, frees, binds, irreds)
703 -- If improvement did some unification, we go round again. There
704 -- are two subtleties:
705 -- a) We start again with irreds, not wanteds
706 -- Using an instance decl might have introduced a fresh type variable
707 -- which might have been unified, so we'd get an infinite loop
708 -- if we started again with wanteds! See example [LOOP]
710 -- b) It's also essential to re-process frees, because unification
711 -- might mean that a type variable that looked free isn't now.
713 -- Hence the (irreds ++ frees)
715 -- However, NOTICE that when we are done, we might have some bindings, but
716 -- the final qtvs might be empty. See [NO TYVARS] below.
718 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
719 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
724 class If b t e r | b t e -> r
727 class Lte a b c | a b -> c where lte :: a -> b -> c
729 instance (Lte a b l,If l b a c) => Max a b c
731 Wanted: Max Z (S x) y
733 Then we'll reduce using the Max instance to:
734 (Lte Z (S x) l, If l (S x) Z y)
735 and improve by binding l->T, after which we can do some reduction
736 on both the Lte and If constraints. What we *can't* do is start again
737 with (Max Z (S x) y)!
741 class Y a b | a -> b where
744 instance Y [[a]] a where
747 k :: X a -> X a -> X a
749 g :: Num a => [X a] -> [X a]
752 h ys = ys ++ map (k (y [[0]])) xs
754 The excitement comes when simplifying the bindings for h. Initially
755 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
756 From this we get t1:=:t2, but also various bindings. We can't forget
757 the bindings (because of [LOOP]), but in fact t1 is what g is
760 The net effect of [NO TYVARS]
763 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
764 isFreeWhenInferring qtvs inst
765 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
766 && isInheritableInst inst -- And no implicit parameter involved
767 -- (see "Notes on implicit parameters")
769 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
770 -> NameSet -- Quantified implicit parameters
772 isFreeWhenChecking qtvs ips inst
773 = isFreeWrtTyVars qtvs inst
774 && isFreeWrtIPs ips inst
776 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
777 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
781 %************************************************************************
783 \subsection{tcSimplifyCheck}
785 %************************************************************************
787 @tcSimplifyCheck@ is used when we know exactly the set of variables
788 we are going to quantify over. For example, a class or instance declaration.
793 -> [TcTyVar] -- Quantify over these
796 -> TcM TcDictBinds -- Bindings
798 -- tcSimplifyCheck is used when checking expression type signatures,
799 -- class decls, instance decls etc.
801 -- NB: tcSimplifyCheck does not consult the
802 -- global type variables in the environment; so you don't
803 -- need to worry about setting them before calling tcSimplifyCheck
804 tcSimplifyCheck doc qtvs givens wanted_lie
805 = ASSERT( all isSkolemTyVar qtvs )
806 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
810 -- get_qtvs = zonkTcTyVarsAndFV qtvs
811 get_qtvs = return (mkVarSet qtvs) -- All skolems
814 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
815 -- against, but we don't know the type variables over which we are going to quantify.
816 -- This happens when we have a type signature for a mutually recursive group
819 -> TcTyVarSet -- fv(T)
822 -> TcM ([TcTyVar], -- Variables over which to quantify
823 TcDictBinds) -- Bindings
825 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
826 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
828 ; return (qtvs', binds) }
830 -- Figure out which type variables to quantify over
831 -- You might think it should just be the signature tyvars,
832 -- but in bizarre cases you can get extra ones
833 -- f :: forall a. Num a => a -> a
834 -- f x = fst (g (x, head [])) + 1
836 -- Here we infer g :: forall a b. a -> b -> (b,a)
837 -- We don't want g to be monomorphic in b just because
838 -- f isn't quantified over b.
839 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
841 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
842 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
844 qtvs = all_tvs' `minusVarSet` gbl_tvs
845 -- We could close gbl_tvs, but its not necessary for
846 -- soundness, and it'll only affect which tyvars, not which
847 -- dictionaries, we quantify over
852 Here is the workhorse function for all three wrappers.
855 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
856 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
858 -- Complain about any irreducible ones
859 ; if not (null irreds)
860 then do { givens' <- mappM zonkInst given_dicts_and_ips
861 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
864 ; returnM (qtvs, frees, binds) }
866 given_dicts_and_ips = filter (not . isMethod) givens
867 -- For error reporting, filter out methods, which are
868 -- only added to the given set as an optimisation
870 ip_set = mkNameSet (ipNamesOfInsts givens)
872 check_loop givens wanteds
874 mappM zonkInst givens `thenM` \ givens' ->
875 mappM zonkInst wanteds `thenM` \ wanteds' ->
876 get_qtvs `thenM` \ qtvs' ->
880 -- When checking against a given signature we always reduce
881 -- until we find a match against something given, or can't reduce
882 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
883 | otherwise = ReduceMe want_scs
885 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
888 if no_improvement then
889 returnM (varSetElems qtvs', frees, binds, irreds)
891 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
892 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
896 %************************************************************************
898 tcSimplifySuperClasses
900 %************************************************************************
902 Note [SUPERCLASS-LOOP 1]
903 ~~~~~~~~~~~~~~~~~~~~~~~~
904 We have to be very, very careful when generating superclasses, lest we
905 accidentally build a loop. Here's an example:
909 class S a => C a where { opc :: a -> a }
910 class S b => D b where { opd :: b -> b }
918 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
919 Simplifying, we may well get:
920 $dfCInt = :C ds1 (opd dd)
923 Notice that we spot that we can extract ds1 from dd.
925 Alas! Alack! We can do the same for (instance D Int):
927 $dfDInt = :D ds2 (opc dc)
931 And now we've defined the superclass in terms of itself.
933 Solution: never generate a superclass selectors at all when
934 satisfying the superclass context of an instance declaration.
936 Two more nasty cases are in
941 tcSimplifySuperClasses qtvs givens sc_wanteds
942 = ASSERT( all isSkolemTyVar qtvs )
943 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
944 ; ext_default <- doptM Opt_ExtendedDefaultRules
945 ; binds2 <- tc_simplify_top doc ext_default NoSCs frees
946 ; return (binds1 `unionBags` binds2) }
948 get_qtvs = return (mkVarSet qtvs)
949 doc = ptext SLIT("instance declaration superclass context")
953 %************************************************************************
955 \subsection{tcSimplifyRestricted}
957 %************************************************************************
959 tcSimplifyRestricted infers which type variables to quantify for a
960 group of restricted bindings. This isn't trivial.
963 We want to quantify over a to get id :: forall a. a->a
966 We do not want to quantify over a, because there's an Eq a
967 constraint, so we get eq :: a->a->Bool (notice no forall)
970 RHS has type 'tau', whose free tyvars are tau_tvs
971 RHS has constraints 'wanteds'
974 Quantify over (tau_tvs \ ftvs(wanteds))
975 This is bad. The constraints may contain (Monad (ST s))
976 where we have instance Monad (ST s) where...
977 so there's no need to be monomorphic in s!
979 Also the constraint might be a method constraint,
980 whose type mentions a perfectly innocent tyvar:
981 op :: Num a => a -> b -> a
982 Here, b is unconstrained. A good example would be
984 We want to infer the polymorphic type
985 foo :: forall b. b -> b
988 Plan B (cunning, used for a long time up to and including GHC 6.2)
989 Step 1: Simplify the constraints as much as possible (to deal
990 with Plan A's problem). Then set
991 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
993 Step 2: Now simplify again, treating the constraint as 'free' if
994 it does not mention qtvs, and trying to reduce it otherwise.
995 The reasons for this is to maximise sharing.
997 This fails for a very subtle reason. Suppose that in the Step 2
998 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
999 In the Step 1 this constraint might have been simplified, perhaps to
1000 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
1001 This won't happen in Step 2... but that in turn might prevent some other
1002 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
1003 and that in turn breaks the invariant that no constraints are quantified over.
1005 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
1010 Step 1: Simplify the constraints as much as possible (to deal
1011 with Plan A's problem). Then set
1012 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1013 Return the bindings from Step 1.
1016 A note about Plan C (arising from "bug" reported by George Russel March 2004)
1019 instance (HasBinary ty IO) => HasCodedValue ty
1021 foo :: HasCodedValue a => String -> IO a
1023 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1024 doDecodeIO codedValue view
1025 = let { act = foo "foo" } in act
1027 You might think this should work becuase the call to foo gives rise to a constraint
1028 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1029 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1030 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1032 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1036 Plan D (a variant of plan B)
1037 Step 1: Simplify the constraints as much as possible (to deal
1038 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1039 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1041 Step 2: Now simplify again, treating the constraint as 'free' if
1042 it does not mention qtvs, and trying to reduce it otherwise.
1044 The point here is that it's generally OK to have too few qtvs; that is,
1045 to make the thing more monomorphic than it could be. We don't want to
1046 do that in the common cases, but in wierd cases it's ok: the programmer
1047 can always add a signature.
1049 Too few qtvs => too many wanteds, which is what happens if you do less
1054 tcSimplifyRestricted -- Used for restricted binding groups
1055 -- i.e. ones subject to the monomorphism restriction
1058 -> [Name] -- Things bound in this group
1059 -> TcTyVarSet -- Free in the type of the RHSs
1060 -> [Inst] -- Free in the RHSs
1061 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1062 TcDictBinds) -- Bindings
1063 -- tcSimpifyRestricted returns no constraints to
1064 -- quantify over; by definition there are none.
1065 -- They are all thrown back in the LIE
1067 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1068 -- Zonk everything in sight
1069 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1071 -- 'reduceMe': Reduce as far as we can. Don't stop at
1072 -- dicts; the idea is to get rid of as many type
1073 -- variables as possible, and we don't want to stop
1074 -- at (say) Monad (ST s), because that reduces
1075 -- immediately, with no constraint on s.
1077 -- BUT do no improvement! See Plan D above
1078 -- HOWEVER, some unification may take place, if we instantiate
1079 -- a method Inst with an equality constraint
1080 reduceContextWithoutImprovement
1081 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1083 -- Next, figure out the tyvars we will quantify over
1084 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1085 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1086 mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' ->
1088 constrained_tvs' = tyVarsOfInsts constrained_dicts'
1089 qtvs' = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1090 `minusVarSet` constrained_tvs'
1092 traceTc (text "tcSimplifyRestricted" <+> vcat [
1093 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts',
1095 ppr constrained_tvs', ppr tau_tvs', ppr qtvs' ]) `thenM_`
1097 -- The first step may have squashed more methods than
1098 -- necessary, so try again, this time more gently, knowing the exact
1099 -- set of type variables to quantify over.
1101 -- We quantify only over constraints that are captured by qtvs';
1102 -- these will just be a subset of non-dicts. This in contrast
1103 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1104 -- all *non-inheritable* constraints too. This implements choice
1105 -- (B) under "implicit parameter and monomorphism" above.
1107 -- Remember that we may need to do *some* simplification, to
1108 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1109 -- just to float all constraints
1111 -- At top level, we *do* squash methods becuase we want to
1112 -- expose implicit parameters to the test that follows
1114 is_nested_group = isNotTopLevel top_lvl
1115 try_me inst | isFreeWrtTyVars qtvs' inst,
1116 (is_nested_group || isDict inst) = Free
1117 | otherwise = ReduceMe AddSCs
1119 reduceContextWithoutImprovement
1120 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1121 ASSERT( null irreds )
1123 -- See "Notes on implicit parameters, Question 4: top level"
1124 if is_nested_group then
1125 extendLIEs frees `thenM_`
1126 returnM (varSetElems qtvs', binds)
1129 (non_ips, bad_ips) = partition isClassDict frees
1131 addTopIPErrs bndrs bad_ips `thenM_`
1132 extendLIEs non_ips `thenM_`
1133 returnM (varSetElems qtvs', binds)
1137 %************************************************************************
1141 %************************************************************************
1143 On the LHS of transformation rules we only simplify methods and constants,
1144 getting dictionaries. We want to keep all of them unsimplified, to serve
1145 as the available stuff for the RHS of the rule.
1147 Example. Consider the following left-hand side of a rule
1149 f (x == y) (y > z) = ...
1151 If we typecheck this expression we get constraints
1153 d1 :: Ord a, d2 :: Eq a
1155 We do NOT want to "simplify" to the LHS
1157 forall x::a, y::a, z::a, d1::Ord a.
1158 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1162 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1163 f ((==) d2 x y) ((>) d1 y z) = ...
1165 Here is another example:
1167 fromIntegral :: (Integral a, Num b) => a -> b
1168 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1170 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1171 we *dont* want to get
1173 forall dIntegralInt.
1174 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1176 because the scsel will mess up RULE matching. Instead we want
1178 forall dIntegralInt, dNumInt.
1179 fromIntegral Int Int dIntegralInt dNumInt = id Int
1183 g (x == y) (y == z) = ..
1185 where the two dictionaries are *identical*, we do NOT WANT
1187 forall x::a, y::a, z::a, d1::Eq a
1188 f ((==) d1 x y) ((>) d1 y z) = ...
1190 because that will only match if the dict args are (visibly) equal.
1191 Instead we want to quantify over the dictionaries separately.
1193 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1194 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1195 from scratch, rather than further parameterise simpleReduceLoop etc
1198 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1199 tcSimplifyRuleLhs wanteds
1200 = go [] emptyBag wanteds
1203 = return (dicts, binds)
1204 go dicts binds (w:ws)
1206 = go (w:dicts) binds ws
1208 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1209 -- to fromInteger; this looks fragile to me
1210 ; lookup_result <- lookupInst w'
1211 ; case lookup_result of
1212 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
1213 SimpleInst rhs -> go dicts (addBind binds w rhs) ws
1214 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1218 tcSimplifyBracket is used when simplifying the constraints arising from
1219 a Template Haskell bracket [| ... |]. We want to check that there aren't
1220 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1221 Show instance), but we aren't otherwise interested in the results.
1222 Nor do we care about ambiguous dictionaries etc. We will type check
1223 this bracket again at its usage site.
1226 tcSimplifyBracket :: [Inst] -> TcM ()
1227 tcSimplifyBracket wanteds
1228 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1231 doc = text "tcSimplifyBracket"
1235 %************************************************************************
1237 \subsection{Filtering at a dynamic binding}
1239 %************************************************************************
1244 we must discharge all the ?x constraints from B. We also do an improvement
1245 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1247 Actually, the constraints from B might improve the types in ?x. For example
1249 f :: (?x::Int) => Char -> Char
1252 then the constraint (?x::Int) arising from the call to f will
1253 force the binding for ?x to be of type Int.
1256 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1259 tcSimplifyIPs given_ips wanteds
1260 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1261 extendLIEs frees `thenM_`
1264 doc = text "tcSimplifyIPs" <+> ppr given_ips
1265 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1267 -- Simplify any methods that mention the implicit parameter
1268 try_me inst | isFreeWrtIPs ip_set inst = Free
1269 | otherwise = ReduceMe NoSCs
1271 simpl_loop givens wanteds
1272 = mappM zonkInst givens `thenM` \ givens' ->
1273 mappM zonkInst wanteds `thenM` \ wanteds' ->
1275 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1277 if no_improvement then
1278 ASSERT( null irreds )
1279 returnM (frees, binds)
1281 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1282 returnM (frees1, binds `unionBags` binds1)
1286 %************************************************************************
1288 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1290 %************************************************************************
1292 When doing a binding group, we may have @Insts@ of local functions.
1293 For example, we might have...
1295 let f x = x + 1 -- orig local function (overloaded)
1296 f.1 = f Int -- two instances of f
1301 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1302 where @f@ is in scope; those @Insts@ must certainly not be passed
1303 upwards towards the top-level. If the @Insts@ were binding-ified up
1304 there, they would have unresolvable references to @f@.
1306 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1307 For each method @Inst@ in the @init_lie@ that mentions one of the
1308 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1309 @LIE@), as well as the @HsBinds@ generated.
1312 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1313 -- Simlifies only MethodInsts, and generate only bindings of form
1315 -- We're careful not to even generate bindings of the form
1317 -- You'd think that'd be fine, but it interacts with what is
1318 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1320 bindInstsOfLocalFuns wanteds local_ids
1321 | null overloaded_ids
1323 = extendLIEs wanteds `thenM_`
1324 returnM emptyLHsBinds
1327 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1328 ASSERT( null irreds )
1329 extendLIEs not_for_me `thenM_`
1330 extendLIEs frees `thenM_`
1333 doc = text "bindInsts" <+> ppr local_ids
1334 overloaded_ids = filter is_overloaded local_ids
1335 is_overloaded id = isOverloadedTy (idType id)
1336 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1338 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1339 -- so it's worth building a set, so that
1340 -- lookup (in isMethodFor) is faster
1341 try_me inst | isMethod inst = ReduceMe NoSCs
1346 %************************************************************************
1348 \subsection{Data types for the reduction mechanism}
1350 %************************************************************************
1352 The main control over context reduction is here
1356 = ReduceMe WantSCs -- Try to reduce this
1357 -- If there's no instance, behave exactly like
1358 -- DontReduce: add the inst to the irreductible ones,
1359 -- but don't produce an error message of any kind.
1360 -- It might be quite legitimate such as (Eq a)!
1362 | DontReduceUnlessConstant -- Return as irreducible unless it can
1363 -- be reduced to a constant in one step
1365 | Free -- Return as free
1367 reduceMe :: Inst -> WhatToDo
1368 reduceMe inst = ReduceMe AddSCs
1370 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1371 -- of a predicate when adding it to the avails
1372 -- The reason for this flag is entirely the super-class loop problem
1373 -- Note [SUPER-CLASS LOOP 1]
1379 type Avails = FiniteMap Inst Avail
1380 emptyAvails = emptyFM
1383 = IsFree -- Used for free Insts
1384 | Irred -- Used for irreducible dictionaries,
1385 -- which are going to be lambda bound
1387 | Given TcId -- Used for dictionaries for which we have a binding
1388 -- e.g. those "given" in a signature
1389 Bool -- True <=> actually consumed (splittable IPs only)
1391 | Rhs -- Used when there is a RHS
1392 (LHsExpr TcId) -- The RHS
1393 [Inst] -- Insts free in the RHS; we need these too
1395 | Linear -- Splittable Insts only.
1396 Int -- The Int is always 2 or more; indicates how
1397 -- many copies are required
1398 Inst -- The splitter
1399 Avail -- Where the "master copy" is
1401 | LinRhss -- Splittable Insts only; this is used only internally
1402 -- by extractResults, where a Linear
1403 -- is turned into an LinRhss
1404 [LHsExpr TcId] -- A supply of suitable RHSs
1406 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1407 | (inst,avail) <- fmToList avails ]
1409 instance Outputable Avail where
1412 pprAvail IsFree = text "Free"
1413 pprAvail Irred = text "Irred"
1414 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1415 if b then text "(used)" else empty
1416 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1417 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1418 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1421 Extracting the bindings from a bunch of Avails.
1422 The bindings do *not* come back sorted in dependency order.
1423 We assume that they'll be wrapped in a big Rec, so that the
1424 dependency analyser can sort them out later
1428 extractResults :: Avails
1430 -> TcM (TcDictBinds, -- Bindings
1431 [Inst], -- Irreducible ones
1432 [Inst]) -- Free ones
1434 extractResults avails wanteds
1435 = go avails emptyBag [] [] wanteds
1437 go avails binds irreds frees []
1438 = returnM (binds, irreds, frees)
1440 go avails binds irreds frees (w:ws)
1441 = case lookupFM avails w of
1442 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1443 go avails binds irreds frees ws
1445 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1446 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1448 Just (Given id _) -> go avails new_binds irreds frees ws
1450 new_binds | id == instToId w = binds
1451 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1452 -- The sought Id can be one of the givens, via a superclass chain
1453 -- and then we definitely don't want to generate an x=x binding!
1455 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1457 new_binds = addBind binds w rhs
1459 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1460 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1461 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1462 go (addToFM avails w (LinRhss rhss))
1463 (binds `unionBags` binds')
1464 irreds' frees' (split_inst : w : ws)
1466 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1467 -> go new_avails new_binds irreds frees ws
1469 new_binds = addBind binds w rhs
1470 new_avails = addToFM avails w (LinRhss rhss)
1472 -- get_root is just used for Linear
1473 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1474 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1475 returnM (w':irreds, frees, instToId w')
1476 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1477 returnM (irreds, w':frees, instToId w')
1479 add_given avails w = addToFM avails w (Given (instToId w) True)
1481 add_free avails w | isMethod w = avails
1482 | otherwise = add_given avails w
1484 -- Do *not* replace Free by Given if it's a method.
1485 -- The following situation shows why this is bad:
1486 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1487 -- From an application (truncate f i) we get
1488 -- t1 = truncate at f
1490 -- If we have also have a second occurrence of truncate, we get
1491 -- t3 = truncate at f
1493 -- When simplifying with i,f free, we might still notice that
1494 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1495 -- will continue to float out!
1497 split :: Int -> TcId -> TcId -> Inst
1498 -> TcM (TcDictBinds, [LHsExpr TcId])
1499 -- (split n split_id root_id wanted) returns
1500 -- * a list of 'n' expressions, all of which witness 'avail'
1501 -- * a bunch of auxiliary bindings to support these expressions
1502 -- * one or zero insts needed to witness the whole lot
1503 -- (maybe be zero if the initial Inst is a Given)
1505 -- NB: 'wanted' is just a template
1507 split n split_id root_id wanted
1510 ty = linearInstType wanted
1511 pair_ty = mkTyConApp pairTyCon [ty,ty]
1512 id = instToId wanted
1515 span = instSpan wanted
1517 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1519 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1520 expand n rhss `thenM` \ (binds2, rhss') ->
1521 returnM (binds1 `unionBags` binds2, rhss')
1524 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1525 -- e.g. expand 3 [rhs1, rhs2]
1526 -- = ( { x = split rhs1 },
1527 -- [fst x, snd x, rhs2] )
1529 | n `rem` 2 == 0 = go rhss -- n is even
1530 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1531 returnM (binds', head rhss : rhss')
1533 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1534 returnM (listToBag binds', concat rhss')
1536 do_one rhs = newUnique `thenM` \ uniq ->
1537 tcLookupId fstName `thenM` \ fst_id ->
1538 tcLookupId sndName `thenM` \ snd_id ->
1540 x = mkUserLocal occ uniq pair_ty loc
1542 returnM (L span (VarBind x (mk_app span split_id rhs)),
1543 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1545 mk_fs_app span id ty var = nlHsTyApp id [ty,ty] `mkHsApp` (L span (HsVar var))
1547 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1549 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1550 (VarBind (instToId inst) rhs))
1551 instSpan wanted = instLocSrcSpan (instLoc wanted)
1555 %************************************************************************
1557 \subsection[reduce]{@reduce@}
1559 %************************************************************************
1561 When the "what to do" predicate doesn't depend on the quantified type variables,
1562 matters are easier. We don't need to do any zonking, unless the improvement step
1563 does something, in which case we zonk before iterating.
1565 The "given" set is always empty.
1568 simpleReduceLoop :: SDoc
1569 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1571 -> TcM ([Inst], -- Free
1573 [Inst]) -- Irreducible
1575 simpleReduceLoop doc try_me wanteds
1576 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1577 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1578 if no_improvement then
1579 returnM (frees, binds, irreds)
1581 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1582 returnM (frees1, binds `unionBags` binds1, irreds1)
1588 reduceContext :: SDoc
1589 -> (Inst -> WhatToDo)
1592 -> TcM (Bool, -- True <=> improve step did no unification
1594 TcDictBinds, -- Dictionary bindings
1595 [Inst]) -- Irreducible
1597 reduceContext doc try_me givens wanteds
1599 traceTc (text "reduceContext" <+> (vcat [
1600 text "----------------------",
1602 text "given" <+> ppr givens,
1603 text "wanted" <+> ppr wanteds,
1604 text "----------------------"
1607 -- Build the Avail mapping from "givens"
1608 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1611 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1613 -- Do improvement, using everything in avails
1614 -- In particular, avails includes all superclasses of everything
1615 tcImprove avails `thenM` \ no_improvement ->
1617 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1619 traceTc (text "reduceContext end" <+> (vcat [
1620 text "----------------------",
1622 text "given" <+> ppr givens,
1623 text "wanted" <+> ppr wanteds,
1625 text "avails" <+> pprAvails avails,
1626 text "frees" <+> ppr frees,
1627 text "no_improvement =" <+> ppr no_improvement,
1628 text "----------------------"
1631 returnM (no_improvement, frees, binds, irreds)
1633 -- reduceContextWithoutImprovement differs from reduceContext
1634 -- (a) no improvement
1635 -- (b) 'givens' is assumed empty
1636 reduceContextWithoutImprovement doc try_me wanteds
1638 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1639 text "----------------------",
1641 text "wanted" <+> ppr wanteds,
1642 text "----------------------"
1646 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1647 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1649 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1650 text "----------------------",
1652 text "wanted" <+> ppr wanteds,
1654 text "avails" <+> pprAvails avails,
1655 text "frees" <+> ppr frees,
1656 text "----------------------"
1659 returnM (frees, binds, irreds)
1661 tcImprove :: Avails -> TcM Bool -- False <=> no change
1662 -- Perform improvement using all the predicates in Avails
1664 = tcGetInstEnvs `thenM` \ inst_envs ->
1666 preds = [ (pred, pp_loc)
1667 | (inst, avail) <- fmToList avails,
1668 pred <- get_preds inst avail,
1669 let pp_loc = pprInstLoc (instLoc inst)
1671 -- Avails has all the superclasses etc (good)
1672 -- It also has all the intermediates of the deduction (good)
1673 -- It does not have duplicates (good)
1674 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1675 -- so that improve will see them separate
1677 -- For free Methods, we want to take predicates from their context,
1678 -- but for Methods that have been squished their context will already
1679 -- be in Avails, and we don't want duplicates. Hence this rather
1680 -- horrid get_preds function
1681 get_preds inst IsFree = fdPredsOfInst inst
1682 get_preds inst other | isDict inst = [dictPred inst]
1685 eqns = improve get_insts preds
1686 get_insts clas = classInstances inst_envs clas
1691 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1692 mappM_ unify eqns `thenM_`
1695 unify ((qtvs, pairs), what1, what2)
1696 = addErrCtxtM (mkEqnMsg what1 what2) $
1697 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1698 mapM_ (unif_pr tenv) pairs
1699 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1701 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1703 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1704 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1705 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1706 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1707 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1708 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1709 ; return (tidy_env, msg) }
1712 The main context-reduction function is @reduce@. Here's its game plan.
1715 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1716 -- along with its depth
1717 -> (Inst -> WhatToDo)
1724 try_me: given an inst, this function returns
1726 DontReduce return this in "irreds"
1727 Free return this in "frees"
1729 wanteds: The list of insts to reduce
1730 state: An accumulating parameter of type Avails
1731 that contains the state of the algorithm
1733 It returns a Avails.
1735 The (n,stack) pair is just used for error reporting.
1736 n is always the depth of the stack.
1737 The stack is the stack of Insts being reduced: to produce X
1738 I had to produce Y, to produce Y I had to produce Z, and so on.
1741 reduceList (n,stack) try_me wanteds state
1742 = do { dopts <- getDOpts
1745 dumpTcRn (text "Interesting! Context reduction stack deeper than 8:"
1746 <+> (int n $$ ifPprDebug (nest 2 (pprStack stack))))
1749 ; if n >= ctxtStkDepth dopts then
1750 failWithTc (reduceDepthErr n stack)
1754 go [] state = return state
1755 go (w:ws) state = do { state' <- reduce (n+1, w:stack) try_me w state
1758 -- Base case: we're done!
1759 reduce stack try_me wanted avails
1760 -- It's the same as an existing inst, or a superclass thereof
1761 | Just avail <- isAvailable avails wanted
1762 = if isLinearInst wanted then
1763 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1764 reduceList stack try_me wanteds' avails'
1766 returnM avails -- No op for non-linear things
1769 = case try_me wanted of {
1771 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1772 -- First, see if the inst can be reduced to a constant in one step
1773 try_simple (addIrred AddSCs) -- Assume want superclasses
1775 ; Free -> -- It's free so just chuck it upstairs
1776 -- First, see if the inst can be reduced to a constant in one step
1779 ; ReduceMe want_scs -> -- It should be reduced
1780 lookupInst wanted `thenM` \ lookup_result ->
1781 case lookup_result of
1782 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1783 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1784 addWanted want_scs avails2 wanted rhs wanteds'
1785 -- Experiment with temporarily doing addIrred *before* the reduceList,
1786 -- which has the effect of adding the thing we are trying
1787 -- to prove to the database before trying to prove the things it
1788 -- needs. See note [RECURSIVE DICTIONARIES]
1789 -- NB: we must not do an addWanted before, because that adds the
1790 -- superclasses too, and thaat can lead to a spurious loop; see
1791 -- the examples in [SUPERCLASS-LOOP]
1792 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1794 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1796 NoInstance -> -- No such instance!
1797 -- Add it and its superclasses
1798 addIrred want_scs avails wanted
1801 try_simple do_this_otherwise
1802 = lookupInst wanted `thenM` \ lookup_result ->
1803 case lookup_result of
1804 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1805 other -> do_this_otherwise avails wanted
1810 -------------------------
1811 isAvailable :: Avails -> Inst -> Maybe Avail
1812 isAvailable avails wanted = lookupFM avails wanted
1813 -- NB 1: the Ord instance of Inst compares by the class/type info
1814 -- *not* by unique. So
1815 -- d1::C Int == d2::C Int
1817 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1818 addLinearAvailable avails avail wanted
1819 -- avails currently maps [wanted -> avail]
1820 -- Extend avails to reflect a neeed for an extra copy of avail
1822 | Just avail' <- split_avail avail
1823 = returnM (addToFM avails wanted avail', [])
1826 = tcLookupId splitName `thenM` \ split_id ->
1827 tcInstClassOp (instLoc wanted) split_id
1828 [linearInstType wanted] `thenM` \ split_inst ->
1829 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1832 split_avail :: Avail -> Maybe Avail
1833 -- (Just av) if there's a modified version of avail that
1834 -- we can use to replace avail in avails
1835 -- Nothing if there isn't, so we need to create a Linear
1836 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1837 split_avail (Given id used) | not used = Just (Given id True)
1838 | otherwise = Nothing
1839 split_avail Irred = Nothing
1840 split_avail IsFree = Nothing
1841 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1843 -------------------------
1844 addFree :: Avails -> Inst -> TcM Avails
1845 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1846 -- to avails, so that any other equal Insts will be commoned up right
1847 -- here rather than also being tossed upstairs. This is really just
1848 -- an optimisation, and perhaps it is more trouble that it is worth,
1849 -- as the following comments show!
1851 -- NB: do *not* add superclasses. If we have
1854 -- but a is not bound here, then we *don't* want to derive
1855 -- dn from df here lest we lose sharing.
1857 addFree avails free = returnM (addToFM avails free IsFree)
1859 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1860 addWanted want_scs avails wanted rhs_expr wanteds
1861 = addAvailAndSCs want_scs avails wanted avail
1863 avail = Rhs rhs_expr wanteds
1865 addGiven :: Avails -> Inst -> TcM Avails
1866 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1867 -- Always add superclasses for 'givens'
1869 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1870 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1871 -- so the assert isn't true
1873 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1874 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1875 addAvailAndSCs want_scs avails irred Irred
1877 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1878 addAvailAndSCs want_scs avails inst avail
1879 | not (isClassDict inst) = return avails_with_inst
1880 | NoSCs <- want_scs = return avails_with_inst
1881 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1882 ; addSCs is_loop avails_with_inst inst }
1884 avails_with_inst = addToFM avails inst avail
1886 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1887 -- Note: this compares by *type*, not by Unique
1888 deps = findAllDeps (unitVarSet (instToId inst)) avail
1889 dep_tys = map idType (varSetElems deps)
1891 findAllDeps :: IdSet -> Avail -> IdSet
1892 -- Find all the Insts that this one depends on
1893 -- See Note [SUPERCLASS-LOOP 2]
1894 -- Watch out, though. Since the avails may contain loops
1895 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1896 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1897 findAllDeps so_far other = so_far
1899 find_all :: IdSet -> Inst -> IdSet
1901 | kid_id `elemVarSet` so_far = so_far
1902 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1903 | otherwise = so_far'
1905 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1906 kid_id = instToId kid
1908 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1909 -- Add all the superclasses of the Inst to Avails
1910 -- The first param says "dont do this because the original thing
1911 -- depends on this one, so you'd build a loop"
1912 -- Invariant: the Inst is already in Avails.
1914 addSCs is_loop avails dict
1915 = do { sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
1916 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1918 (clas, tys) = getDictClassTys dict
1919 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1920 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1922 add_sc avails (sc_dict, sc_sel)
1923 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1924 | is_given sc_dict = return avails
1925 | otherwise = addSCs is_loop avails' sc_dict
1927 sc_sel_rhs = L (instSpan dict) (HsCoerce co_fn (HsVar sc_sel))
1928 co_fn = CoApp (instToId dict) <.> mkCoTyApps tys
1929 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1931 is_given :: Inst -> Bool
1932 is_given sc_dict = case lookupFM avails sc_dict of
1933 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1937 Note [SUPERCLASS-LOOP 2]
1938 ~~~~~~~~~~~~~~~~~~~~~~~~
1939 But the above isn't enough. Suppose we are *given* d1:Ord a,
1940 and want to deduce (d2:C [a]) where
1942 class Ord a => C a where
1943 instance Ord [a] => C [a] where ...
1945 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1946 superclasses of C [a] to avails. But we must not overwrite the binding
1947 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1950 Here's another variant, immortalised in tcrun020
1951 class Monad m => C1 m
1952 class C1 m => C2 m x
1953 instance C2 Maybe Bool
1954 For the instance decl we need to build (C1 Maybe), and it's no good if
1955 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1956 before we search for C1 Maybe.
1958 Here's another example
1959 class Eq b => Foo a b
1960 instance Eq a => Foo [a] a
1964 we'll first deduce that it holds (via the instance decl). We must not
1965 then overwrite the Eq t constraint with a superclass selection!
1967 At first I had a gross hack, whereby I simply did not add superclass constraints
1968 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1969 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1970 I found a very obscure program (now tcrun021) in which improvement meant the
1971 simplifier got two bites a the cherry... so something seemed to be an Irred
1972 first time, but reducible next time.
1974 Now we implement the Right Solution, which is to check for loops directly
1975 when adding superclasses. It's a bit like the occurs check in unification.
1978 Note [RECURSIVE DICTIONARIES]
1979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1981 data D r = ZeroD | SuccD (r (D r));
1983 instance (Eq (r (D r))) => Eq (D r) where
1984 ZeroD == ZeroD = True
1985 (SuccD a) == (SuccD b) = a == b
1988 equalDC :: D [] -> D [] -> Bool;
1991 We need to prove (Eq (D [])). Here's how we go:
1995 by instance decl, holds if
1999 by instance decl of Eq, holds if
2001 where d2 = dfEqList d3
2004 But now we can "tie the knot" to give
2010 and it'll even run! The trick is to put the thing we are trying to prove
2011 (in this case Eq (D []) into the database before trying to prove its
2012 contributing clauses.
2015 %************************************************************************
2017 \section{tcSimplifyTop: defaulting}
2019 %************************************************************************
2022 @tcSimplifyTop@ is called once per module to simplify all the constant
2023 and ambiguous Insts.
2025 We need to be careful of one case. Suppose we have
2027 instance Num a => Num (Foo a b) where ...
2029 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2030 to (Num x), and default x to Int. But what about y??
2032 It's OK: the final zonking stage should zap y to (), which is fine.
2036 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2037 tcSimplifyTop wanteds
2038 = do { ext_default <- doptM Opt_ExtendedDefaultRules
2039 ; tc_simplify_top doc ext_default AddSCs wanteds }
2041 doc = text "tcSimplifyTop"
2043 tcSimplifyInteractive wanteds
2044 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2046 doc = text "tcSimplifyTop"
2048 -- The TcLclEnv should be valid here, solely to improve
2049 -- error message generation for the monomorphism restriction
2050 tc_simplify_top doc use_extended_defaulting want_scs wanteds
2051 = do { lcl_env <- getLclEnv
2052 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2054 ; let try_me inst = ReduceMe want_scs
2055 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2058 -- First get rid of implicit parameters
2059 (non_ips, bad_ips) = partition isClassDict irreds
2061 -- All the non-tv or multi-param ones are definite errors
2062 (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
2063 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2065 -- Group by type variable
2066 tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
2068 -- Pick the ones which its worth trying to disambiguate
2069 -- namely, the ones whose type variable isn't bound
2070 -- up with one of the non-tyvar classes
2071 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2072 defaultable_group ds
2073 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
2074 && defaultable_classes (map get_clas ds)
2075 defaultable_classes clss
2076 | use_extended_defaulting = any isInteractiveClass clss
2077 | otherwise = all isStandardClass clss && any isNumericClass clss
2079 isInteractiveClass cls = isNumericClass cls
2080 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2081 -- In interactive mode, or with -fextended-default-rules,
2082 -- we default Show a to Show () to avoid graututious errors on "show []"
2085 -- Collect together all the bad guys
2086 bad_guys = non_tvs ++ concat non_default_gps
2087 (ambigs, no_insts) = partition isTyVarDict bad_guys
2088 -- If the dict has no type constructors involved, it must be ambiguous,
2089 -- except I suppose that another error with fundeps maybe should have
2090 -- constrained those type variables
2092 -- Report definite errors
2093 ; ASSERT( null frees )
2094 groupErrs (addNoInstanceErrs Nothing []) no_insts
2095 ; strangeTopIPErrs bad_ips
2097 -- Deal with ambiguity errors, but only if
2098 -- if there has not been an error so far:
2099 -- errors often give rise to spurious ambiguous Insts.
2101 -- f = (*) -- Monomorphic
2102 -- g :: Num a => a -> a
2104 -- Here, we get a complaint when checking the type signature for g,
2105 -- that g isn't polymorphic enough; but then we get another one when
2106 -- dealing with the (Num a) context arising from f's definition;
2107 -- we try to unify a with Int (to default it), but find that it's
2108 -- already been unified with the rigid variable from g's type sig
2109 ; binds_ambig <- ifErrsM (returnM []) $
2110 do { -- Complain about the ones that don't fall under
2111 -- the Haskell rules for disambiguation
2112 -- This group includes both non-existent instances
2113 -- e.g. Num (IO a) and Eq (Int -> Int)
2114 -- and ambiguous dictionaries
2116 addTopAmbigErrs ambigs
2118 -- Disambiguate the ones that look feasible
2119 ; mappM disambigGroup default_gps }
2121 ; return (binds `unionBags` unionManyBags binds_ambig) }
2123 ----------------------------------
2124 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2126 is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
2127 -- Invariant: argument is a ClassDict, not IP or method
2128 is_unary_tyvar_dict d = case getDictClassTys d of
2129 (_, [ty]) -> tcIsTyVarTy ty
2132 get_tv d = case getDictClassTys d of
2133 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2134 get_clas d = case getDictClassTys d of
2138 If a dictionary constrains a type variable which is
2139 * not mentioned in the environment
2140 * and not mentioned in the type of the expression
2141 then it is ambiguous. No further information will arise to instantiate
2142 the type variable; nor will it be generalised and turned into an extra
2143 parameter to a function.
2145 It is an error for this to occur, except that Haskell provided for
2146 certain rules to be applied in the special case of numeric types.
2148 * at least one of its classes is a numeric class, and
2149 * all of its classes are numeric or standard
2150 then the type variable can be defaulted to the first type in the
2151 default-type list which is an instance of all the offending classes.
2153 So here is the function which does the work. It takes the ambiguous
2154 dictionaries and either resolves them (producing bindings) or
2155 complains. It works by splitting the dictionary list by type
2156 variable, and using @disambigOne@ to do the real business.
2158 @disambigOne@ assumes that its arguments dictionaries constrain all
2159 the same type variable.
2161 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2162 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2163 the most common use of defaulting is code like:
2165 _ccall_ foo `seqPrimIO` bar
2167 Since we're not using the result of @foo@, the result if (presumably)
2171 disambigGroup :: [Inst] -- All standard classes of form (C a)
2175 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2176 -- SO, TRY DEFAULT TYPES IN ORDER
2178 -- Failure here is caused by there being no type in the
2179 -- default list which can satisfy all the ambiguous classes.
2180 -- For example, if Real a is reqd, but the only type in the
2181 -- default list is Int.
2182 get_default_tys `thenM` \ default_tys ->
2184 try_default [] -- No defaults work, so fail
2187 try_default (default_ty : default_tys)
2188 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2189 -- default_tys instead
2190 tcSimplifyDefault theta `thenM` \ _ ->
2193 theta = [mkClassPred clas [default_ty] | clas <- classes]
2195 -- See if any default works
2196 tryM (try_default default_tys) `thenM` \ mb_ty ->
2199 Right chosen_default_ty -> choose_default chosen_default_ty
2201 tyvar = get_tv (head dicts) -- Should be non-empty
2202 classes = map get_clas dicts
2204 choose_default default_ty -- Commit to tyvar = default_ty
2205 = -- Bind the type variable
2206 unifyType default_ty (mkTyVarTy tyvar) `thenM_`
2207 -- and reduce the context, for real this time
2208 simpleReduceLoop (text "disambig" <+> ppr dicts)
2209 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2210 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2211 warnDefault dicts default_ty `thenM_`
2214 bomb_out = addTopAmbigErrs dicts `thenM_`
2218 = do { mb_defaults <- getDefaultTys
2219 ; case mb_defaults of
2220 Just tys -> return tys
2221 Nothing -> -- No use-supplied default;
2222 -- use [Integer, Double]
2223 do { integer_ty <- tcMetaTy integerTyConName
2224 ; checkWiredInTyCon doubleTyCon
2225 ; return [integer_ty, doubleTy] } }
2228 [Aside - why the defaulting mechanism is turned off when
2229 dealing with arguments and results to ccalls.
2231 When typechecking _ccall_s, TcExpr ensures that the external
2232 function is only passed arguments (and in the other direction,
2233 results) of a restricted set of 'native' types.
2235 The interaction between the defaulting mechanism for numeric
2236 values and CC & CR can be a bit puzzling to the user at times.
2245 What type has 'x' got here? That depends on the default list
2246 in operation, if it is equal to Haskell 98's default-default
2247 of (Integer, Double), 'x' has type Double, since Integer
2248 is not an instance of CR. If the default list is equal to
2249 Haskell 1.4's default-default of (Int, Double), 'x' has type
2255 %************************************************************************
2257 \subsection[simple]{@Simple@ versions}
2259 %************************************************************************
2261 Much simpler versions when there are no bindings to make!
2263 @tcSimplifyThetas@ simplifies class-type constraints formed by
2264 @deriving@ declarations and when specialising instances. We are
2265 only interested in the simplified bunch of class/type constraints.
2267 It simplifies to constraints of the form (C a b c) where
2268 a,b,c are type variables. This is required for the context of
2269 instance declarations.
2272 tcSimplifyDeriv :: TyCon
2274 -> ThetaType -- Wanted
2275 -> TcM ThetaType -- Needed
2277 tcSimplifyDeriv tc tyvars theta
2278 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2279 -- The main loop may do unification, and that may crash if
2280 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2281 -- ToDo: what if two of them do get unified?
2282 newDictBndrsO DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2283 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2284 ASSERT( null frees ) -- reduceMe never returns Free
2286 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
2287 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2289 tv_set = mkVarSet tvs
2291 (bad_insts, ok_insts) = partition is_bad_inst irreds
2293 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2294 in isEmptyVarSet (tyVarsOfPred pred)
2295 -- Things like (Eq T) are bad
2296 || (not gla_exts && not (isTyVarClassPred pred))
2298 simpl_theta = map dictPred ok_insts
2299 weird_preds = [pred | pred <- simpl_theta
2300 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2301 -- Check for a bizarre corner case, when the derived instance decl should
2302 -- have form instance C a b => D (T a) where ...
2303 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2304 -- of problems; in particular, it's hard to compare solutions for
2305 -- equality when finding the fixpoint. So I just rule it out for now.
2307 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2308 -- This reverse-mapping is a Royal Pain,
2309 -- but the result should mention TyVars not TcTyVars
2312 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2313 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2314 returnM (substTheta rev_env simpl_theta)
2316 doc = ptext SLIT("deriving classes for a data type")
2319 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2320 used with \tr{default} declarations. We are only interested in
2321 whether it worked or not.
2324 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2327 tcSimplifyDefault theta
2328 = newDictBndrsO DefaultOrigin theta `thenM` \ wanteds ->
2329 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2330 ASSERT( null frees ) -- try_me never returns Free
2331 addNoInstanceErrs Nothing [] irreds `thenM_`
2337 doc = ptext SLIT("default declaration")
2341 %************************************************************************
2343 \section{Errors and contexts}
2345 %************************************************************************
2347 ToDo: for these error messages, should we note the location as coming
2348 from the insts, or just whatever seems to be around in the monad just
2352 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2353 -> [Inst] -- The offending Insts
2355 -- Group together insts with the same origin
2356 -- We want to report them together in error messages
2358 groupErrs report_err []
2360 groupErrs report_err (inst:insts)
2361 = do_one (inst:friends) `thenM_`
2362 groupErrs report_err others
2365 -- (It may seem a bit crude to compare the error messages,
2366 -- but it makes sure that we combine just what the user sees,
2367 -- and it avoids need equality on InstLocs.)
2368 (friends, others) = partition is_friend insts
2369 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2370 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2371 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2372 -- Add location and context information derived from the Insts
2374 -- Add the "arising from..." part to a message about bunch of dicts
2375 addInstLoc :: [Inst] -> Message -> Message
2376 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2378 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2379 addTopIPErrs bndrs []
2381 addTopIPErrs bndrs ips
2382 = addErrTcM (tidy_env, mk_msg tidy_ips)
2384 (tidy_env, tidy_ips) = tidyInsts ips
2385 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2386 nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
2387 <+> pprBinders bndrs <> colon)],
2388 nest 2 (vcat (map ppr_ip ips)),
2390 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2392 strangeTopIPErrs :: [Inst] -> TcM ()
2393 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2394 = groupErrs report tidy_dicts
2396 (tidy_env, tidy_dicts) = tidyInsts dicts
2397 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2398 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2399 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2401 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2402 -- Just d => d describes the construct
2403 -> [Inst] -- What is given by the context or type sig
2404 -> [Inst] -- What is wanted
2406 addNoInstanceErrs mb_what givens []
2408 addNoInstanceErrs mb_what givens dicts
2409 = -- Some of the dicts are here because there is no instances
2410 -- and some because there are too many instances (overlap)
2411 tcGetInstEnvs `thenM` \ inst_envs ->
2413 (tidy_env1, tidy_givens) = tidyInsts givens
2414 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2416 -- Run through the dicts, generating a message for each
2417 -- overlapping one, but simply accumulating all the
2418 -- no-instance ones so they can be reported as a group
2419 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2420 check_overlap (overlap_doc, no_inst_dicts) dict
2421 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2423 = case lookupInstEnv inst_envs clas tys of
2424 -- The case of exactly one match and no unifiers means
2425 -- a successful lookup. That can't happen here, becuase
2426 -- dicts only end up here if they didn't match in Inst.lookupInst
2428 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2430 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2431 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2433 (clas,tys) = getDictClassTys dict
2436 -- Now generate a good message for the no-instance bunch
2437 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2439 no_inst_doc | null no_inst_dicts = empty
2440 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2441 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2442 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2443 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2444 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2446 -- And emit both the non-instance and overlap messages
2447 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2449 mk_overlap_msg dict (matches, unifiers)
2450 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2451 <+> pprPred (dictPred dict))),
2452 sep [ptext SLIT("Matching instances") <> colon,
2453 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2454 ASSERT( not (null matches) )
2455 if not (isSingleton matches)
2456 then -- Two or more matches
2458 else -- One match, plus some unifiers
2459 ASSERT( not (null unifiers) )
2460 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2461 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2462 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2464 ispecs = [ispec | (_, ispec) <- matches]
2466 mk_probable_fix tidy_env dicts
2467 = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
2469 fixes = add_ors (fix1 ++ fix2)
2471 fix1 = case mb_what of
2472 Nothing -> [] -- Top level
2473 Just what -> -- Nested (type signatures, instance decls)
2474 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2475 ptext SLIT("to the") <+> what] ]
2477 fix2 | null instance_dicts = []
2478 | otherwise = [ sep [ptext SLIT("add an instance declaration for"),
2479 pprDictsTheta instance_dicts] ]
2480 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2481 -- Insts for which it is worth suggesting an adding an instance declaration
2482 -- Exclude implicit parameters, and tyvar dicts
2484 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2485 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2486 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2488 addTopAmbigErrs dicts
2489 -- Divide into groups that share a common set of ambiguous tyvars
2490 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2492 (tidy_env, tidy_dicts) = tidyInsts dicts
2494 tvs_of :: Inst -> [TcTyVar]
2495 tvs_of d = varSetElems (tyVarsOfInst d)
2496 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2498 report :: [(Inst,[TcTyVar])] -> TcM ()
2499 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2500 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2501 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2502 -- the location of the first one will do for the err message
2503 addErrTcM (tidy_env, msg $$ mono_msg)
2505 dicts = map fst pairs
2506 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2507 pprQuotedList tvs <+> in_msg,
2508 nest 2 (pprDictsInFull dicts)]
2509 in_msg = text "in the constraint" <> plural dicts <> colon
2512 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2513 -- There's an error with these Insts; if they have free type variables
2514 -- it's probably caused by the monomorphism restriction.
2515 -- Try to identify the offending variable
2516 -- ASSUMPTION: the Insts are fully zonked
2517 mkMonomorphismMsg tidy_env inst_tvs
2518 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2519 returnM (tidy_env, mk_msg docs)
2521 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2522 -- This happens in things like
2523 -- f x = show (read "foo")
2524 -- whre monomorphism doesn't play any role
2525 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2529 monomorphism_fix :: SDoc
2530 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2531 (ptext SLIT("give these definition(s) an explicit type signature")
2532 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2534 warnDefault dicts default_ty
2535 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2536 addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
2539 (_, tidy_dicts) = tidyInsts dicts
2540 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2541 quotes (ppr default_ty),
2542 pprDictsInFull tidy_dicts]
2544 -- Used for the ...Thetas variants; all top level
2546 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2547 ptext SLIT("type variables that are not data type parameters"),
2548 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2550 reduceDepthErr n stack
2551 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2552 ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
2553 nest 4 (pprStack stack)]
2555 pprStack stack = vcat (map pprInstInFull stack)