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 AddToIrreds            -- 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 AddToIrreds
 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 AddToIrreds
 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 \begin{code}
 618 tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
 619 tcSimplifyToDicts wanted_lie
 620   = simpleReduceLoop doc try_me wanteds         `thenTc` \ (frees, binds, irreds) ->
 621         -- Since try_me doesn't look at types, we don't need to
 622         -- do any zonking, so it's safe to call reduceContext directly
 623     ASSERT( null frees )
 624     returnTc (irreds, binds)
 625
 626   where
 627     doc = text "tcSimplifyToDicts"
 628     wanteds = lieToList wanted_lie
 629
 630         -- Reduce methods and lits only; stop as soon as we get a dictionary
 631     try_me inst | isDict inst = DontReduce
 632                 | otherwise   = ReduceMe AddToIrreds
 633 \end{code}
 634
 635
 636 %************************************************************************
 637 %*                                                                      *
 638 \subsection{Filtering at a dynamic binding}
 639 %*                                                                      *
 640 %************************************************************************
 641
 642 When we have
 643         let ?x = R in B
 644
 645 we must discharge all the ?x constraints from B.  We also do an improvement
 646 step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.  No need to iterate, though.
 647
 648 \begin{code}
 649 tcSimplifyIPs :: [Name]         -- The implicit parameters bound here
 650               -> LIE
 651               -> TcM (LIE, TcDictBinds)
 652 tcSimplifyIPs ip_names wanted_lie
 653   = simpleReduceLoop doc try_me wanteds `thenTc` \ (frees, binds, irreds) ->
 654         -- The irreducible ones should be a subset of the implicit
 655         -- parameters we provided
 656     ASSERT( all here_ip irreds )
 657     returnTc (mkLIE frees, binds)
 658
 659   where
 660     doc     = text "tcSimplifyIPs" <+> ppr ip_names
 661     wanteds = lieToList wanted_lie
 662     ip_set  = mkNameSet ip_names
 663     here_ip ip = isDict ip && ip `instMentionsIPs` ip_set
 664
 665         -- Simplify any methods that mention the implicit parameter
 666     try_me inst | inst `instMentionsIPs` ip_set = ReduceMe AddToIrreds
 667                 | otherwise                     = Free
 668 \end{code}
 669
 670
 671 %************************************************************************
 672 %*                                                                      *
 673 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
 674 %*                                                                      *
 675 %************************************************************************
 676
 677 When doing a binding group, we may have @Insts@ of local functions.
 678 For example, we might have...
 679 \begin{verbatim}
 680 let f x = x + 1     -- orig local function (overloaded)
 681     f.1 = f Int     -- two instances of f
 682     f.2 = f Float
 683  in
 684     (f.1 5, f.2 6.7)
 685 \end{verbatim}
 686 The point is: we must drop the bindings for @f.1@ and @f.2@ here,
 687 where @f@ is in scope; those @Insts@ must certainly not be passed
 688 upwards towards the top-level.  If the @Insts@ were binding-ified up
 689 there, they would have unresolvable references to @f@.
 690
 691 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
 692 For each method @Inst@ in the @init_lie@ that mentions one of the
 693 @Ids@, we create a binding.  We return the remaining @Insts@ (in an
 694 @LIE@), as well as the @HsBinds@ generated.
 695
 696 \begin{code}
 697 bindInstsOfLocalFuns :: LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
 698
 699 bindInstsOfLocalFuns init_lie local_ids
 700   | null overloaded_ids
 701         -- Common case
 702   = returnTc (init_lie, EmptyMonoBinds)
 703
 704   | otherwise
 705   = simpleReduceLoop doc try_me wanteds         `thenTc` \ (frees, binds, irreds) ->
 706     ASSERT( null irreds )
 707     returnTc (mkLIE frees, binds)
 708   where
 709     doc              = text "bindInsts" <+> ppr local_ids
 710     wanteds          = lieToList init_lie
 711     overloaded_ids   = filter is_overloaded local_ids
 712     is_overloaded id = case splitSigmaTy (idType id) of
 713                           (_, theta, _) -> not (null theta)
 714
 715     overloaded_set = mkVarSet overloaded_ids    -- There can occasionally be a lot of them
 716                                                 -- so it's worth building a set, so that
 717                                                 -- lookup (in isMethodFor) is faster
 718
 719     try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
 720                 | otherwise                       = Free
 721 \end{code}
 722
 723
 724 %************************************************************************
 725 %*                                                                      *
 726 \subsection{Data types for the reduction mechanism}
 727 %*                                                                      *
 728 %************************************************************************
 729
 730 The main control over context reduction is here
 731
 732 \begin{code}
 733 data WhatToDo
 734  = ReduceMe               -- Try to reduce this
 735         NoInstanceAction  -- What to do if there's no such instance
 736
 737  | DontReduce                   -- Return as irreducible
 738
 739  | DontReduceUnlessConstant     -- Return as irreducible unless it can
 740                                 -- be reduced to a constant in one step
 741
 742  | Free                   -- Return as free
 743
 744 data NoInstanceAction
 745   = Stop                -- Fail; no error message
 746                         -- (Only used when tautology checking.)
 747
 748   | AddToIrreds         -- Just add the inst to the irreductible ones; don't
 749                         -- produce an error message of any kind.
 750                         -- It might be quite legitimate such as (Eq a)!
 751 \end{code}
 752
 753
 754
 755 \begin{code}
 756 type RedState = (Avails,        -- What's available
 757                  [Inst])        -- Insts for which try_me returned Free
 758
 759 type Avails = FiniteMap Inst Avail
 760
 761 data Avail
 762   = Irred               -- Used for irreducible dictionaries,
 763                         -- which are going to be lambda bound
 764
 765   | BoundTo TcId        -- Used for dictionaries for which we have a binding
 766                         -- e.g. those "given" in a signature
 767
 768   | NoRhs               -- Used for Insts like (CCallable f)
 769                         -- where no witness is required.
 770
 771   | Rhs                 -- Used when there is a RHS
 772         TcExpr          -- The RHS
 773         [Inst]          -- Insts free in the RHS; we need these too
 774
 775 pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
 776                         | (inst,avail) <- fmToList avails ]
 777
 778 instance Outputable Avail where
 779     ppr = pprAvail
 780
 781 pprAvail NoRhs        = text "<no rhs>"
 782 pprAvail Irred        = text "Irred"
 783 pprAvail (BoundTo x)  = text "Bound to" <+> ppr x
 784 pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
 785 \end{code}
 786
 787 Extracting the bindings from a bunch of Avails.
 788 The bindings do *not* come back sorted in dependency order.
 789 We assume that they'll be wrapped in a big Rec, so that the
 790 dependency analyser can sort them out later
 791
 792 The loop startes
 793 \begin{code}
 794 bindsAndIrreds :: Avails
 795                -> [Inst]                -- Wanted
 796                -> (TcDictBinds,         -- Bindings
 797                    [Inst])              -- Irreducible ones
 798
 799 bindsAndIrreds avails wanteds
 800   = go avails EmptyMonoBinds [] wanteds
 801   where
 802     go avails binds irreds [] = (binds, irreds)
 803
 804     go avails binds irreds (w:ws)
 805       = case lookupFM avails w of
 806           Nothing    -> -- Free guys come out here
 807                         -- (If we didn't do addFree we could use this as the
 808                         --  criterion for free-ness, and pick up the free ones here too)
 809                         go avails binds irreds ws
 810
 811           Just NoRhs -> go avails binds irreds ws
 812
 813           Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
 814
 815           Just (BoundTo id) -> go avails new_binds irreds ws
 816                             where
 817                                 -- For implicit parameters, all occurrences share the same
 818                                 -- Id, so there is no need for synonym bindings
 819                                new_binds | new_id == id = binds
 820                                          | otherwise    = binds `AndMonoBinds` new_bind
 821                                new_bind = VarMonoBind new_id (HsVar id)
 822                                new_id   = instToId w
 823
 824           Just (Rhs rhs ws') -> go avails' (binds `AndMonoBinds` new_bind) irreds (ws' ++ ws)
 825                              where
 826                                 id       = instToId w
 827                                 avails'  = addToFM avails w (BoundTo id)
 828                                 new_bind = VarMonoBind id rhs
 829 \end{code}
 830
 831
 832 %************************************************************************
 833 %*                                                                      *
 834 \subsection[reduce]{@reduce@}
 835 %*                                                                      *
 836 %************************************************************************
 837
 838 When the "what to do" predicate doesn't depend on the quantified type variables,
 839 matters are easier.  We don't need to do any zonking, unless the improvement step
 840 does something, in which case we zonk before iterating.
 841
 842 The "given" set is always empty.
 843
 844 \begin{code}
 845 simpleReduceLoop :: SDoc
 846                  -> (Inst -> WhatToDo)          -- What to do, *not* based on the quantified type variables
 847                  -> [Inst]                      -- Wanted
 848                  -> TcM ([Inst],                -- Free
 849                          TcDictBinds,
 850                          [Inst])                -- Irreducible
 851
 852 simpleReduceLoop doc try_me wanteds
 853   = mapNF_Tc zonkInst wanteds                   `thenNF_Tc` \ wanteds' ->
 854     reduceContext doc try_me [] wanteds'        `thenTc` \ (no_improvement, frees, binds, irreds) ->
 855     if no_improvement then
 856         returnTc (frees, binds, irreds)
 857     else
 858         simpleReduceLoop doc try_me (irreds ++ frees)   `thenTc` \ (frees1, binds1, irreds1) ->
 859         returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
 860 \end{code}
 861
 862
 863
 864 \begin{code}
 865 reduceContext :: SDoc
 866               -> (Inst -> WhatToDo)
 867               -> [Inst]                 -- Given
 868               -> [Inst]                 -- Wanted
 869               -> NF_TcM (Bool,          -- True <=> improve step did no unification
 870                          [Inst],        -- Free
 871                          TcDictBinds,   -- Dictionary bindings
 872                          [Inst])        -- Irreducible
 873
 874 reduceContext doc try_me givens wanteds
 875   =
 876     traceTc (text "reduceContext" <+> (vcat [
 877              text "----------------------",
 878              doc,
 879              text "given" <+> ppr givens,
 880              text "wanted" <+> ppr wanteds,
 881              text "----------------------"
 882              ]))                                        `thenNF_Tc_`
 883
 884         -- Build the Avail mapping from "givens"
 885     foldlNF_Tc addGiven (emptyFM, []) givens            `thenNF_Tc` \ init_state ->
 886
 887         -- Do the real work
 888     reduceList (0,[]) try_me wanteds init_state         `thenNF_Tc` \ state@(avails, frees) ->
 889
 890         -- Do improvement, using everything in avails
 891         -- In particular, avails includes all superclasses of everything
 892     tcImprove avails                                    `thenTc` \ no_improvement ->
 893
 894     traceTc (text "reduceContext end" <+> (vcat [
 895              text "----------------------",
 896              doc,
 897              text "given" <+> ppr givens,
 898              text "wanted" <+> ppr wanteds,
 899              text "----",
 900              text "avails" <+> pprAvails avails,
 901              text "frees" <+> ppr frees,
 902              text "no_improvement =" <+> ppr no_improvement,
 903              text "----------------------"
 904              ]))                                        `thenNF_Tc_`
 905      let
 906         (binds, irreds) = bindsAndIrreds avails wanteds
 907      in
 908      returnTc (no_improvement, frees, binds, irreds)
 909
 910 tcImprove avails
 911  =  tcGetInstEnv                                `thenTc` \ inst_env ->
 912     let
 913         preds = predsOfInsts (keysFM avails)
 914                 -- Avails has all the superclasses etc (good)
 915                 -- It also has all the intermediates of the deduction (good)
 916                 -- It does not have duplicates (good)
 917                 -- NB that (?x::t1) and (?x::t2) will be held separately in avails
 918                 --    so that improve will see them separate
 919         eqns  = improve (classInstEnv inst_env) preds
 920      in
 921      if null eqns then
 922         returnTc True
 923      else
 924         traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns))    `thenNF_Tc_`
 925         mapTc_ unify eqns       `thenTc_`
 926         returnTc False
 927   where
 928     unify (qtvs, t1, t2) = tcInstTyVars (varSetElems qtvs)      `thenNF_Tc` \ (_, _, tenv) ->
 929                            unifyTauTy (substTy tenv t1) (substTy tenv t2)
 930     ppr_eqn (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) <+>
 931                              ppr t1 <+> equals <+> ppr t2
 932 \end{code}
 933
 934 The main context-reduction function is @reduce@.  Here's its game plan.
 935
 936 \begin{code}
 937 reduceList :: (Int,[Inst])              -- Stack (for err msgs)
 938                                         -- along with its depth
 939            -> (Inst -> WhatToDo)
 940            -> [Inst]
 941            -> RedState
 942            -> TcM RedState
 943 \end{code}
 944
 945 @reduce@ is passed
 946      try_me:    given an inst, this function returns
 947                   Reduce       reduce this
 948                   DontReduce   return this in "irreds"
 949                   Free         return this in "frees"
 950
 951      wanteds:   The list of insts to reduce
 952      state:     An accumulating parameter of type RedState
 953                 that contains the state of the algorithm
 954
 955   It returns a RedState.
 956
 957 The (n,stack) pair is just used for error reporting.
 958 n is always the depth of the stack.
 959 The stack is the stack of Insts being reduced: to produce X
 960 I had to produce Y, to produce Y I had to produce Z, and so on.
 961
 962 \begin{code}
 963 reduceList (n,stack) try_me wanteds state
 964   | n > opt_MaxContextReductionDepth
 965   = failWithTc (reduceDepthErr n stack)
 966
 967   | otherwise
 968   =
 969 #ifdef DEBUG
 970    (if n > 8 then
 971         pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
 972     else (\x->x))
 973 #endif
 974     go wanteds state
 975   where
 976     go []     state = returnTc state
 977     go (w:ws) state = reduce (n+1, w:stack) try_me w state      `thenTc` \ state' ->
 978                       go ws state'
 979
 980     -- Base case: we're done!
 981 reduce stack try_me wanted state
 982     -- It's the same as an existing inst, or a superclass thereof
 983   | isAvailable state wanted
 984   = returnTc state
 985
 986   | otherwise
 987   = case try_me wanted of {
 988
 989       DontReduce -> addIrred state wanted
 990
 991     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
 992                                      -- First, see if the inst can be reduced to a constant in one step
 993         try_simple addIrred
 994
 995     ; Free ->   -- It's free so just chuck it upstairs
 996                 -- First, see if the inst can be reduced to a constant in one step
 997         try_simple addFree
 998
 999     ; ReduceMe no_instance_action ->    -- It should be reduced
1000         lookupInst wanted             `thenNF_Tc` \ lookup_result ->
1001         case lookup_result of
1002             GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' ->
1003                                     addWanted state' wanted rhs wanteds'
1004             SimpleInst rhs       -> addWanted state wanted rhs []
1005
1006             NoInstance ->    -- No such instance!
1007                     case no_instance_action of
1008                         Stop        -> failTc
1009                         AddToIrreds -> addIrred state wanted
1010
1011     }
1012   where
1013     try_simple do_this_otherwise
1014       = lookupInst wanted         `thenNF_Tc` \ lookup_result ->
1015         case lookup_result of
1016             SimpleInst rhs -> addWanted state wanted rhs []
1017             other          -> do_this_otherwise state wanted
1018 \end{code}
1019
1020
1021 \begin{code}
1022 isAvailable :: RedState -> Inst -> Bool
1023 isAvailable (avails, _) wanted = wanted `elemFM` avails
1024         -- NB: the Ord instance of Inst compares by the class/type info
1025         -- *not* by unique.  So
1026         --      d1::C Int ==  d2::C Int
1027
1028 -------------------------
1029 addFree :: RedState -> Inst -> NF_TcM RedState
1030         -- When an Inst is tossed upstairs as 'free' we nevertheless add it
1031         -- to avails, so that any other equal Insts will be commoned up right
1032         -- here rather than also being tossed upstairs.  This is really just
1033         -- an optimisation, and perhaps it is more trouble that it is worth,
1034         -- as the following comments show!
1035         --
1036         -- NB1: do *not* add superclasses.  If we have
1037         --      df::Floating a
1038         --      dn::Num a
1039         -- but a is not bound here, then we *don't* want to derive
1040         -- dn from df here lest we lose sharing.
1041         --
1042         -- NB2: do *not* add the Inst to avails at all if it's a method.
1043         -- The following situation shows why this is bad:
1044         --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
1045         -- From an application (truncate f i) we get
1046         --      t1 = truncate at f
1047         --      t2 = t1 at i
1048         -- If we have also have a second occurrence of truncate, we get
1049         --      t3 = truncate at f
1050         --      t4 = t3 at i
1051         -- When simplifying with i,f free, we might still notice that
1052         --   t1=t3; but alas, the binding for t2 (which mentions t1)
1053         --   will continue to float out!
1054         -- Solution: never put methods in avail till they are captured
1055         -- in which case addFree isn't used
1056         --
1057         -- NB3: make sure that CCallable/CReturnable use NoRhs rather
1058         --      than BoundTo, else we end up with bogus bindings.
1059         --      c.f. instBindingRequired in addWanted
1060 addFree (avails, frees) free
1061   | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
1062   | otherwise   = returnNF_Tc (avails,                    free:frees)
1063   where
1064     avail | instBindingRequired free = BoundTo (instToId free)
1065           | otherwise                = NoRhs
1066
1067 addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1068 addWanted state@(avails, frees) wanted rhs_expr wanteds
1069 -- Do *not* add superclasses as well.  Here's an example of why not
1070 --      class Eq a => Foo a b
1071 --      instance Eq a => Foo [a] a
1072 -- If we are reducing
1073 --      (Foo [t] t)
1074 -- we'll first deduce that it holds (via the instance decl).  We
1075 -- must not then overwrite the Eq t constraint with a superclass selection!
1076 --      ToDo: this isn't entirely unsatisfactory, because
1077 --            we may also lose some entirely-legitimate sharing this way
1078
1079   = ASSERT( not (isAvailable state wanted) )
1080     returnNF_Tc (addToFM avails wanted avail, frees)
1081   where
1082     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
1083           | otherwise                  = ASSERT( null wanteds ) NoRhs
1084
1085 addGiven :: RedState -> Inst -> NF_TcM RedState
1086 addGiven state given = add_avail state given (BoundTo (instToId given))
1087
1088 addIrred :: RedState -> Inst -> NF_TcM RedState
1089 addIrred state irred = add_avail state irred Irred
1090
1091 add_avail :: RedState -> Inst -> Avail -> NF_TcM RedState
1092 add_avail (avails, frees) wanted avail
1093   = addAvail avails wanted avail        `thenNF_Tc` \ avails' ->
1094     returnNF_Tc (avails', frees)
1095
1096 ---------------------
1097 addAvail :: Avails -> Inst -> Avail -> NF_TcM Avails
1098 addAvail avails wanted avail
1099   = addSuperClasses (addToFM avails wanted avail) wanted
1100
1101 addSuperClasses :: Avails -> Inst -> NF_TcM Avails
1102         -- Add all the superclasses of the Inst to Avails
1103         -- Invariant: the Inst is already in Avails.
1104
1105 addSuperClasses avails dict
1106   | not (isClassDict dict)
1107   = returnNF_Tc avails
1108
1109   | otherwise   -- It is a dictionary
1110   = newDictsFromOld dict sc_theta'      `thenNF_Tc` \ sc_dicts ->
1111     foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_dicts sc_sels)
1112   where
1113     (clas, tys) = getDictClassTys dict
1114     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
1115     sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
1116
1117     add_sc avails (sc_dict, sc_sel)     -- Add it, and its superclasses
1118       = case lookupFM avails sc_dict of
1119           Just (BoundTo _) -> returnNF_Tc avails        -- See Note [SUPER] below
1120           other            -> addAvail avails sc_dict avail
1121       where
1122         sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
1123         avail      = Rhs sc_sel_rhs [dict]
1124 \end{code}
1125
1126 Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
1127 and want to deduce (d2:C [a]) where
1128
1129         class Ord a => C a where
1130         instance Ord a => C [a] where ...
1131
1132 Then we'll use the instance decl to deduce C [a] and then add the
1133 superclasses of C [a] to avails.  But we must not overwrite the binding
1134 for d1:Ord a (which is given) with a superclass selection or we'll just
1135 build a loop!  Hence looking for BoundTo.  Crudely, BoundTo is cheaper
1136 than a selection.
1137
1138
1139 %************************************************************************
1140 %*                                                                      *
1141 \section{tcSimplifyTop: defaulting}
1142 %*                                                                      *
1143 %************************************************************************
1144
1145
1146 If a dictionary constrains a type variable which is
1147         * not mentioned in the environment
1148         * and not mentioned in the type of the expression
1149 then it is ambiguous. No further information will arise to instantiate
1150 the type variable; nor will it be generalised and turned into an extra
1151 parameter to a function.
1152
1153 It is an error for this to occur, except that Haskell provided for
1154 certain rules to be applied in the special case of numeric types.
1155 Specifically, if
1156         * at least one of its classes is a numeric class, and
1157         * all of its classes are numeric or standard
1158 then the type variable can be defaulted to the first type in the
1159 default-type list which is an instance of all the offending classes.
1160
1161 So here is the function which does the work.  It takes the ambiguous
1162 dictionaries and either resolves them (producing bindings) or
1163 complains.  It works by splitting the dictionary list by type
1164 variable, and using @disambigOne@ to do the real business.
1165
1166 @tcSimplifyTop@ is called once per module to simplify all the constant
1167 and ambiguous Insts.
1168
1169 We need to be careful of one case.  Suppose we have
1170
1171         instance Num a => Num (Foo a b) where ...
1172
1173 and @tcSimplifyTop@ is given a constraint (Num (Foo x y)).  Then it'll simplify
1174 to (Num x), and default x to Int.  But what about y??
1175
1176 It's OK: the final zonking stage should zap y to (), which is fine.
1177
1178
1179 \begin{code}
1180 tcSimplifyTop :: LIE -> TcM TcDictBinds
1181 tcSimplifyTop wanted_lie
1182   = simpleReduceLoop (text "tcSimplTop") try_me wanteds `thenTc` \ (frees, binds, irreds) ->
1183     ASSERT( null frees )
1184
1185     let
1186                 -- All the non-std ones are definite errors
1187         (stds, non_stds) = partition isStdClassTyVarDict irreds
1188
1189                 -- Group by type variable
1190         std_groups = equivClasses cmp_by_tyvar stds
1191
1192                 -- Pick the ones which its worth trying to disambiguate
1193         (std_oks, std_bads) = partition worth_a_try std_groups
1194
1195                 -- Have a try at disambiguation
1196                 -- if the type variable isn't bound
1197                 -- up with one of the non-standard classes
1198         worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1199         non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
1200
1201                 -- Collect together all the bad guys
1202         bad_guys = non_stds ++ concat std_bads
1203     in
1204         -- Disambiguate the ones that look feasible
1205     mapTc disambigGroup std_oks         `thenTc` \ binds_ambig ->
1206
1207         -- And complain about the ones that don't
1208         -- This group includes both non-existent instances
1209         --      e.g. Num (IO a) and Eq (Int -> Int)
1210         -- and ambiguous dictionaries
1211         --      e.g. Num a
1212     addTopAmbigErrs bad_guys            `thenNF_Tc_`
1213
1214     returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1215   where
1216     wanteds     = lieToList wanted_lie
1217     try_me inst = ReduceMe AddToIrreds
1218
1219     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1220
1221 get_tv d   = case getDictClassTys d of
1222                    (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
1223 get_clas d = case getDictClassTys d of
1224                    (clas, [ty]) -> clas
1225 \end{code}
1226
1227 @disambigOne@ assumes that its arguments dictionaries constrain all
1228 the same type variable.
1229
1230 ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
1231 @()@ instead of @Int@.  I reckon this is the Right Thing to do since
1232 the most common use of defaulting is code like:
1233 \begin{verbatim}
1234         _ccall_ foo     `seqPrimIO` bar
1235 \end{verbatim}
1236 Since we're not using the result of @foo@, the result if (presumably)
1237 @void@.
1238
1239 \begin{code}
1240 disambigGroup :: [Inst] -- All standard classes of form (C a)
1241               -> TcM TcDictBinds
1242
1243 disambigGroup dicts
1244   |   any isNumericClass classes        -- Guaranteed all standard classes
1245           -- see comment at the end of function for reasons as to
1246           -- why the defaulting mechanism doesn't apply to groups that
1247           -- include CCallable or CReturnable dicts.
1248    && not (any isCcallishClass classes)
1249   =     -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
1250         -- SO, TRY DEFAULT TYPES IN ORDER
1251
1252         -- Failure here is caused by there being no type in the
1253         -- default list which can satisfy all the ambiguous classes.
1254         -- For example, if Real a is reqd, but the only type in the
1255         -- default list is Int.
1256     tcGetDefaultTys                     `thenNF_Tc` \ default_tys ->
1257     let
1258       try_default []    -- No defaults work, so fail
1259         = failTc
1260
1261       try_default (default_ty : default_tys)
1262         = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
1263                                                 -- default_tys instead
1264           tcSimplifyCheckThetas [] thetas       `thenTc` \ _ ->
1265           returnTc default_ty
1266         where
1267           thetas = classes `zip` repeat [default_ty]
1268     in
1269         -- See if any default works, and if so bind the type variable to it
1270         -- If not, add an AmbigErr
1271     recoverTc (addAmbigErrs dicts                       `thenNF_Tc_`
1272                returnTc EmptyMonoBinds) $
1273
1274     try_default default_tys                     `thenTc` \ chosen_default_ty ->
1275
1276         -- Bind the type variable and reduce the context, for real this time
1277     unifyTauTy chosen_default_ty (mkTyVarTy tyvar)      `thenTc_`
1278     simpleReduceLoop (text "disambig" <+> ppr dicts)
1279                      try_me dicts                       `thenTc` \ (frees, binds, ambigs) ->
1280     WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1281     warnDefault dicts chosen_default_ty                 `thenTc_`
1282     returnTc binds
1283
1284   | all isCreturnableClass classes
1285   =     -- Default CCall stuff to (); we don't even both to check that () is an
1286         -- instance of CReturnable, because we know it is.
1287     unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
1288     returnTc EmptyMonoBinds
1289
1290   | otherwise -- No defaults
1291   = addAmbigErrs dicts  `thenNF_Tc_`
1292     returnTc EmptyMonoBinds
1293
1294   where
1295     try_me inst = ReduceMe AddToIrreds          -- This reduce should not fail
1296     tyvar       = get_tv (head dicts)           -- Should be non-empty
1297     classes     = map get_clas dicts
1298 \end{code}
1299
1300 [Aside - why the defaulting mechanism is turned off when
1301  dealing with arguments and results to ccalls.
1302
1303 When typechecking _ccall_s, TcExpr ensures that the external
1304 function is only passed arguments (and in the other direction,
1305 results) of a restricted set of 'native' types. This is
1306 implemented via the help of the pseudo-type classes,
1307 @CReturnable@ (CR) and @CCallable@ (CC.)
1308
1309 The interaction between the defaulting mechanism for numeric
1310 values and CC & CR can be a bit puzzling to the user at times.
1311 For example,
1312
1313     x <- _ccall_ f
1314     if (x /= 0) then
1315        _ccall_ g x
1316      else
1317        return ()
1318
1319 What type has 'x' got here? That depends on the default list
1320 in operation, if it is equal to Haskell 98's default-default
1321 of (Integer, Double), 'x' has type Double, since Integer
1322 is not an instance of CR. If the default list is equal to
1323 Haskell 1.4's default-default of (Int, Double), 'x' has type
1324 Int.
1325
1326 To try to minimise the potential for surprises here, the
1327 defaulting mechanism is turned off in the presence of
1328 CCallable and CReturnable.
1329
1330 ]
1331
1332
1333 %************************************************************************
1334 %*                                                                      *
1335 \subsection[simple]{@Simple@ versions}
1336 %*                                                                      *
1337 %************************************************************************
1338
1339 Much simpler versions when there are no bindings to make!
1340
1341 @tcSimplifyThetas@ simplifies class-type constraints formed by
1342 @deriving@ declarations and when specialising instances.  We are
1343 only interested in the simplified bunch of class/type constraints.
1344
1345 It simplifies to constraints of the form (C a b c) where
1346 a,b,c are type variables.  This is required for the context of
1347 instance declarations.
1348
1349 \begin{code}
1350 tcSimplifyThetas :: ClassContext                -- Wanted
1351                  -> TcM ClassContext            -- Needed
1352
1353 tcSimplifyThetas wanteds
1354   = doptsTc Opt_GlasgowExts             `thenNF_Tc` \ glaExts ->
1355     reduceSimple [] wanteds             `thenNF_Tc` \ irreds ->
1356     let
1357         -- For multi-param Haskell, check that the returned dictionaries
1358         -- don't have any of the form (C Int Bool) for which
1359         -- we expect an instance here
1360         -- For Haskell 98, check that all the constraints are of the form C a,
1361         -- where a is a type variable
1362         bad_guys | glaExts   = [ct | ct@(clas,tys) <- irreds,
1363                                      isEmptyVarSet (tyVarsOfTypes tys)]
1364                  | otherwise = [ct | ct@(clas,tys) <- irreds,
1365                                      not (all isTyVarTy tys)]
1366     in
1367     if null bad_guys then
1368         returnTc irreds
1369     else
1370        mapNF_Tc addNoInstErr bad_guys           `thenNF_Tc_`
1371        failTc
1372 \end{code}
1373
1374 @tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
1375 used with \tr{default} declarations.  We are only interested in
1376 whether it worked or not.
1377
1378 \begin{code}
1379 tcSimplifyCheckThetas :: ClassContext   -- Given
1380                       -> ClassContext   -- Wanted
1381                       -> TcM ()
1382
1383 tcSimplifyCheckThetas givens wanteds
1384   = reduceSimple givens wanteds    `thenNF_Tc`  \ irreds ->
1385     if null irreds then
1386        returnTc ()
1387     else
1388        mapNF_Tc addNoInstErr irreds             `thenNF_Tc_`
1389        failTc
1390 \end{code}
1391
1392
1393 \begin{code}
1394 type AvailsSimple = FiniteMap (Class,[Type]) Bool
1395                     -- True  => irreducible
1396                     -- False => given, or can be derived from a given or from an irreducible
1397
1398 reduceSimple :: ClassContext                    -- Given
1399              -> ClassContext                    -- Wanted
1400              -> NF_TcM ClassContext             -- Irreducible
1401
1402 reduceSimple givens wanteds
1403   = reduce_simple (0,[]) givens_fm wanteds      `thenNF_Tc` \ givens_fm' ->
1404     returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
1405   where
1406     givens_fm     = foldl addNonIrred emptyFM givens
1407
1408 reduce_simple :: (Int,ClassContext)             -- Stack
1409               -> AvailsSimple
1410               -> ClassContext
1411               -> NF_TcM AvailsSimple
1412
1413 reduce_simple (n,stack) avails wanteds
1414   = go avails wanteds
1415   where
1416     go avails []     = returnNF_Tc avails
1417     go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w        `thenNF_Tc` \ avails' ->
1418                        go avails' ws
1419
1420 reduce_simple_help stack givens wanted@(clas,tys)
1421   | wanted `elemFM` givens
1422   = returnNF_Tc givens
1423
1424   | otherwise
1425   = lookupSimpleInst clas tys   `thenNF_Tc` \ maybe_theta ->
1426
1427     case maybe_theta of
1428       Nothing ->    returnNF_Tc (addSimpleIrred givens wanted)
1429       Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
1430
1431 addSimpleIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
1432 addSimpleIrred givens ct@(clas,tys)
1433   = addSCs (addToFM givens ct True) ct
1434
1435 addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
1436 addNonIrred givens ct@(clas,tys)
1437   = addSCs (addToFM givens ct False) ct
1438
1439 addSCs givens ct@(clas,tys)
1440  = foldl add givens sc_theta
1441  where
1442    (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
1443    sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
1444
1445    add givens ct@(clas, tys)
1446      = case lookupFM givens ct of
1447        Nothing    -> -- Add it and its superclasses
1448                      addSCs (addToFM givens ct False) ct
1449
1450        Just True  -> -- Set its flag to False; superclasses already done
1451                      addToFM givens ct False
1452
1453        Just False -> -- Already done
1454                      givens
1455
1456 \end{code}
1457
1458
1459 %************************************************************************
1460 %*                                                                      *
1461 \section{Errors and contexts}
1462 %*                                                                      *
1463 %************************************************************************
1464
1465 ToDo: for these error messages, should we note the location as coming
1466 from the insts, or just whatever seems to be around in the monad just
1467 now?
1468
1469 \begin{code}
1470 addTopAmbigErrs dicts
1471   = mapNF_Tc complain tidy_dicts
1472   where
1473     fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
1474     (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
1475     complain d | not (null (getIPs d))                = addTopIPErr tidy_env d
1476                | not (isTyVarDict d) ||
1477                  tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
1478                | otherwise                            = addAmbigErr tidy_env d
1479
1480 addTopIPErr tidy_env tidy_dict
1481   = addInstErrTcM (instLoc tidy_dict)
1482         (tidy_env,
1483          ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
1484
1485 -- Used for top-level irreducibles
1486 addTopInstanceErr tidy_env tidy_dict
1487   = addInstErrTcM (instLoc tidy_dict)
1488         (tidy_env,
1489          ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
1490
1491 addAmbigErrs dicts
1492   = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
1493   where
1494     (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
1495
1496 addAmbigErr tidy_env tidy_dict
1497   = addInstErrTcM (instLoc tidy_dict)
1498         (tidy_env,
1499          sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1500               nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1501   where
1502     ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1503
1504 warnDefault dicts default_ty
1505   = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
1506     if warn_flag
1507         then mapNF_Tc warn groups  `thenNF_Tc_`  returnNF_Tc ()
1508         else returnNF_Tc ()
1509
1510   where
1511         -- Tidy them first
1512     (_, tidy_dicts) = mapAccumL tidyInst emptyTidyEnv dicts
1513
1514         -- Group the dictionaries by source location
1515     groups      = equivClasses cmp tidy_dicts
1516     i1 `cmp` i2 = get_loc i1 `compare` get_loc i2
1517     get_loc i   = case instLoc i of { (_,loc,_) -> loc }
1518
1519     warn [dict] = tcAddSrcLoc (get_loc dict) $
1520                   warnTc True (ptext SLIT("Defaulting") <+> quotes (pprInst dict) <+>
1521                                ptext SLIT("to type") <+> quotes (ppr default_ty))
1522
1523     warn dicts  = tcAddSrcLoc (get_loc (head dicts)) $
1524                   warnTc True (vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty),
1525                                      pprInstsInFull dicts])
1526
1527 -- The error message when we don't find a suitable instance
1528 -- is complicated by the fact that sometimes this is because
1529 -- there is no instance, and sometimes it's because there are
1530 -- too many instances (overlap).  See the comments in TcEnv.lhs
1531 -- with the InstEnv stuff.
1532 addNoInstanceErr what_doc givens dict
1533   = tcGetInstEnv        `thenNF_Tc` \ inst_env ->
1534     let
1535         doc = vcat [sep [herald <+> quotes (pprInst tidy_dict),
1536                          nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1537                     ambig_doc,
1538                     ptext SLIT("Probable fix:"),
1539                     nest 4 fix1,
1540                     nest 4 fix2]
1541
1542         herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
1543         unambig_doc | ambig_overlap = ptext SLIT("unambiguously")
1544                     | otherwise     = empty
1545
1546         ambig_doc
1547             | not ambig_overlap = empty
1548             | otherwise
1549             = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
1550                     nest 4 (ptext SLIT("depends on the instantiation of") <+>
1551                             quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
1552
1553         fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
1554                     ptext SLIT("to the") <+> what_doc]
1555
1556         fix2 | isTyVarDict dict || ambig_overlap
1557              = empty
1558              | otherwise
1559              = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
1560
1561         (tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
1562
1563             -- Checks for the ambiguous case when we have overlapping instances
1564         ambig_overlap | isClassDict dict
1565                       = case lookupInstEnv inst_env clas tys of
1566                             NoMatch ambig -> ambig
1567                             other         -> False
1568                       | otherwise = False
1569                       where
1570                         (clas,tys) = getDictClassTys dict
1571     in
1572     addInstErrTcM (instLoc dict) (tidy_env, doc)
1573
1574 -- Used for the ...Thetas variants; all top level
1575 addNoInstErr (c,ts)
1576   = addErrTc (ptext SLIT("No instance for") <+> quotes (pprClassPred c ts))
1577
1578 reduceDepthErr n stack
1579   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
1580           ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
1581           nest 4 (pprInstsInFull stack)]
1582
1583 reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1584
1585 -----------------------------------------------
1586 addCantGenErr inst
1587   = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"),
1588                    nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
1589 \end{code}