Improve eta reduction, to reduce Simplifier iterations

I finally got around to investigating why the Simplifier was sometimes
iterating so often.  There's a nice example in Text.ParserCombinators.ReadPrec,
which produced:

NOTE: Simplifier still going after 3 iterations; bailing out.  Size = 339
NOTE: Simplifier still going after 3 iterations; bailing out.  Size = 339
NOTE: Simplifier still going after 3 iterations; bailing out.  Size = 339

No progress is being made.  It turned out that an interaction between
eta-expansion, casts, and eta reduction was responsible. The change is
small and simple, in SimplUtils.mkLam: do not require the body to be
a Lam when floating the cast outwards.  

I also discovered a missing side condition in the same equation, so fixing
that is good too.  Now there is no loop when compiling ReadPrec.

Should do a full nofib run though.

1 files changed, 27 insertions, 9 deletions

diff --git a/compiler/simplCore/SimplUtils.lhs b/compiler/simplCore/SimplUtils.lhs
index 9d0aa078a5..fbbdf45792 100644
--- a/compiler/simplCore/SimplUtils.lhs
+++ b/compiler/simplCore/SimplUtils.lhs
@@ -49,8 +49,7 @@ import Id
 import Var	( isCoVar )
 import NewDemand
 import SimplMonad
-import Type	( Type, funArgTy, mkForAllTys, mkTyVarTys, 
-		  splitTyConApp_maybe, tyConAppArgs )
+import Type	hiding( substTy )
 import TyCon
 import DataCon
 import Unify	( dataConCannotMatch )
@@ -844,12 +843,14 @@ mkLam bndrs body
 	; mkLam' dflags bndrs body }
   where
     mkLam' :: DynFlags -> [OutBndr] -> OutExpr -> SimplM OutExpr
-    mkLam' dflags bndrs (Cast body@(Lam _ _) co)
+    mkLam' dflags bndrs (Cast body co)
+      | not (any bad bndrs)
 	-- Note [Casts and lambdas]
-      = do { lam <- mkLam' dflags (bndrs ++ bndrs') body'
+      = do { lam <- mkLam' dflags bndrs body
 	   ; return (mkCoerce (mkPiTypes bndrs co) lam) }
-      where	
-	(bndrs',body') = collectBinders body
+      where
+	co_vars  = tyVarsOfType co
+	bad bndr = isCoVar bndr && bndr `elemVarSet` co_vars      
 
     mkLam' dflags bndrs body
       | dopt Opt_DoEtaReduction dflags,
@@ -877,9 +878,26 @@ So this equation in mkLam' floats the g1 out, thus:
 	(\x. e `cast` g1)  -->  (\x.e) `cast` (tx -> g1)
 where x:tx.
 
-In general, this floats casts outside lambdas, where (I hope) they might meet
-and cancel with some other cast.
-
+In general, this floats casts outside lambdas, where (I hope) they
+might meet and cancel with some other cast:
+	\x. e `cast` co   ===>   (\x. e) `cast` (tx -> co)
+	/\a. e `cast` co  ===>   (/\a. e) `cast` (/\a. co)
+	/\g. e `cast` co  ===>   (/\g. e) `cast` (/\g. co)
+  		  	  (if not (g `in` co))
+
+Notice that it works regardless of 'e'.  Originally it worked only
+if 'e' was itself a lambda, but in some cases that resulted in 
+fruitless iteration in the simplifier.  A good example was when
+compiling Text.ParserCombinators.ReadPrec, where we had a definition 
+like	(\x. Get `cast` g)
+where Get is a constructor with nonzero arity.  Then mkLam eta-expanded
+the Get, and the next iteration eta-reduced it, and then eta-expanded 
+it again.
+
+Note also the side condition for the case of coercion binders.
+It does not make sense to transform
+	/\g. e `cast` g  ==>  (/\g.e) `cast` (/\g.g)
+because the latter is not well-kinded.
 
 --	c) floating lets out through big lambdas 
 --		[only if all tyvar lambdas, and only if this lambda