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