ghc/compiler/typecheck/TcSimplify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcSimplify]{TcSimplify}
   5
   6
   7
   8 \begin{code}
   9 module TcSimplify (
  10         tcSimplifyInfer, tcSimplifyInferCheck,
  11         tcSimplifyCheck, tcSimplifyRestricted,
  12         tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop,
  13
  14         tcSimplifyThetas, tcSimplifyCheckThetas,
  15         bindInstsOfLocalFuns
  16     ) where
  17
  18 #include "HsVersions.h"
  19
  20 import HsSyn            ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
  21 import TcHsSyn          ( TcExpr, TcId,
  22                           TcMonoBinds, TcDictBinds
  23                         )
  24
  25 import TcMonad
  26 import Inst             ( lookupInst, lookupSimpleInst, LookupInstResult(..),
  27                           tyVarsOfInst, predsOfInsts, predsOfInst,
  28                           isDict, isClassDict,
  29                           isStdClassTyVarDict, isMethodFor,
  30                           instToId, tyVarsOfInsts,
  31                           ipNamesOfInsts, ipNamesOfInst,
  32                           instBindingRequired, instCanBeGeneralised,
  33                           newDictsFromOld,
  34                           getDictClassTys, isTyVarDict,
  35                           instLoc, pprInst, zonkInst, tidyInsts, tidyMoreInsts,
  36                           Inst, LIE, pprInsts, pprInstsInFull,
  37                           mkLIE, lieToList
  38                         )
  39 import TcEnv            ( tcGetGlobalTyVars, tcGetInstEnv )
  40 import InstEnv          ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
  41
  42 import TcMType          ( zonkTcTyVarsAndFV, tcInstTyVars, unifyTauTy )
  43 import TcType           ( ThetaType, PredType, mkClassPred, isOverloadedTy,
  44                           mkTyVarTy, tcGetTyVar, isTyVarClassPred,
  45                           tyVarsOfPred, getClassPredTys_maybe, isClassPred, isIPPred,
  46                           inheritablePred, predHasFDs )
  47 import Id               ( idType )
  48 import NameSet          ( NameSet, mkNameSet, elemNameSet )
  49 import Class            ( classBigSig )
  50 import FunDeps          ( oclose, grow, improve, pprEquationDoc )
  51 import PrelInfo         ( isNumericClass, isCreturnableClass, isCcallishClass )
  52
  53 import Subst            ( mkTopTyVarSubst, substTheta, substTy )
  54 import TysWiredIn       ( unitTy )
  55 import VarSet
  56 import FiniteMap
  57 import Outputable
  58 import ListSetOps       ( equivClasses )
  59 import Util             ( zipEqual )
  60 import List             ( partition )
  61 import CmdLineOpts
  62 \end{code}
  63
  64
  65 %************************************************************************
  66 %*                                                                      *
  67 \subsection{NOTES}
  68 %*                                                                      *
  69 %************************************************************************
  70
  71         --------------------------------------
  72                 Notes on quantification
  73         --------------------------------------
  74
  75 Suppose we are about to do a generalisation step.
  76 We have in our hand
  77
  78         G       the environment
  79         T       the type of the RHS
  80         C       the constraints from that RHS
  81
  82 The game is to figure out
  83
  84         Q       the set of type variables over which to quantify
  85         Ct      the constraints we will *not* quantify over
  86         Cq      the constraints we will quantify over
  87
  88 So we're going to infer the type
  89
  90         forall Q. Cq => T
  91
  92 and float the constraints Ct further outwards.
  93
  94 Here are the things that *must* be true:
  95
  96  (A)    Q intersect fv(G) = EMPTY                       limits how big Q can be
  97  (B)    Q superset fv(Cq union T) \ oclose(fv(G),C)     limits how small Q can be
  98
  99 (A) says we can't quantify over a variable that's free in the
 100 environment.  (B) says we must quantify over all the truly free
 101 variables in T, else we won't get a sufficiently general type.  We do
 102 not *need* to quantify over any variable that is fixed by the free
 103 vars of the environment G.
 104
 105         BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
 106
 107 Example:        class H x y | x->y where ...
 108
 109         fv(G) = {a}     C = {H a b, H c d}
 110                         T = c -> b
 111
 112         (A)  Q intersect {a} is empty
 113         (B)  Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
 114
 115         So Q can be {c,d}, {b,c,d}
 116
 117 Other things being equal, however, we'd like to quantify over as few
 118 variables as possible: smaller types, fewer type applications, more
 119 constraints can get into Ct instead of Cq.
 120
 121
 122 -----------------------------------------
 123 We will make use of
 124
 125   fv(T)         the free type vars of T
 126
 127   oclose(vs,C)  The result of extending the set of tyvars vs
 128                 using the functional dependencies from C
 129
 130   grow(vs,C)    The result of extend the set of tyvars vs
 131                 using all conceivable links from C.
 132
 133                 E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
 134                 Then grow(vs,C) = {a,b,c}
 135
 136                 Note that grow(vs,C) `superset` grow(vs,simplify(C))
 137                 That is, simplfication can only shrink the result of grow.
 138
 139 Notice that
 140    oclose is conservative one way:      v `elem` oclose(vs,C) => v is definitely fixed by vs
 141    grow is conservative the other way:  if v might be fixed by vs => v `elem` grow(vs,C)
 142
 143
 144 -----------------------------------------
 145
 146 Choosing Q
 147 ~~~~~~~~~~
 148 Here's a good way to choose Q:
 149
 150         Q = grow( fv(T), C ) \ oclose( fv(G), C )
 151
 152 That is, quantify over all variable that that MIGHT be fixed by the
 153 call site (which influences T), but which aren't DEFINITELY fixed by
 154 G.  This choice definitely quantifies over enough type variables,
 155 albeit perhaps too many.
 156
 157 Why grow( fv(T), C ) rather than fv(T)?  Consider
 158
 159         class H x y | x->y where ...
 160
 161         T = c->c
 162         C = (H c d)
 163
 164   If we used fv(T) = {c} we'd get the type
 165
 166         forall c. H c d => c -> b
 167
 168   And then if the fn was called at several different c's, each of
 169   which fixed d differently, we'd get a unification error, because
 170   d isn't quantified.  Solution: quantify d.  So we must quantify
 171   everything that might be influenced by c.
 172
 173 Why not oclose( fv(T), C )?  Because we might not be able to see
 174 all the functional dependencies yet:
 175
 176         class H x y | x->y where ...
 177         instance H x y => Eq (T x y) where ...
 178
 179         T = c->c
 180         C = (Eq (T c d))
 181
 182   Now oclose(fv(T),C) = {c}, because the functional dependency isn't
 183   apparent yet, and that's wrong.  We must really quantify over d too.
 184
 185
 186 There really isn't any point in quantifying over any more than
 187 grow( fv(T), C ), because the call sites can't possibly influence
 188 any other type variables.
 189
 190
 191
 192         --------------------------------------
 193                 Notes on ambiguity
 194         --------------------------------------
 195
 196 It's very hard to be certain when a type is ambiguous.  Consider
 197
 198         class K x
 199         class H x y | x -> y
 200         instance H x y => K (x,y)
 201
 202 Is this type ambiguous?
 203         forall a b. (K (a,b), Eq b) => a -> a
 204
 205 Looks like it!  But if we simplify (K (a,b)) we get (H a b) and
 206 now we see that a fixes b.  So we can't tell about ambiguity for sure
 207 without doing a full simplification.  And even that isn't possible if
 208 the context has some free vars that may get unified.  Urgle!
 209
 210 Here's another example: is this ambiguous?
 211         forall a b. Eq (T b) => a -> a
 212 Not if there's an insance decl (with no context)
 213         instance Eq (T b) where ...
 214
 215 You may say of this example that we should use the instance decl right
 216 away, but you can't always do that:
 217
 218         class J a b where ...
 219         instance J Int b where ...
 220
 221         f :: forall a b. J a b => a -> a
 222
 223 (Notice: no functional dependency in J's class decl.)
 224 Here f's type is perfectly fine, provided f is only called at Int.
 225 It's premature to complain when meeting f's signature, or even
 226 when inferring a type for f.
 227
 228
 229
 230 However, we don't *need* to report ambiguity right away.  It'll always
 231 show up at the call site.... and eventually at main, which needs special
 232 treatment.  Nevertheless, reporting ambiguity promptly is an excellent thing.
 233
 234 So here's the plan.  We WARN about probable ambiguity if
 235
 236         fv(Cq) is not a subset of  oclose(fv(T) union fv(G), C)
 237
 238 (all tested before quantification).
 239 That is, all the type variables in Cq must be fixed by the the variables
 240 in the environment, or by the variables in the type.
 241
 242 Notice that we union before calling oclose.  Here's an example:
 243
 244         class J a b c | a b -> c
 245         fv(G) = {a}
 246
 247 Is this ambiguous?
 248         forall b c. (J a b c) => b -> b
 249
 250 Only if we union {a} from G with {b} from T before using oclose,
 251 do we see that c is fixed.
 252
 253 It's a bit vague exactly which C we should use for this oclose call.  If we
 254 don't fix enough variables we might complain when we shouldn't (see
 255 the above nasty example).  Nothing will be perfect.  That's why we can
 256 only issue a warning.
 257
 258
 259 Can we ever be *certain* about ambiguity?  Yes: if there's a constraint
 260
 261         c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
 262
 263 then c is a "bubble"; there's no way it can ever improve, and it's
 264 certainly ambiguous.  UNLESS it is a constant (sigh).  And what about
 265 the nasty example?
 266
 267         class K x
 268         class H x y | x -> y
 269         instance H x y => K (x,y)
 270
 271 Is this type ambiguous?
 272         forall a b. (K (a,b), Eq b) => a -> a
 273
 274 Urk.  The (Eq b) looks "definitely ambiguous" but it isn't.  What we are after
 275 is a "bubble" that's a set of constraints
 276
 277         Cq = Ca union Cq'  st  fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
 278
 279 Hence another idea.  To decide Q start with fv(T) and grow it
 280 by transitive closure in Cq (no functional dependencies involved).
 281 Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
 282 The definitely-ambiguous can then float out, and get smashed at top level
 283 (which squashes out the constants, like Eq (T a) above)
 284
 285
 286         --------------------------------------
 287                 Notes on principal types
 288         --------------------------------------
 289
 290     class C a where
 291       op :: a -> a
 292
 293     f x = let g y = op (y::Int) in True
 294
 295 Here the principal type of f is (forall a. a->a)
 296 but we'll produce the non-principal type
 297     f :: forall a. C Int => a -> a
 298
 299
 300         --------------------------------------
 301                 Notes on implicit parameters
 302         --------------------------------------
 303
 304 Question 1: can we "inherit" implicit parameters
 305 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 306 Consider this:
 307
 308         f x = (x::Int) + ?y
 309
 310 where f is *not* a top-level binding.
 311 From the RHS of f we'll get the constraint (?y::Int).
 312 There are two types we might infer for f:
 313
 314         f :: Int -> Int
 315
 316 (so we get ?y from the context of f's definition), or
 317
 318         f :: (?y::Int) => Int -> Int
 319
 320 At first you might think the first was better, becuase then
 321 ?y behaves like a free variable of the definition, rather than
 322 having to be passed at each call site.  But of course, the WHOLE
 323 IDEA is that ?y should be passed at each call site (that's what
 324 dynamic binding means) so we'd better infer the second.
 325
 326 BOTTOM LINE: when *inferring types* you *must* quantify
 327 over implicit parameters. See the predicate isFreeWhenInferring.
 328
 329
 330 Question 2: type signatures
 331 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 332 BUT WATCH OUT: When you supply a type signature, we can't force you
 333 to quantify over implicit parameters.  For example:
 334
 335         (?x + 1) :: Int
 336
 337 This is perfectly reasonable.  We do not want to insist on
 338
 339         (?x + 1) :: (?x::Int => Int)
 340
 341 That would be silly.  Here, the definition site *is* the occurrence site,
 342 so the above strictures don't apply.  Hence the difference between
 343 tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
 344 and tcSimplifyCheckBind (which does not).
 345
 346 What about when you supply a type signature for a binding?
 347 Is it legal to give the following explicit, user type
 348 signature to f, thus:
 349
 350         f :: Int -> Int
 351         f x = (x::Int) + ?y
 352
 353 At first sight this seems reasonable, but it has the nasty property
 354 that adding a type signature changes the dynamic semantics.
 355 Consider this:
 356
 357         (let f x = (x::Int) + ?y
 358          in (f 3, f 3 with ?y=5))  with ?y = 6
 359
 360                 returns (3+6, 3+5)
 361 vs
 362         (let f :: Int -> Int
 363              f x = x + ?y
 364          in (f 3, f 3 with ?y=5))  with ?y = 6
 365
 366                 returns (3+6, 3+6)
 367
 368 Indeed, simply inlining f (at the Haskell source level) would change the
 369 dynamic semantics.
 370
 371 Nevertheless, as Launchbury says (email Oct 01) we can't really give the
 372 semantics for a Haskell program without knowing its typing, so if you
 373 change the typing you may change the semantics.
 374
 375 To make things consistent in all cases where we are *checking* against
 376 a supplied signature (as opposed to inferring a type), we adopt the
 377 rule:
 378
 379         a signature does not need to quantify over implicit params.
 380
 381 [This represents a (rather marginal) change of policy since GHC 5.02,
 382 which *required* an explicit signature to quantify over all implicit
 383 params for the reasons mentioned above.]
 384
 385 But that raises a new question.  Consider
 386
 387         Given (signature)       ?x::Int
 388         Wanted (inferred)       ?x::Int, ?y::Bool
 389
 390 Clearly we want to discharge the ?x and float the ?y out.  But
 391 what is the criterion that distinguishes them?  Clearly it isn't
 392 what free type variables they have.  The Right Thing seems to be
 393 to float a constraint that
 394         neither mentions any of the quantified type variables
 395         nor any of the quantified implicit parameters
 396
 397 See the predicate isFreeWhenChecking.
 398
 399
 400 Question 3: monomorphism
 401 ~~~~~~~~~~~~~~~~~~~~~~~~
 402 There's a nasty corner case when the monomorphism restriction bites:
 403
 404         z = (x::Int) + ?y
 405
 406 The argument above suggests that we *must* generalise
 407 over the ?y parameter, to get
 408         z :: (?y::Int) => Int,
 409 but the monomorphism restriction says that we *must not*, giving
 410         z :: Int.
 411 Why does the momomorphism restriction say this?  Because if you have
 412
 413         let z = x + ?y in z+z
 414
 415 you might not expect the addition to be done twice --- but it will if
 416 we follow the argument of Question 2 and generalise over ?y.
 417
 418
 419
 420 Possible choices
 421 ~~~~~~~~~~~~~~~~
 422 (A) Always generalise over implicit parameters
 423     Bindings that fall under the monomorphism restriction can't
 424         be generalised
 425
 426     Consequences:
 427         * Inlining remains valid
 428         * No unexpected loss of sharing
 429         * But simple bindings like
 430                 z = ?y + 1
 431           will be rejected, unless you add an explicit type signature
 432           (to avoid the monomorphism restriction)
 433                 z :: (?y::Int) => Int
 434                 z = ?y + 1
 435           This seems unacceptable
 436
 437 (B) Monomorphism restriction "wins"
 438     Bindings that fall under the monomorphism restriction can't
 439         be generalised
 440     Always generalise over implicit parameters *except* for bindings
 441         that fall under the monomorphism restriction
 442
 443     Consequences
 444         * Inlining isn't valid in general
 445         * No unexpected loss of sharing
 446         * Simple bindings like
 447                 z = ?y + 1
 448           accepted (get value of ?y from binding site)
 449
 450 (C) Always generalise over implicit parameters
 451     Bindings that fall under the monomorphism restriction can't
 452         be generalised, EXCEPT for implicit parameters
 453     Consequences
 454         * Inlining remains valid
 455         * Unexpected loss of sharing (from the extra generalisation)
 456         * Simple bindings like
 457                 z = ?y + 1
 458           accepted (get value of ?y from occurrence sites)
 459
 460
 461 Discussion
 462 ~~~~~~~~~~
 463 None of these choices seems very satisfactory.  But at least we should
 464 decide which we want to do.
 465
 466 It's really not clear what is the Right Thing To Do.  If you see
 467
 468         z = (x::Int) + ?y
 469
 470 would you expect the value of ?y to be got from the *occurrence sites*
 471 of 'z', or from the valuue of ?y at the *definition* of 'z'?  In the
 472 case of function definitions, the answer is clearly the former, but
 473 less so in the case of non-fucntion definitions.   On the other hand,
 474 if we say that we get the value of ?y from the definition site of 'z',
 475 then inlining 'z' might change the semantics of the program.
 476
 477 Choice (C) really says "the monomorphism restriction doesn't apply
 478 to implicit parameters".  Which is fine, but remember that every
 479 innocent binding 'x = ...' that mentions an implicit parameter in
 480 the RHS becomes a *function* of that parameter, called at each
 481 use of 'x'.  Now, the chances are that there are no intervening 'with'
 482 clauses that bind ?y, so a decent compiler should common up all
 483 those function calls.  So I think I strongly favour (C).  Indeed,
 484 one could make a similar argument for abolishing the monomorphism
 485 restriction altogether.
 486
 487 BOTTOM LINE: we choose (B) at present.  See tcSimplifyRestricted
 488
 489
 490
 491 %************************************************************************
 492 %*                                                                      *
 493 \subsection{tcSimplifyInfer}
 494 %*                                                                      *
 495 %************************************************************************
 496
 497 tcSimplify is called when we *inferring* a type.  Here's the overall game plan:
 498
 499     1. Compute Q = grow( fvs(T), C )
 500
 501     2. Partition C based on Q into Ct and Cq.  Notice that ambiguous
 502        predicates will end up in Ct; we deal with them at the top level
 503
 504     3. Try improvement, using functional dependencies
 505
 506     4. If Step 3 did any unification, repeat from step 1
 507        (Unification can change the result of 'grow'.)
 508
 509 Note: we don't reduce dictionaries in step 2.  For example, if we have
 510 Eq (a,b), we don't simplify to (Eq a, Eq b).  So Q won't be different
 511 after step 2.  However note that we may therefore quantify over more
 512 type variables than we absolutely have to.
 513
 514 For the guts, we need a loop, that alternates context reduction and
 515 improvement with unification.  E.g. Suppose we have
 516
 517         class C x y | x->y where ...
 518
 519 and tcSimplify is called with:
 520         (C Int a, C Int b)
 521 Then improvement unifies a with b, giving
 522         (C Int a, C Int a)
 523
 524 If we need to unify anything, we rattle round the whole thing all over
 525 again.
 526
 527
 528 \begin{code}
 529 tcSimplifyInfer
 530         :: SDoc
 531         -> TcTyVarSet           -- fv(T); type vars
 532         -> LIE                  -- Wanted
 533         -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
 534                 LIE,            -- Free
 535                 TcDictBinds,    -- Bindings
 536                 [TcId])         -- Dict Ids that must be bound here (zonked)
 537 \end{code}
 538
 539
 540 \begin{code}
 541 tcSimplifyInfer doc tau_tvs wanted_lie
 542   = inferLoop doc (varSetElems tau_tvs)
 543               (lieToList wanted_lie)    `thenTc` \ (qtvs, frees, binds, irreds) ->
 544
 545         -- Check for non-generalisable insts
 546     mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)   `thenTc_`
 547
 548     returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
 549
 550 inferLoop doc tau_tvs wanteds
 551   =     -- Step 1
 552     zonkTcTyVarsAndFV tau_tvs           `thenNF_Tc` \ tau_tvs' ->
 553     mapNF_Tc zonkInst wanteds           `thenNF_Tc` \ wanteds' ->
 554     tcGetGlobalTyVars                   `thenNF_Tc` \ gbl_tvs ->
 555     let
 556         preds = predsOfInsts wanteds'
 557         qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
 558
 559         try_me inst
 560           | isFreeWhenInferring qtvs inst = Free
 561           | isClassDict inst              = DontReduceUnlessConstant    -- Dicts
 562           | otherwise                     = ReduceMe                    -- Lits and Methods
 563     in
 564                 -- Step 2
 565     reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
 566
 567                 -- Step 3
 568     if no_improvement then
 569         returnTc (varSetElems qtvs, frees, binds, irreds)
 570     else
 571         -- If improvement did some unification, we go round again.  There
 572         -- are two subtleties:
 573         --   a) We start again with irreds, not wanteds
 574         --      Using an instance decl might have introduced a fresh type variable
 575         --      which might have been unified, so we'd get an infinite loop
 576         --      if we started again with wanteds!  See example [LOOP]
 577         --
 578         --   b) It's also essential to re-process frees, because unification
 579         --      might mean that a type variable that looked free isn't now.
 580         --
 581         -- Hence the (irreds ++ frees)
 582
 583         -- However, NOTICE that when we are done, we might have some bindings, but
 584         -- the final qtvs might be empty.  See [NO TYVARS] below.
 585
 586         inferLoop doc tau_tvs (irreds ++ frees) `thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
 587         returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
 588 \end{code}
 589
 590 Example [LOOP]
 591
 592         class If b t e r | b t e -> r
 593         instance If T t e t
 594         instance If F t e e
 595         class Lte a b c | a b -> c where lte :: a -> b -> c
 596         instance Lte Z b T
 597         instance (Lte a b l,If l b a c) => Max a b c
 598
 599 Wanted: Max Z (S x) y
 600
 601 Then we'll reduce using the Max instance to:
 602         (Lte Z (S x) l, If l (S x) Z y)
 603 and improve by binding l->T, after which we can do some reduction
 604 on both the Lte and If constraints.  What we *can't* do is start again
 605 with (Max Z (S x) y)!
 606
 607 [NO TYVARS]
 608
 609         class Y a b | a -> b where
 610             y :: a -> X b
 611
 612         instance Y [[a]] a where
 613             y ((x:_):_) = X x
 614
 615         k :: X a -> X a -> X a
 616
 617         g :: Num a => [X a] -> [X a]
 618         g xs = h xs
 619             where
 620             h ys = ys ++ map (k (y [[0]])) xs
 621
 622 The excitement comes when simplifying the bindings for h.  Initially
 623 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
 624 From this we get t1:=:t2, but also various bindings.  We can't forget
 625 the bindings (because of [LOOP]), but in fact t1 is what g is
 626 polymorphic in.
 627
 628 The net effect of [NO TYVARS]
 629
 630 \begin{code}
 631 isFreeWhenInferring :: TyVarSet -> Inst -> Bool
 632 isFreeWhenInferring qtvs inst
 633   =  isFreeWrtTyVars qtvs inst                  -- Constrains no quantified vars
 634   && all inheritablePred (predsOfInst inst)     -- And no implicit parameter involved
 635                                                 -- (see "Notes on implicit parameters")
 636
 637 isFreeWhenChecking :: TyVarSet  -- Quantified tyvars
 638                    -> NameSet   -- Quantified implicit parameters
 639                    -> Inst -> Bool
 640 isFreeWhenChecking qtvs ips inst
 641   =  isFreeWrtTyVars qtvs inst
 642   && isFreeWrtIPs    ips inst
 643
 644 isFreeWrtTyVars qtvs inst = not (tyVarsOfInst inst `intersectsVarSet` qtvs)
 645 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 646 \end{code}
 647
 648
 649 %************************************************************************
 650 %*                                                                      *
 651 \subsection{tcSimplifyCheck}
 652 %*                                                                      *
 653 %************************************************************************
 654
 655 @tcSimplifyCheck@ is used when we know exactly the set of variables
 656 we are going to quantify over.  For example, a class or instance declaration.
 657
 658 \begin{code}
 659 tcSimplifyCheck
 660          :: SDoc
 661          -> [TcTyVar]           -- Quantify over these
 662          -> [Inst]              -- Given
 663          -> LIE                 -- Wanted
 664          -> TcM (LIE,           -- Free
 665                  TcDictBinds)   -- Bindings
 666
 667 -- tcSimplifyCheck is used when checking expression type signatures,
 668 -- class decls, instance decls etc.
 669 -- Note that we psss isFree (not isFreeAndInheritable) to tcSimplCheck
 670 -- It's important that we can float out non-inheritable predicates
 671 -- Example:             (?x :: Int) is ok!
 672 tcSimplifyCheck doc qtvs givens wanted_lie
 673   = tcSimplCheck doc get_qtvs
 674                  givens wanted_lie      `thenTc` \ (qtvs', frees, binds) ->
 675     returnTc (frees, binds)
 676   where
 677     get_qtvs = zonkTcTyVarsAndFV qtvs
 678
 679
 680 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
 681 -- against, but we don't know the type variables over which we are going to quantify.
 682 -- This happens when we have a type signature for a mutually recursive group
 683 tcSimplifyInferCheck
 684          :: SDoc
 685          -> TcTyVarSet          -- fv(T)
 686          -> [Inst]              -- Given
 687          -> LIE                 -- Wanted
 688          -> TcM ([TcTyVar],     -- Variables over which to quantify
 689                  LIE,           -- Free
 690                  TcDictBinds)   -- Bindings
 691
 692 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
 693   = tcSimplCheck doc get_qtvs givens wanted_lie
 694   where
 695         -- Figure out which type variables to quantify over
 696         -- You might think it should just be the signature tyvars,
 697         -- but in bizarre cases you can get extra ones
 698         --      f :: forall a. Num a => a -> a
 699         --      f x = fst (g (x, head [])) + 1
 700         --      g a b = (b,a)
 701         -- Here we infer g :: forall a b. a -> b -> (b,a)
 702         -- We don't want g to be monomorphic in b just because
 703         -- f isn't quantified over b.
 704     all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
 705
 706     get_qtvs = zonkTcTyVarsAndFV all_tvs        `thenNF_Tc` \ all_tvs' ->
 707                tcGetGlobalTyVars                `thenNF_Tc` \ gbl_tvs ->
 708                let
 709                   qtvs = all_tvs' `minusVarSet` gbl_tvs
 710                         -- We could close gbl_tvs, but its not necessary for
 711                         -- soundness, and it'll only affect which tyvars, not which
 712                         -- dictionaries, we quantify over
 713                in
 714                returnNF_Tc qtvs
 715 \end{code}
 716
 717 Here is the workhorse function for all three wrappers.
 718
 719 \begin{code}
 720 tcSimplCheck doc get_qtvs givens wanted_lie
 721   = check_loop givens (lieToList wanted_lie)    `thenTc` \ (qtvs, frees, binds, irreds) ->
 722
 723         -- Complain about any irreducible ones
 724     complainCheck doc givens irreds             `thenNF_Tc_`
 725
 726         -- Done
 727     returnTc (qtvs, mkLIE frees, binds)
 728
 729   where
 730     ip_set = mkNameSet (ipNamesOfInsts givens)
 731
 732     check_loop givens wanteds
 733       =         -- Step 1
 734         mapNF_Tc zonkInst givens        `thenNF_Tc` \ givens' ->
 735         mapNF_Tc zonkInst wanteds       `thenNF_Tc` \ wanteds' ->
 736         get_qtvs                        `thenNF_Tc` \ qtvs' ->
 737
 738                     -- Step 2
 739         let
 740             -- When checking against a given signature we always reduce
 741             -- until we find a match against something given, or can't reduce
 742             try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
 743                         | otherwise                            = ReduceMe
 744         in
 745         reduceContext doc try_me givens' wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
 746
 747                     -- Step 3
 748         if no_improvement then
 749             returnTc (varSetElems qtvs', frees, binds, irreds)
 750         else
 751             check_loop givens' (irreds ++ frees)        `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
 752             returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
 753 \end{code}
 754
 755
 756 %************************************************************************
 757 %*                                                                      *
 758 \subsection{tcSimplifyRestricted}
 759 %*                                                                      *
 760 %************************************************************************
 761
 762 \begin{code}
 763 tcSimplifyRestricted    -- Used for restricted binding groups
 764                         -- i.e. ones subject to the monomorphism restriction
 765         :: SDoc
 766         -> TcTyVarSet           -- Free in the type of the RHSs
 767         -> LIE                  -- Free in the RHSs
 768         -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
 769                 LIE,            -- Free
 770                 TcDictBinds)    -- Bindings
 771
 772 tcSimplifyRestricted doc tau_tvs wanted_lie
 773   =     -- First squash out all methods, to find the constrained tyvars
 774         -- We can't just take the free vars of wanted_lie because that'll
 775         -- have methods that may incidentally mention entirely unconstrained variables
 776         --      e.g. a call to  f :: Eq a => a -> b -> b
 777         -- Here, b is unconstrained.  A good example would be
 778         --      foo = f (3::Int)
 779         -- We want to infer the polymorphic type
 780         --      foo :: forall b. b -> b
 781     let
 782         wanteds = lieToList wanted_lie
 783         try_me inst = ReduceMe          -- Reduce as far as we can.  Don't stop at
 784                                         -- dicts; the idea is to get rid of as many type
 785                                         -- variables as possible, and we don't want to stop
 786                                         -- at (say) Monad (ST s), because that reduces
 787                                         -- immediately, with no constraint on s.
 788     in
 789     simpleReduceLoop doc try_me wanteds         `thenTc` \ (_, _, constrained_dicts) ->
 790
 791         -- Next, figure out the tyvars we will quantify over
 792     zonkTcTyVarsAndFV (varSetElems tau_tvs)     `thenNF_Tc` \ tau_tvs' ->
 793     tcGetGlobalTyVars                           `thenNF_Tc` \ gbl_tvs ->
 794     let
 795         constrained_tvs = tyVarsOfInsts constrained_dicts
 796         qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
 797                          `minusVarSet` constrained_tvs
 798     in
 799
 800         -- The first step may have squashed more methods than
 801         -- necessary, so try again, this time knowing the exact
 802         -- set of type variables to quantify over.
 803         --
 804         -- We quantify only over constraints that are captured by qtvs;
 805         -- these will just be a subset of non-dicts.  This in contrast
 806         -- to normal inference (using isFreeWhenInferring) in which we quantify over
 807         -- all *non-inheritable* constraints too.  This implements choice
 808         -- (B) under "implicit parameter and monomorphism" above.
 809         --
 810         -- Remember that we may need to do *some* simplification, to
 811         -- (for example) squash {Monad (ST s)} into {}.  It's not enough
 812         -- just to float all constraints
 813     mapNF_Tc zonkInst (lieToList wanted_lie)    `thenNF_Tc` \ wanteds' ->
 814     let
 815         try_me inst | isFreeWrtTyVars qtvs inst = Free
 816                     | otherwise                 = ReduceMe
 817     in
 818     reduceContext doc try_me [] wanteds'        `thenTc` \ (no_improvement, frees, binds, irreds) ->
 819     ASSERT( no_improvement )
 820     ASSERT( null irreds )
 821         -- No need to loop because simpleReduceLoop will have
 822         -- already done any improvement necessary
 823
 824     returnTc (varSetElems qtvs, mkLIE frees, binds)
 825 \end{code}
 826
 827
 828 %************************************************************************
 829 %*                                                                      *
 830 \subsection{tcSimplifyToDicts}
 831 %*                                                                      *
 832 %************************************************************************
 833
 834 On the LHS of transformation rules we only simplify methods and constants,
 835 getting dictionaries.  We want to keep all of them unsimplified, to serve
 836 as the available stuff for the RHS of the rule.
 837
 838 The same thing is used for specialise pragmas. Consider
 839
 840         f :: Num a => a -> a
 841         {-# SPECIALISE f :: Int -> Int #-}
 842         f = ...
 843
 844 The type checker generates a binding like:
 845
 846         f_spec = (f :: Int -> Int)
 847
 848 and we want to end up with
 849
 850         f_spec = _inline_me_ (f Int dNumInt)
 851
 852 But that means that we must simplify the Method for f to (f Int dNumInt)!
 853 So tcSimplifyToDicts squeezes out all Methods.
 854
 855 IMPORTANT NOTE:  we *don't* want to do superclass commoning up.  Consider
 856
 857         fromIntegral :: (Integral a, Num b) => a -> b
 858         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
 859
 860 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
 861 want to get
 862
 863         forall dIntegralInt.
 864         fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 865
 866 because the scsel will mess up matching.  Instead we want
 867
 868         forall dIntegralInt, dNumInt.
 869         fromIntegral Int Int dIntegralInt dNumInt = id Int
 870
 871 Hence "DontReduce NoSCs"
 872
 873 \begin{code}
 874 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
 875 tcSimplifyToDicts wanted_lie
 876   = simpleReduceLoop doc try_me wanteds         `thenTc` \ (frees, binds, irreds) ->
 877         -- Since try_me doesn't look at types, we don't need to
 878         -- do any zonking, so it's safe to call reduceContext directly
 879     ASSERT( null frees )
 880     returnTc (irreds, binds)
 881
 882   where
 883     doc = text "tcSimplifyToDicts"
 884     wanteds = lieToList wanted_lie
 885
 886         -- Reduce methods and lits only; stop as soon as we get a dictionary
 887     try_me inst | isDict inst = DontReduce NoSCs
 888                 | otherwise   = ReduceMe
 889 \end{code}
 890
 891
 892 %************************************************************************
 893 %*                                                                      *
 894 \subsection{Filtering at a dynamic binding}
 895 %*                                                                      *
 896 %************************************************************************
 897
 898 When we have
 899         let ?x = R in B
 900
 901 we must discharge all the ?x constraints from B.  We also do an improvement
 902 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
 903
 904 Actually, the constraints from B might improve the types in ?x. For example
 905
 906         f :: (?x::Int) => Char -> Char
 907         let ?x = 3 in f 'c'
 908
 909 then the constraint (?x::Int) arising from the call to f will
 910 force the binding for ?x to be of type Int.
 911
 912 \begin{code}
 913 tcSimplifyIPs :: [Inst]         -- The implicit parameters bound here
 914               -> LIE
 915               -> TcM (LIE, TcDictBinds)
 916 tcSimplifyIPs given_ips wanted_lie
 917   = simpl_loop given_ips wanteds        `thenTc` \ (frees, binds) ->
 918     returnTc (mkLIE frees, binds)
 919   where
 920     doc      = text "tcSimplifyIPs" <+> ppr given_ips
 921     wanteds  = lieToList wanted_lie
 922     ip_set   = mkNameSet (ipNamesOfInsts given_ips)
 923
 924         -- Simplify any methods that mention the implicit parameter
 925     try_me inst | isFreeWrtIPs ip_set inst = Free
 926                 | otherwise                = ReduceMe
 927
 928     simpl_loop givens wanteds
 929       = mapNF_Tc zonkInst givens                `thenNF_Tc` \ givens' ->
 930         mapNF_Tc zonkInst wanteds               `thenNF_Tc` \ wanteds' ->
 931
 932         reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
 933
 934         if no_improvement then
 935             ASSERT( null irreds )
 936             returnTc (frees, binds)
 937         else
 938             simpl_loop givens' (irreds ++ frees)        `thenTc` \ (frees1, binds1) ->
 939             returnTc (frees1, binds `AndMonoBinds` binds1)
 940 \end{code}
 941
 942
 943 %************************************************************************
 944 %*                                                                      *
 945 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
 946 %*                                                                      *
 947 %************************************************************************
 948
 949 When doing a binding group, we may have @Insts@ of local functions.
 950 For example, we might have...
 951 \begin{verbatim}
 952 let f x = x + 1     -- orig local function (overloaded)
 953     f.1 = f Int     -- two instances of f
 954     f.2 = f Float
 955  in
 956     (f.1 5, f.2 6.7)
 957 \end{verbatim}
 958 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
 959 where @f@ is in scope; those @Insts@ must certainly not be passed
 960 upwards towards the top-level.  If the @Insts@ were binding-ified up
 961 there, they would have unresolvable references to @f@.
 962
 963 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
 964 For each method @Inst@ in the @init_lie@ that mentions one of the
 965 @Ids@, we create a binding.  We return the remaining @Insts@ (in an
 966 @LIE@), as well as the @HsBinds@ generated.
 967
 968 \begin{code}
 969 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
 970
 971 bindInstsOfLocalFuns init_lie local_ids
 972   | null overloaded_ids
 973         -- Common case
 974   = returnTc (init_lie, EmptyMonoBinds)
 975
 976   | otherwise
 977   = simpleReduceLoop doc try_me wanteds         `thenTc` \ (frees, binds, irreds) ->
 978     ASSERT( null irreds )
 979     returnTc (mkLIE frees, binds)
 980   where
 981     doc              = text "bindInsts" <+> ppr local_ids
 982     wanteds          = lieToList init_lie
 983     overloaded_ids   = filter is_overloaded local_ids
 984     is_overloaded id = isOverloadedTy (idType id)
 985
 986     overloaded_set = mkVarSet overloaded_ids    -- There can occasionally be a lot of them
 987                                                 -- so it's worth building a set, so that
 988                                                 -- lookup (in isMethodFor) is faster
 989
 990     try_me inst | isMethodFor overloaded_set inst = ReduceMe
 991                 | otherwise                       = Free
 992 \end{code}
 993
 994
 995 %************************************************************************
 996 %*                                                                      *
 997 \subsection{Data types for the reduction mechanism}
 998 %*                                                                      *
 999 %************************************************************************
1000
1001 The main control over context reduction is here
1002
1003 \begin{code}
1004 data WhatToDo
1005  = ReduceMe             -- Try to reduce this
1006                         -- If there's no instance, behave exactly like
1007                         -- DontReduce: add the inst to
1008                         -- the irreductible ones, but don't
1009                         -- produce an error message of any kind.
1010                         -- It might be quite legitimate such as (Eq a)!
1011
1012  | DontReduce WantSCs           -- Return as irreducible
1013
1014  | DontReduceUnlessConstant     -- Return as irreducible unless it can
1015                                 -- be reduced to a constant in one step
1016
1017  | Free                   -- Return as free
1018
1019 data WantSCs = NoSCs | AddSCs   -- Tells whether we should add the superclasses
1020                                 -- of a predicate when adding it to the avails
1021 \end{code}
1022
1023
1024
1025 \begin{code}
1026 type RedState = (Avails,        -- What's available
1027                  [Inst])        -- Insts for which try_me returned Free
1028
1029 type Avails = FiniteMap Inst Avail
1030
1031 data Avail
1032   = Irred               -- Used for irreducible dictionaries,
1033                         -- which are going to be lambda bound
1034
1035   | BoundTo TcId        -- Used for dictionaries for which we have a binding
1036                         -- e.g. those "given" in a signature
1037
1038   | NoRhs               -- Used for Insts like (CCallable f)
1039                         -- where no witness is required.
1040
1041   | Rhs                 -- Used when there is a RHS
1042         TcExpr          -- The RHS
1043         [Inst]          -- Insts free in the RHS; we need these too
1044
1045 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
1046                         | (inst,avail) <- fmToList avails ]
1047
1048 instance Outputable Avail where
1049     ppr = pprAvail
1050
1051 pprAvail NoRhs        = text "<no rhs>"
1052 pprAvail Irred        = text "Irred"
1053 pprAvail (BoundTo x)  = text "Bound to" <+> ppr x
1054 pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
1055 \end{code}
1056
1057 Extracting the bindings from a bunch of Avails.
1058 The bindings do *not* come back sorted in dependency order.
1059 We assume that they'll be wrapped in a big Rec, so that the
1060 dependency analyser can sort them out later
1061
1062 The loop startes
1063 \begin{code}
1064 bindsAndIrreds :: Avails
1065                -> [Inst]                -- Wanted
1066                -> (TcDictBinds,         -- Bindings
1067                    [Inst])              -- Irreducible ones
1068
1069 bindsAndIrreds avails wanteds
1070   = go avails EmptyMonoBinds [] wanteds
1071   where
1072     go avails binds irreds [] = (binds, irreds)
1073
1074     go avails binds irreds (w:ws)
1075       = case lookupFM avails w of
1076           Nothing    -> -- Free guys come out here
1077                         -- (If we didn't do addFree we could use this as the
1078                         --  criterion for free-ness, and pick up the free ones here too)
1079                         go avails binds irreds ws
1080
1081           Just NoRhs -> go avails binds irreds ws
1082
1083           Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
1084
1085           Just (BoundTo id) -> go avails new_binds irreds ws
1086                             where
1087                                 -- For implicit parameters, all occurrences share the same
1088                                 -- Id, so there is no need for synonym bindings
1089                                new_binds | new_id == id = binds
1090                                          | otherwise    = addBind binds new_id (HsVar id)
1091                                new_id   = instToId w
1092
1093           Just (Rhs rhs ws') -> go avails' (addBind binds id rhs) irreds (ws' ++ ws)
1094                              where
1095                                 id       = instToId w
1096                                 avails'  = addToFM avails w (BoundTo id)
1097
1098 addBind binds id rhs = binds `AndMonoBinds` VarMonoBind id rhs
1099 \end{code}
1100
1101
1102 %************************************************************************
1103 %*                                                                      *
1104 \subsection[reduce]{@reduce@}
1105 %*                                                                      *
1106 %************************************************************************
1107
1108 When the "what to do" predicate doesn't depend on the quantified type variables,
1109 matters are easier.  We don't need to do any zonking, unless the improvement step
1110 does something, in which case we zonk before iterating.
1111
1112 The "given" set is always empty.
1113
1114 \begin{code}
1115 simpleReduceLoop :: SDoc
1116                  -> (Inst -> WhatToDo)          -- What to do, *not* based on the quantified type variables
1117                  -> [Inst]                      -- Wanted
1118                  -> TcM ([Inst],                -- Free
1119                          TcDictBinds,
1120                          [Inst])                -- Irreducible
1121
1122 simpleReduceLoop doc try_me wanteds
1123   = mapNF_Tc zonkInst wanteds                   `thenNF_Tc` \ wanteds' ->
1124     reduceContext doc try_me [] wanteds'        `thenTc` \ (no_improvement, frees, binds, irreds) ->
1125     if no_improvement then
1126         returnTc (frees, binds, irreds)
1127     else
1128         simpleReduceLoop doc try_me (irreds ++ frees)   `thenTc` \ (frees1, binds1, irreds1) ->
1129         returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1130 \end{code}
1131
1132
1133
1134 \begin{code}
1135 reduceContext :: SDoc
1136               -> (Inst -> WhatToDo)
1137               -> [Inst]                 -- Given
1138               -> [Inst]                 -- Wanted
1139               -> NF_TcM (Bool,          -- True <=> improve step did no unification
1140                          [Inst],        -- Free
1141                          TcDictBinds,   -- Dictionary bindings
1142                          [Inst])        -- Irreducible
1143
1144 reduceContext doc try_me givens wanteds
1145   =
1146     traceTc (text "reduceContext" <+> (vcat [
1147              text "----------------------",
1148              doc,
1149              text "given" <+> ppr givens,
1150              text "wanted" <+> ppr wanteds,
1151              text "----------------------"
1152              ]))                                        `thenNF_Tc_`
1153
1154         -- Build the Avail mapping from "givens"
1155     foldlNF_Tc addGiven (emptyFM, []) givens            `thenNF_Tc` \ init_state ->
1156
1157         -- Do the real work
1158     reduceList (0,[]) try_me wanteds init_state         `thenNF_Tc` \ state@(avails, frees) ->
1159
1160         -- Do improvement, using everything in avails
1161         -- In particular, avails includes all superclasses of everything
1162     tcImprove avails                                    `thenTc` \ no_improvement ->
1163
1164     traceTc (text "reduceContext end" <+> (vcat [
1165              text "----------------------",
1166              doc,
1167              text "given" <+> ppr givens,
1168              text "wanted" <+> ppr wanteds,
1169              text "----",
1170              text "avails" <+> pprAvails avails,
1171              text "frees" <+> ppr frees,
1172              text "no_improvement =" <+> ppr no_improvement,
1173              text "----------------------"
1174              ]))                                        `thenNF_Tc_`
1175      let
1176         (binds, irreds) = bindsAndIrreds avails wanteds
1177      in
1178      returnTc (no_improvement, frees, binds, irreds)
1179
1180 tcImprove avails
1181  =  tcGetInstEnv                                `thenTc` \ inst_env ->
1182     let
1183         preds = [ (pred, pp_loc)
1184                 | inst <- keysFM avails,
1185                   let pp_loc = pprInstLoc (instLoc inst),
1186                   pred <- predsOfInst inst,
1187                   predHasFDs pred
1188                 ]
1189                 -- Avails has all the superclasses etc (good)
1190                 -- It also has all the intermediates of the deduction (good)
1191                 -- It does not have duplicates (good)
1192                 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1193                 --    so that improve will see them separate
1194         eqns  = improve (classInstEnv inst_env) preds
1195      in
1196      if null eqns then
1197         returnTc True
1198      else
1199         traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))     `thenNF_Tc_`
1200         mapTc_ unify eqns       `thenTc_`
1201         returnTc False
1202   where
1203     unify ((qtvs, t1, t2), doc)
1204          = tcAddErrCtxt doc                     $
1205            tcInstTyVars (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
1206            unifyTauTy (substTy tenv t1) (substTy tenv t2)
1207 \end{code}
1208
1209 The main context-reduction function is @reduce@.  Here's its game plan.
1210
1211 \begin{code}
1212 reduceList :: (Int,[Inst])              -- Stack (for err msgs)
1213                                         -- along with its depth
1214            -> (Inst -> WhatToDo)
1215            -> [Inst]
1216            -> RedState
1217            -> TcM RedState
1218 \end{code}
1219
1220 @reduce@ is passed
1221      try_me:    given an inst, this function returns
1222                   Reduce       reduce this
1223                   DontReduce   return this in "irreds"
1224                   Free         return this in "frees"
1225
1226      wanteds:   The list of insts to reduce
1227      state:     An accumulating parameter of type RedState
1228                 that contains the state of the algorithm
1229
1230   It returns a RedState.
1231
1232 The (n,stack) pair is just used for error reporting.
1233 n is always the depth of the stack.
1234 The stack is the stack of Insts being reduced: to produce X
1235 I had to produce Y, to produce Y I had to produce Z, and so on.
1236
1237 \begin{code}
1238 reduceList (n,stack) try_me wanteds state
1239   | n > opt_MaxContextReductionDepth
1240   = failWithTc (reduceDepthErr n stack)
1241
1242   | otherwise
1243   =
1244 #ifdef DEBUG
1245    (if n > 8 then
1246         pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1247     else (\x->x))
1248 #endif
1249     go wanteds state
1250   where
1251     go []     state = returnTc state
1252     go (w:ws) state = reduce (n+1, w:stack) try_me w state      `thenTc` \ state' ->
1253                       go ws state'
1254
1255     -- Base case: we're done!
1256 reduce stack try_me wanted state
1257     -- It's the same as an existing inst, or a superclass thereof
1258   | isAvailable state wanted
1259   = returnTc state
1260
1261   | otherwise
1262   = case try_me wanted of {
1263
1264       DontReduce want_scs -> addIrred want_scs state wanted
1265
1266     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
1267                                      -- First, see if the inst can be reduced to a constant in one step
1268         try_simple (addIrred AddSCs)    -- Assume want superclasses
1269
1270     ; Free ->   -- It's free so just chuck it upstairs
1271                 -- First, see if the inst can be reduced to a constant in one step
1272         try_simple addFree
1273
1274     ; ReduceMe ->               -- It should be reduced
1275         lookupInst wanted             `thenNF_Tc` \ lookup_result ->
1276         case lookup_result of
1277             GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' ->
1278                                     addWanted state' wanted rhs wanteds'
1279             SimpleInst rhs       -> addWanted state wanted rhs []
1280
1281             NoInstance ->    -- No such instance!
1282                              -- Add it and its superclasses
1283                              addIrred AddSCs state wanted
1284
1285     }
1286   where
1287     try_simple do_this_otherwise
1288       = lookupInst wanted         `thenNF_Tc` \ lookup_result ->
1289         case lookup_result of
1290             SimpleInst rhs -> addWanted state wanted rhs []
1291             other          -> do_this_otherwise state wanted
1292 \end{code}
1293
1294
1295 \begin{code}
1296 isAvailable :: RedState -> Inst -> Bool
1297 isAvailable (avails, _) wanted = wanted `elemFM` avails
1298         -- NB: the Ord instance of Inst compares by the class/type info
1299         -- *not* by unique.  So
1300         --      d1::C Int ==  d2::C Int
1301
1302 -------------------------
1303 addFree :: RedState -> Inst -> NF_TcM RedState
1304         -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1305         -- to avails, so that any other equal Insts will be commoned up right
1306         -- here rather than also being tossed upstairs.  This is really just
1307         -- an optimisation, and perhaps it is more trouble that it is worth,
1308         -- as the following comments show!
1309         --
1310         -- NB1: do *not* add superclasses.  If we have
1311         --      df::Floating a
1312         --      dn::Num a
1313         -- but a is not bound here, then we *don't* want to derive
1314         -- dn from df here lest we lose sharing.
1315         --
1316         -- NB2: do *not* add the Inst to avails at all if it's a method.
1317         -- The following situation shows why this is bad:
1318         --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1319         -- From an application (truncate f i) we get
1320         --      t1 = truncate at f
1321         --      t2 = t1 at i
1322         -- If we have also have a second occurrence of truncate, we get
1323         --      t3 = truncate at f
1324         --      t4 = t3 at i
1325         -- When simplifying with i,f free, we might still notice that
1326         --   t1=t3; but alas, the binding for t2 (which mentions t1)
1327         --   will continue to float out!
1328         -- Solution: never put methods in avail till they are captured
1329         -- in which case addFree isn't used
1330         --
1331         -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1332         --      than BoundTo, else we end up with bogus bindings.
1333         --      c.f. instBindingRequired in addWanted
1334 addFree (avails, frees) free
1335   | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1336   | otherwise   = returnNF_Tc (avails,                    free:frees)
1337   where
1338     avail | instBindingRequired free = BoundTo (instToId free)
1339           | otherwise                = NoRhs
1340
1341 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1342 addWanted state@(avails, frees) wanted rhs_expr wanteds
1343 -- Do *not* add superclasses as well.  Here's an example of why not
1344 --      class Eq a => Foo a b
1345 --      instance Eq a => Foo [a] a
1346 -- If we are reducing
1347 --      (Foo [t] t)
1348 -- we'll first deduce that it holds (via the instance decl).  We
1349 -- must not then overwrite the Eq t constraint with a superclass selection!
1350 --      ToDo: this isn't entirely unsatisfactory, because
1351 --            we may also lose some entirely-legitimate sharing this way
1352
1353   = ASSERT( not (isAvailable state wanted) )
1354     returnNF_Tc (addToFM avails wanted avail, frees)
1355   where
1356     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1357           | otherwise                  = ASSERT( null wanteds ) NoRhs
1358
1359 addGiven :: RedState -> Inst -> NF_TcM RedState
1360 addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
1361
1362 addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
1363 addIrred NoSCs  (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
1364 addIrred AddSCs state          irred = addAvailAndSCs state irred Irred
1365
1366 addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
1367 addAvailAndSCs (avails, frees) wanted avail
1368   = add_avail_and_scs avails wanted avail       `thenNF_Tc` \ avails' ->
1369     returnNF_Tc (avails', frees)
1370
1371 ---------------------
1372 add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
1373 add_avail_and_scs avails wanted avail
1374   = add_scs (addToFM avails wanted avail) wanted
1375
1376 add_scs :: Avails -> Inst -> NF_TcM Avails
1377         -- Add all the superclasses of the Inst to Avails
1378         -- Invariant: the Inst is already in Avails.
1379
1380 add_scs avails dict
1381   | not (isClassDict dict)
1382   = returnNF_Tc avails
1383
1384   | otherwise   -- It is a dictionary
1385   = newDictsFromOld dict sc_theta'      `thenNF_Tc` \ sc_dicts ->
1386     foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1387   where
1388     (clas, tys) = getDictClassTys dict
1389     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1390     sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1391
1392     add_sc avails (sc_dict, sc_sel)     -- Add it, and its superclasses
1393       = case lookupFM avails sc_dict of
1394           Just (BoundTo _) -> returnNF_Tc avails        -- See Note [SUPER] below
1395           other            -> add_avail_and_scs avails sc_dict avail
1396       where
1397         sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1398         avail      = Rhs sc_sel_rhs [dict]
1399 \end{code}
1400
1401 Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
1402 and want to deduce (d2:C [a]) where
1403
1404         class Ord a => C a where
1405         instance Ord a => C [a] where ...
1406
1407 Then we'll use the instance decl to deduce C [a] and then add the
1408 superclasses of C [a] to avails.  But we must not overwrite the binding
1409 for d1:Ord a (which is given) with a superclass selection or we'll just
1410 build a loop!  Hence looking for BoundTo.  Crudely, BoundTo is cheaper
1411 than a selection.
1412
1413
1414 %************************************************************************
1415 %*                                                                      *
1416 \section{tcSimplifyTop: defaulting}
1417 %*                                                                      *
1418 %************************************************************************
1419
1420
1421 If a dictionary constrains a type variable which is
1422         * not mentioned in the environment
1423         * and not mentioned in the type of the expression
1424 then it is ambiguous. No further information will arise to instantiate
1425 the type variable; nor will it be generalised and turned into an extra
1426 parameter to a function.
1427
1428 It is an error for this to occur, except that Haskell provided for
1429 certain rules to be applied in the special case of numeric types.
1430 Specifically, if
1431         * at least one of its classes is a numeric class, and
1432         * all of its classes are numeric or standard
1433 then the type variable can be defaulted to the first type in the
1434 default-type list which is an instance of all the offending classes.
1435
1436 So here is the function which does the work.  It takes the ambiguous
1437 dictionaries and either resolves them (producing bindings) or
1438 complains.  It works by splitting the dictionary list by type
1439 variable, and using @disambigOne@ to do the real business.
1440
1441 @tcSimplifyTop@ is called once per module to simplify all the constant
1442 and ambiguous Insts.
1443
1444 We need to be careful of one case.  Suppose we have
1445
1446         instance Num a => Num (Foo a b) where ...
1447
1448 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)).  Then it'll simplify
1449 to (Num x), and default x to Int.  But what about y??
1450
1451 It's OK: the final zonking stage should zap y to (), which is fine.
1452
1453
1454 \begin{code}
1455 tcSimplifyTop :: LIE -> TcM TcDictBinds
1456 tcSimplifyTop wanted_lie
1457   = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1458     ASSERT( null frees )
1459
1460     let
1461                 -- All the non-std ones are definite errors
1462         (stds, non_stds) = partition isStdClassTyVarDict irreds
1463
1464                 -- Group by type variable
1465         std_groups = equivClasses cmp_by_tyvar stds
1466
1467                 -- Pick the ones which its worth trying to disambiguate
1468         (std_oks, std_bads) = partition worth_a_try std_groups
1469
1470                 -- Have a try at disambiguation
1471                 -- if the type variable isn't bound
1472                 -- up with one of the non-standard classes
1473         worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1474         non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
1475
1476                 -- Collect together all the bad guys
1477         bad_guys = non_stds ++ concat std_bads
1478     in
1479         -- Disambiguate the ones that look feasible
1480     mapTc disambigGroup std_oks         `thenTc` \ binds_ambig ->
1481
1482         -- And complain about the ones that don't
1483         -- This group includes both non-existent instances
1484         --      e.g. Num (IO a) and Eq (Int -> Int)
1485         -- and ambiguous dictionaries
1486         --      e.g. Num a
1487     addTopAmbigErrs bad_guys            `thenNF_Tc_`
1488
1489     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1490   where
1491     wanteds     = lieToList wanted_lie
1492     try_me inst = ReduceMe
1493
1494     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1495
1496 get_tv d   = case getDictClassTys d of
1497                    (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1498 get_clas d = case getDictClassTys d of
1499                    (clas, [ty]) -> clas
1500 \end{code}
1501
1502 @disambigOne@ assumes that its arguments dictionaries constrain all
1503 the same type variable.
1504
1505 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1506 @()@ instead of @Int@.  I reckon this is the Right Thing to do since
1507 the most common use of defaulting is code like:
1508 \begin{verbatim}
1509         _ccall_ foo     `seqPrimIO` bar
1510 \end{verbatim}
1511 Since we're not using the result of @foo@, the result if (presumably)
1512 @void@.
1513
1514 \begin{code}
1515 disambigGroup :: [Inst] -- All standard classes of form (C a)
1516               -> TcM TcDictBinds
1517
1518 disambigGroup dicts
1519   |   any isNumericClass classes        -- Guaranteed all standard classes
1520           -- see comment at the end of function for reasons as to
1521           -- why the defaulting mechanism doesn't apply to groups that
1522           -- include CCallable or CReturnable dicts.
1523    && not (any isCcallishClass classes)
1524   =     -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1525         -- SO, TRY DEFAULT TYPES IN ORDER
1526
1527         -- Failure here is caused by there being no type in the
1528         -- default list which can satisfy all the ambiguous classes.
1529         -- For example, if Real a is reqd, but the only type in the
1530         -- default list is Int.
1531     tcGetDefaultTys                     `thenNF_Tc` \ default_tys ->
1532     let
1533       try_default []    -- No defaults work, so fail
1534         = failTc
1535
1536       try_default (default_ty : default_tys)
1537         = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
1538                                                 -- default_tys instead
1539           tcSimplifyCheckThetas [] theta        `thenTc` \ _ ->
1540           returnTc default_ty
1541         where
1542           theta = [mkClassPred clas [default_ty] | clas <- classes]
1543     in
1544         -- See if any default works, and if so bind the type variable to it
1545         -- If not, add an AmbigErr
1546     recoverTc (addAmbigErrs dicts                       `thenNF_Tc_`
1547                returnTc EmptyMonoBinds) $
1548
1549     try_default default_tys                     `thenTc` \ chosen_default_ty ->
1550
1551         -- Bind the type variable and reduce the context, for real this time
1552     unifyTauTy chosen_default_ty (mkTyVarTy tyvar)      `thenTc_`
1553     simpleReduceLoop (text "disambig" <+> ppr dicts)
1554                      try_me dicts                       `thenTc` \ (frees, binds, ambigs) ->
1555     WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1556     warnDefault dicts chosen_default_ty                 `thenTc_`
1557     returnTc binds
1558
1559   | all isCreturnableClass classes
1560   =     -- Default CCall stuff to (); we don't even both to check that () is an
1561         -- instance of CReturnable, because we know it is.
1562     unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
1563     returnTc EmptyMonoBinds
1564
1565   | otherwise -- No defaults
1566   = addAmbigErrs dicts  `thenNF_Tc_`
1567     returnTc EmptyMonoBinds
1568
1569   where
1570     try_me inst = ReduceMe                      -- This reduce should not fail
1571     tyvar       = get_tv (head dicts)           -- Should be non-empty
1572     classes     = map get_clas dicts
1573 \end{code}
1574
1575 [Aside - why the defaulting mechanism is turned off when
1576  dealing with arguments and results to ccalls.
1577
1578 When typechecking _ccall_s, TcExpr ensures that the external
1579 function is only passed arguments (and in the other direction,
1580 results) of a restricted set of 'native' types. This is
1581 implemented via the help of the pseudo-type classes,
1582 @CReturnable@ (CR) and @CCallable@ (CC.)
1583
1584 The interaction between the defaulting mechanism for numeric
1585 values and CC & CR can be a bit puzzling to the user at times.
1586 For example,
1587
1588     x <- _ccall_ f
1589     if (x /= 0) then
1590        _ccall_ g x
1591      else
1592        return ()
1593
1594 What type has 'x' got here? That depends on the default list
1595 in operation, if it is equal to Haskell 98's default-default
1596 of (Integer, Double), 'x' has type Double, since Integer
1597 is not an instance of CR. If the default list is equal to
1598 Haskell 1.4's default-default of (Int, Double), 'x' has type
1599 Int.
1600
1601 To try to minimise the potential for surprises here, the
1602 defaulting mechanism is turned off in the presence of
1603 CCallable and CReturnable.
1604
1605 End of aside]
1606
1607
1608 %************************************************************************
1609 %*                                                                      *
1610 \subsection[simple]{@Simple@ versions}
1611 %*                                                                      *
1612 %************************************************************************
1613
1614 Much simpler versions when there are no bindings to make!
1615
1616 @tcSimplifyThetas@ simplifies class-type constraints formed by
1617 @deriving@ declarations and when specialising instances.  We are
1618 only interested in the simplified bunch of class/type constraints.
1619
1620 It simplifies to constraints of the form (C a b c) where
1621 a,b,c are type variables.  This is required for the context of
1622 instance declarations.
1623
1624 \begin{code}
1625 tcSimplifyThetas :: ThetaType           -- Wanted
1626                  -> TcM ThetaType               -- Needed
1627
1628 tcSimplifyThetas wanteds
1629   = doptsTc Opt_GlasgowExts             `thenNF_Tc` \ glaExts ->
1630     reduceSimple [] wanteds             `thenNF_Tc` \ irreds ->
1631     let
1632         -- For multi-param Haskell, check that the returned dictionaries
1633         -- don't have any of the form (C Int Bool) for which
1634         -- we expect an instance here
1635         -- For Haskell 98, check that all the constraints are of the form C a,
1636         -- where a is a type variable
1637         bad_guys | glaExts   = [pred | pred <- irreds,
1638                                        isEmptyVarSet (tyVarsOfPred pred)]
1639                  | otherwise = [pred | pred <- irreds,
1640                                        not (isTyVarClassPred pred)]
1641     in
1642     if null bad_guys then
1643         returnTc irreds
1644     else
1645        mapNF_Tc addNoInstErr bad_guys           `thenNF_Tc_`
1646        failTc
1647 \end{code}
1648
1649 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1650 used with \tr{default} declarations.  We are only interested in
1651 whether it worked or not.
1652
1653 \begin{code}
1654 tcSimplifyCheckThetas :: ThetaType      -- Given
1655                       -> ThetaType      -- Wanted
1656                       -> TcM ()
1657
1658 tcSimplifyCheckThetas givens wanteds
1659   = reduceSimple givens wanteds    `thenNF_Tc`  \ irreds ->
1660     if null irreds then
1661        returnTc ()
1662     else
1663        mapNF_Tc addNoInstErr irreds             `thenNF_Tc_`
1664        failTc
1665 \end{code}
1666
1667
1668 \begin{code}
1669 type AvailsSimple = FiniteMap PredType Bool
1670                     -- True  => irreducible
1671                     -- False => given, or can be derived from a given or from an irreducible
1672
1673 reduceSimple :: ThetaType                       -- Given
1674              -> ThetaType                       -- Wanted
1675              -> NF_TcM ThetaType                -- Irreducible
1676
1677 reduceSimple givens wanteds
1678   = reduce_simple (0,[]) givens_fm wanteds      `thenNF_Tc` \ givens_fm' ->
1679     returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
1680   where
1681     givens_fm     = foldl addNonIrred emptyFM givens
1682
1683 reduce_simple :: (Int,ThetaType)                -- Stack
1684               -> AvailsSimple
1685               -> ThetaType
1686               -> NF_TcM AvailsSimple
1687
1688 reduce_simple (n,stack) avails wanteds
1689   = go avails wanteds
1690   where
1691     go avails []     = returnNF_Tc avails
1692     go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w        `thenNF_Tc` \ avails' ->
1693                        go avails' ws
1694
1695 reduce_simple_help stack givens wanted
1696   | wanted `elemFM` givens
1697   = returnNF_Tc givens
1698
1699   | Just (clas, tys) <- getClassPredTys_maybe wanted
1700   = lookupSimpleInst clas tys   `thenNF_Tc` \ maybe_theta ->
1701     case maybe_theta of
1702       Nothing ->    returnNF_Tc (addSimpleIrred givens wanted)
1703       Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1704
1705   | otherwise
1706   = returnNF_Tc (addSimpleIrred givens wanted)
1707
1708 addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
1709 addSimpleIrred givens pred
1710   = addSCs (addToFM givens pred True) pred
1711
1712 addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
1713 addNonIrred givens pred
1714   = addSCs (addToFM givens pred False) pred
1715
1716 addSCs givens pred
1717   | not (isClassPred pred) = givens
1718   | otherwise              = foldl add givens sc_theta
1719  where
1720    Just (clas,tys) = getClassPredTys_maybe pred
1721    (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1722    sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1723
1724    add givens ct
1725      = case lookupFM givens ct of
1726        Nothing    -> -- Add it and its superclasses
1727                      addSCs (addToFM givens ct False) ct
1728
1729        Just True  -> -- Set its flag to False; superclasses already done
1730                      addToFM givens ct False
1731
1732        Just False -> -- Already done
1733                      givens
1734
1735 \end{code}
1736
1737
1738 %************************************************************************
1739 %*                                                                      *
1740 \section{Errors and contexts}
1741 %*                                                                      *
1742 %************************************************************************
1743
1744 ToDo: for these error messages, should we note the location as coming
1745 from the insts, or just whatever seems to be around in the monad just
1746 now?
1747
1748 \begin{code}
1749 groupInsts :: [Inst] -> [[Inst]]
1750 -- Group together insts with the same origin
1751 -- We want to report them together in error messages
1752 groupInsts []           = []
1753 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1754                         where
1755                                 -- (It may seem a bit crude to compare the error messages,
1756                                 --  but it makes sure that we combine just what the user sees,
1757                                 --  and it avoids need equality on InstLocs.)
1758                           (friends, others) = partition is_friend insts
1759                           loc_msg           = showSDoc (pprInstLoc (instLoc inst))
1760                           is_friend friend  = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1761
1762
1763 addTopAmbigErrs dicts
1764   = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts)        `thenNF_Tc_`
1765     mapNF_Tc (addTopIPErrs tidy_env)       (groupInsts bad_ips)         `thenNF_Tc_`
1766     mapNF_Tc (addAmbigErr tidy_env)        ambigs                       `thenNF_Tc_`
1767     returnNF_Tc ()
1768   where
1769     fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1770     (tidy_env, tidy_dicts) = tidyInsts dicts
1771     (bad_ips, non_ips)     = partition is_ip tidy_dicts
1772     (no_insts, ambigs)     = partition no_inst non_ips
1773     is_ip d   = any isIPPred (predsOfInst d)
1774     no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1775
1776 plural [x] = empty
1777 plural xs  = char 's'
1778
1779 addTopIPErrs tidy_env tidy_dicts
1780   = addInstErrTcM (instLoc (head tidy_dicts))
1781         (tidy_env,
1782          ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1783
1784 -- Used for top-level irreducibles
1785 addTopInstanceErrs tidy_env tidy_dicts
1786   = addInstErrTcM (instLoc (head tidy_dicts))
1787         (tidy_env,
1788          ptext SLIT("No instance") <> plural tidy_dicts <+>
1789                 ptext SLIT("for") <+> pprInsts tidy_dicts)
1790
1791 addAmbigErrs dicts
1792   = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1793   where
1794     (tidy_env, tidy_dicts) = tidyInsts dicts
1795
1796 addAmbigErr tidy_env tidy_dict
1797   = addInstErrTcM (instLoc tidy_dict)
1798         (tidy_env,
1799          sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1800               nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1801   where
1802     ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1803
1804 warnDefault dicts default_ty
1805   = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
1806     tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1807   where
1808         -- Tidy them first
1809     (_, tidy_dicts) = tidyInsts dicts
1810     get_loc i = case instLoc i of { (_,loc,_) -> loc }
1811     warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1812                                 quotes (ppr default_ty),
1813                       pprInstsInFull tidy_dicts]
1814
1815 complainCheck doc givens irreds
1816   = mapNF_Tc zonkInst given_dicts                                 `thenNF_Tc` \ givens' ->
1817     mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds)  `thenNF_Tc_`
1818     returnNF_Tc ()
1819   where
1820     given_dicts = filter isDict givens
1821         -- Filter out methods, which are only added to
1822         -- the given set as an optimisation
1823
1824 addNoInstanceErrs what_doc givens dicts
1825   = tcGetInstEnv        `thenNF_Tc` \ inst_env ->
1826     let
1827         (tidy_env1, tidy_givens) = tidyInsts givens
1828         (tidy_env2, tidy_dicts)  = tidyMoreInsts tidy_env1 dicts
1829
1830         doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1831                          nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1832                     ambig_doc,
1833                     ptext SLIT("Probable fix:"),
1834                     nest 4 fix1,
1835                     nest 4 fix2]
1836
1837         herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1838         unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1839                     | otherwise     = empty
1840
1841                 -- The error message when we don't find a suitable instance
1842                 -- is complicated by the fact that sometimes this is because
1843                 -- there is no instance, and sometimes it's because there are
1844                 -- too many instances (overlap).  See the comments in TcEnv.lhs
1845                 -- with the InstEnv stuff.
1846
1847         ambig_doc
1848             | not ambig_overlap = empty
1849             | otherwise
1850             = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1851                     nest 4 (ptext SLIT("depends on the instantiation of") <+>
1852                             quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1853
1854         fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1855                     ptext SLIT("to the") <+> what_doc]
1856
1857         fix2 | null instance_dicts
1858              = empty
1859              | otherwise
1860              = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1861
1862         instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1863                 -- Insts for which it is worth suggesting an adding an instance declaration
1864                 -- Exclude implicit parameters, and tyvar dicts
1865
1866             -- Checks for the ambiguous case when we have overlapping instances
1867         ambig_overlap = any ambig_overlap1 dicts
1868         ambig_overlap1 dict
1869                 | isClassDict dict
1870                 = case lookupInstEnv inst_env clas tys of
1871                             NoMatch ambig -> ambig
1872                             other         -> False
1873                 | otherwise = False
1874                 where
1875                   (clas,tys) = getDictClassTys dict
1876     in
1877     addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
1878
1879 -- Used for the ...Thetas variants; all top level
1880 addNoInstErr pred
1881   = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
1882
1883 reduceDepthErr n stack
1884   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1885           ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1886           nest 4 (pprInstsInFull stack)]
1887
1888 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1889
1890 -----------------------------------------------
1891 addCantGenErr inst
1892   = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1893                    nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
1894 \end{code}