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