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, TyVarDetails(VanillaTv),
  45                           mkClassPred, isOverloadedTy, mkTyConApp,
  46                           mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
  47                           tyVarsOfPred, isIPPred, isInheritablePred, 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                           splitName, fstName, sndName )
  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 isInheritablePred (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 --
 674 -- NB: tcSimplifyCheck does not consult the
 675 --      global type variables in the environment; so you don't
 676 --      need to worry about setting them before calling tcSimplifyCheck
 677 tcSimplifyCheck doc qtvs givens wanted_lie
 678   = tcSimplCheck doc get_qtvs
 679                  givens wanted_lie      `thenTc` \ (qtvs', frees, binds) ->
 680     returnTc (frees, binds)
 681   where
 682     get_qtvs = zonkTcTyVarsAndFV qtvs
 683
 684
 685 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
 686 -- against, but we don't know the type variables over which we are going to quantify.
 687 -- This happens when we have a type signature for a mutually recursive group
 688 tcSimplifyInferCheck
 689          :: SDoc
 690          -> TcTyVarSet          -- fv(T)
 691          -> [Inst]              -- Given
 692          -> LIE                 -- Wanted
 693          -> TcM ([TcTyVar],     -- Variables over which to quantify
 694                  LIE,           -- Free
 695                  TcDictBinds)   -- Bindings
 696
 697 tcSimplifyInferCheck doc tau_tvs givens wanted_lie
 698   = tcSimplCheck doc get_qtvs givens wanted_lie
 699   where
 700         -- Figure out which type variables to quantify over
 701         -- You might think it should just be the signature tyvars,
 702         -- but in bizarre cases you can get extra ones
 703         --      f :: forall a. Num a => a -> a
 704         --      f x = fst (g (x, head [])) + 1
 705         --      g a b = (b,a)
 706         -- Here we infer g :: forall a b. a -> b -> (b,a)
 707         -- We don't want g to be monomorphic in b just because
 708         -- f isn't quantified over b.
 709     all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
 710
 711     get_qtvs = zonkTcTyVarsAndFV all_tvs        `thenNF_Tc` \ all_tvs' ->
 712                tcGetGlobalTyVars                `thenNF_Tc` \ gbl_tvs ->
 713                let
 714                   qtvs = all_tvs' `minusVarSet` gbl_tvs
 715                         -- We could close gbl_tvs, but its not necessary for
 716                         -- soundness, and it'll only affect which tyvars, not which
 717                         -- dictionaries, we quantify over
 718                in
 719                returnNF_Tc qtvs
 720 \end{code}
 721
 722 Here is the workhorse function for all three wrappers.
 723
 724 \begin{code}
 725 tcSimplCheck doc get_qtvs givens wanted_lie
 726   = check_loop givens (lieToList wanted_lie)    `thenTc` \ (qtvs, frees, binds, irreds) ->
 727
 728         -- Complain about any irreducible ones
 729     complainCheck doc givens irreds             `thenNF_Tc_`
 730
 731         -- Done
 732     returnTc (qtvs, mkLIE frees, binds)
 733
 734   where
 735     ip_set = mkNameSet (ipNamesOfInsts givens)
 736
 737     check_loop givens wanteds
 738       =         -- Step 1
 739         mapNF_Tc zonkInst givens        `thenNF_Tc` \ givens' ->
 740         mapNF_Tc zonkInst wanteds       `thenNF_Tc` \ wanteds' ->
 741         get_qtvs                        `thenNF_Tc` \ qtvs' ->
 742
 743                     -- Step 2
 744         let
 745             -- When checking against a given signature we always reduce
 746             -- until we find a match against something given, or can't reduce
 747             try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free
 748                         | otherwise                            = ReduceMe
 749         in
 750         reduceContext doc try_me givens' wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
 751
 752                     -- Step 3
 753         if no_improvement then
 754             returnTc (varSetElems qtvs', frees, binds, irreds)
 755         else
 756             check_loop givens' (irreds ++ frees)        `thenTc` \ (qtvs', frees1, binds1, irreds1) ->
 757             returnTc (qtvs', frees1, binds `AndMonoBinds` binds1, irreds1)
 758 \end{code}
 759
 760
 761 %************************************************************************
 762 %*                                                                      *
 763 \subsection{tcSimplifyRestricted}
 764 %*                                                                      *
 765 %************************************************************************
 766
 767 \begin{code}
 768 tcSimplifyRestricted    -- Used for restricted binding groups
 769                         -- i.e. ones subject to the monomorphism restriction
 770         :: SDoc
 771         -> TcTyVarSet           -- Free in the type of the RHSs
 772         -> LIE                  -- Free in the RHSs
 773         -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
 774                 LIE,            -- Free
 775                 TcDictBinds)    -- Bindings
 776
 777 tcSimplifyRestricted doc tau_tvs wanted_lie
 778   =     -- First squash out all methods, to find the constrained tyvars
 779         -- We can't just take the free vars of wanted_lie because that'll
 780         -- have methods that may incidentally mention entirely unconstrained variables
 781         --      e.g. a call to  f :: Eq a => a -> b -> b
 782         -- Here, b is unconstrained.  A good example would be
 783         --      foo = f (3::Int)
 784         -- We want to infer the polymorphic type
 785         --      foo :: forall b. b -> b
 786     let
 787         wanteds = lieToList wanted_lie
 788         try_me inst = ReduceMe          -- Reduce as far as we can.  Don't stop at
 789                                         -- dicts; the idea is to get rid of as many type
 790                                         -- variables as possible, and we don't want to stop
 791                                         -- at (say) Monad (ST s), because that reduces
 792                                         -- immediately, with no constraint on s.
 793     in
 794     simpleReduceLoop doc try_me wanteds         `thenTc` \ (_, _, constrained_dicts) ->
 795
 796         -- Next, figure out the tyvars we will quantify over
 797     zonkTcTyVarsAndFV (varSetElems tau_tvs)     `thenNF_Tc` \ tau_tvs' ->
 798     tcGetGlobalTyVars                           `thenNF_Tc` \ gbl_tvs ->
 799     let
 800         constrained_tvs = tyVarsOfInsts constrained_dicts
 801         qtvs = (tau_tvs' `minusVarSet` oclose (predsOfInsts constrained_dicts) gbl_tvs)
 802                          `minusVarSet` constrained_tvs
 803     in
 804
 805         -- The first step may have squashed more methods than
 806         -- necessary, so try again, this time knowing the exact
 807         -- set of type variables to quantify over.
 808         --
 809         -- We quantify only over constraints that are captured by qtvs;
 810         -- these will just be a subset of non-dicts.  This in contrast
 811         -- to normal inference (using isFreeWhenInferring) in which we quantify over
 812         -- all *non-inheritable* constraints too.  This implements choice
 813         -- (B) under "implicit parameter and monomorphism" above.
 814         --
 815         -- Remember that we may need to do *some* simplification, to
 816         -- (for example) squash {Monad (ST s)} into {}.  It's not enough
 817         -- just to float all constraints
 818     mapNF_Tc zonkInst (lieToList wanted_lie)    `thenNF_Tc` \ wanteds' ->
 819     let
 820         try_me inst | isFreeWrtTyVars qtvs inst = Free
 821                     | otherwise                 = ReduceMe
 822     in
 823     reduceContext doc try_me [] wanteds'        `thenTc` \ (no_improvement, frees, binds, irreds) ->
 824     ASSERT( no_improvement )
 825     ASSERT( null irreds )
 826         -- No need to loop because simpleReduceLoop will have
 827         -- already done any improvement necessary
 828
 829     returnTc (varSetElems qtvs, mkLIE frees, binds)
 830 \end{code}
 831
 832
 833 %************************************************************************
 834 %*                                                                      *
 835 \subsection{tcSimplifyToDicts}
 836 %*                                                                      *
 837 %************************************************************************
 838
 839 On the LHS of transformation rules we only simplify methods and constants,
 840 getting dictionaries.  We want to keep all of them unsimplified, to serve
 841 as the available stuff for the RHS of the rule.
 842
 843 The same thing is used for specialise pragmas. Consider
 844
 845         f :: Num a => a -> a
 846         {-# SPECIALISE f :: Int -> Int #-}
 847         f = ...
 848
 849 The type checker generates a binding like:
 850
 851         f_spec = (f :: Int -> Int)
 852
 853 and we want to end up with
 854
 855         f_spec = _inline_me_ (f Int dNumInt)
 856
 857 But that means that we must simplify the Method for f to (f Int dNumInt)!
 858 So tcSimplifyToDicts squeezes out all Methods.
 859
 860 IMPORTANT NOTE:  we *don't* want to do superclass commoning up.  Consider
 861
 862         fromIntegral :: (Integral a, Num b) => a -> b
 863         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
 864
 865 Here, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont*
 866 want to get
 867
 868         forall dIntegralInt.
 869         fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 870
 871 because the scsel will mess up matching.  Instead we want
 872
 873         forall dIntegralInt, dNumInt.
 874         fromIntegral Int Int dIntegralInt dNumInt = id Int
 875
 876 Hence "DontReduce NoSCs"
 877
 878 \begin{code}
 879 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
 880 tcSimplifyToDicts wanted_lie
 881   = simpleReduceLoop doc try_me wanteds         `thenTc` \ (frees, binds, irreds) ->
 882         -- Since try_me doesn't look at types, we don't need to
 883         -- do any zonking, so it's safe to call reduceContext directly
 884     ASSERT( null frees )
 885     returnTc (irreds, binds)
 886
 887   where
 888     doc = text "tcSimplifyToDicts"
 889     wanteds = lieToList wanted_lie
 890
 891         -- Reduce methods and lits only; stop as soon as we get a dictionary
 892     try_me inst | isDict inst = DontReduce NoSCs
 893                 | otherwise   = ReduceMe
 894 \end{code}
 895
 896
 897 %************************************************************************
 898 %*                                                                      *
 899 \subsection{Filtering at a dynamic binding}
 900 %*                                                                      *
 901 %************************************************************************
 902
 903 When we have
 904         let ?x = R in B
 905
 906 we must discharge all the ?x constraints from B.  We also do an improvement
 907 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.
 908
 909 Actually, the constraints from B might improve the types in ?x. For example
 910
 911         f :: (?x::Int) => Char -> Char
 912         let ?x = 3 in f 'c'
 913
 914 then the constraint (?x::Int) arising from the call to f will
 915 force the binding for ?x to be of type Int.
 916
 917 \begin{code}
 918 tcSimplifyIPs :: [Inst]         -- The implicit parameters bound here
 919               -> LIE
 920               -> TcM (LIE, TcDictBinds)
 921 tcSimplifyIPs given_ips wanted_lie
 922   = simpl_loop given_ips wanteds        `thenTc` \ (frees, binds) ->
 923     returnTc (mkLIE frees, binds)
 924   where
 925     doc      = text "tcSimplifyIPs" <+> ppr given_ips
 926     wanteds  = lieToList wanted_lie
 927     ip_set   = mkNameSet (ipNamesOfInsts given_ips)
 928
 929         -- Simplify any methods that mention the implicit parameter
 930     try_me inst | isFreeWrtIPs ip_set inst = Free
 931                 | otherwise                = ReduceMe
 932
 933     simpl_loop givens wanteds
 934       = mapNF_Tc zonkInst givens                `thenNF_Tc` \ givens' ->
 935         mapNF_Tc zonkInst wanteds               `thenNF_Tc` \ wanteds' ->
 936
 937         reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
 938
 939         if no_improvement then
 940             ASSERT( null irreds )
 941             returnTc (frees, binds)
 942         else
 943             simpl_loop givens' (irreds ++ frees)        `thenTc` \ (frees1, binds1) ->
 944             returnTc (frees1, binds `AndMonoBinds` binds1)
 945 \end{code}
 946
 947
 948 %************************************************************************
 949 %*                                                                      *
 950 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
 951 %*                                                                      *
 952 %************************************************************************
 953
 954 When doing a binding group, we may have @Insts@ of local functions.
 955 For example, we might have...
 956 \begin{verbatim}
 957 let f x = x + 1     -- orig local function (overloaded)
 958     f.1 = f Int     -- two instances of f
 959     f.2 = f Float
 960  in
 961     (f.1 5, f.2 6.7)
 962 \end{verbatim}
 963 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
 964 where @f@ is in scope; those @Insts@ must certainly not be passed
 965 upwards towards the top-level.  If the @Insts@ were binding-ified up
 966 there, they would have unresolvable references to @f@.
 967
 968 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
 969 For each method @Inst@ in the @init_lie@ that mentions one of the
 970 @Ids@, we create a binding.  We return the remaining @Insts@ (in an
 971 @LIE@), as well as the @HsBinds@ generated.
 972
 973 \begin{code}
 974 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
 975
 976 bindInstsOfLocalFuns init_lie local_ids
 977   | null overloaded_ids
 978         -- Common case
 979   = returnTc (init_lie, EmptyMonoBinds)
 980
 981   | otherwise
 982   = simpleReduceLoop doc try_me wanteds         `thenTc` \ (frees, binds, irreds) ->
 983     ASSERT( null irreds )
 984     returnTc (mkLIE frees, binds)
 985   where
 986     doc              = text "bindInsts" <+> ppr local_ids
 987     wanteds          = lieToList init_lie
 988     overloaded_ids   = filter is_overloaded local_ids
 989     is_overloaded id = isOverloadedTy (idType id)
 990
 991     overloaded_set = mkVarSet overloaded_ids    -- There can occasionally be a lot of them
 992                                                 -- so it's worth building a set, so that
 993                                                 -- lookup (in isMethodFor) is faster
 994
 995     try_me inst | isMethodFor overloaded_set inst = ReduceMe
 996                 | otherwise                       = Free
 997 \end{code}
 998
 999
1000 %************************************************************************
1001 %*                                                                      *
1002 \subsection{Data types for the reduction mechanism}
1003 %*                                                                      *
1004 %************************************************************************
1005
1006 The main control over context reduction is here
1007
1008 \begin{code}
1009 data WhatToDo
1010  = ReduceMe             -- Try to reduce this
1011                         -- If there's no instance, behave exactly like
1012                         -- DontReduce: add the inst to
1013                         -- the irreductible ones, but don't
1014                         -- produce an error message of any kind.
1015                         -- It might be quite legitimate such as (Eq a)!
1016
1017  | DontReduce WantSCs           -- Return as irreducible
1018
1019  | DontReduceUnlessConstant     -- Return as irreducible unless it can
1020                                 -- be reduced to a constant in one step
1021
1022  | Free                   -- Return as free
1023
1024 reduceMe :: Inst -> WhatToDo
1025 reduceMe inst = ReduceMe
1026
1027 data WantSCs = NoSCs | AddSCs   -- Tells whether we should add the superclasses
1028                                 -- of a predicate when adding it to the avails
1029 \end{code}
1030
1031
1032
1033 \begin{code}
1034 type Avails = FiniteMap Inst Avail
1035
1036 data Avail
1037   = IsFree              -- Used for free Insts
1038   | Irred               -- Used for irreducible dictionaries,
1039                         -- which are going to be lambda bound
1040
1041   | Given TcId          -- Used for dictionaries for which we have a binding
1042                         -- e.g. those "given" in a signature
1043           Bool          -- True <=> actually consumed (splittable IPs only)
1044
1045   | NoRhs               -- Used for Insts like (CCallable f)
1046                         -- where no witness is required.
1047
1048   | Rhs                 -- Used when there is a RHS
1049         TcExpr          -- The RHS
1050         [Inst]          -- Insts free in the RHS; we need these too
1051
1052   | Linear              -- Splittable Insts only.
1053         Int             -- The Int is always 2 or more; indicates how
1054                         -- many copies are required
1055         Inst            -- The splitter
1056         Avail           -- Where the "master copy" is
1057
1058   | LinRhss             -- Splittable Insts only; this is used only internally
1059                         --      by extractResults, where a Linear
1060                         --      is turned into an LinRhss
1061         [TcExpr]        -- A supply of suitable RHSs
1062
1063 pprAvails avails = vcat [sep [ppr inst, nest 2 (equals <+> pprAvail avail)]
1064                         | (inst,avail) <- fmToList avails ]
1065
1066 instance Outputable Avail where
1067     ppr = pprAvail
1068
1069 pprAvail NoRhs          = text "<no rhs>"
1070 pprAvail IsFree         = text "Free"
1071 pprAvail Irred          = text "Irred"
1072 pprAvail (Given x b)    = text "Given" <+> ppr x <+>
1073                           if b then text "(used)" else empty
1074 pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
1075 pprAvail (Linear n i a) = text "Linear" <+> ppr n <+> braces (ppr i) <+> ppr a
1076 pprAvail (LinRhss rhss) = text "LinRhss" <+> ppr rhss
1077 \end{code}
1078
1079 Extracting the bindings from a bunch of Avails.
1080 The bindings do *not* come back sorted in dependency order.
1081 We assume that they'll be wrapped in a big Rec, so that the
1082 dependency analyser can sort them out later
1083
1084 The loop startes
1085 \begin{code}
1086 extractResults :: Avails
1087                -> [Inst]                -- Wanted
1088                -> NF_TcM (TcDictBinds,  -- Bindings
1089                           [Inst],       -- Irreducible ones
1090                           [Inst])       -- Free ones
1091
1092 extractResults avails wanteds
1093   = go avails EmptyMonoBinds [] [] wanteds
1094   where
1095     go avails binds irreds frees []
1096       = returnNF_Tc (binds, irreds, frees)
1097
1098     go avails binds irreds frees (w:ws)
1099       = case lookupFM avails w of
1100           Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
1101                         go avails binds irreds frees ws
1102
1103           Just NoRhs  -> go avails               binds irreds     frees     ws
1104           Just IsFree -> go (add_free avails w)  binds irreds     (w:frees) ws
1105           Just Irred  -> go (add_given avails w) binds (w:irreds) frees     ws
1106
1107           Just (Given id _) -> go avails new_binds irreds frees ws
1108                             where
1109                                new_binds | id == instToId w = binds
1110                                          | otherwise        = addBind binds w (HsVar id)
1111                 -- The sought Id can be one of the givens, via a superclass chain
1112                 -- and then we definitely don't want to generate an x=x binding!
1113
1114           Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds frees (ws' ++ ws)
1115                              where
1116                                 new_binds = addBind binds w rhs
1117
1118           Just (Linear n split_inst avail)      -- Transform Linear --> LinRhss
1119             -> get_root irreds frees avail w            `thenNF_Tc` \ (irreds', frees', root_id) ->
1120                split n (instToId split_inst) root_id w  `thenNF_Tc` \ (binds', rhss) ->
1121                go (addToFM avails w (LinRhss rhss))
1122                   (binds `AndMonoBinds` binds')
1123                   irreds' frees' (split_inst : w : ws)
1124
1125           Just (LinRhss (rhs:rhss))             -- Consume one of the Rhss
1126                 -> go new_avails new_binds irreds frees ws
1127                 where
1128                    new_binds  = addBind binds w rhs
1129                    new_avails = addToFM avails w (LinRhss rhss)
1130
1131     get_root irreds frees (Given id _) w = returnNF_Tc (irreds, frees, id)
1132     get_root irreds frees Irred        w = cloneDict w  `thenNF_Tc` \ w' ->
1133                                            returnNF_Tc (w':irreds, frees, instToId w')
1134     get_root irreds frees IsFree       w = cloneDict w  `thenNF_Tc` \ w' ->
1135                                            returnNF_Tc (irreds, w':frees, instToId w')
1136
1137     add_given avails w
1138         | instBindingRequired w = addToFM avails w (Given (instToId w) True)
1139         | otherwise             = addToFM avails w NoRhs
1140         -- NB: make sure that CCallable/CReturnable use NoRhs rather
1141         --      than Given, else we end up with bogus bindings.
1142
1143     add_free avails w | isMethod w = avails
1144                       | otherwise  = add_given avails w
1145         -- NB: Hack alert!
1146         -- Do *not* replace Free by Given if it's a method.
1147         -- The following situation shows why this is bad:
1148         --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1149         -- From an application (truncate f i) we get
1150         --      t1 = truncate at f
1151         --      t2 = t1 at i
1152         -- If we have also have a second occurrence of truncate, we get
1153         --      t3 = truncate at f
1154         --      t4 = t3 at i
1155         -- When simplifying with i,f free, we might still notice that
1156         --   t1=t3; but alas, the binding for t2 (which mentions t1)
1157         --   will continue to float out!
1158         -- (split n i a) returns: n rhss
1159         --                        auxiliary bindings
1160         --                        1 or 0 insts to add to irreds
1161
1162
1163 split :: Int -> TcId -> TcId -> Inst
1164       -> NF_TcM (TcDictBinds, [TcExpr])
1165 -- (split n split_id root_id wanted) returns
1166 --      * a list of 'n' expressions, all of which witness 'avail'
1167 --      * a bunch of auxiliary bindings to support these expressions
1168 --      * one or zero insts needed to witness the whole lot
1169 --        (maybe be zero if the initial Inst is a Given)
1170 --
1171 -- NB: 'wanted' is just a template
1172
1173 split n split_id root_id wanted
1174   = go n
1175   where
1176     ty      = linearInstType wanted
1177     pair_ty = mkTyConApp pairTyCon [ty,ty]
1178     id      = instToId wanted
1179     occ     = getOccName id
1180     loc     = getSrcLoc id
1181
1182     go 1 = returnNF_Tc (EmptyMonoBinds, [HsVar root_id])
1183
1184     go n = go ((n+1) `div` 2)           `thenNF_Tc` \ (binds1, rhss) ->
1185            expand n rhss                `thenNF_Tc` \ (binds2, rhss') ->
1186            returnNF_Tc (binds1 `AndMonoBinds` binds2, rhss')
1187
1188         -- (expand n rhss)
1189         -- Given ((n+1)/2) rhss, make n rhss, using auxiliary bindings
1190         --  e.g.  expand 3 [rhs1, rhs2]
1191         --        = ( { x = split rhs1 },
1192         --            [fst x, snd x, rhs2] )
1193     expand n rhss
1194         | n `rem` 2 == 0 = go rhss      -- n is even
1195         | otherwise      = go (tail rhss)       `thenNF_Tc` \ (binds', rhss') ->
1196                            returnNF_Tc (binds', head rhss : rhss')
1197         where
1198           go rhss = mapAndUnzipNF_Tc do_one rhss        `thenNF_Tc` \ (binds', rhss') ->
1199                     returnNF_Tc (andMonoBindList binds', concat rhss')
1200
1201           do_one rhs = tcGetUnique                      `thenNF_Tc` \ uniq ->
1202                        tcLookupGlobalId fstName         `thenNF_Tc` \ fst_id ->
1203                        tcLookupGlobalId sndName         `thenNF_Tc` \ snd_id ->
1204                        let
1205                           x = mkUserLocal occ uniq pair_ty loc
1206                        in
1207                        returnNF_Tc (VarMonoBind x (mk_app split_id rhs),
1208                                     [mk_fs_app fst_id ty x, mk_fs_app snd_id ty x])
1209
1210 mk_fs_app id ty var = HsVar id `TyApp` [ty,ty] `HsApp` HsVar var
1211
1212 mk_app id rhs = HsApp (HsVar id) rhs
1213
1214 addBind binds inst rhs = binds `AndMonoBinds` VarMonoBind (instToId inst) rhs
1215 \end{code}
1216
1217
1218 %************************************************************************
1219 %*                                                                      *
1220 \subsection[reduce]{@reduce@}
1221 %*                                                                      *
1222 %************************************************************************
1223
1224 When the "what to do" predicate doesn't depend on the quantified type variables,
1225 matters are easier.  We don't need to do any zonking, unless the improvement step
1226 does something, in which case we zonk before iterating.
1227
1228 The "given" set is always empty.
1229
1230 \begin{code}
1231 simpleReduceLoop :: SDoc
1232                  -> (Inst -> WhatToDo)          -- What to do, *not* based on the quantified type variables
1233                  -> [Inst]                      -- Wanted
1234                  -> TcM ([Inst],                -- Free
1235                          TcDictBinds,
1236                          [Inst])                -- Irreducible
1237
1238 simpleReduceLoop doc try_me wanteds
1239   = mapNF_Tc zonkInst wanteds                   `thenNF_Tc` \ wanteds' ->
1240     reduceContext doc try_me [] wanteds'        `thenTc` \ (no_improvement, frees, binds, irreds) ->
1241     if no_improvement then
1242         returnTc (frees, binds, irreds)
1243     else
1244         simpleReduceLoop doc try_me (irreds ++ frees)   `thenTc` \ (frees1, binds1, irreds1) ->
1245         returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
1246 \end{code}
1247
1248
1249
1250 \begin{code}
1251 reduceContext :: SDoc
1252               -> (Inst -> WhatToDo)
1253               -> [Inst]                 -- Given
1254               -> [Inst]                 -- Wanted
1255               -> NF_TcM (Bool,          -- True <=> improve step did no unification
1256                          [Inst],        -- Free
1257                          TcDictBinds,   -- Dictionary bindings
1258                          [Inst])        -- Irreducible
1259
1260 reduceContext doc try_me givens wanteds
1261   =
1262     traceTc (text "reduceContext" <+> (vcat [
1263              text "----------------------",
1264              doc,
1265              text "given" <+> ppr givens,
1266              text "wanted" <+> ppr wanteds,
1267              text "----------------------"
1268              ]))                                        `thenNF_Tc_`
1269
1270         -- Build the Avail mapping from "givens"
1271     foldlNF_Tc addGiven emptyFM givens                  `thenNF_Tc` \ init_state ->
1272
1273         -- Do the real work
1274     reduceList (0,[]) try_me wanteds init_state         `thenNF_Tc` \ avails ->
1275
1276         -- Do improvement, using everything in avails
1277         -- In particular, avails includes all superclasses of everything
1278     tcImprove avails                                    `thenTc` \ no_improvement ->
1279
1280     extractResults avails wanteds                       `thenNF_Tc` \ (binds, irreds, frees) ->
1281
1282     traceTc (text "reduceContext end" <+> (vcat [
1283              text "----------------------",
1284              doc,
1285              text "given" <+> ppr givens,
1286              text "wanted" <+> ppr wanteds,
1287              text "----",
1288              text "avails" <+> pprAvails avails,
1289              text "frees" <+> ppr frees,
1290              text "no_improvement =" <+> ppr no_improvement,
1291              text "----------------------"
1292              ]))                                        `thenNF_Tc_`
1293
1294     returnTc (no_improvement, frees, binds, irreds)
1295
1296 tcImprove avails
1297  =  tcGetInstEnv                                `thenTc` \ inst_env ->
1298     let
1299         preds = [ (pred, pp_loc)
1300                 | inst <- keysFM avails,
1301                   let pp_loc = pprInstLoc (instLoc inst),
1302                   pred <- predsOfInst inst,
1303                   predHasFDs pred
1304                 ]
1305                 -- Avails has all the superclasses etc (good)
1306                 -- It also has all the intermediates of the deduction (good)
1307                 -- It does not have duplicates (good)
1308                 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
1309                 --    so that improve will see them separate
1310         eqns  = improve (classInstEnv inst_env) preds
1311      in
1312      if null eqns then
1313         returnTc True
1314      else
1315         traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))     `thenNF_Tc_`
1316         mapTc_ unify eqns       `thenTc_`
1317         returnTc False
1318   where
1319     unify ((qtvs, t1, t2), doc)
1320          = tcAddErrCtxt doc                             $
1321            tcInstTyVars VanillaTv (varSetElems qtvs)    `thenNF_Tc` \ (_, _, tenv) ->
1322            unifyTauTy (substTy tenv t1) (substTy tenv t2)
1323 \end{code}
1324
1325 The main context-reduction function is @reduce@.  Here's its game plan.
1326
1327 \begin{code}
1328 reduceList :: (Int,[Inst])              -- Stack (for err msgs)
1329                                         -- along with its depth
1330            -> (Inst -> WhatToDo)
1331            -> [Inst]
1332            -> Avails
1333            -> TcM Avails
1334 \end{code}
1335
1336 @reduce@ is passed
1337      try_me:    given an inst, this function returns
1338                   Reduce       reduce this
1339                   DontReduce   return this in "irreds"
1340                   Free         return this in "frees"
1341
1342      wanteds:   The list of insts to reduce
1343      state:     An accumulating parameter of type Avails
1344                 that contains the state of the algorithm
1345
1346   It returns a Avails.
1347
1348 The (n,stack) pair is just used for error reporting.
1349 n is always the depth of the stack.
1350 The stack is the stack of Insts being reduced: to produce X
1351 I had to produce Y, to produce Y I had to produce Z, and so on.
1352
1353 \begin{code}
1354 reduceList (n,stack) try_me wanteds state
1355   | n > opt_MaxContextReductionDepth
1356   = failWithTc (reduceDepthErr n stack)
1357
1358   | otherwise
1359   =
1360 #ifdef DEBUG
1361    (if n > 8 then
1362         pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1363     else (\x->x))
1364 #endif
1365     go wanteds state
1366   where
1367     go []     state = returnTc state
1368     go (w:ws) state = reduce (n+1, w:stack) try_me w state      `thenTc` \ state' ->
1369                       go ws state'
1370
1371     -- Base case: we're done!
1372 reduce stack try_me wanted state
1373     -- It's the same as an existing inst, or a superclass thereof
1374   | Just avail <- isAvailable state wanted
1375   = if isLinearInst wanted then
1376         addLinearAvailable state avail wanted   `thenNF_Tc` \ (state', wanteds') ->
1377         reduceList stack try_me wanteds' state'
1378     else
1379         returnTc state          -- No op for non-linear things
1380
1381   | otherwise
1382   = case try_me wanted of {
1383
1384       DontReduce want_scs -> addIrred want_scs state wanted
1385
1386     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
1387                                      -- First, see if the inst can be reduced to a constant in one step
1388         try_simple (addIrred AddSCs)    -- Assume want superclasses
1389
1390     ; Free ->   -- It's free so just chuck it upstairs
1391                 -- First, see if the inst can be reduced to a constant in one step
1392         try_simple addFree
1393
1394     ; ReduceMe ->               -- It should be reduced
1395         lookupInst wanted             `thenNF_Tc` \ lookup_result ->
1396         case lookup_result of
1397             GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' ->
1398                                     addWanted state' wanted rhs wanteds'
1399             SimpleInst rhs       -> addWanted state wanted rhs []
1400
1401             NoInstance ->    -- No such instance!
1402                              -- Add it and its superclasses
1403                              addIrred AddSCs state wanted
1404
1405     }
1406   where
1407     try_simple do_this_otherwise
1408       = lookupInst wanted         `thenNF_Tc` \ lookup_result ->
1409         case lookup_result of
1410             SimpleInst rhs -> addWanted state wanted rhs []
1411             other          -> do_this_otherwise state wanted
1412 \end{code}
1413
1414
1415 \begin{code}
1416 -------------------------
1417 isAvailable :: Avails -> Inst -> Maybe Avail
1418 isAvailable avails wanted = lookupFM avails wanted
1419         -- NB 1: the Ord instance of Inst compares by the class/type info
1420         -- *not* by unique.  So
1421         --      d1::C Int ==  d2::C Int
1422
1423 addLinearAvailable :: Avails -> Avail -> Inst -> NF_TcM (Avails, [Inst])
1424 addLinearAvailable avails avail wanted
1425         -- avails currently maps [wanted -> avail]
1426         -- Extend avails to reflect a neeed for an extra copy of avail
1427
1428   | Just avail' <- split_avail avail
1429   = returnNF_Tc (addToFM avails wanted avail', [])
1430
1431   | otherwise
1432   = tcLookupGlobalId splitName                  `thenNF_Tc` \ split_id ->
1433     newMethodAtLoc (instLoc wanted) split_id
1434                    [linearInstType wanted]      `thenNF_Tc` \ (split_inst,_) ->
1435     returnNF_Tc (addToFM avails wanted (Linear 2 split_inst avail), [split_inst])
1436
1437   where
1438     split_avail :: Avail -> Maybe Avail
1439         -- (Just av) if there's a modified version of avail that
1440         --           we can use to replace avail in avails
1441         -- Nothing   if there isn't, so we need to create a Linear
1442     split_avail (Linear n i a)              = Just (Linear (n+1) i a)
1443     split_avail (Given id used) | not used  = Just (Given id True)
1444                                 | otherwise = Nothing
1445     split_avail Irred                       = Nothing
1446     split_avail IsFree                      = Nothing
1447     split_avail other = pprPanic "addLinearAvailable" (ppr avail $$ ppr wanted $$ ppr avails)
1448
1449 -------------------------
1450 addFree :: Avails -> Inst -> NF_TcM Avails
1451         -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1452         -- to avails, so that any other equal Insts will be commoned up right
1453         -- here rather than also being tossed upstairs.  This is really just
1454         -- an optimisation, and perhaps it is more trouble that it is worth,
1455         -- as the following comments show!
1456         --
1457         -- NB: do *not* add superclasses.  If we have
1458         --      df::Floating a
1459         --      dn::Num a
1460         -- but a is not bound here, then we *don't* want to derive
1461         -- dn from df here lest we lose sharing.
1462         --
1463 addFree avails free = returnNF_Tc (addToFM avails free IsFree)
1464
1465 addWanted :: Avails -> Inst -> TcExpr -> [Inst] -> NF_TcM Avails
1466 addWanted avails wanted rhs_expr wanteds
1467   = ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
1468     addAvailAndSCs avails wanted avail
1469   where
1470     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1471           | otherwise                  = ASSERT( null wanteds ) NoRhs
1472
1473 addGiven :: Avails -> Inst -> NF_TcM Avails
1474 addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
1475         -- No ASSERT( not (given `elemFM` avails) ) because in an instance
1476         -- decl for Ord t we can add both Ord t and Eq t as 'givens',
1477         -- so the assert isn't true
1478
1479 addIrred :: WantSCs -> Avails -> Inst -> NF_TcM Avails
1480 addIrred NoSCs  avails irred = returnNF_Tc (addToFM avails irred Irred)
1481 addIrred AddSCs avails irred = ASSERT2( not (irred `elemFM` avails), ppr irred $$ ppr avails )
1482                                addAvailAndSCs avails irred Irred
1483
1484 addAvailAndSCs :: Avails -> Inst -> Avail -> NF_TcM Avails
1485 addAvailAndSCs avails inst avail
1486   | not (isClassDict inst) = returnNF_Tc avails1
1487   | otherwise              = addSCs is_loop avails1 inst
1488   where
1489     avails1 = addToFM avails inst avail
1490     is_loop inst = inst `elem` deps     -- Note: this compares by *type*, not by Unique
1491     deps         = findAllDeps avails avail
1492
1493 findAllDeps :: Avails -> Avail -> [Inst]
1494 -- Find all the Insts that this one depends on
1495 -- See Note [SUPERCLASS-LOOP]
1496 findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
1497 findAllDeps avails other        = []
1498
1499 find_all_deps_help :: Avails -> Inst -> [Inst]
1500 find_all_deps_help avails inst
1501   = case lookupFM avails inst of
1502         Just avail -> findAllDeps avails avail
1503         Nothing    -> []
1504
1505 addSCs :: (Inst -> Bool) -> Avails -> Inst -> NF_TcM Avails
1506         -- Add all the superclasses of the Inst to Avails
1507         -- The first param says "dont do this because the original thing
1508         --      depends on this one, so you'd build a loop"
1509         -- Invariant: the Inst is already in Avails.
1510
1511 addSCs is_loop avails dict
1512   = newDictsFromOld dict sc_theta'      `thenNF_Tc` \ sc_dicts ->
1513     foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1514   where
1515     (clas, tys) = getDictClassTys dict
1516     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1517     sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1518
1519     add_sc avails (sc_dict, sc_sel)     -- Add it, and its superclasses
1520       = case lookupFM avails sc_dict of
1521           Just (Given _ _) -> returnNF_Tc avails        -- Given is cheaper than
1522                                                         --   a superclass selection
1523           Just other | is_loop sc_dict -> returnNF_Tc avails    -- See Note [SUPERCLASS-LOOP]
1524                      | otherwise       -> returnNF_Tc avails'   -- SCs already added
1525
1526           Nothing -> addSCs is_loop avails' sc_dict
1527       where
1528         sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1529         avail      = Rhs sc_sel_rhs [dict]
1530         avails'    = addToFM avails sc_dict avail
1531 \end{code}
1532
1533 Note [SUPERCLASS-LOOP]: Checking for loops
1534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1535 We have to be careful here.  If we are *given* d1:Ord a,
1536 and want to deduce (d2:C [a]) where
1537
1538         class Ord a => C a where
1539         instance Ord a => C [a] where ...
1540
1541 Then we'll use the instance decl to deduce C [a] and then add the
1542 superclasses of C [a] to avails.  But we must not overwrite the binding
1543 for d1:Ord a (which is given) with a superclass selection or we'll just
1544 build a loop!
1545
1546 Here's another example
1547         class Eq b => Foo a b
1548         instance Eq a => Foo [a] a
1549 If we are reducing
1550         (Foo [t] t)
1551
1552 we'll first deduce that it holds (via the instance decl).  We must not
1553 then overwrite the Eq t constraint with a superclass selection!
1554
1555 At first I had a gross hack, whereby I simply did not add superclass constraints
1556 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
1557 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1558 I found a very obscure program (now tcrun021) in which improvement meant the
1559 simplifier got two bites a the cherry... so something seemed to be an Irred
1560 first time, but reducible next time.
1561
1562 Now we implement the Right Solution, which is to check for loops directly
1563 when adding superclasses.  It's a bit like the occurs check in unification.
1564
1565
1566
1567 %************************************************************************
1568 %*                                                                      *
1569 \section{tcSimplifyTop: defaulting}
1570 %*                                                                      *
1571 %************************************************************************
1572
1573
1574 @tcSimplifyTop@ is called once per module to simplify all the constant
1575 and ambiguous Insts.
1576
1577 We need to be careful of one case.  Suppose we have
1578
1579         instance Num a => Num (Foo a b) where ...
1580
1581 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)).  Then it'll simplify
1582 to (Num x), and default x to Int.  But what about y??
1583
1584 It's OK: the final zonking stage should zap y to (), which is fine.
1585
1586
1587 \begin{code}
1588 tcSimplifyTop :: LIE -> TcM TcDictBinds
1589 tcSimplifyTop wanted_lie
1590   = simpleReduceLoop (text "tcSimplTop") reduceMe wanteds       `thenTc` \ (frees, binds, irreds) ->
1591     ASSERT( null frees )
1592
1593     let
1594                 -- All the non-std ones are definite errors
1595         (stds, non_stds) = partition isStdClassTyVarDict irreds
1596
1597                 -- Group by type variable
1598         std_groups = equivClasses cmp_by_tyvar stds
1599
1600                 -- Pick the ones which its worth trying to disambiguate
1601         (std_oks, std_bads) = partition worth_a_try std_groups
1602
1603                 -- Have a try at disambiguation
1604                 -- if the type variable isn't bound
1605                 -- up with one of the non-standard classes
1606         worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1607         non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
1608
1609                 -- Collect together all the bad guys
1610         bad_guys = non_stds ++ concat std_bads
1611     in
1612
1613     ifErrsTc (returnTc []) (
1614         -- Don't check for ambiguous things
1615         -- if there has been an error; errors often
1616         -- give rise to spurious ambiguous Insts
1617
1618
1619         -- And complain about the ones that don't fall under
1620         -- the Haskell rules for disambiguation
1621         -- This group includes both non-existent instances
1622         --      e.g. Num (IO a) and Eq (Int -> Int)
1623         -- and ambiguous dictionaries
1624         --      e.g. Num a
1625         addTopAmbigErrs bad_guys        `thenNF_Tc_`
1626
1627         -- Disambiguate the ones that look feasible
1628         mapTc disambigGroup std_oks
1629     )                                   `thenTc` \ binds_ambig ->
1630
1631
1632     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1633   where
1634     wanteds     = lieToList wanted_lie
1635
1636     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1637
1638 get_tv d   = case getDictClassTys d of
1639                    (clas, [ty]) -> tcGetTyVar "tcSimplify" ty
1640 get_clas d = case getDictClassTys d of
1641                    (clas, [ty]) -> clas
1642 \end{code}
1643
1644 If a dictionary constrains a type variable which is
1645         * not mentioned in the environment
1646         * and not mentioned in the type of the expression
1647 then it is ambiguous. No further information will arise to instantiate
1648 the type variable; nor will it be generalised and turned into an extra
1649 parameter to a function.
1650
1651 It is an error for this to occur, except that Haskell provided for
1652 certain rules to be applied in the special case of numeric types.
1653 Specifically, if
1654         * at least one of its classes is a numeric class, and
1655         * all of its classes are numeric or standard
1656 then the type variable can be defaulted to the first type in the
1657 default-type list which is an instance of all the offending classes.
1658
1659 So here is the function which does the work.  It takes the ambiguous
1660 dictionaries and either resolves them (producing bindings) or
1661 complains.  It works by splitting the dictionary list by type
1662 variable, and using @disambigOne@ to do the real business.
1663
1664 @disambigOne@ assumes that its arguments dictionaries constrain all
1665 the same type variable.
1666
1667 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1668 @()@ instead of @Int@.  I reckon this is the Right Thing to do since
1669 the most common use of defaulting is code like:
1670 \begin{verbatim}
1671         _ccall_ foo     `seqPrimIO` bar
1672 \end{verbatim}
1673 Since we're not using the result of @foo@, the result if (presumably)
1674 @void@.
1675
1676 \begin{code}
1677 disambigGroup :: [Inst] -- All standard classes of form (C a)
1678               -> TcM TcDictBinds
1679
1680 disambigGroup dicts
1681   |   any isNumericClass classes        -- Guaranteed all standard classes
1682           -- see comment at the end of function for reasons as to
1683           -- why the defaulting mechanism doesn't apply to groups that
1684           -- include CCallable or CReturnable dicts.
1685    && not (any isCcallishClass classes)
1686   =     -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1687         -- SO, TRY DEFAULT TYPES IN ORDER
1688
1689         -- Failure here is caused by there being no type in the
1690         -- default list which can satisfy all the ambiguous classes.
1691         -- For example, if Real a is reqd, but the only type in the
1692         -- default list is Int.
1693     tcGetDefaultTys                     `thenNF_Tc` \ default_tys ->
1694     let
1695       try_default []    -- No defaults work, so fail
1696         = failTc
1697
1698       try_default (default_ty : default_tys)
1699         = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
1700                                                 -- default_tys instead
1701           tcSimplifyDefault theta               `thenTc` \ _ ->
1702           returnTc default_ty
1703         where
1704           theta = [mkClassPred clas [default_ty] | clas <- classes]
1705     in
1706         -- See if any default works, and if so bind the type variable to it
1707         -- If not, add an AmbigErr
1708     recoverTc (addAmbigErrs dicts                       `thenNF_Tc_`
1709                returnTc EmptyMonoBinds) $
1710
1711     try_default default_tys                     `thenTc` \ chosen_default_ty ->
1712
1713         -- Bind the type variable and reduce the context, for real this time
1714     unifyTauTy chosen_default_ty (mkTyVarTy tyvar)      `thenTc_`
1715     simpleReduceLoop (text "disambig" <+> ppr dicts)
1716                      reduceMe dicts                     `thenTc` \ (frees, binds, ambigs) ->
1717     WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1718     warnDefault dicts chosen_default_ty                 `thenTc_`
1719     returnTc binds
1720
1721   | all isCreturnableClass classes
1722   =     -- Default CCall stuff to (); we don't even both to check that () is an
1723         -- instance of CReturnable, because we know it is.
1724     unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
1725     returnTc EmptyMonoBinds
1726
1727   | otherwise -- No defaults
1728   = addAmbigErrs dicts  `thenNF_Tc_`
1729     returnTc EmptyMonoBinds
1730
1731   where
1732     tyvar       = get_tv (head dicts)           -- Should be non-empty
1733     classes     = map get_clas dicts
1734 \end{code}
1735
1736 [Aside - why the defaulting mechanism is turned off when
1737  dealing with arguments and results to ccalls.
1738
1739 When typechecking _ccall_s, TcExpr ensures that the external
1740 function is only passed arguments (and in the other direction,
1741 results) of a restricted set of 'native' types. This is
1742 implemented via the help of the pseudo-type classes,
1743 @CReturnable@ (CR) and @CCallable@ (CC.)
1744
1745 The interaction between the defaulting mechanism for numeric
1746 values and CC & CR can be a bit puzzling to the user at times.
1747 For example,
1748
1749     x <- _ccall_ f
1750     if (x /= 0) then
1751        _ccall_ g x
1752      else
1753        return ()
1754
1755 What type has 'x' got here? That depends on the default list
1756 in operation, if it is equal to Haskell 98's default-default
1757 of (Integer, Double), 'x' has type Double, since Integer
1758 is not an instance of CR. If the default list is equal to
1759 Haskell 1.4's default-default of (Int, Double), 'x' has type
1760 Int.
1761
1762 To try to minimise the potential for surprises here, the
1763 defaulting mechanism is turned off in the presence of
1764 CCallable and CReturnable.
1765
1766 End of aside]
1767
1768
1769 %************************************************************************
1770 %*                                                                      *
1771 \subsection[simple]{@Simple@ versions}
1772 %*                                                                      *
1773 %************************************************************************
1774
1775 Much simpler versions when there are no bindings to make!
1776
1777 @tcSimplifyThetas@ simplifies class-type constraints formed by
1778 @deriving@ declarations and when specialising instances.  We are
1779 only interested in the simplified bunch of class/type constraints.
1780
1781 It simplifies to constraints of the form (C a b c) where
1782 a,b,c are type variables.  This is required for the context of
1783 instance declarations.
1784
1785 \begin{code}
1786 tcSimplifyDeriv :: [TyVar]
1787                 -> ThetaType            -- Wanted
1788                 -> TcM ThetaType        -- Needed
1789
1790 tcSimplifyDeriv tyvars theta
1791   = tcInstTyVars VanillaTv tyvars                       `thenNF_Tc` \ (tvs, _, tenv) ->
1792         -- The main loop may do unification, and that may crash if
1793         -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
1794         -- ToDo: what if two of them do get unified?
1795     newDicts DataDeclOrigin (substTheta tenv theta)     `thenNF_Tc` \ wanteds ->
1796     simpleReduceLoop doc reduceMe wanteds               `thenTc` \ (frees, _, irreds) ->
1797     ASSERT( null frees )                        -- reduceMe never returns Free
1798
1799     doptsTc Opt_AllowUndecidableInstances               `thenNF_Tc` \ undecidable_ok ->
1800     let
1801         tv_set      = mkVarSet tvs
1802         simpl_theta = map dictPred irreds       -- reduceMe squashes all non-dicts
1803
1804         check_pred pred
1805           | isEmptyVarSet pred_tyvars   -- Things like (Eq T) should be rejected
1806           = addErrTc (noInstErr pred)
1807
1808           | not undecidable_ok && not (isTyVarClassPred pred)
1809           -- Check that the returned dictionaries are all of form (C a b)
1810           --    (where a, b are type variables).
1811           -- We allow this if we had -fallow-undecidable-instances,
1812           -- but note that risks non-termination in the 'deriving' context-inference
1813           -- fixpoint loop.   It is useful for situations like
1814           --    data Min h a = E | M a (h a)
1815           -- which gives the instance decl
1816           --    instance (Eq a, Eq (h a)) => Eq (Min h a)
1817           = addErrTc (noInstErr pred)
1818
1819           | not (pred_tyvars `subVarSet` tv_set)
1820           -- Check for a bizarre corner case, when the derived instance decl should
1821           -- have form  instance C a b => D (T a) where ...
1822           -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
1823           -- of problems; in particular, it's hard to compare solutions for
1824           -- equality when finding the fixpoint.  So I just rule it out for now.
1825           = addErrTc (badDerivedPred pred)
1826
1827           | otherwise
1828           = returnNF_Tc ()
1829           where
1830             pred_tyvars = tyVarsOfPred pred
1831
1832         rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
1833                 -- This reverse-mapping is a Royal Pain,
1834                 -- but the result should mention TyVars not TcTyVars
1835     in
1836
1837     mapNF_Tc check_pred simpl_theta             `thenNF_Tc_`
1838     checkAmbiguity tvs simpl_theta tv_set       `thenTc_`
1839     returnTc (substTheta rev_env simpl_theta)
1840   where
1841     doc    = ptext SLIT("deriving classes for a data type")
1842 \end{code}
1843
1844 @tcSimplifyDefault@ just checks class-type constraints, essentially;
1845 used with \tr{default} declarations.  We are only interested in
1846 whether it worked or not.
1847
1848 \begin{code}
1849 tcSimplifyDefault :: ThetaType  -- Wanted; has no type variables in it
1850                   -> TcM ()
1851
1852 tcSimplifyDefault theta
1853   = newDicts DataDeclOrigin theta               `thenNF_Tc` \ wanteds ->
1854     simpleReduceLoop doc reduceMe wanteds       `thenTc` \ (frees, _, irreds) ->
1855     ASSERT( null frees )        -- try_me never returns Free
1856     mapNF_Tc (addErrTc . noInstErr) irreds      `thenNF_Tc_`
1857     if null irreds then
1858         returnTc ()
1859     else
1860         failTc
1861   where
1862     doc = ptext SLIT("default declaration")
1863 \end{code}
1864
1865
1866 %************************************************************************
1867 %*                                                                      *
1868 \section{Errors and contexts}
1869 %*                                                                      *
1870 %************************************************************************
1871
1872 ToDo: for these error messages, should we note the location as coming
1873 from the insts, or just whatever seems to be around in the monad just
1874 now?
1875
1876 \begin{code}
1877 groupInsts :: [Inst] -> [[Inst]]
1878 -- Group together insts with the same origin
1879 -- We want to report them together in error messages
1880 groupInsts []           = []
1881 groupInsts (inst:insts) = (inst:friends) : groupInsts others
1882                         where
1883                                 -- (It may seem a bit crude to compare the error messages,
1884                                 --  but it makes sure that we combine just what the user sees,
1885                                 --  and it avoids need equality on InstLocs.)
1886                           (friends, others) = partition is_friend insts
1887                           loc_msg           = showSDoc (pprInstLoc (instLoc inst))
1888                           is_friend friend  = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
1889
1890
1891 addTopAmbigErrs dicts
1892   = mapNF_Tc (addTopInstanceErrs tidy_env) (groupInsts no_insts)        `thenNF_Tc_`
1893     mapNF_Tc (addTopIPErrs tidy_env)       (groupInsts bad_ips)         `thenNF_Tc_`
1894     mapNF_Tc (addAmbigErr tidy_env)        ambigs                       `thenNF_Tc_`
1895     returnNF_Tc ()
1896   where
1897     fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1898     (tidy_env, tidy_dicts) = tidyInsts dicts
1899     (bad_ips, non_ips)     = partition is_ip tidy_dicts
1900     (no_insts, ambigs)     = partition no_inst non_ips
1901     is_ip d   = any isIPPred (predsOfInst d)
1902     no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
1903
1904 plural [x] = empty
1905 plural xs  = char 's'
1906
1907 addTopIPErrs tidy_env tidy_dicts
1908   = addInstErrTcM (instLoc (head tidy_dicts))
1909         (tidy_env,
1910          ptext SLIT("Unbound implicit parameter") <> plural tidy_dicts <+> pprInsts tidy_dicts)
1911
1912 -- Used for top-level irreducibles
1913 addTopInstanceErrs tidy_env tidy_dicts
1914   = addInstErrTcM (instLoc (head tidy_dicts))
1915         (tidy_env,
1916          ptext SLIT("No instance") <> plural tidy_dicts <+>
1917                 ptext SLIT("for") <+> pprInsts tidy_dicts)
1918
1919 addAmbigErrs dicts
1920   = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1921   where
1922     (tidy_env, tidy_dicts) = tidyInsts dicts
1923
1924 addAmbigErr tidy_env tidy_dict
1925   = addInstErrTcM (instLoc tidy_dict)
1926         (tidy_env,
1927          sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1928               nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1929   where
1930     ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1931
1932 warnDefault dicts default_ty
1933   = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
1934     tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1935   where
1936         -- Tidy them first
1937     (_, tidy_dicts) = tidyInsts dicts
1938     get_loc i = case instLoc i of { (_,loc,_) -> loc }
1939     warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1940                                 quotes (ppr default_ty),
1941                       pprInstsInFull tidy_dicts]
1942
1943 complainCheck doc givens irreds
1944   = mapNF_Tc zonkInst given_dicts_and_ips                         `thenNF_Tc` \ givens' ->
1945     mapNF_Tc (addNoInstanceErrs doc givens') (groupInsts irreds)  `thenNF_Tc_`
1946     returnNF_Tc ()
1947   where
1948     given_dicts_and_ips = filter (not . isMethod) givens
1949         -- Filter out methods, which are only added to
1950         -- the given set as an optimisation
1951
1952 addNoInstanceErrs what_doc givens dicts
1953   = getDOptsTc          `thenNF_Tc` \ dflags ->
1954     tcGetInstEnv        `thenNF_Tc` \ inst_env ->
1955     let
1956         (tidy_env1, tidy_givens) = tidyInsts givens
1957         (tidy_env2, tidy_dicts)  = tidyMoreInsts tidy_env1 dicts
1958
1959         doc = vcat [sep [herald <+> pprInsts tidy_dicts,
1960                          nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1961                     ambig_doc,
1962                     ptext SLIT("Probable fix:"),
1963                     nest 4 fix1,
1964                     nest 4 fix2]
1965
1966         herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1967         unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1968                     | otherwise     = empty
1969
1970                 -- The error message when we don't find a suitable instance
1971                 -- is complicated by the fact that sometimes this is because
1972                 -- there is no instance, and sometimes it's because there are
1973                 -- too many instances (overlap).  See the comments in TcEnv.lhs
1974                 -- with the InstEnv stuff.
1975
1976         ambig_doc
1977             | not ambig_overlap = empty
1978             | otherwise
1979             = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1980                     nest 4 (ptext SLIT("depends on the instantiation of") <+>
1981                             quotes (pprWithCommas ppr (varSetElems (tyVarsOfInsts tidy_dicts))))]
1982
1983         fix1 = sep [ptext SLIT("Add") <+> pprInsts tidy_dicts,
1984                     ptext SLIT("to the") <+> what_doc]
1985
1986         fix2 | null instance_dicts
1987              = empty
1988              | otherwise
1989              = ptext SLIT("Or add an instance declaration for") <+> pprInsts instance_dicts
1990
1991         instance_dicts = [d | d <- tidy_dicts, isClassDict d, not (isTyVarDict d)]
1992                 -- Insts for which it is worth suggesting an adding an instance declaration
1993                 -- Exclude implicit parameters, and tyvar dicts
1994
1995             -- Checks for the ambiguous case when we have overlapping instances
1996         ambig_overlap = any ambig_overlap1 dicts
1997         ambig_overlap1 dict
1998                 | isClassDict dict
1999                 = case lookupInstEnv dflags inst_env clas tys of
2000                             NoMatch ambig -> ambig
2001                             other         -> False
2002                 | otherwise = False
2003                 where
2004                   (clas,tys) = getDictClassTys dict
2005     in
2006     addInstErrTcM (instLoc (head dicts)) (tidy_env2, doc)
2007
2008 -- Used for the ...Thetas variants; all top level
2009 noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
2010
2011 badDerivedPred pred
2012   = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
2013           ptext SLIT("type variables that are not data type parameters"),
2014           nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
2015
2016 reduceDepthErr n stack
2017   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
2018           ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
2019           nest 4 (pprInstsInFull stack)]
2020
2021 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
2022
2023 -----------------------------------------------
2024 addCantGenErr inst
2025   = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
2026                    nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
2027 \end{code}