ghc/compiler/typecheck/TcSimplify.lhs

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