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