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