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