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
  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 = predsOfInsts (keysFM avails)
 972                 -- Avails has all the superclasses etc (good)
 973                 -- It also has all the intermediates of the deduction (good)
 974                 -- It does not have duplicates (good)
 975                 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
 976                 --    so that improve will see them separate
 977         eqns  = improve (classInstEnv inst_env) preds
 978      in
 979      if null eqns then
 980         returnTc True
 981      else
 982         traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns))    `thenNF_Tc_`
 983         mapTc_ unify eqns       `thenTc_`
 984         returnTc False
 985   where
 986     unify (qtvs, t1, t2) = tcInstTyVars (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
 987                            unifyTauTy (substTy tenv t1) (substTy tenv t2)
 988     ppr_eqn (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) <+>
 989                              ppr t1 <+> equals <+> ppr t2
 990 \end{code}
 991
 992 The main context-reduction function is @reduce@.  Here's its game plan.
 993
 994 \begin{code}
 995 reduceList :: (Int,[Inst])              -- Stack (for err msgs)
 996                                         -- along with its depth
 997            -> (Inst -> WhatToDo)
 998            -> [Inst]
 999            -> RedState
1000            -> TcM RedState
1001 \end{code}
1002
1003 @reduce@ is passed
1004      try_me:    given an inst, this function returns
1005                   Reduce       reduce this
1006                   DontReduce   return this in "irreds"
1007                   Free         return this in "frees"
1008
1009      wanteds:   The list of insts to reduce
1010      state:     An accumulating parameter of type RedState
1011                 that contains the state of the algorithm
1012
1013   It returns a RedState.
1014
1015 The (n,stack) pair is just used for error reporting.
1016 n is always the depth of the stack.
1017 The stack is the stack of Insts being reduced: to produce X
1018 I had to produce Y, to produce Y I had to produce Z, and so on.
1019
1020 \begin{code}
1021 reduceList (n,stack) try_me wanteds state
1022   | n > opt_MaxContextReductionDepth
1023   = failWithTc (reduceDepthErr n stack)
1024
1025   | otherwise
1026   =
1027 #ifdef DEBUG
1028    (if n > 8 then
1029         pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
1030     else (\x->x))
1031 #endif
1032     go wanteds state
1033   where
1034     go []     state = returnTc state
1035     go (w:ws) state = reduce (n+1, w:stack) try_me w state      `thenTc` \ state' ->
1036                       go ws state'
1037
1038     -- Base case: we're done!
1039 reduce stack try_me wanted state
1040     -- It's the same as an existing inst, or a superclass thereof
1041   | isAvailable state wanted
1042   = returnTc state
1043
1044   | otherwise
1045   = case try_me wanted of {
1046
1047       DontReduce want_scs -> addIrred want_scs state wanted
1048
1049     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
1050                                      -- First, see if the inst can be reduced to a constant in one step
1051         try_simple (addIrred AddSCs)    -- Assume want superclasses
1052
1053     ; Free ->   -- It's free so just chuck it upstairs
1054                 -- First, see if the inst can be reduced to a constant in one step
1055         try_simple addFree
1056
1057     ; ReduceMe ->               -- It should be reduced
1058         lookupInst wanted             `thenNF_Tc` \ lookup_result ->
1059         case lookup_result of
1060             GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' ->
1061                                     addWanted state' wanted rhs wanteds'
1062             SimpleInst rhs       -> addWanted state wanted rhs []
1063
1064             NoInstance ->    -- No such instance!
1065                              -- Add it and its superclasses
1066                              addIrred AddSCs state wanted
1067
1068     }
1069   where
1070     try_simple do_this_otherwise
1071       = lookupInst wanted         `thenNF_Tc` \ lookup_result ->
1072         case lookup_result of
1073             SimpleInst rhs -> addWanted state wanted rhs []
1074             other          -> do_this_otherwise state wanted
1075 \end{code}
1076
1077
1078 \begin{code}
1079 isAvailable :: RedState -> Inst -> Bool
1080 isAvailable (avails, _) wanted = wanted `elemFM` avails
1081         -- NB: the Ord instance of Inst compares by the class/type info
1082         -- *not* by unique.  So
1083         --      d1::C Int ==  d2::C Int
1084
1085 -------------------------
1086 addFree :: RedState -> Inst -> NF_TcM RedState
1087         -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1088         -- to avails, so that any other equal Insts will be commoned up right
1089         -- here rather than also being tossed upstairs.  This is really just
1090         -- an optimisation, and perhaps it is more trouble that it is worth,
1091         -- as the following comments show!
1092         --
1093         -- NB1: do *not* add superclasses.  If we have
1094         --      df::Floating a
1095         --      dn::Num a
1096         -- but a is not bound here, then we *don't* want to derive
1097         -- dn from df here lest we lose sharing.
1098         --
1099         -- NB2: do *not* add the Inst to avails at all if it's a method.
1100         -- The following situation shows why this is bad:
1101         --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1102         -- From an application (truncate f i) we get
1103         --      t1 = truncate at f
1104         --      t2 = t1 at i
1105         -- If we have also have a second occurrence of truncate, we get
1106         --      t3 = truncate at f
1107         --      t4 = t3 at i
1108         -- When simplifying with i,f free, we might still notice that
1109         --   t1=t3; but alas, the binding for t2 (which mentions t1)
1110         --   will continue to float out!
1111         -- Solution: never put methods in avail till they are captured
1112         -- in which case addFree isn't used
1113         --
1114         -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1115         --      than BoundTo, else we end up with bogus bindings.
1116         --      c.f. instBindingRequired in addWanted
1117 addFree (avails, frees) free
1118   | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1119   | otherwise   = returnNF_Tc (avails,                    free:frees)
1120   where
1121     avail | instBindingRequired free = BoundTo (instToId free)
1122           | otherwise                = NoRhs
1123
1124 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1125 addWanted state@(avails, frees) wanted rhs_expr wanteds
1126 -- Do *not* add superclasses as well.  Here's an example of why not
1127 --      class Eq a => Foo a b
1128 --      instance Eq a => Foo [a] a
1129 -- If we are reducing
1130 --      (Foo [t] t)
1131 -- we'll first deduce that it holds (via the instance decl).  We
1132 -- must not then overwrite the Eq t constraint with a superclass selection!
1133 --      ToDo: this isn't entirely unsatisfactory, because
1134 --            we may also lose some entirely-legitimate sharing this way
1135
1136   = ASSERT( not (isAvailable state wanted) )
1137     returnNF_Tc (addToFM avails wanted avail, frees)
1138   where
1139     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1140           | otherwise                  = ASSERT( null wanteds ) NoRhs
1141
1142 addGiven :: RedState -> Inst -> NF_TcM RedState
1143 addGiven state given = addAvailAndSCs state given (BoundTo (instToId given))
1144
1145 addIrred :: WantSCs -> RedState -> Inst -> NF_TcM RedState
1146 addIrred NoSCs  (avails,frees) irred = returnNF_Tc (addToFM avails irred Irred, frees)
1147 addIrred AddSCs state          irred = addAvailAndSCs state irred Irred
1148
1149 addAvailAndSCs :: RedState -> Inst -> Avail -> NF_TcM RedState
1150 addAvailAndSCs (avails, frees) wanted avail
1151   = add_avail_and_scs avails wanted avail       `thenNF_Tc` \ avails' ->
1152     returnNF_Tc (avails', frees)
1153
1154 ---------------------
1155 add_avail_and_scs :: Avails -> Inst -> Avail -> NF_TcM Avails
1156 add_avail_and_scs avails wanted avail
1157   = add_scs (addToFM avails wanted avail) wanted
1158
1159 add_scs :: Avails -> Inst -> NF_TcM Avails
1160         -- Add all the superclasses of the Inst to Avails
1161         -- Invariant: the Inst is already in Avails.
1162
1163 add_scs avails dict
1164   | not (isClassDict dict)
1165   = returnNF_Tc avails
1166
1167   | otherwise   -- It is a dictionary
1168   = newDictsFromOld dict sc_theta'      `thenNF_Tc` \ sc_dicts ->
1169     foldlNF_Tc add_sc avails (zipEqual "add_scs" sc_dicts sc_sels)
1170   where
1171     (clas, tys) = getDictClassTys dict
1172     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1173     sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
1174
1175     add_sc avails (sc_dict, sc_sel)     -- Add it, and its superclasses
1176       = case lookupFM avails sc_dict of
1177           Just (BoundTo _) -> returnNF_Tc avails        -- See Note [SUPER] below
1178           other            -> add_avail_and_scs avails sc_dict avail
1179       where
1180         sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1181         avail      = Rhs sc_sel_rhs [dict]
1182 \end{code}
1183
1184 Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
1185 and want to deduce (d2:C [a]) where
1186
1187         class Ord a => C a where
1188         instance Ord a => C [a] where ...
1189
1190 Then we'll use the instance decl to deduce C [a] and then add the
1191 superclasses of C [a] to avails.  But we must not overwrite the binding
1192 for d1:Ord a (which is given) with a superclass selection or we'll just
1193 build a loop!  Hence looking for BoundTo.  Crudely, BoundTo is cheaper
1194 than a selection.
1195
1196
1197 %************************************************************************
1198 %*                                                                      *
1199 \section{tcSimplifyTop: defaulting}
1200 %*                                                                      *
1201 %************************************************************************
1202
1203
1204 If a dictionary constrains a type variable which is
1205         * not mentioned in the environment
1206         * and not mentioned in the type of the expression
1207 then it is ambiguous. No further information will arise to instantiate
1208 the type variable; nor will it be generalised and turned into an extra
1209 parameter to a function.
1210
1211 It is an error for this to occur, except that Haskell provided for
1212 certain rules to be applied in the special case of numeric types.
1213 Specifically, if
1214         * at least one of its classes is a numeric class, and
1215         * all of its classes are numeric or standard
1216 then the type variable can be defaulted to the first type in the
1217 default-type list which is an instance of all the offending classes.
1218
1219 So here is the function which does the work.  It takes the ambiguous
1220 dictionaries and either resolves them (producing bindings) or
1221 complains.  It works by splitting the dictionary list by type
1222 variable, and using @disambigOne@ to do the real business.
1223
1224 @tcSimplifyTop@ is called once per module to simplify all the constant
1225 and ambiguous Insts.
1226
1227 We need to be careful of one case.  Suppose we have
1228
1229         instance Num a => Num (Foo a b) where ...
1230
1231 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)).  Then it'll simplify
1232 to (Num x), and default x to Int.  But what about y??
1233
1234 It's OK: the final zonking stage should zap y to (), which is fine.
1235
1236
1237 \begin{code}
1238 tcSimplifyTop :: LIE -> TcM TcDictBinds
1239 tcSimplifyTop wanted_lie
1240   = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1241     ASSERT( null frees )
1242
1243     let
1244                 -- All the non-std ones are definite errors
1245         (stds, non_stds) = partition isStdClassTyVarDict irreds
1246
1247                 -- Group by type variable
1248         std_groups = equivClasses cmp_by_tyvar stds
1249
1250                 -- Pick the ones which its worth trying to disambiguate
1251         (std_oks, std_bads) = partition worth_a_try std_groups
1252
1253                 -- Have a try at disambiguation
1254                 -- if the type variable isn't bound
1255                 -- up with one of the non-standard classes
1256         worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1257         non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
1258
1259                 -- Collect together all the bad guys
1260         bad_guys = non_stds ++ concat std_bads
1261     in
1262         -- Disambiguate the ones that look feasible
1263     mapTc disambigGroup std_oks         `thenTc` \ binds_ambig ->
1264
1265         -- And complain about the ones that don't
1266         -- This group includes both non-existent instances
1267         --      e.g. Num (IO a) and Eq (Int -> Int)
1268         -- and ambiguous dictionaries
1269         --      e.g. Num a
1270     addTopAmbigErrs bad_guys            `thenNF_Tc_`
1271
1272     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1273   where
1274     wanteds     = lieToList wanted_lie
1275     try_me inst = ReduceMe
1276
1277     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1278
1279 get_tv d   = case getDictClassTys d of
1280                    (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
1281 get_clas d = case getDictClassTys d of
1282                    (clas, [ty]) -> clas
1283 \end{code}
1284
1285 @disambigOne@ assumes that its arguments dictionaries constrain all
1286 the same type variable.
1287
1288 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1289 @()@ instead of @Int@.  I reckon this is the Right Thing to do since
1290 the most common use of defaulting is code like:
1291 \begin{verbatim}
1292         _ccall_ foo     `seqPrimIO` bar
1293 \end{verbatim}
1294 Since we're not using the result of @foo@, the result if (presumably)
1295 @void@.
1296
1297 \begin{code}
1298 disambigGroup :: [Inst] -- All standard classes of form (C a)
1299               -> TcM TcDictBinds
1300
1301 disambigGroup dicts
1302   |   any isNumericClass classes        -- Guaranteed all standard classes
1303           -- see comment at the end of function for reasons as to
1304           -- why the defaulting mechanism doesn't apply to groups that
1305           -- include CCallable or CReturnable dicts.
1306    && not (any isCcallishClass classes)
1307   =     -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1308         -- SO, TRY DEFAULT TYPES IN ORDER
1309
1310         -- Failure here is caused by there being no type in the
1311         -- default list which can satisfy all the ambiguous classes.
1312         -- For example, if Real a is reqd, but the only type in the
1313         -- default list is Int.
1314     tcGetDefaultTys                     `thenNF_Tc` \ default_tys ->
1315     let
1316       try_default []    -- No defaults work, so fail
1317         = failTc
1318
1319       try_default (default_ty : default_tys)
1320         = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
1321                                                 -- default_tys instead
1322           tcSimplifyCheckThetas [] theta        `thenTc` \ _ ->
1323           returnTc default_ty
1324         where
1325           theta = [mkClassPred clas [default_ty] | clas <- classes]
1326     in
1327         -- See if any default works, and if so bind the type variable to it
1328         -- If not, add an AmbigErr
1329     recoverTc (addAmbigErrs dicts                       `thenNF_Tc_`
1330                returnTc EmptyMonoBinds) $
1331
1332     try_default default_tys                     `thenTc` \ chosen_default_ty ->
1333
1334         -- Bind the type variable and reduce the context, for real this time
1335     unifyTauTy chosen_default_ty (mkTyVarTy tyvar)      `thenTc_`
1336     simpleReduceLoop (text "disambig" <+> ppr dicts)
1337                      try_me dicts                       `thenTc` \ (frees, binds, ambigs) ->
1338     WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1339     warnDefault dicts chosen_default_ty                 `thenTc_`
1340     returnTc binds
1341
1342   | all isCreturnableClass classes
1343   =     -- Default CCall stuff to (); we don't even both to check that () is an
1344         -- instance of CReturnable, because we know it is.
1345     unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
1346     returnTc EmptyMonoBinds
1347
1348   | otherwise -- No defaults
1349   = addAmbigErrs dicts  `thenNF_Tc_`
1350     returnTc EmptyMonoBinds
1351
1352   where
1353     try_me inst = ReduceMe                      -- This reduce should not fail
1354     tyvar       = get_tv (head dicts)           -- Should be non-empty
1355     classes     = map get_clas dicts
1356 \end{code}
1357
1358 [Aside - why the defaulting mechanism is turned off when
1359  dealing with arguments and results to ccalls.
1360
1361 When typechecking _ccall_s, TcExpr ensures that the external
1362 function is only passed arguments (and in the other direction,
1363 results) of a restricted set of 'native' types. This is
1364 implemented via the help of the pseudo-type classes,
1365 @CReturnable@ (CR) and @CCallable@ (CC.)
1366
1367 The interaction between the defaulting mechanism for numeric
1368 values and CC & CR can be a bit puzzling to the user at times.
1369 For example,
1370
1371     x <- _ccall_ f
1372     if (x /= 0) then
1373        _ccall_ g x
1374      else
1375        return ()
1376
1377 What type has 'x' got here? That depends on the default list
1378 in operation, if it is equal to Haskell 98's default-default
1379 of (Integer, Double), 'x' has type Double, since Integer
1380 is not an instance of CR. If the default list is equal to
1381 Haskell 1.4's default-default of (Int, Double), 'x' has type
1382 Int.
1383
1384 To try to minimise the potential for surprises here, the
1385 defaulting mechanism is turned off in the presence of
1386 CCallable and CReturnable.
1387
1388 ]
1389
1390
1391 %************************************************************************
1392 %*                                                                      *
1393 \subsection[simple]{@Simple@ versions}
1394 %*                                                                      *
1395 %************************************************************************
1396
1397 Much simpler versions when there are no bindings to make!
1398
1399 @tcSimplifyThetas@ simplifies class-type constraints formed by
1400 @deriving@ declarations and when specialising instances.  We are
1401 only interested in the simplified bunch of class/type constraints.
1402
1403 It simplifies to constraints of the form (C a b c) where
1404 a,b,c are type variables.  This is required for the context of
1405 instance declarations.
1406
1407 \begin{code}
1408 tcSimplifyThetas :: ThetaType           -- Wanted
1409                  -> TcM ThetaType               -- Needed
1410
1411 tcSimplifyThetas wanteds
1412   = doptsTc Opt_GlasgowExts             `thenNF_Tc` \ glaExts ->
1413     reduceSimple [] wanteds             `thenNF_Tc` \ irreds ->
1414     let
1415         -- For multi-param Haskell, check that the returned dictionaries
1416         -- don't have any of the form (C Int Bool) for which
1417         -- we expect an instance here
1418         -- For Haskell 98, check that all the constraints are of the form C a,
1419         -- where a is a type variable
1420         bad_guys | glaExts   = [pred | pred <- irreds,
1421                                        isEmptyVarSet (tyVarsOfPred pred)]
1422                  | otherwise = [pred | pred <- irreds,
1423                                        not (isTyVarClassPred pred)]
1424     in
1425     if null bad_guys then
1426         returnTc irreds
1427     else
1428        mapNF_Tc addNoInstErr bad_guys           `thenNF_Tc_`
1429        failTc
1430 \end{code}
1431
1432 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1433 used with \tr{default} declarations.  We are only interested in
1434 whether it worked or not.
1435
1436 \begin{code}
1437 tcSimplifyCheckThetas :: ThetaType      -- Given
1438                       -> ThetaType      -- Wanted
1439                       -> TcM ()
1440
1441 tcSimplifyCheckThetas givens wanteds
1442   = reduceSimple givens wanteds    `thenNF_Tc`  \ irreds ->
1443     if null irreds then
1444        returnTc ()
1445     else
1446        mapNF_Tc addNoInstErr irreds             `thenNF_Tc_`
1447        failTc
1448 \end{code}
1449
1450
1451 \begin{code}
1452 type AvailsSimple = FiniteMap PredType Bool
1453                     -- True  => irreducible
1454                     -- False => given, or can be derived from a given or from an irreducible
1455
1456 reduceSimple :: ThetaType                       -- Given
1457              -> ThetaType                       -- Wanted
1458              -> NF_TcM ThetaType                -- Irreducible
1459
1460 reduceSimple givens wanteds
1461   = reduce_simple (0,[]) givens_fm wanteds      `thenNF_Tc` \ givens_fm' ->
1462     returnNF_Tc [pred | (pred,True) <- fmToList givens_fm']
1463   where
1464     givens_fm     = foldl addNonIrred emptyFM givens
1465
1466 reduce_simple :: (Int,ThetaType)                -- Stack
1467               -> AvailsSimple
1468               -> ThetaType
1469               -> NF_TcM AvailsSimple
1470
1471 reduce_simple (n,stack) avails wanteds
1472   = go avails wanteds
1473   where
1474     go avails []     = returnNF_Tc avails
1475     go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w        `thenNF_Tc` \ avails' ->
1476                        go avails' ws
1477
1478 reduce_simple_help stack givens wanted
1479   | wanted `elemFM` givens
1480   = returnNF_Tc givens
1481
1482   | Just (clas, tys) <- getClassPredTys_maybe wanted
1483   = lookupSimpleInst clas tys   `thenNF_Tc` \ maybe_theta ->
1484     case maybe_theta of
1485       Nothing ->    returnNF_Tc (addSimpleIrred givens wanted)
1486       Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1487
1488   | otherwise
1489   = returnNF_Tc (addSimpleIrred givens wanted)
1490
1491 addSimpleIrred :: AvailsSimple -> PredType -> AvailsSimple
1492 addSimpleIrred givens pred
1493   = addSCs (addToFM givens pred True) pred
1494
1495 addNonIrred :: AvailsSimple -> PredType -> AvailsSimple
1496 addNonIrred givens pred
1497   = addSCs (addToFM givens pred False) pred
1498
1499 addSCs givens pred
1500   | not (isClassPred pred) = givens
1501   | otherwise              = foldl add givens sc_theta
1502  where
1503    Just (clas,tys) = getClassPredTys_maybe pred
1504    (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1505    sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1506
1507    add givens ct
1508      = case lookupFM givens ct of
1509        Nothing    -> -- Add it and its superclasses
1510                      addSCs (addToFM givens ct False) ct
1511
1512        Just True  -> -- Set its flag to False; superclasses already done
1513                      addToFM givens ct False
1514
1515        Just False -> -- Already done
1516                      givens
1517
1518 \end{code}
1519
1520
1521 %************************************************************************
1522 %*                                                                      *
1523 \section{Errors and contexts}
1524 %*                                                                      *
1525 %************************************************************************
1526
1527 ToDo: for these error messages, should we note the location as coming
1528 from the insts, or just whatever seems to be around in the monad just
1529 now?
1530
1531 \begin{code}
1532 addTopAmbigErrs dicts
1533   = mapNF_Tc complain tidy_dicts
1534   where
1535     fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1536     (tidy_env, tidy_dicts) = tidyInsts dicts
1537     complain d | any isIPPred (predsOfInst d)         = addTopIPErr tidy_env d
1538                | not (isTyVarDict d) ||
1539                  tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
1540                | otherwise                            = addAmbigErr tidy_env d
1541
1542 addTopIPErr tidy_env tidy_dict
1543   = addInstErrTcM (instLoc tidy_dict)
1544         (tidy_env,
1545          ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
1546
1547 -- Used for top-level irreducibles
1548 addTopInstanceErr tidy_env tidy_dict
1549   = addInstErrTcM (instLoc tidy_dict)
1550         (tidy_env,
1551          ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
1552
1553 addAmbigErrs dicts
1554   = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1555   where
1556     (tidy_env, tidy_dicts) = tidyInsts dicts
1557
1558 addAmbigErr tidy_env tidy_dict
1559   = addInstErrTcM (instLoc tidy_dict)
1560         (tidy_env,
1561          sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1562               nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1563   where
1564     ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1565
1566 warnDefault dicts default_ty
1567   = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
1568     tcAddSrcLoc (get_loc (head dicts)) (warnTc warn_flag warn_msg)
1569   where
1570         -- Tidy them first
1571     (_, tidy_dicts) = tidyInsts dicts
1572     get_loc i = case instLoc i of { (_,loc,_) -> loc }
1573     warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
1574                                 quotes (ppr default_ty),
1575                       pprInstsInFull tidy_dicts]
1576
1577 -- The error message when we don't find a suitable instance
1578 -- is complicated by the fact that sometimes this is because
1579 -- there is no instance, and sometimes it's because there are
1580 -- too many instances (overlap).  See the comments in TcEnv.lhs
1581 -- with the InstEnv stuff.
1582 addNoInstanceErr what_doc givens dict
1583   = tcGetInstEnv        `thenNF_Tc` \ inst_env ->
1584     let
1585         doc = vcat [sep [herald <+> quotes (pprInst tidy_dict),
1586                          nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1587                     ambig_doc,
1588                     ptext SLIT("Probable fix:"),
1589                     nest 4 fix1,
1590                     nest 4 fix2]
1591
1592         herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1593         unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1594                     | otherwise     = empty
1595
1596         ambig_doc
1597             | not ambig_overlap = empty
1598             | otherwise
1599             = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1600                     nest 4 (ptext SLIT("depends on the instantiation of") <+>
1601                             quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
1602
1603         fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
1604                     ptext SLIT("to the") <+> what_doc]
1605
1606         fix2 | isTyVarDict dict || ambig_overlap
1607              = empty
1608              | otherwise
1609              = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
1610
1611         (tidy_env, tidy_dict:tidy_givens) = tidyInsts (dict:givens)
1612
1613             -- Checks for the ambiguous case when we have overlapping instances
1614         ambig_overlap | isClassDict dict
1615                       = case lookupInstEnv inst_env clas tys of
1616                             NoMatch ambig -> ambig
1617                             other         -> False
1618                       | otherwise = False
1619                       where
1620                         (clas,tys) = getDictClassTys dict
1621     in
1622     addInstErrTcM (instLoc dict) (tidy_env, doc)
1623
1624 -- Used for the ...Thetas variants; all top level
1625 addNoInstErr pred
1626   = addErrTc (ptext SLIT("No instance for") <+> quotes (ppr pred))
1627
1628 reduceDepthErr n stack
1629   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1630           ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1631           nest 4 (pprInstsInFull stack)]
1632
1633 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1634
1635 -----------------------------------------------
1636 addCantGenErr inst
1637   = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1638                    nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
1639 \end{code}