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, emptyLHsBinds )
25 import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp )
28 import Inst ( lookupInst, LookupInstResult(..),
29 tyVarsOfInst, fdPredsOfInsts, newDicts,
30 isDict, isClassDict, isLinearInst, linearInstType,
31 isMethodFor, isMethod,
32 instToId, tyVarsOfInsts, cloneDict,
33 ipNamesOfInsts, ipNamesOfInst, dictPred,
35 newDictsAtLoc, tcInstClassOp,
36 getDictClassTys, isTyVarDict, instLoc,
37 zonkInst, tidyInsts, tidyMoreInsts,
38 pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
39 isInheritableInst, pprDictsTheta
41 import TcEnv ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders,
42 lclEnvElts, tcMetaTy )
43 import InstEnv ( lookupInstEnv, classInstances, pprInstances )
44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType )
45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,
46 mkClassPred, isOverloadedTy, mkTyConApp, isSkolemTyVar,
47 mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
48 tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )
49 import TcIface ( checkWiredInTyCon )
50 import Id ( idType, mkUserLocal )
52 import TyCon ( TyCon )
53 import Name ( Name, getOccName, getSrcLoc )
54 import NameSet ( NameSet, mkNameSet, elemNameSet )
55 import Class ( classBigSig, classKey )
56 import FunDeps ( oclose, grow, improve, pprEquation )
57 import PrelInfo ( isNumericClass, isStandardClass )
58 import PrelNames ( splitName, fstName, sndName, integerTyConName,
59 showClassKey, eqClassKey, ordClassKey )
60 import Type ( zipTopTvSubst, substTheta, substTy )
61 import TysWiredIn ( pairTyCon, doubleTy, doubleTyCon )
62 import ErrUtils ( Message )
63 import BasicTypes ( TopLevelFlag, isNotTopLevel )
65 import VarEnv ( TidyEnv )
69 import ListSetOps ( equivClasses )
70 import Util ( zipEqual, isSingleton )
71 import List ( partition )
72 import SrcLoc ( Located(..) )
73 import DynFlags ( DynFlags(ctxtStkDepth),
74 DynFlag( Opt_GlasgowExts, Opt_AllowUndecidableInstances,
75 Opt_WarnTypeDefaults, Opt_ExtendedDefaultRules ) )
79 %************************************************************************
83 %************************************************************************
85 --------------------------------------
86 Notes on functional dependencies (a bug)
87 --------------------------------------
94 instance D a b => C a b -- Undecidable
95 -- (Not sure if it's crucial to this eg)
96 f :: C a b => a -> Bool
99 g :: C a b => a -> Bool
102 Here f typechecks, but g does not!! Reason: before doing improvement,
103 we reduce the (C a b1) constraint from the call of f to (D a b1).
105 Here is a more complicated example:
107 | > class Foo a b | a->b
109 | > class Bar a b | a->b
113 | > instance Bar Obj Obj
115 | > instance (Bar a b) => Foo a b
117 | > foo:: (Foo a b) => a -> String
120 | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
126 | Could not deduce (Bar a b) from the context (Foo a b)
127 | arising from use of `foo' at <interactive>:1
129 | Add (Bar a b) to the expected type of an expression
130 | In the first argument of `runFoo', namely `foo'
131 | In the definition of `it': it = runFoo foo
133 | Why all of the sudden does GHC need the constraint Bar a b? The
134 | function foo didn't ask for that...
136 The trouble is that to type (runFoo foo), GHC has to solve the problem:
138 Given constraint Foo a b
139 Solve constraint Foo a b'
141 Notice that b and b' aren't the same. To solve this, just do
142 improvement and then they are the same. But GHC currently does
147 That is usually fine, but it isn't here, because it sees that Foo a b is
148 not the same as Foo a b', and so instead applies the instance decl for
149 instance Bar a b => Foo a b. And that's where the Bar constraint comes
152 The Right Thing is to improve whenever the constraint set changes at
153 all. Not hard in principle, but it'll take a bit of fiddling to do.
157 --------------------------------------
158 Notes on quantification
159 --------------------------------------
161 Suppose we are about to do a generalisation step.
165 T the type of the RHS
166 C the constraints from that RHS
168 The game is to figure out
170 Q the set of type variables over which to quantify
171 Ct the constraints we will *not* quantify over
172 Cq the constraints we will quantify over
174 So we're going to infer the type
178 and float the constraints Ct further outwards.
180 Here are the things that *must* be true:
182 (A) Q intersect fv(G) = EMPTY limits how big Q can be
183 (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be
185 (A) says we can't quantify over a variable that's free in the
186 environment. (B) says we must quantify over all the truly free
187 variables in T, else we won't get a sufficiently general type. We do
188 not *need* to quantify over any variable that is fixed by the free
189 vars of the environment G.
191 BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
193 Example: class H x y | x->y where ...
195 fv(G) = {a} C = {H a b, H c d}
198 (A) Q intersect {a} is empty
199 (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
201 So Q can be {c,d}, {b,c,d}
203 Other things being equal, however, we'd like to quantify over as few
204 variables as possible: smaller types, fewer type applications, more
205 constraints can get into Ct instead of Cq.
208 -----------------------------------------
211 fv(T) the free type vars of T
213 oclose(vs,C) The result of extending the set of tyvars vs
214 using the functional dependencies from C
216 grow(vs,C) The result of extend the set of tyvars vs
217 using all conceivable links from C.
219 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
220 Then grow(vs,C) = {a,b,c}
222 Note that grow(vs,C) `superset` grow(vs,simplify(C))
223 That is, simplfication can only shrink the result of grow.
226 oclose is conservative one way: v `elem` oclose(vs,C) => v is definitely fixed by vs
227 grow is conservative the other way: if v might be fixed by vs => v `elem` grow(vs,C)
230 -----------------------------------------
234 Here's a good way to choose Q:
236 Q = grow( fv(T), C ) \ oclose( fv(G), C )
238 That is, quantify over all variable that that MIGHT be fixed by the
239 call site (which influences T), but which aren't DEFINITELY fixed by
240 G. This choice definitely quantifies over enough type variables,
241 albeit perhaps too many.
243 Why grow( fv(T), C ) rather than fv(T)? Consider
245 class H x y | x->y where ...
250 If we used fv(T) = {c} we'd get the type
252 forall c. H c d => c -> b
254 And then if the fn was called at several different c's, each of
255 which fixed d differently, we'd get a unification error, because
256 d isn't quantified. Solution: quantify d. So we must quantify
257 everything that might be influenced by c.
259 Why not oclose( fv(T), C )? Because we might not be able to see
260 all the functional dependencies yet:
262 class H x y | x->y where ...
263 instance H x y => Eq (T x y) where ...
268 Now oclose(fv(T),C) = {c}, because the functional dependency isn't
269 apparent yet, and that's wrong. We must really quantify over d too.
272 There really isn't any point in quantifying over any more than
273 grow( fv(T), C ), because the call sites can't possibly influence
274 any other type variables.
278 -------------------------------------
280 -------------------------------------
282 It's very hard to be certain when a type is ambiguous. Consider
286 instance H x y => K (x,y)
288 Is this type ambiguous?
289 forall a b. (K (a,b), Eq b) => a -> a
291 Looks like it! But if we simplify (K (a,b)) we get (H a b) and
292 now we see that a fixes b. So we can't tell about ambiguity for sure
293 without doing a full simplification. And even that isn't possible if
294 the context has some free vars that may get unified. Urgle!
296 Here's another example: is this ambiguous?
297 forall a b. Eq (T b) => a -> a
298 Not if there's an insance decl (with no context)
299 instance Eq (T b) where ...
301 You may say of this example that we should use the instance decl right
302 away, but you can't always do that:
304 class J a b where ...
305 instance J Int b where ...
307 f :: forall a b. J a b => a -> a
309 (Notice: no functional dependency in J's class decl.)
310 Here f's type is perfectly fine, provided f is only called at Int.
311 It's premature to complain when meeting f's signature, or even
312 when inferring a type for f.
316 However, we don't *need* to report ambiguity right away. It'll always
317 show up at the call site.... and eventually at main, which needs special
318 treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.
320 So here's the plan. We WARN about probable ambiguity if
322 fv(Cq) is not a subset of oclose(fv(T) union fv(G), C)
324 (all tested before quantification).
325 That is, all the type variables in Cq must be fixed by the the variables
326 in the environment, or by the variables in the type.
328 Notice that we union before calling oclose. Here's an example:
330 class J a b c | a b -> c
334 forall b c. (J a b c) => b -> b
336 Only if we union {a} from G with {b} from T before using oclose,
337 do we see that c is fixed.
339 It's a bit vague exactly which C we should use for this oclose call. If we
340 don't fix enough variables we might complain when we shouldn't (see
341 the above nasty example). Nothing will be perfect. That's why we can
342 only issue a warning.
345 Can we ever be *certain* about ambiguity? Yes: if there's a constraint
347 c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
349 then c is a "bubble"; there's no way it can ever improve, and it's
350 certainly ambiguous. UNLESS it is a constant (sigh). And what about
355 instance H x y => K (x,y)
357 Is this type ambiguous?
358 forall a b. (K (a,b), Eq b) => a -> a
360 Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after
361 is a "bubble" that's a set of constraints
363 Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
365 Hence another idea. To decide Q start with fv(T) and grow it
366 by transitive closure in Cq (no functional dependencies involved).
367 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
368 The definitely-ambiguous can then float out, and get smashed at top level
369 (which squashes out the constants, like Eq (T a) above)
372 --------------------------------------
373 Notes on principal types
374 --------------------------------------
379 f x = let g y = op (y::Int) in True
381 Here the principal type of f is (forall a. a->a)
382 but we'll produce the non-principal type
383 f :: forall a. C Int => a -> a
386 --------------------------------------
387 The need for forall's in constraints
388 --------------------------------------
390 [Exchange on Haskell Cafe 5/6 Dec 2000]
392 class C t where op :: t -> Bool
393 instance C [t] where op x = True
395 p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
396 q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
398 The definitions of p and q differ only in the order of the components in
399 the pair on their right-hand sides. And yet:
401 ghc and "Typing Haskell in Haskell" reject p, but accept q;
402 Hugs rejects q, but accepts p;
403 hbc rejects both p and q;
404 nhc98 ... (Malcolm, can you fill in the blank for us!).
406 The type signature for f forces context reduction to take place, and
407 the results of this depend on whether or not the type of y is known,
408 which in turn depends on which component of the pair the type checker
411 Solution: if y::m a, float out the constraints
412 Monad m, forall c. C (m c)
413 When m is later unified with [], we can solve both constraints.
416 --------------------------------------
417 Notes on implicit parameters
418 --------------------------------------
420 Question 1: can we "inherit" implicit parameters
421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
426 where f is *not* a top-level binding.
427 From the RHS of f we'll get the constraint (?y::Int).
428 There are two types we might infer for f:
432 (so we get ?y from the context of f's definition), or
434 f :: (?y::Int) => Int -> Int
436 At first you might think the first was better, becuase then
437 ?y behaves like a free variable of the definition, rather than
438 having to be passed at each call site. But of course, the WHOLE
439 IDEA is that ?y should be passed at each call site (that's what
440 dynamic binding means) so we'd better infer the second.
442 BOTTOM LINE: when *inferring types* you *must* quantify
443 over implicit parameters. See the predicate isFreeWhenInferring.
446 Question 2: type signatures
447 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
448 BUT WATCH OUT: When you supply a type signature, we can't force you
449 to quantify over implicit parameters. For example:
453 This is perfectly reasonable. We do not want to insist on
455 (?x + 1) :: (?x::Int => Int)
457 That would be silly. Here, the definition site *is* the occurrence site,
458 so the above strictures don't apply. Hence the difference between
459 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
460 and tcSimplifyCheckBind (which does not).
462 What about when you supply a type signature for a binding?
463 Is it legal to give the following explicit, user type
464 signature to f, thus:
469 At first sight this seems reasonable, but it has the nasty property
470 that adding a type signature changes the dynamic semantics.
473 (let f x = (x::Int) + ?y
474 in (f 3, f 3 with ?y=5)) with ?y = 6
480 in (f 3, f 3 with ?y=5)) with ?y = 6
484 Indeed, simply inlining f (at the Haskell source level) would change the
487 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
488 semantics for a Haskell program without knowing its typing, so if you
489 change the typing you may change the semantics.
491 To make things consistent in all cases where we are *checking* against
492 a supplied signature (as opposed to inferring a type), we adopt the
495 a signature does not need to quantify over implicit params.
497 [This represents a (rather marginal) change of policy since GHC 5.02,
498 which *required* an explicit signature to quantify over all implicit
499 params for the reasons mentioned above.]
501 But that raises a new question. Consider
503 Given (signature) ?x::Int
504 Wanted (inferred) ?x::Int, ?y::Bool
506 Clearly we want to discharge the ?x and float the ?y out. But
507 what is the criterion that distinguishes them? Clearly it isn't
508 what free type variables they have. The Right Thing seems to be
509 to float a constraint that
510 neither mentions any of the quantified type variables
511 nor any of the quantified implicit parameters
513 See the predicate isFreeWhenChecking.
516 Question 3: monomorphism
517 ~~~~~~~~~~~~~~~~~~~~~~~~
518 There's a nasty corner case when the monomorphism restriction bites:
522 The argument above suggests that we *must* generalise
523 over the ?y parameter, to get
524 z :: (?y::Int) => Int,
525 but the monomorphism restriction says that we *must not*, giving
527 Why does the momomorphism restriction say this? Because if you have
529 let z = x + ?y in z+z
531 you might not expect the addition to be done twice --- but it will if
532 we follow the argument of Question 2 and generalise over ?y.
535 Question 4: top level
536 ~~~~~~~~~~~~~~~~~~~~~
537 At the top level, monomorhism makes no sense at all.
540 main = let ?x = 5 in print foo
544 woggle :: (?x :: Int) => Int -> Int
547 We definitely don't want (foo :: Int) with a top-level implicit parameter
548 (?x::Int) becuase there is no way to bind it.
553 (A) Always generalise over implicit parameters
554 Bindings that fall under the monomorphism restriction can't
558 * Inlining remains valid
559 * No unexpected loss of sharing
560 * But simple bindings like
562 will be rejected, unless you add an explicit type signature
563 (to avoid the monomorphism restriction)
564 z :: (?y::Int) => Int
566 This seems unacceptable
568 (B) Monomorphism restriction "wins"
569 Bindings that fall under the monomorphism restriction can't
571 Always generalise over implicit parameters *except* for bindings
572 that fall under the monomorphism restriction
575 * Inlining isn't valid in general
576 * No unexpected loss of sharing
577 * Simple bindings like
579 accepted (get value of ?y from binding site)
581 (C) Always generalise over implicit parameters
582 Bindings that fall under the monomorphism restriction can't
583 be generalised, EXCEPT for implicit parameters
585 * Inlining remains valid
586 * Unexpected loss of sharing (from the extra generalisation)
587 * Simple bindings like
589 accepted (get value of ?y from occurrence sites)
594 None of these choices seems very satisfactory. But at least we should
595 decide which we want to do.
597 It's really not clear what is the Right Thing To Do. If you see
601 would you expect the value of ?y to be got from the *occurrence sites*
602 of 'z', or from the valuue of ?y at the *definition* of 'z'? In the
603 case of function definitions, the answer is clearly the former, but
604 less so in the case of non-fucntion definitions. On the other hand,
605 if we say that we get the value of ?y from the definition site of 'z',
606 then inlining 'z' might change the semantics of the program.
608 Choice (C) really says "the monomorphism restriction doesn't apply
609 to implicit parameters". Which is fine, but remember that every
610 innocent binding 'x = ...' that mentions an implicit parameter in
611 the RHS becomes a *function* of that parameter, called at each
612 use of 'x'. Now, the chances are that there are no intervening 'with'
613 clauses that bind ?y, so a decent compiler should common up all
614 those function calls. So I think I strongly favour (C). Indeed,
615 one could make a similar argument for abolishing the monomorphism
616 restriction altogether.
618 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted
622 %************************************************************************
624 \subsection{tcSimplifyInfer}
626 %************************************************************************
628 tcSimplify is called when we *inferring* a type. Here's the overall game plan:
630 1. Compute Q = grow( fvs(T), C )
632 2. Partition C based on Q into Ct and Cq. Notice that ambiguous
633 predicates will end up in Ct; we deal with them at the top level
635 3. Try improvement, using functional dependencies
637 4. If Step 3 did any unification, repeat from step 1
638 (Unification can change the result of 'grow'.)
640 Note: we don't reduce dictionaries in step 2. For example, if we have
641 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different
642 after step 2. However note that we may therefore quantify over more
643 type variables than we absolutely have to.
645 For the guts, we need a loop, that alternates context reduction and
646 improvement with unification. E.g. Suppose we have
648 class C x y | x->y where ...
650 and tcSimplify is called with:
652 Then improvement unifies a with b, giving
655 If we need to unify anything, we rattle round the whole thing all over
662 -> TcTyVarSet -- fv(T); type vars
664 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
665 TcDictBinds, -- Bindings
666 [TcId]) -- Dict Ids that must be bound here (zonked)
667 -- Any free (escaping) Insts are tossed into the environment
672 tcSimplifyInfer doc tau_tvs wanted_lie
673 = inferLoop doc (varSetElems tau_tvs)
674 wanted_lie `thenM` \ (qtvs, frees, binds, irreds) ->
676 extendLIEs frees `thenM_`
677 returnM (qtvs, binds, map instToId irreds)
679 inferLoop doc tau_tvs wanteds
681 zonkTcTyVarsAndFV tau_tvs `thenM` \ tau_tvs' ->
682 mappM zonkInst wanteds `thenM` \ wanteds' ->
683 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
685 preds = fdPredsOfInsts wanteds'
686 qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
689 | isFreeWhenInferring qtvs inst = Free
690 | isClassDict inst = DontReduceUnlessConstant -- Dicts
691 | otherwise = ReduceMe NoSCs -- Lits and Methods
693 traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds,
694 ppr (grow preds tau_tvs'), ppr qtvs]) `thenM_`
696 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
699 if no_improvement then
700 returnM (varSetElems qtvs, frees, binds, irreds)
702 -- If improvement did some unification, we go round again. There
703 -- are two subtleties:
704 -- a) We start again with irreds, not wanteds
705 -- Using an instance decl might have introduced a fresh type variable
706 -- which might have been unified, so we'd get an infinite loop
707 -- if we started again with wanteds! See example [LOOP]
709 -- b) It's also essential to re-process frees, because unification
710 -- might mean that a type variable that looked free isn't now.
712 -- Hence the (irreds ++ frees)
714 -- However, NOTICE that when we are done, we might have some bindings, but
715 -- the final qtvs might be empty. See [NO TYVARS] below.
717 inferLoop doc tau_tvs (irreds ++ frees) `thenM` \ (qtvs1, frees1, binds1, irreds1) ->
718 returnM (qtvs1, frees1, binds `unionBags` binds1, irreds1)
723 class If b t e r | b t e -> r
726 class Lte a b c | a b -> c where lte :: a -> b -> c
728 instance (Lte a b l,If l b a c) => Max a b c
730 Wanted: Max Z (S x) y
732 Then we'll reduce using the Max instance to:
733 (Lte Z (S x) l, If l (S x) Z y)
734 and improve by binding l->T, after which we can do some reduction
735 on both the Lte and If constraints. What we *can't* do is start again
736 with (Max Z (S x) y)!
740 class Y a b | a -> b where
743 instance Y [[a]] a where
746 k :: X a -> X a -> X a
748 g :: Num a => [X a] -> [X a]
751 h ys = ys ++ map (k (y [[0]])) xs
753 The excitement comes when simplifying the bindings for h. Initially
754 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
755 From this we get t1:=:t2, but also various bindings. We can't forget
756 the bindings (because of [LOOP]), but in fact t1 is what g is
759 The net effect of [NO TYVARS]
762 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
763 isFreeWhenInferring qtvs inst
764 = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars
765 && isInheritableInst inst -- And no implicit parameter involved
766 -- (see "Notes on implicit parameters")
768 isFreeWhenChecking :: TyVarSet -- Quantified tyvars
769 -> NameSet -- Quantified implicit parameters
771 isFreeWhenChecking qtvs ips inst
772 = isFreeWrtTyVars qtvs inst
773 && isFreeWrtIPs ips inst
775 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
776 isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
780 %************************************************************************
782 \subsection{tcSimplifyCheck}
784 %************************************************************************
786 @tcSimplifyCheck@ is used when we know exactly the set of variables
787 we are going to quantify over. For example, a class or instance declaration.
792 -> [TcTyVar] -- Quantify over these
795 -> TcM TcDictBinds -- Bindings
797 -- tcSimplifyCheck is used when checking expression type signatures,
798 -- class decls, instance decls etc.
800 -- NB: tcSimplifyCheck does not consult the
801 -- global type variables in the environment; so you don't
802 -- need to worry about setting them before calling tcSimplifyCheck
803 tcSimplifyCheck doc qtvs givens wanted_lie
804 = ASSERT( all isSkolemTyVar qtvs )
805 do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
809 -- get_qtvs = zonkTcTyVarsAndFV qtvs
810 get_qtvs = return (mkVarSet qtvs) -- All skolems
813 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
814 -- against, but we don't know the type variables over which we are going to quantify.
815 -- This happens when we have a type signature for a mutually recursive group
818 -> TcTyVarSet -- fv(T)
821 -> TcM ([TcTyVar], -- Variables over which to quantify
822 TcDictBinds) -- Bindings
824 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
825 = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie
827 ; return (qtvs', binds) }
829 -- Figure out which type variables to quantify over
830 -- You might think it should just be the signature tyvars,
831 -- but in bizarre cases you can get extra ones
832 -- f :: forall a. Num a => a -> a
833 -- f x = fst (g (x, head [])) + 1
835 -- Here we infer g :: forall a b. a -> b -> (b,a)
836 -- We don't want g to be monomorphic in b just because
837 -- f isn't quantified over b.
838 all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
840 get_qtvs = zonkTcTyVarsAndFV all_tvs `thenM` \ all_tvs' ->
841 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
843 qtvs = all_tvs' `minusVarSet` gbl_tvs
844 -- We could close gbl_tvs, but its not necessary for
845 -- soundness, and it'll only affect which tyvars, not which
846 -- dictionaries, we quantify over
851 Here is the workhorse function for all three wrappers.
854 tcSimplCheck doc get_qtvs want_scs givens wanted_lie
855 = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie
857 -- Complain about any irreducible ones
858 ; if not (null irreds)
859 then do { givens' <- mappM zonkInst given_dicts_and_ips
860 ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds }
863 ; returnM (qtvs, frees, binds) }
865 given_dicts_and_ips = filter (not . isMethod) givens
866 -- For error reporting, filter out methods, which are
867 -- only added to the given set as an optimisation
869 ip_set = mkNameSet (ipNamesOfInsts givens)
871 check_loop givens wanteds
873 mappM zonkInst givens `thenM` \ givens' ->
874 mappM zonkInst wanteds `thenM` \ wanteds' ->
875 get_qtvs `thenM` \ qtvs' ->
879 -- When checking against a given signature we always reduce
880 -- until we find a match against something given, or can't reduce
881 try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
882 | otherwise = ReduceMe want_scs
884 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
887 if no_improvement then
888 returnM (varSetElems qtvs', frees, binds, irreds)
890 check_loop givens' (irreds ++ frees) `thenM` \ (qtvs', frees1, binds1, irreds1) ->
891 returnM (qtvs', frees1, binds `unionBags` binds1, irreds1)
895 %************************************************************************
897 tcSimplifySuperClasses
899 %************************************************************************
901 Note [SUPERCLASS-LOOP 1]
902 ~~~~~~~~~~~~~~~~~~~~~~~~
903 We have to be very, very careful when generating superclasses, lest we
904 accidentally build a loop. Here's an example:
908 class S a => C a where { opc :: a -> a }
909 class S b => D b where { opd :: b -> b }
917 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
918 Simplifying, we may well get:
919 $dfCInt = :C ds1 (opd dd)
922 Notice that we spot that we can extract ds1 from dd.
924 Alas! Alack! We can do the same for (instance D Int):
926 $dfDInt = :D ds2 (opc dc)
930 And now we've defined the superclass in terms of itself.
932 Solution: never generate a superclass selectors at all when
933 satisfying the superclass context of an instance declaration.
935 Two more nasty cases are in
940 tcSimplifySuperClasses qtvs givens sc_wanteds
941 = ASSERT( all isSkolemTyVar qtvs )
942 do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds
943 ; ext_default <- doptM Opt_ExtendedDefaultRules
944 ; binds2 <- tc_simplify_top doc ext_default NoSCs frees
945 ; return (binds1 `unionBags` binds2) }
947 get_qtvs = return (mkVarSet qtvs)
948 doc = ptext SLIT("instance declaration superclass context")
952 %************************************************************************
954 \subsection{tcSimplifyRestricted}
956 %************************************************************************
958 tcSimplifyRestricted infers which type variables to quantify for a
959 group of restricted bindings. This isn't trivial.
962 We want to quantify over a to get id :: forall a. a->a
965 We do not want to quantify over a, because there's an Eq a
966 constraint, so we get eq :: a->a->Bool (notice no forall)
969 RHS has type 'tau', whose free tyvars are tau_tvs
970 RHS has constraints 'wanteds'
973 Quantify over (tau_tvs \ ftvs(wanteds))
974 This is bad. The constraints may contain (Monad (ST s))
975 where we have instance Monad (ST s) where...
976 so there's no need to be monomorphic in s!
978 Also the constraint might be a method constraint,
979 whose type mentions a perfectly innocent tyvar:
980 op :: Num a => a -> b -> a
981 Here, b is unconstrained. A good example would be
983 We want to infer the polymorphic type
984 foo :: forall b. b -> b
987 Plan B (cunning, used for a long time up to and including GHC 6.2)
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 ) )
992 Step 2: Now simplify again, treating the constraint as 'free' if
993 it does not mention qtvs, and trying to reduce it otherwise.
994 The reasons for this is to maximise sharing.
996 This fails for a very subtle reason. Suppose that in the Step 2
997 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
998 In the Step 1 this constraint might have been simplified, perhaps to
999 (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
1000 This won't happen in Step 2... but that in turn might prevent some other
1001 constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
1002 and that in turn breaks the invariant that no constraints are quantified over.
1004 Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
1009 Step 1: Simplify the constraints as much as possible (to deal
1010 with Plan A's problem). Then set
1011 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1012 Return the bindings from Step 1.
1015 A note about Plan C (arising from "bug" reported by George Russel March 2004)
1018 instance (HasBinary ty IO) => HasCodedValue ty
1020 foo :: HasCodedValue a => String -> IO a
1022 doDecodeIO :: HasCodedValue a => () -> () -> IO a
1023 doDecodeIO codedValue view
1024 = let { act = foo "foo" } in act
1026 You might think this should work becuase the call to foo gives rise to a constraint
1027 (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the
1028 restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
1029 constraint using the (rather bogus) instance declaration, and now we are stuffed.
1031 I claim this is not really a bug -- but it bit Sergey as well as George. So here's
1035 Plan D (a variant of plan B)
1036 Step 1: Simplify the constraints as much as possible (to deal
1037 with Plan A's problem), BUT DO NO IMPROVEMENT. Then set
1038 qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
1040 Step 2: Now simplify again, treating the constraint as 'free' if
1041 it does not mention qtvs, and trying to reduce it otherwise.
1043 The point here is that it's generally OK to have too few qtvs; that is,
1044 to make the thing more monomorphic than it could be. We don't want to
1045 do that in the common cases, but in wierd cases it's ok: the programmer
1046 can always add a signature.
1048 Too few qtvs => too many wanteds, which is what happens if you do less
1053 tcSimplifyRestricted -- Used for restricted binding groups
1054 -- i.e. ones subject to the monomorphism restriction
1057 -> [Name] -- Things bound in this group
1058 -> TcTyVarSet -- Free in the type of the RHSs
1059 -> [Inst] -- Free in the RHSs
1060 -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
1061 TcDictBinds) -- Bindings
1062 -- tcSimpifyRestricted returns no constraints to
1063 -- quantify over; by definition there are none.
1064 -- They are all thrown back in the LIE
1066 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1067 -- Zonk everything in sight
1068 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1070 -- 'reduceMe': Reduce as far as we can. Don't stop at
1071 -- dicts; the idea is to get rid of as many type
1072 -- variables as possible, and we don't want to stop
1073 -- at (say) Monad (ST s), because that reduces
1074 -- immediately, with no constraint on s.
1076 -- BUT do no improvement! See Plan D above
1077 -- HOWEVER, some unification may take place, if we instantiate
1078 -- a method Inst with an equality constraint
1079 reduceContextWithoutImprovement
1080 doc reduceMe wanteds' `thenM` \ (_frees, _binds, constrained_dicts) ->
1082 -- Next, figure out the tyvars we will quantify over
1083 zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' ->
1084 tcGetGlobalTyVars `thenM` \ gbl_tvs' ->
1085 mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' ->
1087 constrained_tvs' = tyVarsOfInsts constrained_dicts'
1088 qtvs' = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
1089 `minusVarSet` constrained_tvs'
1091 traceTc (text "tcSimplifyRestricted" <+> vcat [
1092 pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts',
1094 ppr constrained_tvs', ppr tau_tvs', ppr qtvs' ]) `thenM_`
1096 -- The first step may have squashed more methods than
1097 -- necessary, so try again, this time more gently, knowing the exact
1098 -- set of type variables to quantify over.
1100 -- We quantify only over constraints that are captured by qtvs';
1101 -- these will just be a subset of non-dicts. This in contrast
1102 -- to normal inference (using isFreeWhenInferring) in which we quantify over
1103 -- all *non-inheritable* constraints too. This implements choice
1104 -- (B) under "implicit parameter and monomorphism" above.
1106 -- Remember that we may need to do *some* simplification, to
1107 -- (for example) squash {Monad (ST s)} into {}. It's not enough
1108 -- just to float all constraints
1110 -- At top level, we *do* squash methods becuase we want to
1111 -- expose implicit parameters to the test that follows
1113 is_nested_group = isNotTopLevel top_lvl
1114 try_me inst | isFreeWrtTyVars qtvs' inst,
1115 (is_nested_group || isDict inst) = Free
1116 | otherwise = ReduceMe AddSCs
1118 reduceContextWithoutImprovement
1119 doc try_me wanteds' `thenM` \ (frees, binds, irreds) ->
1120 ASSERT( null irreds )
1122 -- See "Notes on implicit parameters, Question 4: top level"
1123 if is_nested_group then
1124 extendLIEs frees `thenM_`
1125 returnM (varSetElems qtvs', binds)
1128 (non_ips, bad_ips) = partition isClassDict frees
1130 addTopIPErrs bndrs bad_ips `thenM_`
1131 extendLIEs non_ips `thenM_`
1132 returnM (varSetElems qtvs', binds)
1136 %************************************************************************
1140 %************************************************************************
1142 On the LHS of transformation rules we only simplify methods and constants,
1143 getting dictionaries. We want to keep all of them unsimplified, to serve
1144 as the available stuff for the RHS of the rule.
1146 Example. Consider the following left-hand side of a rule
1148 f (x == y) (y > z) = ...
1150 If we typecheck this expression we get constraints
1152 d1 :: Ord a, d2 :: Eq a
1154 We do NOT want to "simplify" to the LHS
1156 forall x::a, y::a, z::a, d1::Ord a.
1157 f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1161 forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
1162 f ((==) d2 x y) ((>) d1 y z) = ...
1164 Here is another example:
1166 fromIntegral :: (Integral a, Num b) => a -> b
1167 {-# RULES "foo" fromIntegral = id :: Int -> Int #-}
1169 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
1170 we *dont* want to get
1172 forall dIntegralInt.
1173 fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
1175 because the scsel will mess up RULE matching. Instead we want
1177 forall dIntegralInt, dNumInt.
1178 fromIntegral Int Int dIntegralInt dNumInt = id Int
1182 g (x == y) (y == z) = ..
1184 where the two dictionaries are *identical*, we do NOT WANT
1186 forall x::a, y::a, z::a, d1::Eq a
1187 f ((==) d1 x y) ((>) d1 y z) = ...
1189 because that will only match if the dict args are (visibly) equal.
1190 Instead we want to quantify over the dictionaries separately.
1192 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
1193 all dicts unchanged, with absolutely no sharing. It's simpler to do this
1194 from scratch, rather than further parameterise simpleReduceLoop etc
1197 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
1198 tcSimplifyRuleLhs wanteds
1199 = go [] emptyBag wanteds
1202 = return (dicts, binds)
1203 go dicts binds (w:ws)
1205 = go (w:dicts) binds ws
1207 = do { w' <- zonkInst w -- So that (3::Int) does not generate a call
1208 -- to fromInteger; this looks fragile to me
1209 ; lookup_result <- lookupInst w'
1210 ; case lookup_result of
1211 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
1212 SimpleInst rhs -> go dicts (addBind binds w rhs) ws
1213 NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
1217 tcSimplifyBracket is used when simplifying the constraints arising from
1218 a Template Haskell bracket [| ... |]. We want to check that there aren't
1219 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
1220 Show instance), but we aren't otherwise interested in the results.
1221 Nor do we care about ambiguous dictionaries etc. We will type check
1222 this bracket again at its usage site.
1225 tcSimplifyBracket :: [Inst] -> TcM ()
1226 tcSimplifyBracket wanteds
1227 = simpleReduceLoop doc reduceMe wanteds `thenM_`
1230 doc = text "tcSimplifyBracket"
1234 %************************************************************************
1236 \subsection{Filtering at a dynamic binding}
1238 %************************************************************************
1243 we must discharge all the ?x constraints from B. We also do an improvement
1244 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
1246 Actually, the constraints from B might improve the types in ?x. For example
1248 f :: (?x::Int) => Char -> Char
1251 then the constraint (?x::Int) arising from the call to f will
1252 force the binding for ?x to be of type Int.
1255 tcSimplifyIPs :: [Inst] -- The implicit parameters bound here
1258 tcSimplifyIPs given_ips wanteds
1259 = simpl_loop given_ips wanteds `thenM` \ (frees, binds) ->
1260 extendLIEs frees `thenM_`
1263 doc = text "tcSimplifyIPs" <+> ppr given_ips
1264 ip_set = mkNameSet (ipNamesOfInsts given_ips)
1266 -- Simplify any methods that mention the implicit parameter
1267 try_me inst | isFreeWrtIPs ip_set inst = Free
1268 | otherwise = ReduceMe NoSCs
1270 simpl_loop givens wanteds
1271 = mappM zonkInst givens `thenM` \ givens' ->
1272 mappM zonkInst wanteds `thenM` \ wanteds' ->
1274 reduceContext doc try_me givens' wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1276 if no_improvement then
1277 ASSERT( null irreds )
1278 returnM (frees, binds)
1280 simpl_loop givens' (irreds ++ frees) `thenM` \ (frees1, binds1) ->
1281 returnM (frees1, binds `unionBags` binds1)
1285 %************************************************************************
1287 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
1289 %************************************************************************
1291 When doing a binding group, we may have @Insts@ of local functions.
1292 For example, we might have...
1294 let f x = x + 1 -- orig local function (overloaded)
1295 f.1 = f Int -- two instances of f
1300 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
1301 where @f@ is in scope; those @Insts@ must certainly not be passed
1302 upwards towards the top-level. If the @Insts@ were binding-ified up
1303 there, they would have unresolvable references to @f@.
1305 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
1306 For each method @Inst@ in the @init_lie@ that mentions one of the
1307 @Ids@, we create a binding. We return the remaining @Insts@ (in an
1308 @LIE@), as well as the @HsBinds@ generated.
1311 bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
1312 -- Simlifies only MethodInsts, and generate only bindings of form
1314 -- We're careful not to even generate bindings of the form
1316 -- You'd think that'd be fine, but it interacts with what is
1317 -- arguably a bug in Match.tidyEqnInfo (see notes there)
1319 bindInstsOfLocalFuns wanteds local_ids
1320 | null overloaded_ids
1322 = extendLIEs wanteds `thenM_`
1323 returnM emptyLHsBinds
1326 = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
1327 ASSERT( null irreds )
1328 extendLIEs not_for_me `thenM_`
1329 extendLIEs frees `thenM_`
1332 doc = text "bindInsts" <+> ppr local_ids
1333 overloaded_ids = filter is_overloaded local_ids
1334 is_overloaded id = isOverloadedTy (idType id)
1335 (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
1337 overloaded_set = mkVarSet overloaded_ids -- There can occasionally be a lot of them
1338 -- so it's worth building a set, so that
1339 -- lookup (in isMethodFor) is faster
1340 try_me inst | isMethod inst = ReduceMe NoSCs
1345 %************************************************************************
1347 \subsection{Data types for the reduction mechanism}
1349 %************************************************************************
1351 The main control over context reduction is here
1355 = ReduceMe WantSCs -- Try to reduce this
1356 -- If there's no instance, behave exactly like
1357 -- DontReduce: add the inst to the irreductible ones,
1358 -- but don't produce an error message of any kind.
1359 -- It might be quite legitimate such as (Eq a)!
1361 | DontReduceUnlessConstant -- Return as irreducible unless it can
1362 -- be reduced to a constant in one step
1364 | Free -- Return as free
1366 reduceMe :: Inst -> WhatToDo
1367 reduceMe inst = ReduceMe AddSCs
1369 data WantSCs = NoSCs | AddSCs -- Tells whether we should add the superclasses
1370 -- of a predicate when adding it to the avails
1371 -- The reason for this flag is entirely the super-class loop problem
1372 -- Note [SUPER-CLASS LOOP 1]
1378 type Avails = FiniteMap Inst Avail
1379 emptyAvails = emptyFM
1382 = IsFree -- Used for free Insts
1383 | Irred -- Used for irreducible dictionaries,
1384 -- which are going to be lambda bound
1386 | Given TcId -- Used for dictionaries for which we have a binding
1387 -- e.g. those "given" in a signature
1388 Bool -- True <=> actually consumed (splittable IPs only)
1390 | Rhs -- Used when there is a RHS
1391 (LHsExpr TcId) -- The RHS
1392 [Inst] -- Insts free in the RHS; we need these too
1394 | Linear -- Splittable Insts only.
1395 Int -- The Int is always 2 or more; indicates how
1396 -- many copies are required
1397 Inst -- The splitter
1398 Avail -- Where the "master copy" is
1400 | LinRhss -- Splittable Insts only; this is used only internally
1401 -- by extractResults, where a Linear
1402 -- is turned into an LinRhss
1403 [LHsExpr TcId] -- A supply of suitable RHSs
1405 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1406 | (inst,avail) <- fmToList avails ]
1408 instance Outputable Avail where
1411 pprAvail IsFree = text "Free"
1412 pprAvail Irred = text "Irred"
1413 pprAvail (Given x b) = text "Given" <+> ppr x <+>
1414 if b then text "(used)" else empty
1415 pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1416 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1417 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1420 Extracting the bindings from a bunch of Avails.
1421 The bindings do *not* come back sorted in dependency order.
1422 We assume that they'll be wrapped in a big Rec, so that the
1423 dependency analyser can sort them out later
1427 extractResults :: Avails
1429 -> TcM (TcDictBinds, -- Bindings
1430 [Inst], -- Irreducible ones
1431 [Inst]) -- Free ones
1433 extractResults avails wanteds
1434 = go avails emptyBag [] [] wanteds
1436 go avails binds irreds frees []
1437 = returnM (binds, irreds, frees)
1439 go avails binds irreds frees (w:ws)
1440 = case lookupFM avails w of
1441 Nothing -> pprTrace "Urk: extractResults" (ppr w) $
1442 go avails binds irreds frees ws
1444 Just IsFree -> go (add_free avails w) binds irreds (w:frees) ws
1445 Just Irred -> go (add_given avails w) binds (w:irreds) frees ws
1447 Just (Given id _) -> go avails new_binds irreds frees ws
1449 new_binds | id == instToId w = binds
1450 | otherwise = addBind binds w (L (instSpan w) (HsVar id))
1451 -- The sought Id can be one of the givens, via a superclass chain
1452 -- and then we definitely don't want to generate an x=x binding!
1454 Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1456 new_binds = addBind binds w rhs
1458 Just (Linear n split_inst avail) -- Transform Linear --> LinRhss
1459 -> get_root irreds frees avail w `thenM` \ (irreds', frees', root_id) ->
1460 split n (instToId split_inst) root_id w `thenM` \ (binds', rhss) ->
1461 go (addToFM avails w (LinRhss rhss))
1462 (binds `unionBags` binds')
1463 irreds' frees' (split_inst : w : ws)
1465 Just (LinRhss (rhs:rhss)) -- Consume one of the Rhss
1466 -> go new_avails new_binds irreds frees ws
1468 new_binds = addBind binds w rhs
1469 new_avails = addToFM avails w (LinRhss rhss)
1471 get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
1472 get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
1473 returnM (w':irreds, frees, instToId w')
1474 get_root irreds frees IsFree w = cloneDict w `thenM` \ w' ->
1475 returnM (irreds, w':frees, instToId w')
1477 add_given avails w = addToFM avails w (Given (instToId w) True)
1479 add_free avails w | isMethod w = avails
1480 | otherwise = add_given avails w
1482 -- Do *not* replace Free by Given if it's a method.
1483 -- The following situation shows why this is bad:
1484 -- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1485 -- From an application (truncate f i) we get
1486 -- t1 = truncate at f
1488 -- If we have also have a second occurrence of truncate, we get
1489 -- t3 = truncate at f
1491 -- When simplifying with i,f free, we might still notice that
1492 -- t1=t3; but alas, the binding for t2 (which mentions t1)
1493 -- will continue to float out!
1495 split :: Int -> TcId -> TcId -> Inst
1496 -> TcM (TcDictBinds, [LHsExpr TcId])
1497 -- (split n split_id root_id wanted) returns
1498 -- * a list of 'n' expressions, all of which witness 'avail'
1499 -- * a bunch of auxiliary bindings to support these expressions
1500 -- * one or zero insts needed to witness the whole lot
1501 -- (maybe be zero if the initial Inst is a Given)
1503 -- NB: 'wanted' is just a template
1505 split n split_id root_id wanted
1508 ty = linearInstType wanted
1509 pair_ty = mkTyConApp pairTyCon [ty,ty]
1510 id = instToId wanted
1513 span = instSpan wanted
1515 go 1 = returnM (emptyBag, [L span $ HsVar root_id])
1517 go n = go ((n+1) `div` 2) `thenM` \ (binds1, rhss) ->
1518 expand n rhss `thenM` \ (binds2, rhss') ->
1519 returnM (binds1 `unionBags` binds2, rhss')
1522 -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1523 -- e.g. expand 3 [rhs1, rhs2]
1524 -- = ( { x = split rhs1 },
1525 -- [fst x, snd x, rhs2] )
1527 | n `rem` 2 == 0 = go rhss -- n is even
1528 | otherwise = go (tail rhss) `thenM` \ (binds', rhss') ->
1529 returnM (binds', head rhss : rhss')
1531 go rhss = mapAndUnzipM do_one rhss `thenM` \ (binds', rhss') ->
1532 returnM (listToBag binds', concat rhss')
1534 do_one rhs = newUnique `thenM` \ uniq ->
1535 tcLookupId fstName `thenM` \ fst_id ->
1536 tcLookupId sndName `thenM` \ snd_id ->
1538 x = mkUserLocal occ uniq pair_ty loc
1540 returnM (L span (VarBind x (mk_app span split_id rhs)),
1541 [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
1543 mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
1545 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
1547 addBind binds inst rhs = binds `unionBags` unitBag (L (instLocSrcSpan (instLoc inst))
1548 (VarBind (instToId inst) rhs))
1549 instSpan wanted = instLocSrcSpan (instLoc wanted)
1553 %************************************************************************
1555 \subsection[reduce]{@reduce@}
1557 %************************************************************************
1559 When the "what to do" predicate doesn't depend on the quantified type variables,
1560 matters are easier. We don't need to do any zonking, unless the improvement step
1561 does something, in which case we zonk before iterating.
1563 The "given" set is always empty.
1566 simpleReduceLoop :: SDoc
1567 -> (Inst -> WhatToDo) -- What to do, *not* based on the quantified type variables
1569 -> TcM ([Inst], -- Free
1571 [Inst]) -- Irreducible
1573 simpleReduceLoop doc try_me wanteds
1574 = mappM zonkInst wanteds `thenM` \ wanteds' ->
1575 reduceContext doc try_me [] wanteds' `thenM` \ (no_improvement, frees, binds, irreds) ->
1576 if no_improvement then
1577 returnM (frees, binds, irreds)
1579 simpleReduceLoop doc try_me (irreds ++ frees) `thenM` \ (frees1, binds1, irreds1) ->
1580 returnM (frees1, binds `unionBags` binds1, irreds1)
1586 reduceContext :: SDoc
1587 -> (Inst -> WhatToDo)
1590 -> TcM (Bool, -- True <=> improve step did no unification
1592 TcDictBinds, -- Dictionary bindings
1593 [Inst]) -- Irreducible
1595 reduceContext doc try_me givens wanteds
1597 traceTc (text "reduceContext" <+> (vcat [
1598 text "----------------------",
1600 text "given" <+> ppr givens,
1601 text "wanted" <+> ppr wanteds,
1602 text "----------------------"
1605 -- Build the Avail mapping from "givens"
1606 foldlM addGiven emptyAvails givens `thenM` \ init_state ->
1609 reduceList (0,[]) try_me wanteds init_state `thenM` \ avails ->
1611 -- Do improvement, using everything in avails
1612 -- In particular, avails includes all superclasses of everything
1613 tcImprove avails `thenM` \ no_improvement ->
1615 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1617 traceTc (text "reduceContext end" <+> (vcat [
1618 text "----------------------",
1620 text "given" <+> ppr givens,
1621 text "wanted" <+> ppr wanteds,
1623 text "avails" <+> pprAvails avails,
1624 text "frees" <+> ppr frees,
1625 text "no_improvement =" <+> ppr no_improvement,
1626 text "----------------------"
1629 returnM (no_improvement, frees, binds, irreds)
1631 -- reduceContextWithoutImprovement differs from reduceContext
1632 -- (a) no improvement
1633 -- (b) 'givens' is assumed empty
1634 reduceContextWithoutImprovement doc try_me wanteds
1636 traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
1637 text "----------------------",
1639 text "wanted" <+> ppr wanteds,
1640 text "----------------------"
1644 reduceList (0,[]) try_me wanteds emptyAvails `thenM` \ avails ->
1645 extractResults avails wanteds `thenM` \ (binds, irreds, frees) ->
1647 traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
1648 text "----------------------",
1650 text "wanted" <+> ppr wanteds,
1652 text "avails" <+> pprAvails avails,
1653 text "frees" <+> ppr frees,
1654 text "----------------------"
1657 returnM (frees, binds, irreds)
1659 tcImprove :: Avails -> TcM Bool -- False <=> no change
1660 -- Perform improvement using all the predicates in Avails
1662 = tcGetInstEnvs `thenM` \ inst_envs ->
1664 preds = [ (pred, pp_loc)
1665 | (inst, avail) <- fmToList avails,
1666 pred <- get_preds inst avail,
1667 let pp_loc = pprInstLoc (instLoc inst)
1669 -- Avails has all the superclasses etc (good)
1670 -- It also has all the intermediates of the deduction (good)
1671 -- It does not have duplicates (good)
1672 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1673 -- so that improve will see them separate
1675 -- For free Methods, we want to take predicates from their context,
1676 -- but for Methods that have been squished their context will already
1677 -- be in Avails, and we don't want duplicates. Hence this rather
1678 -- horrid get_preds function
1679 get_preds inst IsFree = fdPredsOfInst inst
1680 get_preds inst other | isDict inst = [dictPred inst]
1683 eqns = improve get_insts preds
1684 get_insts clas = classInstances inst_envs clas
1689 traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns)) `thenM_`
1690 mappM_ unify eqns `thenM_`
1693 unify ((qtvs, pairs), what1, what2)
1694 = addErrCtxtM (mkEqnMsg what1 what2) $
1695 tcInstTyVars (varSetElems qtvs) `thenM` \ (_, _, tenv) ->
1696 mapM_ (unif_pr tenv) pairs
1697 unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
1699 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1701 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1702 = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
1703 ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
1704 ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
1705 nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]),
1706 nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1707 ; return (tidy_env, msg) }
1710 The main context-reduction function is @reduce@. Here's its game plan.
1713 reduceList :: (Int,[Inst]) -- Stack (for err msgs)
1714 -- along with its depth
1715 -> (Inst -> WhatToDo)
1722 try_me: given an inst, this function returns
1724 DontReduce return this in "irreds"
1725 Free return this in "frees"
1727 wanteds: The list of insts to reduce
1728 state: An accumulating parameter of type Avails
1729 that contains the state of the algorithm
1731 It returns a Avails.
1733 The (n,stack) pair is just used for error reporting.
1734 n is always the depth of the stack.
1735 The stack is the stack of Insts being reduced: to produce X
1736 I had to produce Y, to produce Y I had to produce Z, and so on.
1739 reduceList (n,stack) try_me wanteds state
1740 = do { dopts <- getDOpts
1743 dumpTcRn (text "Interesting! Context reduction stack deeper than 8:"
1744 <+> (int n $$ ifPprDebug (nest 2 (pprStack stack))))
1747 ; if n >= ctxtStkDepth dopts then
1748 failWithTc (reduceDepthErr n stack)
1752 go [] state = return state
1753 go (w:ws) state = do { state' <- reduce (n+1, w:stack) try_me w state
1756 -- Base case: we're done!
1757 reduce stack try_me wanted avails
1758 -- It's the same as an existing inst, or a superclass thereof
1759 | Just avail <- isAvailable avails wanted
1760 = if isLinearInst wanted then
1761 addLinearAvailable avails avail wanted `thenM` \ (avails', wanteds') ->
1762 reduceList stack try_me wanteds' avails'
1764 returnM avails -- No op for non-linear things
1767 = case try_me wanted of {
1769 ; DontReduceUnlessConstant -> -- It's irreducible (or at least should not be reduced)
1770 -- First, see if the inst can be reduced to a constant in one step
1771 try_simple (addIrred AddSCs) -- Assume want superclasses
1773 ; Free -> -- It's free so just chuck it upstairs
1774 -- First, see if the inst can be reduced to a constant in one step
1777 ; ReduceMe want_scs -> -- It should be reduced
1778 lookupInst wanted `thenM` \ lookup_result ->
1779 case lookup_result of
1780 GenInst wanteds' rhs -> addIrred NoSCs avails wanted `thenM` \ avails1 ->
1781 reduceList stack try_me wanteds' avails1 `thenM` \ avails2 ->
1782 addWanted want_scs avails2 wanted rhs wanteds'
1783 -- Experiment with temporarily doing addIrred *before* the reduceList,
1784 -- which has the effect of adding the thing we are trying
1785 -- to prove to the database before trying to prove the things it
1786 -- needs. See note [RECURSIVE DICTIONARIES]
1787 -- NB: we must not do an addWanted before, because that adds the
1788 -- superclasses too, and thaat can lead to a spurious loop; see
1789 -- the examples in [SUPERCLASS-LOOP]
1790 -- So we do an addIrred before, and then overwrite it afterwards with addWanted
1792 SimpleInst rhs -> addWanted want_scs avails wanted rhs []
1794 NoInstance -> -- No such instance!
1795 -- Add it and its superclasses
1796 addIrred want_scs avails wanted
1799 try_simple do_this_otherwise
1800 = lookupInst wanted `thenM` \ lookup_result ->
1801 case lookup_result of
1802 SimpleInst rhs -> addWanted AddSCs avails wanted rhs []
1803 other -> do_this_otherwise avails wanted
1808 -------------------------
1809 isAvailable :: Avails -> Inst -> Maybe Avail
1810 isAvailable avails wanted = lookupFM avails wanted
1811 -- NB 1: the Ord instance of Inst compares by the class/type info
1812 -- *not* by unique. So
1813 -- d1::C Int == d2::C Int
1815 addLinearAvailable :: Avails -> Avail -> Inst -> TcM (Avails, [Inst])
1816 addLinearAvailable avails avail wanted
1817 -- avails currently maps [wanted -> avail]
1818 -- Extend avails to reflect a neeed for an extra copy of avail
1820 | Just avail' <- split_avail avail
1821 = returnM (addToFM avails wanted avail', [])
1824 = tcLookupId splitName `thenM` \ split_id ->
1825 tcInstClassOp (instLoc wanted) split_id
1826 [linearInstType wanted] `thenM` \ split_inst ->
1827 returnM (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1830 split_avail :: Avail -> Maybe Avail
1831 -- (Just av) if there's a modified version of avail that
1832 -- we can use to replace avail in avails
1833 -- Nothing if there isn't, so we need to create a Linear
1834 split_avail (Linear n i a) = Just (Linear (n+1) i a)
1835 split_avail (Given id used) | not used = Just (Given id True)
1836 | otherwise = Nothing
1837 split_avail Irred = Nothing
1838 split_avail IsFree = Nothing
1839 split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1841 -------------------------
1842 addFree :: Avails -> Inst -> TcM Avails
1843 -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1844 -- to avails, so that any other equal Insts will be commoned up right
1845 -- here rather than also being tossed upstairs. This is really just
1846 -- an optimisation, and perhaps it is more trouble that it is worth,
1847 -- as the following comments show!
1849 -- NB: do *not* add superclasses. If we have
1852 -- but a is not bound here, then we *don't* want to derive
1853 -- dn from df here lest we lose sharing.
1855 addFree avails free = returnM (addToFM avails free IsFree)
1857 addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
1858 addWanted want_scs avails wanted rhs_expr wanteds
1859 = addAvailAndSCs want_scs avails wanted avail
1861 avail = Rhs rhs_expr wanteds
1863 addGiven :: Avails -> Inst -> TcM Avails
1864 addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given) False)
1865 -- Always add superclasses for 'givens'
1867 -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1868 -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1869 -- so the assert isn't true
1871 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
1872 addIrred want_scs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1873 addAvailAndSCs want_scs avails irred Irred
1875 addAvailAndSCs :: WantSCs -> Avails -> Inst -> Avail -> TcM Avails
1876 addAvailAndSCs want_scs avails inst avail
1877 | not (isClassDict inst) = return avails_with_inst
1878 | NoSCs <- want_scs = return avails_with_inst
1879 | otherwise = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
1880 ; addSCs is_loop avails_with_inst inst }
1882 avails_with_inst = addToFM avails inst avail
1884 is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
1885 -- Note: this compares by *type*, not by Unique
1886 deps = findAllDeps (unitVarSet (instToId inst)) avail
1887 dep_tys = map idType (varSetElems deps)
1889 findAllDeps :: IdSet -> Avail -> IdSet
1890 -- Find all the Insts that this one depends on
1891 -- See Note [SUPERCLASS-LOOP 2]
1892 -- Watch out, though. Since the avails may contain loops
1893 -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
1894 findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
1895 findAllDeps so_far other = so_far
1897 find_all :: IdSet -> Inst -> IdSet
1899 | kid_id `elemVarSet` so_far = so_far
1900 | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
1901 | otherwise = so_far'
1903 so_far' = extendVarSet so_far kid_id -- Add the new kid to so_far
1904 kid_id = instToId kid
1906 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
1907 -- Add all the superclasses of the Inst to Avails
1908 -- The first param says "dont do this because the original thing
1909 -- depends on this one, so you'd build a loop"
1910 -- Invariant: the Inst is already in Avails.
1912 addSCs is_loop avails dict
1913 = do { sc_dicts <- newDictsAtLoc (instLoc dict) sc_theta'
1914 ; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
1916 (clas, tys) = getDictClassTys dict
1917 (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1918 sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
1920 add_sc avails (sc_dict, sc_sel)
1921 | is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
1922 | is_given sc_dict = return avails
1923 | otherwise = addSCs is_loop avails' sc_dict
1925 sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
1926 avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
1928 is_given :: Inst -> Bool
1929 is_given sc_dict = case lookupFM avails sc_dict of
1930 Just (Given _ _) -> True -- Given is cheaper than superclass selection
1934 Note [SUPERCLASS-LOOP 2]
1935 ~~~~~~~~~~~~~~~~~~~~~~~~
1936 But the above isn't enough. Suppose we are *given* d1:Ord a,
1937 and want to deduce (d2:C [a]) where
1939 class Ord a => C a where
1940 instance Ord [a] => C [a] where ...
1942 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1943 superclasses of C [a] to avails. But we must not overwrite the binding
1944 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1947 Here's another variant, immortalised in tcrun020
1948 class Monad m => C1 m
1949 class C1 m => C2 m x
1950 instance C2 Maybe Bool
1951 For the instance decl we need to build (C1 Maybe), and it's no good if
1952 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1953 before we search for C1 Maybe.
1955 Here's another example
1956 class Eq b => Foo a b
1957 instance Eq a => Foo [a] a
1961 we'll first deduce that it holds (via the instance decl). We must not
1962 then overwrite the Eq t constraint with a superclass selection!
1964 At first I had a gross hack, whereby I simply did not add superclass constraints
1965 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1966 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1967 I found a very obscure program (now tcrun021) in which improvement meant the
1968 simplifier got two bites a the cherry... so something seemed to be an Irred
1969 first time, but reducible next time.
1971 Now we implement the Right Solution, which is to check for loops directly
1972 when adding superclasses. It's a bit like the occurs check in unification.
1975 Note [RECURSIVE DICTIONARIES]
1976 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1978 data D r = ZeroD | SuccD (r (D r));
1980 instance (Eq (r (D r))) => Eq (D r) where
1981 ZeroD == ZeroD = True
1982 (SuccD a) == (SuccD b) = a == b
1985 equalDC :: D [] -> D [] -> Bool;
1988 We need to prove (Eq (D [])). Here's how we go:
1992 by instance decl, holds if
1996 by instance decl of Eq, holds if
1998 where d2 = dfEqList d3
2001 But now we can "tie the knot" to give
2007 and it'll even run! The trick is to put the thing we are trying to prove
2008 (in this case Eq (D []) into the database before trying to prove its
2009 contributing clauses.
2012 %************************************************************************
2014 \section{tcSimplifyTop: defaulting}
2016 %************************************************************************
2019 @tcSimplifyTop@ is called once per module to simplify all the constant
2020 and ambiguous Insts.
2022 We need to be careful of one case. Suppose we have
2024 instance Num a => Num (Foo a b) where ...
2026 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)). Then it'll simplify
2027 to (Num x), and default x to Int. But what about y??
2029 It's OK: the final zonking stage should zap y to (), which is fine.
2033 tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
2034 tcSimplifyTop wanteds
2035 = do { ext_default <- doptM Opt_ExtendedDefaultRules
2036 ; tc_simplify_top doc ext_default AddSCs wanteds }
2038 doc = text "tcSimplifyTop"
2040 tcSimplifyInteractive wanteds
2041 = tc_simplify_top doc True {- Interactive loop -} AddSCs wanteds
2043 doc = text "tcSimplifyTop"
2045 -- The TcLclEnv should be valid here, solely to improve
2046 -- error message generation for the monomorphism restriction
2047 tc_simplify_top doc use_extended_defaulting want_scs wanteds
2048 = do { lcl_env <- getLclEnv
2049 ; traceTc (text "tcSimplifyTop" <+> ppr (lclEnvElts lcl_env))
2051 ; let try_me inst = ReduceMe want_scs
2052 ; (frees, binds, irreds) <- simpleReduceLoop doc try_me wanteds
2055 -- First get rid of implicit parameters
2056 (non_ips, bad_ips) = partition isClassDict irreds
2058 -- All the non-tv or multi-param ones are definite errors
2059 (unary_tv_dicts, non_tvs) = partition is_unary_tyvar_dict non_ips
2060 bad_tyvars = unionVarSets (map tyVarsOfInst non_tvs)
2062 -- Group by type variable
2063 tv_groups = equivClasses cmp_by_tyvar unary_tv_dicts
2065 -- Pick the ones which its worth trying to disambiguate
2066 -- namely, the ones whose type variable isn't bound
2067 -- up with one of the non-tyvar classes
2068 (default_gps, non_default_gps) = partition defaultable_group tv_groups
2069 defaultable_group ds
2070 = not (bad_tyvars `intersectsVarSet` tyVarsOfInst (head ds))
2071 && defaultable_classes (map get_clas ds)
2072 defaultable_classes clss
2073 | use_extended_defaulting = any isInteractiveClass clss
2074 | otherwise = all isStandardClass clss && any isNumericClass clss
2076 isInteractiveClass cls = isNumericClass cls
2077 || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
2078 -- In interactive mode, or with -fextended-default-rules,
2079 -- we default Show a to Show () to avoid graututious errors on "show []"
2082 -- Collect together all the bad guys
2083 bad_guys = non_tvs ++ concat non_default_gps
2084 (ambigs, no_insts) = partition isTyVarDict bad_guys
2085 -- If the dict has no type constructors involved, it must be ambiguous,
2086 -- except I suppose that another error with fundeps maybe should have
2087 -- constrained those type variables
2089 -- Report definite errors
2090 ; ASSERT( null frees )
2091 groupErrs (addNoInstanceErrs Nothing []) no_insts
2092 ; strangeTopIPErrs bad_ips
2094 -- Deal with ambiguity errors, but only if
2095 -- if there has not been an error so far:
2096 -- errors often give rise to spurious ambiguous Insts.
2098 -- f = (*) -- Monomorphic
2099 -- g :: Num a => a -> a
2101 -- Here, we get a complaint when checking the type signature for g,
2102 -- that g isn't polymorphic enough; but then we get another one when
2103 -- dealing with the (Num a) context arising from f's definition;
2104 -- we try to unify a with Int (to default it), but find that it's
2105 -- already been unified with the rigid variable from g's type sig
2106 ; binds_ambig <- ifErrsM (returnM []) $
2107 do { -- Complain about the ones that don't fall under
2108 -- the Haskell rules for disambiguation
2109 -- This group includes both non-existent instances
2110 -- e.g. Num (IO a) and Eq (Int -> Int)
2111 -- and ambiguous dictionaries
2113 addTopAmbigErrs ambigs
2115 -- Disambiguate the ones that look feasible
2116 ; mappM disambigGroup default_gps }
2118 ; return (binds `unionBags` unionManyBags binds_ambig) }
2120 ----------------------------------
2121 d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
2123 is_unary_tyvar_dict :: Inst -> Bool -- Dicts of form (C a)
2124 -- Invariant: argument is a ClassDict, not IP or method
2125 is_unary_tyvar_dict d = case getDictClassTys d of
2126 (_, [ty]) -> tcIsTyVarTy ty
2129 get_tv d = case getDictClassTys d of
2130 (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
2131 get_clas d = case getDictClassTys d of
2135 If a dictionary constrains a type variable which is
2136 * not mentioned in the environment
2137 * and not mentioned in the type of the expression
2138 then it is ambiguous. No further information will arise to instantiate
2139 the type variable; nor will it be generalised and turned into an extra
2140 parameter to a function.
2142 It is an error for this to occur, except that Haskell provided for
2143 certain rules to be applied in the special case of numeric types.
2145 * at least one of its classes is a numeric class, and
2146 * all of its classes are numeric or standard
2147 then the type variable can be defaulted to the first type in the
2148 default-type list which is an instance of all the offending classes.
2150 So here is the function which does the work. It takes the ambiguous
2151 dictionaries and either resolves them (producing bindings) or
2152 complains. It works by splitting the dictionary list by type
2153 variable, and using @disambigOne@ to do the real business.
2155 @disambigOne@ assumes that its arguments dictionaries constrain all
2156 the same type variable.
2158 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
2159 @()@ instead of @Int@. I reckon this is the Right Thing to do since
2160 the most common use of defaulting is code like:
2162 _ccall_ foo `seqPrimIO` bar
2164 Since we're not using the result of @foo@, the result if (presumably)
2168 disambigGroup :: [Inst] -- All standard classes of form (C a)
2172 = -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
2173 -- SO, TRY DEFAULT TYPES IN ORDER
2175 -- Failure here is caused by there being no type in the
2176 -- default list which can satisfy all the ambiguous classes.
2177 -- For example, if Real a is reqd, but the only type in the
2178 -- default list is Int.
2179 get_default_tys `thenM` \ default_tys ->
2181 try_default [] -- No defaults work, so fail
2184 try_default (default_ty : default_tys)
2185 = tryTcLIE_ (try_default default_tys) $ -- If default_ty fails, we try
2186 -- default_tys instead
2187 tcSimplifyDefault theta `thenM` \ _ ->
2190 theta = [mkClassPred clas [default_ty] | clas <- classes]
2192 -- See if any default works
2193 tryM (try_default default_tys) `thenM` \ mb_ty ->
2196 Right chosen_default_ty -> choose_default chosen_default_ty
2198 tyvar = get_tv (head dicts) -- Should be non-empty
2199 classes = map get_clas dicts
2201 choose_default default_ty -- Commit to tyvar = default_ty
2202 = -- Bind the type variable
2203 unifyType default_ty (mkTyVarTy tyvar) `thenM_`
2204 -- and reduce the context, for real this time
2205 simpleReduceLoop (text "disambig" <+> ppr dicts)
2206 reduceMe dicts `thenM` \ (frees, binds, ambigs) ->
2207 WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
2208 warnDefault dicts default_ty `thenM_`
2211 bomb_out = addTopAmbigErrs dicts `thenM_`
2215 = do { mb_defaults <- getDefaultTys
2216 ; case mb_defaults of
2217 Just tys -> return tys
2218 Nothing -> -- No use-supplied default;
2219 -- use [Integer, Double]
2220 do { integer_ty <- tcMetaTy integerTyConName
2221 ; checkWiredInTyCon doubleTyCon
2222 ; return [integer_ty, doubleTy] } }
2225 [Aside - why the defaulting mechanism is turned off when
2226 dealing with arguments and results to ccalls.
2228 When typechecking _ccall_s, TcExpr ensures that the external
2229 function is only passed arguments (and in the other direction,
2230 results) of a restricted set of 'native' types.
2232 The interaction between the defaulting mechanism for numeric
2233 values and CC & CR can be a bit puzzling to the user at times.
2242 What type has 'x' got here? That depends on the default list
2243 in operation, if it is equal to Haskell 98's default-default
2244 of (Integer, Double), 'x' has type Double, since Integer
2245 is not an instance of CR. If the default list is equal to
2246 Haskell 1.4's default-default of (Int, Double), 'x' has type
2252 %************************************************************************
2254 \subsection[simple]{@Simple@ versions}
2256 %************************************************************************
2258 Much simpler versions when there are no bindings to make!
2260 @tcSimplifyThetas@ simplifies class-type constraints formed by
2261 @deriving@ declarations and when specialising instances. We are
2262 only interested in the simplified bunch of class/type constraints.
2264 It simplifies to constraints of the form (C a b c) where
2265 a,b,c are type variables. This is required for the context of
2266 instance declarations.
2269 tcSimplifyDeriv :: TyCon
2271 -> ThetaType -- Wanted
2272 -> TcM ThetaType -- Needed
2274 tcSimplifyDeriv tc tyvars theta
2275 = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
2276 -- The main loop may do unification, and that may crash if
2277 -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
2278 -- ToDo: what if two of them do get unified?
2279 newDicts DerivOrigin (substTheta tenv theta) `thenM` \ wanteds ->
2280 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2281 ASSERT( null frees ) -- reduceMe never returns Free
2283 doptM Opt_GlasgowExts `thenM` \ gla_exts ->
2284 doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
2286 tv_set = mkVarSet tvs
2288 (bad_insts, ok_insts) = partition is_bad_inst irreds
2290 = let pred = dictPred dict -- reduceMe squashes all non-dicts
2291 in isEmptyVarSet (tyVarsOfPred pred)
2292 -- Things like (Eq T) are bad
2293 || (not gla_exts && not (isTyVarClassPred pred))
2295 simpl_theta = map dictPred ok_insts
2296 weird_preds = [pred | pred <- simpl_theta
2297 , not (tyVarsOfPred pred `subVarSet` tv_set)]
2298 -- Check for a bizarre corner case, when the derived instance decl should
2299 -- have form instance C a b => D (T a) where ...
2300 -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
2301 -- of problems; in particular, it's hard to compare solutions for
2302 -- equality when finding the fixpoint. So I just rule it out for now.
2304 rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
2305 -- This reverse-mapping is a Royal Pain,
2306 -- but the result should mention TyVars not TcTyVars
2309 addNoInstanceErrs Nothing [] bad_insts `thenM_`
2310 mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
2311 returnM (substTheta rev_env simpl_theta)
2313 doc = ptext SLIT("deriving classes for a data type")
2316 @tcSimplifyDefault@ just checks class-type constraints, essentially;
2317 used with \tr{default} declarations. We are only interested in
2318 whether it worked or not.
2321 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
2324 tcSimplifyDefault theta
2325 = newDicts DefaultOrigin theta `thenM` \ wanteds ->
2326 simpleReduceLoop doc reduceMe wanteds `thenM` \ (frees, _, irreds) ->
2327 ASSERT( null frees ) -- try_me never returns Free
2328 addNoInstanceErrs Nothing [] irreds `thenM_`
2334 doc = ptext SLIT("default declaration")
2338 %************************************************************************
2340 \section{Errors and contexts}
2342 %************************************************************************
2344 ToDo: for these error messages, should we note the location as coming
2345 from the insts, or just whatever seems to be around in the monad just
2349 groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
2350 -> [Inst] -- The offending Insts
2352 -- Group together insts with the same origin
2353 -- We want to report them together in error messages
2355 groupErrs report_err []
2357 groupErrs report_err (inst:insts)
2358 = do_one (inst:friends) `thenM_`
2359 groupErrs report_err others
2362 -- (It may seem a bit crude to compare the error messages,
2363 -- but it makes sure that we combine just what the user sees,
2364 -- and it avoids need equality on InstLocs.)
2365 (friends, others) = partition is_friend insts
2366 loc_msg = showSDoc (pprInstLoc (instLoc inst))
2367 is_friend friend = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
2368 do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
2369 -- Add location and context information derived from the Insts
2371 -- Add the "arising from..." part to a message about bunch of dicts
2372 addInstLoc :: [Inst] -> Message -> Message
2373 addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
2375 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
2376 addTopIPErrs bndrs []
2378 addTopIPErrs bndrs ips
2379 = addErrTcM (tidy_env, mk_msg tidy_ips)
2381 (tidy_env, tidy_ips) = tidyInsts ips
2382 mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
2383 nest 2 (ptext SLIT("the monomorphic top-level binding(s) of")
2384 <+> pprBinders bndrs <> colon)],
2385 nest 2 (vcat (map ppr_ip ips)),
2387 ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
2389 strangeTopIPErrs :: [Inst] -> TcM ()
2390 strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
2391 = groupErrs report tidy_dicts
2393 (tidy_env, tidy_dicts) = tidyInsts dicts
2394 report dicts = addErrTcM (tidy_env, mk_msg dicts)
2395 mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <>
2396 plural tidy_dicts <+> pprDictsTheta tidy_dicts)
2398 addNoInstanceErrs :: Maybe SDoc -- Nothing => top level
2399 -- Just d => d describes the construct
2400 -> [Inst] -- What is given by the context or type sig
2401 -> [Inst] -- What is wanted
2403 addNoInstanceErrs mb_what givens []
2405 addNoInstanceErrs mb_what givens dicts
2406 = -- Some of the dicts are here because there is no instances
2407 -- and some because there are too many instances (overlap)
2408 tcGetInstEnvs `thenM` \ inst_envs ->
2410 (tidy_env1, tidy_givens) = tidyInsts givens
2411 (tidy_env2, tidy_dicts) = tidyMoreInsts tidy_env1 dicts
2413 -- Run through the dicts, generating a message for each
2414 -- overlapping one, but simply accumulating all the
2415 -- no-instance ones so they can be reported as a group
2416 (overlap_doc, no_inst_dicts) = foldl check_overlap (empty, []) tidy_dicts
2417 check_overlap (overlap_doc, no_inst_dicts) dict
2418 | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
2420 = case lookupInstEnv inst_envs clas tys of
2421 -- The case of exactly one match and no unifiers means
2422 -- a successful lookup. That can't happen here, becuase
2423 -- dicts only end up here if they didn't match in Inst.lookupInst
2425 ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
2427 ([], _) -> (overlap_doc, dict : no_inst_dicts) -- No match
2428 res -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
2430 (clas,tys) = getDictClassTys dict
2433 -- Now generate a good message for the no-instance bunch
2434 mk_probable_fix tidy_env2 no_inst_dicts `thenM` \ (tidy_env3, probable_fix) ->
2436 no_inst_doc | null no_inst_dicts = empty
2437 | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
2438 heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+>
2439 ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
2440 | otherwise = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
2441 nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
2443 -- And emit both the non-instance and overlap messages
2444 addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
2446 mk_overlap_msg dict (matches, unifiers)
2447 = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for")
2448 <+> pprPred (dictPred dict))),
2449 sep [ptext SLIT("Matching instances") <> colon,
2450 nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
2451 ASSERT( not (null matches) )
2452 if not (isSingleton matches)
2453 then -- Two or more matches
2455 else -- One match, plus some unifiers
2456 ASSERT( not (null unifiers) )
2457 parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
2458 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
2459 ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
2461 ispecs = [ispec | (_, ispec) <- matches]
2463 mk_probable_fix tidy_env dicts
2464 = returnM (tidy_env, sep [ptext SLIT("Possible fix:"), nest 2 (vcat fixes)])
2466 fixes = add_ors (fix1 ++ fix2)
2468 fix1 = case mb_what of
2469 Nothing -> [] -- Top level
2470 Just what -> -- Nested (type signatures, instance decls)
2471 [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
2472 ptext SLIT("to the") <+> what] ]
2474 fix2 | null instance_dicts = []
2475 | otherwise = [ sep [ptext SLIT("add an instance declaration for"),
2476 pprDictsTheta instance_dicts] ]
2477 instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
2478 -- Insts for which it is worth suggesting an adding an instance declaration
2479 -- Exclude implicit parameters, and tyvar dicts
2481 add_ors :: [SDoc] -> [SDoc] -- The empty case should not happen
2482 add_ors [] = [ptext SLIT("[No suggested fixes]")] -- Strange
2483 add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
2485 addTopAmbigErrs dicts
2486 -- Divide into groups that share a common set of ambiguous tyvars
2487 = mapM report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
2489 (tidy_env, tidy_dicts) = tidyInsts dicts
2491 tvs_of :: Inst -> [TcTyVar]
2492 tvs_of d = varSetElems (tyVarsOfInst d)
2493 cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
2495 report :: [(Inst,[TcTyVar])] -> TcM ()
2496 report pairs@((inst,tvs) : _) -- The pairs share a common set of ambiguous tyvars
2497 = mkMonomorphismMsg tidy_env tvs `thenM` \ (tidy_env, mono_msg) ->
2498 setSrcSpan (instLocSrcSpan (instLoc inst)) $
2499 -- the location of the first one will do for the err message
2500 addErrTcM (tidy_env, msg $$ mono_msg)
2502 dicts = map fst pairs
2503 msg = sep [text "Ambiguous type variable" <> plural tvs <+>
2504 pprQuotedList tvs <+> in_msg,
2505 nest 2 (pprDictsInFull dicts)]
2506 in_msg = text "in the constraint" <> plural dicts <> colon
2509 mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
2510 -- There's an error with these Insts; if they have free type variables
2511 -- it's probably caused by the monomorphism restriction.
2512 -- Try to identify the offending variable
2513 -- ASSUMPTION: the Insts are fully zonked
2514 mkMonomorphismMsg tidy_env inst_tvs
2515 = findGlobals (mkVarSet inst_tvs) tidy_env `thenM` \ (tidy_env, docs) ->
2516 returnM (tidy_env, mk_msg docs)
2518 mk_msg [] = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
2519 -- This happens in things like
2520 -- f x = show (read "foo")
2521 -- whre monomorphism doesn't play any role
2522 mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
2526 monomorphism_fix :: SDoc
2527 monomorphism_fix = ptext SLIT("Probable fix:") <+>
2528 (ptext SLIT("give these definition(s) an explicit type signature")
2529 $$ ptext SLIT("or use -fno-monomorphism-restriction"))
2531 warnDefault dicts default_ty
2532 = doptM Opt_WarnTypeDefaults `thenM` \ warn_flag ->
2533 addInstCtxt (instLoc (head dicts)) (warnTc warn_flag warn_msg)
2536 (_, tidy_dicts) = tidyInsts dicts
2537 warn_msg = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
2538 quotes (ppr default_ty),
2539 pprDictsInFull tidy_dicts]
2541 -- Used for the ...Thetas variants; all top level
2543 = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2544 ptext SLIT("type variables that are not data type parameters"),
2545 nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2547 reduceDepthErr n stack
2548 = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2549 ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
2550 nest 4 (pprStack stack)]
2552 pprStack stack = vcat (map pprInstInFull stack)