TcSimplify.lhs 89.9 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
%
5

6
TcSimplify
7 8

\begin{code}
9
module TcSimplify (
10
	tcSimplifyInfer, tcSimplifyInferCheck,
11
	tcSimplifyCheck, tcSimplifyRestricted,
12
	tcSimplifyRuleLhs, tcSimplifyIPs, 
13
	tcSimplifySuperClasses,
14
	tcSimplifyTop, tcSimplifyInteractive,
15
	tcSimplifyBracket, tcSimplifyCheckPat,
16

17
	tcSimplifyDeriv, tcSimplifyDefault,
18
	bindInstsOfLocalFuns, bindIrreds,
19 20
    ) where

21
#include "HsVersions.h"
22

23
import {-# SOURCE #-} TcUnify( unifyType )
24
import HsSyn
25

26
import TcRnMonad
27 28 29
import Inst
import TcEnv
import InstEnv
30
import TcGadt
31
import TcType
32
import TcMType
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
45
import VarSet
46
import VarEnv
47
import FiniteMap
48
import Bag
49
import Outputable
50 51 52 53 54 55
import ListSetOps
import Util
import SrcLoc
import DynFlags

import Data.List
56 57 58 59 60
\end{code}


%************************************************************************
%*									*
61
\subsection{NOTES}
62 63 64
%*									*
%************************************************************************

65 66 67 68
	--------------------------------------
	Notes on functional dependencies (a bug)
	--------------------------------------

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
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:

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
| 
| <interactive>:1:
|     Could not deduce (Bar a b) from the context (Foo a b)
|       arising from use of `foo' at <interactive>: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.  



137
	--------------------------------------
138
		Notes on quantification
139
	--------------------------------------
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
146
	C	the constraints from that RHS
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

158
and float the constraints Ct further outwards.
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
197
		using all conceivable links from C.
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.

205
Notice that
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 ...
226

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

234
  And then if the fn was called at several different c's, each of
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's avatar
simonpj@microsoft.com committed
258 259 260
-------------------------------------
	Note [Ambiguity]
-------------------------------------
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.

300
So here's the plan.  We WARN about probable ambiguity if
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
306
in the environment, or by the variables in the type.
307 308 309

Notice that we union before calling oclose.  Here's an example:

310
	class J a b c | a b -> c
311 312 313
	fv(G) = {a}

Is this ambiguous?
314
	forall b c. (J a b c) => b -> b
315 316

Only if we union {a} from G with {b} from T before using oclose,
317
do we see that c is fixed.
318

319
It's a bit vague exactly which C we should use for this oclose call.  If we
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

329
then c is a "bubble"; there's no way it can ever improve, and it's
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.
348
The definitely-ambiguous can then float out, and get smashed at top level
349 350 351
(which squashes out the constants, like Eq (T a) above)


352
	--------------------------------------
353
		Notes on principal types
354
	--------------------------------------
355 356 357

    class C a where
      op :: a -> a
358

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


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.


396
	--------------------------------------
397
		Notes on implicit parameters
398
	--------------------------------------
399

400 401
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402 403 404
Consider this:

	f x = (x::Int) + ?y
405

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:
409

410 411 412
	f :: Int -> Int

(so we get ?y from the context of f's definition), or
413 414 415

	f :: (?y::Int) => Int -> Int

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.

422 423
BOTTOM LINE: when *inferring types* you *must* quantify 
over implicit parameters. See the predicate isFreeWhenInferring.
424

425

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'.


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:
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).
456

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:
460

461
	f :: Int -> Int
462
	f x = (x::Int) + ?y
463

464
At first sight this seems reasonable, but it has the nasty property
465
that adding a type signature changes the dynamic semantics.
466
Consider this:
467

468
	(let f x = (x::Int) + ?y
469 470 471 472
 	 in (f 3, f 3 with ?y=5))  with ?y = 6

		returns (3+6, 3+5)
vs
473
	(let f :: Int -> Int
474
	     f x = x + ?y
475 476 477 478
	 in (f 3, f 3 with ?y=5))  with ?y = 6

		returns (3+6, 3+6)

479 480
Indeed, simply inlining f (at the Haskell source level) would change the
dynamic semantics.
481

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.
509

510

511 512 513
Question 3: monomorphism
~~~~~~~~~~~~~~~~~~~~~~~~
There's a nasty corner case when the monomorphism restriction bites:
514

515 516
	z = (x::Int) + ?y

517 518
The argument above suggests that we *must* generalise
over the ?y parameter, to get
519 520
	z :: (?y::Int) => Int,
but the monomorphism restriction says that we *must not*, giving
521
	z :: Int.
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.


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.  

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:
553
	* Inlining remains valid
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.
591

592
It's really not clear what is the Right Thing To Do.  If you see
593

594
	z = (x::Int) + ?y
595

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.
602

603
Choice (C) really says "the monomorphism restriction doesn't apply
604
to implicit parameters".  Which is fine, but remember that every
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'
608
clauses that bind ?y, so a decent compiler should common up all
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.
612

613
BOTTOM LINE: we choose (B) at present.  See tcSimplifyRestricted
614

615

616

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 )
626 627

    2. Partition C based on Q into Ct and Cq.  Notice that ambiguous
628
       predicates will end up in Ct; we deal with them at the top level
629

630
    3. Try improvement, using functional dependencies
631

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
636
Eq (a,b), we don't simplify to (Eq a, Eq b).  So Q won't be different
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 ...
644

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
651
again.
652

653 654

\begin{code}
655
tcSimplifyInfer
656 657
	:: SDoc
	-> TcTyVarSet		-- fv(T); type vars
658
	-> [Inst]		-- Wanted
659
	-> TcM ([TcTyVar],	-- Tyvars to quantify (zonked and quantified)
660 661
		[Inst],		-- Dict Ids that must be bound here (zonked)
		TcDictBinds)	-- Bindings
662
	-- Any free (escaping) Insts are tossed into the environment
663
\end{code}
664

665 666

\begin{code}
667 668 669
tcSimplifyInfer doc tau_tvs wanted
  = do	{ tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
	; wanted' <- mappM zonkInst wanted	-- Zonk before deciding quantified tyvars
670
	; gbl_tvs  <- tcGetGlobalTyVars
671
	; let preds = fdPredsOfInsts wanted'
672
	      qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
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
676

677
		-- To make types simple, reduce as much as possible
678
	; let try_me inst = ReduceMe AddSCs
679
	; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound
680

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) }
689 690
	-- NB: when we are done, we might have some bindings, but
	-- the final qtvs might be empty.  See Note [NO TYVARS] below.
691
\end{code}
692

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}

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]
~~~~~~~~~~~~~~~~~
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
768 769 770
polymorphic in.  

The net effect of [NO TYVARS] 
771

772
\begin{code}
773 774
isFreeWhenInferring :: TyVarSet -> Inst	-> Bool
isFreeWhenInferring qtvs inst
775 776 777
  =  isFreeWrtTyVars qtvs inst	-- Constrains no quantified vars
  && isInheritableInst inst	-- and no implicit parameter involved
				--   see Note [Inheriting implicit parameters]
778

779
{-	No longer used (with implication constraints)
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
786
-}
787

788
isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
789
isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
790
\end{code}
791

792

793 794 795 796 797
%************************************************************************
%*									*
\subsection{tcSimplifyCheck}
%*									*
%************************************************************************
798

799
@tcSimplifyCheck@ is used when we know exactly the set of variables
800
we are going to quantify over.  For example, a class or instance declaration.
801 802

\begin{code}
803
-----------------------------------------------------------
804
-- tcSimplifyCheck is used when checking expression type signatures,
805
-- class decls, instance decls etc.
806 807 808 809 810 811
tcSimplifyCheck	:: InstLoc
	 	-> [TcTyVar]		-- Quantify over these
	 	-> [Inst]		-- Given
	 	-> [Inst]		-- Wanted
	 	-> TcM TcDictBinds	-- Bindings
tcSimplifyCheck loc qtvs givens wanteds 
812 813 814
  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
    do	{ (irreds, binds) <- innerCheckLoop loc givens wanteds
	; implic_bind <- bindIrreds loc qtvs givens irreds
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
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
830 831 832
	; return (binds `unionBags` implic_bind) }

-----------------------------------------------------------
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	
842 843
-- Make a binding that binds 'irreds', by generating an implication
-- constraint for them, *and* throwing the constraint into the LIE
844 845 846 847
bindIrredsR loc qtvs co_vars reft givens irreds
  | null irreds
  = return emptyBag
  | otherwise
848 849
  = do	{ let givens' = filter isDict givens
		-- The givens can include methods
850
		-- See Note [Pruning the givens in an implication constraint]
851

852 853
	   -- If there are no 'givens' *and* the refinement is empty
	   -- (the refinement is like more givens), then it's safe to 
854 855
	   -- partition the 'wanteds' by their qtvs, thereby trimming irreds
	   -- See Note [Freeness and implications]
856
	; irreds' <- if null givens' && isEmptyRefinement reft
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's avatar
simonpj@microsoft.com committed
866 867
			-- This call does the real work
			-- If irreds' is empty, it does something sensible
868 869
	; extendLIEs implics
	; return bind } 
870 871


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's avatar
simonpj@microsoft.com committed
880 881
--	f :: forall qtvs. {reft} givens => (ir1, .., irn)
-- qtvs includes coercion variables
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 
891
	; span <- getSrcSpanM
892
	; let name = mkInternalName uniq (mkVarOcc "ic") (srcSpanStart span)
893 894
	      implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
					 tci_tyvars = all_tvs, 
895
					 tci_given = givens,
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)))
903
	      co  = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
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) $
910
	  return ([implic_inst], unitBag (L span bind)) }
911 912 913 914

-----------------------------------------------------------
topCheckLoop :: SDoc
	     -> [Inst]			-- Wanted
915
	     -> TcM ([Inst], TcDictBinds)
916 917 918

topCheckLoop doc wanteds
  = checkLoop (mkRedEnv doc try_me []) wanteds
919
  where
920 921 922
    try_me inst = ReduceMe AddSCs

-----------------------------------------------------------
923
innerCheckLoop :: InstLoc
924 925
	       -> [Inst]		-- Given
	       -> [Inst]		-- Wanted
926
	       -> TcM ([Inst], TcDictBinds)
927

928
innerCheckLoop inst_loc givens wanteds
929 930 931 932
  = checkLoop env wanteds
  where
    env = mkRedEnv (pprInstLoc inst_loc) try_me givens

933 934
    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
		| otherwise	     = Stop
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
967 968
	  -> TcM ([Inst], TcDictBinds)
-- Precondition: givens are completely rigid
969 970 971 972 973

checkLoop env wanteds
  = do { -- Givens are skolems, so no need to zonk them
	 wanteds' <- mappM zonkInst wanteds

974
	; (improved, binds, irreds) <- reduceContext env wanteds'
975

976
	; if not improved then
977
 	     return (irreds, binds)
978 979
	  else do

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]
985 986
	{ (irreds1, binds1) <- checkLoop env irreds
	; return (irreds1, binds `unionBags` binds1) } }
987
\end{code}
988

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)!

1006

1007

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}
1053 1054 1055 1056 1057 1058
tcSimplifySuperClasses 
	:: InstLoc 
	-> [Inst]	-- Given 
	-> [Inst]	-- Wanted
	-> TcM TcDictBinds
tcSimplifySuperClasses loc givens sc_wanteds
1059
  = do	{ (irreds, binds1) <- checkLoop env sc_wanteds
1060 1061 1062
	; let (tidy_env, tidy_irreds) = tidyInsts irreds
	; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
	; return binds1 }
1063
  where
1064 1065 1066
    env = mkRedEnv (pprInstLoc loc) try_me givens
    try_me inst = ReduceMe NoSCs
	-- Like topCheckLoop, but with NoSCs
1067 1068 1069
\end{code}


1070 1071 1072 1073 1074 1075
%************************************************************************
%*									*
\subsection{tcSimplifyRestricted}
%*									*
%************************************************************************

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
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.
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.
  

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.
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.

1169

1170 1171
\begin{code}
tcSimplifyRestricted 	-- Used for restricted binding groups
1172
			-- i.e. ones subject to the monomorphism restriction
1173
	:: SDoc
1174 1175
	-> TopLevelFlag
	-> [Name]		-- Things bound in this group
1176
	-> TcTyVarSet		-- Free in the type of the RHSs
1177
	-> [Inst]		-- Free in the RHSs
1178
	-> TcM ([TyVar],	-- Tyvars to quantify (zonked and quantified)
1179
		TcDictBinds)	-- Bindings
1180 1181 1182
	-- tcSimpifyRestricted returns no constraints to
	-- quantify over; by definition there are none.
	-- They are all thrown back in the LIE
1183

1184
tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
1185
	-- Zonk everything in sight
1186
  = do	{ wanteds' <- mappM zonkInst wanteds
1187

1188
   	-- 'ReduceMe': Reduce as far as we can.  Don't stop at
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.
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
1197 1198
	; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
	; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
1199 1200

	-- Next, figure out the tyvars we will quantify over
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])

1221
	; traceTc (text "tcSimplifyRestricted" <+> vcat [
1222
		pprInsts wanteds, pprInsts constrained_dicts',
1223
		ppr _binds,
1224
		ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
1225

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.
	--
1230
	-- We quantify only over constraints that are captured by qtvs;
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
1239 1240 1241
	--
	-- At top level, we *do* squash methods becuase we want to 
	-- expose implicit parameters to the test that follows
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'
1248 1249

	-- See "Notes on implicit parameters, Question 4: top level"
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) }
1259 1260
\end{code}

1261 1262 1263

%************************************************************************
%*									*
1264
		tcSimplifyRuleLhs
1265 1266 1267
%*									*
%************************************************************************

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.

1272 1273 1274
Example.  Consider the following left-hand side of a rule
	
	f (x == y) (y > z) = ...
1275

1276
If we typecheck this expression we get constraints
1277

1278
	d1 :: Ord a, d2 :: Eq a
1279

1280
We do NOT want to "simplify" to the LHS
1281

1282 1283
	forall x::a, y::a, z::a, d1::Ord a.
	  f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
1284

1285
Instead we want	
1286

1287 1288
	forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
	  f ((==) d2 x y) ((>) d1 y z) = ...
1289