TcSimplify.lhs 89.9 KB
 partain committed Jan 08, 1996 1 %  Simon Marlow committed Oct 11, 2006 2 % (c) The University of Glasgow 2006  simonm committed Dec 02, 1998 3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998  partain committed Jan 08, 1996 4 %  simonm committed Jan 08, 1998 5   Simon Marlow committed Oct 11, 2006 6 TcSimplify  simonm committed Jan 08, 1998 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@microsoft.com committed Nov 10, 2006 15  tcSimplifyBracket, tcSimplifyCheckPat,  simonpj committed Mar 13, 2001 16   simonpj committed Dec 28, 2001 17  tcSimplifyDeriv, tcSimplifyDefault,  simonpj@microsoft.com committed Dec 11, 2006 18  bindInstsOfLocalFuns, bindIrreds,  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 )  Simon Marlow committed Oct 11, 2006 24 import HsSyn  partain committed Mar 19, 1996 25   simonpj committed Sep 13, 2002 26 import TcRnMonad  Simon Marlow committed Oct 11, 2006 27 28 29 import Inst import TcEnv import InstEnv  simonpj@microsoft.com committed Nov 10, 2006 30 import TcGadt  Simon Marlow committed Oct 11, 2006 31 import TcType  simonpj@microsoft.com committed Jan 02, 2007 32 import TcMType  Simon Marlow committed Oct 11, 2006 33 34 35 36 37 38 39 40 41 42 43 44 import TcIface import Var import Name import NameSet import Class import FunDeps import PrelInfo import PrelNames import Type import TysWiredIn import ErrUtils import BasicTypes  simonm committed Dec 02, 1998 45 import VarSet  Simon Marlow committed Oct 11, 2006 46 import VarEnv  simonm committed Jan 08, 1998 47 import FiniteMap  simonmar committed Dec 10, 2003 48 import Bag  simonm committed Jan 08, 1998 49 import Outputable  Simon Marlow committed Oct 11, 2006 50 51 52 53 54 55 import ListSetOps import Util import SrcLoc import DynFlags import Data.List  partain committed Jan 08, 1996 56 57 58 59 60 \end{code} %************************************************************************ %* *  simonpj committed Jan 25, 2001 61 \subsection{NOTES}  partain committed Jan 08, 1996 62 63 64 %* * %************************************************************************  simonpj committed Feb 10, 2004 65 66 67 68  -------------------------------------- Notes on functional dependencies (a bug) --------------------------------------  simonpj@microsoft.com committed Sep 18, 2006 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 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 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 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 | > 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 137  --------------------------------------  simonpj committed Jan 25, 2001 138  Notes on quantification  qrczak committed Jul 17, 2001 139  --------------------------------------  simonpj committed Jan 25, 2001 140 141 142 143 144 145  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 146  C the constraints from that RHS  simonpj committed Jan 25, 2001 147 148 149 150 151 152 153 154 155 156 157  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 158 and float the constraints Ct further outwards.  simonpj committed Jan 25, 2001 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196  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 197  using all conceivable links from C.  simonpj committed Jan 25, 2001 198 199 200 201 202 203 204  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 205 Notice that  simonpj committed Jan 25, 2001 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225  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 226   simonpj committed Jan 25, 2001 227 228 229 230 231 232 233  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 234  And then if the fn was called at several different c's, each of  simonpj committed Jan 25, 2001 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257  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 258 259 260 ------------------------------------- Note [Ambiguity] -------------------------------------  simonpj committed Jan 25, 2001 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299  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 300 So here's the plan. We WARN about probable ambiguity if  simonpj committed Jan 25, 2001 301 302 303 304 305  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 306 in the environment, or by the variables in the type.  simonpj committed Jan 25, 2001 307 308 309  Notice that we union before calling oclose. Here's an example:  qrczak committed Jan 26, 2001 310  class J a b c | a b -> c  simonpj committed Jan 25, 2001 311 312 313  fv(G) = {a} Is this ambiguous?  qrczak committed Jan 26, 2001 314  forall b c. (J a b c) => b -> b  simonpj committed Jan 25, 2001 315 316  Only if we union {a} from G with {b} from T before using oclose,  qrczak committed Jul 17, 2001 317 do we see that c is fixed.  simonpj committed Jan 25, 2001 318   qrczak committed Jul 17, 2001 319 It's a bit vague exactly which C we should use for this oclose call. If we  simonpj committed Jan 25, 2001 320 321 322 323 324 325 326 327 328 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 329 then c is a "bubble"; there's no way it can ever improve, and it's  simonpj committed Jan 25, 2001 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 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 348 The definitely-ambiguous can then float out, and get smashed at top level  simonpj committed Jan 25, 2001 349 350 351 (which squashes out the constants, like Eq (T a) above)  qrczak committed Jul 17, 2001 352  --------------------------------------  simonpj committed May 03, 2001 353  Notes on principal types  qrczak committed Jul 17, 2001 354  --------------------------------------  simonpj committed May 03, 2001 355 356 357  class C a where op :: a -> a  qrczak committed Jul 17, 2001 358   simonpj committed May 03, 2001 359 360 361 362 363 364 365  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 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395  -------------------------------------- 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 396  --------------------------------------  simonpj committed Jan 25, 2001 397  Notes on implicit parameters  qrczak committed Jul 17, 2001 398  --------------------------------------  simonpj committed Jan 25, 2001 399   simonpj@microsoft.com committed Nov 24, 2006 400 401 Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  simonpj committed May 03, 2001 402 403 404 Consider this: f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 405   simonpj committed May 03, 2001 406 407 408 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 409   simonpj committed May 03, 2001 410 411 412  f :: Int -> Int (so we get ?y from the context of f's definition), or  simonpj committed Jan 25, 2001 413 414 415  f :: (?y::Int) => Int -> Int  simonpj committed May 03, 2001 416 417 418 419 420 421 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 422 423 BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring.  simonpj committed Jun 25, 2001 424   simonpj committed Oct 25, 2001 425   simonpj@microsoft.com committed Nov 24, 2006 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 Note [Implicit parameters and ambiguity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ What type should we infer for this? f x = (show ?y, x::Int) Since we must quantify over the ?y, the most plausible type is f :: (Show a, ?y::a) => Int -> (String, Int) But notice that the type of the RHS is (String,Int), with no type varibables mentioned at all! The type of f looks ambiguous. But it isn't, because at a call site we might have let ?y = 5::Int in f 7 and all is well. In effect, implicit parameters are, well, parameters, so we can take their type variables into account as part of the "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.  simonpj committed Oct 25, 2001 441 442 443 444 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 445 446 447 448 449 450 451 452 453 454 455  (?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 456   simonpj committed Oct 25, 2001 457 458 459 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 460   simonpj committed Jan 25, 2001 461  f :: Int -> Int  simonpj committed May 03, 2001 462  f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 463   simonpj committed May 03, 2001 464 At first sight this seems reasonable, but it has the nasty property  simonpj committed Jul 12, 2001 465 that adding a type signature changes the dynamic semantics.  simonpj committed May 03, 2001 466 Consider this:  simonpj committed Jan 25, 2001 467   simonpj committed May 03, 2001 468  (let f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 469 470 471 472  in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+5) vs  simonpj committed Jul 12, 2001 473  (let f :: Int -> Int  simonpj committed May 03, 2001 474  f x = x + ?y  simonpj committed Jan 25, 2001 475 476 477 478  in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+6)  simonpj committed May 03, 2001 479 480 Indeed, simply inlining f (at the Haskell source level) would change the dynamic semantics.  simonpj committed Jan 25, 2001 481   simonpj committed Oct 25, 2001 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 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 509   simonpj committed Apr 30, 2001 510   simonpj committed May 03, 2001 511 512 513 Question 3: monomorphism ~~~~~~~~~~~~~~~~~~~~~~~~ There's a nasty corner case when the monomorphism restriction bites:  simonpj committed Apr 30, 2001 514   simonpj committed May 03, 2001 515 516  z = (x::Int) + ?y  simonpj committed Jul 12, 2001 517 518 The argument above suggests that we *must* generalise over the ?y parameter, to get  simonpj committed May 03, 2001 519 520  z :: (?y::Int) => Int, but the monomorphism restriction says that we *must not*, giving  qrczak committed Jul 17, 2001 521  z :: Int.  simonpj committed May 03, 2001 522 523 524 525 526 527 528 529 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 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 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 545 546 547 548 549 550 551 552  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 553  * Inlining remains valid  simonpj committed May 03, 2001 554 555 556 557 558 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  * 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 591   simonpj committed May 03, 2001 592 It's really not clear what is the Right Thing To Do. If you see  simonpj committed Jan 25, 2001 593   simonpj committed May 03, 2001 594  z = (x::Int) + ?y  simonpj committed Jan 25, 2001 595   simonpj committed May 03, 2001 596 597 598 599 600 601 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 602   simonpj committed May 03, 2001 603 Choice (C) really says "the monomorphism restriction doesn't apply  simonpj committed Jul 12, 2001 604 to implicit parameters". Which is fine, but remember that every  simonpj committed May 03, 2001 605 606 607 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 608 clauses that bind ?y, so a decent compiler should common up all  simonpj committed May 03, 2001 609 610 611 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 612   simonpj committed May 03, 2001 613 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted  simonpj committed Jan 25, 2001 614   qrczak committed Jul 17, 2001 615   simonpj committed May 03, 2001 616   simonpj committed Jan 25, 2001 617 618 619 620 621 622 623 624 625 %************************************************************************ %* * \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 626 627  2. Partition C based on Q into Ct and Cq. Notice that ambiguous  simonpj committed Jan 25, 2001 628  predicates will end up in Ct; we deal with them at the top level  qrczak committed Jul 17, 2001 629   simonpj committed Jan 25, 2001 630  3. Try improvement, using functional dependencies  qrczak committed Jul 17, 2001 631   simonpj committed Jan 25, 2001 632 633 634 635  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 636 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different  simonpj committed Jan 25, 2001 637 638 639 640 641 642 643 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 644   simonpj committed Jan 25, 2001 645 646 647 648 649 650 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 651 again.  simonpj committed Jan 25, 2001 652   partain committed Jan 08, 1996 653 654  \begin{code}  simonpj committed Jan 25, 2001 655 tcSimplifyInfer  qrczak committed Jul 17, 2001 656 657  :: SDoc -> TcTyVarSet -- fv(T); type vars  simonpj committed Sep 13, 2002 658  -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 12, 2006 659  -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)  simonpj@microsoft.com committed Dec 11, 2006 660 661  [Inst], -- Dict Ids that must be bound here (zonked) TcDictBinds) -- Bindings  simonpj committed Sep 13, 2002 662  -- Any free (escaping) Insts are tossed into the environment  simonpj committed Jan 25, 2001 663 \end{code}  simonm committed Dec 02, 1998 664   simonpj committed Jan 25, 2001 665 666  \begin{code}  simonpj@microsoft.com committed Dec 11, 2006 667 668 669 tcSimplifyInfer doc tau_tvs wanted = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars  simonpj@microsoft.com committed Nov 23, 2006 670  ; gbl_tvs <- tcGetGlobalTyVars  simonpj@microsoft.com committed Dec 11, 2006 671  ; let preds = fdPredsOfInsts wanted'  simonpj@microsoft.com committed Nov 23, 2006 672  qtvs = grow preds tau_tvs' minusVarSet oclose preds gbl_tvs  simonpj@microsoft.com committed Dec 11, 2006 673 674 675  (free, bound) = partition (isFreeWhenInferring qtvs) wanted' ; traceTc (text "infer" <+> (ppr preds $$ppr (grow preds tau_tvs')$$ ppr gbl_tvs $$ppr (oclose preds gbl_tvs)$$ ppr free  ppr bound)) ; extendLIEs free  simonpj@microsoft.com committed Nov 23, 2006 676   simonpj@microsoft.com committed Dec 11, 2006 677  -- To make types simple, reduce as much as possible  simonpj@microsoft.com committed Nov 23, 2006 678  ; let try_me inst = ReduceMe AddSCs  simonpj@microsoft.com committed Dec 11, 2006 679  ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound  simonpj@microsoft.com committed Nov 23, 2006 680   simonpj@microsoft.com committed Dec 11, 2006 681 682 683 684 685 686 687 688  ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs) -- We can't abstract over implications ; let (dicts, implics) = partition isDict irreds ; loc <- getInstLoc (ImplicOrigin doc) ; implic_bind <- bindIrreds loc qtvs' dicts implics ; return (qtvs', dicts, binds unionBags implic_bind) }  simonpj@microsoft.com committed Nov 23, 2006 689 690  -- NB: when we are done, we might have some bindings, but -- the final qtvs might be empty. See Note [NO TYVARS] below.  qrczak committed Jul 17, 2001 691 \end{code}  simonpj committed Mar 19, 1998 692   simonpj@microsoft.com committed Dec 11, 2006 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 \begin{code} ----------------------------------------------------------- -- 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 :: InstLoc -> TcTyVarSet -- fv(T) -> [Inst] -- Given -> [Inst] -- Wanted -> TcM ([TyVar], -- Fully zonked, and quantified TcDictBinds) -- Bindings tcSimplifyInferCheck loc tau_tvs givens wanteds = do { (irreds, binds) <- innerCheckLoop loc givens wanteds -- 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. ; let all_tvs = varSetElems (tau_tvs unionVarSet tyVarsOfInsts givens) ; all_tvs <- zonkTcTyVarsAndFV all_tvs ; gbl_tvs <- tcGetGlobalTyVars ; let qtvs = varSetElems (all_tvs minusVarSet gbl_tvs) -- We could close gbl_tvs, but its not necessary for -- soundness, and it'll only affect which tyvars, not which -- dictionaries, we quantify over ; qtvs' <- zonkQuantifiedTyVars qtvs -- Now we are back to normal (c.f. tcSimplCheck) ; implic_bind <- bindIrreds loc qtvs' givens irreds ; return (qtvs', binds unionBags implic_bind) } \end{code}  simonpj@microsoft.com committed Nov 23, 2006 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 Note [Squashing methods] ~~~~~~~~~~~~~~~~~~~~~~~~~ Be careful if you want to float methods more: truncate :: forall a. RealFrac a => forall b. Integral b => a -> b From an application (truncate f i) we get t1 = truncate at f t2 = t1 at i If we have also have a second occurrence of truncate, we get t3 = truncate at f t4 = t3 at i When simplifying with i,f free, we might still notice that t1=t3; but alas, the binding for t2 (which mentions t1) may continue to float out! Note [NO TYVARS] ~~~~~~~~~~~~~~~~~  simonpj committed Oct 17, 2001 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767  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 768 769 770 polymorphic in. The net effect of [NO TYVARS]  simonpj committed Oct 17, 2001 771   simonpj committed Jan 25, 2001 772 \begin{code}  simonpj committed Oct 25, 2001 773 774 isFreeWhenInferring :: TyVarSet -> Inst -> Bool isFreeWhenInferring qtvs inst  simonpj@microsoft.com committed Nov 24, 2006 775 776 777  = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars && isInheritableInst inst -- and no implicit parameter involved -- see Note [Inheriting implicit parameters]  simonpj committed Oct 25, 2001 778   simonpj@microsoft.com committed Nov 10, 2006 779 {- No longer used (with implication constraints)  simonpj committed Oct 25, 2001 780 781 782 783 784 785 isFreeWhenChecking :: TyVarSet -- Quantified tyvars -> NameSet -- Quantified implicit parameters -> Inst -> Bool isFreeWhenChecking qtvs ips inst = isFreeWrtTyVars qtvs inst && isFreeWrtIPs ips inst  simonpj@microsoft.com committed Nov 10, 2006 786 -}  simonpj committed Oct 25, 2001 787   simonpj@microsoft.com committed Sep 23, 2006 788 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst disjointVarSet qtvs  simonpj committed Oct 25, 2001 789 isFreeWrtIPs ips inst = not (any (elemNameSet ips) (ipNamesOfInst inst))  simonpj committed Jan 25, 2001 790 \end{code}  simonpj committed Mar 19, 1998 791   simonpj committed Feb 10, 1998 792   simonpj committed Jan 25, 2001 793 794 795 796 797 %************************************************************************ %* * \subsection{tcSimplifyCheck} %* * %************************************************************************  partain committed Mar 19, 1996 798   simonpj committed Jan 25, 2001 799 @tcSimplifyCheck@ is used when we know exactly the set of variables  simonpj committed Feb 20, 2001 800 we are going to quantify over. For example, a class or instance declaration.  partain committed Jan 08, 1996 801 802  \begin{code}  simonpj@microsoft.com committed Nov 10, 2006 803 -----------------------------------------------------------  simonpj committed Oct 25, 2001 804 -- tcSimplifyCheck is used when checking expression type signatures,  simonpj committed Jun 25, 2001 805 -- class decls, instance decls etc.  simonpj@microsoft.com committed Nov 10, 2006 806 807 808 809 810 811 tcSimplifyCheck :: InstLoc -> [TcTyVar] -- Quantify over these -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings tcSimplifyCheck loc qtvs givens wanteds  simonpj@microsoft.com committed Dec 11, 2006 812 813 814  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) do { (irreds, binds) <- innerCheckLoop loc givens wanteds ; implic_bind <- bindIrreds loc qtvs givens irreds  simonpj@microsoft.com committed Nov 10, 2006 815 816 817 818 819 820 821 822 823 824 825  ; return (binds unionBags implic_bind) } ----------------------------------------------------------- -- tcSimplifyCheckPat is used for existential pattern match tcSimplifyCheckPat :: InstLoc -> [CoVar] -> Refinement -> [TcTyVar] -- Quantify over these -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds  simonpj@microsoft.com committed Dec 11, 2006 826 827 828 829  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) do { (irreds, binds) <- innerCheckLoop loc givens wanteds ; implic_bind <- bindIrredsR loc qtvs co_vars reft givens irreds  simonpj@microsoft.com committed Nov 10, 2006 830 831 832  ; return (binds unionBags implic_bind) } -----------------------------------------------------------  simonpj@microsoft.com committed Dec 11, 2006 833 834 835 836 837 838 839 840 841 bindIrreds :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds bindIrreds loc qtvs givens irreds = bindIrredsR loc qtvs [] emptyRefinement givens irreds bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar] -> Refinement -> [Inst] -> [Inst] -> TcM TcDictBinds  simonpj@microsoft.com committed Nov 10, 2006 842 843 -- Make a binding that binds 'irreds', by generating an implication -- constraint for them, *and* throwing the constraint into the LIE  simonpj@microsoft.com committed Dec 11, 2006 844 845 846 847 bindIrredsR loc qtvs co_vars reft givens irreds | null irreds = return emptyBag | otherwise  simonpj@microsoft.com committed Nov 10, 2006 848 849  = do { let givens' = filter isDict givens -- The givens can include methods  simonpj@microsoft.com committed Dec 11, 2006 850  -- See Note [Pruning the givens in an implication constraint]  simonpj@microsoft.com committed Nov 10, 2006 851   simonpj@microsoft.com committed Jan 09, 2007 852 853  -- If there are no 'givens' *and* the refinement is empty -- (the refinement is like more givens), then it's safe to  simonpj@microsoft.com committed Nov 10, 2006 854 855  -- partition the 'wanteds' by their qtvs, thereby trimming irreds -- See Note [Freeness and implications]  simonpj@microsoft.com committed Jan 09, 2007 856  ; irreds' <- if null givens' && isEmptyRefinement reft  simonpj@microsoft.com committed Nov 22, 2006 857 858 859 860 861 862 863 864 865  then do { let qtv_set = mkVarSet qtvs (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds ; extendLIEs frees ; return real_irreds } else return irreds ; let all_tvs = qtvs ++ co_vars -- Abstract over all these ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'  simonpj@microsoft.com committed Feb 02, 2007 866 867  -- This call does the real work -- If irreds' is empty, it does something sensible  simonpj@microsoft.com committed Nov 22, 2006 868 869  ; extendLIEs implics ; return bind }  simonpj@microsoft.com committed Nov 10, 2006 870 871   simonpj@microsoft.com committed Nov 22, 2006 872 873 874 875 876 877 878 879 makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -> [Inst] -> [Inst] -> TcM ([Inst], TcDictBinds) -- Make a binding that binds 'irreds', by generating an implication -- constraint for them, *and* throwing the constraint into the LIE -- The binding looks like -- (ir1, .., irn) = f qtvs givens -- where f is (evidence for) the new implication constraint  simonpj@microsoft.com committed Feb 02, 2007 880 881 -- f :: forall qtvs. {reft} givens => (ir1, .., irn) -- qtvs includes coercion variables  simonpj@microsoft.com committed Nov 22, 2006 882 883 884 885 886 887 888 889 890 -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs reft givens -- Guaranteed all Dicts irreds | null irreds -- If there are no irreds, we are done = return ([], emptyBag) | otherwise -- Otherwise we must generate a binding = do { uniq <- newUnique  simonpj@microsoft.com committed Nov 10, 2006 891  ; span <- getSrcSpanM  simonpj@microsoft.com committed Nov 22, 2006 892  ; let name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)  simonpj@microsoft.com committed Nov 10, 2006 893 894  implic_inst = ImplicInst { tci_name = name, tci_reft = reft, tci_tyvars = all_tvs,  simonpj@microsoft.com committed Nov 22, 2006 895  tci_given = givens,  simonpj@microsoft.com committed Nov 10, 2006 896 897 898 899 900 901 902  tci_wanted = irreds, tci_loc = loc } ; let n_irreds = length irreds irred_ids = map instToId irreds tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids) pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))  simonpj@microsoft.com committed Nov 22, 2006 903  co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)  simonpj@microsoft.com committed Nov 10, 2006 904 905 906 907 908 909  bind | n_irreds==1 = VarBind (head irred_ids) rhs | otherwise = PatBind { pat_lhs = L span pat, pat_rhs = unguardedGRHSs rhs, pat_rhs_ty = tup_ty, bind_fvs = placeHolderNames } ; -- pprTrace "Make implic inst" (ppr implic_inst) $ simonpj@microsoft.com committed Nov 22, 2006 910  return ([implic_inst], unitBag (L span bind)) }  simonpj@microsoft.com committed Nov 10, 2006 911 912 913 914  ----------------------------------------------------------- topCheckLoop :: SDoc -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 11, 2006 915  -> TcM ([Inst], TcDictBinds)  simonpj@microsoft.com committed Nov 10, 2006 916 917 918  topCheckLoop doc wanteds = checkLoop (mkRedEnv doc try_me []) wanteds  simonpj committed Jun 25, 2001 919  where  simonpj@microsoft.com committed Nov 10, 2006 920 921 922  try_me inst = ReduceMe AddSCs -----------------------------------------------------------  simonpj@microsoft.com committed Nov 23, 2006 923 innerCheckLoop :: InstLoc  simonpj@microsoft.com committed Nov 10, 2006 924 925  -> [Inst] -- Given -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 11, 2006 926  -> TcM ([Inst], TcDictBinds)  simonpj@microsoft.com committed Nov 10, 2006 927   simonpj@microsoft.com committed Nov 23, 2006 928 innerCheckLoop inst_loc givens wanteds  simonpj@microsoft.com committed Nov 10, 2006 929 930 931 932  = checkLoop env wanteds where env = mkRedEnv (pprInstLoc inst_loc) try_me givens  simonpj@microsoft.com committed Nov 23, 2006 933 934  try_me inst | isMethodOrLit inst = ReduceMe AddSCs | otherwise = Stop  simonpj@microsoft.com committed Nov 10, 2006 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966  -- When checking against a given signature -- we MUST be very gentle: Note [Check gently] \end{code} Note [Check gently] ~~~~~~~~~~~~~~~~~~~~ We have to very careful about not simplifying too vigorously Example: data T a where MkT :: a -> T [a] f :: Show b => T b -> b f (MkT x) = show [x] Inside the pattern match, which binds (a:*, x:a), we know that b ~ [a] Hence we have a dictionary for Show [a] available; and indeed we need it. We are going to build an implication contraint forall a. (b~[a]) => Show [a] Later, we will solve this constraint using the knowledge (Show b) But we MUST NOT reduce (Show [a]) to (Show a), else the whole thing becomes insoluble. So we simplify gently (get rid of literals and methods only, plus common up equal things), deferring the real work until top level, when we solve the implication constraint with topCheckLooop. \begin{code} ----------------------------------------------------------- checkLoop :: RedEnv -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 11, 2006 967 968  -> TcM ([Inst], TcDictBinds) -- Precondition: givens are completely rigid  simonpj@microsoft.com committed Nov 10, 2006 969 970 971 972 973  checkLoop env wanteds = do { -- Givens are skolems, so no need to zonk them wanteds' <- mappM zonkInst wanteds  simonpj@microsoft.com committed Nov 23, 2006 974  ; (improved, binds, irreds) <- reduceContext env wanteds'  simonpj@microsoft.com committed Nov 10, 2006 975   simonpj@microsoft.com committed Nov 23, 2006 976  ; if not improved then  simonpj@microsoft.com committed Dec 11, 2006 977  return (irreds, binds)  simonpj@microsoft.com committed Nov 10, 2006 978 979  else do  simonpj@microsoft.com committed Nov 23, 2006 980 981 982 983 984  -- If improvement did some unification, we go round again. -- 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 Note [LOOP]  simonpj@microsoft.com committed Dec 11, 2006 985 986  { (irreds1, binds1) <- checkLoop env irreds ; return (irreds1, binds unionBags binds1) } }  simonpj@microsoft.com committed Nov 10, 2006 987 \end{code}  simonpj committed Jun 25, 2001 988   simonpj@microsoft.com committed Nov 23, 2006 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 Note [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) and improve by binding l->T, after which we can do some reduction on both the Lte and If constraints. What we *can't* do is start again with (Max Z (S x) y)!  simonpj committed Jun 25, 2001 1006   simonpj committed Jan 25, 2001 1007   simonpj committed Mar 09, 2005 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 %************************************************************************ %* * 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}  simonpj@microsoft.com committed Nov 10, 2006 1053 1054 1055 1056 1057 1058 tcSimplifySuperClasses :: InstLoc -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds tcSimplifySuperClasses loc givens sc_wanteds  simonpj@microsoft.com committed Dec 11, 2006 1059  = do { (irreds, binds1) <- checkLoop env sc_wanteds  simonpj@microsoft.com committed Nov 10, 2006 1060 1061 1062  ; let (tidy_env, tidy_irreds) = tidyInsts irreds ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds ; return binds1 }  simonpj committed Mar 09, 2005 1063  where  simonpj@microsoft.com committed Nov 10, 2006 1064 1065 1066  env = mkRedEnv (pprInstLoc loc) try_me givens try_me inst = ReduceMe NoSCs -- Like topCheckLoop, but with NoSCs  simonpj committed Mar 09, 2005 1067 1068 1069 \end{code}  simonpj committed May 03, 2001 1070 1071 1072 1073 1074 1075 %************************************************************************ %* * \subsection{tcSimplifyRestricted} %* * %************************************************************************  simonpj committed Mar 11, 2004 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 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 1119 1120  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 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132  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 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 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 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168  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 1169   simonpj committed May 03, 2001 1170 1171 \begin{code} tcSimplifyRestricted -- Used for restricted binding groups  simonpj committed Jun 25, 2001 1172  -- i.e. ones subject to the monomorphism restriction  qrczak committed Jul 17, 2001 1173  :: SDoc  simonpj committed Feb 04, 2005 1174 1175  -> TopLevelFlag -> [Name] -- Things bound in this group  simonpj committed Jun 25, 2001 1176  -> TcTyVarSet -- Free in the type of the RHSs  simonpj committed Sep 13, 2002 1177  -> [Inst] -- Free in the RHSs  simonpj@microsoft.com committed Dec 12, 2006 1178  -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)  simonpj committed May 03, 2001 1179  TcDictBinds) -- Bindings  simonpj committed Mar 11, 2004 1180 1181 1182  -- 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 1183   simonpj committed Feb 04, 2005 1184 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds  simonpj committed May 12, 2004 1185  -- Zonk everything in sight  simonpj@microsoft.com committed Dec 11, 2006 1186  = do { wanteds' <- mappM zonkInst wanteds  simonpj committed May 12, 2004 1187   simonpj@microsoft.com committed Nov 22, 2006 1188  -- 'ReduceMe': Reduce as far as we can. Don't stop at  simonpj committed Apr 09, 2003 1189 1190 1191 1192  -- 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 1193 1194  -- -- BUT do no improvement! See Plan D above  1195 1196  -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint  simonpj@microsoft.com committed Dec 11, 2006 1197 1198  ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'  simonpj committed May 03, 2001 1199 1200  -- Next, figure out the tyvars we will quantify over  simonpj@microsoft.com committed Dec 11, 2006 1201 1202 1203 1204  ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) ; gbl_tvs' <- tcGetGlobalTyVars ; constrained_dicts' <- mappM zonkInst constrained_dicts  1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220  ; let qtvs1 = tau_tvs' minusVarSet oclose (fdPredsOfInsts constrained_dicts) gbl_tvs' -- As in tcSimplifyInfer -- Do not quantify over constrained type variables: -- this is the monomorphism restriction constrained_tvs' = tyVarsOfInsts constrained_dicts' qtvs = qtvs1 minusVarSet constrained_tvs' pp_bndrs = pprWithCommas (quotes . ppr) bndrs -- Warn in the mono ; warn_mono <- doptM Opt_WarnMonomorphism ; warnTc (warn_mono && (constrained_tvs' intersectsVarSet qtvs1)) (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding") <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs, ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])  simonpj@microsoft.com committed Dec 11, 2006 1221  ; traceTc (text "tcSimplifyRestricted" <+> vcat [  simonpj@microsoft.com committed Nov 23, 2006 1222  pprInsts wanteds, pprInsts constrained_dicts',  simonpj committed May 12, 2004 1223  ppr _binds,  simonpj@microsoft.com committed Dec 11, 2006 1224  ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])  simonpj committed May 03, 2001 1225   simonpj committed May 12, 2004 1226 1227 1228 1229  -- 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. --  simonpj@microsoft.com committed Nov 23, 2006 1230  -- We quantify only over constraints that are captured by qtvs;  simonpj committed May 12, 2004 1231 1232 1233 1234 1235 1236 1237 1238  -- 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 1239 1240 1241  -- -- At top level, we *do* squash methods becuase we want to -- expose implicit parameters to the test that follows  simonpj@microsoft.com committed Dec 11, 2006 1242 1243 1244 1245 1246 1247  ; let is_nested_group = isNotTopLevel top_lvl try_me inst | isFreeWrtTyVars qtvs inst, (is_nested_group || isDict inst) = Stop | otherwise = ReduceMe AddSCs env = mkNoImproveRedEnv doc try_me ; (_imp, binds, irreds) <- reduceContext env wanteds'  simonpj committed Feb 04, 2005 1248 1249  -- See "Notes on implicit parameters, Question 4: top level"  simonpj@microsoft.com committed Dec 11, 2006 1250 1251 1252 1253 1254 1255 1256 1257 1258  ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured if is_nested_group then extendLIEs irreds else do { let (bad_ips, non_ips) = partition isIPDict irreds ; addTopIPErrs bndrs bad_ips ; extendLIEs non_ips } ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs) ; return (qtvs', binds) }  simonpj committed May 03, 2001 1259 1260 \end{code}  simonpj committed Jan 25, 2001 1261 1262 1263  %************************************************************************ %* *  simonpj@microsoft.com committed May 19, 2006 1264  tcSimplifyRuleLhs  simonpj committed Jan 25, 2001 1265 1266 1267 %* * %************************************************************************  simonpj committed May 18, 1999 1268 1269 1270 1271 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 1272 1273 1274 Example. Consider the following left-hand side of a rule f (x == y) (y > z) = ...  qrczak committed Jul 17, 2001 1275   simonpj@microsoft.com committed May 19, 2006 1276 If we typecheck this expression we get constraints  simonpj committed Jun 28, 1999 1277   simonpj@microsoft.com committed May 19, 2006 1278  d1 :: Ord a, d2 :: Eq a  simonpj committed Jun 28, 1999 1279   simonpj@microsoft.com committed May 19, 2006 1280 We do NOT want to "simplify" to the LHS  simonpj committed Jun 28, 1999 1281   simonpj@microsoft.com committed May 19, 2006 1282 1283  forall x::a, y::a, z::a, d1::Ord a. f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...  simonpj committed Jun 28, 1999 1284   simonpj@microsoft.com committed May 19, 2006 1285 Instead we want  simonpj committed Jun 28, 1999 1286   simonpj@microsoft.com committed May 19, 2006 1287 1288  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 1289   simonpj@microsoft.com committed May 19, 2006