TcSimplify.lhs 107 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}  Ian Lynagh committed Sep 03, 2007 9 {-# OPTIONS -w #-}  Ian Lynagh committed Sep 01, 2007 10 11 12 -- The above warning supression flag is a temporary kludge. -- While working on this module you are encouraged to remove it and fix -- any warnings in the module. See  Ian Lynagh committed Sep 04, 2007 13 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings  Ian Lynagh committed Sep 01, 2007 14 15 -- for details  partain committed Jan 08, 1996 16 module TcSimplify (  qrczak committed Jul 17, 2001 17  tcSimplifyInfer, tcSimplifyInferCheck,  simonpj committed Jun 25, 2001 18  tcSimplifyCheck, tcSimplifyRestricted,  simonpj@microsoft.com committed May 19, 2006 19  tcSimplifyRuleLhs, tcSimplifyIPs,  simonpj committed Mar 09, 2005 20  tcSimplifySuperClasses,  simonpj committed Jul 09, 2003 21  tcSimplifyTop, tcSimplifyInteractive,  simonpj@microsoft.com committed Nov 10, 2006 22  tcSimplifyBracket, tcSimplifyCheckPat,  simonpj committed Mar 13, 2001 23   simonpj committed Dec 28, 2001 24  tcSimplifyDeriv, tcSimplifyDefault,  simonpj@microsoft.com committed Oct 27, 2007 25  bindInstsOfLocalFuns,  chak@cse.unsw.edu.au. committed Aug 28, 2007 26 27  misMatchMsg  partain committed Jan 08, 1996 28 29  ) where  simonm committed Jan 08, 1998 30 #include "HsVersions.h"  partain committed Mar 19, 1996 31   simonpj@microsoft.com committed Jan 25, 2006 32 import {-# SOURCE #-} TcUnify( unifyType )  Simon Marlow committed Oct 11, 2006 33 import HsSyn  partain committed Mar 19, 1996 34   simonpj committed Sep 13, 2002 35 import TcRnMonad  Simon Marlow committed Oct 11, 2006 36 37 38 39 import Inst import TcEnv import InstEnv import TcType  simonpj@microsoft.com committed Jan 02, 2007 40 import TcMType  Simon Marlow committed Oct 11, 2006 41 import TcIface  chak@cse.unsw.edu.au. committed Aug 28, 2007 42 43 import TcTyFuns import TypeRep  Simon Marlow committed Oct 11, 2006 44 45 46 47 48 49 50 51 52 53 54 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 55 import VarSet  Simon Marlow committed Oct 11, 2006 56 import VarEnv  chak@cse.unsw.edu.au. committed Aug 28, 2007 57 import Module  simonm committed Jan 08, 1998 58 import FiniteMap  simonmar committed Dec 10, 2003 59 import Bag  simonm committed Jan 08, 1998 60 import Outputable  simonpj@microsoft.com committed Jul 04, 2007 61 import Maybes  Simon Marlow committed Oct 11, 2006 62 63 import ListSetOps import Util  chak@cse.unsw.edu.au. committed Aug 28, 2007 64 import UniqSet  Simon Marlow committed Oct 11, 2006 65 66 67 import SrcLoc import DynFlags  Ian Lynagh committed Mar 29, 2008 68 import Control.Monad  Simon Marlow committed Oct 11, 2006 69 import Data.List  partain committed Jan 08, 1996 70 71 72 73 74 \end{code} %************************************************************************ %* *  simonpj committed Jan 25, 2001 75 \subsection{NOTES}  partain committed Jan 08, 1996 76 77 78 %* * %************************************************************************  simonpj committed Feb 10, 2004 79 80 81 82  -------------------------------------- Notes on functional dependencies (a bug) --------------------------------------  simonpj@microsoft.com committed Sep 18, 2006 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 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 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 137 138 139 140 141 142 143 144 145 146 147 148 | > 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.  simonpj@microsoft.com committed Jun 29, 2007 149 150 151 Note [Choosing which variables to quantify] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we are about to do a generalisation step. We have in our hand  simonpj committed Jan 25, 2001 152 153 154  G the environment T the type of the RHS  qrczak committed Jan 26, 2001 155  C the constraints from that RHS  simonpj committed Jan 25, 2001 156 157 158 159 160 161 162 163 164 165 166  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 167 and float the constraints Ct further outwards.  simonpj committed Jan 25, 2001 168 169 170 171 172 173  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  simonpj@microsoft.com committed Jun 29, 2007 174 175 176 177 178 179  (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.  simonpj committed Jan 25, 2001 180 181 182 183 184 185 186 187 188 189 190 191 192  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}  simonpj@microsoft.com committed Jun 29, 2007 193 194 195 196 197 In particular, it's perfectly OK to quantify over more type variables than strictly necessary; there is no need to quantify over 'b', since it is determined by 'a' which is free in the envt, but it's perfectly OK to do so. However we must not quantify over 'a' itself.  simonpj committed Jan 25, 2001 198 199 Other things being equal, however, we'd like to quantify over as few variables as possible: smaller types, fewer type applications, more  simonpj@microsoft.com committed Jun 29, 2007 200 201 constraints can get into Ct instead of Cq. Here's a good way to choose Q:  simonpj committed Jan 25, 2001 202 203 204 205 206 207 208 209 210 211 212  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 213   simonpj committed Jan 25, 2001 214 215 216 217 218 219 220  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 221  And then if the fn was called at several different c's, each of  simonpj committed Jan 25, 2001 222 223 224 225 226 227 228 229 230 231 232 233 234  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))  simonpj@microsoft.com committed Jun 29, 2007 235 236 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.  simonpj committed Jan 25, 2001 237 238 239 240 241 242 243  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 244 245 246 ------------------------------------- Note [Ambiguity] -------------------------------------  simonpj committed Jan 25, 2001 247 248 249 250 251 252 253 254 255 256 257 258 259 260 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  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 286 So here's the plan. We WARN about probable ambiguity if  simonpj committed Jan 25, 2001 287 288 289 290 291  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 292 in the environment, or by the variables in the type.  simonpj committed Jan 25, 2001 293 294 295  Notice that we union before calling oclose. Here's an example:  qrczak committed Jan 26, 2001 296  class J a b c | a b -> c  simonpj committed Jan 25, 2001 297 298 299  fv(G) = {a} Is this ambiguous?  qrczak committed Jan 26, 2001 300  forall b c. (J a b c) => b -> b  simonpj committed Jan 25, 2001 301 302  Only if we union {a} from G with {b} from T before using oclose,  qrczak committed Jul 17, 2001 303 do we see that c is fixed.  simonpj committed Jan 25, 2001 304   qrczak committed Jul 17, 2001 305 It's a bit vague exactly which C we should use for this oclose call. If we  simonpj committed Jan 25, 2001 306 307 308 309 310 311 312 313 314 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 315 then c is a "bubble"; there's no way it can ever improve, and it's  simonpj committed Jan 25, 2001 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 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 334 The definitely-ambiguous can then float out, and get smashed at top level  simonpj committed Jan 25, 2001 335 336 337 (which squashes out the constants, like Eq (T a) above)  qrczak committed Jul 17, 2001 338  --------------------------------------  simonpj committed May 03, 2001 339  Notes on principal types  qrczak committed Jul 17, 2001 340  --------------------------------------  simonpj committed May 03, 2001 341 342 343  class C a where op :: a -> a  qrczak committed Jul 17, 2001 344   simonpj committed May 03, 2001 345 346 347 348 349 350 351  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 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381  -------------------------------------- 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 382  --------------------------------------  simonpj committed Jan 25, 2001 383  Notes on implicit parameters  qrczak committed Jul 17, 2001 384  --------------------------------------  simonpj committed Jan 25, 2001 385   simonpj@microsoft.com committed Nov 24, 2006 386 387 Note [Inheriting implicit parameters] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  simonpj committed May 03, 2001 388 389 390 Consider this: f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 391   simonpj committed May 03, 2001 392 393 394 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 395   simonpj committed May 03, 2001 396 397 398  f :: Int -> Int (so we get ?y from the context of f's definition), or  simonpj committed Jan 25, 2001 399 400 401  f :: (?y::Int) => Int -> Int  simonpj committed May 03, 2001 402 403 404 405 406 407 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 408 409 BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring.  simonpj committed Jun 25, 2001 410   simonpj committed Oct 25, 2001 411   simonpj@microsoft.com committed Nov 24, 2006 412 413 Note [Implicit parameters and ambiguity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  simonpj@microsoft.com committed Sep 11, 2007 414 415 416 417 418 419 420 421 422 423 424 425 426 Only a *class* predicate can give rise to ambiguity An *implicit parameter* cannot. For example: foo :: (?x :: [a]) => Int foo = length ?x is fine. The call site will suppply a particular 'x' Furthermore, the type variables fixed by an implicit parameter propagate to the others. E.g. foo :: (Show a, ?x::[a]) => Int foo = show (?x++?x) The type of foo looks ambiguous. But it isn't, because at a call site we might have let ?x = 5::Int in foo  simonpj@microsoft.com committed Nov 24, 2006 427 428 429 430 431 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 432 433 434 435 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 436 437 438 439 440 441 442 443 444 445 446  (?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 447   simonpj committed Oct 25, 2001 448 449 450 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 451   simonpj committed Jan 25, 2001 452  f :: Int -> Int  simonpj committed May 03, 2001 453  f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 454   simonpj committed May 03, 2001 455 At first sight this seems reasonable, but it has the nasty property  simonpj committed Jul 12, 2001 456 that adding a type signature changes the dynamic semantics.  simonpj committed May 03, 2001 457 Consider this:  simonpj committed Jan 25, 2001 458   simonpj committed May 03, 2001 459  (let f x = (x::Int) + ?y  simonpj committed Jan 25, 2001 460 461 462 463  in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+5) vs  simonpj committed Jul 12, 2001 464  (let f :: Int -> Int  simonpj committed May 03, 2001 465  f x = x + ?y  simonpj committed Jan 25, 2001 466 467 468 469  in (f 3, f 3 with ?y=5)) with ?y = 6 returns (3+6, 3+6)  simonpj committed May 03, 2001 470 471 Indeed, simply inlining f (at the Haskell source level) would change the dynamic semantics.  simonpj committed Jan 25, 2001 472   simonpj committed Oct 25, 2001 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 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 500   simonpj committed Apr 30, 2001 501   simonpj committed May 03, 2001 502 503 504 Question 3: monomorphism ~~~~~~~~~~~~~~~~~~~~~~~~ There's a nasty corner case when the monomorphism restriction bites:  simonpj committed Apr 30, 2001 505   simonpj committed May 03, 2001 506 507  z = (x::Int) + ?y  simonpj committed Jul 12, 2001 508 509 The argument above suggests that we *must* generalise over the ?y parameter, to get  simonpj committed May 03, 2001 510 511  z :: (?y::Int) => Int, but the monomorphism restriction says that we *must not*, giving  qrczak committed Jul 17, 2001 512  z :: Int.  simonpj committed May 03, 2001 513 514 515 516 517 518 519 520 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 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 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 536 537 538 539 540 541 542 543  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 544  * Inlining remains valid  simonpj committed May 03, 2001 545 546 547 548 549 550 551 552 553 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  * 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 582   simonpj committed May 03, 2001 583 It's really not clear what is the Right Thing To Do. If you see  simonpj committed Jan 25, 2001 584   simonpj committed May 03, 2001 585  z = (x::Int) + ?y  simonpj committed Jan 25, 2001 586   simonpj committed May 03, 2001 587 588 589 590 591 592 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 593   simonpj committed May 03, 2001 594 Choice (C) really says "the monomorphism restriction doesn't apply  simonpj committed Jul 12, 2001 595 to implicit parameters". Which is fine, but remember that every  simonpj committed May 03, 2001 596 597 598 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 599 clauses that bind ?y, so a decent compiler should common up all  simonpj committed May 03, 2001 600 601 602 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 603   simonpj committed May 03, 2001 604 BOTTOM LINE: we choose (B) at present. See tcSimplifyRestricted  simonpj committed Jan 25, 2001 605   qrczak committed Jul 17, 2001 606   simonpj committed May 03, 2001 607   simonpj committed Jan 25, 2001 608 609 610 611 612 613 614 615 616 %************************************************************************ %* * \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 617 618  2. Partition C based on Q into Ct and Cq. Notice that ambiguous  simonpj committed Jan 25, 2001 619  predicates will end up in Ct; we deal with them at the top level  qrczak committed Jul 17, 2001 620   simonpj committed Jan 25, 2001 621  3. Try improvement, using functional dependencies  qrczak committed Jul 17, 2001 622   simonpj committed Jan 25, 2001 623 624 625 626  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 627 Eq (a,b), we don't simplify to (Eq a, Eq b). So Q won't be different  simonpj committed Jan 25, 2001 628 629 630 631 632 633 634 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 635   simonpj committed Jan 25, 2001 636 637 638 639 640 641 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 642 again.  simonpj committed Jan 25, 2001 643   partain committed Jan 08, 1996 644 645  \begin{code}  simonpj committed Jan 25, 2001 646 tcSimplifyInfer  qrczak committed Jul 17, 2001 647 648  :: SDoc -> TcTyVarSet -- fv(T); type vars  simonpj committed Sep 13, 2002 649  -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 12, 2006 650  -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)  simonpj@microsoft.com committed Dec 11, 2006 651 652  [Inst], -- Dict Ids that must be bound here (zonked) TcDictBinds) -- Bindings  simonpj committed Sep 13, 2002 653  -- Any free (escaping) Insts are tossed into the environment  simonpj committed Jan 25, 2001 654 \end{code}  simonm committed Dec 02, 1998 655   simonpj committed Jan 25, 2001 656 657  \begin{code}  simonpj@microsoft.com committed Dec 11, 2006 658 tcSimplifyInfer doc tau_tvs wanted  simonpj@microsoft.com committed Aug 01, 2007 659  = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)  twanvl committed Jan 17, 2008 660  ; wanted' <- mapM zonkInst wanted -- Zonk before deciding quantified tyvars  simonpj@microsoft.com committed Nov 23, 2006 661  ; gbl_tvs <- tcGetGlobalTyVars  simonpj@microsoft.com committed Aug 02, 2007 662 663 664  ; let preds1 = fdPredsOfInsts wanted' gbl_tvs1 = oclose preds1 gbl_tvs qtvs = grow preds1 tau_tvs1 minusVarSet gbl_tvs1  simonpj@microsoft.com committed May 30, 2007 665 666 667 668  -- See Note [Choosing which variables to quantify] -- To maximise sharing, remove from consideration any -- constraints that don't mention qtvs at all  simonpj@microsoft.com committed Aug 01, 2007 669 670  ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted' ; extendLIEs free  simonpj@microsoft.com committed Nov 23, 2006 671   simonpj@microsoft.com committed Dec 11, 2006 672  -- To make types simple, reduce as much as possible  simonpj@microsoft.com committed Aug 02, 2007 673 674  ; traceTc (text "infer" <+> (ppr preds1 $$ppr (grow preds1 tau_tvs1)$$ ppr gbl_tvs $$ppr gbl_tvs1$$ ppr free  ppr bound))  simonpj@microsoft.com committed Jun 20, 2007 675  ; (irreds1, binds1) <- tryHardCheckLoop doc bound  simonpj@microsoft.com committed Jun 19, 2007 676 677  -- Note [Inference and implication constraints]  simonpj@microsoft.com committed Jun 20, 2007 678 679  ; let want_dict d = tyVarsOfInst d intersectsVarSet qtvs ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1  simonpj@microsoft.com committed Jun 19, 2007 680   simonpj@microsoft.com committed Aug 01, 2007 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703  -- Now work out all over again which type variables to quantify, -- exactly in the same way as before, but starting from irreds2. Why? -- a) By now improvment may have taken place, and we must *not* -- quantify over any variable free in the environment -- tc137 (function h inside g) is an example -- -- b) Do not quantify over constraints that *now* do not -- mention quantified type variables, because they are -- simply ambiguous (or might be bound further out). Example: -- f :: Eq b => a -> (a, b) -- g x = fst (f x) -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta) -- We decide to quantify over 'alpha' alone, but free1 does not include f77 -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous) -- constraint (Eq beta), which we dump back into the free set -- See test tcfail181 -- -- c) irreds may contain type variables not previously mentioned, -- e.g. instance D a x => Foo [a] -- wanteds = Foo [a] -- Then after simplifying we'll get (D a x), and x is fresh -- We must quantify over x else it'll be totally unbound ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)  simonpj@microsoft.com committed Aug 02, 2007 704 705 706 707 708 709 710 711 712 713 714  ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1) -- Note that we start from gbl_tvs1 -- We use tcGetGlobalTyVars, then oclose wrt preds2, because -- we've already put some of the original preds1 into frees -- E.g. wanteds = C a b (where a->b) -- gbl_tvs = {a} -- tau_tvs = {b} -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and -- irreds2 will be empty. But we don't want to generalise over b! ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked qtvs = grow preds2 tau_tvs2 minusVarSet oclose preds2 gbl_tvs2  simonpj@microsoft.com committed Aug 01, 2007 715 716 717 718 719 720  ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2 ; extendLIEs free -- Turn the quantified meta-type variables into real type variables ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)  simonpj@microsoft.com committed Jun 19, 2007 721 722  -- We can't abstract over any remaining unsolved -- implications so instead just float them outwards. Ugh.  chak@cse.unsw.edu.au. committed Aug 28, 2007 723  ; let (q_dicts0, implics) = partition isAbstractableInst irreds3  simonpj@microsoft.com committed Dec 11, 2006 724  ; loc <- getInstLoc (ImplicOrigin doc)  chak@cse.unsw.edu.au. committed Aug 28, 2007 725 726 727 728  ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics -- Prepare equality instances for quantification ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0  twanvl committed Jan 17, 2008 729  ; q_eqs <- mapM finalizeEqInst q_eqs0  simonpj@microsoft.com committed Dec 11, 2006 730   chak@cse.unsw.edu.au. committed Aug 28, 2007 731  ; return (qtvs2, q_eqs ++ q_dicts, binds1 unionBags binds2 unionBags implic_bind) }  simonpj@microsoft.com committed Nov 23, 2006 732 733  -- NB: when we are done, we might have some bindings, but -- the final qtvs might be empty. See Note [NO TYVARS] below.  simonpj@microsoft.com committed Jun 19, 2007 734   simonpj@microsoft.com committed Jun 20, 2007 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds) -- Note [Inference and implication constraints] -- Given a bunch of Dict and ImplicInsts, try to approximate the implications by -- - fetching any dicts inside them that are free -- - using those dicts as cruder constraints, to solve the implications -- - returning the extra ones too approximateImplications doc want_dict irreds | null extra_dicts = return (irreds, emptyBag) | otherwise = do { extra_dicts' <- mapM cloneDict extra_dicts ; tryHardCheckLoop doc (extra_dicts' ++ irreds) } -- By adding extra_dicts', we make them -- available to solve the implication constraints where extra_dicts = get_dicts (filter isImplicInst irreds) get_dicts :: [Inst] -> [Inst] -- Returns only Dicts -- Find the wanted constraints in implication constraints that satisfy -- want_dict, and are not bound by forall's in the constraint itself get_dicts ds = concatMap get_dict ds get_dict d@(Dict {}) | want_dict d = [d] | otherwise = [] get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})  simonpj@microsoft.com committed Jun 19, 2007 761  = [ d | let tv_set = mkVarSet tvs  simonpj@microsoft.com committed Jun 20, 2007 762  , d <- get_dicts wanteds  simonpj@microsoft.com committed Jun 19, 2007 763  , not (tyVarsOfInst d intersectsVarSet tv_set)]  chak@cse.unsw.edu.au. committed Aug 28, 2007 764 765  get_dict i@(EqInst {}) | want_dict i = [i] | otherwise = []  simonpj@microsoft.com committed Jun 20, 2007 766  get_dict other = pprPanic "approximateImplications" (ppr other)  qrczak committed Jul 17, 2001 767 \end{code}  simonpj committed Mar 19, 1998 768   simonpj@microsoft.com committed Jun 19, 2007 769 770 Note [Inference and implication constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  simonpj@microsoft.com committed Jun 20, 2007 771 772 773 774 775 776 777 778 779 780 781 782 783 Suppose we have a wanted implication constraint (perhaps arising from a nested pattern match) like C a => D [a] and we are now trying to quantify over 'a' when inferring the type for a function. In principle it's possible that there might be an instance instance (C a, E a) => D [a] so the context (E a) would suffice. The Right Thing is to abstract over the implication constraint, but we don't do that (a) because it'll be surprising to programmers and (b) because we don't have the machinery to deal with 'given' implications. So our best approximation is to make (D [a]) part of the inferred context, so we can use that to discharge the implication. Hence  simonpj@microsoft.com committed Oct 10, 2007 784 the strange function get_dicts in approximateImplications.  simonpj@microsoft.com committed Jun 20, 2007 785 786 787 788 789 790  The common cases are more clear-cut, when we have things like forall a. C a => C b Here, abstracting over (C b) is not an approximation at all -- but see Note [Freeness and implications].  simonpj@microsoft.com committed Jun 19, 2007 791 792 793 See Trac #1430 and test tc228.  simonpj@microsoft.com committed Dec 11, 2006 794 795 796 797 798 799 800 801 802 803 804 805 806 807 \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  chak@cse.unsw.edu.au. committed Aug 28, 2007 808  = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)  twanvl committed Jan 17, 2008 809  ; (irreds, binds) <- gentleCheckLoop loc givens wanteds  simonpj@microsoft.com committed Dec 11, 2006 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832  -- 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  chak@cse.unsw.edu.au. committed Aug 28, 2007 833  ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))  simonpj@microsoft.com committed Dec 11, 2006 834 835 836  ; return (qtvs', binds unionBags implic_bind) } \end{code}  simonpj@microsoft.com committed Nov 23, 2006 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 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 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870  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 871 872 873 polymorphic in. The net effect of [NO TYVARS]  simonpj committed Oct 17, 2001 874   simonpj committed Jan 25, 2001 875 \begin{code}  simonpj committed Oct 25, 2001 876 877 isFreeWhenInferring :: TyVarSet -> Inst -> Bool isFreeWhenInferring qtvs inst  simonpj@microsoft.com committed Nov 24, 2006 878 879 880  = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars && isInheritableInst inst -- and no implicit parameter involved -- see Note [Inheriting implicit parameters]  simonpj committed Oct 25, 2001 881   simonpj@microsoft.com committed Nov 10, 2006 882 {- No longer used (with implication constraints)  simonpj committed Oct 25, 2001 883 884 885 886 887 888 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 889 -}  simonpj committed Oct 25, 2001 890   simonpj@microsoft.com committed Sep 23, 2006 891 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst disjointVarSet qtvs  simonpj committed Oct 25, 2001 892 isFreeWrtIPs ips inst = not (any (elemNameSet ips) (ipNamesOfInst inst))  simonpj committed Jan 25, 2001 893 \end{code}  simonpj committed Mar 19, 1998 894   simonpj committed Feb 10, 1998 895   simonpj committed Jan 25, 2001 896 897 898 899 900 %************************************************************************ %* * \subsection{tcSimplifyCheck} %* * %************************************************************************  partain committed Mar 19, 1996 901   simonpj committed Jan 25, 2001 902 @tcSimplifyCheck@ is used when we know exactly the set of variables  simonpj committed Feb 20, 2001 903 we are going to quantify over. For example, a class or instance declaration.  partain committed Jan 08, 1996 904 905  \begin{code}  simonpj@microsoft.com committed Nov 10, 2006 906 -----------------------------------------------------------  simonpj committed Oct 25, 2001 907 -- tcSimplifyCheck is used when checking expression type signatures,  simonpj committed Jun 25, 2001 908 -- class decls, instance decls etc.  simonpj@microsoft.com committed Nov 10, 2006 909 910 911 912 913 914 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 915  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )  chak@cse.unsw.edu.au. committed Aug 28, 2007 916 917  do { traceTc (text "tcSimplifyCheck") ; (irreds, binds) <- gentleCheckLoop loc givens wanteds  simonpj@microsoft.com committed Dec 11, 2006 918  ; implic_bind <- bindIrreds loc qtvs givens irreds  simonpj@microsoft.com committed Nov 10, 2006 919 920 921 922 923 924 925 926 927  ; return (binds unionBags implic_bind) } ----------------------------------------------------------- -- tcSimplifyCheckPat is used for existential pattern match tcSimplifyCheckPat :: InstLoc -> [TcTyVar] -- Quantify over these -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings  chak@cse.unsw.edu.au. committed Feb 29, 2008 928 tcSimplifyCheckPat loc qtvs givens wanteds  simonpj@microsoft.com committed Dec 11, 2006 929  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )  chak@cse.unsw.edu.au. committed Aug 28, 2007 930 931  do { traceTc (text "tcSimplifyCheckPat") ; (irreds, binds) <- gentleCheckLoop loc givens wanteds  chak@cse.unsw.edu.au. committed Feb 29, 2008 932  ; implic_bind <- bindIrredsR loc qtvs givens irreds  simonpj@microsoft.com committed Nov 10, 2006 933 934 935  ; return (binds unionBags implic_bind) } -----------------------------------------------------------  simonpj@microsoft.com committed Dec 11, 2006 936 937 938 939 bindIrreds :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds bindIrreds loc qtvs givens irreds  chak@cse.unsw.edu.au. committed Feb 29, 2008 940  = bindIrredsR loc qtvs givens irreds  simonpj@microsoft.com committed Dec 11, 2006 941   chak@cse.unsw.edu.au. committed Feb 29, 2008 942 bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds  simonpj@microsoft.com committed Nov 10, 2006 943 944 -- Make a binding that binds 'irreds', by generating an implication -- constraint for them, *and* throwing the constraint into the LIE  chak@cse.unsw.edu.au. committed Feb 29, 2008 945 bindIrredsR loc qtvs givens irreds  simonpj@microsoft.com committed Dec 11, 2006 946 947 948  | null irreds = return emptyBag | otherwise  simonpj@microsoft.com committed Oct 27, 2007 949 950 951 952  = do { let givens' = filter isAbstractableInst givens -- The givens can (redundantly) include methods -- We want to retain both EqInsts and Dicts -- There should be no implicadtion constraints  simonpj@microsoft.com committed Dec 11, 2006 953  -- See Note [Pruning the givens in an implication constraint]  simonpj@microsoft.com committed Nov 10, 2006 954   chak@cse.unsw.edu.au. committed Feb 28, 2008 955  -- If there are no 'givens', then it's safe to  simonpj@microsoft.com committed Nov 10, 2006 956 957  -- partition the 'wanteds' by their qtvs, thereby trimming irreds -- See Note [Freeness and implications]  chak@cse.unsw.edu.au. committed Feb 28, 2008 958  ; irreds' <- if null givens'  simonpj@microsoft.com committed Nov 22, 2006 959 960 961 962 963 964 965  then do { let qtv_set = mkVarSet qtvs (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds ; extendLIEs frees ; return real_irreds } else return irreds  chak@cse.unsw.edu.au. committed Feb 29, 2008 966  ; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'  simonpj@microsoft.com committed Feb 02, 2007 967 968  -- This call does the real work -- If irreds' is empty, it does something sensible  simonpj@microsoft.com committed Nov 22, 2006 969 970  ; extendLIEs implics ; return bind }  simonpj@microsoft.com committed Nov 10, 2006 971 972   chak@cse.unsw.edu.au. committed Feb 28, 2008 973 makeImplicationBind :: InstLoc -> [TcTyVar]  simonpj@microsoft.com committed Nov 22, 2006 974 975 976 977 978 979 980  -> [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 981 982 -- f :: forall qtvs. {reft} givens => (ir1, .., irn) -- qtvs includes coercion variables  simonpj@microsoft.com committed Nov 22, 2006 983 984 -- -- This binding must line up the 'rhs' in reduceImplication  chak@cse.unsw.edu.au. committed Feb 28, 2008 985 makeImplicationBind loc all_tvs  simonpj@microsoft.com committed Oct 27, 2007 986 987  givens -- Guaranteed all Dicts -- or EqInsts  simonpj@microsoft.com committed Nov 22, 2006 988 989 990 991 992  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 993  ; span <- getSrcSpanM  chak@cse.unsw.edu.au. committed Sep 06, 2007 994  ; let (eq_givens, dict_givens) = partition isEqInst givens  simonpj@microsoft.com committed Oct 27, 2007 995 996 997 998  eq_tyvar_cos = mkTyVarTys (varSetElems $tyVarsOfTypes$ map eqInstType eq_givens) -- Urgh! See line 2187 or thereabouts. I believe that all these -- 'givens' must be a simple CoVar. This MUST be cleaned up.  Simon Marlow committed May 11, 2007 999  ; let name = mkInternalName uniq (mkVarOcc "ic") span  chak@cse.unsw.edu.au. committed Feb 29, 2008 1000  implic_inst = ImplicInst { tci_name = name,  simonpj@microsoft.com committed Nov 10, 2006 1001  tci_tyvars = all_tvs,  chak@cse.unsw.edu.au. committed Aug 28, 2007 1002  tci_given = (eq_givens ++ dict_givens),  simonpj@microsoft.com committed Nov 10, 2006 1003  tci_wanted = irreds, tci_loc = loc }  chak@cse.unsw.edu.au. committed Sep 06, 2007 1004 1005  ; let -- only create binder for dict_irreds (eq_irreds, dict_irreds) = partition isEqInst irreds  chak@cse.unsw.edu.au. committed Aug 28, 2007 1006 1007 1008 1009  n_dict_irreds = length dict_irreds dict_irred_ids = map instToId dict_irreds tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids) pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty  simonpj@microsoft.com committed Nov 10, 2006 1010  rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))  simonpj@microsoft.com committed Nov 05, 2007 1011 1012 1013  co = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)  chak@cse.unsw.edu.au. committed Aug 28, 2007 1014 1015 1016 1017 1018  bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs | otherwise = PatBind { pat_lhs = L span pat, pat_rhs = unguardedGRHSs rhs, pat_rhs_ty = tup_ty, bind_fvs = placeHolderNames }  chak@cse.unsw.edu.au. committed Nov 22, 2007 1019 1020 1021  ; traceTc \$ text "makeImplicationBind" <+> ppr implic_inst ; return ([implic_inst], unitBag (L span bind)) }  simonpj@microsoft.com committed Nov 10, 2006 1022 1023  -----------------------------------------------------------  simonpj@microsoft.com committed Jun 20, 2007 1024 tryHardCheckLoop :: SDoc  simonpj@microsoft.com committed Nov 10, 2006 1025  -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 11, 2006 1026  -> TcM ([Inst], TcDictBinds)  simonpj@microsoft.com committed Nov 10, 2006 1027   simonpj@microsoft.com committed Jun 20, 2007 1028 tryHardCheckLoop doc wanteds  simonpj@microsoft.com committed Nov 28, 2007 1029  = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds  chak@cse.unsw.edu.au. committed Aug 28, 2007 1030 1031  ; return (irreds,binds) }  simonpj committed Jun 25, 2001 1032  where  simonpj@microsoft.com committed Nov 10, 2006 1033  try_me inst = ReduceMe AddSCs  simonpj@microsoft.com committed Jun 20, 2007 1034  -- Here's the try-hard bit  simonpj@microsoft.com committed Nov 10, 2006 1035 1036  -----------------------------------------------------------  simonpj@microsoft.com committed Jun 20, 2007 1037 gentleCheckLoop :: InstLoc  simonpj@microsoft.com committed Nov 10, 2006 1038 1039  -> [Inst] -- Given -> [Inst] -- Wanted  simonpj@microsoft.com committed Dec 11, 2006 1040  -> TcM ([Inst], TcDictBinds)  simonpj@microsoft.com committed Nov 10, 2006 1041   simonpj@microsoft.com committed Jun 20, 2007 1042 gentleCheckLoop inst_loc givens wanteds  simonpj@microsoft.com committed Nov 28, 2007 1043  = do { (irreds,binds) <- checkLoop env wanteds  chak@cse.unsw.edu.au. committed Aug 28, 2007 1044 1045  ; return (irreds,binds) }  simonpj@microsoft.com committed Nov 10, 2006 1046 1047 1048  where env = mkRedEnv (pprInstLoc inst_loc) try_me givens  simonpj@microsoft.com committed Nov 23, 2006 1049 1050  try_me inst | isMethodOrLit inst = ReduceMe AddSCs | otherwise = Stop  simonpj@microsoft.com committed Nov 10, 2006 1051 1052  -- When checking against a given signature -- we MUST be very gentle: Note [Check gently]  simonpj@microsoft.com committed Oct 10, 2007 1053 1054 1055 1056  gentleInferLoop :: SDoc -> [Inst] -> TcM ([Inst], TcDictBinds) gentleInferLoop doc wanteds  simonpj@microsoft.com committed Nov 28, 2007 1057  = do { (irreds, binds) <- checkLoop env wanteds  simonpj@microsoft.com committed Oct 10, 2007 1058 1059 1060 1061 1062  ; return (irreds, binds) } where env = mkRedEnv doc try_me [] try_me inst | isMethodOrLit inst = ReduceMe AddSCs | otherwise = Stop  simonpj@microsoft.com committed Nov 10, 2006 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 \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]  simonpj@microsoft.com committed Oct 10, 2007 1080 Later, we will solve this constraint using the knowledge (Show b)  simonpj@microsoft.com committed Nov 10, 2006 1081 1082 1083 1084 1085  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  simonpj@microsoft.com committed Jun 20, 2007 1086 with tryHardCheckLooop.  simonpj@microsoft.com committed Nov 10, 2006 1087 1088 1089 1090 1091 1092  \begin{code} ----------------------------------------------------------- checkLoop :: RedEnv -> [Inst] -- Wanted  simonpj@microsoft.com committed Nov 28, 2007 1093  -> TcM ([Inst], TcDictBinds)  simonpj@microsoft.com committed Dec 11, 2006 1094 -- Precondition: givens are completely rigid  simonpj@microsoft.com committed Jun 20, 2007 1095 -- Postcondition: returned Insts are zonked  simonpj@microsoft.com committed Nov 10, 2006 1096 1097  checkLoop env wanteds  1098 1099  = go env wanteds (return ()) where go env wanteds elim_skolems  twanvl committed Jan 17, 2008 1100  = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]  chak@cse.unsw.edu.au. committed Sep 19, 2007 1101 1102  ; env' <- zonkRedEnv env ; wanteds' <- zonkInsts wanteds  chak@cse.unsw.edu.au. committed Aug 28, 2007 1103   1104 1105 1106  ; (improved, binds, irreds, elim_more_skolems) <- reduceContext env' wanteds' ; let elim_skolems' = elim_skolems >> elim_more_skolems  simonpj@microsoft.com committed Nov 10, 2006 1107   chak@cse.unsw.edu.au. committed Aug 28, 2007 1108  ; if not improved then  1109  elim_skolems' >> return (irreds, binds)  chak@cse.unsw.edu.au. committed Aug 28, 2007 1110 1111 1112 1113  else do -- If improvement did some unification, we go round again. -- We start again with irreds, not wanteds  1114 1115 1116 1117 1118  -- 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] { (irreds1, binds1) <- go env' irreds elim_skolems'  simonpj@microsoft.com committed Nov 28, 2007 1119  ; return (irreds1, binds unionBags binds1) } }  simonpj@microsoft.com committed Nov 10, 2006 1120 \end{code}  simonpj committed Jun 25, 2001 1121   chak@cse.unsw.edu.au. committed Sep 19, 2007 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 Note [Zonking RedEnv] ~~~~~~~~~~~~~~~~~~~~~ It might appear as if the givens in RedEnv are always rigid, but that is not necessarily the case for programs involving higher-rank types that have class contexts constraining the higher-rank variables. An example from tc237 in the testsuite is class Modular s a | s -> a wim :: forall a w. Integral a => a -> (forall s. Modular s a => M s w) -> w wim i k = error "urk" test5 :: (Modular s a, Integral a) => M s a test5 = error "urk" test4 = wim 4 test4' Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is quantified further outside. When type checking test4, we have to check whether the signature of test5 is an instance of (forall s. Modular s a => M s w) Consequently, we will get (Modular s t_a), where t_a is a TauTv into the givens. Given the FD of Modular in this example, class improvement will instantiate t_a to 'a', where 'a' is the skolem from test5's signatures (due to the Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in the givens, we will get into a loop as improveOne uses the unification engine TcGadt.tcUnifyTys, which doesn't know about mutable type variables.  simonpj@microsoft.com committed Nov 23, 2006 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 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 1173   simonpj committed Jan 25, 2001 1174   simonpj committed Mar 09, 2005 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197