TcSimplify.lhs 81.7 KB
 partain committed Jan 08, 1996 1 %  simonm committed Dec 02, 1998 2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998  partain committed Jan 08, 1996 3 4 5 % \section[TcSimplify]{TcSimplify}  simonm committed Jan 08, 1998 6 7 8  \begin{code}  partain committed Jan 08, 1996 9 module TcSimplify (  qrczak committed Jul 17, 2001 10  tcSimplifyInfer, tcSimplifyInferCheck,  simonpj committed Jun 25, 2001 11  tcSimplifyCheck, tcSimplifyRestricted,  simonpj@microsoft.com committed May 19, 2006 12  tcSimplifyRuleLhs, tcSimplifyIPs,  simonpj committed Mar 09, 2005 13  tcSimplifySuperClasses,  simonpj committed Jul 09, 2003 14  tcSimplifyTop, tcSimplifyInteractive,  simonpj committed Sep 13, 2002 15  tcSimplifyBracket,  simonpj committed Mar 13, 2001 16   simonpj committed Dec 28, 2001 17  tcSimplifyDeriv, tcSimplifyDefault,  simonpj committed Jan 25, 2001 18  bindInstsOfLocalFuns  partain committed Jan 08, 1996 19 20  ) where  simonm committed Jan 08, 1998 21 #include "HsVersions.h"  partain committed Mar 19, 1996 22   simonpj@microsoft.com committed Jan 25, 2006 23 import {-# SOURCE #-} TcUnify( unifyType )  simonpj@microsoft.com committed Sep 29, 2006 24 import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, mkWpTyApps,  simonpj@microsoft.com committed Sep 29, 2006 25  HsWrapper(..), (<.>), emptyLHsBinds )  partain committed Mar 19, 1996 26   simonpj committed Sep 13, 2002 27 import TcRnMonad  simonpj committed Feb 05, 2002 28 import Inst ( lookupInst, LookupInstResult(..),  chak@cse.unsw.edu.au. committed Sep 20, 2006 29  tyVarsOfInst, fdPredsOfInsts,  simonpj@microsoft.com committed Sep 29, 2006 30  isDict, isClassDict,  simonpj committed May 20, 2005 31  isMethodFor, isMethod,  simonpj@microsoft.com committed Sep 29, 2006 32  instToId, tyVarsOfInsts,  simonpj committed Dec 28, 2001 33  ipNamesOfInsts, ipNamesOfInst, dictPred,  chak@cse.unsw.edu.au. committed Sep 20, 2006 34  fdPredsOfInst,  simonpj@microsoft.com committed Sep 29, 2006 35  newDictBndrs, newDictBndrsO,  simonpj committed Mar 09, 2005 36 37  getDictClassTys, isTyVarDict, instLoc, zonkInst, tidyInsts, tidyMoreInsts,  simonpj committed Jul 12, 2005 38  pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,  simonpj committed Apr 28, 2005 39  isInheritableInst, pprDictsTheta  sof committed Jul 26, 1997 40  )  simonpj@microsoft.com committed Sep 29, 2006 41 import TcEnv ( tcGetGlobalTyVars, findGlobals, pprBinders,  simonpj committed May 19, 2005 42  lclEnvElts, tcMetaTy )  simonpj committed Apr 28, 2005 43 import InstEnv ( lookupInstEnv, classInstances, pprInstances )  simonpj@microsoft.com committed Jun 26, 2006 44 import TcMType ( zonkTcTyVarsAndFV, tcInstTyVars, zonkTcPredType )  simonpj@microsoft.com committed Feb 23, 2006 45 import TcType ( TcTyVar, TcTyVarSet, ThetaType, TcPredType, tidyPred,  simonpj@microsoft.com committed Sep 29, 2006 46  mkClassPred, isOverloadedTy, isSkolemTyVar,  simonpj committed Dec 28, 2001 47  mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,  simonpj committed Jul 12, 2005 48  tyVarsOfPred, tcEqType, pprPred, mkPredTy, tcIsTyVarTy )  simonpj committed Apr 28, 2005 49 import TcIface ( checkWiredInTyCon )  simonpj@microsoft.com committed Sep 29, 2006 50 import Id ( idType )  simonpj committed Dec 28, 2001 51 import Var ( TyVar )  Ross Paterson committed Feb 13, 2006 52 import TyCon ( TyCon )  simonpj@microsoft.com committed Sep 29, 2006 53 import Name ( Name )  simonpj committed Oct 25, 2001 54 import NameSet ( NameSet, mkNameSet, elemNameSet )  simonpj committed Jul 03, 2003 55 import Class ( classBigSig, classKey )  simonpj@microsoft.com committed Feb 23, 2006 56 import FunDeps ( oclose, grow, improve, pprEquation )  simonpj committed May 20, 2005 57 import PrelInfo ( isNumericClass, isStandardClass )  simonpj@microsoft.com committed Sep 29, 2006 58 import PrelNames ( integerTyConName,  simonpj committed Oct 09, 2003 59  showClassKey, eqClassKey, ordClassKey )  simonpj committed Sep 30, 2004 60 import Type ( zipTopTvSubst, substTheta, substTy )  simonpj@microsoft.com committed Sep 29, 2006 61 import TysWiredIn ( doubleTy, doubleTyCon )  simonpj committed Nov 28, 2002 62 import ErrUtils ( Message )  simonpj committed Feb 04, 2005 63 import BasicTypes ( TopLevelFlag, isNotTopLevel )  simonm committed Dec 02, 1998 64 import VarSet  simonpj committed Nov 28, 2002 65 import VarEnv ( TidyEnv )  simonm committed Jan 08, 1998 66 import FiniteMap  simonmar committed Dec 10, 2003 67 import Bag  simonm committed Jan 08, 1998 68 import Outputable  simonpj committed Oct 03, 2000 69 import ListSetOps ( equivClasses )  simonpj committed Feb 19, 2003 70 import Util ( zipEqual, isSingleton )  simonm committed Jan 08, 1998 71 import List ( partition )  simonmar committed Dec 10, 2003 72 import SrcLoc ( Located(..) )  simonpj@microsoft.com committed Jul 27, 2006 73 import DynFlags ( DynFlags(ctxtStkDepth),  simonpj@microsoft.com committed Aug 07, 2006 74 75  DynFlag( Opt_GlasgowExts, Opt_AllowUndecidableInstances, Opt_WarnTypeDefaults, Opt_ExtendedDefaultRules ) )  partain committed Jan 08, 1996 76 77 78 79 80 \end{code} %************************************************************************ %* *  simonpj committed Jan 25, 2001 81 \subsection{NOTES}  partain committed Jan 08, 1996 82 83 84 %* * %************************************************************************  simonpj committed Feb 10, 2004 85 86 87 88  -------------------------------------- Notes on functional dependencies (a bug) --------------------------------------  simonpj@microsoft.com committed Sep 18, 2006 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 Consider this: class C a b | a -> b class D a b | a -> b instance D a b => C a b -- Undecidable -- (Not sure if it's crucial to this eg) f :: C a b => a -> Bool f _ = True g :: C a b => a -> Bool g = f Here f typechecks, but g does not!! Reason: before doing improvement, we reduce the (C a b1) constraint from the call of f to (D a b1). Here is a more complicated example:  simonpj committed Feb 10, 2004 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 | > class Foo a b | a->b | > | > class Bar a b | a->b | > | > data Obj = Obj | > | > instance Bar Obj Obj | > | > instance (Bar a b) => Foo a b | > | > foo:: (Foo a b) => a -> String | > foo _ = "works" | > | > runFoo:: (forall a b. (Foo a b) => a -> w) -> w | > runFoo f = f Obj | | *Test> runFoo foo | | :1: | Could not deduce (Bar a b) from the context (Foo a b) | arising from use of foo' at :1 | Probable fix: | Add (Bar a b) to the expected type of an expression | In the first argument of runFoo', namely foo' | In the definition of it': it = runFoo foo | | Why all of the sudden does GHC need the constraint Bar a b? The | function foo didn't ask for that... The trouble is that to type (runFoo foo), GHC has to solve the problem: Given constraint Foo a b Solve constraint Foo a b' Notice that b and b' aren't the same. To solve this, just do improvement and then they are the same. But GHC currently does simplify constraints apply improvement and loop That is usually fine, but it isn't here, because it sees that Foo a b is not the same as Foo a b', and so instead applies the instance decl for instance Bar a b => Foo a b. And that's where the Bar constraint comes from. The Right Thing is to improve whenever the constraint set changes at all. Not hard in principle, but it'll take a bit of fiddling to do.  qrczak committed Jul 17, 2001 157  --------------------------------------  simonpj committed Jan 25, 2001 158  Notes on quantification  qrczak committed Jul 17, 2001 159  --------------------------------------  simonpj committed Jan 25, 2001 160 161 162 163 164 165  Suppose we are about to do a generalisation step. We have in our hand G the environment T the type of the RHS  qrczak committed Jan 26, 2001 166  C the constraints from that RHS  simonpj committed Jan 25, 2001 167 168 169 170 171 172 173 174 175 176 177  The game is to figure out Q the set of type variables over which to quantify Ct the constraints we will *not* quantify over Cq the constraints we will quantify over So we're going to infer the type forall Q. Cq => T  qrczak committed Jul 17, 2001 178 and float the constraints Ct further outwards.  simonpj committed Jan 25, 2001 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216  Here are the things that *must* be true: (A) Q intersect fv(G) = EMPTY limits how big Q can be (B) Q superset fv(Cq union T) \ oclose(fv(G),C) limits how small Q can be (A) says we can't quantify over a variable that's free in the environment. (B) says we must quantify over all the truly free variables in T, else we won't get a sufficiently general type. We do not *need* to quantify over any variable that is fixed by the free vars of the environment G. BETWEEN THESE TWO BOUNDS, ANY Q WILL DO! Example: class H x y | x->y where ... fv(G) = {a} C = {H a b, H c d} T = c -> b (A) Q intersect {a} is empty (B) Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d} So Q can be {c,d}, {b,c,d} Other things being equal, however, we'd like to quantify over as few variables as possible: smaller types, fewer type applications, more constraints can get into Ct instead of Cq. ----------------------------------------- We will make use of fv(T) the free type vars of T oclose(vs,C) The result of extending the set of tyvars vs using the functional dependencies from C grow(vs,C) The result of extend the set of tyvars vs  qrczak committed Jul 17, 2001 217  using all conceivable links from C.  simonpj committed Jan 25, 2001 218 219 220 221 222 223 224  E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e} Then grow(vs,C) = {a,b,c} Note that grow(vs,C) superset grow(vs,simplify(C)) That is, simplfication can only shrink the result of grow.  qrczak committed Jul 17, 2001 225 Notice that  simonpj committed Jan 25, 2001 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245  oclose is conservative one way: v elem oclose(vs,C) => v is definitely fixed by vs grow is conservative the other way: if v might be fixed by vs => v elem grow(vs,C) ----------------------------------------- Choosing Q ~~~~~~~~~~ Here's a good way to choose Q: Q = grow( fv(T), C ) \ oclose( fv(G), C ) That is, quantify over all variable that that MIGHT be fixed by the call site (which influences T), but which aren't DEFINITELY fixed by G. This choice definitely quantifies over enough type variables, albeit perhaps too many. Why grow( fv(T), C ) rather than fv(T)? Consider class H x y | x->y where ...  qrczak committed Jul 17, 2001 246   simonpj committed Jan 25, 2001 247 248 249 250 251 252 253  T = c->c C = (H c d) If we used fv(T) = {c} we'd get the type forall c. H c d => c -> b  qrczak committed Jul 17, 2001 254  And then if the fn was called at several different c's, each of  simonpj committed Jan 25, 2001 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277  which fixed d differently, we'd get a unification error, because d isn't quantified. Solution: quantify d. So we must quantify everything that might be influenced by c. Why not oclose( fv(T), C )? Because we might not be able to see all the functional dependencies yet: class H x y | x->y where ... instance H x y => Eq (T x y) where ... T = c->c C = (Eq (T c d)) Now oclose(fv(T),C) = {c}, because the functional dependency isn't apparent yet, and that's wrong. We must really quantify over d too. There really isn't any point in quantifying over any more than grow( fv(T), C ), because the call sites can't possibly influence any other type variables.  simonpj@microsoft.com committed Sep 18, 2006 278 279 280 ------------------------------------- Note [Ambiguity] -------------------------------------  simonpj committed Jan 25, 2001 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319  It's very hard to be certain when a type is ambiguous. Consider class K x class H x y | x -> y instance H x y => K (x,y) Is this type ambiguous? forall a b. (K (a,b), Eq b) => a -> a Looks like it! But if we simplify (K (a,b)) we get (H a b) and now we see that a fixes b. So we can't tell about ambiguity for sure without doing a full simplification. And even that isn't possible if the context has some free vars that may get unified. Urgle! Here's another example: is this ambiguous? forall a b. Eq (T b) => a -> a Not if there's an insance decl (with no context) instance Eq (T b) where ... You may say of this example that we should use the instance decl right away, but you can't always do that: class J a b where ... instance J Int b where ... f :: forall a b. J a b => a -> a (Notice: no functional dependency in J's class decl.) Here f's type is perfectly fine, provided f is only called at Int. It's premature to complain when meeting f's signature, or even when inferring a type for f. However, we don't *need* to report ambiguity right away. It'll always show up at the call site.... and eventually at main, which needs special treatment. Nevertheless, reporting ambiguity promptly is an excellent thing.  simonpj committed May 03, 2001 320 So here's the plan. We WARN about probable ambiguity if  simonpj committed Jan 25, 2001 321 322 323 324 325  fv(Cq) is not a subset of oclose(fv(T) union fv(G), C) (all tested before quantification). That is, all the type variables in Cq must be fixed by the the variables  qrczak committed Jul 17, 2001 326 in the environment, or by the variables in the type.  simonpj committed Jan 25, 2001 327 328 329  Notice that we union before calling oclose. Here's an example:  qrczak committed Jan 26, 2001 330  class J a b c | a b -> c  simonpj committed Jan 25, 2001 331 332 333  fv(G) = {a} Is this ambiguous?  qrczak committed Jan 26, 2001 334  forall b c. (J a b c) => b -> b  simonpj committed Jan 25, 2001 335 336  Only if we union {a} from G with {b} from T before using oclose,  qrczak committed Jul 17, 2001 337 do we see that c is fixed.  simonpj committed Jan 25, 2001 338   qrczak committed Jul 17, 2001 339 It's a bit vague exactly which C we should use for this oclose call. If we  simonpj committed Jan 25, 2001 340 341 342 343 344 345 346 347 348 don't fix enough variables we might complain when we shouldn't (see the above nasty example). Nothing will be perfect. That's why we can only issue a warning. Can we ever be *certain* about ambiguity? Yes: if there's a constraint c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY  qrczak committed Jul 17, 2001 349 then c is a "bubble"; there's no way it can ever improve, and it's  simonpj committed Jan 25, 2001 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 certainly ambiguous. UNLESS it is a constant (sigh). And what about the nasty example? class K x class H x y | x -> y instance H x y => K (x,y) Is this type ambiguous? forall a b. (K (a,b), Eq b) => a -> a Urk. The (Eq b) looks "definitely ambiguous" but it isn't. What we are after is a "bubble" that's a set of constraints Cq = Ca union Cq' st fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY Hence another idea. To decide Q start with fv(T) and grow it by transitive closure in Cq (no functional dependencies involved). Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.  simonpj committed May 03, 2001 368 The definitely-ambiguous can then float out, and get smashed at top level  simonpj committed Jan 25, 2001 369 370 371 (which squashes out the constants, like Eq (T a) above)  qrczak committed Jul 17, 2001 372  --------------------------------------  simonpj committed May 03, 2001 373  Notes on principal types  qrczak committed Jul 17, 2001 374  --------------------------------------  simonpj committed May 03, 2001 375 376 377  class C a where op :: a -> a  qrczak committed Jul 17, 2001 378   simonpj committed May 03, 2001 379 380 381 382 383 384 385  f x = let g y = op (y::Int) in True Here the principal type of f is (forall a. a->a) but we'll produce the non-principal type f :: forall a. C Int => a -> a  simonpj committed Feb 10, 2004 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415  -------------------------------------- The need for forall's in constraints -------------------------------------- [Exchange on Haskell Cafe 5/6 Dec 2000] class C t where op :: t -> Bool instance C [t] where op x = True p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ []) q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f) The definitions of p and q differ only in the order of the components in the pair on their right-hand sides. And yet: ghc and "Typing Haskell in Haskell" reject p, but accept q; Hugs rejects q, but accepts p; hbc rejects both p and q; nhc98 ... (Malcolm, can you fill in the blank for us!). The type signature for f forces context reduction to take place, and the results of this depend on whether or not the type of y is known, which in turn depends on which component of the pair the type checker analyzes first. Solution: if y::m a, float out the constraints Monad m, forall c. C (m c) When m is later unified with [], we can solve both constraints.  qrczak committed Jul 17, 2001 416  --------------------------------------  simonpj committed Jan 25, 2001 417  Notes on implicit parameters  qrczak committed Jul 17, 2001 418  --------------------------------------  simonpj committed Jan 25, 2001 419   simonpj committed May 03, 2001 420 421 422 423 424 Question 1: can we "inherit" implicit parameters ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 425   simonpj committed May 03, 2001 426 427 428 where f is *not* a top-level binding. From the RHS of f we'll get the constraint (?y::Int). There are two types we might infer for f:  simonpj committed Jan 25, 2001 429   simonpj committed May 03, 2001 430 431 432  f :: Int -> Int (so we get ?y from the context of f's definition), or  simonpj committed Jan 25, 2001 433 434 435  f :: (?y::Int) => Int -> Int  simonpj committed May 03, 2001 436 437 438 439 440 441 At first you might think the first was better, becuase then ?y behaves like a free variable of the definition, rather than having to be passed at each call site. But of course, the WHOLE IDEA is that ?y should be passed at each call site (that's what dynamic binding means) so we'd better infer the second.  simonpj committed Oct 25, 2001 442 443 BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring.  simonpj committed Jun 25, 2001 444   simonpj committed Oct 25, 2001 445 446 447 448 449  Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ BUT WATCH OUT: When you supply a type signature, we can't force you to quantify over implicit parameters. For example:  simonpj committed Jun 25, 2001 450 451 452 453 454 455 456 457 458 459 460  (?x + 1) :: Int This is perfectly reasonable. We do not want to insist on (?x + 1) :: (?x::Int => Int) That would be silly. Here, the definition site *is* the occurrence site, so the above strictures don't apply. Hence the difference between tcSimplifyCheck (which *does* allow implicit paramters to be inherited) and tcSimplifyCheckBind (which does not).  simonpj committed May 03, 2001 461   simonpj committed Oct 25, 2001 462 463 464 What about when you supply a type signature for a binding? Is it legal to give the following explicit, user type signature to f, thus:  simonpj committed May 03, 2001 465   simonpj committed Jan 25, 2001 466  f :: Int -> Int  simonpj committed May 03, 2001 467  f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 468   simonpj committed May 03, 2001 469 At first sight this seems reasonable, but it has the nasty property  simonpj committed Jul 12, 2001 470 that adding a type signature changes the dynamic semantics.  simonpj committed May 03, 2001 471 Consider this:  simonpj committed Jan 25, 2001 472   simonpj committed May 03, 2001 473  (let f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 474 475 476 477  in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+5) vs  simonpj committed Jul 12, 2001 478  (let f :: Int -> Int  simonpj committed May 03, 2001 479  f x = x + ?y  simonpj committed Jan 25, 2001 480 481 482 483  in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+6)  simonpj committed May 03, 2001 484 485 Indeed, simply inlining f (at the Haskell source level) would change the dynamic semantics.  simonpj committed Jan 25, 2001 486   simonpj committed Oct 25, 2001 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 Nevertheless, as Launchbury says (email Oct 01) we can't really give the semantics for a Haskell program without knowing its typing, so if you change the typing you may change the semantics. To make things consistent in all cases where we are *checking* against a supplied signature (as opposed to inferring a type), we adopt the rule: a signature does not need to quantify over implicit params. [This represents a (rather marginal) change of policy since GHC 5.02, which *required* an explicit signature to quantify over all implicit params for the reasons mentioned above.] But that raises a new question. Consider Given (signature) ?x::Int Wanted (inferred) ?x::Int, ?y::Bool Clearly we want to discharge the ?x and float the ?y out. But what is the criterion that distinguishes them? Clearly it isn't what free type variables they have. The Right Thing seems to be to float a constraint that neither mentions any of the quantified type variables nor any of the quantified implicit parameters See the predicate isFreeWhenChecking.  simonpj committed Jan 25, 2001 514   simonpj committed Apr 30, 2001 515   simonpj committed May 03, 2001 516 517 518 Question 3: monomorphism ~~~~~~~~~~~~~~~~~~~~~~~~ There's a nasty corner case when the monomorphism restriction bites:  simonpj committed Apr 30, 2001 519   simonpj committed May 03, 2001 520 521  z = (x::Int) + ?y  simonpj committed Jul 12, 2001 522 523 The argument above suggests that we *must* generalise over the ?y parameter, to get  simonpj committed May 03, 2001 524 525  z :: (?y::Int) => Int, but the monomorphism restriction says that we *must not*, giving  qrczak committed Jul 17, 2001 526  z :: Int.  simonpj committed May 03, 2001 527 528 529 530 531 532 533 534 Why does the momomorphism restriction say this? Because if you have let z = x + ?y in z+z you might not expect the addition to be done twice --- but it will if we follow the argument of Question 2 and generalise over ?y.  simonpj committed Feb 04, 2005 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 Question 4: top level ~~~~~~~~~~~~~~~~~~~~~ At the top level, monomorhism makes no sense at all. module Main where main = let ?x = 5 in print foo foo = woggle 3 woggle :: (?x :: Int) => Int -> Int woggle y = ?x + y We definitely don't want (foo :: Int) with a top-level implicit parameter (?x::Int) becuase there is no way to bind it.  simonpj committed May 03, 2001 550 551 552 553 554 555 556 557  Possible choices ~~~~~~~~~~~~~~~~ (A) Always generalise over implicit parameters Bindings that fall under the monomorphism restriction can't be generalised Consequences:  qrczak committed Jul 17, 2001 558  * Inlining remains valid  simonpj committed May 03, 2001 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595  * No unexpected loss of sharing * But simple bindings like z = ?y + 1 will be rejected, unless you add an explicit type signature (to avoid the monomorphism restriction) z :: (?y::Int) => Int z = ?y + 1 This seems unacceptable (B) Monomorphism restriction "wins" Bindings that fall under the monomorphism restriction can't be generalised Always generalise over implicit parameters *except* for bindings that fall under the monomorphism restriction Consequences * Inlining isn't valid in general * No unexpected loss of sharing * Simple bindings like z = ?y + 1 accepted (get value of ?y from binding site) (C) Always generalise over implicit parameters Bindings that fall under the monomorphism restriction can't be generalised, EXCEPT for implicit parameters Consequences * Inlining remains valid * Unexpected loss of sharing (from the extra generalisation) * Simple bindings like z = ?y + 1 accepted (get value of ?y from occurrence sites) Discussion ~~~~~~~~~~ None of these choices seems very satisfactory. But at least we should decide which we want to do.  simonpj committed Apr 30, 2001 596   simonpj committed May 03, 2001 597 It's really not clear what is the Right Thing To Do. If you see  simonpj committed Jan 25, 2001 598   simonpj committed May 03, 2001 599  z = (x::Int) + ?y  simonpj committed Jan 25, 2001 600   simonpj committed May 03, 2001 601 602 603 604 605 606 would you expect the value of ?y to be got from the *occurrence sites* of 'z', or from the valuue of ?y at the *definition* of 'z'? In the case of function definitions, the answer is clearly the former, but less so in the case of non-fucntion definitions. On the other hand, if we say that we get the value of ?y from the definition site of 'z', then inlining 'z' might change the semantics of the program.  simonpj committed Jan 25, 2001 607   simonpj committed May 03, 2001 608 Choice (C) really says "the monomorphism restriction doesn't apply  simonpj committed Jul 12, 2001 609 to implicit parameters". Which is fine, but remember that every  simonpj committed May 03, 2001 610 611 612 innocent binding 'x = ...' that mentions an implicit parameter in the RHS becomes a *function* of that parameter, called at each use of 'x'. Now, the chances are that there are no intervening 'with'  simonpj committed Jul 12, 2001 613 clauses that bind ?y, so a decent compiler should common up all  simonpj committed May 03, 2001 614 615 616 those function calls. So I think I strongly favour (C). Indeed, one could make a similar argument for abolishing the monomorphism restriction altogether.  simonpj committed Jan 25, 2001 617   simonpj committed May 03, 2001 618 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted  simonpj committed Jan 25, 2001 619   qrczak committed Jul 17, 2001 620   simonpj committed May 03, 2001 621   simonpj committed Jan 25, 2001 622 623 624 625 626 627 628 629 630 %************************************************************************ %* * \subsection{tcSimplifyInfer} %* * %************************************************************************ tcSimplify is called when we *inferring* a type. Here's the overall game plan: 1. Compute Q = grow( fvs(T), C )  qrczak committed Jul 17, 2001 631 632  2. Partition C based on Q into Ct and Cq. Notice that ambiguous  simonpj committed Jan 25, 2001 633  predicates will end up in Ct; we deal with them at the top level  qrczak committed Jul 17, 2001 634   simonpj committed Jan 25, 2001 635  3. Try improvement, using functional dependencies  qrczak committed Jul 17, 2001 636   simonpj committed Jan 25, 2001 637 638 639 640  4. If Step 3 did any unification, repeat from step 1 (Unification can change the result of 'grow'.) Note: we don't reduce dictionaries in step 2. For example, if we have  qrczak committed Jul 17, 2001 641 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different  simonpj committed Jan 25, 2001 642 643 644 645 646 647 648 after step 2. However note that we may therefore quantify over more type variables than we absolutely have to. For the guts, we need a loop, that alternates context reduction and improvement with unification. E.g. Suppose we have class C x y | x->y where ...  qrczak committed Jul 17, 2001 649   simonpj committed Jan 25, 2001 650 651 652 653 654 655 and tcSimplify is called with: (C Int a, C Int b) Then improvement unifies a with b, giving (C Int a, C Int a) If we need to unify anything, we rattle round the whole thing all over  qrczak committed Jul 17, 2001 656 again.  simonpj committed Jan 25, 2001 657   partain committed Jan 08, 1996 658 659  \begin{code}  simonpj committed Jan 25, 2001 660 tcSimplifyInfer  qrczak committed Jul 17, 2001 661 662  :: SDoc -> TcTyVarSet -- fv(T); type vars  simonpj committed Sep 13, 2002 663  -> [Inst] -- Wanted  simonpj committed Jan 25, 2001 664 665 666  -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) TcDictBinds, -- Bindings [TcId]) -- Dict Ids that must be bound here (zonked)  simonpj committed Sep 13, 2002 667  -- Any free (escaping) Insts are tossed into the environment  simonpj committed Jan 25, 2001 668 \end{code}  simonm committed Dec 02, 1998 669   simonpj committed Jan 25, 2001 670 671 672  \begin{code} tcSimplifyInfer doc tau_tvs wanted_lie  qrczak committed Jul 17, 2001 673  = inferLoop doc (varSetElems tau_tvs)  simonpj committed Sep 13, 2002 674  wanted_lie thenM \ (qtvs, frees, binds, irreds) ->  simonpj committed Feb 10, 1998 675   simonpj committed Sep 13, 2002 676 677  extendLIEs frees thenM_ returnM (qtvs, binds, map instToId irreds)  simonpj committed Jan 25, 2001 678 679 680  inferLoop doc tau_tvs wanteds = -- Step 1  simonpj committed Sep 13, 2002 681 682 683  zonkTcTyVarsAndFV tau_tvs thenM \ tau_tvs' -> mappM zonkInst wanteds thenM \ wanteds' -> tcGetGlobalTyVars thenM \ gbl_tvs ->  simonpj committed Feb 10, 1998 684  let  simonpj committed Sep 13, 2002 685  preds = fdPredsOfInsts wanteds'  simonpj committed Jan 25, 2001 686  qtvs = grow preds tau_tvs' minusVarSet oclose preds gbl_tvs  qrczak committed Jul 17, 2001 687 688  try_me inst  simonpj committed Oct 25, 2001 689 690  | isFreeWhenInferring qtvs inst = Free | isClassDict inst = DontReduceUnlessConstant -- Dicts  simonpj committed Mar 09, 2005 691  | otherwise = ReduceMe NoSCs -- Lits and Methods  simonpj committed Mar 19, 1998 692  in  simonpj committed Sep 30, 2004 693 694  traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, ppr (grow preds tau_tvs'), ppr qtvs]) thenM_  simonpj committed Jan 25, 2001 695  -- Step 2  simonpj committed Sep 13, 2002 696  reduceContext doc try_me [] wanteds' thenM \ (no_improvement, frees, binds, irreds) ->  qrczak committed Jul 17, 2001 697   simonpj committed Jan 25, 2001 698 699  -- Step 3 if no_improvement then  simonpj committed Sep 13, 2002 700  returnM (varSetElems qtvs, frees, binds, irreds)  simonpj committed Jan 25, 2001 701  else  simonpj committed Feb 20, 2001 702 703 704 705 706 707 708 709 710 711 712 713  -- If improvement did some unification, we go round again. There -- are two subtleties: -- a) We start again with irreds, not wanteds -- Using an instance decl might have introduced a fresh type variable -- which might have been unified, so we'd get an infinite loop -- if we started again with wanteds! See example [LOOP] -- -- b) It's also essential to re-process frees, because unification -- might mean that a type variable that looked free isn't now. -- -- Hence the (irreds ++ frees)  simonpj committed Oct 17, 2001 714 715 716  -- However, NOTICE that when we are done, we might have some bindings, but -- the final qtvs might be empty. See [NO TYVARS] below.  simonpj committed Sep 13, 2002 717  inferLoop doc tau_tvs (irreds ++ frees) thenM \ (qtvs1, frees1, binds1, irreds1) ->  simonmar committed Dec 10, 2003 718  returnM (qtvs1, frees1, binds unionBags binds1, irreds1)  qrczak committed Jul 17, 2001 719 \end{code}  simonpj committed Mar 19, 1998 720   simonpj committed Jan 30, 2001 721 722 723 724 725 726 727 728 729 730 731 732 733 Example [LOOP] class If b t e r | b t e -> r instance If T t e t instance If F t e e class Lte a b c | a b -> c where lte :: a -> b -> c instance Lte Z b T instance (Lte a b l,If l b a c) => Max a b c Wanted: Max Z (S x) y Then we'll reduce using the Max instance to: (Lte Z (S x) l, If l (S x) Z y)  qrczak committed Jul 17, 2001 734 and improve by binding l->T, after which we can do some reduction  simonpj committed Jan 30, 2001 735 736 737 on both the Lte and If constraints. What we *can't* do is start again with (Max Z (S x) y)!  simonpj committed Oct 17, 2001 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 [NO TYVARS] class Y a b | a -> b where y :: a -> X b instance Y [[a]] a where y ((x:_):_) = X x k :: X a -> X a -> X a g :: Num a => [X a] -> [X a] g xs = h xs where h ys = ys ++ map (k (y [[0]])) xs The excitement comes when simplifying the bindings for h. Initially try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}. From this we get t1:=:t2, but also various bindings. We can't forget the bindings (because of [LOOP]), but in fact t1 is what g is  simonpj committed Oct 25, 2001 757 758 759 polymorphic in. The net effect of [NO TYVARS]  simonpj committed Oct 17, 2001 760   simonpj committed Jan 25, 2001 761 \begin{code}  simonpj committed Oct 25, 2001 762 763 isFreeWhenInferring :: TyVarSet -> Inst -> Bool isFreeWhenInferring qtvs inst  simonpj committed Sep 13, 2002 764 765 766  = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars && isInheritableInst inst -- And no implicit parameter involved -- (see "Notes on implicit parameters")  simonpj committed Oct 25, 2001 767 768 769 770 771 772 773 774  isFreeWhenChecking :: TyVarSet -- Quantified tyvars -> NameSet -- Quantified implicit parameters -> Inst -> Bool isFreeWhenChecking qtvs ips inst = isFreeWrtTyVars qtvs inst && isFreeWrtIPs ips inst  simonpj@microsoft.com committed Sep 23, 2006 775 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst disjointVarSet qtvs  simonpj committed Oct 25, 2001 776 isFreeWrtIPs ips inst = not (any (elemNameSet ips) (ipNamesOfInst inst))  simonpj committed Jan 25, 2001 777 \end{code}  simonpj committed Mar 19, 1998 778   simonpj committed Feb 10, 1998 779   simonpj committed Jan 25, 2001 780 781 782 783 784 %************************************************************************ %* * \subsection{tcSimplifyCheck} %* * %************************************************************************  partain committed Mar 19, 1996 785   simonpj committed Jan 25, 2001 786 @tcSimplifyCheck@ is used when we know exactly the set of variables  simonpj committed Feb 20, 2001 787 we are going to quantify over. For example, a class or instance declaration.  partain committed Jan 08, 1996 788 789  \begin{code}  simonpj committed Jan 25, 2001 790 tcSimplifyCheck  qrczak committed Jul 17, 2001 791  :: SDoc  simonpj committed Jan 25, 2001 792 793  -> [TcTyVar] -- Quantify over these -> [Inst] -- Given  simonpj committed Sep 13, 2002 794 795  -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings  partain committed Mar 19, 1996 796   simonpj committed Oct 25, 2001 797 -- tcSimplifyCheck is used when checking expression type signatures,  simonpj committed Jun 25, 2001 798 -- class decls, instance decls etc.  simonpj committed Feb 15, 2002 799 800 801 802 -- -- NB: tcSimplifyCheck does not consult the -- global type variables in the environment; so you don't -- need to worry about setting them before calling tcSimplifyCheck  simonpj committed Jan 25, 2001 803 tcSimplifyCheck doc qtvs givens wanted_lie  simonpj committed Mar 09, 2005 804 805 806 807  = ASSERT( all isSkolemTyVar qtvs ) do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie ; extendLIEs frees ; return binds }  simonpj committed Jun 25, 2001 808  where  simonpj committed Mar 09, 2005 809 810 -- get_qtvs = zonkTcTyVarsAndFV qtvs get_qtvs = return (mkVarSet qtvs) -- All skolems  simonpj committed Jun 25, 2001 811 812 813 814 815 816  -- tcSimplifyInferCheck is used when we know the constraints we are to simplify -- against, but we don't know the type variables over which we are going to quantify. -- This happens when we have a type signature for a mutually recursive group tcSimplifyInferCheck  qrczak committed Jul 17, 2001 817  :: SDoc  simonpj committed Jun 25, 2001 818 819  -> TcTyVarSet -- fv(T) -> [Inst] -- Given  simonpj committed Sep 13, 2002 820  -> [Inst] -- Wanted  simonpj committed Jun 25, 2001 821 822 823 824  -> TcM ([TcTyVar], -- Variables over which to quantify TcDictBinds) -- Bindings tcSimplifyInferCheck doc tau_tvs givens wanted_lie  simonpj committed Mar 09, 2005 825 826 827  = do { (qtvs', frees, binds) <- tcSimplCheck doc get_qtvs AddSCs givens wanted_lie ; extendLIEs frees ; return (qtvs', binds) }  simonpj committed Jun 25, 2001 828 829 830 831 832 833 834 835 836 837 838 839  where -- Figure out which type variables to quantify over -- You might think it should just be the signature tyvars, -- but in bizarre cases you can get extra ones -- f :: forall a. Num a => a -> a -- f x = fst (g (x, head [])) + 1 -- g a b = (b,a) -- Here we infer g :: forall a b. a -> b -> (b,a) -- We don't want g to be monomorphic in b just because -- f isn't quantified over b. all_tvs = varSetElems (tau_tvs unionVarSet tyVarsOfInsts givens)  simonpj committed Sep 13, 2002 840 841  get_qtvs = zonkTcTyVarsAndFV all_tvs thenM \ all_tvs' -> tcGetGlobalTyVars thenM \ gbl_tvs ->  simonpj committed Jun 25, 2001 842 843 844  let qtvs = all_tvs' minusVarSet gbl_tvs -- We could close gbl_tvs, but its not necessary for  qrczak committed Jul 17, 2001 845  -- soundness, and it'll only affect which tyvars, not which  simonpj committed Jun 25, 2001 846 847  -- dictionaries, we quantify over in  simonpj committed Sep 13, 2002 848  returnM qtvs  simonpj committed Jun 25, 2001 849 850 851 852 \end{code} Here is the workhorse function for all three wrappers.  qrczak committed Jul 17, 2001 853 \begin{code}  simonpj committed Mar 09, 2005 854 855 tcSimplCheck doc get_qtvs want_scs givens wanted_lie = do { (qtvs, frees, binds, irreds) <- check_loop givens wanted_lie  partain committed Mar 19, 1996 856   simonpj committed Mar 09, 2005 857 858 859 860 861  -- Complain about any irreducible ones ; if not (null irreds) then do { givens' <- mappM zonkInst given_dicts_and_ips ; groupErrs (addNoInstanceErrs (Just doc) givens') irreds } else return ()  lewie committed Apr 12, 2001 862   simonpj committed Mar 09, 2005 863  ; returnM (qtvs, frees, binds) }  simonpj committed Jun 25, 2001 864  where  simonpj committed Oct 09, 2003 865 866 867 868  given_dicts_and_ips = filter (not . isMethod) givens -- For error reporting, filter out methods, which are -- only added to the given set as an optimisation  simonpj committed Oct 25, 2001 869 870  ip_set = mkNameSet (ipNamesOfInsts givens)  simonpj committed Jun 25, 2001 871 872  check_loop givens wanteds = -- Step 1  simonpj committed Sep 13, 2002 873 874  mappM zonkInst givens thenM \ givens' -> mappM zonkInst wanteds thenM \ wanteds' ->  simonpj committed Apr 09, 2003 875  get_qtvs thenM \ qtvs' ->  qrczak committed Jul 17, 2001 876   simonpj committed Jun 25, 2001 877 878 879 880  -- Step 2 let -- When checking against a given signature we always reduce -- until we find a match against something given, or can't reduce  simonpj committed Oct 25, 2001 881  try_me inst | isFreeWhenChecking qtvs' ip_set inst = Free  simonpj committed Mar 09, 2005 882  | otherwise = ReduceMe want_scs  simonpj committed Jun 25, 2001 883  in  simonpj committed Sep 13, 2002 884  reduceContext doc try_me givens' wanteds' thenM \ (no_improvement, frees, binds, irreds) ->  qrczak committed Jul 17, 2001 885   simonpj committed Jun 25, 2001 886 887  -- Step 3 if no_improvement then  simonpj committed Sep 13, 2002 888  returnM (varSetElems qtvs', frees, binds, irreds)  simonpj committed Jun 25, 2001 889  else  simonpj committed Sep 13, 2002 890  check_loop givens' (irreds ++ frees) thenM \ (qtvs', frees1, binds1, irreds1) ->  simonmar committed Dec 10, 2003 891  returnM (qtvs', frees1, binds unionBags binds1, irreds1)  simonpj committed Jan 25, 2001 892 893 894 \end{code}  simonpj committed Mar 09, 2005 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 %************************************************************************ %* * tcSimplifySuperClasses %* * %************************************************************************ Note [SUPERCLASS-LOOP 1] ~~~~~~~~~~~~~~~~~~~~~~~~ We have to be very, very careful when generating superclasses, lest we accidentally build a loop. Here's an example: class S a class S a => C a where { opc :: a -> a } class S b => D b where { opd :: b -> b } instance C Int where opc = opd instance D Int where opd = opc From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int} Simplifying, we may well get: $dfCInt = :C ds1 (opd dd) dd =$dfDInt ds1 = $p1 dd Notice that we spot that we can extract ds1 from dd. Alas! Alack! We can do the same for (instance D Int):$dfDInt = :D ds2 (opc dc) dc = $dfCInt ds2 =$p1 dc And now we've defined the superclass in terms of itself. Solution: never generate a superclass selectors at all when satisfying the superclass context of an instance declaration. Two more nasty cases are in tcrun021 tcrun033 \begin{code} tcSimplifySuperClasses qtvs givens sc_wanteds = ASSERT( all isSkolemTyVar qtvs ) do { (_, frees, binds1) <- tcSimplCheck doc get_qtvs NoSCs givens sc_wanteds  simonpj@microsoft.com committed Aug 07, 2006 943 944  ; ext_default <- doptM Opt_ExtendedDefaultRules ; binds2 <- tc_simplify_top doc ext_default NoSCs frees  simonpj committed Mar 09, 2005 945 946 947 948 949 950 951  ; return (binds1 unionBags binds2) } where get_qtvs = return (mkVarSet qtvs) doc = ptext SLIT("instance declaration superclass context") \end{code}  simonpj committed May 03, 2001 952 953 954 955 956 957 %************************************************************************ %* * \subsection{tcSimplifyRestricted} %* * %************************************************************************  simonpj committed Mar 11, 2004 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 tcSimplifyRestricted infers which type variables to quantify for a group of restricted bindings. This isn't trivial. Eg1: id = \x -> x We want to quantify over a to get id :: forall a. a->a Eg2: eq = (==) We do not want to quantify over a, because there's an Eq a constraint, so we get eq :: a->a->Bool (notice no forall) So, assume: RHS has type 'tau', whose free tyvars are tau_tvs RHS has constraints 'wanteds' Plan A (simple) Quantify over (tau_tvs \ ftvs(wanteds)) This is bad. The constraints may contain (Monad (ST s)) where we have instance Monad (ST s) where... so there's no need to be monomorphic in s! Also the constraint might be a method constraint, whose type mentions a perfectly innocent tyvar: op :: Num a => a -> b -> a Here, b is unconstrained. A good example would be foo = op (3::Int) We want to infer the polymorphic type foo :: forall b. b -> b Plan B (cunning, used for a long time up to and including GHC 6.2) Step 1: Simplify the constraints as much as possible (to deal with Plan A's problem). Then set qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) Step 2: Now simplify again, treating the constraint as 'free' if it does not mention qtvs, and trying to reduce it otherwise. The reasons for this is to maximise sharing. This fails for a very subtle reason. Suppose that in the Step 2 a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'. In the Step 1 this constraint might have been simplified, perhaps to (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'. This won't happen in Step 2... but that in turn might prevent some other  simonpj committed May 12, 2004 1001 1002  constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) and that in turn breaks the invariant that no constraints are quantified over.  simonpj committed Mar 11, 2004 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014  Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates the problem. Plan C (brutal) Step 1: Simplify the constraints as much as possible (to deal with Plan A's problem). Then set qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) Return the bindings from Step 1.  simonpj committed Mar 19, 2004 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 A note about Plan C (arising from "bug" reported by George Russel March 2004) Consider this: instance (HasBinary ty IO) => HasCodedValue ty foo :: HasCodedValue a => String -> IO a doDecodeIO :: HasCodedValue a => () -> () -> IO a doDecodeIO codedValue view = let { act = foo "foo" } in act You might think this should work becuase the call to foo gives rise to a constraint (HasCodedValue t), which can be satisfied by the type sig for doDecodeIO. But the restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the constraint using the (rather bogus) instance declaration, and now we are stuffed.  simonpj committed May 12, 2004 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050  I claim this is not really a bug -- but it bit Sergey as well as George. So here's plan D Plan D (a variant of plan B) Step 1: Simplify the constraints as much as possible (to deal with Plan A's problem), BUT DO NO IMPROVEMENT. Then set qtvs = tau_tvs \ ftvs( simplify( wanteds ) ) Step 2: Now simplify again, treating the constraint as 'free' if it does not mention qtvs, and trying to reduce it otherwise. The point here is that it's generally OK to have too few qtvs; that is, to make the thing more monomorphic than it could be. We don't want to do that in the common cases, but in wierd cases it's ok: the programmer can always add a signature. Too few qtvs => too many wanteds, which is what happens if you do less improvement.  simonpj committed Mar 11, 2004 1051   simonpj committed May 03, 2001 1052 1053 \begin{code} tcSimplifyRestricted -- Used for restricted binding groups  simonpj committed Jun 25, 2001 1054  -- i.e. ones subject to the monomorphism restriction  qrczak committed Jul 17, 2001 1055  :: SDoc  simonpj committed Feb 04, 2005 1056 1057  -> TopLevelFlag -> [Name] -- Things bound in this group  simonpj committed Jun 25, 2001 1058  -> TcTyVarSet -- Free in the type of the RHSs  simonpj committed Sep 13, 2002 1059  -> [Inst] -- Free in the RHSs  simonpj committed May 03, 2001 1060 1061  -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) TcDictBinds) -- Bindings  simonpj committed Mar 11, 2004 1062 1063 1064  -- tcSimpifyRestricted returns no constraints to -- quantify over; by definition there are none. -- They are all thrown back in the LIE  simonpj committed May 03, 2001 1065   simonpj committed Feb 04, 2005 1066 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds  simonpj committed May 12, 2004 1067 1068 1069 1070  -- Zonk everything in sight = mappM zonkInst wanteds thenM \ wanteds' -> -- 'reduceMe': Reduce as far as we can. Don't stop at  simonpj committed Apr 09, 2003 1071 1072 1073 1074  -- dicts; the idea is to get rid of as many type -- variables as possible, and we don't want to stop -- at (say) Monad (ST s), because that reduces -- immediately, with no constraint on s.  simonpj committed May 12, 2004 1075 1076  -- -- BUT do no improvement! See Plan D above  1077 1078  -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint  simonpj committed May 12, 2004 1079 1080  reduceContextWithoutImprovement doc reduceMe wanteds' thenM \ (_frees, _binds, constrained_dicts) ->  simonpj committed May 03, 2001 1081 1082  -- Next, figure out the tyvars we will quantify over  1083 1084 1085  zonkTcTyVarsAndFV (varSetElems tau_tvs) thenM \ tau_tvs' -> tcGetGlobalTyVars thenM \ gbl_tvs' -> mappM zonkInst constrained_dicts thenM \ constrained_dicts' ->  simonpj committed May 03, 2001 1086  let  1087 1088 1089  constrained_tvs' = tyVarsOfInsts constrained_dicts' qtvs' = (tau_tvs' minusVarSet oclose (fdPredsOfInsts constrained_dicts) gbl_tvs') minusVarSet constrained_tvs'  simonpj committed May 03, 2001 1090  in  simonpj committed Apr 09, 2003 1091  traceTc (text "tcSimplifyRestricted" <+> vcat [  1092  pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts',  simonpj committed May 12, 2004 1093  ppr _binds,  1094  ppr constrained_tvs', ppr tau_tvs', ppr qtvs' ]) thenM_  simonpj committed May 03, 2001 1095   simonpj committed May 12, 2004 1096 1097 1098 1099  -- The first step may have squashed more methods than -- necessary, so try again, this time more gently, knowing the exact -- set of type variables to quantify over. --  1100  -- We quantify only over constraints that are captured by qtvs';  simonpj committed May 12, 2004 1101 1102 1103 1104 1105 1106 1107 1108  -- these will just be a subset of non-dicts. This in contrast -- to normal inference (using isFreeWhenInferring) in which we quantify over -- all *non-inheritable* constraints too. This implements choice -- (B) under "implicit parameter and monomorphism" above. -- -- Remember that we may need to do *some* simplification, to -- (for example) squash {Monad (ST s)} into {}. It's not enough -- just to float all constraints  simonpj committed Feb 04, 2005 1109 1110 1111 1112 1113  -- -- At top level, we *do* squash methods becuase we want to -- expose implicit parameters to the test that follows let is_nested_group = isNotTopLevel top_lvl  1114  try_me inst | isFreeWrtTyVars qtvs' inst,  simonpj committed Feb 04, 2005 1115  (is_nested_group || isDict inst) = Free  simonpj committed Mar 09, 2005 1116  | otherwise = ReduceMe AddSCs  simonpj committed Feb 04, 2005 1117  in  simonpj committed May 12, 2004 1118 1119 1120  reduceContextWithoutImprovement doc try_me wanteds' thenM \ (frees, binds, irreds) -> ASSERT( null irreds )  simonpj committed Feb 04, 2005 1121 1122 1123 1124  -- See "Notes on implicit parameters, Question 4: top level" if is_nested_group then extendLIEs frees thenM_  1125  returnM (varSetElems qtvs', binds)  simonpj committed Feb 04, 2005 1126 1127 1128 1129 1130 1131  else let (non_ips, bad_ips) = partition isClassDict frees in addTopIPErrs bndrs bad_ips thenM_ extendLIEs non_ips thenM_  1132  returnM (varSetElems qtvs', binds)  simonpj committed May 03, 2001 1133 1134 \end{code}  simonpj committed Jan 25, 2001 1135 1136 1137  %************************************************************************ %* *  simonpj@microsoft.com committed May 19, 2006 1138  tcSimplifyRuleLhs  simonpj committed Jan 25, 2001 1139 1140 1141 %* * %************************************************************************  simonpj committed May 18, 1999 1142 1143 1144 1145 On the LHS of transformation rules we only simplify methods and constants, getting dictionaries. We want to keep all of them unsimplified, to serve as the available stuff for the RHS of the rule.  simonpj@microsoft.com committed May 19, 2006 1146 1147 1148 Example. Consider the following left-hand side of a rule f (x == y) (y > z) = ...  qrczak committed Jul 17, 2001 1149   simonpj@microsoft.com committed May 19, 2006 1150 If we typecheck this expression we get constraints  simonpj committed Jun 28, 1999 1151   simonpj@microsoft.com committed May 19, 2006 1152  d1 :: Ord a, d2 :: Eq a  simonpj committed Jun 28, 1999 1153   simonpj@microsoft.com committed May 19, 2006 1154 We do NOT want to "simplify" to the LHS  simonpj committed Jun 28, 1999 1155   simonpj@microsoft.com committed May 19, 2006 1156 1157  forall x::a, y::a, z::a, d1::Ord a. f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...  simonpj committed Jun 28, 1999 1158   simonpj@microsoft.com committed May 19, 2006 1159 Instead we want  simonpj committed Jun 28, 1999 1160   simonpj@microsoft.com committed May 19, 2006 1161 1162  forall x::a, y::a, z::a, d1::Ord a, d2::Eq a. f ((==) d2 x y) ((>) d1 y z) = ...  simonpj committed Jun 28, 1999 1163   simonpj@microsoft.com committed May 19, 2006 1164 Here is another example:  simonpj committed Feb 28, 2001 1165 1166 1167 1168  fromIntegral :: (Integral a, Num b) => a -> b {-# RULES "foo" fromIntegral = id :: Int -> Int #-}  simonpj@microsoft.com committed May 19, 2006 1169 1170 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But we *dont* want to get  simonpj committed Feb 28, 2001 1171 1172  forall dIntegralInt.  simonpj@microsoft.com committed May 19, 2006 1173  fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int