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