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