Merge branch 'master' of http://darcs.haskell.org/ghc

61 files changed, 2331 insertions, 2036 deletions

diff --git a/compiler/basicTypes/DataCon.lhs b/compiler/basicTypes/DataCon.lhs
index 06c5bb255a..a0cc4bdbdf 100644
--- a/compiler/basicTypes/DataCon.lhs
+++ b/compiler/basicTypes/DataCon.lhs
@@ -563,6 +563,7 @@ instance Outputable StrictnessMark where
 
 
 eqHsBang :: HsBang -> HsBang -> Bool
+eqHsBang HsNoBang             HsNoBang             = True
 eqHsBang HsStrict             HsStrict             = True
 eqHsBang (HsUserBang u1 b1)   (HsUserBang u2 b2)   = u1==u2 && b1==b2
 eqHsBang (HsUnpack Nothing)   (HsUnpack Nothing)   = True
diff --git a/compiler/basicTypes/Demand.lhs b/compiler/basicTypes/Demand.lhs
index bd3638a093..ad778d16ad 100644
--- a/compiler/basicTypes/Demand.lhs
+++ b/compiler/basicTypes/Demand.lhs
@@ -2,259 +2,864 @@
 % (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section[Demand]{@Demand@: the amount of demand on a value}
+\section[Demand]{@Demand@: A decoupled implementation of a demand domain}
 
 \begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
-module Demand(
-	Demand(..), 
-	topDmd, lazyDmd, seqDmd, evalDmd, errDmd, isStrictDmd, 
-	isTop, isAbsent, seqDemand,
-
-	DmdType(..), topDmdType, botDmdType, mkDmdType, mkTopDmdType, 
-		dmdTypeDepth, seqDmdType,
-	DmdEnv, emptyDmdEnv,
-	DmdResult(..), retCPR, isBotRes, returnsCPR, resTypeArgDmd,
-	
-	Demands(..), mapDmds, zipWithDmds, allTop, seqDemands,
-
-	StrictSig(..), mkStrictSig, topSig, botSig, cprSig,
-        isTopSig,
-	splitStrictSig, increaseStrictSigArity,
-	pprIfaceStrictSig, appIsBottom, isBottomingSig, seqStrictSig,
+
+module Demand (
+        StrDmd, strBot, strTop, strStr, strProd, strCall,
+        AbsDmd, absBot, absTop, absProd,
+
+        Demand, JointDmd, mkProdDmd, 
+        absDmd, topDmd, botDmd,
+        lubDmd, bothDmd,
+        isTopDmd, isBotDmd, isAbsDmd, isSeqDmd, 
+
+        DmdType(..), dmdTypeDepth, lubDmdType, bothDmdType,
+        topDmdType, botDmdType, mkDmdType, mkTopDmdType, 
+
+        DmdEnv, emptyDmdEnv,
+
+        DmdResult, CPRResult, PureResult, 
+        isBotRes, isTopRes, resTypeArgDmd, 
+        topRes, botRes, cprRes,
+        appIsBottom, isBottomingSig, pprIfaceStrictSig, returnsCPR, 
+        StrictSig(..), mkStrictSig, topSig, botSig, cprSig,
+        isTopSig, splitStrictSig, increaseStrictSigArity,
+       
+        seqStrDmd, seqStrDmdList, seqAbsDmd, seqAbsDmdList,
+        seqDemand, seqDemandList, seqDmdType, seqStrictSig, 
+        evalDmd, vanillaCall, isStrictDmd, splitCallDmd, splitDmdTy,
+        someCompUsed, isUsed, isUsedDmd,
+        defer, deferType, deferEnv, modifyEnv,
+
+        isProdDmd, splitProdDmd, splitProdDmd_maybe, peelCallDmd, mkCallDmd,
+        dmdTransformSig, dmdTransformDataConSig,
+
+        worthSplittingFun, worthSplittingThunk
      ) where
 
 #include "HsVersions.h"
 
 import StaticFlags
-import BasicTypes
+import Outputable
 import VarEnv
 import UniqFM
 import Util
-import Outputable
+import BasicTypes
+import Binary
+import Maybes                    ( expectJust )
+\end{code}
+
+%************************************************************************
+%*                                                                      *
+\subsection{Lattice-like structure for domains}
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+
+class LatticeLike a where
+  bot    :: a
+  top    :: a
+  pre    :: a -> a -> Bool
+  lub    :: a -> a -> a 
+  both   :: a -> a -> a
+
+-- False < True
+instance LatticeLike Bool where
+  bot     = False
+  top     = True
+-- x `pre` y <==> (x => y)
+  pre x y = (not x) || y  
+  lub     = (||)
+  both    = (&&)
+
 \end{code}
 
 
 %************************************************************************
-%*									*
-\subsection{Demands}
-%*									*
+%*                                                                      *
+\subsection{Strictness domain}
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
-data Demand
-  = Top			-- T; used for unlifted types too, so that
-			--	A `lub` T = T
-  | Abs			-- A
-
-  | Call Demand		-- C(d)
-
-  | Eval Demands	-- U(ds)
-
-  | Defer Demands	-- D(ds)
-
-  | Box Demand		-- B(d)
-
-  | Bot			-- B
-  deriving( Eq )
-	-- Equality needed for fixpoints in DmdAnal
-
-data Demands = Poly Demand	-- Polymorphic case
-	     | Prod [Demand]	-- Product case
-	     deriving( Eq )
-
-allTop :: Demands -> Bool
-allTop (Poly d)  = isTop d
-allTop (Prod ds) = all isTop ds
-
-isTop :: Demand -> Bool
-isTop Top = True
-isTop _   = False 
-
-isAbsent :: Demand -> Bool
-isAbsent Abs = True
-isAbsent _   = False 
-
-mapDmds :: (Demand -> Demand) -> Demands -> Demands
-mapDmds f (Poly d)  = Poly (f d)
-mapDmds f (Prod ds) = Prod (map f ds)
-
-zipWithDmds :: (Demand -> Demand -> Demand)
-	    -> Demands -> Demands -> Demands
-zipWithDmds f (Poly d1)  (Poly d2)  = Poly (d1 `f` d2)
-zipWithDmds f (Prod ds1) (Poly d2)  = Prod [d1 `f` d2 | d1 <- ds1]
-zipWithDmds f (Poly d1)  (Prod ds2) = Prod [d1 `f` d2 | d2 <- ds2]
-zipWithDmds f (Prod ds1) (Prod ds2) 
-  | length ds1 == length ds2 = Prod (zipWithEqual "zipWithDmds" f ds1 ds2)
-  | otherwise		     = Poly topDmd
-	-- This really can happen with polymorphism
-	-- \f. case f x of (a,b) -> ...
-	--     case f y of (a,b,c) -> ...
-	-- Here the two demands on f are C(LL) and C(LLL)!
-
-topDmd, lazyDmd, seqDmd, evalDmd, errDmd :: Demand
-topDmd  = Top			-- The most uninformative demand
-lazyDmd = Box Abs
-seqDmd  = Eval (Poly Abs)	-- Polymorphic seq demand
-evalDmd = Box seqDmd		-- Evaluate and return
-errDmd  = Box Bot		-- This used to be called X
 
-isStrictDmd :: Demand -> Bool
-isStrictDmd Bot      = True
-isStrictDmd (Eval _) = True
-isStrictDmd (Call _) = True
-isStrictDmd (Box d)  = isStrictDmd d
-isStrictDmd _        = False
-
-seqDemand :: Demand -> ()
-seqDemand (Call d)   = seqDemand d
-seqDemand (Eval ds)  = seqDemands ds
-seqDemand (Defer ds) = seqDemands ds
-seqDemand (Box d)    = seqDemand d
-seqDemand _          = ()
-
-seqDemands :: Demands -> ()
-seqDemands (Poly d)  = seqDemand d
-seqDemands (Prod ds) = seqDemandList ds
-
-seqDemandList :: [Demand] -> ()
+-- Vanilla strictness domain
+data StrDmd
+  = HyperStr             -- Hyper-strict 
+                         -- Bottom of the lattice
+
+  | SCall StrDmd         -- Call demand
+                         -- Used only for values of function type
+
+  | SProd [StrDmd]       -- Product
+                         -- Used only for values of product type
+                         -- Invariant: not all components are HyperStr (use HyperStr)
+                         --            not all components are Lazy     (use Str)
+
+  | Str                  -- Head-Strict
+                         -- A polymorphic demand: used for values of all types,
+                         --                       including a type variable
+
+  | Lazy                 -- Lazy
+                         -- Top of the lattice
+  deriving ( Eq, Show )
+
+-- Well-formedness preserving constructors for the Strictness domain
+strBot, strTop, strStr :: StrDmd
+strBot     = HyperStr
+strTop     = Lazy
+strStr     = Str
+
+strCall :: StrDmd -> StrDmd
+strCall Lazy     = Lazy
+strCall HyperStr = HyperStr
+strCall s        = SCall s
+
+strProd :: [StrDmd] -> StrDmd
+strProd sx
+  | any (== HyperStr) sx    = strBot
+  | all (== Lazy) sx        = strStr
+  | otherwise               = SProd sx
+
+-- Pretty-printing
+instance Outputable StrDmd where
+  ppr HyperStr      = char 'B'
+  ppr Lazy          = char 'L'
+  ppr (SCall s)     = char 'C' <> parens (ppr s)
+  ppr Str           = char 'S'
+  ppr (SProd sx)    = char 'S' <> parens (hcat (map ppr sx))
+
+-- LatticeLike implementation for strictness demands
+instance LatticeLike StrDmd where
+  bot = HyperStr
+  top = Lazy
+  
+  pre _ Lazy                               = True
+  pre HyperStr _                           = True
+  pre (SCall s1) (SCall s2)                = pre s1 s2
+  pre (SCall _) Str                        = True
+  pre (SProd _) Str                        = True
+  pre (SProd sx1) (SProd sx2)    
+            | length sx1 == length sx2     = all (== True) $ zipWith pre sx1 sx2 
+  pre x y                                  = x == y
+
+  lub x y | x == y                         = x 
+  lub y x | x `pre` y                      = lub x y
+  lub HyperStr s                           = s
+  lub _ Lazy                               = strTop
+  lub (SProd _) Str                        = strStr
+  lub (SProd sx1) (SProd sx2) 
+           | length sx1 == length sx2      = strProd $ zipWith lub sx1 sx2
+           | otherwise                     = strStr
+  lub (SCall s1) (SCall s2)                = strCall (s1 `lub` s2)
+  lub (SCall _)  Str                       = strStr
+  lub _ _                                  = strTop
+
+  both x y | x == y                        = x 
+  both y x | x `pre` y                     = both x y
+  both HyperStr _                          = strBot
+  both s Lazy                              = s
+  both s@(SProd _) Str                     = s
+  both (SProd sx1) (SProd sx2) 
+           | length sx1 == length sx2      = strProd $ zipWith both sx1 sx2 
+  both (SCall s1) (SCall s2)               = strCall (s1 `both` s2)
+  both s@(SCall _)  Str                    = s
+  both _ _                                 = strBot
+
+-- utility functions to deal with memory leaks
+seqStrDmd :: StrDmd -> ()
+seqStrDmd (SProd ds)   = seqStrDmdList ds
+seqStrDmd (SCall s)     = s `seq` () 
+seqStrDmd _            = ()
+
+seqStrDmdList :: [StrDmd] -> ()
+seqStrDmdList [] = ()
+seqStrDmdList (d:ds) = seqStrDmd d `seq` seqStrDmdList ds
+
+-- Splitting polymorphic demands
+splitStrProdDmd :: Int -> StrDmd -> [StrDmd]
+splitStrProdDmd n Lazy         = replicate n Lazy
+splitStrProdDmd n HyperStr     = replicate n HyperStr
+splitStrProdDmd n Str          = replicate n Lazy
+splitStrProdDmd n (SProd ds)   = ASSERT( ds `lengthIs` n) ds
+splitStrProdDmd n (SCall d)    = ASSERT( n == 1 ) [d]
+\end{code}
+
+%************************************************************************
+%*                                                                      *
+\subsection{Absence domain}
+%*                                                                      *
+%************************************************************************
+
+Note [Don't optimise UProd(Used) to Used]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+An AbsDmds
+   UProd [Used, Used]   and    Used
+are semantically equivalent, but we do not turn the former into
+the latter, for a regrettable-subtle reason.  Suppose we did.
+then
+  f (x,y) = (y,x)
+would get 
+  StrDmd = Str  = SProd [Lazy, Lazy]
+  AbsDmd = Used = UProd [Used, Used]
+But with the joint demand of <Str, Used> doesn't convey any clue
+that there is a product involved, and so the worthSplittingFun
+will not fire.  (We'd need to use the type as well to make it fire.)
+Moreover, consider
+  g h p@(_,_) = h p
+This too would get <Str, Used>, but this time there really isn't any
+point in w/w since the components of the pair are not used at all.
+
+So the solution is: don't collapse UProd [Used,Used] to Used; intead
+leave it as-is.  
+    
+
+\begin{code}
+data AbsDmd
+  = Abs                  -- Definitely unused
+                         -- Bottom of the lattice
+
+  | UCall AbsDmd         -- Call demand for absence
+                         -- Used only for values of function type
+
+  | UProd [AbsDmd]       -- Product 
+                         -- Used only for values of product type
+                         -- See Note [Don't optimise UProd(Used) to Used]
+                         -- [Invariant] Not all components are Abs
+                         --             (in that case, use UHead)
+
+  | UHead                -- May be used; but its sub-components are 
+                         -- definitely *not* used.  
+                         -- Eg the usage of x in x `seq` e
+                         -- A polymorphic demand: used for values of all types,
+                         --                       including a type variable
+
+  | Used                 -- May be used; and its sub-components may be used
+                         -- Top of the lattice
+  deriving ( Eq, Show )
+
+
+-- Pretty-printing
+instance Outputable AbsDmd where
+  ppr Abs         = char 'A'
+  ppr Used        = char 'U'
+  ppr (UCall a)   = char 'C' <> parens (ppr a)
+  ppr UHead       = char 'H'
+  ppr (UProd as)  = (char 'U') <> parens (hcat (map ppr as))
+
+-- Well-formedness preserving constructors for the Absence domain
+absBot, absTop, absHead :: AbsDmd
+absBot     = Abs
+absHead    = UHead
+absTop     = Used
+
+absCall :: AbsDmd -> AbsDmd
+absCall Used = Used 
+absCall Abs  = Abs 
+absCall a    = UCall a
+
+absProd :: [AbsDmd] -> AbsDmd
+absProd ux 
+--  | all (== Used) ux   = Used
+  | all (== Abs) ux    = UHead
+  | otherwise          = UProd ux
+
+instance LatticeLike AbsDmd where
+  bot                            = absBot
+  top                            = absTop
+ 
+  pre Abs _                      = True
+  pre _ Used                     = True
+  pre UHead (UProd _)            = True
+  pre (UCall u1) (UCall u2)      = pre u1 u2
+  pre (UProd ux1) (UProd ux2)
+     | length ux1 == length ux2  = all (== True) $ zipWith pre ux1 ux2 
+  pre x y                        = x == y
+
+  lub x y | x == y               = x 
+  lub y x | x `pre` y            = lub x y
+  lub Abs a                      = a
+  lub a Abs                      = a
+  lub UHead u                    = u
+  lub u UHead                    = u
+  lub (UProd ux1) (UProd ux2)
+     | length ux1 == length ux2  = absProd $ zipWith lub ux1 ux2
+  lub (UCall u1) (UCall u2)      = absCall (u1 `lub` u2)
+  lub (UProd ds) Used            = UProd (map (`lub` Used) ds)
+  lub Used (UProd ds)            = UProd (map (`lub` Used) ds)
+  lub _ _                        = Used
+
+  both                           = lub
+
+-- utility functions
+seqAbsDmd :: AbsDmd -> ()
+seqAbsDmd (UProd ds) = seqAbsDmdList ds
+seqAbsDmd (UCall d)  = seqAbsDmd d
+seqAbsDmd _          = ()
+
+seqAbsDmdList :: [AbsDmd] -> ()
+seqAbsDmdList [] = ()
+seqAbsDmdList (d:ds) = seqAbsDmd d `seq` seqAbsDmdList ds
+
+-- Splitting polymorphic demands
+splitAbsProdDmd :: Int -> AbsDmd -> [AbsDmd]
+splitAbsProdDmd n Abs        = replicate n Abs
+splitAbsProdDmd n Used       = replicate n Used
+splitAbsProdDmd n UHead      = replicate n Abs
+splitAbsProdDmd n (UProd ds) = ASSERT( ds `lengthIs` n ) ds
+splitAbsProdDmd n (UCall d)  = ASSERT( n == 1 ) [d]
+\end{code}
+  
+%************************************************************************
+%*                                                                      *
+\subsection{Joint domain for Strictness and Absence}
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+
+data JointDmd = JD { strd :: StrDmd, absd :: AbsDmd } 
+  deriving ( Eq, Show )
+
+-- Pretty-printing
+instance Outputable JointDmd where
+  ppr (JD {strd = s, absd = a}) = angleBrackets (ppr s <> char ',' <> ppr a)
+
+-- Well-formedness preserving constructors for the joint domain
+mkJointDmd :: StrDmd -> AbsDmd -> JointDmd
+mkJointDmd s a = JD { strd = s, absd = a }
+-- = case (s, a) of 
+--     (HyperStr, UProd _) -> JD {strd = HyperStr, absd = Used}
+--     _                   -> JD {strd = s, absd = a}
+
+mkJointDmds :: [StrDmd] -> [AbsDmd] -> [JointDmd]
+mkJointDmds ss as = zipWithEqual "mkJointDmds" mkJointDmd ss as
+
+mkProdDmd :: [JointDmd] -> JointDmd
+mkProdDmd dx 
+  = mkJointDmd sp up 
+  where
+    sp = strProd $ map strd dx
+    up = absProd $ map absd dx   
+     
+instance LatticeLike JointDmd where
+  bot  = botDmd
+  top  = topDmd
+  pre  = preDmd
+  lub  = lubDmd
+  both = bothDmd
+
+absDmd :: JointDmd
+absDmd = mkJointDmd top bot 
+
+topDmd :: JointDmd
+topDmd = mkJointDmd top top
+
+botDmd :: JointDmd
+botDmd = mkJointDmd bot bot
+
+preDmd :: JointDmd -> JointDmd -> Bool
+preDmd (JD {strd = s1, absd = a1}) 
+       (JD {strd = s2, absd = a2})  = pre s1 s2 && pre a1 a2
+
+lubDmd :: JointDmd -> JointDmd -> JointDmd
+lubDmd (JD {strd = s1, absd = a1}) 
+       (JD {strd = s2, absd = a2}) = mkJointDmd (lub s1 s2) (lub a1 a2)
+
+bothDmd :: JointDmd -> JointDmd -> JointDmd
+bothDmd (JD {strd = s1, absd = a1}) 
+        (JD {strd = s2, absd = a2}) = mkJointDmd (both s1 s2) (both a1 a2)
+
+isTopDmd :: JointDmd -> Bool
+isTopDmd (JD {strd = Lazy, absd = Used}) = True
+isTopDmd _                               = False 
+
+isBotDmd :: JointDmd -> Bool
+isBotDmd (JD {strd = HyperStr, absd = Abs}) = True
+isBotDmd _                                  = False 
+  
+isAbsDmd :: JointDmd -> Bool
+isAbsDmd (JD {absd = Abs})  = True   -- The strictness part can be HyperStr 
+isAbsDmd _                  = False  -- for a bottom demand
+
+isSeqDmd :: JointDmd -> Bool
+isSeqDmd (JD {strd=Str, absd=UHead}) = True
+isSeqDmd _                           = False
+
+-- More utility functions for strictness
+seqDemand :: JointDmd -> ()
+seqDemand (JD {strd = x, absd = y}) = x `seq` y `seq` ()
+
+seqDemandList :: [JointDmd] -> ()
 seqDemandList [] = ()
 seqDemandList (d:ds) = seqDemand d `seq` seqDemandList ds
 
-instance Outputable Demand where
-    ppr Top  = char 'T'
-    ppr Abs  = char 'A'
-    ppr Bot  = char 'B'
-
-    ppr (Defer ds)      = char 'D' <> ppr ds
-    ppr (Eval ds)       = char 'U' <> ppr ds
-				      
-    ppr (Box (Eval ds)) = char 'S' <> ppr ds
-    ppr (Box Abs)	= char 'L'
-    ppr (Box Bot)	= char 'X'
-    ppr d@(Box _)	= pprPanic "ppr: Bad boxed demand" (ppr d)
-
-    ppr (Call d)	= char 'C' <> parens (ppr d)
-
-
-instance Outputable Demands where
-    ppr (Poly Abs) = empty
-    ppr (Poly d)   = parens (ppr d <> char '*')
-    ppr (Prod ds)  = parens (hcat (map ppr ds))
-	-- At one time I printed U(AAA) as U, but that
-	-- confuses (Poly Abs) with (Prod AAA), and the
-	-- worker/wrapper generation differs slightly for these two
-	-- [Reason: in the latter case we can avoid passing the arg;
-	--  see notes with WwLib.mkWWstr_one.]
+isStrictDmd :: Demand -> Bool
+isStrictDmd (JD {strd = x}) = x /= top
+
+isUsedDmd :: Demand -> Bool
+isUsedDmd (JD {absd = x}) = x /= bot
+
+isUsed :: AbsDmd -> Bool
+isUsed x = x /= bot
+
+someCompUsed :: AbsDmd -> Bool
+someCompUsed Used      = True
+someCompUsed (UProd _) = True
+someCompUsed _         = False
+
+evalDmd :: JointDmd
+-- Evaluated strictly, and used arbitrarily deeply
+evalDmd = mkJointDmd strStr absTop
+
+defer :: Demand -> Demand
+defer (JD {absd = a}) = mkJointDmd top a 
+
+-- use :: Demand -> Demand
+-- use (JD {strd = d}) = mkJointDmd d top
 \end{code}
 
+Note [Dealing with call demands]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Call demands are constructed and deconstructed coherently for
+strictness and absence. For instance, the strictness signature for the
+following function
+
+f :: (Int -> (Int, Int)) -> (Int, Bool)
+f g = (snd (g 3), True)
+
+should be: <L,C(U(AU))>m
+
+\begin{code}
+mkCallDmd :: JointDmd -> JointDmd
+mkCallDmd (JD {strd = d, absd = a}) 
+          = mkJointDmd (strCall d) (absCall a)
+
+peelCallDmd :: JointDmd -> Maybe JointDmd
+-- Exploiting the fact that 
+-- on the strictness side      C(B) = B
+-- and on the usage side       C(U) = U 
+peelCallDmd (JD {strd = s, absd = u}) 
+  | Just s' <- peel_s s
+  , Just u' <- peel_u u
+  = Just $ mkJointDmd s' u'
+  | otherwise
+  = Nothing
+  where
+    peel_s (SCall s) = Just s
+    peel_s HyperStr  = Just HyperStr
+    peel_s _         = Nothing
+
+    peel_u (UCall u) = Just u
+    peel_u Used      = Just Used
+    peel_u Abs       = Just Abs
+    peel_u UHead     = Just Abs
+    peel_u _         = Nothing    
+
+splitCallDmd :: JointDmd -> (Int, JointDmd)
+splitCallDmd (JD {strd = SCall d, absd = UCall a}) 
+  = case splitCallDmd (mkJointDmd d a) of
+      (n, r) -> (n + 1, r)
+-- Exploiting the fact that C(U) === U
+splitCallDmd (JD {strd = SCall d, absd = Used}) 
+  = case splitCallDmd (mkJointDmd d Used) of
+      (n, r) -> (n + 1, r)
+splitCallDmd d        = (0, d)
+
+vanillaCall :: Arity -> Demand
+vanillaCall 0 = evalDmd
+vanillaCall n =
+  -- generate S^n (S)  
+  let strComp = (iterate strCall strStr) !! n
+      absComp = (iterate absCall absTop) !! n
+   in mkJointDmd strComp absComp
+\end{code}
+
+Note [Replicating polymorphic demands]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Some demands can be considered as polymorphic. Generally, it is
+applicable to such beasts as tops, bottoms as well as Head-Used adn
+Head-stricts demands. For instance,
+
+S ~ S(L, ..., L)
+
+Also, when top or bottom is occurred as a result demand, it in fact
+can be expanded to saturate a callee's arity. 
+
+
+\begin{code}
+splitProdDmd :: Int -> Demand -> [Demand]
+-- Split a product demands into its components, 
+-- regardless of whether it has juice in it
+-- The demand is not ncessarily strict
+splitProdDmd n (JD {strd=x, absd=y}) 
+  = mkJointDmds (splitStrProdDmd n x) (splitAbsProdDmd n y)
+
+splitProdDmd_maybe :: Demand -> Maybe [Demand]
+-- Split a product into its components, iff there is any
+-- useful information to be extracted thereby
+-- The demand is not necessarily strict!
+splitProdDmd_maybe JD {strd=SProd sx, absd=UProd ux}
+  = ASSERT( sx `lengthIs` length ux ) 
+    Just (mkJointDmds sx ux)
+splitProdDmd_maybe JD {strd=SProd sx, absd=u} 
+  = Just (mkJointDmds sx (splitAbsProdDmd (length sx) u))
+splitProdDmd_maybe (JD {strd=s, absd=UProd ux})
+  = Just (mkJointDmds (splitStrProdDmd (length ux) s) ux)
+splitProdDmd_maybe _ = Nothing
+
+-- Check whether is a product demand with *some* useful info inside
+-- The demand is not ncessarily strict
+isProdDmd :: Demand -> Bool
+isProdDmd (JD {strd = SProd _}) = True
+isProdDmd (JD {absd = UProd _}) = True
+isProdDmd _                     = False
+\end{code}
 
 %************************************************************************
-%*									*
-\subsection{Demand types}
-%*									*
+%*                                                                      *
+\subsection{Demand results}
+%*                                                                      *
 %************************************************************************
 
 \begin{code}
-data DmdType = DmdType 
-		    DmdEnv	-- Demand on explicitly-mentioned 
-				--	free variables
-		    [Demand]	-- Demand on arguments
-		    DmdResult	-- Nature of result
 
-	-- 		IMPORTANT INVARIANT
-	-- The default demand on free variables not in the DmdEnv is:
-	-- DmdResult = BotRes        <=>  Bot
-	-- DmdResult = TopRes/ResCPR <=>  Abs
+------------------------------------------------------------------------
+-- Pure demand result                                             
+------------------------------------------------------------------------
+
+data PureResult = TopRes        -- Nothing known, assumed to be just lazy
+                | BotRes        -- Diverges or errors
+               deriving( Eq, Show )
+
+instance LatticeLike PureResult where
+     bot = BotRes
+     top = TopRes
+     pre x y = (x == y) || (y == top)
+     lub x y | x == y = x 
+     lub _ _          = top
+     both x y | x == y = x 
+     both _ _          = bot
+
+
+------------------------------------------------------------------------
+-- Constructed Product Result                                             
+------------------------------------------------------------------------
+
+data CPRResult = NoCPR
+               | RetCPR
+               deriving( Eq, Show )
+
+instance LatticeLike CPRResult where
+     bot = RetCPR
+     top = NoCPR
+     pre x y = (x == y) || (y == top)
+     lub x y | x == y  = x 
+     lub _ _           = top
+     both x y | x == y = x 
+     both _ _          = bot
+
+------------------------------------------------------------------------
+-- Combined demand result                                             --
+------------------------------------------------------------------------
+
+data DmdResult = DR { res :: PureResult, cpr :: CPRResult }
+     deriving ( Eq )
+
+-- TODO rework DmdResult to make it more clear
+instance LatticeLike DmdResult where
+  bot                        = botRes
+  top                        = topRes
+
+  pre x _ | x == bot         = True
+  pre _ x | x == top         = True
+  pre (DR s1 a1) (DR s2 a2)  = (pre s1 s2) && (pre a1 a2)
+
+  lub  r r' | isBotRes r                   = r'
+  lub  r r' | isBotRes r'                  = r
+  lub  r r' 
+        | returnsCPR r && returnsCPR r'    = r
+  lub  _ _                                 = top
+
+  both _ r2 | isBotRes r2 = r2
+  both r1 _               = r1
+
+-- Pretty-printing
+instance Outputable DmdResult where
+  ppr (DR {res=TopRes, cpr=RetCPR}) = char 'm'   --    DDDr without ambiguity
+  ppr (DR {res=BotRes}) = char 'b'   
+  ppr _ = empty   -- Keep these distinct from Demand letters
 
-	-- 		ANOTHER IMPORTANT INVARIANT
-	-- The Demands in the argument list are never
-	--	Bot, Defer d
-	-- Handwavey reason: these don't correspond to calling conventions
-	-- See DmdAnal.funArgDemand for details
+mkDmdResult :: PureResult -> CPRResult -> DmdResult
+mkDmdResult BotRes RetCPR = botRes
+mkDmdResult x y = DR {res=x, cpr=y}
 
+seqDmdResult :: DmdResult -> ()
+seqDmdResult (DR {res=x, cpr=y}) = x `seq` y `seq` ()
 
--- This guy lets us switch off CPR analysis
+-- [cprRes] lets us switch off CPR analysis
 -- by making sure that everything uses TopRes instead of RetCPR
 -- Assuming, of course, that they don't mention RetCPR by name.
 -- They should onlyu use retCPR
-retCPR :: DmdResult
-retCPR | opt_CprOff = TopRes
-       | otherwise  = RetCPR
+topRes, botRes, cprRes :: DmdResult
+topRes = mkDmdResult TopRes NoCPR
+botRes = mkDmdResult BotRes NoCPR
+cprRes | opt_CprOff = topRes
+       | otherwise  = mkDmdResult TopRes RetCPR
 
-seqDmdType :: DmdType -> ()
-seqDmdType (DmdType _env ds res) = 
-  {- ??? env `seq` -} seqDemandList ds `seq` res `seq` ()
+isTopRes :: DmdResult -> Bool
+isTopRes (DR {res=TopRes, cpr=NoCPR})  = True
+isTopRes _                  = False
+
+isBotRes :: DmdResult -> Bool
+isBotRes (DR {res=BotRes})      = True
+isBotRes _                  = False
+
+returnsCPR :: DmdResult -> Bool
+returnsCPR (DR {res=TopRes, cpr=RetCPR}) = True
+returnsCPR _                  = False
+
+resTypeArgDmd :: DmdResult -> Demand
+-- TopRes and BotRes are polymorphic, so that
+--      BotRes === Bot -> BotRes === ...
+--      TopRes === Top -> TopRes === ...
+-- This function makes that concrete
+resTypeArgDmd r | isBotRes r = bot
+resTypeArgDmd _              = top
+\end{code}
+
+%************************************************************************
+%*                                                                      *
+            Whether a demand justifies a w/w split
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+worthSplittingFun :: [Demand] -> DmdResult -> Bool
+                -- True <=> the wrapper would not be an identity function
+worthSplittingFun ds res
+  = any worth_it ds || returnsCPR res
+        -- worthSplitting returns False for an empty list of demands,
+        -- and hence do_strict_ww is False if arity is zero and there is no CPR
+  where
+    -- See Note [Worker-wrapper for bottoming functions]
+    worth_it (JD {strd=HyperStr, absd=a})     = isUsed a  -- A Hyper-strict argument, safe to do W/W
+    -- See Note [Worthy functions for Worker-Wrapper split]    
+    worth_it (JD {absd=Abs})                  = True      -- Absent arg
+    worth_it (JD {strd=SProd _})              = True      -- Product arg to evaluate
+    worth_it (JD {strd=Str, absd=UProd _})    = True      -- Strictly used product arg
+    worth_it (JD {strd=Str, absd=UHead})      = True 
+    worth_it _                                = False
+
+worthSplittingThunk :: Demand           -- Demand on the thunk
+                    -> DmdResult        -- CPR info for the thunk
+                    -> Bool
+worthSplittingThunk dmd res
+  = worth_it dmd || returnsCPR res
+  where
+        -- Split if the thing is unpacked
+    worth_it (JD {strd=SProd _, absd=a})   = someCompUsed a
+    worth_it (JD {strd=Str, absd=UProd _}) = True   
+        -- second component points out that at least some of     
+    worth_it _                             = False
+\end{code}
+
+Note [Worthy functions for Worker-Wrapper split]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+For non-bottoming functions a worker-wrapper transformation takes into
+account several possibilities to decide if the function is worthy for
+splitting:
+
+1. The result is of product type and the function is strict in some
+(or even all) of its arguments. The check that the argument is used is
+more of sanity nature, since strictness implies usage. Example:
+
+f :: (Int, Int) -> Int
+f p = (case p of (a,b) -> a) + 1
+
+should be splitted to
+
+f :: (Int, Int) -> Int
+f p = case p of (a,b) -> $wf a
+
+$wf :: Int -> Int
+$wf a = a + 1
+
+2. Sometimes it also makes sense to perform a WW split if the
+strictness analysis cannot say for sure if the function is strict in
+components of its argument. Then we reason according to the inferred
+usage information: if the function uses its product argument's
+components, the WW split can be beneficial. Example:
+
+g :: Bool -> (Int, Int) -> Int
+g c p = case p of (a,b) -> 
+          if c then a else b
+
+The function g is strict in is argument p and lazy in its
+components. However, both components are used in the RHS. The idea is
+since some of the components (both in this case) are used in the
+right-hand side, the product must presumable be taken apart.
+
+Therefore, the WW transform splits the function g to
+
+g :: Bool -> (Int, Int) -> Int
+g c p = case p of (a,b) -> $wg c a b
+
+$wg :: Bool -> Int -> Int -> Int
+$wg c a b = if c then a else b
+
+3. If an argument is absent, it would be silly to pass it to a
+function, hence the worker with reduced arity is generated.
+
+
+Note [Worker-wrapper for bottoming functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We used not to split if the result is bottom.
+[Justification:  there's no efficiency to be gained.]
+
+But it's sometimes bad not to make a wrapper.  Consider
+        fw = \x# -> let x = I# x# in case e of
+                                        p1 -> error_fn x
+                                        p2 -> error_fn x
+                                        p3 -> the real stuff
+The re-boxing code won't go away unless error_fn gets a wrapper too.
+[We don't do reboxing now, but in general it's better to pass an
+unboxed thing to f, and have it reboxed in the error cases....]
+
+
+%************************************************************************
+%*                                                                      *
+\subsection{Demand environments and types}
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+type Demand = JointDmd
 
 type DmdEnv = VarEnv Demand
 
-data DmdResult = TopRes	-- Nothing known	
-	       | RetCPR	-- Returns a constructed product
-	       | BotRes	-- Diverges or errors
-	       deriving( Eq, Show )
-	-- Equality for fixpoints
-	-- Show needed for Show in Lex.Token (sigh)
+data DmdType = DmdType 
+                  DmdEnv        -- Demand on explicitly-mentioned 
+                                --      free variables
+                  [Demand]      -- Demand on arguments
+                  DmdResult     -- Nature of result
+\end{code}
+
+Note [Nature of result demand]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We assume the result in a demand type to be either a top or bottom
+in order to represent the information about demand on the function
+result, imposed by its definition. There are not so many things we 
+can say, though. 
+
+For instance, one can consider a function
+
+        h = \v -> error "urk"
+
+Taking the definition of strictness, we can easily see that 
+
+        h undefined = undefined
 
+that is, h is strict in v. However, v is not used somehow in the body
+of h How can we know that h is strict in v? In fact, we know it by
+considering a result demand of error and bottom and unleashing it on
+all the variables in scope at a call site (in this case, this is only
+v). We can also consider a case
+
+       h = \v -> f x
+
+where we know that the result of f is not hyper-strict (i.e, it is
+lazy, or top). So, we put the same demand on v, which allow us to
+infer a lazy demand that h puts on v.
+
+Note [Asymmetry of 'both' for DmdType and DmdResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+'both' for DmdTypes is *assymetrical*, because there is only one
+result!  For example, given (e1 e2), we get a DmdType dt1 for e1, use
+its arg demand to analyse e2 giving dt2, and then do (dt1 `both` dt2).
+
+
+\begin{code}
 -- Equality needed for fixpoints in DmdAnal
 instance Eq DmdType where
   (==) (DmdType fv1 ds1 res1)
        (DmdType fv2 ds2 res2) =  ufmToList fv1 == ufmToList fv2
-			      && ds1 == ds2 && res1 == res2
+                              && ds1 == ds2 && res1 == res2
+
+instance LatticeLike DmdType where
+  bot  = botDmdType
+  top  = topDmdType
+  pre  = preDmdType
+  lub  = lubDmdType
+  both = bothDmdType
+
+preDmdType :: DmdType -> DmdType -> Bool
+preDmdType (DmdType _ ds1 res1) (DmdType _ ds2 res2)
+  =  (res1 `pre` res2)
+  && (length ds1 == length ds2)
+  && all (\(x, y) -> x `pre` y) (zip ds1 ds2)
+
+lubDmdType :: DmdType -> DmdType -> DmdType
+lubDmdType (DmdType fv1 ds1 r1) (DmdType fv2 ds2 r2)
+  = DmdType lub_fv2 (lub_ds ds1 ds2) (r1 `lub` r2)
+  where
+    absLub  = lub absDmd
+    lub_fv  = plusVarEnv_C lub fv1 fv2
+    -- Consider (if x then y else []) with demand V
+    -- Then the first branch gives {y->V} and the second
+    -- *implicitly* has {y->A}.  So we must put {y->(V `lub` A)}
+    -- in the result env.
+    lub_fv1 = modifyEnv (not (isBotRes r1)) absLub fv2 fv1 lub_fv
+    lub_fv2 = modifyEnv (not (isBotRes r2)) absLub fv1 fv2 lub_fv1
+      -- lub is the identity for Bot
+
+      -- Extend the shorter argument list to match the longer
+    lub_ds (d1:ds1) (d2:ds2) = lub d1 d2 : lub_ds ds1 ds2
+    lub_ds []     []       = []
+    lub_ds ds1    []       = map (`lub` resTypeArgDmd r2) ds1
+    lub_ds []     ds2      = map (resTypeArgDmd r1 `lub`) ds2
+ 
+bothDmdType :: DmdType -> DmdType -> DmdType
+bothDmdType (DmdType fv1 ds1 r1) (DmdType fv2 _ r2)
+    -- See Note [Asymmetry of 'both' for DmdType and DmdResult]
+    -- 'both' takes the argument/result info from its *first* arg,
+    -- using its second arg just for its free-var info.
+    -- NB: Don't forget about r2!  It might be BotRes, which is
+    -- a bottom demand on all the in-scope variables.
+  = DmdType both_fv2 ds1 (r1 `both` r2)
+  where
+    both_fv  = plusVarEnv_C both fv1 fv2
+    both_fv1 = modifyEnv (isBotRes r1) (`both` bot) fv2 fv1 both_fv
+    both_fv2 = modifyEnv (isBotRes r2) (`both` bot) fv1 fv2 both_fv1
+
 
 instance Outputable DmdType where
   ppr (DmdType fv ds res) 
     = hsep [text "DmdType",
-	    hcat (map ppr ds) <> ppr res,
-	    if null fv_elts then empty
-	    else braces (fsep (map pp_elt fv_elts))]
+            hcat (map ppr ds) <> ppr res,
+            if null fv_elts then empty
+            else braces (fsep (map pp_elt fv_elts))]
     where
       pp_elt (uniq, dmd) = ppr uniq <> text "->" <> ppr dmd
       fv_elts = ufmToList fv
 
-instance Outputable DmdResult where
-  ppr TopRes = empty	  -- Keep these distinct from Demand letters
-  ppr RetCPR = char 'm'	  -- so that we can print strictness sigs as
-  ppr BotRes = char 'b'   --    dddr
-			  -- without ambiguity
-
 emptyDmdEnv :: VarEnv Demand
 emptyDmdEnv = emptyVarEnv
 
 topDmdType, botDmdType, cprDmdType :: DmdType
-topDmdType = DmdType emptyDmdEnv [] TopRes
-botDmdType = DmdType emptyDmdEnv [] BotRes
-cprDmdType = DmdType emptyVarEnv [] retCPR
+topDmdType = DmdType emptyDmdEnv [] topRes
+botDmdType = DmdType emptyDmdEnv [] botRes
+cprDmdType = DmdType emptyDmdEnv [] cprRes
 
 isTopDmdType :: DmdType -> Bool
--- Only used on top-level types, hence the assert
-isTopDmdType (DmdType env [] TopRes) = ASSERT( isEmptyVarEnv env) True	
-isTopDmdType _                       = False
-
-isBotRes :: DmdResult -> Bool
-isBotRes BotRes = True
-isBotRes _      = False
-
-resTypeArgDmd :: DmdResult -> Demand
--- TopRes and BotRes are polymorphic, so that
---	BotRes = Bot -> BotRes
---	TopRes = Top -> TopRes
--- This function makes that concrete
--- We can get a RetCPR, because of the way in which we are (now)
--- giving CPR info to strict arguments.  On the first pass, when
--- nothing has demand info, we optimistically give CPR info or RetCPR to all args
-resTypeArgDmd TopRes = Top
-resTypeArgDmd RetCPR = Top
-resTypeArgDmd BotRes = Bot
-
-returnsCPR :: DmdResult -> Bool
-returnsCPR RetCPR = True
-returnsCPR _      = False
+isTopDmdType (DmdType env [] res)
+             | isTopRes res && isEmptyVarEnv env = True
+isTopDmdType _                                   = False
 
 mkDmdType :: DmdEnv -> [Demand] -> DmdResult -> DmdType
 mkDmdType fv ds res = DmdType fv ds res
@@ -264,43 +869,80 @@ mkTopDmdType ds res = DmdType emptyDmdEnv ds res
 
 dmdTypeDepth :: DmdType -> Arity
 dmdTypeDepth (DmdType _ ds _) = length ds
-\end{code}
 
+seqDmdType :: DmdType -> ()
+seqDmdType (DmdType _env ds res) = 
+  {- ??? env `seq` -} seqDemandList ds `seq` seqDmdResult res `seq` ()
+
+splitDmdTy :: DmdType -> (Demand, DmdType)
+-- Split off one function argument
+-- We already have a suitable demand on all
+-- free vars, so no need to add more!
+splitDmdTy (DmdType fv (dmd:dmds) res_ty) = (dmd, DmdType fv dmds res_ty)
+splitDmdTy ty@(DmdType _ [] res_ty)       = (resTypeArgDmd res_ty, ty)
+
+deferType :: DmdType -> DmdType
+deferType (DmdType fv _ _) = DmdType (deferEnv fv) [] top
+
+deferEnv :: DmdEnv -> DmdEnv
+deferEnv fv = mapVarEnv defer fv
+
+modifyEnv :: Bool                       -- No-op if False
+          -> (Demand -> Demand)         -- The zapper
+          -> DmdEnv -> DmdEnv           -- Env1 and Env2
+          -> DmdEnv -> DmdEnv           -- Transform this env
+        -- Zap anything in Env1 but not in Env2
+        -- Assume: dom(env) includes dom(Env1) and dom(Env2)
+modifyEnv need_to_modify zapper env1 env2 env
+  | need_to_modify = foldr zap env (varEnvKeys (env1 `minusUFM` env2))
+  | otherwise      = env
+  where
+    zap uniq env = addToUFM_Directly env uniq (zapper current_val)
+                 where
+                   current_val = expectJust "modifyEnv" (lookupUFM_Directly env uniq)
+
+\end{code}
 
 %************************************************************************
-%*									*
-\subsection{Strictness signature
-%*									*
+%*                                                                      *
+                     Demand signatures
+%*                                                                      *
 %************************************************************************
 
 In a let-bound Id we record its strictness info.  
 In principle, this strictness info is a demand transformer, mapping
 a demand on the Id into a DmdType, which gives
-	a) the free vars of the Id's value
-	b) the Id's arguments
-	c) an indication of the result of applying 
-	   the Id to its arguments
+        a) the free vars of the Id's value
+        b) the Id's arguments
+        c) an indication of the result of applying 
+           the Id to its arguments
 
 However, in fact we store in the Id an extremely emascuated demand transfomer,
 namely 
-		a single DmdType
+                a single DmdType
 (Nevertheless we dignify StrictSig as a distinct type.)
 
 This DmdType gives the demands unleashed by the Id when it is applied
 to as many arguments as are given in by the arg demands in the DmdType.
 
+If an Id is applied to less arguments than its arity, it means that
+the demand on the function at a call site is weaker than the vanilla
+call demand, used for signature inference. Therefore we place a top
+demand on all arguments. Otherwise, the demand is specified by Id's
+signature.
+
 For example, the demand transformer described by the DmdType
-		DmdType {x -> U(LL)} [V,A] Top
+                DmdType {x -> <S(LL),U(UU)>} [V,A] Top
 says that when the function is applied to two arguments, it
-unleashes demand U(LL) on the free var x, V on the first arg,
+unleashes demand <S(LL),U(UU)> on the free var x, V on the first arg,
 and A on the second.  
 
-If this same function is applied to one arg, all we can say is
-that it uses x with U*(LL), and its arg with demand L.
+If this same function is applied to one arg, all we can say is that it
+uses x with <L,U>, and its arg with demand <L,U>.
 
 \begin{code}
 newtype StrictSig = StrictSig DmdType
-		  deriving( Eq )
+                  deriving( Eq )
 
 instance Outputable StrictSig where
    ppr (StrictSig ty) = ppr ty
@@ -314,33 +956,180 @@ splitStrictSig (StrictSig (DmdType _ dmds res)) = (dmds, res)
 increaseStrictSigArity :: Int -> StrictSig -> StrictSig
 -- Add extra arguments to a strictness signature
 increaseStrictSigArity arity_increase (StrictSig (DmdType env dmds res))
-  = StrictSig (DmdType env (replicate arity_increase topDmd ++ dmds) res)
+  = StrictSig (DmdType env (replicate arity_increase top ++ dmds) res)
 
 isTopSig :: StrictSig -> Bool
 isTopSig (StrictSig ty) = isTopDmdType ty
 
-topSig, botSig, cprSig :: StrictSig
+isBottomingSig :: StrictSig -> Bool
+isBottomingSig (StrictSig (DmdType _ _ res)) = isBotRes res
+
+topSig, botSig, cprSig:: StrictSig
 topSig = StrictSig topDmdType
 botSig = StrictSig botDmdType
 cprSig = StrictSig cprDmdType
-	
+
+dmdTransformSig :: StrictSig -> Demand -> DmdType
+-- (dmdTransformSig fun_sig dmd) considers a call to a function whose
+-- signature is fun_sig, with demand dmd.  We return the demand
+-- that the function places on its context (eg its args)
+dmdTransformSig (StrictSig dmd_ty@(DmdType _ arg_ds _)) dmd
+  = go arg_ds dmd
+  where
+    go [] dmd 
+      | isBotDmd dmd = bot     -- Transform bottom demand to bottom type
+      | otherwise    = dmd_ty  -- Saturated
+    go (_:as) dmd    = case peelCallDmd dmd of
+                        Just dmd' -> go as dmd'
+                        Nothing   -> deferType dmd_ty
+        -- NB: it's important to use deferType, and not just return topDmdType
+        -- Consider     let { f x y = p + x } in f 1
+        -- The application isn't saturated, but we must nevertheless propagate 
+        --      a lazy demand for p!  
+
+dmdTransformDataConSig :: Arity -> StrictSig -> Demand -> DmdType
+-- Same as dmdTranformSig but for a data constructor (worker), 
+-- which has a special kind of demand transformer.
+-- If the constructor is saturated, we feed the demand on 
+-- the result into the constructor arguments.
+dmdTransformDataConSig arity (StrictSig (DmdType _ _ con_res)) dmd
+  = go arity dmd
+  where
+    go 0 dmd = DmdType emptyDmdEnv (splitProdDmd arity dmd) con_res
+                -- Must remember whether it's a product, hence con_res, not TopRes
+    go n dmd = case peelCallDmd dmd of
+                 Nothing   -> topDmdType
+                 Just dmd' -> go (n-1) dmd'
+\end{code}
+
+Note [Non-full application] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+
+If a function having bottom as its demand result is applied to a less
+number of arguments than its syntactic arity, we cannot say for sure
+that it is going to diverge. This is the reason why we use the
+function appIsBottom, which, given a strictness signature and a number
+of arguments, says conservatively if the function is going to diverge
+or not.
+
+\begin{code}
 
 -- appIsBottom returns true if an application to n args would diverge
 appIsBottom :: StrictSig -> Int -> Bool
-appIsBottom (StrictSig (DmdType _ ds BotRes)) n = listLengthCmp ds n /= GT
-appIsBottom _				      _ = False
-
-isBottomingSig :: StrictSig -> Bool
-isBottomingSig (StrictSig (DmdType _ _ BotRes)) = True
-isBottomingSig _				= False
+appIsBottom (StrictSig (DmdType _ ds res)) n
+            | isBotRes res                      = not $ lengthExceeds ds n 
+appIsBottom _                                 _ = False
 
 seqStrictSig :: StrictSig -> ()
 seqStrictSig (StrictSig ty) = seqDmdType ty
 
-pprIfaceStrictSig :: StrictSig -> SDoc
 -- Used for printing top-level strictness pragmas in interface files
+pprIfaceStrictSig :: StrictSig -> SDoc
 pprIfaceStrictSig (StrictSig (DmdType _ dmds res))
   = hcat (map ppr dmds) <> ppr res
 \end{code}
-    
 
+
+%************************************************************************
+%*                                                                      *
+                     Serialisation
+%*                                                                      *
+%************************************************************************
+
+
+\begin{code}
+instance Binary StrDmd where
+  put_ bh HyperStr     = do putByte bh 0
+  put_ bh Lazy         = do putByte bh 1
+  put_ bh Str          = do putByte bh 2
+  put_ bh (SCall s)    = do putByte bh 3
+                            put_ bh s
+  put_ bh (SProd sx)   = do putByte bh 4
+                            put_ bh sx  
+  get bh = do 
+         h <- getByte bh
+         case h of
+           0 -> do return strBot
+           1 -> do return strTop
+           2 -> do return strStr
+           3 -> do s  <- get bh
+                   return $ strCall s
+           _ -> do sx <- get bh
+                   return $ strProd sx
+
+instance Binary AbsDmd where
+    put_ bh Abs         = do 
+            putByte bh 0
+    put_ bh Used        = do 
+            putByte bh 1
+    put_ bh UHead       = do 
+            putByte bh 2
+    put_ bh (UCall u)   = do
+            putByte bh 3
+            put_ bh u
+    put_ bh (UProd ux) = do
+            putByte bh 4
+            put_ bh ux
+
+    get  bh = do
+            h <- getByte bh
+            case h of 
+              0 -> return absBot       
+              1 -> return absTop
+              2 -> return absHead
+              3 -> do u  <- get bh
+                      return $ absCall u  
+              _ -> do ux <- get bh
+                      return $ absProd ux
+
+instance Binary JointDmd where
+    put_ bh (JD {strd = x, absd = y}) = do put_ bh x; put_ bh y
+    get  bh = do 
+              x <- get bh
+              y <- get bh
+              return $ mkJointDmd x y
+
+instance Binary PureResult where
+    put_ bh BotRes       = do putByte bh 0
+    put_ bh TopRes       = do putByte bh 1
+
+    get  bh = do
+            h <- getByte bh
+            case h of 
+              0 -> return bot       
+              _ -> return top
+
+instance Binary StrictSig where
+    put_ bh (StrictSig aa) = do
+            put_ bh aa
+    get bh = do
+          aa <- get bh
+          return (StrictSig aa)
+
+instance Binary DmdType where
+  -- Ignore DmdEnv when spitting out the DmdType
+  put_ bh (DmdType _ ds dr) 
+       = do put_ bh ds 
+            put_ bh dr
+  get bh 
+      = do ds <- get bh 
+           dr <- get bh 
+           return (DmdType emptyDmdEnv ds dr)
+
+instance Binary CPRResult where
+    put_ bh RetCPR       = do putByte bh 0
+    put_ bh NoCPR        = do putByte bh 1
+
+    get  bh = do
+            h <- getByte bh
+            case h of 
+              0 -> return bot       
+              _ -> return top
+
+instance Binary DmdResult where
+    put_ bh (DR {res=x, cpr=y}) = do put_ bh x; put_ bh y
+    get  bh = do 
+              x <- get bh
+              y <- get bh
+              return $ mkDmdResult x y
+\end{code}
\ No newline at end of file
diff --git a/compiler/basicTypes/Id.lhs b/compiler/basicTypes/Id.lhs
index cc7d4c58bb..ccd490f0fb 100644
--- a/compiler/basicTypes/Id.lhs
+++ b/compiler/basicTypes/Id.lhs
@@ -38,15 +38,15 @@ module Id (
         recordSelectorFieldLabel,
 
         -- ** Modifying an Id
-        setIdName, setIdUnique, Id.setIdType,
-        setIdExported, setIdNotExported,
-        globaliseId, localiseId,
+        setIdName, setIdUnique, Id.setIdType, 
+        setIdExported, setIdNotExported, 
+        globaliseId, localiseId, 
         setIdInfo, lazySetIdInfo, modifyIdInfo, maybeModifyIdInfo,
         zapLamIdInfo, zapDemandIdInfo, zapFragileIdInfo, transferPolyIdInfo,
-
+        zapIdStrictness,
 
         -- ** Predicates on Ids
-        isImplicitId, isDeadBinder,
+        isImplicitId, isDeadBinder, 
         isStrictId,
         isExportedId, isLocalId, isGlobalId,
         isRecordSelector, isNaughtyRecordSelector,
@@ -69,9 +69,7 @@ module Id (
         setOneShotLambda, clearOneShotLambda,
 
         -- ** Reading 'IdInfo' fields
-        idArity,
-        idDemandInfo, idDemandInfo_maybe,
-        idStrictness, idStrictness_maybe,
+        idArity, 
         idUnfolding, realIdUnfolding,
         idSpecialisation, idCoreRules, idHasRules,
         idCafInfo,
@@ -82,12 +80,17 @@ module Id (
         setIdUnfoldingLazily,
         setIdUnfolding,
         setIdArity,
-        setIdDemandInfo,
-        setIdStrictness, zapIdStrictness,
+
         setIdSpecialisation,
         setIdCafInfo,
         setIdOccInfo, zapIdOccInfo,
 
+        setIdDemandInfo, 
+        setIdStrictness, 
+
+        idDemandInfo, 
+        idStrictness,
+
     ) where
 
 #include "HsVersions.h"
@@ -127,12 +130,14 @@ infixl  1 `setIdUnfoldingLazily`,
           `setIdUnfolding`,
           `setIdArity`,
           `setIdOccInfo`,
-          `setIdDemandInfo`,
-          `setIdStrictness`,
+
           `setIdSpecialisation`,
           `setInlinePragma`,
           `setInlineActivation`,
-          `idCafInfo`
+          `idCafInfo`,
+
+          `setIdDemandInfo`,
+          `setIdStrictness`
 \end{code}
 
 %************************************************************************
@@ -464,17 +469,14 @@ idRepArity x = typeRepArity (idArity x) (idType x)
 isBottomingId :: Id -> Bool
 isBottomingId id = isBottomingSig (idStrictness id)
 
-idStrictness_maybe :: Id -> Maybe StrictSig
 idStrictness :: Id -> StrictSig
-
-idStrictness_maybe id = strictnessInfo (idInfo id)
-idStrictness       id = idStrictness_maybe id `orElse` topSig
+idStrictness id = strictnessInfo (idInfo id)
 
 setIdStrictness :: Id -> StrictSig -> Id
-setIdStrictness id sig = modifyIdInfo (`setStrictnessInfo` Just sig) id
+setIdStrictness id sig = modifyIdInfo (`setStrictnessInfo` sig) id
 
 zapIdStrictness :: Id -> Id
-zapIdStrictness id = modifyIdInfo (`setStrictnessInfo` Nothing) id
+zapIdStrictness id = modifyIdInfo (`setStrictnessInfo` topSig) id
 
 -- | This predicate says whether the 'Id' has a strict demand placed on it or
 -- has a type such that it can always be evaluated strictly (e.g., an
@@ -485,8 +487,9 @@ zapIdStrictness id = modifyIdInfo (`setStrictnessInfo` Nothing) id
 isStrictId :: Id -> Bool
 isStrictId id
   = ASSERT2( isId id, text "isStrictId: not an id: " <+> ppr id )
-           (isStrictDmd (idDemandInfo id)) ||
-           (isStrictType (idType id))
+           (isStrictType (idType id)) ||
+           -- Take the best of both strictnesses - old and new               
+           (isStrictDmd (idDemandInfo id))
 
         ---------------------------------
         -- UNFOLDING
@@ -508,14 +511,11 @@ setIdUnfoldingLazily id unfolding = modifyIdInfo (`setUnfoldingInfoLazily` unfol
 setIdUnfolding :: Id -> Unfolding -> Id
 setIdUnfolding id unfolding = modifyIdInfo (`setUnfoldingInfo` unfolding) id
 
-idDemandInfo_maybe :: Id -> Maybe Demand
 idDemandInfo       :: Id -> Demand
-
-idDemandInfo_maybe id = demandInfo (idInfo id)
-idDemandInfo       id = demandInfo (idInfo id) `orElse` topDmd
+idDemandInfo       id = demandInfo (idInfo id)
 
 setIdDemandInfo :: Id -> Demand -> Id
-setIdDemandInfo id dmd = modifyIdInfo (`setDemandInfo` Just dmd) id
+setIdDemandInfo id dmd = modifyIdInfo (`setDemandInfo` dmd) id
 
         ---------------------------------
         -- SPECIALISATION
@@ -654,11 +654,11 @@ zapInfo zapper id = maybeModifyIdInfo (zapper (idInfo id)) id
 zapLamIdInfo :: Id -> Id
 zapLamIdInfo = zapInfo zapLamInfo
 
+zapFragileIdInfo :: Id -> Id
+zapFragileIdInfo = zapInfo zapFragileInfo 
+
 zapDemandIdInfo :: Id -> Id
 zapDemandIdInfo = zapInfo zapDemandInfo
-
-zapFragileIdInfo :: Id -> Id
-zapFragileIdInfo = zapInfo zapFragileInfo
 \end{code}
 
 Note [transferPolyIdInfo]
@@ -725,11 +725,12 @@ transferPolyIdInfo old_id abstract_wrt new_id
     old_inline_prag = inlinePragInfo old_info
     old_occ_info    = occInfo old_info
     new_arity       = old_arity + arity_increase
+
     old_strictness  = strictnessInfo old_info
-    new_strictness  = fmap (increaseStrictSigArity arity_increase) old_strictness
+    new_strictness  = increaseStrictSigArity arity_increase old_strictness
 
-    transfer new_info = new_info `setStrictnessInfo` new_strictness
-                                 `setArityInfo` new_arity
+    transfer new_info = new_info `setArityInfo` new_arity
                                  `setInlinePragInfo` old_inline_prag
                                  `setOccInfo` old_occ_info
+                                 `setStrictnessInfo` new_strictness
 \end{code}
diff --git a/compiler/basicTypes/IdInfo.lhs b/compiler/basicTypes/IdInfo.lhs
index 1d777895e4..0107e411d0 100644
--- a/compiler/basicTypes/IdInfo.lhs
+++ b/compiler/basicTypes/IdInfo.lhs
@@ -25,7 +25,9 @@ module IdInfo (
 	seqIdInfo, megaSeqIdInfo,
 
 	-- ** Zapping various forms of Info
-	zapLamInfo, zapDemandInfo, zapFragileInfo,
+	zapLamInfo, zapFragileInfo,
+
+        zapDemandInfo,
 
 	-- ** The ArityInfo type
 	ArityInfo,
@@ -82,12 +84,10 @@ import BasicTypes
 import DataCon
 import TyCon
 import ForeignCall
-import Demand
 import Outputable	
 import Module
 import FastString
-
-import Data.Maybe
+import Demand
 
 -- infixl so you can say (id `set` a `set` b)
 infixl 	1 `setSpecInfo`,
@@ -203,14 +203,10 @@ data IdInfo
 	inlinePragInfo	:: InlinePragma,	-- ^ Any inline pragma atached to the 'Id'
 	occInfo		:: OccInfo,		-- ^ How the 'Id' occurs in the program
 
-	strictnessInfo :: Maybe StrictSig,	-- ^ Id strictness information. Reason for Maybe: 
-	                                        -- the DmdAnal phase needs to know whether
-						-- this is the first visit, so it can assign botSig.
-						-- Other customers want topSig.  So @Nothing@ is good.
+        strictnessInfo  :: StrictSig,      --  ^ A strictness signature
+
+        demandInfo      :: Demand        -- ^ ID demand information
 
-	demandInfo	  :: Maybe Demand	-- ^ Id demand information. Similarly we want to know 
-	                                        -- if there's no known demand yet, for when we are looking
-						-- for CPR info
     }
 
 -- | Just evaluate the 'IdInfo' to WHNF
@@ -227,20 +223,18 @@ megaSeqIdInfo info
 -- some unfoldings are not calculated at all
 --    seqUnfolding (unfoldingInfo info)		`seq`
 
-    seqDemandInfo (demandInfo info)	`seq`
+    seqDemandInfo (demandInfo info)         `seq`
     seqStrictnessInfo (strictnessInfo info) `seq`
 
     seqCaf (cafInfo info)			`seq`
     seqLBVar (lbvarInfo info)			`seq`
     seqOccInfo (occInfo info) 
 
-seqStrictnessInfo :: Maybe StrictSig -> ()
-seqStrictnessInfo Nothing = ()
-seqStrictnessInfo (Just ty) = seqStrictSig ty
+seqStrictnessInfo :: StrictSig -> ()
+seqStrictnessInfo ty = seqStrictSig ty
 
-seqDemandInfo :: Maybe Demand -> ()
-seqDemandInfo Nothing    = ()
-seqDemandInfo (Just dmd) = seqDemand dmd
+seqDemandInfo :: Demand -> ()
+seqDemandInfo dmd = seqDemand dmd
 \end{code}
 
 Setters
@@ -275,10 +269,10 @@ setCafInfo        info caf = info { cafInfo = caf }
 setLBVarInfo :: IdInfo -> LBVarInfo -> IdInfo
 setLBVarInfo      info lb = {-lb `seq`-} info { lbvarInfo = lb }
 
-setDemandInfo :: IdInfo -> Maybe Demand -> IdInfo
-setDemandInfo     info dd = dd `seq` info { demandInfo = dd }
+setDemandInfo :: IdInfo -> Demand -> IdInfo
+setDemandInfo info dd = dd `seq` info { demandInfo = dd }
 
-setStrictnessInfo :: IdInfo -> Maybe StrictSig -> IdInfo
+setStrictnessInfo :: IdInfo -> StrictSig -> IdInfo
 setStrictnessInfo info dd = dd `seq` info { strictnessInfo = dd }
 \end{code}
 
@@ -295,8 +289,8 @@ vanillaIdInfo
 	    lbvarInfo		= NoLBVarInfo,
 	    inlinePragInfo 	= defaultInlinePragma,
 	    occInfo		= NoOccInfo,
-	    demandInfo	= Nothing,
-	    strictnessInfo   = Nothing
+            demandInfo	        = topDmd,
+	    strictnessInfo      = topSig
 	   }
 
 -- | More informative 'IdInfo' we can use when we know the 'Id' has no CAF references
@@ -363,9 +357,8 @@ type InlinePragInfo = InlinePragma
 %************************************************************************
 
 \begin{code}
-pprStrictness :: Maybe StrictSig -> SDoc
-pprStrictness Nothing    = empty
-pprStrictness (Just sig) = ppr sig
+pprStrictness :: StrictSig -> SDoc
+pprStrictness sig = ppr sig
 \end{code}
 
 
@@ -524,7 +517,7 @@ zapLamInfo info@(IdInfo {occInfo = occ, demandInfo = demand})
   | is_safe_occ occ && is_safe_dmd demand
   = Nothing
   | otherwise
-  = Just (info {occInfo = safe_occ, demandInfo = Nothing})
+  = Just (info {occInfo = safe_occ, demandInfo = topDmd})
   where
 	-- The "unsafe" occ info is the ones that say I'm not in a lambda
 	-- because that might not be true for an unsaturated lambda
@@ -535,16 +528,13 @@ zapLamInfo info@(IdInfo {occInfo = occ, demandInfo = demand})
 		 OneOcc _ once int_cxt -> OneOcc insideLam once int_cxt
 		 _other	       	       -> occ
 
-    is_safe_dmd Nothing    = True
-    is_safe_dmd (Just dmd) = not (isStrictDmd dmd)
+    is_safe_dmd dmd = not (isStrictDmd dmd)
 \end{code}
 
 \begin{code}
 -- | Remove demand info on the 'IdInfo' if it is present, otherwise return @Nothing@
 zapDemandInfo :: IdInfo -> Maybe IdInfo
-zapDemandInfo info@(IdInfo {demandInfo = dmd})
-  | isJust dmd = Just (info {demandInfo = Nothing})
-  | otherwise  = Nothing
+zapDemandInfo info = Just (info {demandInfo = topDmd})
 \end{code}
 
 \begin{code}
diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index 375e731077..3fdf86dd02 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -230,7 +230,6 @@ Hence we translate to
         -- Coercion from family type to representation type
   Co7T a :: T [a] ~ :R7T a
 
-
 Note [Newtype datacons]
 ~~~~~~~~~~~~~~~~~~~~~~~
 The "data constructor" for a newtype should always be vanilla.  At one
@@ -286,10 +285,10 @@ mkDictSelId dflags no_unf name clas
         -- to get (say)         C a -> (a -> a)
 
     base_info = noCafIdInfo
-                `setArityInfo`      1
-                `setStrictnessInfo` Just strict_sig
-                `setUnfoldingInfo`  (if no_unf then noUnfolding
-	                             else mkImplicitUnfolding dflags rhs)
+                `setArityInfo`         1
+                `setStrictnessInfo`    strict_sig
+                `setUnfoldingInfo`     (if no_unf then noUnfolding
+	                                else mkImplicitUnfolding dflags rhs)
 		   -- In module where class op is defined, we must add
 		   -- the unfolding, even though it'll never be inlined
 		   -- becuase we use that to generate a top-level binding
@@ -318,10 +317,12 @@ mkDictSelId dflags no_unf name clas
         -- where the V depends on which item we are selecting
         -- It's worth giving one, so that absence info etc is generated
         -- even if the selector isn't inlined
-    strict_sig = mkStrictSig (mkTopDmdType [arg_dmd] TopRes)
+
+    strict_sig = mkStrictSig (mkTopDmdType [arg_dmd] topRes)
     arg_dmd | new_tycon = evalDmd
-            | otherwise = Eval (Prod [ if the_arg_id == id then evalDmd else Abs
-                                     | id <- arg_ids ])
+            | otherwise = mkProdDmd [ if the_arg_id == id then evalDmd else absDmd
+                                    | id <- arg_ids ]
+
 
     tycon      	   = classTyCon clas
     new_tycon  	   = isNewTyCon tycon
@@ -384,7 +385,7 @@ mkDataConWorkId wkr_name data_con
     wkr_arity = dataConRepArity data_con
     wkr_info  = noCafIdInfo
                 `setArityInfo`       wkr_arity
-                `setStrictnessInfo`  Just wkr_sig
+                `setStrictnessInfo`  wkr_sig
                 `setUnfoldingInfo`   evaldUnfolding  -- Record that it's evaluated,
                                                      -- even if arity = 0
 
@@ -428,9 +429,9 @@ dataConCPR con
   , isDataTyCon tycon
   , wkr_arity > 0
   , wkr_arity <= mAX_CPR_SIZE
-  = retCPR
+  = cprRes
   | otherwise
-  = TopRes
+  = topRes
         -- RetCPR is only true for products that are real data types;
         -- that is, not unboxed tuples or [non-recursive] newtypes
   where
@@ -486,7 +487,7 @@ mkDataConRep dflags fam_envs wrap_name data_con
                     	     -- applications are treated as values
 		    	 `setInlinePragInfo`    alwaysInlinePragma
                     	 `setUnfoldingInfo`     wrap_unf
-                    	 `setStrictnessInfo`    Just wrap_sig
+                    	 `setStrictnessInfo`    wrap_sig
                     	     -- We need to get the CAF info right here because TidyPgm
                     	     -- does not tidy the IdInfo of implicit bindings (like the wrapper)
                     	     -- so it not make sure that the CAF info is sane
@@ -494,7 +495,7 @@ mkDataConRep dflags fam_envs wrap_name data_con
     	     wrap_sig = mkStrictSig (mkTopDmdType wrap_arg_dmds (dataConCPR data_con))
     	     wrap_arg_dmds = map mk_dmd (dropList eq_spec wrap_bangs)
     	     mk_dmd str | isBanged str = evalDmd
-    	                | otherwise    = lazyDmd
+    	                | otherwise    = topDmd
     	         -- The Cpr info can be important inside INLINE rhss, where the
     	         -- wrapper constructor isn't inlined.
     	         -- And the argument strictness can be important too; we
@@ -599,10 +600,10 @@ dataConArgRep _ _ arg_ty (HsUserBang _ False)  -- No '!'
 dataConArgRep dflags fam_envs arg_ty 
     (HsUserBang unpk_prag True)  -- {-# UNPACK #-} !
   | not (gopt Opt_OmitInterfacePragmas dflags) -- Don't unpack if -fomit-iface-pragmas
-          -- Don't unpack if we aren't optimising; 
-          -- rather arbitrarily, we use -fomit-iface-pragmas
-          -- as the indication
+          -- Don't unpack if we aren't optimising; rather arbitrarily, 
+          -- we use -fomit-iface-pragmas as the indication
   , let mb_co   = topNormaliseType fam_envs arg_ty
+                     -- Unwrap type families and newtypes
         arg_ty' = case mb_co of { Just (_,ty) -> ty; Nothing -> arg_ty }
   , isUnpackableType fam_envs arg_ty'
   , (rep_tys, wrappers) <- dataConArgUnpack arg_ty'
@@ -670,7 +671,10 @@ dataConArgUnpack
 
 dataConArgUnpack arg_ty
   | Just (tc, tc_args) <- splitTyConApp_maybe arg_ty
-  , Just con <- tyConSingleDataCon_maybe tc
+  , Just con <- tyConSingleAlgDataCon_maybe tc
+      -- NB: check for an *algebraic* data type
+      -- A recursive newtype might mean that 
+      -- 'arg_ty' is a newtype
   , let rep_tys = dataConInstArgTys con tc_args
   = ASSERT( isVanillaDataCon con )
     ( rep_tys `zip` dataConRepStrictness con
@@ -698,7 +702,7 @@ isUnpackableType :: FamInstEnvs -> Type -> Bool
 -- end up relying on ourselves!
 isUnpackableType fam_envs ty
   | Just (tc, _) <- splitTyConApp_maybe ty
-  , Just con <- tyConSingleDataCon_maybe tc
+  , Just con <- tyConSingleAlgDataCon_maybe tc
   , isVanillaDataCon con
   = ok_con_args (unitNameSet (getName tc)) con
   | otherwise
@@ -713,7 +717,7 @@ isUnpackableType fam_envs ty
       | Just (tc, _) <- splitTyConApp_maybe ty
       , let tc_name = getName tc
       =  not (tc_name `elemNameSet` tcs)
-      && case tyConSingleDataCon_maybe tc of
+      && case tyConSingleAlgDataCon_maybe tc of
             Just con | isVanillaDataCon con
                     -> ok_con_args (tcs `addOneToNameSet` getName tc) con
             _ -> True
@@ -888,10 +892,10 @@ mkPrimOpId prim_op
     id   = mkGlobalId (PrimOpId prim_op) name ty info
                 
     info = noCafIdInfo
-           `setSpecInfo`       mkSpecInfo (maybeToList $ primOpRules name prim_op)
-           `setArityInfo`      arity
-           `setStrictnessInfo` Just strict_sig
-           `setInlinePragInfo` neverInlinePragma
+           `setSpecInfo`          mkSpecInfo (maybeToList $ primOpRules name prim_op)
+           `setArityInfo`         arity
+           `setStrictnessInfo`    strict_sig
+           `setInlinePragInfo`    neverInlinePragma
                -- We give PrimOps a NOINLINE pragma so that we don't
                -- get silly warnings from Desugar.dsRule (the inline_shadows_rule 
                -- test) about a RULE conflicting with a possible inlining
@@ -921,12 +925,12 @@ mkFCallId dflags uniq fcall ty
 
     info = noCafIdInfo
            `setArityInfo`         arity
-           `setStrictnessInfo` Just strict_sig
+           `setStrictnessInfo`    strict_sig
 
-    (_, tau)     = tcSplitForAllTys ty
-    (arg_tys, _) = tcSplitFunTys tau
-    arity        = length arg_tys
-    strict_sig   = mkStrictSig (mkTopDmdType (replicate arity evalDmd) TopRes)
+    (_, tau)        = tcSplitForAllTys ty
+    (arg_tys, _)    = tcSplitFunTys tau
+    arity           = length arg_tys
+    strict_sig      = mkStrictSig (mkTopDmdType (replicate arity evalDmd) topRes)
 \end{code}
 
 
diff --git a/compiler/cmm/CmmInfo.hs b/compiler/cmm/CmmInfo.hs
index 89b9c4c0df..f04974c321 100644
--- a/compiler/cmm/CmmInfo.hs
+++ b/compiler/cmm/CmmInfo.hs
@@ -9,7 +9,31 @@ module CmmInfo (
   mkEmptyContInfoTable,
   cmmToRawCmm,
   mkInfoTable,
-  srtEscape
+  srtEscape,
+
+  -- info table accessors
+  closureInfoPtr,
+  entryCode,
+  getConstrTag,
+  cmmGetClosureType,
+  infoTable,
+  infoTableConstrTag,
+  infoTableSrtBitmap,
+  infoTableClosureType,
+  infoTablePtrs,
+  infoTableNonPtrs,
+  funInfoTable,
+
+  -- info table sizes and offsets
+  stdInfoTableSizeW,
+  fixedInfoTableSizeW,
+  profInfoTableSizeW,
+  maxStdInfoTableSizeW,
+  maxRetInfoTableSizeW,
+  stdInfoTableSizeB,
+  stdSrtBitmapOffset,
+  stdClosureTypeOffset,
+  stdPtrsOffset, stdNonPtrsOffset,
 ) where
 
 #include "HsVersions.h"
@@ -388,3 +412,132 @@ newStringLit bytes
 -- | Value of the srt field of an info table when using an StgLargeSRT
 srtEscape :: DynFlags -> StgHalfWord
 srtEscape dflags = toStgHalfWord dflags (-1)
+
+-------------------------------------------------------------------------
+--
+--	Accessing fields of an info table
+--
+-------------------------------------------------------------------------
+
+closureInfoPtr :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes a closure pointer and returns the info table pointer
+closureInfoPtr dflags e = CmmLoad e (bWord dflags)
+
+entryCode :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes an info pointer (the first word of a closure)
+-- and returns its entry code
+entryCode dflags e
+ | tablesNextToCode dflags = e
+ | otherwise               = CmmLoad e (bWord dflags)
+
+getConstrTag :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes a closure pointer, and return the *zero-indexed*
+-- constructor tag obtained from the info table
+-- This lives in the SRT field of the info table
+-- (constructors don't need SRTs).
+getConstrTag dflags closure_ptr
+  = CmmMachOp (MO_UU_Conv (halfWordWidth dflags) (wordWidth dflags)) [infoTableConstrTag dflags info_table]
+  where
+    info_table = infoTable dflags (closureInfoPtr dflags closure_ptr)
+
+cmmGetClosureType :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes a closure pointer, and return the closure type
+-- obtained from the info table
+cmmGetClosureType dflags closure_ptr
+  = CmmMachOp (MO_UU_Conv (halfWordWidth dflags) (wordWidth dflags)) [infoTableClosureType dflags info_table]
+  where
+    info_table = infoTable dflags (closureInfoPtr dflags closure_ptr)
+
+infoTable :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes an info pointer (the first word of a closure)
+-- and returns a pointer to the first word of the standard-form
+-- info table, excluding the entry-code word (if present)
+infoTable dflags info_ptr
+  | tablesNextToCode dflags = cmmOffsetB dflags info_ptr (- stdInfoTableSizeB dflags)
+  | otherwise               = cmmOffsetW dflags info_ptr 1 -- Past the entry code pointer
+
+infoTableConstrTag :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes an info table pointer (from infoTable) and returns the constr tag
+-- field of the info table (same as the srt_bitmap field)
+infoTableConstrTag = infoTableSrtBitmap
+
+infoTableSrtBitmap :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes an info table pointer (from infoTable) and returns the srt_bitmap
+-- field of the info table
+infoTableSrtBitmap dflags info_tbl
+  = CmmLoad (cmmOffsetB dflags info_tbl (stdSrtBitmapOffset dflags)) (bHalfWord dflags)
+
+infoTableClosureType :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes an info table pointer (from infoTable) and returns the closure type
+-- field of the info table.
+infoTableClosureType dflags info_tbl
+  = CmmLoad (cmmOffsetB dflags info_tbl (stdClosureTypeOffset dflags)) (bHalfWord dflags)
+
+infoTablePtrs :: DynFlags -> CmmExpr -> CmmExpr
+infoTablePtrs dflags info_tbl
+  = CmmLoad (cmmOffsetB dflags info_tbl (stdPtrsOffset dflags)) (bHalfWord dflags)
+
+infoTableNonPtrs :: DynFlags -> CmmExpr -> CmmExpr
+infoTableNonPtrs dflags info_tbl
+  = CmmLoad (cmmOffsetB dflags info_tbl (stdNonPtrsOffset dflags)) (bHalfWord dflags)
+
+funInfoTable :: DynFlags -> CmmExpr -> CmmExpr
+-- Takes the info pointer of a function,
+-- and returns a pointer to the first word of the StgFunInfoExtra struct
+-- in the info table.
+funInfoTable dflags info_ptr
+  | tablesNextToCode dflags
+  = cmmOffsetB dflags info_ptr (- stdInfoTableSizeB dflags - sIZEOF_StgFunInfoExtraRev dflags)
+  | otherwise
+  = cmmOffsetW dflags info_ptr (1 + stdInfoTableSizeW dflags)
+				-- Past the entry code pointer
+
+-----------------------------------------------------------------------------
+--
+--      Info table sizes & offsets
+--
+-----------------------------------------------------------------------------
+	
+stdInfoTableSizeW :: DynFlags -> WordOff
+-- The size of a standard info table varies with profiling/ticky etc,
+-- so we can't get it from Constants
+-- It must vary in sync with mkStdInfoTable
+stdInfoTableSizeW dflags
+  = fixedInfoTableSizeW
+  + if gopt Opt_SccProfilingOn dflags
+       then profInfoTableSizeW
+       else 0
+
+fixedInfoTableSizeW :: WordOff
+fixedInfoTableSizeW = 2 -- layout, type
+
+profInfoTableSizeW :: WordOff
+profInfoTableSizeW = 2
+
+maxStdInfoTableSizeW :: WordOff
+maxStdInfoTableSizeW =
+  1 {- entry, when !tablesNextToCode -}
+  + fixedInfoTableSizeW
+  + profInfoTableSizeW
+
+maxRetInfoTableSizeW :: WordOff
+maxRetInfoTableSizeW =
+  maxStdInfoTableSizeW
+  + 1 {- srt label -}
+
+stdInfoTableSizeB  :: DynFlags -> ByteOff
+stdInfoTableSizeB dflags = stdInfoTableSizeW dflags * wORD_SIZE dflags
+
+stdSrtBitmapOffset :: DynFlags -> ByteOff
+-- Byte offset of the SRT bitmap half-word which is 
+-- in the *higher-addressed* part of the type_lit
+stdSrtBitmapOffset dflags = stdInfoTableSizeB dflags - hALF_WORD_SIZE dflags
+
+stdClosureTypeOffset :: DynFlags -> ByteOff
+-- Byte offset of the closure type half-word 
+stdClosureTypeOffset dflags = stdInfoTableSizeB dflags - wORD_SIZE dflags
+
+stdPtrsOffset, stdNonPtrsOffset :: DynFlags -> ByteOff
+stdPtrsOffset    dflags = stdInfoTableSizeB dflags - 2 * wORD_SIZE dflags
+stdNonPtrsOffset dflags = stdInfoTableSizeB dflags - 2 * wORD_SIZE dflags + hALF_WORD_SIZE dflags
+
diff --git a/compiler/cmm/CmmLayoutStack.hs b/compiler/cmm/CmmLayoutStack.hs
index 78bef17a42..a48d48742d 100644
--- a/compiler/cmm/CmmLayoutStack.hs
+++ b/compiler/cmm/CmmLayoutStack.hs
@@ -5,9 +5,9 @@ module CmmLayoutStack (
 
 import StgCmmUtils      ( callerSaveVolatileRegs ) -- XXX layering violation
 import StgCmmForeign    ( saveThreadState, loadThreadState ) -- XXX layering violation
-import StgCmmLayout     ( entryCode ) -- XXX layering violation
 
 import Cmm
+import CmmInfo
 import BlockId
 import CLabel
 import CmmUtils
diff --git a/compiler/cmm/CmmParse.y b/compiler/cmm/CmmParse.y
index dff62e2fa7..edeeebb9db 100644
--- a/compiler/cmm/CmmParse.y
+++ b/compiler/cmm/CmmParse.y
@@ -186,6 +186,7 @@ import StgCmmBind       ( emitBlackHoleCode, emitUpdateFrame )
 import MkGraph
 import Cmm
 import CmmUtils
+import CmmInfo
 import BlockId
 import CmmLex
 import CLabel
diff --git a/compiler/codeGen/StgCmmBind.hs b/compiler/codeGen/StgCmmBind.hs
index 4870455fe2..136bb52b07 100644
--- a/compiler/codeGen/StgCmmBind.hs
+++ b/compiler/codeGen/StgCmmBind.hs
@@ -32,6 +32,7 @@ import MkGraph
 import CoreSyn          ( AltCon(..) )
 import SMRep
 import Cmm
+import CmmInfo
 import CmmUtils
 import CLabel
 import StgSyn
diff --git a/compiler/codeGen/StgCmmExpr.hs b/compiler/codeGen/StgCmmExpr.hs
index d7c015e689..f4186f7b9b 100644
--- a/compiler/codeGen/StgCmmExpr.hs
+++ b/compiler/codeGen/StgCmmExpr.hs
@@ -30,6 +30,7 @@ import StgSyn
 import MkGraph
 import BlockId
 import Cmm
+import CmmInfo
 import CoreSyn
 import DataCon
 import ForeignCall
diff --git a/compiler/codeGen/StgCmmLayout.hs b/compiler/codeGen/StgCmmLayout.hs
index 3b4d954d8e..8544709bd8 100644
--- a/compiler/codeGen/StgCmmLayout.hs
+++ b/compiler/codeGen/StgCmmLayout.hs
@@ -24,14 +24,6 @@ module StgCmmLayout (
 
 	mkVirtHeapOffsets, mkVirtConstrOffsets, getHpRelOffset, hpRel,
 
-	stdInfoTableSizeB,
-	entryCode, closureInfoPtr,
-	getConstrTag,
-        cmmGetClosureType,
-	infoTable, infoTableClosureType,
-	infoTablePtrs, infoTableNonPtrs,
-        funInfoTable,
-
         ArgRep(..), toArgRep, argRepSizeW
   ) where
 
@@ -49,6 +41,7 @@ import MkGraph
 import SMRep
 import Cmm
 import CmmUtils
+import CmmInfo
 import CLabel
 import StgSyn
 import Id
@@ -534,116 +527,3 @@ emitClosureAndInfoTable info_tbl conv args body
        ; let entry_lbl = toEntryLbl (cit_lbl info_tbl)
        ; emitProcWithConvention conv (Just info_tbl) entry_lbl args blks
        }
-
------------------------------------------------------------------------------
---
---	Info table offsets
---
------------------------------------------------------------------------------
-	
-stdInfoTableSizeW :: DynFlags -> WordOff
--- The size of a standard info table varies with profiling/ticky etc,
--- so we can't get it from Constants
--- It must vary in sync with mkStdInfoTable
-stdInfoTableSizeW dflags
-  = size_fixed + size_prof
-  where
-    size_fixed = 2	-- layout, type
-    size_prof | gopt Opt_SccProfilingOn dflags = 2
-	      | otherwise	   = 0
-
-stdInfoTableSizeB  :: DynFlags -> ByteOff
-stdInfoTableSizeB dflags = stdInfoTableSizeW dflags * wORD_SIZE dflags
-
-stdSrtBitmapOffset :: DynFlags -> ByteOff
--- Byte offset of the SRT bitmap half-word which is 
--- in the *higher-addressed* part of the type_lit
-stdSrtBitmapOffset dflags = stdInfoTableSizeB dflags - hALF_WORD_SIZE dflags
-
-stdClosureTypeOffset :: DynFlags -> ByteOff
--- Byte offset of the closure type half-word 
-stdClosureTypeOffset dflags = stdInfoTableSizeB dflags - wORD_SIZE dflags
-
-stdPtrsOffset, stdNonPtrsOffset :: DynFlags -> ByteOff
-stdPtrsOffset    dflags = stdInfoTableSizeB dflags - 2 * wORD_SIZE dflags
-stdNonPtrsOffset dflags = stdInfoTableSizeB dflags - 2 * wORD_SIZE dflags + hALF_WORD_SIZE dflags
-
--------------------------------------------------------------------------
---
---	Accessing fields of an info table
---
--------------------------------------------------------------------------
-
-closureInfoPtr :: DynFlags -> CmmExpr -> CmmExpr
--- Takes a closure pointer and returns the info table pointer
-closureInfoPtr dflags e = CmmLoad e (bWord dflags)
-
-entryCode :: DynFlags -> CmmExpr -> CmmExpr
--- Takes an info pointer (the first word of a closure)
--- and returns its entry code
-entryCode dflags e
- | tablesNextToCode dflags = e
- | otherwise               = CmmLoad e (bWord dflags)
-
-getConstrTag :: DynFlags -> CmmExpr -> CmmExpr
--- Takes a closure pointer, and return the *zero-indexed*
--- constructor tag obtained from the info table
--- This lives in the SRT field of the info table
--- (constructors don't need SRTs).
-getConstrTag dflags closure_ptr
-  = CmmMachOp (MO_UU_Conv (halfWordWidth dflags) (wordWidth dflags)) [infoTableConstrTag dflags info_table]
-  where
-    info_table = infoTable dflags (closureInfoPtr dflags closure_ptr)
-
-cmmGetClosureType :: DynFlags -> CmmExpr -> CmmExpr
--- Takes a closure pointer, and return the closure type
--- obtained from the info table
-cmmGetClosureType dflags closure_ptr
-  = CmmMachOp (MO_UU_Conv (halfWordWidth dflags) (wordWidth dflags)) [infoTableClosureType dflags info_table]
-  where
-    info_table = infoTable dflags (closureInfoPtr dflags closure_ptr)
-
-infoTable :: DynFlags -> CmmExpr -> CmmExpr
--- Takes an info pointer (the first word of a closure)
--- and returns a pointer to the first word of the standard-form
--- info table, excluding the entry-code word (if present)
-infoTable dflags info_ptr
-  | tablesNextToCode dflags = cmmOffsetB dflags info_ptr (- stdInfoTableSizeB dflags)
-  | otherwise               = cmmOffsetW dflags info_ptr 1 -- Past the entry code pointer
-
-infoTableConstrTag :: DynFlags -> CmmExpr -> CmmExpr
--- Takes an info table pointer (from infoTable) and returns the constr tag
--- field of the info table (same as the srt_bitmap field)
-infoTableConstrTag = infoTableSrtBitmap
-
-infoTableSrtBitmap :: DynFlags -> CmmExpr -> CmmExpr
--- Takes an info table pointer (from infoTable) and returns the srt_bitmap
--- field of the info table
-infoTableSrtBitmap dflags info_tbl
-  = CmmLoad (cmmOffsetB dflags info_tbl (stdSrtBitmapOffset dflags)) (bHalfWord dflags)
-
-infoTableClosureType :: DynFlags -> CmmExpr -> CmmExpr
--- Takes an info table pointer (from infoTable) and returns the closure type
--- field of the info table.
-infoTableClosureType dflags info_tbl
-  = CmmLoad (cmmOffsetB dflags info_tbl (stdClosureTypeOffset dflags)) (bHalfWord dflags)
-
-infoTablePtrs :: DynFlags -> CmmExpr -> CmmExpr
-infoTablePtrs dflags info_tbl
-  = CmmLoad (cmmOffsetB dflags info_tbl (stdPtrsOffset dflags)) (bHalfWord dflags)
-
-infoTableNonPtrs :: DynFlags -> CmmExpr -> CmmExpr
-infoTableNonPtrs dflags info_tbl
-  = CmmLoad (cmmOffsetB dflags info_tbl (stdNonPtrsOffset dflags)) (bHalfWord dflags)
-
-funInfoTable :: DynFlags -> CmmExpr -> CmmExpr
--- Takes the info pointer of a function,
--- and returns a pointer to the first word of the StgFunInfoExtra struct
--- in the info table.
-funInfoTable dflags info_ptr
-  | tablesNextToCode dflags
-  = cmmOffsetB dflags info_ptr (- stdInfoTableSizeB dflags - sIZEOF_StgFunInfoExtraRev dflags)
-  | otherwise
-  = cmmOffsetW dflags info_ptr (1 + stdInfoTableSizeW dflags)
-				-- Past the entry code pointer
-
diff --git a/compiler/codeGen/StgCmmPrim.hs b/compiler/codeGen/StgCmmPrim.hs
index 66832c125a..986286647b 100644
--- a/compiler/codeGen/StgCmmPrim.hs
+++ b/compiler/codeGen/StgCmmPrim.hs
@@ -29,6 +29,7 @@ import BasicTypes
 import MkGraph
 import StgSyn
 import Cmm
+import CmmInfo
 import Type     ( Type, tyConAppTyCon )
 import TyCon
 import CLabel
diff --git a/compiler/codeGen/StgCmmTicky.hs b/compiler/codeGen/StgCmmTicky.hs
index ffa5168a63..2bca544ac8 100644
--- a/compiler/codeGen/StgCmmTicky.hs
+++ b/compiler/codeGen/StgCmmTicky.hs
@@ -410,6 +410,6 @@ showTypeCategory ty
 	  else if isPrimTyCon tycon {- array, we hope -}   then 'A'	-- Bogus
 	  else if isEnumerationTyCon tycon		   then 'E'
 	  else if isTupleTyCon tycon			   then 'T'
-	  else if isJust (tyConSingleDataCon_maybe tycon)       then 'S'
+	  else if isJust (tyConSingleDataCon_maybe tycon)  then 'S'
 	  else if utc == listTyConKey			   then 'L'
 	  else 'M' -- oh, well...
diff --git a/compiler/coreSyn/CoreArity.lhs b/compiler/coreSyn/CoreArity.lhs
index fbb98c2174..50b834be3f 100644
--- a/compiler/coreSyn/CoreArity.lhs
+++ b/compiler/coreSyn/CoreArity.lhs
@@ -131,9 +131,10 @@ exprBotStrictness_maybe :: CoreExpr -> Maybe (Arity, StrictSig)
 exprBotStrictness_maybe e
   = case getBotArity (arityType env e) of
 	Nothing -> Nothing
-	Just ar -> Just (ar, mkStrictSig (mkTopDmdType (replicate ar topDmd) BotRes))
+	Just ar -> Just (ar, sig ar)
   where
-    env = AE { ae_bndrs = [], ae_ped_bot = True, ae_cheap_fn = \ _ _ -> False }
+    env    = AE { ae_bndrs = [], ae_ped_bot = True, ae_cheap_fn = \ _ _ -> False }
+    sig ar = mkStrictSig (mkTopDmdType (replicate ar topDmd) botRes)
                   -- For this purpose we can be very simple
 \end{code}
 
@@ -627,7 +628,8 @@ arityType env (Cast e co)
     --   Casts don't affect that part. Getting this wrong provoked #5475
 
 arityType _ (Var v)
-  | Just strict_sig <- idStrictness_maybe v
+  | strict_sig <- idStrictness v
+  , not $ isTopSig strict_sig
   , (ds, res) <- splitStrictSig strict_sig
   , let arity = length ds
   = if isBotRes res then ABot arity
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index cd041a5d15..ac3be95983 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -51,8 +51,7 @@ import PrelNames
 import Outputable
 import FastString
 import Util
-import Unify
-import InstEnv ( instanceBindFun )
+import OptCoercion ( checkAxInstCo )
 import Control.Monad
 import MonadUtils
 import Data.Maybe
@@ -224,16 +223,15 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
 
       -- Check whether arity and demand type are consistent (only if demand analysis
       -- already happened)
-       ; checkL (case maybeDmdTy of
-                  Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
-                  Nothing -> True)
+       ; checkL (case dmdTy of
+                  StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
            (mkArityMsg binder) }
 	  
 	-- We should check the unfolding, if any, but this is tricky because
  	-- the unfolding is a SimplifiableCoreExpr. Give up for now.
    where
     binder_ty                  = idType binder
-    maybeDmdTy                 = idStrictness_maybe binder
+    dmdTy                      = idStrictness binder
     bndr_vars                  = varSetElems (idFreeVars binder)
 
     -- If you edit this function, you may need to update the GHC formalism
@@ -413,31 +411,6 @@ kind coercions and produce the following substitution which is to be
 applied in the type variables:
   k_ag   ~~>   * -> *
 
-Note [Conflict checking with AxiomInstCo]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the following type family and axiom:
-
-type family Equal (a :: k) (b :: k) :: Bool
-type instance where
-  Equal a a = True
-  Equal a b = False
---
-Equal :: forall k::BOX. k -> k -> Bool
-axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
-           ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
-
-We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is 0-based,
-so this is the second branch of the axiom.) The problem is that, on the surface, it
-seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) and that all is
-OK. But, all is not OK: we want to use the first branch of the axiom in this case,
-not the second. The problem is that the parameters of the first branch can unify with
-the supplied coercions, thus meaning that the first branch should be taken. See also
-Note [Instance checking within groups] in types/FamInstEnv.lhs.
-
-However, if the right-hand side of the previous branch coincides with the right-hand
-side of the selected branch, we wish to accept the AxiomInstCo. See also Note
-[Confluence checking within groups], also in types/FamInstEnv.lhs.
-
 %************************************************************************
 %*									*
 \subsection[lintCoreArgs]{lintCoreArgs}
@@ -951,7 +924,7 @@ lintCoercion co@(AxiomInstCo con ind cos)
                                       (ktvs `zip` cos)
        ; let lhs' = Type.substTys subst_l lhs
              rhs' = Type.substTy subst_r rhs
-       ; case check_no_conflict lhs' (ind - 1) of
+       ; case checkAxInstCo co of
            Just bad_index -> bad_ax $ ptext (sLit "inconsistent with") <+> (ppr bad_index)
            Nothing -> return ()
        ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs') }
@@ -959,17 +932,6 @@ lintCoercion co@(AxiomInstCo con ind cos)
     bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
                         2 (ppr co))
 
-      -- See Note [Conflict checking with AxiomInstCo]
-    check_no_conflict :: [Type] -> Int -> Maybe Int
-    check_no_conflict _ (-1) = Nothing
-    check_no_conflict lhs' j
-      | SurelyApart <- tcApartTys instanceBindFun lhs' lhsj
-      = check_no_conflict lhs' (j-1)
-      | otherwise
-      = Just j
-      where
-        (CoAxBranch { cab_lhs = lhsj }) = coAxiomNthBranch con j
-
     check_ki (subst_l, subst_r) (ktv, co)
       = do { (k, t1, t2) <- lintCoercion co
            ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
diff --git a/compiler/coreSyn/CorePrep.lhs b/compiler/coreSyn/CorePrep.lhs
index fda2bccf9a..458b192a0b 100644
--- a/compiler/coreSyn/CorePrep.lhs
+++ b/compiler/coreSyn/CorePrep.lhs
@@ -336,8 +336,7 @@ Into this one:
 %************************************************************************
 
 \begin{code}
-cpeBind :: TopLevelFlag
-        -> CorePrepEnv -> CoreBind
+cpeBind :: TopLevelFlag -> CorePrepEnv -> CoreBind
         -> UniqSM (CorePrepEnv, Floats)
 cpeBind top_lvl env (NonRec bndr rhs)
   = do { (_, bndr1) <- cpCloneBndr env bndr
@@ -472,8 +471,8 @@ cpeRhsE _env expr@(Type {})      = return (emptyFloats, expr)
 cpeRhsE _env expr@(Coercion {})  = return (emptyFloats, expr)
 cpeRhsE env (Lit (LitInteger i _))
     = cpeRhsE env (cvtLitInteger (cpe_dynFlags env) (getMkIntegerId env) i)
-cpeRhsE _env expr@(Lit {})       = return (emptyFloats, expr)
-cpeRhsE env expr@(Var {})        = cpeApp env expr
+cpeRhsE _env expr@(Lit {}) = return (emptyFloats, expr)
+cpeRhsE env expr@(Var {})  = cpeApp env expr
 
 cpeRhsE env (Var f `App` _ `App` arg)
   | f `hasKey` lazyIdKey          -- Replace (lazy a) by a
@@ -642,12 +641,13 @@ cpeApp env expr
       = do { (fun',hd,fun_ty,floats,ss) <- collect_args fun (depth+1)
            ; let
               (ss1, ss_rest)   = case ss of
-                                   (ss1:ss_rest) -> (ss1,     ss_rest)
-                                   []            -> (lazyDmd, [])
+                                   (ss1:ss_rest)             -> (ss1,     ss_rest)
+                                   []                        -> (topDmd, [])
               (arg_ty, res_ty) = expectJust "cpeBody:collect_args" $
                                  splitFunTy_maybe fun_ty
+              is_strict = isStrictDmd ss1
 
-           ; (fs, arg') <- cpeArg env (isStrictDmd ss1) arg arg_ty
+           ; (fs, arg') <- cpeArg env is_strict arg arg_ty
            ; return (App fun' arg', hd, res_ty, fs `appendFloats` floats, ss_rest) }
 
     collect_args (Var v) depth
@@ -656,10 +656,10 @@ cpeApp env expr
            ; return (Var v2, (Var v2, depth), idType v2, emptyFloats, stricts) }
         where
           stricts = case idStrictness v of
-                        StrictSig (DmdType _ demands _)
-                            | listLengthCmp demands depth /= GT -> demands
+                            StrictSig (DmdType _ demands _)
+                              | listLengthCmp demands depth /= GT -> demands
                                     -- length demands <= depth
-                            | otherwise                         -> []
+                              | otherwise                         -> []
                 -- If depth < length demands, then we have too few args to
                 -- satisfy strictness  info so we have to  ignore all the
                 -- strictness info, e.g. + (error "urk")
@@ -689,8 +689,8 @@ cpeApp env expr
 -- ---------------------------------------------------------------------------
 
 -- This is where we arrange that a non-trivial argument is let-bound
-cpeArg :: CorePrepEnv -> RhsDemand -> CoreArg -> Type
-       -> UniqSM (Floats, CpeTriv)
+cpeArg :: CorePrepEnv -> RhsDemand 
+       -> CoreArg -> Type -> UniqSM (Floats, CpeTriv)
 cpeArg env is_strict arg arg_ty
   = do { (floats1, arg1) <- cpeRhsE env arg     -- arg1 can be a lambda
        ; (floats2, arg2) <- if want_float floats1 arg1
diff --git a/compiler/coreSyn/CoreTidy.lhs b/compiler/coreSyn/CoreTidy.lhs
index e29c50cc9d..a46dc65ccf 100644
--- a/compiler/coreSyn/CoreTidy.lhs
+++ b/compiler/coreSyn/CoreTidy.lhs
@@ -171,8 +171,8 @@ tidyLetBndr rec_tidy_env env (id,rhs)
     idinfo   = idInfo id
     new_info = idInfo new_id
 		`setArityInfo`		exprArity rhs
-		`setStrictnessInfo`	strictnessInfo idinfo
-		`setDemandInfo`		demandInfo idinfo
+                `setStrictnessInfo`	strictnessInfo idinfo
+                `setDemandInfo`	        demandInfo idinfo
 		`setInlinePragInfo`	inlinePragInfo idinfo
 		`setUnfoldingInfo`	new_unf
 
diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs
index 42f83151f7..4cc199853b 100644
--- a/compiler/coreSyn/MkCore.lhs
+++ b/compiler/coreSyn/MkCore.lhs
@@ -74,8 +74,9 @@ import Type
 import Coercion
 import TysPrim
 import DataCon          ( DataCon, dataConWorkId )
-import IdInfo		( vanillaIdInfo, setStrictnessInfo, setArityInfo )
-import Demand
+import IdInfo		( vanillaIdInfo, setStrictnessInfo, 
+                          setArityInfo )
+import Demand 
 import Name      hiding ( varName )
 import Outputable
 import FastString
@@ -733,7 +734,7 @@ pc_bottoming_Id :: Name -> Type -> Id
 pc_bottoming_Id name ty
  = mkVanillaGlobalWithInfo name ty bottoming_info
  where
-    bottoming_info = vanillaIdInfo `setStrictnessInfo` Just strict_sig
+    bottoming_info = vanillaIdInfo `setStrictnessInfo`    strict_sig
 				   `setArityInfo`         1
 			-- Make arity and strictness agree
 
@@ -746,7 +747,7 @@ pc_bottoming_Id name ty
         -- any pc_bottoming_Id will itself have CafRefs, which bloats
         -- SRTs.
 
-    strict_sig = mkStrictSig (mkTopDmdType [evalDmd] BotRes)
-        -- These "bottom" out, no matter what their arguments
+    strict_sig = mkStrictSig (mkTopDmdType [evalDmd] botRes)
+    -- These "bottom" out, no matter what their arguments
 \end{code}
 
diff --git a/compiler/coreSyn/PprCore.lhs b/compiler/coreSyn/PprCore.lhs
index cdae3bd7c7..4877ec7dde 100644
--- a/compiler/coreSyn/PprCore.lhs
+++ b/compiler/coreSyn/PprCore.lhs
@@ -29,7 +29,6 @@ import BasicTypes
 import Util
 import Outputable
 import FastString
-import Data.Maybe
 \end{code}
 
 %************************************************************************
@@ -336,10 +335,10 @@ pprIdBndrInfo info
     dmd_info  = demandInfo info
     lbv_info  = lbvarInfo info
 
-    has_prag = not (isDefaultInlinePragma prag_info)
-    has_occ  = not (isNoOcc occ_info)
-    has_dmd  = case dmd_info of { Nothing -> False; Just d -> not (isTop d) }
-    has_lbv  = not (hasNoLBVarInfo lbv_info)
+    has_prag  = not (isDefaultInlinePragma prag_info)
+    has_occ   = not (isNoOcc occ_info)
+    has_dmd   = not $ isTopDmd dmd_info 
+    has_lbv   = not (hasNoLBVarInfo lbv_info)
 
     doc = showAttributes
           [ (has_prag, ptext (sLit "InlPrag=") <> ppr prag_info)
@@ -365,7 +364,7 @@ ppIdInfo id info
     [ (True, pp_scope <> ppr (idDetails id))
     , (has_arity,      ptext (sLit "Arity=") <> int arity)
     , (has_caf_info,   ptext (sLit "Caf=") <> ppr caf_info)
-    , (has_strictness, ptext (sLit "Str=") <> pprStrictness str_info)
+    , (True,           ptext (sLit "Str=") <> pprStrictness str_info)
     , (has_unf,        ptext (sLit "Unf=") <> ppr unf_info)
     , (not (null rules), ptext (sLit "RULES:") <+> vcat (map pprRule rules))
     ]   -- Inline pragma, occ, demand, lbvar info
@@ -383,7 +382,6 @@ ppIdInfo id info
     has_caf_info = not (mayHaveCafRefs caf_info)
 
     str_info = strictnessInfo info
-    has_strictness = isJust str_info
 
     unf_info = unfoldingInfo info
     has_unf = hasSomeUnfolding unf_info
diff --git a/compiler/ghc.mk b/compiler/ghc.mk
index 24c11b8448..9621f1de4b 100644
--- a/compiler/ghc.mk
+++ b/compiler/ghc.mk
@@ -130,53 +130,48 @@ endif
 
 PLATFORM_H = ghc_boot_platform.h
 
-ifeq "$(BuildingCrossCompiler)" "YES"
-compiler/stage1/$(PLATFORM_H) : compiler/stage2/$(PLATFORM_H)
-	cp $< $@
-else
 compiler/stage1/$(PLATFORM_H) : mk/config.mk mk/project.mk | $$(dir $$@)/.
 	$(call removeFiles,$@)
 	@echo "Creating $@..."
 	@echo "#ifndef __PLATFORM_H__"                           >> $@
 	@echo "#define __PLATFORM_H__"                           >> $@
 	@echo                                                    >> $@
-	@echo "#define BuildPlatform_NAME  \"$(BUILDPLATFORM)\"" >> $@
-	@echo "#define HostPlatform_NAME   \"$(BUILDPLATFORM)\"" >> $@
-	@echo "#define TargetPlatform_NAME \"$(HOSTPLATFORM)\""  >> $@
-	@echo                                                    >> $@
-	@echo "#define $(BuildPlatform_CPP)_BUILD 1"             >> $@
-	@echo "#define $(BuildPlatform_CPP)_HOST 1"              >> $@
-	@echo "#define $(HostPlatform_CPP)_TARGET 1"             >> $@
-	@echo                                                    >> $@
-	@echo "#define $(BuildArch_CPP)_BUILD_ARCH 1"            >> $@
-	@echo "#define $(BuildArch_CPP)_HOST_ARCH 1"             >> $@
-	@echo "#define $(HostArch_CPP)_TARGET_ARCH 1"            >> $@
-	@echo "#define BUILD_ARCH \"$(BuildArch_CPP)\""          >> $@
-	@echo "#define HOST_ARCH \"$(BuildArch_CPP)\""           >> $@
-	@echo "#define TARGET_ARCH \"$(HostArch_CPP)\""          >> $@
-	@echo                                                    >> $@
-	@echo "#define $(BuildOS_CPP)_BUILD_OS 1"                >> $@
-	@echo "#define $(BuildOS_CPP)_HOST_OS 1"                 >> $@
-	@echo "#define $(HostOS_CPP)_TARGET_OS 1"                >> $@
-	@echo "#define BUILD_OS \"$(BuildOS_CPP)\""              >> $@
-	@echo "#define HOST_OS \"$(BuildOS_CPP)\""               >> $@
-	@echo "#define TARGET_OS \"$(HostOS_CPP)\""              >> $@
-ifeq "$(HostOS_CPP)" "irix"
-	@echo "#ifndef $(IRIX_MAJOR)_TARGET_OS"                  >> $@
-	@echo "#define $(IRIX_MAJOR)_TARGET_OS 1"                >> $@
-	@echo "#endif"                                           >> $@
+	@echo "#define BuildPlatform_NAME  \"$(BUILDPLATFORM)\""  >> $@
+	@echo "#define HostPlatform_NAME   \"$(HOSTPLATFORM)\""   >> $@
+	@echo "#define TargetPlatform_NAME \"$(TARGETPLATFORM)\"" >> $@
+	@echo                                                     >> $@
+	@echo "#define $(BuildPlatform_CPP)_BUILD 1"              >> $@
+	@echo "#define $(HostPlatform_CPP)_HOST 1"                >> $@
+	@echo "#define $(TargetPlatform_CPP)_TARGET 1"            >> $@
+	@echo                                                     >> $@
+	@echo "#define $(BuildArch_CPP)_BUILD_ARCH 1"             >> $@
+	@echo "#define $(HostArch_CPP)_HOST_ARCH 1"               >> $@
+	@echo "#define $(TargetArch_CPP)_TARGET_ARCH 1"           >> $@
+	@echo "#define BUILD_ARCH \"$(BuildArch_CPP)\""           >> $@
+	@echo "#define HOST_ARCH \"$(HostArch_CPP)\""             >> $@
+	@echo "#define TARGET_ARCH \"$(TargetArch_CPP)\""         >> $@
+	@echo                                                     >> $@
+	@echo "#define $(BuildOS_CPP)_BUILD_OS 1"                 >> $@
+	@echo "#define $(HostOS_CPP)_HOST_OS 1"                   >> $@
+	@echo "#define $(TargetOS_CPP)_TARGET_OS 1"               >> $@
+	@echo "#define BUILD_OS \"$(BuildOS_CPP)\""               >> $@
+	@echo "#define HOST_OS \"$(HostOS_CPP)\""                 >> $@
+	@echo "#define TARGET_OS \"$(TargetOS_CPP)\""             >> $@
+ifeq "$(TargetOS_CPP)" "irix"
+	@echo "#ifndef $(IRIX_MAJOR)_TARGET_OS"                   >> $@
+	@echo "#define $(IRIX_MAJOR)_TARGET_OS 1"                 >> $@
+	@echo "#endif"                                            >> $@
 endif
-	@echo                                                    >> $@
-	@echo "#define $(BuildVendor_CPP)_BUILD_VENDOR 1"        >> $@
-	@echo "#define $(BuildVendor_CPP)_HOST_VENDOR 1"         >> $@
-	@echo "#define $(HostVendor_CPP)_TARGET_VENDOR 1"        >> $@
-	@echo "#define BUILD_VENDOR \"$(BuildVendor_CPP)\""      >> $@
-	@echo "#define HOST_VENDOR \"$(BuildVendor_CPP)\""       >> $@
-	@echo "#define TARGET_VENDOR \"$(HostVendor_CPP)\""      >> $@
-	@echo                                                    >> $@
-	@echo "#endif /* __PLATFORM_H__ */"                      >> $@
+	@echo                                                     >> $@
+	@echo "#define $(BuildVendor_CPP)_BUILD_VENDOR 1"         >> $@
+	@echo "#define $(HostVendor_CPP)_HOST_VENDOR 1"           >> $@
+	@echo "#define $(TargetVendor_CPP)_TARGET_VENDOR  1"      >> $@
+	@echo "#define BUILD_VENDOR \"$(BuildVendor_CPP)\""       >> $@
+	@echo "#define HOST_VENDOR \"$(HostVendor_CPP)\""         >> $@
+	@echo "#define TARGET_VENDOR \"$(TargetVendor_CPP)\""     >> $@
+	@echo                                                     >> $@
+	@echo "#endif /* __PLATFORM_H__ */"                       >> $@
 	@echo "Done."
-endif
 
 # For stage2 and above, the BUILD platform is the HOST of stage1, and
 # the HOST platform is the TARGET of stage1.  The TARGET remains the same
@@ -187,26 +182,26 @@ compiler/stage2/$(PLATFORM_H) : mk/config.mk mk/project.mk | $$(dir $$@)/.
 	@echo "#ifndef __PLATFORM_H__"                            >> $@
 	@echo "#define __PLATFORM_H__"                            >> $@
 	@echo                                                     >> $@
-	@echo "#define BuildPlatform_NAME  \"$(BUILDPLATFORM)\""  >> $@
-	@echo "#define HostPlatform_NAME   \"$(HOSTPLATFORM)\""   >> $@
+	@echo "#define BuildPlatform_NAME  \"$(HOSTPLATFORM)\""   >> $@
+	@echo "#define HostPlatform_NAME   \"$(TARGETPLATFORM)\"" >> $@
 	@echo "#define TargetPlatform_NAME \"$(TARGETPLATFORM)\"" >> $@
 	@echo                                                     >> $@
-	@echo "#define $(BuildPlatform_CPP)_BUILD 1"              >> $@
-	@echo "#define $(HostPlatform_CPP)_HOST 1"                >> $@
+	@echo "#define $(HostPlatform_CPP)_BUILD 1"               >> $@
+	@echo "#define $(TargetPlatform_CPP)_HOST 1"              >> $@
 	@echo "#define $(TargetPlatform_CPP)_TARGET 1"            >> $@
 	@echo                                                     >> $@
-	@echo "#define $(BuildArch_CPP)_BUILD_ARCH 1"             >> $@
-	@echo "#define $(HostArch_CPP)_HOST_ARCH 1"               >> $@
+	@echo "#define $(HostArch_CPP)_BUILD_ARCH 1"              >> $@
+	@echo "#define $(TargetArch_CPP)_HOST_ARCH 1"             >> $@
 	@echo "#define $(TargetArch_CPP)_TARGET_ARCH 1"           >> $@
 	@echo "#define BUILD_ARCH \"$(HostArch_CPP)\""            >> $@
-	@echo "#define HOST_ARCH \"$(HostArch_CPP)\""             >> $@
+	@echo "#define HOST_ARCH \"$(TargetArch_CPP)\""           >> $@
 	@echo "#define TARGET_ARCH \"$(TargetArch_CPP)\""         >> $@
 	@echo                                                     >> $@
 	@echo "#define $(HostOS_CPP)_BUILD_OS 1"                  >> $@
-	@echo "#define $(HostOS_CPP)_HOST_OS 1"                   >> $@
+	@echo "#define $(TargetOS_CPP)_HOST_OS 1"                 >> $@
 	@echo "#define $(TargetOS_CPP)_TARGET_OS 1"               >> $@
 	@echo "#define BUILD_OS \"$(HostOS_CPP)\""                >> $@
-	@echo "#define HOST_OS \"$(HostOS_CPP)\""                 >> $@
+	@echo "#define HOST_OS \"$(TargetOS_CPP)\""               >> $@
 	@echo "#define TARGET_OS \"$(TargetOS_CPP)\""             >> $@
 ifeq "$(TargetOS_CPP)" "irix"
 	@echo "#ifndef $(IRIX_MAJOR)_TARGET_OS"                   >> $@
@@ -214,11 +209,11 @@ ifeq "$(TargetOS_CPP)" "irix"
 	@echo "#endif"                                            >> $@
 endif
 	@echo                                                     >> $@
-	@echo "#define $(BuildVendor_CPP)_BUILD_VENDOR 1"         >> $@
-	@echo "#define $(HostVendor_CPP)_HOST_VENDOR 1"           >> $@
+	@echo "#define $(HostVendor_CPP)_BUILD_VENDOR 1"          >> $@
+	@echo "#define $(TargetVendor_CPP)_HOST_VENDOR 1"         >> $@
 	@echo "#define $(TargetVendor_CPP)_TARGET_VENDOR  1"      >> $@
-	@echo "#define BUILD_VENDOR \"$(BuildVendor_CPP)\""       >> $@
-	@echo "#define HOST_VENDOR \"$(HostVendor_CPP)\""         >> $@
+	@echo "#define BUILD_VENDOR \"$(HostVendor_CPP)\""        >> $@
+	@echo "#define HOST_VENDOR \"$(TargetVendor_CPP)\""       >> $@
 	@echo "#define TARGET_VENDOR \"$(TargetVendor_CPP)\""     >> $@
 	@echo                                                     >> $@
 	@echo "#endif /* __PLATFORM_H__ */"                       >> $@
diff --git a/compiler/ghci/DebuggerUtils.hs b/compiler/ghci/DebuggerUtils.hs
index 8a421baf6b..7a03bbcdc2 100644
--- a/compiler/ghci/DebuggerUtils.hs
+++ b/compiler/ghci/DebuggerUtils.hs
@@ -2,7 +2,7 @@ module DebuggerUtils (
        dataConInfoPtrToName,
   ) where
 
-import StgCmmLayout ( stdInfoTableSizeB )
+import CmmInfo ( stdInfoTableSizeB )
 import ByteCodeItbls
 import DynFlags
 import FastString
diff --git a/compiler/iface/BinIface.hs b/compiler/iface/BinIface.hs
index f39c21f0d2..ac244fab79 100644
--- a/compiler/iface/BinIface.hs
+++ b/compiler/iface/BinIface.hs
@@ -30,13 +30,11 @@ import TysWiredIn
 import IfaceEnv
 import HscTypes
 import BasicTypes
-import Demand
 import Annotations
 import IfaceSyn
 import Module
 import Name
 import Avail
-import VarEnv
 import DynFlags
 import UniqFM
 import UniqSupply
@@ -389,7 +387,6 @@ data BinSymbolTable = BinSymbolTable {
                                 -- indexed by Name
   }
 
-
 putFastString :: BinDictionary -> BinHandle -> FastString -> IO ()
 putFastString dict bh fs = allocateFastString dict fs >>= put_ bh
 
@@ -427,12 +424,6 @@ data BinDictionary = BinDictionary {
 {-! for StrictnessMark derive: Binary !-}
 {-! for Activation derive: Binary !-}
 
--- Demand
-{-! for Demand derive: Binary !-}
-{-! for Demands derive: Binary !-}
-{-! for DmdResult derive: Binary !-}
-{-! for StrictSig derive: Binary !-}
-
 -- Class
 {-! for DefMeth derive: Binary !-}
 
@@ -818,87 +809,6 @@ instance Binary Fixity where
           ab <- get bh
           return (Fixity aa ab)
 
--------------------------------------------------------------------------
---              Types from: Demand
--------------------------------------------------------------------------
-
-instance Binary DmdType where
-        -- Ignore DmdEnv when spitting out the DmdType
-  put bh (DmdType _ ds dr) = do p <- put bh ds; put_ bh dr; return (castBin p)
-  get bh = do ds <- get bh; dr <- get bh; return (DmdType emptyVarEnv ds dr)
-
-instance Binary Demand where
-    put_ bh Top = do
-            putByte bh 0
-    put_ bh Abs = do
-            putByte bh 1
-    put_ bh (Call aa) = do
-            putByte bh 2
-            put_ bh aa
-    put_ bh (Eval ab) = do
-            putByte bh 3
-            put_ bh ab
-    put_ bh (Defer ac) = do
-            putByte bh 4
-            put_ bh ac
-    put_ bh (Box ad) = do
-            putByte bh 5
-            put_ bh ad
-    put_ bh Bot = do
-            putByte bh 6
-    get bh = do
-            h <- getByte bh
-            case h of
-              0 -> do return Top
-              1 -> do return Abs
-              2 -> do aa <- get bh
-                      return (Call aa)
-              3 -> do ab <- get bh
-                      return (Eval ab)
-              4 -> do ac <- get bh
-                      return (Defer ac)
-              5 -> do ad <- get bh
-                      return (Box ad)
-              _ -> do return Bot
-
-instance Binary Demands where
-    put_ bh (Poly aa) = do
-            putByte bh 0
-            put_ bh aa
-    put_ bh (Prod ab) = do
-            putByte bh 1
-            put_ bh ab
-    get bh = do
-            h <- getByte bh
-            case h of
-              0 -> do aa <- get bh
-                      return (Poly aa)
-              _ -> do ab <- get bh
-                      return (Prod ab)
-
-instance Binary DmdResult where
-    put_ bh TopRes = do
-            putByte bh 0
-    put_ bh RetCPR = do
-            putByte bh 1
-    put_ bh BotRes = do
-            putByte bh 2
-    get bh = do
-            h <- getByte bh
-            case h of
-              0 -> do return TopRes
-              1 -> do return RetCPR     -- Really use RetCPR even if -fcpr-off
-                                        -- The wrapper was generated for CPR in 
-                                        -- the imported module!
-              _ -> do return BotRes
-
-instance Binary StrictSig where
-    put_ bh (StrictSig aa) = do
-            put_ bh aa
-    get bh = do
-          aa <- get bh
-          return (StrictSig aa)
-
 
 -------------------------------------------------------------------------
 --              Types from: CostCentre
@@ -1219,11 +1129,11 @@ instance Binary IfaceIdInfo where
             _ -> lazyGet bh >>= (return . HasInfo)     -- NB lazyGet
 
 instance Binary IfaceInfoItem where
-    put_ bh (HsArity aa)      = putByte bh 0 >> put_ bh aa
-    put_ bh (HsStrictness ab) = putByte bh 1 >> put_ bh ab
-    put_ bh (HsUnfold lb ad)  = putByte bh 2 >> put_ bh lb >> put_ bh ad
-    put_ bh (HsInline ad)     = putByte bh 3 >> put_ bh ad
-    put_ bh HsNoCafRefs       = putByte bh 4
+    put_ bh (HsArity aa)          = putByte bh 0 >> put_ bh aa
+    put_ bh (HsStrictness ab)     = putByte bh 1 >> put_ bh ab
+    put_ bh (HsUnfold lb ad)      = putByte bh 2 >> put_ bh lb >> put_ bh ad
+    put_ bh (HsInline ad)         = putByte bh 3 >> put_ bh ad
+    put_ bh HsNoCafRefs           = putByte bh 4
     get bh = do
         h <- getByte bh
         case h of
diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
index 0fa38d74bc..8ba5e86eb9 100644
--- a/compiler/iface/IfaceSyn.lhs
+++ b/compiler/iface/IfaceSyn.lhs
@@ -231,11 +231,11 @@ data IfaceIdInfo
 --      and so gives a new version.
 
 data IfaceInfoItem
-  = HsArity      Arity
-  | HsStrictness StrictSig
-  | HsInline     InlinePragma
-  | HsUnfold     Bool             -- True <=> isStrongLoopBreaker is true
-                 IfaceUnfolding   -- See Note [Expose recursive functions]
+  = HsArity         Arity
+  | HsStrictness    StrictSig
+  | HsInline        InlinePragma
+  | HsUnfold        Bool             -- True <=> isStrongLoopBreaker is true
+                    IfaceUnfolding   -- See Note [Expose recursive functions]
   | HsNoCafRefs
 
 -- NB: Specialisations and rules come in separately and are
@@ -756,13 +756,13 @@ instance Outputable IfaceIdInfo where
                      <+> ptext (sLit "-}")
 
 instance Outputable IfaceInfoItem where
-  ppr (HsUnfold lb unf)  = ptext (sLit "Unfolding")
-                           <> ppWhen lb (ptext (sLit "(loop-breaker)"))
-                           <> colon <+> ppr unf
-  ppr (HsInline prag)    = ptext (sLit "Inline:") <+> ppr prag
-  ppr (HsArity arity)    = ptext (sLit "Arity:") <+> int arity
+  ppr (HsUnfold lb unf)     = ptext (sLit "Unfolding")
+                              <> ppWhen lb (ptext (sLit "(loop-breaker)"))
+                              <> colon <+> ppr unf
+  ppr (HsInline prag)       = ptext (sLit "Inline:") <+> ppr prag
+  ppr (HsArity arity)       = ptext (sLit "Arity:") <+> int arity
   ppr (HsStrictness str) = ptext (sLit "Strictness:") <+> pprIfaceStrictSig str
-  ppr HsNoCafRefs        = ptext (sLit "HasNoCafRefs")
+  ppr HsNoCafRefs           = ptext (sLit "HasNoCafRefs")
 
 instance Outputable IfaceUnfolding where
   ppr (IfCompulsory e)     = ptext (sLit "<compulsory>") <+> parens (ppr e)
diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
index bf6c1d7768..f145ec1a3a 100644
--- a/compiler/iface/MkIface.lhs
+++ b/compiler/iface/MkIface.lhs
@@ -1696,7 +1696,7 @@ toIfaceIdDetails other                          = pprTrace "toIfaceIdDetails" (p
 
 toIfaceIdInfo :: IdInfo -> IfaceIdInfo
 toIfaceIdInfo id_info
-  = case catMaybes [arity_hsinfo, caf_hsinfo, strict_hsinfo, 
+  = case catMaybes [arity_hsinfo, caf_hsinfo, strict_hsinfo,
                     inline_hsinfo,  unfold_hsinfo] of
        []    -> NoInfo
        infos -> HasInfo infos
@@ -1716,9 +1716,9 @@ toIfaceIdInfo id_info
 
     ------------  Strictness  --------------
         -- No point in explicitly exporting TopSig
-    strict_hsinfo = case strictnessInfo id_info of
-                        Just sig | not (isTopSig sig) -> Just (HsStrictness sig)
-                        _other                        -> Nothing
+    sig_info = strictnessInfo id_info
+    strict_hsinfo | not (isTopSig sig_info) = Just (HsStrictness sig_info)
+                  | otherwise               = Nothing
 
     ------------  Unfolding  --------------
     unfold_hsinfo = toIfUnfolding loop_breaker (unfoldingInfo id_info) 
diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
index 32e4425df2..3ef0ddcf18 100644
--- a/compiler/iface/TcIface.lhs
+++ b/compiler/iface/TcIface.lhs
@@ -31,8 +31,8 @@ import CoreSyn
 import CoreUtils
 import CoreUnfold
 import CoreLint
-import WorkWrap
-import MkCore( castBottomExpr )
+import WorkWrap                     ( mkWrapper )
+import MkCore                       ( castBottomExpr )
 import Id
 import MkId
 import IdInfo
@@ -1205,7 +1205,7 @@ tcIdInfo ignore_prags name ty info
     tcPrag :: IdInfo -> IfaceInfoItem -> IfL IdInfo
     tcPrag info HsNoCafRefs        = return (info `setCafInfo`   NoCafRefs)
     tcPrag info (HsArity arity)    = return (info `setArityInfo` arity)
-    tcPrag info (HsStrictness str) = return (info `setStrictnessInfo` Just str)
+    tcPrag info (HsStrictness str) = return (info `setStrictnessInfo` str)
     tcPrag info (HsInline prag)    = return (info `setInlinePragInfo` prag)
 
         -- The next two are lazy, so they don't transitively suck stuff in
@@ -1226,12 +1226,11 @@ tcUnfolding name _ info (IfCoreUnfold stable if_expr)
                     Nothing   -> NoUnfolding
                     Just expr -> mkUnfolding dflags unf_src
                                              True {- Top level -} 
-                                             is_bottoming expr) }
+                                             is_bottoming
+                                             expr) }
   where
      -- Strictness should occur before unfolding!
-    is_bottoming = case strictnessInfo info of
-                     Just sig -> isBottomingSig sig
-                     Nothing  -> False
+    is_bottoming = isBottomingSig $ strictnessInfo info              
 
 tcUnfolding name _ _ (IfCompulsory if_expr)
   = do  { mb_expr <- tcPragExpr name if_expr
@@ -1278,12 +1277,9 @@ tcIfaceWrapper name ty info arity get_worker
         = mkWwInlineRule wkr_id
                          (initUs_ us (mkWrapper dflags ty strict_sig) wkr_id) 
                          arity
-
-        -- Again we rely here on strictness info always appearing 
-        -- before unfolding
-    strict_sig = case strictnessInfo info of
-                   Just sig -> sig
-                   Nothing  -> pprPanic "Worker info but no strictness for" (ppr name)
+        -- Again we rely here on strictness info 
+        -- always appearing before unfolding
+    strict_sig = strictnessInfo info
 \end{code}
 
 For unfoldings we try to do the job lazily, so that we never type check
diff --git a/compiler/llvmGen/Llvm/Types.hs b/compiler/llvmGen/Llvm/Types.hs
index 9e77990160..c4d9995e47 100644
--- a/compiler/llvmGen/Llvm/Types.hs
+++ b/compiler/llvmGen/Llvm/Types.hs
@@ -18,6 +18,8 @@ import Unique
 -- from NCG
 import PprBase
 
+import GHC.Float
+
 -- -----------------------------------------------------------------------------
 -- * LLVM Basic Types and Variables
 --
@@ -227,7 +229,8 @@ getLit :: LlvmLit -> String
 getLit (LMIntLit i (LMInt 32)) = show (fromInteger i :: Int32)
 getLit (LMIntLit i (LMInt 64)) = show (fromInteger i :: Int64)
 getLit (LMIntLit i _         ) = show (fromInteger i :: Int)
-getLit (LMFloatLit r LMFloat ) = fToStr $ realToFrac r
+-- See Note [LLVM Float Types].
+getLit (LMFloatLit r LMFloat ) = (dToStr . widenFp . narrowFp) r
 getLit (LMFloatLit r LMDouble) = dToStr r
 getLit f@(LMFloatLit _ _) = error $ "Can't print this float literal!" ++ show f
 getLit (LMNullLit _     ) = "null"
@@ -792,6 +795,8 @@ instance Show LlvmCastOp where
 -- | Convert a Haskell Double to an LLVM hex encoded floating point form. In
 -- Llvm float literals can be printed in a big-endian hexadecimal format,
 -- regardless of underlying architecture.
+--
+-- See Note [LLVM Float Types].
 dToStr :: Double -> String
 dToStr d
   = let bs     = doubleToBytes d
@@ -804,13 +809,30 @@ dToStr d
         str  = map toUpper $ concat . fixEndian . (map hex) $ bs
     in  "0x" ++ str
 
--- | Convert a Haskell Float to an LLVM hex encoded floating point form.
--- LLVM uses the same encoding for both floats and doubles (16 digit hex
--- string) but floats must have the last half all zeroes so it can fit into
--- a float size type.
-{-# NOINLINE fToStr #-}
-fToStr :: Float -> String
-fToStr = (dToStr . realToFrac)
+-- Note [LLVM Float Types]
+-- ~~~~~~~~~~~~~~~~~~~~~~~
+-- We use 'dToStr' for both printing Float and Double floating point types. This is
+-- as LLVM expects all floating point constants (single & double) to be in IEEE
+-- 754 Double precision format. However, for single precision numbers (Float)
+-- they should be *representable* in IEEE 754 Single precision format. So the
+-- easiest way to do this is to narrow and widen again.
+-- (i.e., Double -> Float -> Double). We must be careful doing this that GHC
+-- doesn't optimize that away.
+
+-- Note [narrowFp & widenFp]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~
+-- NOTE: we use float2Double & co directly as GHC likes to optimize away
+-- successive calls of 'realToFrac', defeating the narrowing. (Bug #7600).
+-- 'realToFrac' has inconsistent behaviour with optimisation as well that can
+-- also cause issues, these methods don't.
+
+narrowFp :: Double -> Float
+{-# NOINLINE narrowFp #-}
+narrowFp = double2Float
+
+widenFp :: Float -> Double
+{-# NOINLINE widenFp #-}
+widenFp = float2Double
 
 -- | Reverse or leave byte data alone to fix endianness on this target.
 fixEndian :: [a] -> [a]
diff --git a/compiler/llvmGen/LlvmCodeGen.hs b/compiler/llvmGen/LlvmCodeGen.hs
index 4b8455f2be..a157a258fe 100644
--- a/compiler/llvmGen/LlvmCodeGen.hs
+++ b/compiler/llvmGen/LlvmCodeGen.hs
@@ -68,11 +68,14 @@ llvmCodeGen dflags h us cmms
         ver <- (fromMaybe defaultLlvmVersion) `fmap` figureLlvmVersion dflags
         -- cache llvm version for later use
         writeIORef (llvmVersion dflags) ver
-        when (ver < minSupportLlvmVersion) $
+        debugTraceMsg dflags 2
+            (text "Using LLVM version:" <+> text (show ver))
+        let doWarn = wopt Opt_WarnUnsupportedLlvmVersion dflags
+        when (ver < minSupportLlvmVersion && doWarn) $
             errorMsg dflags (text "You are using an old version of LLVM that"
                              <> text " isn't supported anymore!"
                              $+$ text "We will try though...")
-        when (ver > maxSupportLlvmVersion) $
+        when (ver > maxSupportLlvmVersion && doWarn) $
             putMsg dflags (text "You are using a new version of LLVM that"
                            <> text " hasn't been tested yet!"
                            $+$ text "We will try though...")
diff --git a/compiler/llvmGen/LlvmCodeGen/Base.hs b/compiler/llvmGen/LlvmCodeGen/Base.hs
index 56537d2ae2..45f20d7f7f 100644
--- a/compiler/llvmGen/LlvmCodeGen/Base.hs
+++ b/compiler/llvmGen/LlvmCodeGen/Base.hs
@@ -164,7 +164,7 @@ minSupportLlvmVersion :: LlvmVersion
 minSupportLlvmVersion = 28
 
 maxSupportLlvmVersion :: LlvmVersion
-maxSupportLlvmVersion = 31
+maxSupportLlvmVersion = 33
 
 -- ----------------------------------------------------------------------------
 -- * Environment Handling
diff --git a/compiler/llvmGen/LlvmCodeGen/CodeGen.hs b/compiler/llvmGen/LlvmCodeGen/CodeGen.hs
index 763656a53b..28933831f4 100644
--- a/compiler/llvmGen/LlvmCodeGen/CodeGen.hs
+++ b/compiler/llvmGen/LlvmCodeGen/CodeGen.hs
@@ -31,8 +31,7 @@ import UniqSupply
 import Unique
 import Util
 
-import Data.List ( partition )
-
+import Data.List  ( partition )
 
 type LlvmStatements = OrdList LlvmStatement
 
@@ -706,6 +705,7 @@ genCondBranch :: LlvmEnv -> CmmExpr -> BlockId -> BlockId -> UniqSM StmtData
 genCondBranch env cond idT idF = do
     let labelT = blockIdToLlvm idT
     let labelF = blockIdToLlvm idF
+    -- See Note [Literals and branch conditions].
     (env', vc, stmts, top) <- exprToVarOpt env i1Option cond
     if getVarType vc == i1
         then do
@@ -714,6 +714,57 @@ genCondBranch env cond idT idF = do
         else
             panic $ "genCondBranch: Cond expr not bool! (" ++ show vc ++ ")"
 
+{- Note [Literals and branch conditions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+It is important that whenever we generate branch conditions for
+literals like '1', they are properly narrowed to an LLVM expression of
+type 'i1' (for bools.) Otherwise, nobody is happy. So when we convert
+a CmmExpr to an LLVM expression for a branch conditional, exprToVarOpt
+must be certain to return a properly narrowed type. genLit is
+responsible for this, in the case of literal integers.
+
+Often, we won't see direct statements like:
+
+    if(1) {
+      ...
+    } else {
+      ...
+    }
+
+at this point in the pipeline, because the Glorious Code Generator
+will do trivial branch elimination in the sinking pass (among others,)
+which will eliminate the expression entirely.
+
+However, it's certainly possible and reasonable for this to occur in
+hand-written C-- code. Consider something like:
+
+    #ifndef SOME_CONDITIONAL
+    #define CHECK_THING(x) 1
+    #else
+    #define CHECK_THING(x) some_operation((x))
+    #endif
+
+    f() {
+
+      if (CHECK_THING(xyz)) {
+        ...
+      } else {
+        ...
+      }
+
+    }
+
+In such an instance, CHECK_THING might result in an *expression* in
+one case, and a *literal* in the other, depending on what in
+particular was #define'd. So we must be sure to properly narrow the
+literal in this case to i1 as it won't be eliminated beforehand.
+
+For a real example of this, see ./rts/StgStdThunks.cmm
+
+-}
+
+
 
 -- | Switch branch
 --
@@ -746,31 +797,30 @@ type ExprData = (LlvmEnv, LlvmVar, LlvmStatements, [LlvmCmmDecl])
 
 -- | Values which can be passed to 'exprToVar' to configure its
 -- behaviour in certain circumstances.
-data EOption = EOption {
-        -- | The expected LlvmType for the returned variable.
-        --
-        -- Currently just used for determining if a comparison should return
-        -- a boolean (i1) or a int (i32/i64).
-        eoExpectedType :: Maybe LlvmType
-  }
+--
+-- Currently just used for determining if a comparison should return
+-- a boolean (i1) or a word. See Note [Literals and branch conditions].
+newtype EOption = EOption { i1Expected :: Bool }
+-- XXX: EOption is an ugly and inefficient solution to this problem.
 
+-- | i1 type expected (condition scrutinee).
 i1Option :: EOption
-i1Option = EOption (Just i1)
-
-wordOption :: DynFlags -> EOption
-wordOption dflags = EOption (Just (llvmWord dflags))
+i1Option = EOption True
 
+-- | Word type expected (usual).
+wordOption :: EOption
+wordOption = EOption False
 
 -- | Convert a CmmExpr to a list of LlvmStatements with the result of the
 -- expression being stored in the returned LlvmVar.
 exprToVar :: LlvmEnv -> CmmExpr -> UniqSM ExprData
-exprToVar env = exprToVarOpt env (wordOption (getDflags env))
+exprToVar env = exprToVarOpt env wordOption
 
 exprToVarOpt :: LlvmEnv -> EOption -> CmmExpr -> UniqSM ExprData
 exprToVarOpt env opt e = case e of
 
     CmmLit lit
-        -> genLit env lit
+        -> genLit opt env lit
 
     CmmLoad e' ty
         -> genLoad env e' ty
@@ -1020,26 +1070,16 @@ genMachOp_slow env opt op [x, y] = case op of
 
         -- | Need to use EOption here as Cmm expects word size results from
         -- comparisons while LLVM return i1. Need to extend to llvmWord type
-        -- if expected
+        -- if expected. See Note [Literals and branch conditions].
         genBinComp opt cmp = do
-            ed@(env', v1, stmts, top) <- binLlvmOp (\_ -> i1) $ Compare cmp
-
+            ed@(env', v1, stmts, top) <- binLlvmOp (\_ -> i1) (Compare cmp)
             if getVarType v1 == i1
-                then
-                    case eoExpectedType opt of
-                         Nothing ->
-                             return ed
-
-                         Just t | t == i1 ->
-                                    return ed
-
-                                | isInt t -> do
-                                    (v2, s1) <- doExpr t $ Cast LM_Zext v1 t
-                                    return (env', v2, stmts `snocOL` s1, top)
-
-                                | otherwise ->
-                                    panic $ "genBinComp: Can't case i1 compare"
-                                        ++ "res to non int type " ++ show (t)
+                then case i1Expected opt of
+                    True  -> return ed
+                    False -> do
+                        let w_ = llvmWord dflags
+                        (v2, s1) <- doExpr w_ $ Cast LM_Zext v1 w_
+                        return (env', v2, stmts `snocOL` s1, top)
                 else
                     panic $ "genBinComp: Compare returned type other then i1! "
                         ++ (show $ getVarType v1)
@@ -1206,15 +1246,22 @@ allocReg _ = panic $ "allocReg: Global reg encountered! Global registers should"
 
 
 -- | Generate code for a literal
-genLit :: LlvmEnv -> CmmLit -> UniqSM ExprData
-genLit env (CmmInt i w)
-  = return (env, mkIntLit (LMInt $ widthInBits w) i, nilOL, [])
-
-genLit env (CmmFloat r w)
+genLit :: EOption -> LlvmEnv -> CmmLit -> UniqSM ExprData
+genLit opt env (CmmInt i w)
+  -- See Note [Literals and branch conditions].
+  = let width | i1Expected opt = i1
+              | otherwise      = LMInt (widthInBits w)
+        -- comm  = Comment [ fsLit $ "EOption: " ++ show opt
+        --                 , fsLit $ "Width  : " ++ show w
+        --                 , fsLit $ "Width' : " ++ show (widthInBits w)
+        --                 ]
+    in return (env, mkIntLit width i, nilOL, [])
+
+genLit _ env (CmmFloat r w)
   = return (env, LMLitVar $ LMFloatLit (fromRational r) (widthToLlvmFloat w),
               nilOL, [])
 
-genLit env cmm@(CmmLabel l)
+genLit _ env cmm@(CmmLabel l)
   = let dflags = getDflags env
         label = strCLabel_llvm env l
         ty = funLookup label env
@@ -1236,17 +1283,17 @@ genLit env cmm@(CmmLabel l)
                 (v1, s1) <- doExpr lmty $ Cast LM_Ptrtoint var (llvmWord dflags)
                 return (env, v1, unitOL s1, [])
 
-genLit env (CmmLabelOff label off) = do
+genLit opt env (CmmLabelOff label off) = do
     let dflags = getDflags env
-    (env', vlbl, stmts, stat) <- genLit env (CmmLabel label)
+    (env', vlbl, stmts, stat) <- genLit opt env (CmmLabel label)
     let voff = toIWord dflags off
     (v1, s1) <- doExpr (getVarType vlbl) $ LlvmOp LM_MO_Add vlbl voff
     return (env', v1, stmts `snocOL` s1, stat)
 
-genLit env (CmmLabelDiffOff l1 l2 off) = do
+genLit opt env (CmmLabelDiffOff l1 l2 off) = do
     let dflags = getDflags env
-    (env1, vl1, stmts1, stat1) <- genLit env (CmmLabel l1)
-    (env2, vl2, stmts2, stat2) <- genLit env1 (CmmLabel l2)
+    (env1, vl1, stmts1, stat1) <- genLit opt env (CmmLabel l1)
+    (env2, vl2, stmts2, stat2) <- genLit opt env1 (CmmLabel l2)
     let voff = toIWord dflags off
     let ty1 = getVarType vl1
     let ty2 = getVarType vl2
@@ -1262,10 +1309,10 @@ genLit env (CmmLabelDiffOff l1 l2 off) = do
         else
             panic "genLit: CmmLabelDiffOff encountered with different label ty!"
 
-genLit env (CmmBlock b)
-  = genLit env (CmmLabel $ infoTblLbl b)
+genLit opt env (CmmBlock b)
+  = genLit opt env (CmmLabel $ infoTblLbl b)
 
-genLit _ CmmHighStackMark
+genLit _ _ CmmHighStackMark
   = panic "genStaticLit - CmmHighStackMark unsupported!"
 
 
diff --git a/compiler/llvmGen/LlvmCodeGen/Ppr.hs b/compiler/llvmGen/LlvmCodeGen/Ppr.hs
index 218870a5b8..5d9fb23fe9 100644
--- a/compiler/llvmGen/LlvmCodeGen/Ppr.hs
+++ b/compiler/llvmGen/LlvmCodeGen/Ppr.hs
@@ -58,6 +58,9 @@ moduleLayout = sdocWithPlatform $ \platform ->
     Platform { platformArch = ArchARM {}, platformOS = OSLinux } ->
         text "target datalayout = \"e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:64:128-a0:0:64-n32\""
         $+$ text "target triple = \"arm-unknown-linux-gnueabi\""
+    Platform { platformArch = ArchARM {}, platformOS = OSAndroid } ->
+        text "target datalayout = \"e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:64:128-a0:0:64-n32\""
+        $+$ text "target triple = \"arm-unknown-linux-androideabi\""
     _ ->
         -- FIX: Other targets
         empty
diff --git a/compiler/main/CmdLineParser.hs b/compiler/main/CmdLineParser.hs
index b6618af1a9..252a376432 100644
--- a/compiler/main/CmdLineParser.hs
+++ b/compiler/main/CmdLineParser.hs
@@ -53,6 +53,8 @@ data OptKind m                             -- Suppose the flag is -f
     | AnySuffix (String -> EwM m ())       -- -f or -farg; pass entire "-farg" to fn
     | PrefixPred    (String -> Bool) (String -> EwM m ())
     | AnySuffixPred (String -> Bool) (String -> EwM m ())
+    | VersionSuffix (Int -> Int -> EwM m ())
+      -- -f or -f=maj.min; pass major and minor version to fn
 
 
 --------------------------------------------------------
@@ -196,6 +198,13 @@ processOneArg opt_kind rest arg args
         AnySuffix f       -> Right (f dash_arg, args)
         AnySuffixPred _ f -> Right (f dash_arg, args)
 
+        VersionSuffix f | [maj_s, min_s] <- split '.' rest_no_eq,
+                          Just maj <- parseInt maj_s,
+                          Just min <- parseInt min_s -> Right (f maj min, args)
+                        | [maj_s] <- split '.' rest_no_eq,
+                          Just maj <- parseInt maj_s -> Right (f maj 0, args)
+                        | otherwise -> Left ("malformed version argument in " ++ dash_arg)
+
 
 findArg :: [Flag m] -> String -> Maybe (String, OptKind m)
 findArg spec arg =
@@ -222,6 +231,7 @@ arg_ok (OptPrefix       _)  _    _   = True
 arg_ok (PassFlag        _)  rest _   = null rest
 arg_ok (AnySuffix       _)  _    _   = True
 arg_ok (AnySuffixPred p _)  _    arg = p arg
+arg_ok (VersionSuffix   _)  _    _   = True
 
 -- | Parse an Int
 --
diff --git a/compiler/main/DriverPipeline.hs b/compiler/main/DriverPipeline.hs
index b128c1f107..c24bb51833 100644
--- a/compiler/main/DriverPipeline.hs
+++ b/compiler/main/DriverPipeline.hs
@@ -1232,18 +1232,18 @@ runPhase As input_fn dflags
         let whichAsProg | hscTarget dflags == HscLlvm &&
                           platformOS (targetPlatform dflags) == OSDarwin
                         = do
+                            -- be careful what options we call clang with
+                            -- see #5903 and #7617 for bugs caused by this.
                             llvmVer <- liftIO $ figureLlvmVersion dflags
                             return $ case llvmVer of
-                                Just n | n >= 30 ->
-                                    (SysTools.runClang, getOpts dflags opt_c)
+                                Just n | n >= 30 -> SysTools.runClang
+                                _                -> SysTools.runAs
 
-                                _ -> (SysTools.runAs, getOpts dflags opt_a)
+                        | otherwise = return SysTools.runAs
 
-                        | otherwise
-                        = return (SysTools.runAs, getOpts dflags opt_a)
-
-        (as_prog, as_opts) <- whichAsProg
-        let cmdline_include_paths = includePaths dflags
+        as_prog <- whichAsProg
+        let as_opts = getOpts dflags opt_a
+            cmdline_include_paths = includePaths dflags
 
         next_phase <- maybeMergeStub
         output_fn <- phaseOutputFilename next_phase
@@ -1436,7 +1436,8 @@ runPhase LlvmLlc input_fn dflags
                 ++ map SysTools.Option lc_opts
                 ++ [SysTools.Option tbaa]
                 ++ map SysTools.Option fpOpts
-                ++ map SysTools.Option abiOpts)
+                ++ map SysTools.Option abiOpts
+                ++ map SysTools.Option sseOpts)
 
     return (next_phase, output_fn)
   where
@@ -1462,6 +1463,10 @@ runPhase LlvmLlc input_fn dflags
                     ArchARM ARMv7 _ _    -> []
                     _                    -> []
 
+        sseOpts | isSse4_2Enabled dflags = ["-mattr=+sse42"]
+                | isSse2Enabled dflags   = ["-mattr=+sse2"]
+                | otherwise              = []
+
 -----------------------------------------------------------------------------
 -- LlvmMangle phase
 
@@ -1747,7 +1752,16 @@ linkBinary dflags o_files dep_packages = do
                   rpath = if gopt Opt_RPath dflags
                           then ["-Wl,-rpath",      "-Wl," ++ libpath]
                           else []
-              in ["-L" ++ l, "-Wl,-rpath-link", "-Wl," ++ l] ++ rpath
+                  -- Solaris 11's linker does not support -rpath-link option. It silently
+                  -- ignores it and then complains about next option which is -l<some
+                  -- dir> as being a directory and not expected object file, E.g
+                  -- ld: elf error: file
+                  -- /tmp/ghc-src/libraries/base/dist-install/build:
+                  -- elf_begin: I/O error: region read: Is a directory
+                  rpathlink = if (platformOS platform) == OSSolaris2
+                              then []
+                              else ["-Wl,-rpath-link", "-Wl," ++ l]
+              in ["-L" ++ l] ++ rpathlink ++ rpath
          | otherwise = ["-L" ++ l]
 
     let lib_paths = libraryPaths dflags
@@ -1814,7 +1828,7 @@ linkBinary dflags o_files dep_packages = do
             let os = platformOS (targetPlatform dflags)
             in if os == OSOsf3 then ["-lpthread", "-lexc"]
                else if os `elem` [OSMinGW32, OSFreeBSD, OSOpenBSD,
-                                  OSNetBSD, OSHaiku]
+                                  OSNetBSD, OSHaiku, OSQNXNTO]
                then []
                else ["-lpthread"]
          | otherwise               = []
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 4edeb23ef4..feadd3d6a8 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -322,8 +322,6 @@ data GeneralFlag
    | Opt_EmitExternalCore
    | Opt_SharedImplib
    | Opt_BuildingCabalPackage
-   | Opt_SSE2
-   | Opt_SSE4_2
    | Opt_IgnoreDotGhci
    | Opt_GhciSandbox
    | Opt_GhciHistory
@@ -425,6 +423,7 @@ data WarningFlag =
    | Opt_WarnSafe
    | Opt_WarnPointlessPragmas
    | Opt_WarnUnsupportedCallingConventions
+   | Opt_WarnUnsupportedLlvmVersion
    | Opt_WarnInlineRuleShadowing
    deriving (Eq, Show, Enum)
 
@@ -710,7 +709,10 @@ data DynFlags = DynFlags {
 
   llvmVersion           :: IORef Int,
 
-  nextWrapperNum        :: IORef Int
+  nextWrapperNum        :: IORef Int,
+
+  -- | Machine dependant flags (-m<blah> stuff)
+  sseVersion            :: Maybe (Int, Int)  -- (major, minor)
  }
 
 class HasDynFlags m where
@@ -1304,7 +1306,8 @@ defaultDynFlags mySettings =
         profAuto = NoProfAuto,
         llvmVersion = panic "defaultDynFlags: No llvmVersion",
         interactivePrint = Nothing,
-        nextWrapperNum = panic "defaultDynFlags: No nextWrapperNum"
+        nextWrapperNum = panic "defaultDynFlags: No nextWrapperNum",
+        sseVersion = Nothing
       }
 
 defaultWays :: Settings -> [Way]
@@ -2180,13 +2183,7 @@ dynamic_flags = [
   , Flag "monly-2-regs" (NoArg (addWarn "The -monly-2-regs flag does nothing; it will be removed in a future GHC release"))
   , Flag "monly-3-regs" (NoArg (addWarn "The -monly-3-regs flag does nothing; it will be removed in a future GHC release"))
   , Flag "monly-4-regs" (NoArg (addWarn "The -monly-4-regs flag does nothing; it will be removed in a future GHC release"))
-  , Flag "msse2"        (NoArg (setGeneralFlag Opt_SSE2))
-  , Flag "msse4.2"      (NoArg (setGeneralFlag Opt_SSE4_2))
-    -- at some point we should probably have a single SSE flag that
-    -- contains the SSE version, instead of having a different flag
-    -- per version. That would make it easier to e.g. check if SSE2 is
-    -- enabled as you wouldn't have to check if either Opt_SSE2 or
-    -- Opt_SSE4_2 is set (as the latter implies the former).
+  , Flag "msse"         (versionSuffix (\maj min d -> d{ sseVersion = Just (maj, min) }))
 
      ------ Warning opts -------------------------------------------------
   , Flag "W"      (NoArg (mapM_ setWarningFlag minusWOpts))
@@ -2398,7 +2395,8 @@ fWarningFlags = [
   ( "warn-safe",                        Opt_WarnSafe, setWarnSafe ),
   ( "warn-pointless-pragmas",           Opt_WarnPointlessPragmas, nop ),
   ( "warn-unsupported-calling-conventions", Opt_WarnUnsupportedCallingConventions, nop ),
-  ( "warn-inline-rule-shadowing",       Opt_WarnInlineRuleShadowing, nop ) ]
+  ( "warn-inline-rule-shadowing",       Opt_WarnInlineRuleShadowing, nop ),
+  ( "warn-unsupported-llvm-version",    Opt_WarnUnsupportedLlvmVersion, nop ) ]
 
 -- | These @-\<blah\>@ flags can all be reversed with @-no-\<blah\>@
 negatableFlags :: [FlagSpec GeneralFlag]
@@ -2783,6 +2781,7 @@ standardWarnings
         Opt_WarnAlternativeLayoutRuleTransitional,
         Opt_WarnPointlessPragmas,
         Opt_WarnUnsupportedCallingConventions,
+        Opt_WarnUnsupportedLlvmVersion,
         Opt_WarnInlineRuleShadowing,
         Opt_WarnDuplicateConstraints
       ]
@@ -2941,6 +2940,9 @@ optIntSuffixM :: (Maybe Int -> DynFlags -> DynP DynFlags)
               -> OptKind (CmdLineP DynFlags)
 optIntSuffixM fn = OptIntSuffix (\mi -> updM (fn mi))
 
+versionSuffix :: (Int -> Int -> DynFlags -> DynFlags) -> OptKind (CmdLineP DynFlags)
+versionSuffix fn = VersionSuffix (\maj min -> upd (fn maj min))
+
 setDumpFlag :: DumpFlag -> OptKind (CmdLineP DynFlags)
 setDumpFlag dump_flag = NoArg (setDumpFlag' dump_flag)
 
@@ -3374,7 +3376,7 @@ makeDynFlagsConsistent dflags
       else let dflags' = dflags { hscTarget = HscLlvm }
                warn = "Compiler not unregisterised, so using LLVM rather than compiling via C"
            in loop dflags' warn
- | hscTarget dflags /= HscC &&
+ | hscTarget dflags /= HscC && hscTarget dflags /= HscLlvm &&
    platformUnregisterised (targetPlatform dflags)
     = loop (dflags { hscTarget = HscC })
            "Compiler unregisterised, so compiling via C"
@@ -3408,18 +3410,20 @@ makeDynFlagsConsistent dflags
 -- -----------------------------------------------------------------------------
 -- SSE
 
+-- TODO: Instead of using a separate predicate (i.e. isSse2Enabled) to
+-- check if SSE is enabled, we might have x86-64 imply the -msse2
+-- flag.
+
 isSse2Enabled :: DynFlags -> Bool
-isSse2Enabled dflags = isSse4_2Enabled dflags || isSse2Enabled'
-  where
-    isSse2Enabled' = case platformArch (targetPlatform dflags) of
-        ArchX86_64 -> -- SSE2 is fixed on for x86_64.  It would be
-                      -- possible to make it optional, but we'd need to
-                      -- fix at least the foreign call code where the
-                      -- calling convention specifies the use of xmm regs,
-                      -- and possibly other places.
-                      True
-        ArchX86    -> gopt Opt_SSE2 dflags
-        _          -> False
+isSse2Enabled dflags = case platformArch (targetPlatform dflags) of
+    ArchX86_64 -> -- SSE2 is fixed on for x86_64.  It would be
+                  -- possible to make it optional, but we'd need to
+                  -- fix at least the foreign call code where the
+                  -- calling convention specifies the use of xmm regs,
+                  -- and possibly other places.
+                  True
+    ArchX86    -> sseVersion dflags >= Just (2,0)
+    _          -> False
 
 isSse4_2Enabled :: DynFlags -> Bool
-isSse4_2Enabled dflags = gopt Opt_SSE4_2 dflags
+isSse4_2Enabled dflags = sseVersion dflags >= Just (4,2)
diff --git a/compiler/main/HscMain.hs b/compiler/main/HscMain.hs
index 3562f27d5c..2f2b53efba 100644
--- a/compiler/main/HscMain.hs
+++ b/compiler/main/HscMain.hs
@@ -1614,6 +1614,7 @@ hscImport hsc_env str = runInteractiveHsc hsc_env $ do
                      ptext (sLit "parse error in import declaration")
 
 -- | Typecheck an expression (but don't run it)
+-- Returns its most general type
 hscTcExpr :: HscEnv
           -> String -- ^ The expression
           -> IO Type
@@ -1628,6 +1629,7 @@ hscTcExpr hsc_env0 expr = runInteractiveHsc hsc_env0 $ do
                 (text "not an expression:" <+> quotes (text expr))
 
 -- | Find the kind of a type
+-- Currently this does *not* generalise the kinds of the type
 hscKcType
   :: HscEnv
   -> Bool            -- ^ Normalise the type
diff --git a/compiler/main/HscStats.lhs b/compiler/main/HscStats.lhs
deleted file mode 100644
index 299f688359..0000000000
--- a/compiler/main/HscStats.lhs
+++ /dev/null
@@ -1,187 +0,0 @@
-%
-% (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
-%
-\section[GHC_Stats]{Statistics for per-module compilations}
-
-\begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
-
-module HscStats ( ppSourceStats ) where
-
-#include "HsVersions.h"
-
-import HsSyn
-import Outputable
-import SrcLoc
-import Bag
-import Util
-import RdrName
-
-import Data.Char
-\end{code}
-
-%************************************************************************
-%*									*
-\subsection{Statistics}
-%*									*
-%************************************************************************
-
-\begin{code}
-ppSourceStats :: Bool -> Located (HsModule RdrName) -> SDoc
-ppSourceStats short (L _ (HsModule _ exports imports ldecls _ _))
- = (if short then hcat else vcat)
-        (map pp_val
-	       [("ExportAll        ", export_all), -- 1 if no export list
-		("ExportDecls      ", export_ds),
-		("ExportModules    ", export_ms),
-		("Imports          ", imp_no),
-		("  ImpSafe        ", imp_safe),
-		("  ImpQual        ", imp_qual),
-		("  ImpAs          ", imp_as),
-		("  ImpAll         ", imp_all),
-		("  ImpPartial     ", imp_partial),
-		("  ImpHiding      ", imp_hiding),
-		("FixityDecls      ", fixity_sigs),
-		("DefaultDecls     ", default_ds),
-	      	("TypeDecls        ", type_ds),
-	      	("DataDecls        ", data_ds),
-	      	("NewTypeDecls     ", newt_ds),
-	      	("TypeFamilyDecls  ", type_fam_ds),
-	      	("DataConstrs      ", data_constrs),
-		("DataDerivings    ", data_derivs),
-	      	("ClassDecls       ", class_ds),
-	      	("ClassMethods     ", class_method_ds),
-	      	("DefaultMethods   ", default_method_ds),
-	      	("InstDecls        ", inst_ds),
-	      	("InstMethods      ", inst_method_ds),
-	      	("InstType         ", inst_type_ds),
-	      	("InstData         ", inst_data_ds),
-	      	("TypeSigs         ", bind_tys),
-	      	("GenericSigs      ", generic_sigs),
-	      	("ValBinds         ", val_bind_ds),
-	      	("FunBinds         ", fn_bind_ds),
-	      	("InlineMeths      ", method_inlines),
-		("InlineBinds      ", bind_inlines),
---	      	("SpecialisedData  ", data_specs),
---	      	("SpecialisedInsts ", inst_specs),
-	      	("SpecialisedMeths ", method_specs),
-	      	("SpecialisedBinds ", bind_specs)
-	       ])
-  where
-    decls = map unLoc ldecls
-
-    pp_val (_, 0) = empty
-    pp_val (str, n) 
-      | not short   = hcat [text str, int n]
-      | otherwise   = hcat [text (trim str), equals, int n, semi]
-    
-    trim ls     = takeWhile (not.isSpace) (dropWhile isSpace ls)
-
-    (fixity_sigs, bind_tys, bind_specs, bind_inlines, generic_sigs) 
-	= count_sigs [d | SigD d <- decls]
-		-- NB: this omits fixity decls on local bindings and
-		-- in class decls.  ToDo
-
-    tycl_decls  = [d | TyClD d <- decls]
-    (class_ds, type_ds, data_ds, newt_ds, type_fam_ds) = 
-      countTyClDecls tycl_decls
-
-    inst_decls  = [d | InstD d <- decls]
-    inst_ds     = length inst_decls
-    default_ds  = count (\ x -> case x of { DefD{} -> True; _ -> False}) decls
-    val_decls   = [d | ValD d <- decls]
-
-    real_exports = case exports of { Nothing -> []; Just es -> es }
-    n_exports  	 = length real_exports
-    export_ms  	 = count (\ e -> case unLoc e of { IEModuleContents{} -> True;_ -> False})
-                         real_exports
-    export_ds  	 = n_exports - export_ms
-    export_all 	 = case exports of { Nothing -> 1; _ -> 0 }
-
-    (val_bind_ds, fn_bind_ds)
-	= foldr add2 (0,0) (map count_bind val_decls)
-
-    (imp_no, imp_safe, imp_qual, imp_as, imp_all, imp_partial, imp_hiding)
-	= foldr add7 (0,0,0,0,0,0,0) (map import_info imports)
-    (data_constrs, data_derivs)
-	= foldr add2 (0,0) (map data_info tycl_decls)
-    (class_method_ds, default_method_ds)
-	= foldr add2 (0,0) (map class_info tycl_decls)
-    (inst_method_ds, method_specs, method_inlines, inst_type_ds, inst_data_ds)
-	= foldr add5 (0,0,0,0,0) (map inst_info inst_decls)
-
-    count_bind (PatBind { pat_lhs = L _ (VarPat _) }) = (1,0)
-    count_bind (PatBind {})                           = (0,1)
-    count_bind (FunBind {})                           = (0,1)
-    count_bind b = pprPanic "count_bind: Unhandled binder" (ppr b)
-
-    count_sigs sigs = foldr add5 (0,0,0,0,0) (map sig_info sigs)
-
-    sig_info (FixSig _)		= (1,0,0,0,0)
-    sig_info (TypeSig _ _)      = (0,1,0,0,0)
-    sig_info (SpecSig _ _ _)    = (0,0,1,0,0)
-    sig_info (InlineSig _ _)    = (0,0,0,1,0)
-    sig_info (GenericSig _ _)   = (0,0,0,0,1)
-    sig_info _                  = (0,0,0,0,0)
-
-    import_info (L _ (ImportDecl { ideclSafe = safe, ideclQualified = qual
-                                 , ideclAs = as, ideclHiding = spec }))
-	= add7 (1, safe_info safe, qual_info qual, as_info as, 0,0,0) (spec_info spec)
-    safe_info = qual_info
-    qual_info False  = 0
-    qual_info True   = 1
-    as_info Nothing  = 0
-    as_info (Just _) = 1
-    spec_info Nothing 	        = (0,0,0,0,1,0,0)
-    spec_info (Just (False, _)) = (0,0,0,0,0,1,0)
-    spec_info (Just (True, _))  = (0,0,0,0,0,0,1)
-
-    data_info (SynDecl { tcdTyDefn = TyData {td_cons = cs, td_derivs = derivs}})
-	= (length cs, case derivs of Nothing -> 0
-				     Just ds -> length ds)
-    data_info _ = (0,0)
-
-    class_info decl@(ClassDecl {})
-	= case count_sigs (map unLoc (tcdSigs decl)) of
-	    (_,classops,_,_,_) ->
-	       (classops, addpr (foldr add2 (0,0) (map (count_bind.unLoc) (bagToList (tcdMeths decl)))))
-    class_info _ = (0,0)
-
-    inst_info (FamInstD d) = case countATDecl d of
-                                  (tyd, dtd) -> (0,0,0,tyd,dtd)
-    inst_info (ClsInstD _ inst_meths inst_sigs ats)
-	= case count_sigs (map unLoc inst_sigs) of
-	    (_,_,ss,is,_) ->
-	      case foldr add2 (0, 0) (map (countATDecl . unLoc) ats) of
-	        (SynDecl, dtDecl) ->
-	          (addpr (foldr add2 (0,0) 
-			   (map (count_bind.unLoc) (bagToList inst_meths))), 
-                   ss, is, SynDecl, dtDecl)
-        where
-    countATDecl (FamInstDecl { fid_defn = TyData    {} }) = (0, 1)
-    countATDecl (FamInstDecl { fid_defn = TySynonym {} }) = (1, 0)
-
-    addpr :: (Int,Int) -> Int
-    add2  :: (Int,Int) -> (Int,Int) -> (Int, Int)
-    add5  :: (Int,Int,Int,Int,Int) -> (Int,Int,Int,Int,Int) -> (Int, Int, Int, Int, Int)
-    add7  :: (Int,Int,Int,Int,Int,Int,Int) -> (Int,Int,Int,Int,Int,Int,Int) -> (Int, Int, Int, Int, Int, Int, Int)
-
-    addpr (x,y) = x+y
-    add2 (x1,x2) (y1,y2) = (x1+y1,x2+y2)
-    add5 (x1,x2,x3,x4,x5) (y1,y2,y3,y4,y5) = (x1+y1,x2+y2,x3+y3,x4+y4,x5+y5)
-    add7 (x1,x2,x3,x4,x5,x6,x7) (y1,y2,y3,y4,y5,y6,y7) = (x1+y1,x2+y2,x3+y3,x4+y4,x5+y5,x6+y6,x7+y7)
-\end{code}
-
-
-
-
-
-
-
-
-
diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs
index 7fa156aec3..8d64900c71 100644
--- a/compiler/main/InteractiveEval.hs
+++ b/compiler/main/InteractiveEval.hs
@@ -972,6 +972,7 @@ parseName str = withSession $ \hsc_env -> do
 -- Getting the type of an expression
 
 -- | Get the type of an expression
+-- Returns its most general type
 exprType :: GhcMonad m => String -> m Type
 exprType expr = withSession $ \hsc_env -> do
    ty <- liftIO $ hscTcExpr hsc_env expr
diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs
index 932b46c2f5..a60644155f 100644
--- a/compiler/main/PprTyThing.hs
+++ b/compiler/main/PprTyThing.hs
@@ -33,6 +33,7 @@ import Coercion( pprCoAxiom )
 import HscTypes( tyThingParent_maybe )
 import TcType
 import Name
+import VarEnv( emptyTidyEnv )
 import StaticFlags( opt_PprStyle_Debug )
 import Outputable
 import FastString
@@ -161,8 +162,12 @@ pprTypeForUser print_foralls ty
   | print_foralls = ppr tidy_ty
   | otherwise     = ppr (mkPhiTy ctxt ty')
   where
-    tidy_ty     = tidyTopType ty
     (_, ctxt, ty') = tcSplitSigmaTy tidy_ty
+    (_, tidy_ty)   = tidyOpenType emptyTidyEnv ty
+     -- Often the types/kinds we print in ghci are fully generalised
+     -- and have no free variables, but it turns out that we sometimes
+     -- print un-generalised kinds (eg when doing :k T), so it's
+     -- better to use tidyOpenType here
 
 pprTyCon :: PrintExplicitForalls -> ShowSub -> TyCon -> SDoc
 pprTyCon pefas ss tyCon
diff --git a/compiler/main/SysTools.lhs b/compiler/main/SysTools.lhs
index f4e5f2cf0f..28ff49969d 100644
--- a/compiler/main/SysTools.lhs
+++ b/compiler/main/SysTools.lhs
@@ -527,12 +527,19 @@ runClang :: DynFlags -> [Option] -> IO ()
 runClang dflags args = do
   -- we simply assume its available on the PATH
   let clang = "clang"
+      -- be careful what options we call clang with
+      -- see #5903 and #7617 for bugs caused by this.
+      (_,args0) = pgm_a dflags
+      args1 = args0 ++ args
+  mb_env <- getGccEnv args1
   Exception.catch (do
-        runSomething dflags "Clang (Assembler)" clang args
+        runSomethingFiltered dflags id "Clang (Assembler)" clang args1 mb_env
     )
     (\(err :: SomeException) -> do
-        errorMsg dflags $ text $ "Error running clang! you need clang installed"
-                              ++ " to use the LLVM backend"
+        errorMsg dflags $
+            text ("Error running clang! you need clang installed to use the" ++
+                "LLVM backend") $+$
+            text "(or GHC tried to execute clang incorrectly)"
         throw err
     )
 
diff --git a/compiler/main/TidyPgm.lhs b/compiler/main/TidyPgm.lhs
index bc4c6b9abf..990f6cd8ec 100644
--- a/compiler/main/TidyPgm.lhs
+++ b/compiler/main/TidyPgm.lhs
@@ -29,7 +29,7 @@ import Id
 import IdInfo
 import InstEnv
 import FamInstEnv
-import Demand
+import Demand           ( appIsBottom, isTopSig, isBottomingSig )
 import BasicTypes
 import Name hiding (varName)
 import NameSet
@@ -420,6 +420,8 @@ tidyTypeEnv :: Bool       -- Compiling without -O, so omit prags
 --          the externally-accessible ones
 -- This truncates the type environment to include only the
 -- exported Ids and things needed from them, which saves space
+--
+-- See Note [Don't attempt to trim data types]
 
 tidyTypeEnv omit_prags type_env
  = let
@@ -469,6 +471,33 @@ tidyVectInfo (_, var_env) info@(VectInfo { vectInfoVar          = vars
     lookup_var var = lookupWithDefaultVarEnv var_env var var
 \end{code}
 
+Note [Don't attempt to trim data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For some time GHC tried to avoid exporting the data constructors
+of a data type if it wasn't strictly necessary to do so; see Trac #835.
+But "strictly necessary" accumulated a longer and longer list 
+of execeptions, and finally I gave up the battle:
+
+    commit 9a20e540754fc2af74c2e7392f2786a81d8d5f11
+    Author: Simon Peyton Jones <simonpj@microsoft.com>
+    Date:   Thu Dec 6 16:03:16 2012 +0000
+
+    Stop attempting to "trim" data types in interface files
+    
+    Without -O, we previously tried to make interface files smaller
+    by not including the data constructors of data types.  But
+    there are a lot of exceptions, notably when Template Haskell is
+    involved or, more recently, DataKinds.
+    
+    However Trac #7445 shows that even without TemplateHaskell, using
+    the Data class and invoking Language.Haskell.TH.Quote.dataToExpQ
+    is enough to require us to expose the data constructors.
+    
+    So I've given up on this "optimisation" -- it's probably not
+    important anyway.  Now I'm simply not attempting to trim off
+    the data constructors.  The gain in simplicity is worth the
+    modest cost in interface file growth, which is limited to the
+    bits reqd to describe those data constructors.
 
 %************************************************************************
 %*                                                                      *
@@ -663,7 +692,7 @@ addExternal expose_all id = (new_needed_ids, show_unfold)
     show_unfold    = show_unfolding (unfoldingInfo idinfo)
     never_active   = isNeverActive (inlinePragmaActivation (inlinePragInfo idinfo))
     loop_breaker   = isStrongLoopBreaker (occInfo idinfo)
-    bottoming_fn   = isBottomingSig (strictnessInfo idinfo `orElse` topSig)
+    bottoming_fn   = isBottomingSig (strictnessInfo idinfo)
 
         -- Stuff to do with the Id's unfolding
         -- We leave the unfolding there even if there is a worker
@@ -1069,27 +1098,25 @@ tidyTopIdInfo dflags rhs_tidy_env name orig_rhs tidy_rhs idinfo show_unfold caf_
     -- when we are doing -fexpose-all-unfoldings
 
     --------- Strictness ------------
-    final_sig | Just sig <- strictnessInfo idinfo
-              = WARN( _bottom_hidden sig, ppr name ) Just sig
-              | Just (_, sig) <- mb_bot_str = Just sig
-              | otherwise                   = Nothing
+    mb_bot_str = exprBotStrictness_maybe orig_rhs
 
-    -- If the cheap-and-cheerful bottom analyser can see that
-    -- the RHS is bottom, it should jolly well be exposed
-    _bottom_hidden id_sig = case mb_bot_str of
-                               Nothing         -> False
-                               Just (arity, _) -> not (appIsBottom id_sig arity)
+    sig = strictnessInfo idinfo
+    final_sig | not $ isTopSig sig 
+                 = WARN( _bottom_hidden sig , ppr name ) sig 
+                 -- try a cheap-and-cheerful bottom analyser
+                 | Just (_, nsig) <- mb_bot_str = nsig
+                 | otherwise                    = sig
 
-    mb_bot_str = exprBotStrictness_maybe orig_rhs
+    _bottom_hidden id_sig = case mb_bot_str of
+                                  Nothing         -> False
+                                  Just (arity, _) -> not (appIsBottom id_sig arity)
 
     --------- Unfolding ------------
     unf_info = unfoldingInfo idinfo
     unfold_info | show_unfold = tidyUnfolding rhs_tidy_env unf_info unf_from_rhs
                 | otherwise   = noUnfolding
     unf_from_rhs = mkTopUnfolding dflags is_bot tidy_rhs
-    is_bot = case final_sig of
-                Just sig -> isBottomingSig sig
-                Nothing  -> False
+    is_bot = isBottomingSig final_sig
     -- NB: do *not* expose the worker if show_unfold is off,
     --     because that means this thing is a loop breaker or
     --     marked NOINLINE or something like that
diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index 77236a1727..6d551d90e5 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -45,10 +45,9 @@ defaults
    can_fail         = False   -- See Note Note [PrimOp can_fail and has_side_effects] in PrimOp
    commutable       = False
    code_size        = { primOpCodeSizeDefault }
-   strictness       = { \ arity -> mkStrictSig (mkTopDmdType (replicate arity lazyDmd) TopRes) }
+   strictness       = { \ arity -> mkStrictSig (mkTopDmdType (replicate arity topDmd) topRes) }
    fixity           = Nothing
 
-
 -- Currently, documentation is produced using latex, so contents of
 -- description fields should be legal latex. Descriptions can contain
 -- matched pairs of embedded curly brackets.
@@ -1530,7 +1529,7 @@ primop  CatchOp "catch#" GenPrimOp
 primop  RaiseOp "raise#" GenPrimOp
    a -> b
    with
-   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [lazyDmd] BotRes) }
+   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [topDmd] botRes) }
       -- NB: result is bottom
    out_of_line = True
 
@@ -1547,7 +1546,7 @@ primop  RaiseOp "raise#" GenPrimOp
 primop  RaiseIOOp "raiseIO#" GenPrimOp
    a -> State# RealWorld -> (# State# RealWorld, b #)
    with
-   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [lazyDmd,lazyDmd] BotRes) }
+   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [topDmd, topDmd] botRes) }
    out_of_line = True
    has_side_effects = True
 
@@ -2028,7 +2027,8 @@ section "Tag to enum stuff"
 primop  DataToTagOp "dataToTag#" GenPrimOp
    a -> Int#
    with
-   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [seqDmd] TopRes) }
+   strictness  = { \ _arity -> mkStrictSig (mkTopDmdType [evalDmd] topRes) }
+
 	-- dataToTag# must have an evaluated argument
 
 primop  TagToEnumOp "tagToEnum#" GenPrimOp     
diff --git a/compiler/simplCore/CSE.lhs b/compiler/simplCore/CSE.lhs
index 18c0178900..8bd15864c7 100644
--- a/compiler/simplCore/CSE.lhs
+++ b/compiler/simplCore/CSE.lhs
@@ -170,6 +170,12 @@ Now CSE may transform to
 But the WorkerInfo for f still says $wf, which is now dead!  This won't
 happen now that we don't look inside INLINEs (which wrappers are).
 
+Note [CSE for case expressions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  case f x of y { pat -> ...let y = f x in ... }
+Then we can CSE the inner (f x) to y.  In fact 'case' is like a strict
+let-binding, and we can use cseRhs for dealing with the scrutinee.
 
 %************************************************************************
 %*									*
@@ -226,7 +232,7 @@ cseExpr env (Coercion c)           = Coercion (substCo (csEnvSubst env) c)
 cseExpr _   (Lit lit)              = Lit lit
 cseExpr env (Var v)		   = lookupSubst env v
 cseExpr env (App f a)        	   = App (cseExpr env f) (tryForCSE env a)
-cseExpr env (Tick t e)           = Tick t (cseExpr env e)
+cseExpr env (Tick t e)             = Tick t (cseExpr env e)
 cseExpr env (Cast e co)            = Cast (cseExpr env e) (substCo (csEnvSubst env) co)
 cseExpr env (Lam b e)	     	   = let (env', b') = addBinder env b
 				     in Lam b' (cseExpr env' e)
@@ -234,13 +240,14 @@ cseExpr env (Let bind e)    	   = let (env', bind') = cseBind env bind
 				     in Let bind' (cseExpr env' e)
 cseExpr env (Case scrut bndr ty alts) = Case scrut' bndr'' ty alts'
 				   where
-                                     alts' = cseAlts env' scrut' bndr bndr'' alts
-				     scrut' = tryForCSE env scrut
-				     (env', bndr') = addBinder env bndr
+                                     alts' = cseAlts env2 scrut' bndr bndr'' alts
+				     (env1, bndr') = addBinder env bndr
 				     bndr'' = zapIdOccInfo bndr'
 					-- The swizzling from Note [Case binders 2] may
 					-- cause a dead case binder to be alive, so we
 					-- play safe here and bring them all to life
+                                     (env2, scrut') = cseRhs env1 (bndr'', scrut)
+                                        -- Note [CSE for case expressions]
 
 cseAlts :: CSEnv -> OutExpr -> InBndr -> InBndr -> [InAlt] -> [OutAlt]
 
diff --git a/compiler/simplCore/FloatOut.lhs b/compiler/simplCore/FloatOut.lhs
index f5cf9f107d..0a6e8b9357 100644
--- a/compiler/simplCore/FloatOut.lhs
+++ b/compiler/simplCore/FloatOut.lhs
@@ -359,8 +359,12 @@ Here y is demanded.  If we float it outside the lazy 'x=..' then
 we'd have to zap its demand info, and it may never be restored.
 
 So at a 'let' we leave the binding right where the are unless
-the binding will escape a value lambda.  That's what the 
-partitionByMajorLevel does in the floatExpr (Let ...) case.
+the binding will escape a value lambda, e.g.  
+
+(\x -> let y = fac 100 in y)
+
+That's what the partitionByMajorLevel does in the floatExpr (Let ...)
+case.
 
 Notice, though, that we must take care to drop any bindings
 from the body of the let that depend on the staying-put bindings.
diff --git a/compiler/simplCore/SetLevels.lhs b/compiler/simplCore/SetLevels.lhs
index 076df2e67c..78cb0be97b 100644
--- a/compiler/simplCore/SetLevels.lhs
+++ b/compiler/simplCore/SetLevels.lhs
@@ -77,7 +77,7 @@ import Var
 import VarSet
 import VarEnv
 import Literal		( litIsTrivial )
-import Demand		( StrictSig, increaseStrictSigArity )
+import Demand           ( StrictSig, increaseStrictSigArity )
 import Name		( getOccName, mkSystemVarName )
 import OccName		( occNameString )
 import Type		( isUnLiftedType, Type, mkPiTypes )
@@ -100,9 +100,10 @@ type LevelledExpr = TaggedExpr FloatSpec
 type LevelledBind = TaggedBind FloatSpec
 type LevelledBndr = TaggedBndr FloatSpec
 
-data Level = Level Int	-- Level number of enclosing lambdas
-	  	   Int	-- Number of big-lambda and/or case expressions between
-			-- here and the nearest enclosing lambda
+data Level = Level Int	-- Major level: number of enclosing value lambdas
+	  	   Int	-- Minor level: number of big-lambda and/or case 
+                        -- expressions between here and the nearest 
+                        -- enclosing value lambda
 
 data FloatSpec 
   = FloatMe Level	-- Float to just inside the binding 
@@ -563,8 +564,8 @@ Doesn't change any other allocation at all.
 \begin{code}
 annotateBotStr :: Id -> Maybe (Arity, StrictSig) -> Id
 annotateBotStr id Nothing            = id
-annotateBotStr id (Just (arity,sig)) = id `setIdArity` arity
-				          `setIdStrictness` sig
+annotateBotStr id (Just (arity, sig)) = id `setIdArity` arity
+     		                              `setIdStrictness` sig
 
 notWorthFloating :: CoreExprWithFVs -> [Var] -> Bool
 -- Returns True if the expression would be replaced by
@@ -820,7 +821,8 @@ lvlLamBndrs lvl bndrs
 \begin{code}
   -- Destination level is the max Id level of the expression
   -- (We'll abstract the type variables, if any.)
-destLevel :: LevelEnv -> VarSet -> Bool -> Maybe (Arity, StrictSig) -> Level
+destLevel :: LevelEnv -> VarSet -> Bool -> 
+             Maybe (Arity, StrictSig) -> Level
 destLevel env fvs is_function mb_bot
   | Just {} <- mb_bot = tOP_LEVEL	-- Send bottoming bindings to the top 
 					-- regardless; see Note [Bottoming floats]
@@ -1079,9 +1081,10 @@ newLvlVar vars body_ty mb_bot
     arity = count isId vars
     info = case mb_bot of
 		Nothing               -> vanillaIdInfo
-		Just (bot_arity, sig) -> vanillaIdInfo 
-					   `setArityInfo`      (arity + bot_arity)
-					   `setStrictnessInfo` Just (increaseStrictSigArity arity sig)
+		Just (bot_arity, sig) -> 
+                     vanillaIdInfo 
+		    `setArityInfo`      (arity + bot_arity)
+		    `setStrictnessInfo` (increaseStrictSigArity arity sig)
     
 -- The deeply tiresome thing is that we have to apply the substitution
 -- to the rules inside each Id.  Grr.  But it matters.
@@ -1114,7 +1117,9 @@ cloneVar :: LevelEnv -> Var -> Level -> LvlM (LevelEnv, Var)
 cloneVar env v dest_lvl -- Works for Ids, TyVars and CoVars
   = do { u <- getUniqueM
        ; let (subst', v1) = cloneBndr (le_subst env) u v
-      	     v2     	  = if isId v1 then zapDemandIdInfo v1 else v1
+      	     v2     	  = if isId v1 
+                            then zapDemandIdInfo v1  
+                            else v1
       	     env'	  = extendCloneLvlEnv dest_lvl env subst' [(v,v2)]
        ; return (env', v2) }
 
@@ -1127,7 +1132,8 @@ cloneRecVars env vs dest_lvl -- Works for CoVars too (since cloneRecIdBndrs does
     us <- getUniqueSupplyM
     let
       (subst', vs1) = cloneRecIdBndrs (le_subst env) us vs
-      vs2	    = map zapDemandIdInfo vs1  -- Note [Zapping the demand info]
+      -- Note [Zapping the demand info]
+      vs2	    = map zapDemandIdInfo vs1  
       env'	    = extendCloneLvlEnv dest_lvl env subst' (vs `zip` vs2)
     return (env', vs2)
 \end{code}
diff --git a/compiler/simplCore/SimplCore.lhs b/compiler/simplCore/SimplCore.lhs
index 8d2a667bf6..8270260e16 100644
--- a/compiler/simplCore/SimplCore.lhs
+++ b/compiler/simplCore/SimplCore.lhs
@@ -43,7 +43,7 @@ import LiberateCase     ( liberateCase )
 import SAT              ( doStaticArgs )
 import Specialise       ( specProgram)
 import SpecConstr       ( specConstrProgram)
-import DmdAnal          ( dmdAnalPgm )
+import DmdAnal       ( dmdAnalProgram )
 import WorkWrap         ( wwTopBinds )
 import Vectorise        ( vectorise )
 import FastString
@@ -190,6 +190,13 @@ getCoreToDo dflags
                           -- Don't do case-of-case transformations.
                           -- This makes full laziness work better
 
+    -- New demand analyser
+    demand_analyser = (CoreDoPasses ([
+                           CoreDoStrictness,
+                           CoreDoWorkerWrapper,
+                           simpl_phase 0 ["post-worker-wrapper"] max_iter
+                           ]))
+
     core_todo =
      if opt_level == 0 then
        [ vectorisation
@@ -256,11 +263,7 @@ getCoreToDo dflags
                 -- Don't stop now!
         simpl_phase 0 ["main"] (max max_iter 3),
 
-        runWhen strictness (CoreDoPasses [
-                CoreDoStrictness,
-                CoreDoWorkerWrapper,
-                simpl_phase 0 ["post-worker-wrapper"] max_iter
-                ]),
+        runWhen strictness demand_analyser,
 
         runWhen full_laziness $
            CoreDoFloatOutwards FloatOutSwitches {
@@ -387,8 +390,8 @@ doCorePass _      (CoreDoFloatOutwards f)   = {-# SCC "FloatOutwards" #-}
 doCorePass _      CoreDoStaticArgs          = {-# SCC "StaticArgs" #-}
                                               doPassU doStaticArgs
 
-doCorePass _      CoreDoStrictness          = {-# SCC "Stranal" #-}
-                                              doPassDM dmdAnalPgm
+doCorePass _      CoreDoStrictness          = {-# SCC "NewStranal" #-}
+                                              doPassDM dmdAnalProgram
 
 doCorePass dflags CoreDoWorkerWrapper       = {-# SCC "WorkWrap" #-}
                                               doPassU (wwTopBinds dflags)
@@ -896,7 +899,7 @@ transferIdInfo exported_id local_id
   = modifyIdInfo transfer exported_id
   where
     local_info = idInfo local_id
-    transfer exp_info = exp_info `setStrictnessInfo` strictnessInfo local_info
+    transfer exp_info = exp_info `setStrictnessInfo`    strictnessInfo local_info
                                  `setUnfoldingInfo`     unfoldingInfo local_info
                                  `setInlinePragInfo`    inlinePragInfo local_info
                                  `setSpecInfo`          addSpecInfo (specInfo exp_info) new_info
diff --git a/compiler/simplCore/Simplify.lhs b/compiler/simplCore/Simplify.lhs
index d3688f589c..2d00d296ff 100644
--- a/compiler/simplCore/Simplify.lhs
+++ b/compiler/simplCore/Simplify.lhs
@@ -454,7 +454,7 @@ prepareRhs top_lvl env id (Cast rhs co)    -- Note [Float coercions]
         ; return (env', Cast rhs' co) }
   where
     sanitised_info = vanillaIdInfo `setStrictnessInfo` strictnessInfo info
-                                   `setDemandInfo`     demandInfo info
+                                   `setDemandInfo` demandInfo info
     info = idInfo id
 
 prepareRhs top_lvl env0 _ rhs0
@@ -676,8 +676,7 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
               -- than that of the strictness sig. This can happen: see Note [Arity decrease].
             info3 | isEvaldUnfolding new_unfolding
                     || (case strictnessInfo info2 of
-                          Just (StrictSig dmd_ty) -> new_arity < dmdTypeDepth dmd_ty
-                          Nothing                 -> False)
+                          StrictSig dmd_ty -> new_arity < dmdTypeDepth dmd_ty)
                   = zapDemandInfo info2 `orElse` info2
                   | otherwise
                   = info2
diff --git a/compiler/specialise/SpecConstr.lhs b/compiler/specialise/SpecConstr.lhs
index 7a01ee2ee5..3dc527475f 100644
--- a/compiler/specialise/SpecConstr.lhs
+++ b/compiler/specialise/SpecConstr.lhs
@@ -42,7 +42,6 @@ import DynFlags         ( DynFlags(..) )
 import StaticFlags      ( opt_PprStyle_Debug )
 import Maybes           ( orElse, catMaybes, isJust, isNothing )
 import Demand
-import DmdAnal          ( both )
 import Serialized       ( deserializeWithData )
 import Util
 import Pair
@@ -1386,22 +1385,24 @@ spec_one env fn arg_bndrs body (call_pat@(qvars, pats), rule_number)
               -- changes (#4012).
               rule_name  = mkFastString ("SC:" ++ occNameString fn_occ ++ show rule_number)
               spec_name  = mkInternalName spec_uniq spec_occ fn_loc
---      ; pprTrace "{spec_one" (ppr (sc_count env) <+> ppr fn <+> ppr pats <+> text "-->" <+> ppr spec_name) $
+--      ; pprTrace "{spec_one" (ppr (sc_count env) <+> ppr fn <+> ppr pats <+> text "-->" <+> ppr spec_name) $ 
 --        return ()
 
         -- Specialise the body
         ; (spec_usg, spec_body) <- scExpr spec_env body
 
---      ; pprTrace "done spec_one}" (ppr fn) $
+--      ; pprTrace "done spec_one}" (ppr fn) $ 
 --        return ()
 
                 -- And build the results
-        ; let spec_id = mkLocalId spec_name (mkPiTypes spec_lam_args body_ty)
-                             `setIdStrictness` spec_str         -- See Note [Transfer strictness]
+        ; let spec_id = mkLocalId spec_name (mkPiTypes spec_lam_args body_ty) 
+                             -- See Note [Transfer strictness]
+                             `setIdStrictness` spec_str
                              `setIdArity` count isId spec_lam_args
               spec_str   = calcSpecStrictness fn spec_lam_args pats
-              (spec_lam_args, spec_call_args) = mkWorkerArgs qvars body_ty
-                -- Usual w/w hack to avoid generating
+                -- Conditionally use result of new worker-wrapper transform
+              (spec_lam_args, spec_call_args) = mkWorkerArgs qvars False body_ty
+                -- Usual w/w hack to avoid generating 
                 -- a spec_rhs of unlifted type and no args
 
               spec_rhs   = mkLams spec_lam_args spec_body
@@ -1418,24 +1419,25 @@ calcSpecStrictness :: Id                     -- The original function
                    -> StrictSig              -- Strictness of specialised thing
 -- See Note [Transfer strictness]
 calcSpecStrictness fn qvars pats
-  = StrictSig (mkTopDmdType spec_dmds TopRes)
+  = StrictSig (mkTopDmdType spec_dmds topRes)
   where
-    spec_dmds = [ lookupVarEnv dmd_env qv `orElse` lazyDmd | qv <- qvars, isId qv ]
+    spec_dmds = [ lookupVarEnv dmd_env qv `orElse` topDmd | qv <- qvars, isId qv ]
     StrictSig (DmdType _ dmds _) = idStrictness fn
 
     dmd_env = go emptyVarEnv dmds pats
 
+    go :: DmdEnv -> [Demand] -> [CoreExpr] -> DmdEnv
     go env ds (Type {} : pats) = go env ds pats
     go env ds (Coercion {} : pats) = go env ds pats
     go env (d:ds) (pat : pats) = go (go_one env d pat) ds pats
     go env _      _            = env
 
-    go_one env d   (Var v) = extendVarEnv_C both env v d
-    go_one env (Box d)   e = go_one env d e
-    go_one env (Eval (Prod ds)) e
-           | (Var _, args) <- collectArgs e = go env ds args
+    go_one :: DmdEnv -> Demand -> CoreExpr -> DmdEnv
+    go_one env d   (Var v) = extendVarEnv_C bothDmd env v d
+    go_one env d e 
+           | Just ds <- splitProdDmd_maybe d
+           , (Var _, args) <- collectArgs e = go env ds args
     go_one env _         _ = env
-
 \end{code}
 
 Note [Specialise original body]
diff --git a/compiler/stranal/DmdAnal.lhs b/compiler/stranal/DmdAnal.lhs
index 0ecefa7565..9e38bb7c0d 100644
--- a/compiler/stranal/DmdAnal.lhs
+++ b/compiler/stranal/DmdAnal.lhs
@@ -8,59 +8,36 @@
 
 \begin{code}
 {-# OPTIONS -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
 
-module DmdAnal ( dmdAnalPgm, dmdAnalTopRhs, 
-		 both {- needed by WwLib -}
-   ) where
+module DmdAnal ( dmdAnalProgram ) where
 
 #include "HsVersions.h"
 
+import Var		( isTyVar )
 import DynFlags
+import WwLib            ( deepSplitProductType_maybe )
 import Demand	-- All of it
 import CoreSyn
-import PprCore	
-import Coercion		( isCoVarType )
-import CoreUtils	( exprIsHNF, exprIsTrivial )
-import CoreArity	( exprArity )
-import DataCon		( dataConTyCon, dataConRepStrictness, isMarkedStrict )
-import TyCon		( isProductTyCon, isRecursiveTyCon )
-import Id		( Id, idType, idInlineActivation,
-			  isDataConWorkId, isGlobalId, idArity,
-			  idStrictness, 
-			  setIdStrictness, idDemandInfo, idUnfolding,
-			  idDemandInfo_maybe, setIdDemandInfo
-			)
-import Var		( Var, isTyVar )
+import Outputable
 import VarEnv
-import TysWiredIn	( unboxedPairDataCon )
-import TysPrim		( realWorldStatePrimTy )
-import UniqFM		( addToUFM_Directly, lookupUFM_Directly,
-			  minusUFM, filterUFM )
-import Type		( isUnLiftedType, eqType, tyConAppTyCon_maybe )
+import BasicTypes	
+import FastString
+import Data.List
+import DataCon		( dataConTyCon, dataConRepStrictness, isMarkedStrict )
+import Id
+import CoreUtils	( exprIsHNF, exprIsTrivial )
+import PprCore	
+import UniqFM		( filterUFM )
+import TyCon
+import Pair
+import Type		( eqType, tyConAppTyCon_maybe )
 import Coercion         ( coercionKind )
 import Util
-import BasicTypes	( Arity, TopLevelFlag(..), isTopLevel, isNeverActive,
-			  RecFlag(..), isRec )
-import Maybes		( orElse, expectJust )
-import Outputable
-import Pair
-import Data.List
-import FastString
+import Maybes		( orElse )
+import TysWiredIn	( unboxedPairDataCon )
+import TysPrim		( realWorldStatePrimTy )
 \end{code}
 
-To think about
-
-* set a noinline pragma on bottoming Ids
-
-* Consider f x = x+1 `fatbar` error (show x)
-  We'd like to unbox x, even if that means reboxing it in the error case.
-
-
 %************************************************************************
 %*									*
 \subsection{Top level stuff}
@@ -68,8 +45,9 @@ To think about
 %************************************************************************
 
 \begin{code}
-dmdAnalPgm :: DynFlags -> CoreProgram -> IO CoreProgram
-dmdAnalPgm dflags binds
+
+dmdAnalProgram :: DynFlags -> CoreProgram -> IO CoreProgram
+dmdAnalProgram dflags binds
   = do {
 	let { binds_plus_dmds = do_prog binds } ;
 	return binds_plus_dmds
@@ -78,6 +56,7 @@ dmdAnalPgm dflags binds
     do_prog :: CoreProgram -> CoreProgram
     do_prog binds = snd $ mapAccumL (dmdAnalTopBind dflags) emptySigEnv binds
 
+-- Analyse a (group of) top-level binding(s)
 dmdAnalTopBind :: DynFlags
                -> SigEnv
 	       -> CoreBind 
@@ -97,26 +76,7 @@ dmdAnalTopBind dflags sigs (Rec pairs)
     (sigs', _, pairs')  = dmdFix dflags TopLevel (virgin sigs) pairs
 		-- We get two iterations automatically
 		-- c.f. the NonRec case above
-\end{code}
 
-\begin{code}
-dmdAnalTopRhs :: DynFlags -> CoreExpr -> (StrictSig, CoreExpr)
--- Analyse the RHS and return
---	a) appropriate strictness info
---	b) the unfolding (decorated with strictness info)
-dmdAnalTopRhs dflags rhs
-  = (sig, rhs2)
-  where
-    call_dmd	   = vanillaCall (exprArity rhs)
-    (_,      rhs1) = dmdAnal dflags (virgin emptySigEnv)    call_dmd rhs
-    (rhs_ty, rhs2) = dmdAnal dflags (nonVirgin emptySigEnv) call_dmd rhs1
-    sig		   = mkTopSigTy dflags rhs rhs_ty
-	-- Do two passes; see notes with extendSigsWithLam
-	-- Otherwise we get bogus CPR info for constructors like
-	-- 	newtype T a = MkT a
-	-- The constructor looks like (\x::T a -> x), modulo the coerce
-	-- extendSigsWithLam will optimistically give x a CPR tag the 
-	-- first time, which is wrong in the end.
 \end{code}
 
 %************************************************************************
@@ -125,34 +85,64 @@ dmdAnalTopRhs dflags rhs
 %*									*
 %************************************************************************
 
+Note [Ensure demand is strict]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's important not to analyse e with a lazy demand because
+a) When we encounter   case s of (a,b) -> 
+	we demand s with U(d1d2)... but if the overall demand is lazy
+	that is wrong, and we'd need to reduce the demand on s,
+	which is inconvenient
+b) More important, consider
+	f (let x = R in x+x), where f is lazy
+   We still want to mark x as demanded, because it will be when we
+   enter the let.  If we analyse f's arg with a Lazy demand, we'll
+   just mark x as Lazy
+c) The application rule wouldn't be right either
+   Evaluating (f x) in a L demand does *not* cause
+   evaluation of f in a C(L) demand!
+
+Note [Always analyse in virgin pass]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Tricky point: make sure that we analyse in the 'virgin' pass. Consider
+   rec { f acc x True  = f (...rec { g y = ...g... }...)
+         f acc x False = acc }
+In the virgin pass for 'f' we'll give 'f' a very strict (bottom) type.
+That might mean that we analyse the sub-expression containing the 
+E = "...rec g..." stuff in a bottom demand.  Suppose we *didn't analyse*
+E, but just retuned botType.  
+
+Then in the *next* (non-virgin) iteration for 'f', we might analyse E
+in a weaker demand, and that will trigger doing a fixpoint iteration
+for g.  But *because it's not the virgin pass* we won't start g's
+iteration at bottom.  Disaster.  (This happened in $sfibToList' of 
+nofib/spectral/fibheaps.)
+
+So in the virgin pass we make sure that we do analyse the expression
+at least once, to initialise its signatures.
+
 \begin{code}
-dmdAnal :: DynFlags -> AnalEnv -> Demand -> CoreExpr -> (DmdType, CoreExpr)
+evalDmdAnal :: DynFlags -> AnalEnv -> CoreExpr -> (DmdType, CoreExpr)
+-- See Note [Ensure demand is strict]
+evalDmdAnal dflags env e
+  | (res_ty, e') <- dmdAnal dflags env evalDmd e
+  = (deferType res_ty, e')
+
+simpleDmdAnal :: DynFlags -> AnalEnv -> DmdType -> CoreExpr -> (DmdType, CoreExpr)
+simpleDmdAnal dflags env res_ty e
+  | ae_virgin env -- See Note [Always analyse in virgin pass]
+  , (_discarded_res_ty, e') <- dmdAnal dflags env evalDmd e
+  = (res_ty, e')
+  | otherwise
+  = (res_ty, e)
 
-dmdAnal _ _ Abs  e = (topDmdType, e)
+dmdAnal :: DynFlags -> AnalEnv -> Demand -> CoreExpr -> (DmdType, CoreExpr)
+dmdAnal dflags env dmd e 
+  | isBotDmd dmd  	  = simpleDmdAnal dflags env botDmdType e
+  | isAbsDmd dmd          = simpleDmdAnal dflags env topDmdType e
+  | not (isStrictDmd dmd) = evalDmdAnal   dflags env            e
 
-dmdAnal dflags env dmd e
-  | not (isStrictDmd dmd)
-  = let 
-	(res_ty, e') = dmdAnal dflags env evalDmd e
-    in
-    (deferType res_ty, e')
-	-- It's important not to analyse e with a lazy demand because
-	-- a) When we encounter   case s of (a,b) -> 
-	--	we demand s with U(d1d2)... but if the overall demand is lazy
-	--	that is wrong, and we'd need to reduce the demand on s,
-	--	which is inconvenient
-	-- b) More important, consider
-	--	f (let x = R in x+x), where f is lazy
-	--    We still want to mark x as demanded, because it will be when we
-	--    enter the let.  If we analyse f's arg with a Lazy demand, we'll
-	--    just mark x as Lazy
-	-- c) The application rule wouldn't be right either
-	--    Evaluating (f x) in a L demand does *not* cause
-	--    evaluation of f in a C(L) demand!
-
-
-dmdAnal _ _ _ (Lit lit) = (topDmdType, Lit lit)
-dmdAnal _ _ _ (Type ty) = (topDmdType, Type ty)	-- Doesn't happen, in fact
+dmdAnal _ _ _ (Lit lit)     = (topDmdType, Lit lit)
+dmdAnal _ _ _ (Type ty)     = (topDmdType, Type ty)	-- Doesn't happen, in fact
 dmdAnal _ _ _ (Coercion co) = (topDmdType, Coercion co)
 
 dmdAnal _ env dmd (Var var)
@@ -191,12 +181,20 @@ dmdAnal dflags sigs dmd (App fun (Coercion co))
 -- Lots of the other code is there to make this
 -- beautiful, compositional, application rule :-)
 dmdAnal dflags env dmd (App fun arg)	-- Non-type arguments
-  = let				-- [Type arg handled above]
-	(fun_ty, fun') 	  = dmdAnal dflags env (Call dmd) fun
+  = let	     		                -- [Type arg handled above]
+	(fun_ty, fun') 	  = dmdAnal dflags env (mkCallDmd dmd) fun
 	(arg_ty, arg') 	  = dmdAnal dflags env arg_dmd arg
 	(arg_dmd, res_ty) = splitDmdTy fun_ty
     in
-    (res_ty `bothType` arg_ty, App fun' arg')
+--    pprTrace "dmdAnal:app" (vcat
+--         [ text "dmd =" <+> ppr dmd
+--         , text "expr =" <+> ppr (App fun arg)
+--         , text "fun dmd_ty =" <+> ppr fun_ty
+--         , text "arg dmd =" <+> ppr arg_dmd
+--         , text "arg dmd_ty =" <+> ppr arg_ty
+--         , text "res dmd_ty =" <+> ppr res_ty
+--         , text "overall res dmd_ty =" <+> ppr (res_ty `bothDmdType` arg_ty) ])
+    (res_ty `bothDmdType` arg_ty, App fun' arg')
 
 dmdAnal dflags env dmd (Lam var body)
   | isTyVar var
@@ -205,7 +203,7 @@ dmdAnal dflags env dmd (Lam var body)
     in
     (body_ty, Lam var body')
 
-  | Call body_dmd <- dmd	-- A call demand: good!
+  | Just body_dmd <- peelCallDmd dmd	-- A call demand: good!
   = let	
 	env'		 = extendSigsWithLam env var
 	(body_ty, body') = dmdAnal dflags env' body_dmd body
@@ -221,11 +219,12 @@ dmdAnal dflags env dmd (Lam var body)
     (deferType lam_ty, Lam var' body')
 
 dmdAnal dflags env dmd (Case scrut case_bndr ty [alt@(DataAlt dc, _, _)])
+  -- Only one alternative with a product constructor
   | let tycon = dataConTyCon dc
   , isProductTyCon tycon
   , not (isRecursiveTyCon tycon)
   = let
-	env_alt	      = extendAnalEnv NotTopLevel env case_bndr case_bndr_sig
+	env_alt	              = extendAnalEnv NotTopLevel env case_bndr case_bndr_sig
 	(alt_ty, alt')	      = dmdAnalAlt dflags env_alt dmd alt
 	(alt_ty1, case_bndr') = annotateBndr alt_ty case_bndr
 	(_, bndrs', _)	      = alt'
@@ -249,7 +248,7 @@ dmdAnal dflags env dmd (Case scrut case_bndr ty [alt@(DataAlt dc, _, _)])
 	--	x = (a, absent-error)
 	-- and that'll crash.
 	-- So at one stage I had:
-	--	dead_case_bndr		 = isAbsentDmd (idDemandInfo case_bndr')
+	--	dead_case_bndr		 = isAbsDmd (idDemandInfo case_bndr')
 	--	keepity | dead_case_bndr = Drop
 	--		| otherwise	 = Keep		
 	--
@@ -260,25 +259,29 @@ dmdAnal dflags env dmd (Case scrut case_bndr ty [alt@(DataAlt dc, _, _)])
 	-- The insight is, of course, that a demand on y is a demand on the
 	-- scrutinee, so we need to `both` it with the scrut demand
 
-	alt_dmd 	   = Eval (Prod [idDemandInfo b | b <- bndrs', isId b])
-        scrut_dmd 	   = alt_dmd `both`
+	alt_dmd 	   = mkProdDmd [idDemandInfo b | b <- bndrs', isId b]
+        scrut_dmd 	   = alt_dmd `bothDmd`
 			     idDemandInfo case_bndr'
 
 	(scrut_ty, scrut') = dmdAnal dflags env scrut_dmd scrut
-        res_ty =           alt_ty1 `bothType` scrut_ty
+        res_ty             = alt_ty1 `bothDmdType` scrut_ty
     in
 --    pprTrace "dmdAnal:Case1" (vcat [ text "scrut" <+> ppr scrut
---                                  , text "scrut_ty" <+> ppr scrut_ty
---                                  , text "alt_ty" <+> ppr alt_ty1
---                                  , text "res_ty" <+> ppr res_ty ]) $
+--                                   , text "dmd" <+> ppr dmd
+--                                   , text "alt_dmd" <+> ppr alt_dmd
+--                                   , text "case_bndr_dmd" <+> ppr (idDemandInfo case_bndr')
+--                                   , text "scrut_dmd" <+> ppr scrut_dmd
+--                                   , text "scrut_ty" <+> ppr scrut_ty
+--                                   , text "alt_ty" <+> ppr alt_ty1
+--                                   , text "res_ty" <+> ppr res_ty ]) $
     (res_ty, Case scrut' case_bndr' ty [alt'])
 
 dmdAnal dflags env dmd (Case scrut case_bndr ty alts)
-  = let
+  = let      -- Case expression with multiple alternatives
 	(alt_tys, alts')        = mapAndUnzip (dmdAnalAlt dflags env dmd) alts
 	(scrut_ty, scrut')      = dmdAnal dflags env evalDmd scrut
-	(alt_ty, case_bndr')	= annotateBndr (foldr lubType botDmdType alt_tys) case_bndr
-        res_ty                  = alt_ty `bothType` scrut_ty
+	(alt_ty, case_bndr')	= annotateBndr (foldr lubDmdType botDmdType alt_tys) case_bndr
+        res_ty                  = alt_ty `bothDmdType` scrut_ty
     in
 --    pprTrace "dmdAnal:Case2" (vcat [ text "scrut" <+> ppr scrut
 --                                   , text "scrut_ty" <+> ppr scrut_ty
@@ -331,7 +334,7 @@ dmdAnalAlt dflags env dmd (con,bndrs,rhs)
 	(rhs_ty, rhs')   = dmdAnal dflags env dmd rhs
         rhs_ty'          = addDataConPatDmds con bndrs rhs_ty
 	(alt_ty, bndrs') = annotateBndrs rhs_ty' bndrs
-	final_alt_ty | io_hack_reqd = alt_ty `lubType` topDmdType
+	final_alt_ty | io_hack_reqd = alt_ty `lubDmdType` topDmdType
 		     | otherwise    = alt_ty
 
 	-- There's a hack here for I/O operations.  Consider
@@ -363,45 +366,13 @@ addDataConPatDmds (LitAlt _) _ dmd_ty = dmd_ty
 addDataConPatDmds (DataAlt con) bndrs dmd_ty
   = foldr add dmd_ty str_bndrs 
   where
-    add bndr dmd_ty = addVarDmd dmd_ty bndr seqDmd
+    add bndr dmd_ty = addVarDmd dmd_ty bndr absDmd
     str_bndrs = [ b | (b,s) <- zipEqual "addDataConPatBndrs"
                                    (filter isId bndrs)
                                    (dataConRepStrictness con)
                     , isMarkedStrict s ]
-\end{code}
-
-Note [Add demands for strict constructors]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this program (due to Roman):
-
-    data X a = X !a
-
-    foo :: X Int -> Int -> Int
-    foo (X a) n = go 0
-     where
-       go i | i < n     = a + go (i+1)
-            | otherwise = 0
-
-We want the worker for 'foo' too look like this:
-
-    $wfoo :: Int# -> Int# -> Int#
-
-with the first argument unboxed, so that it is not eval'd each time
-around the loop (which would otherwise happen, since 'foo' is not
-strict in 'a'.  It is sound for the wrapper to pass an unboxed arg
-because X is strict, so its argument must be evaluated.  And if we
-*don't* pass an unboxed argument, we can't even repair it by adding a
-`seq` thus:
-
-    foo (X a) n = a `seq` go 0
-
-because the seq is discarded (very early) since X is strict!
-
-There is the usual danger of reboxing, which as usual we ignore. But 
-if X is monomorphic, and has an UNPACK pragma, then this optimisation
-is even more important.  We don't want the wrapper to rebox an unboxed
-argument, and pass an Int to $wfoo!
 
+\end{code}
 
 %************************************************************************
 %*									*
@@ -418,67 +389,21 @@ dmdTransform :: AnalEnv		-- The strictness environment
 	-- this function plus demand on its free variables
 
 dmdTransform env var dmd
+  | isDataConWorkId var		                 -- Data constructor
+  = dmdTransformDataConSig 
+       (idArity var) (idStrictness var) dmd
 
------- 	DATA CONSTRUCTOR
-  | isDataConWorkId var		-- Data constructor
-  = let 
-	StrictSig dmd_ty    = idStrictness var	-- It must have a strictness sig
-	DmdType _ _ con_res = dmd_ty
-	arity		    = idArity var
-    in
-    if arity == call_depth then		-- Saturated, so unleash the demand
-	let 
-		-- Important!  If we Keep the constructor application, then
-		-- we need the demands the constructor places (always lazy)
-		-- If not, we don't need to.  For example:
-		--	f p@(x,y) = (p,y)	-- S(AL)
-		--	g a b     = f (a,b)
-		-- It's vital that we don't calculate Absent for a!
-	   dmd_ds = case res_dmd of
-			Box (Eval ds) -> mapDmds box ds
-			Eval ds	      -> ds
-			_	      -> Poly Top
-
-		-- ds can be empty, when we are just seq'ing the thing
-		-- If so we must make up a suitable bunch of demands
-	   arg_ds = case dmd_ds of
-		      Poly d  -> replicate arity d
-		      Prod ds -> ASSERT( ds `lengthIs` arity ) ds
-
-	in
-	mkDmdType emptyDmdEnv arg_ds con_res
-		-- Must remember whether it's a product, hence con_res, not TopRes
-    else
-	topDmdType
-
------- 	IMPORTED FUNCTION
-  | isGlobalId var,		-- Imported function
-    let StrictSig dmd_ty = idStrictness var
-  = -- pprTrace "strict-sig" (ppr var $$ ppr dmd_ty) $
-    if dmdTypeDepth dmd_ty <= call_depth then	-- Saturated, so unleash the demand
-	dmd_ty
-    else
-	topDmdType
-
------- 	LOCAL LET/REC BOUND THING
-  | Just (StrictSig dmd_ty, top_lvl) <- lookupSigEnv env var
-  = let
-	fn_ty | dmdTypeDepth dmd_ty <= call_depth = dmd_ty 
-	      | otherwise   		          = deferType dmd_ty
-	-- NB: it's important to use deferType, and not just return topDmdType
-	-- Consider	let { f x y = p + x } in f 1
-	-- The application isn't saturated, but we must nevertheless propagate 
-	--	a lazy demand for p!  
-    in
-    if isTopLevel top_lvl then fn_ty	-- Don't record top level things
+  | isGlobalId var	                         -- Imported function
+  = dmdTransformSig (idStrictness var) dmd
+
+  | Just (sig, top_lvl) <- lookupSigEnv env var  -- Local letrec bound thing
+  , let fn_ty = dmdTransformSig sig dmd
+  = if isTopLevel top_lvl           
+    then fn_ty	-- Don't record top level things
     else addVarDmd fn_ty var dmd
 
------- 	LOCAL NON-LET/REC BOUND THING
-  | otherwise	 		-- Default case
+  | otherwise	 		                 -- Local non-letrec-bound thing
   = unitVarDmd var dmd
-
-  where
-    (call_depth, res_dmd) = splitCallDmd dmd
 \end{code}
 
 %************************************************************************
@@ -488,6 +413,8 @@ dmdTransform env var dmd
 %************************************************************************
 
 \begin{code}
+
+-- Recursive bindings
 dmdFix :: DynFlags
        -> TopLevelFlag
        -> AnalEnv 		-- Does not include bindings for this binding
@@ -545,19 +472,19 @@ dmdFix dflags top_lvl env orig_pairs
           = ((sigs', lazy_fv'), pair')
           where
 	    (sigs', lazy_fv1, pair') = dmdAnalRhs dflags top_lvl Recursive (updSigEnv env sigs) (id,rhs)
-	    lazy_fv'		     = plusVarEnv_C both lazy_fv lazy_fv1
+	    lazy_fv'		     = plusVarEnv_C bothDmd lazy_fv lazy_fv1
 	   
     same_sig sigs sigs' var = lookup sigs var == lookup sigs' var
     lookup sigs var = case lookupVarEnv sigs var of
 			Just (sig,_) -> sig
                         Nothing      -> pprPanic "dmdFix" (ppr var)
 
+-- Non-recursive bindings
 dmdAnalRhs :: DynFlags -> TopLevelFlag -> RecFlag
 	-> AnalEnv -> (Id, CoreExpr)
 	-> (SigEnv,  DmdEnv, (Id, CoreExpr))
 -- Process the RHS of the binding, add the strictness signature
 -- to the Id, and augment the environment with the signature as well.
-
 dmdAnalRhs dflags top_lvl rec_flag env (id, rhs)
  = (sigs', lazy_fv, (id', rhs'))
  where
@@ -565,13 +492,13 @@ dmdAnalRhs dflags top_lvl rec_flag env (id, rhs)
 				    -- The simplifier was run just beforehand
   (rhs_dmd_ty, rhs') = dmdAnal dflags env (vanillaCall arity) rhs
   (lazy_fv, sig_ty)  = WARN( arity /= dmdTypeDepth rhs_dmd_ty && not (exprIsTrivial rhs), ppr id )
-				-- The RHS can be eta-reduced to just a variable, 
-				-- in which case we should not complain. 
-		       mkSigTy dflags top_lvl rec_flag id rhs rhs_dmd_ty
+                       -- The RHS can be eta-reduced to just a variable, 
+                       -- in which case we should not complain. 
+		       mkSigTy top_lvl rec_flag env id rhs rhs_dmd_ty
   id'		     = id `setIdStrictness` sig_ty
   sigs'		     = extendSigEnv top_lvl (sigEnv env) id sig_ty
-\end{code}
 
+\end{code}
 
 %************************************************************************
 %*									*
@@ -580,26 +507,134 @@ dmdAnalRhs dflags top_lvl rec_flag env (id, rhs)
 %************************************************************************
 
 \begin{code}
-mkTopSigTy :: DynFlags -> CoreExpr -> DmdType -> StrictSig
-	-- Take a DmdType and turn it into a StrictSig
-	-- NB: not used for never-inline things; hence False
-mkTopSigTy dflags rhs dmd_ty = snd (mk_sig_ty dflags False False rhs dmd_ty)
-
-mkSigTy :: DynFlags -> TopLevelFlag -> RecFlag -> Id -> CoreExpr -> DmdType -> (DmdEnv, StrictSig)
-mkSigTy dflags top_lvl rec_flag id rhs dmd_ty 
-  = mk_sig_ty dflags never_inline thunk_cpr_ok rhs dmd_ty
+unitVarDmd :: Var -> Demand -> DmdType
+unitVarDmd var dmd 
+  = DmdType (unitVarEnv var dmd) [] topRes
+
+addVarDmd :: DmdType -> Var -> Demand -> DmdType
+addVarDmd (DmdType fv ds res) var dmd
+  = DmdType (extendVarEnv_C bothDmd fv var dmd) ds res
+
+addLazyFVs :: DmdType -> DmdEnv -> DmdType
+addLazyFVs (DmdType fv ds res) lazy_fvs
+  = DmdType both_fv1 ds res
   where
-    never_inline = isNeverActive (idInlineActivation id)
-    maybe_id_dmd = idDemandInfo_maybe id
-	-- Is Nothing the first time round
+    both_fv = plusVarEnv_C bothDmd fv lazy_fvs
+    both_fv1 = modifyEnv (isBotRes res) (`bothDmd` botDmd) lazy_fvs fv both_fv
+	-- This modifyEnv is vital.  Consider
+	--	let f = \x -> (x,y)
+	--	in  error (f 3)
+	-- Here, y is treated as a lazy-fv of f, but we must `bothDmd` that L
+	-- demand with the bottom coming up from 'error'
+	-- 
+	-- I got a loop in the fixpointer without this, due to an interaction
+	-- with the lazy_fv filtering in mkSigTy.  Roughly, it was
+	--	letrec f n x 
+	--	    = letrec g y = x `fatbar` 
+	--			   letrec h z = z + ...g...
+	--			   in h (f (n-1) x)
+	-- 	in ...
+	-- In the initial iteration for f, f=Bot
+	-- Suppose h is found to be strict in z, but the occurrence of g in its RHS
+	-- is lazy.  Now consider the fixpoint iteration for g, esp the demands it
+	-- places on its free variables.  Suppose it places none.  Then the
+	-- 	x `fatbar` ...call to h...
+	-- will give a x->V demand for x.  That turns into a L demand for x,
+	-- which floats out of the defn for h.  Without the modifyEnv, that
+	-- L demand doesn't get both'd with the Bot coming up from the inner
+	-- call to f.  So we just get an L demand for x for g.
+	--
+	-- A better way to say this is that the lazy-fv filtering should give the
+	-- same answer as putting the lazy fv demands in the function's type.
+
+
+removeFV :: DmdEnv -> Var -> DmdResult -> (DmdEnv, Demand)
+removeFV fv id res = -- pprTrace "rfv" (ppr id <+> ppr dmd $$ ppr fv)
+                     (fv', dmd)
+		where
+		  fv' = fv `delVarEnv` id
+		  dmd = lookupVarEnv fv id `orElse` deflt
+                  -- See note [Default demand for variables]
+	 	  deflt | isBotRes res = botDmd
+		        | otherwise    = absDmd
+\end{code}
+
+Note [Default demand for variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+If the variable is not mentioned in the environment of a demand type,
+its demand is taken to be a result demand of the type: either L or the
+bottom. Both are safe from the semantical pont of view, however, for
+the safe result we also have absent demand set to Abs, which makes it
+possible to safely ignore non-mentioned variables (their joint demand
+is <L,A>).
+
+\begin{code}
+annotateBndr :: DmdType -> Var -> (DmdType, Var)
+-- The returned env has the var deleted
+-- The returned var is annotated with demand info
+-- according to the result demand of the provided demand type
+-- No effect on the argument demands
+annotateBndr dmd_ty@(DmdType fv ds res) var
+  | isTyVar var = (dmd_ty, var)
+  | otherwise   = (DmdType fv' ds res, setIdDemandInfo var dmd)
+  where
+    (fv', dmd) = removeFV fv var res
+
+annotateBndrs :: DmdType -> [Var] -> (DmdType, [Var])
+annotateBndrs = mapAccumR annotateBndr
+
+annotateLamIdBndr :: DynFlags
+                  -> AnalEnv
+                  -> DmdType 	-- Demand type of body
+		  -> Id 	-- Lambda binder
+		  -> (DmdType, 	-- Demand type of lambda
+		      Id)	-- and binder annotated with demand	
+
+annotateLamIdBndr dflags env (DmdType fv ds res) id
+-- For lambdas we add the demand to the argument demands
+-- Only called for Ids
+  = ASSERT( isId id )
+    (final_ty, setIdDemandInfo id dmd)
+  where
+      -- Watch out!  See note [Lambda-bound unfoldings]
+    final_ty = case maybeUnfoldingTemplate (idUnfolding id) of
+                 Nothing  -> main_ty
+                 Just unf -> main_ty `bothDmdType` unf_ty
+                          where
+                             (unf_ty, _) = dmdAnal dflags env dmd unf
+    
+    main_ty = DmdType fv' (dmd:ds) res
+
+    (fv', dmd) = removeFV fv id res
+
+mkSigTy :: TopLevelFlag -> RecFlag -> AnalEnv -> Id -> 
+           CoreExpr -> DmdType -> (DmdEnv, StrictSig)
+mkSigTy top_lvl rec_flag env id rhs (DmdType fv dmds res)
+  = (lazy_fv, mkStrictSig dmd_ty)
+	-- See Note [NOINLINE and strictness]
+  where
+    dmd_ty = mkDmdType strict_fv dmds res'
+
+    -- See Note [Lazy and strict free variables]
+    lazy_fv   = filterUFM (not . isStrictDmd) fv
+    strict_fv = filterUFM isStrictDmd         fv
+
+    ignore_cpr_info = not (exprIsHNF rhs || thunk_cpr_ok)
+    res' = if returnsCPR res && ignore_cpr_info 
+	   then topRes
+           else res 
 
+    -- Is it okay or not to assign CPR 
+    -- (not okay in the first pass)
     thunk_cpr_ok   -- See Note [CPR for thunks]
-	| isTopLevel top_lvl       = False	-- Top level things don't get
-						-- their demandInfo set at all
-	| isRec rec_flag	   = False	-- Ditto recursive things
-	| Just dmd <- maybe_id_dmd = isStrictDmd dmd
-	| otherwise 		   = True	-- Optimistic, first time round
-						-- See notes below
+        | isTopLevel top_lvl       	= False	-- Top level things don't get
+				                -- their demandInfo set at all
+	| isRec rec_flag	   	= False	-- Ditto recursive things
+        | ae_virgin env            	= True  -- Optimistic, first time round
+        -- See Note [Optimistic CPR in the "virgin" case]
+	| isStrictDmd (idDemandInfo id) = True
+	| otherwise 		        = False	
 \end{code}
 
 Note [CPR for thunks]
@@ -663,15 +698,15 @@ have a CPR in it or not.  Simple solution:
 
 NB: strictly_demanded is never true of a top-level Id, or of a recursive Id.
 
-Note [Optimistic in the Nothing case]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Demand info now has a 'Nothing' state, just like strictness info.
-The analysis works from 'dangerous' towards a 'safe' state; so we 
-start with botSig for 'Nothing' strictness infos, and we start with
-"yes, it's demanded" for 'Nothing' in the demand info.  The
-fixpoint iteration will sort it all out.
+Note [Optimistic CPR in the "virgin" case]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+
+Demand and strictness info are initialized by top elements. However,
+this prevents from inferring a CPR property in the first pass of the
+analyser, so we keep an explicit flag ae_virgin in the AnalEnv
+datatype.
 
-We can't start with 'not-demanded' because then consider
+We can't start with 'not-demanded' (i.e., top) because then consider
 	f x = let 
 		  t = ... I# x
 	      in
@@ -680,9 +715,9 @@ We can't start with 'not-demanded' because then consider
 In the first iteration we'd have no demand info for x, so assume
 not-demanded; then we'd get TopRes for f's CPR info.  Next iteration
 we'd see that t was demanded, and so give it the CPR property, but by
-now f has TopRes, so it will stay TopRes.  Instead, with the Nothing
-setting the first time round, we say 'yes t is demanded' the first
-time.
+now f has TopRes, so it will stay TopRes.  Instead, by checking the
+ae_virgin flag at the first time round, we say 'yes t is demanded' the
+first time.
 
 However, this does mean that for non-recursive bindings we must
 iterate twice to be sure of not getting over-optimistic CPR info,
@@ -726,204 +761,40 @@ strictness.  For example, if you have a function implemented by an
 error stub, but which has RULES, you may want it not to be eliminated
 in favour of error!
 
+Note [Lazy and strict free variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-\begin{code}
-mk_sig_ty :: DynFlags -> Bool -> Bool -> CoreExpr
-          -> DmdType -> (DmdEnv, StrictSig)
-mk_sig_ty dflags _never_inline thunk_cpr_ok rhs (DmdType fv dmds res) 
-  = (lazy_fv, mkStrictSig dmd_ty)
-	-- Re unused never_inline, see Note [NOINLINE and strictness]
-  where
-    dmd_ty = DmdType strict_fv final_dmds res'
-
-    lazy_fv   = filterUFM (not . isStrictDmd) fv
-    strict_fv = filterUFM isStrictDmd         fv
-	-- We put the strict FVs in the DmdType of the Id, so 
-	-- that at its call sites we unleash demands on its strict fvs.
-	-- An example is 'roll' in imaginary/wheel-sieve2
-	-- Something like this:
-	--	roll x = letrec 
-	--		     go y = if ... then roll (x-1) else x+1
-	--		 in 
-	--		 go ms
-	-- We want to see that roll is strict in x, which is because
-	-- go is called.   So we put the DmdEnv for x in go's DmdType.
-	--
-	-- Another example:
-	--	f :: Int -> Int -> Int
-	--	f x y = let t = x+1
-	--	    h z = if z==0 then t else 
-	--		  if z==1 then x+1 else
-	--		  x + h (z-1)
-	--	in
-	--	h y
-	-- Calling h does indeed evaluate x, but we can only see
-	-- that if we unleash a demand on x at the call site for t.
-	--
-	-- Incidentally, here's a place where lambda-lifting h would
-	-- lose the cigar --- we couldn't see the joint strictness in t/x
-	--
-	--	ON THE OTHER HAND
-	-- We don't want to put *all* the fv's from the RHS into the
-	-- DmdType, because that makes fixpointing very slow --- the 
-	-- DmdType gets full of lazy demands that are slow to converge.
-
-    final_dmds = setUnpackStrategy dflags dmds
-	-- Set the unpacking strategy
-	
-    res' = case res of
-		RetCPR | ignore_cpr_info -> TopRes
-		_	 		 -> res
-    ignore_cpr_info = not (exprIsHNF rhs || thunk_cpr_ok)
-\end{code}
+We put the strict FVs in the DmdType of the Id, so 
+that at its call sites we unleash demands on its strict fvs.
+An example is 'roll' in imaginary/wheel-sieve2
+Something like this:
+	roll x = letrec 
+		     go y = if ... then roll (x-1) else x+1
+		 in 
+		 go ms
+We want to see that roll is strict in x, which is because
+go is called.   So we put the DmdEnv for x in go's DmdType.
 
-The unpack strategy determines whether we'll *really* unpack the argument,
-or whether we'll just remember its strictness.  If unpacking would give
-rise to a *lot* of worker args, we may decide not to unpack after all.
+Another example:
 
-\begin{code}
-setUnpackStrategy :: DynFlags -> [Demand] -> [Demand]
-setUnpackStrategy dflags ds
-  = snd (go (maxWorkerArgs dflags - nonAbsentArgs ds) ds)
-  where
-    go :: Int 			-- Max number of args available for sub-components of [Demand]
-       -> [Demand]
-       -> (Int, [Demand])	-- Args remaining after subcomponents of [Demand] are unpacked
-
-    go n (Eval (Prod cs) : ds) 
-	| n' >= 0   = Eval (Prod cs') `cons` go n'' ds
-        | otherwise = Box (Eval (Prod cs)) `cons` go n ds
-	where
-	  (n'',cs') = go n' cs
-	  n' = n + 1 - non_abs_args
-		-- Add one to the budget 'cos we drop the top-level arg
-	  non_abs_args = nonAbsentArgs cs
-		-- Delete # of non-absent args to which we'll now be committed
-				
-    go n (d:ds) = d `cons` go n ds
-    go n []     = (n,[])
-
-    cons d (n,ds) = (n, d:ds)
-
-nonAbsentArgs :: [Demand] -> Int
-nonAbsentArgs []	 = 0
-nonAbsentArgs (Abs : ds) = nonAbsentArgs ds
-nonAbsentArgs (_   : ds) = 1 + nonAbsentArgs ds
-\end{code}
+	f :: Int -> Int -> Int
+	f x y = let t = x+1
+	    h z = if z==0 then t else 
+		  if z==1 then x+1 else
+		  x + h (z-1)
+	in h y
 
+Calling h does indeed evaluate x, but we can only see
+that if we unleash a demand on x at the call site for t.
 
-%************************************************************************
-%*									*
-\subsection{Strictness signatures and types}
-%*									*
-%************************************************************************
+Incidentally, here's a place where lambda-lifting h would
+lose the cigar --- we couldn't see the joint strictness in t/x
 
-\begin{code}
-unitVarDmd :: Var -> Demand -> DmdType
-unitVarDmd var dmd = DmdType (unitVarEnv var dmd) [] TopRes
+	ON THE OTHER HAND
+We don't want to put *all* the fv's from the RHS into the
+DmdType, because that makes fixpointing very slow --- the 
+DmdType gets full of lazy demands that are slow to converge.
 
-addVarDmd :: DmdType -> Var -> Demand -> DmdType
-addVarDmd (DmdType fv ds res) var dmd
-  = DmdType (extendVarEnv_C both fv var dmd) ds res
-
-addLazyFVs :: DmdType -> DmdEnv -> DmdType
-addLazyFVs (DmdType fv ds res) lazy_fvs
-  = DmdType both_fv1 ds res
-  where
-    both_fv = plusVarEnv_C both fv lazy_fvs
-    both_fv1 = modifyEnv (isBotRes res) (`both` Bot) lazy_fvs fv both_fv
-	-- This modifyEnv is vital.  Consider
-	--	let f = \x -> (x,y)
-	--	in  error (f 3)
-	-- Here, y is treated as a lazy-fv of f, but we must `both` that L
-	-- demand with the bottom coming up from 'error'
-	-- 
-	-- I got a loop in the fixpointer without this, due to an interaction
-	-- with the lazy_fv filtering in mkSigTy.  Roughly, it was
-	--	letrec f n x 
-	--	    = letrec g y = x `fatbar` 
-	--			   letrec h z = z + ...g...
-	--			   in h (f (n-1) x)
-	-- 	in ...
-	-- In the initial iteration for f, f=Bot
-	-- Suppose h is found to be strict in z, but the occurrence of g in its RHS
-	-- is lazy.  Now consider the fixpoint iteration for g, esp the demands it
-	-- places on its free variables.  Suppose it places none.  Then the
-	-- 	x `fatbar` ...call to h...
-	-- will give a x->V demand for x.  That turns into a L demand for x,
-	-- which floats out of the defn for h.  Without the modifyEnv, that
-	-- L demand doesn't get both'd with the Bot coming up from the inner
-	-- call to f.  So we just get an L demand for x for g.
-	--
-	-- A better way to say this is that the lazy-fv filtering should give the
-	-- same answer as putting the lazy fv demands in the function's type.
-
-annotateBndr :: DmdType -> Var -> (DmdType, Var)
--- The returned env has the var deleted
--- The returned var is annotated with demand info
--- No effect on the argument demands
-annotateBndr dmd_ty@(DmdType fv ds res) var
-  | isTyVar var = (dmd_ty, var)
-  | otherwise   = (DmdType fv' ds res, setIdDemandInfo var dmd)
-  where
-    (fv', dmd) = removeFV fv var res
-
-annotateBndrs :: DmdType -> [Var] -> (DmdType, [Var])
-annotateBndrs = mapAccumR annotateBndr
-
-annotateLamIdBndr :: DynFlags
-                  -> AnalEnv
-                  -> DmdType 	-- Demand type of body
-		  -> Id 	-- Lambda binder
-		  -> (DmdType, 	-- Demand type of lambda
-		      Id)	-- and binder annotated with demand	
-
-annotateLamIdBndr dflags env (DmdType fv ds res) id
--- For lambdas we add the demand to the argument demands
--- Only called for Ids
-  = ASSERT( isId id )
-    (final_ty, setIdDemandInfo id hacked_dmd)
-  where
-      -- Watch out!  See note [Lambda-bound unfoldings]
-    final_ty = case maybeUnfoldingTemplate (idUnfolding id) of
-                 Nothing  -> main_ty
-                 Just unf -> main_ty `bothType` unf_ty
-                          where
-                             (unf_ty, _) = dmdAnal dflags env dmd unf
-    
-    main_ty = DmdType fv' (hacked_dmd:ds) res
-
-    (fv', dmd) = removeFV fv id res
-    hacked_dmd = argDemand dmd
-	-- This call to argDemand is vital, because otherwise we label
-	-- a lambda binder with demand 'B'.  But in terms of calling
-	-- conventions that's Abs, because we don't pass it.  But
-	-- when we do a w/w split we get
-	--	fw x = (\x y:B -> ...) x (error "oops")
-	-- And then the simplifier things the 'B' is a strict demand
-	-- and evaluates the (error "oops").  Sigh
-
-removeFV :: DmdEnv -> Var -> DmdResult -> (DmdEnv, Demand)
-removeFV fv id res = (fv', zapUnlifted id dmd)
-		where
-		  fv' = fv `delVarEnv` id
-		  dmd = lookupVarEnv fv id `orElse` deflt
-	 	  deflt | isBotRes res = Bot
-		        | otherwise    = Abs
-
-zapUnlifted :: Id -> Demand -> Demand
--- For unlifted-type variables, we are only 
--- interested in Bot/Abs/Box Abs
-zapUnlifted id dmd
-  = case dmd of
-      _ | isCoVarType ty    -> lazyDmd	-- For coercions, ignore str/abs totally
-      Bot                   -> Bot
-      Abs                   -> Abs
-      _ | isUnLiftedType ty -> lazyDmd	-- For unlifted types, ignore strictness
-	| otherwise	    -> dmd
-  where
-    ty = idType id
-\end{code}
 
 Note [Lamba-bound unfoldings]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -995,323 +866,77 @@ nonVirgin sigs = AE { ae_sigs = sigs, ae_virgin = False }
 
 extendSigsWithLam :: AnalEnv -> Id -> AnalEnv
 -- Extend the AnalEnv when we meet a lambda binder
--- If the binder is marked demanded with a product demand, then give it a CPR 
--- signature, because in the likely event that this is a lambda on a fn defn 
--- [we only use this when the lambda is being consumed with a call demand],
--- it'll be w/w'd and so it will be CPR-ish.  E.g.
---	f = \x::(Int,Int).  if ...strict in x... then
---				x
---			    else
---				(a,b)
--- We want f to have the CPR property because x does, by the time f has been w/w'd
---
--- Also note that we only want to do this for something that
--- definitely has product type, else we may get over-optimistic 
--- CPR results (e.g. from \x -> x!).
-
 extendSigsWithLam env id
-  = case idDemandInfo_maybe id of
-	Nothing	             -> extendAnalEnv NotTopLevel env id cprSig
-		-- See Note [Optimistic in the Nothing case]
-	Just (Eval (Prod _)) -> extendAnalEnv NotTopLevel env id cprSig
-	_                    -> env
-\end{code}
-
-Note [Initialising strictness]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Our basic plan is to initialise the strictness of each Id in 
-a recursive group to "bottom", and find a fixpoint from there.
-However, this group A might be inside an *enclosing* recursive
-group B, in which case we'll do the entire fixpoint shebang on A
-for each iteration of B.
-
-To speed things up, we initialise each iteration of B from the result
-of the last one, which is neatly recorded in each binder.  That way we
-make use of earlier iterations of the fixpoint algorithm.  (Cunning
-plan.)  
-
-But on the *first* iteration we want to *ignore* the current strictness
-of the Id, and start from "bottom".  Nowadays the Id can have a current
-strictness, because interface files record strictness for nested bindings.
-To know when we are in the first iteration, we look at the ae_virgin
-field of the AnalEnv.
-
-
-%************************************************************************
-%*									*
-                   Demands
-%*									*
-%************************************************************************
+  | ae_virgin env   -- See Note [Optimistic CPR in the "virgin" case]
+  = extendAnalEnv NotTopLevel env id cprSig
 
-\begin{code}
-splitDmdTy :: DmdType -> (Demand, DmdType)
--- Split off one function argument
--- We already have a suitable demand on all
--- free vars, so no need to add more!
-splitDmdTy (DmdType fv (dmd:dmds) res_ty) = (dmd, DmdType fv dmds res_ty)
-splitDmdTy ty@(DmdType _ [] res_ty)       = (resTypeArgDmd res_ty, ty)
-
-splitCallDmd :: Demand -> (Int, Demand)
-splitCallDmd (Call d) = case splitCallDmd d of
-			  (n, r) -> (n+1, r)
-splitCallDmd d	      = (0, d)
-
-vanillaCall :: Arity -> Demand
-vanillaCall 0 = evalDmd
-vanillaCall n = Call (vanillaCall (n-1))
-
-deferType :: DmdType -> DmdType
-deferType (DmdType fv _ _) = DmdType (deferEnv fv) [] TopRes
-	-- Notice that we throw away info about both arguments and results
-	-- For example,   f = let ... in \x -> x
-	-- We don't want to get a stricness type V->T for f.
-
-deferEnv :: DmdEnv -> DmdEnv
-deferEnv fv = mapVarEnv defer fv
-
-
-----------------
-argDemand :: Demand -> Demand
--- The 'Defer' demands are just Lazy at function boundaries
--- Ugly!  Ask John how to improve it.
-argDemand Top 	    = lazyDmd
-argDemand (Defer _) = lazyDmd
-argDemand (Eval ds) = Eval (mapDmds argDemand ds)
-argDemand (Box Bot) = evalDmd
-argDemand (Box d)   = box (argDemand d)
-argDemand Bot	    = Abs	-- Don't pass args that are consumed (only) by bottom
-argDemand d	    = d
-\end{code}
+  | isStrictDmd dmd_info  -- Might be bottom, first time round
+  , Just {} <- deepSplitProductType_maybe $ idType id
+  = extendAnalEnv NotTopLevel env id cprSig
+       -- See Note [Initial CPR for strict binders]
 
-\begin{code}
--------------------------
-lubType :: DmdType -> DmdType -> DmdType
--- Consider (if x then y else []) with demand V
--- Then the first branch gives {y->V} and the second
---  *implicitly* has {y->A}.  So we must put {y->(V `lub` A)}
--- in the result env.
-lubType (DmdType fv1 ds1 r1) (DmdType fv2 ds2 r2)
-  = DmdType lub_fv2 (lub_ds ds1 ds2) (r1 `lubRes` r2)
-  where
-    lub_fv  = plusVarEnv_C lub fv1 fv2
-    lub_fv1 = modifyEnv (not (isBotRes r1)) absLub fv2 fv1 lub_fv
-    lub_fv2 = modifyEnv (not (isBotRes r2)) absLub fv1 fv2 lub_fv1
-	-- lub is the identity for Bot
-
-	-- Extend the shorter argument list to match the longer
-    lub_ds (d1:ds1) (d2:ds2) = lub d1 d2 : lub_ds ds1 ds2
-    lub_ds []	    []	     = []
-    lub_ds ds1	    []	     = map (`lub` resTypeArgDmd r2) ds1
-    lub_ds []	    ds2	     = map (resTypeArgDmd r1 `lub`) ds2
-
------------------------------------
-bothType :: DmdType -> DmdType -> DmdType
--- (t1 `bothType` t2) takes the argument/result info from t1,
--- using t2 just for its free-var info
--- NB: Don't forget about r2!  It might be BotRes, which is
---     a bottom demand on all the in-scope variables.
--- Peter: can this be done more neatly?
-bothType (DmdType fv1 ds1 r1) (DmdType fv2 _ r2)
-  = DmdType both_fv2 ds1 (r1 `bothRes` r2)
+  | otherwise = env
   where
-    both_fv  = plusVarEnv_C both fv1 fv2
-    both_fv1 = modifyEnv (isBotRes r1) (`both` Bot) fv2 fv1 both_fv
-    both_fv2 = modifyEnv (isBotRes r2) (`both` Bot) fv1 fv2 both_fv1
-	-- both is the identity for Abs
+    dmd_info = idDemandInfo id
 \end{code}
 
+Note [Initial CPR for strict binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-\begin{code}
-lubRes :: DmdResult -> DmdResult -> DmdResult
-lubRes BotRes r      = r
-lubRes r      BotRes = r
-lubRes RetCPR RetCPR = RetCPR
-lubRes _      _      = TopRes
-
-bothRes :: DmdResult -> DmdResult -> DmdResult
--- If either diverges, the whole thing does
--- Otherwise take CPR info from the first
-bothRes _  BotRes = BotRes
-bothRes r1 _      = r1
-\end{code}
+CPR is initialized for a lambda binder in an optimistic manner, i.e,
+if the binder is used strictly and at least some of its components as
+a product are used, which is checked by the value of the absence
+demand.
 
-\begin{code}
-modifyEnv :: Bool			-- No-op if False
-	  -> (Demand -> Demand)		-- The zapper
-	  -> DmdEnv -> DmdEnv		-- Env1 and Env2
-	  -> DmdEnv -> DmdEnv		-- Transform this env
-	-- Zap anything in Env1 but not in Env2
-	-- Assume: dom(env) includes dom(Env1) and dom(Env2)
-
-modifyEnv need_to_modify zapper env1 env2 env
-  | need_to_modify = foldr zap env (varEnvKeys (env1 `minusUFM` env2))
-  | otherwise	   = env
-  where
-    zap uniq env = addToUFM_Directly env uniq (zapper current_val)
-		 where
-		   current_val = expectJust "modifyEnv" (lookupUFM_Directly env uniq)
-\end{code}
+If the binder is marked demanded with a strict demand, then give it a
+CPR signature, because in the likely event that this is a lambda on a
+fn defn [we only use this when the lambda is being consumed with a
+call demand], it'll be w/w'd and so it will be CPR-ish.  E.g.
 
+	f = \x::(Int,Int).  if ...strict in x... then
+				x
+			    else
+				(a,b)
+We want f to have the CPR property because x does, by the time f has been w/w'd
 
-%************************************************************************
-%*									*
-\subsection{LUB and BOTH}
-%*									*
-%************************************************************************
+Also note that we only want to do this for something that definitely
+has product type, else we may get over-optimistic CPR results
+(e.g. from \x -> x!).
 
-\begin{code}
-lub :: Demand -> Demand -> Demand
-
-lub Bot  	d2 = d2
-lub Abs  	d2 = absLub d2
-lub Top 	_  = Top
-lub (Defer ds1) d2 = defer (Eval ds1 `lub` d2)
-
-lub (Call d1)   (Call d2)    = Call (d1 `lub` d2)
-lub d1@(Call _) (Box d2)     = d1 `lub` d2	-- Just strip the box
-lub    (Call _) d2@(Eval _)  = d2		-- Presumably seq or vanilla eval
-lub d1@(Call _) d2	     = d2 `lub` d1	-- Bot, Abs, Top
-
--- For the Eval case, we use these approximation rules
--- Box Bot	 <= Eval (Box Bot ...)
--- Box Top	 <= Defer (Box Bot ...)
--- Box (Eval ds) <= Eval (map Box ds)
-lub (Eval ds1)  (Eval ds2)  	  = Eval (ds1 `lubs` ds2)
-lub (Eval ds1)  (Box Bot)   	  = Eval (mapDmds (`lub` Box Bot) ds1)
-lub (Eval ds1)  (Box (Eval ds2)) = Eval (ds1 `lubs` mapDmds box ds2)
-lub (Eval ds1)  (Box Abs)        = deferEval (mapDmds (`lub` Box Bot) ds1)
-lub d1@(Eval _) d2	          = d2 `lub` d1	-- Bot,Abs,Top,Call,Defer
-
-lub (Box d1)   (Box d2) = box (d1 `lub` d2)
-lub d1@(Box _)  d2	= d2 `lub` d1
-
-lubs :: Demands -> Demands -> Demands
-lubs ds1 ds2 = zipWithDmds lub ds1 ds2
-
----------------------
-box :: Demand -> Demand
--- box is the smart constructor for Box
--- It computes <B,bot> & d
--- INVARIANT: (Box d) => d = Bot, Abs, Eval
--- Seems to be no point in allowing (Box (Call d))
-box (Call d)  = Call d	-- The odd man out.  Why?
-box (Box d)   = Box d
-box (Defer _) = lazyDmd
-box Top       = lazyDmd	-- Box Abs and Box Top
-box Abs       = lazyDmd	-- are the same <B,L>
-box d 	      = Box d	-- Bot, Eval
-
----------------
-defer :: Demand -> Demand
-
--- defer is the smart constructor for Defer
--- The idea is that (Defer ds) = <U(ds), L>
---
--- It specifies what happens at a lazy function argument
--- or a lambda; the L* operator
--- Set the strictness part to L, but leave
--- the boxity side unaffected
--- It also ensures that Defer (Eval [LLLL]) = L
-
-defer Bot	 = Abs
-defer Abs	 = Abs
-defer Top	 = Top
-defer (Call _)	 = lazyDmd	-- Approximation here?
-defer (Box _)	 = lazyDmd
-defer (Defer ds) = Defer ds
-defer (Eval ds)  = deferEval ds
-
-deferEval :: Demands -> Demand
--- deferEval ds = defer (Eval ds)
-deferEval ds | allTop ds = Top
-	     | otherwise  = Defer ds
-
----------------------
-absLub :: Demand -> Demand
--- Computes (Abs `lub` d)
--- For the Bot case consider
---	f x y = if ... then x else error x
---   Then for y we get Abs `lub` Bot, and we really
---   want Abs overall
-absLub Bot  	  = Abs
-absLub Abs  	  = Abs
-absLub Top 	  = Top
-absLub (Call _)   = Top
-absLub (Box _)    = Top
-absLub (Eval ds)  = Defer (absLubs ds)	-- Or (Defer ds)?
-absLub (Defer ds) = Defer (absLubs ds)	-- Or (Defer ds)?
-
-absLubs :: Demands -> Demands
-absLubs = mapDmds absLub
-
----------------
-both :: Demand -> Demand -> Demand
-
-both Abs d2 = d2
-
--- Note [Bottom demands]
-both Bot Bot 	    = Bot
-both Bot Abs 	    = Bot 
-both Bot (Eval ds)  = Eval (mapDmds (`both` Bot) ds)
-both Bot (Defer ds) = Eval (mapDmds (`both` Bot) ds)
-both Bot _          = errDmd
-
-both Top Bot 	    = errDmd
-both Top Abs 	    = Top
-both Top Top 	    = Top
-both Top (Box d)    = Box d
-both Top (Call d)   = Call d
-both Top (Eval ds)  = Eval (mapDmds (`both` Top) ds)
-both Top (Defer ds) 	-- = defer (Top `both` Eval ds)
-			-- = defer (Eval (mapDmds (`both` Top) ds))
-		     = deferEval (mapDmds (`both` Top) ds)
-
-
-both (Box d1) 	(Box d2)    = box (d1 `both` d2)
-both (Box d1) 	d2@(Call _) = box (d1 `both` d2)
-both (Box d1) 	d2@(Eval _) = box (d1 `both` d2)
-both (Box d1) 	(Defer _)   = Box d1
-both d1@(Box _) d2	    = d2 `both` d1
-
-both (Call d1) 	 (Call d2)   = Call (d1 `both` d2)
-both (Call d1) 	 (Eval _)    = Call d1	-- Could do better for (Poly Bot)?
-both (Call d1) 	 (Defer _)   = Call d1	-- Ditto
-both d1@(Call _) d2	     = d2 `both` d1
-
-both (Eval ds1)  (Eval  ds2) = Eval (ds1 `boths` ds2)
-both (Eval ds1)  (Defer ds2) = Eval (ds1 `boths` mapDmds defer ds2)
-both d1@(Eval _) d2	     = d2 `both` d1
-
-both (Defer ds1)  (Defer ds2) = deferEval (ds1 `boths` ds2)
-both d1@(Defer _) d2	      = d2 `both` d1
- 
-boths :: Demands -> Demands -> Demands
-boths ds1 ds2 = zipWithDmds both ds1 ds2
-\end{code}
 
-Note [Bottom demands]
-~~~~~~~~~~~~~~~~~~~~~
-Consider
-	f x = error x
-From 'error' itself we get demand Bot on x
-From the arg demand on x we get 
-	x :-> evalDmd = Box (Eval (Poly Abs))
-So we get  Bot `both` Box (Eval (Poly Abs))
-	    = Seq Keep (Poly Bot)
-
-Consider also
-	f x = if ... then error (fst x) else fst x
-Then we get (Eval (Box Bot, Bot) `lub` Eval (SA))
-	= Eval (SA)
-which is what we want.
-
-Consider also
-  f x = error [fst x]
-Then we get 
-     x :-> Bot `both` Defer [SA]
-and we want the Bot demand to cancel out the Defer
-so that we get Eval [SA].  Otherwise we'd have the odd
-situation that
-  f x = error (fst x)      -- Strictness U(SA)b
-  g x = error ('y':fst x)  -- Strictness Tb
+Note [Initialising strictness]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See section 9.2 (Finding fixpoints) of the paper.
+
+Our basic plan is to initialise the strictness of each Id in a
+recursive group to "bottom", and find a fixpoint from there.  However,
+this group B might be inside an *enclosing* recursiveb group A, in
+which case we'll do the entire fixpoint shebang on for each iteration
+of A. This can be illustrated by the following example:
+
+Example:
+
+  f [] = []
+  f (x:xs) = let g []     = f xs
+                 g (y:ys) = y+1 : g ys
+              in g (h x)
+
+At each iteration of the fixpoint for f, the analyser has to find a
+fixpoint for the enclosed function g. In the meantime, the demand
+values for g at each iteration for f are *greater* than those we
+encountered in the previous iteration for f. Therefore, we can begin
+the fixpoint for g not with the bottom value but rather with the
+result of the previous analysis. I.e., when beginning the fixpoint
+process for g, we can start from the demand signature computed for g
+previously and attached to the binding occurrence of g.
+
+To speed things up, we initialise each iteration of A (the enclosing
+one) from the result of the last one, which is neatly recorded in each
+binder.  That way we make use of earlier iterations of the fixpoint
+algorithm. (Cunning plan.)
 
+But on the *first* iteration we want to *ignore* the current strictness
+of the Id, and start from "bottom".  Nowadays the Id can have a current
+strictness, because interface files record strictness for nested bindings.
+To know when we are in the first iteration, we look at the ae_virgin
+field of the AnalEnv.
diff --git a/compiler/stranal/WorkWrap.lhs b/compiler/stranal/WorkWrap.lhs
index 5be63a9bc7..e697dfe1ff 100644
--- a/compiler/stranal/WorkWrap.lhs
+++ b/compiler/stranal/WorkWrap.lhs
@@ -21,12 +21,11 @@ import Var
 import Id
 import Type		( Type )
 import IdInfo
-import Demand
 import UniqSupply
 import BasicTypes
 import DynFlags
 import VarEnv		( isEmptyVarEnv )
-import Maybes		( orElse )
+import Demand
 import WwLib
 import Util
 import Outputable
@@ -258,7 +257,7 @@ tryWW dflags is_rec fn_id rhs
 	-- Furthermore, don't even expose strictness info
   = return [ (fn_id, rhs) ]
 
-  | is_thunk && worthSplittingThunk maybe_fn_dmd res_info
+  | is_thunk && worthSplittingThunk fn_dmd res_info
   	-- See Note [Thunk splitting]
   = ASSERT2( isNonRec is_rec, ppr new_fn_id )	-- The thunk must be non-recursive
     checkSize dflags new_fn_id rhs $ 
@@ -273,12 +272,12 @@ tryWW dflags is_rec fn_id rhs
 
   where
     fn_info   	 = idInfo fn_id
-    maybe_fn_dmd = demandInfo fn_info
+    fn_dmd       = demandInfo fn_info
     inline_act   = inlinePragmaActivation (inlinePragInfo fn_info)
 
 	-- In practice it always will have a strictness 
 	-- signature, even if it's a uninformative one
-    strict_sig  = strictnessInfo fn_info `orElse` topSig
+    strict_sig  = strictnessInfo fn_info
     StrictSig (DmdType env wrap_dmds res_info) = strict_sig
 
 	-- new_fn_id has the DmdEnv zapped.  
@@ -376,8 +375,8 @@ splitFun dflags fn_id fn_info wrap_dmds res_info rhs
     		    -- The arity is set by the simplifier using exprEtaExpandArity
 		    -- So it may be more than the number of top-level-visible lambdas
 
-    work_res_info | isBotRes res_info = BotRes	-- Cpr stuff done by wrapper
-		  | otherwise	      = TopRes
+    work_res_info | isBotRes res_info = botRes	-- Cpr stuff done by wrapper
+		  | otherwise	      = topRes
 
     one_shots = get_one_shots rhs
 
@@ -451,51 +450,6 @@ splitThunk dflags fn_id rhs = do
 
 %************************************************************************
 %*									*
-\subsection{Functions over Demands}
-%*									*
-%************************************************************************
-
-\begin{code}
-worthSplittingFun :: [Demand] -> DmdResult -> Bool
-		-- True <=> the wrapper would not be an identity function
-worthSplittingFun ds res
-  = any worth_it ds || returnsCPR res
-	-- worthSplitting returns False for an empty list of demands,
-	-- and hence do_strict_ww is False if arity is zero and there is no CPR
-  -- See Note [Worker-wrapper for bottoming functions]
-  where
-    worth_it Abs	      = True	-- Absent arg
-    worth_it (Eval (Prod _)) = True	-- Product arg to evaluate
-    worth_it _    	      = False
-
-worthSplittingThunk :: Maybe Demand	-- Demand on the thunk
-		    -> DmdResult	-- CPR info for the thunk
-		    -> Bool
-worthSplittingThunk maybe_dmd res
-  = worth_it maybe_dmd || returnsCPR res
-  where
-	-- Split if the thing is unpacked
-    worth_it (Just (Eval (Prod ds))) = not (all isAbsent ds)
-    worth_it _    	   	     = False
-\end{code}
-
-Note [Worker-wrapper for bottoming functions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We used not to split if the result is bottom.
-[Justification:  there's no efficiency to be gained.]
-
-But it's sometimes bad not to make a wrapper.  Consider
-	fw = \x# -> let x = I# x# in case e of
-					p1 -> error_fn x
-					p2 -> error_fn x
-					p3 -> the real stuff
-The re-boxing code won't go away unless error_fn gets a wrapper too.
-[We don't do reboxing now, but in general it's better to pass an
-unboxed thing to f, and have it reboxed in the error cases....]
-
-
-%************************************************************************
-%*									*
 \subsection{The worker wrapper core}
 %*									*
 %************************************************************************
diff --git a/compiler/stranal/WwLib.lhs b/compiler/stranal/WwLib.lhs
index 8aaa13171c..1cbebf8c23 100644
--- a/compiler/stranal/WwLib.lhs
+++ b/compiler/stranal/WwLib.lhs
@@ -11,7 +11,7 @@
 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
 -- for details
 
-module WwLib ( mkWwBodies, mkWWstr, mkWorkerArgs ) where
+module WwLib ( mkWwBodies, mkWWstr, mkWorkerArgs, deepSplitProductType_maybe ) where
 
 #include "HsVersions.h"
 
@@ -23,7 +23,7 @@ import Id		( Id, idType, mkSysLocal, idDemandInfo, setIdDemandInfo,
 			)
 import IdInfo		( vanillaIdInfo )
 import DataCon
-import Demand		( Demand(..), DmdResult(..), Demands(..) ) 
+import Demand        
 import MkCore		( mkRuntimeErrorApp, aBSENT_ERROR_ID )
 import MkId		( realWorldPrimId, voidArgId
                         , wrapNewTypeBody, unwrapNewTypeBody )
@@ -36,7 +36,7 @@ import Literal		( absentLiteralOf )
 import TyCon
 import UniqSupply
 import Unique
-import Util		( zipWithEqual )
+import Util
 import Outputable
 import DynFlags
 import FastString
@@ -133,13 +133,14 @@ mkWwBodies :: DynFlags
 
 mkWwBodies dflags fun_ty demands res_info one_shots
   = do	{ let arg_info = demands `zip` (one_shots ++ repeat False)
+              all_one_shots = all snd arg_info
 	; (wrap_args, wrap_fn_args, work_fn_args, res_ty) <- mkWWargs emptyTvSubst fun_ty arg_info
 	; (work_args, wrap_fn_str,  work_fn_str) <- mkWWstr dflags wrap_args
 
         -- Do CPR w/w.  See Note [Always do CPR w/w]
 	; (wrap_fn_cpr, work_fn_cpr,  cpr_res_ty) <- mkWWcpr res_ty res_info
 
-	; let (work_lam_args, work_call_args) = mkWorkerArgs work_args cpr_res_ty
+	; let (work_lam_args, work_call_args) = mkWorkerArgs work_args all_one_shots cpr_res_ty
 	; return ([idDemandInfo v | v <- work_call_args, isId v],
                   wrap_fn_args . wrap_fn_cpr . wrap_fn_str . applyToVars work_call_args . Var,
                   mkLams work_lam_args. work_fn_str . work_fn_cpr . work_fn_args) }
@@ -184,16 +185,39 @@ We use the state-token type which generates no code.
 
 \begin{code}
 mkWorkerArgs :: [Var]
+             -> Bool    -- Whether all arguments are one-shot
 	     -> Type	-- Type of body
 	     -> ([Var],	-- Lambda bound args
 		 [Var])	-- Args at call site
-mkWorkerArgs args res_ty
+mkWorkerArgs args all_one_shot res_ty
     | any isId args || not (isUnLiftedType res_ty)
     = (args, args)
     | otherwise	
-    = (args ++ [voidArgId], args ++ [realWorldPrimId])
+    = (args ++ [newArg], args ++ [realWorldPrimId])
+    where
+      -- see Note [All One-Shot Arguments of a Worker]
+      newArg = if all_one_shot 
+               then setOneShotLambda voidArgId
+               else voidArgId     
 \end{code}
 
+Note [All One-Shot Arguments of a Worker]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Sometimes, derived joint-points are just lambda-lifted thunks, whose
+only argument is of the unit type and is never used. This might
+interfere with the absence analysis, basing on which results these
+never-used arguments are eliminated in the worker. The additional
+argument `all_one_shot` of `mkWorkerArgs` is to prevent this.
+
+An example for this phenomenon is a `treejoin` program from the
+`nofib` suite, which features the following joint points:
+
+$j_s1l1 =
+  \ _ ->
+     case GHC.Prim.<=# 56320 y_aOy of _ {
+        GHC.Types.False -> $j_s1kP GHC.Prim.realWorld#;
+        GHC.Types.True ->  ... }
 
 %************************************************************************
 %*									*
@@ -342,6 +366,24 @@ mkWWstr dflags (arg : args) = do
     (args2, wrap_fn2, work_fn2) <- mkWWstr dflags args
     return (args1 ++ args2, wrap_fn1 . wrap_fn2, work_fn1 . work_fn2)
 
+\end{code}
+
+Note [Unpacking arguments with product and polymorphic demands]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The argument is unpacked in a case if it has a product type and has a
+strict and used demand put on it. I.e., arguments, with demands such
+as the following ones:
+
+<S,U(U, L)>
+<S(L,S),U>
+
+will be unpacked. Moreover, for arguments whose demand is <S,U> or
+<S,H>, we take an advantage of the polymorphic nature of S and U and
+replicate the enclosed demand correspondingly (see definition of
+replicateDmd).
+
+
+\begin{code}
 ----------------------
 -- mkWWstr_one wrap_arg = (work_args, wrap_fn, work_fn)
 --   *  wrap_fn assumes wrap_arg is in scope,
@@ -353,39 +395,19 @@ mkWWstr_one dflags arg
   | isTyVar arg
   = return ([arg],  nop_fn, nop_fn)
 
-  | otherwise
-  = case idDemandInfo arg of
-
-	-- Absent case.  We can't always handle absence for arbitrary
-        -- unlifted types, so we need to choose just the cases we can
-	-- (that's what mk_absent_let does)
-      Abs | Just work_fn <- mk_absent_let dflags arg
-          -> return ([], nop_fn, work_fn)
-
-	-- Unpack case
-      Eval (Prod cs)
-	| Just (_arg_tycon, _tycon_arg_tys, data_con, inst_con_arg_tys) 
-		<- deepSplitProductType_maybe (idType arg)
-	-> do uniqs <- getUniquesM
-	      let
-	        unpk_args      = zipWith mk_ww_local uniqs inst_con_arg_tys
-	        unpk_args_w_ds = zipWithEqual "mkWWstr" set_worker_arg_info unpk_args cs
-	        unbox_fn       = mkUnpackCase (sanitiseCaseBndr arg) (Var arg) unpk_args data_con
-	        rebox_fn       = Let (NonRec arg con_app) 
-	        con_app        = mkProductBox unpk_args (idType arg)
-	      (worker_args, wrap_fn, work_fn) <- mkWWstr dflags unpk_args_w_ds
-	      return (worker_args, unbox_fn . wrap_fn, work_fn . rebox_fn) 
-	  		   -- Don't pass the arg, rebox instead
-
-	-- `seq` demand; evaluate in wrapper in the hope
-	-- of dropping seqs in the worker
-      Eval (Poly Abs)
-	-> let
-		arg_w_unf = arg `setIdUnfolding` evaldUnfolding
-		-- Tell the worker arg that it's sure to be evaluated
-		-- so that internal seqs can be dropped
-	   in
-	   return ([arg_w_unf], mk_seq_case arg, nop_fn)
+  | isAbsDmd dmd
+  , Just work_fn <- mk_absent_let dflags arg
+     -- Absent case.  We can't always handle absence for arbitrary
+     -- unlifted types, so we need to choose just the cases we can
+     --- (that's what mk_absent_let does)
+  = return ([], nop_fn, work_fn)
+      
+  | isSeqDmd dmd  -- `seq` demand; evaluate in wrapper in the hope
+                  -- of dropping seqs in the worker
+  = let arg_w_unf = arg `setIdUnfolding` evaldUnfolding
+	  -- Tell the worker arg that it's sure to be evaluated
+          -- so that internal seqs can be dropped
+    in return ([arg_w_unf], mk_seq_case arg, nop_fn)
 	  	-- Pass the arg, anyway, even if it is in theory discarded
 		-- Consider
 		--	f x y = x `seq` y
@@ -398,11 +420,28 @@ mkWWstr_one dflags arg
 		-- we end up evaluating the absent thunk.
 		-- But the Evald flag is pretty weird, and I worry that it might disappear
 		-- during simplification, so for now I've just nuked this whole case
+
+  	-- Unpack case, 
+        -- see note [Unpacking arguments with product and polymorphic demands]
+  | isStrictDmd dmd
+  , Just (_arg_tycon, _tycon_arg_tys, data_con, inst_con_arg_tys) 
+             <- deepSplitProductType_maybe (idType arg)
+  =  do { uniqs <- getUniquesM
+	; let   cs             = splitProdDmd (length inst_con_arg_tys) dmd
+	        unpk_args      = zipWith mk_ww_local uniqs inst_con_arg_tys
+	        unpk_args_w_ds = zipWithEqual "mkWWstr" set_worker_arg_info unpk_args cs
+	        unbox_fn       = mkUnpackCase (sanitiseCaseBndr arg) (Var arg) unpk_args data_con
+	        rebox_fn       = Let (NonRec arg con_app) 
+	        con_app        = mkProductBox unpk_args (idType arg)
+	 ; (worker_args, wrap_fn, work_fn) <- mkWWstr dflags unpk_args_w_ds
+	 ; return (worker_args, unbox_fn . wrap_fn, work_fn . rebox_fn) }
+	  		   -- Don't pass the arg, rebox instead
 			
-	-- Other cases
-      _other_demand -> return ([arg], nop_fn, nop_fn)
+  | otherwise	-- Other cases
+  = return ([arg], nop_fn, nop_fn)
 
   where
+    dmd = idDemandInfo arg
 	-- If the wrapper argument is a one-shot lambda, then
 	-- so should (all) the corresponding worker arguments be
 	-- This bites when we do w/w on a case join point
@@ -416,8 +455,6 @@ nop_fn :: CoreExpr -> CoreExpr
 nop_fn body = body
 \end{code}
 
-
-
 \begin{code}
 mkUnpackCase ::  Id -> CoreExpr -> [Id] -> DataCon -> CoreExpr -> CoreExpr
 -- (mkUnpackCase x e args Con body)
@@ -496,7 +533,10 @@ mkWWcpr :: Type                              -- function body type
                    CoreExpr -> CoreExpr,	     -- New worker
 		   Type)			-- Type of worker's body 
 
-mkWWcpr body_ty RetCPR
+mkWWcpr body_ty res
+    | not (returnsCPR res) -- No CPR info
+    = return (id, id, body_ty)
+
     | not (isClosedAlgType body_ty)
     = WARN( True, 
             text "mkWWcpr: non-algebraic or open body type" <+> ppr body_ty )
@@ -537,9 +577,6 @@ mkWWcpr body_ty RetCPR
       n_con_args  = length con_arg_tys
       con_arg_ty1 = head con_arg_tys
 
-mkWWcpr body_ty _other		-- No CPR info
-    = return (id, id, body_ty)
-
 -- If the original function looked like
 --	f = \ x -> _scc_ "foo" E
 --
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 9ab83c133d..e34b139bfb 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -26,6 +26,7 @@ import TcEvidence
 import TcHsType
 import TcPat
 import TcMType
+import FunDeps( growThetaTyVars )
 import TyCon
 import TcType
 import TysPrim
diff --git a/compiler/typecheck/TcForeign.lhs b/compiler/typecheck/TcForeign.lhs
index b1aef2fd77..630157ee79 100644
--- a/compiler/typecheck/TcForeign.lhs
+++ b/compiler/typecheck/TcForeign.lhs
@@ -90,8 +90,7 @@ normaliseFfiType' env ty0 = go [] ty0
         = do { rdr_env <- getGlobalRdrEnv 
              ; case checkNewtypeFFI rdr_env rec_nts tc of
                  Nothing  -> children_only
-                 Just gre -> do { let nt_co = mkUnbranchedAxInstCo (newTyConCo tc) tys
-                                ; (co', ty', gres) <- go rec_nts' nt_rhs
+                 Just gre -> do { (co', ty', gres) <- go rec_nts' nt_rhs
                                 ; return (mkTransCo nt_co co', ty', gre `consBag` gres) } }
 
         | isFamilyTyCon tc              -- Expand open tycons
@@ -108,7 +107,9 @@ normaliseFfiType' env ty0 = go [] ty0
             = do xs <- mapM (go rec_nts) tys
                  let (cos, tys', gres) = unzip3 xs
                  return (mkTyConAppCo tc cos, mkTyConApp tc tys', unionManyBags gres)
+          nt_co  = mkUnbranchedAxInstCo (newTyConCo tc) tys
           nt_rhs = newTyConInstRhs tc tys
+
           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
                    | otherwise           = rec_nts
 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 35e5ff8fa5..8af1e4c57e 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -48,9 +48,6 @@ module TcMType (
   tcSkolDFunType, tcSuperSkolTyVars,
 
   --------------------------------
-  growThetaTyVars, quantifyPred, 
-
-  --------------------------------
   -- Zonking
   zonkTcPredType, 
   skolemiseSigTv, skolemiseUnboundMetaTyVar,
@@ -942,58 +939,6 @@ zonkTcTyVar tv
 zonkTcKind :: TcKind -> TcM TcKind
 zonkTcKind k = zonkTcType k
 \end{code}
-			
-Note [Inheriting implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this:
-
-	f x = (x::Int) + ?y
-
-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:
-
-	f :: Int -> Int
-
-(so we get ?y from the context of f's definition), or
-
-	f :: (?y::Int) => Int -> Int
-
-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.
-
-BOTTOM LINE: when *inferring types* you *must* quantify 
-over implicit parameters. See the predicate isFreeWhenInferring.
-
-\begin{code}
-quantifyPred :: TyVarSet      -- Quantifying over these
-	     -> PredType -> Bool	    -- True <=> quantify over this wanted
-quantifyPred qtvs pred
-  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
-  | otherwise	  = tyVarsOfType pred `intersectsVarSet` qtvs
-
-growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
--- See Note [Growing the tau-tvs using constraints]
-growThetaTyVars theta tvs
-  | null theta = tvs
-  | otherwise  = fixVarSet mk_next tvs
-  where
-    mk_next tvs = foldr grow_one tvs theta
-    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
-
-growPredTyVars :: TcPredType
-               -> TyVarSet	-- The set to extend
-	       -> TyVarSet	-- TyVars of the predicate if it intersects the set, 
-growPredTyVars pred tvs 
-   | isIPPred pred                   = pred_tvs   -- Always quantify over implicit parameers
-   | pred_tvs `intersectsVarSet` tvs = pred_tvs
-   | otherwise                       = emptyVarSet
-  where
-    pred_tvs = tyVarsOfType pred
-\end{code}
     
 
 
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index eadcffe2f1..2da70231f2 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -1529,6 +1529,7 @@ tcRnExpr :: HscEnv
          -> InteractiveContext
          -> LHsExpr RdrName
          -> IO (Messages, Maybe Type)
+-- Type checks the expression and returns its most general type
 tcRnExpr hsc_env ictxt rdr_expr
   = initTcPrintErrors hsc_env iNTERACTIVE $
     setInteractiveContext hsc_env ictxt $ do {
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 2dc06c2cef..8e5ec4111c 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -7,7 +7,8 @@
 -- for details
 
 module TcSimplify( 
-       simplifyInfer, simplifyAmbiguityCheck,
+       simplifyInfer, quantifyPred,
+       simplifyAmbiguityCheck,
        simplifyDefault, 
        simplifyRule, simplifyTop, simplifyInteractive,
        solveWantedsTcM
@@ -23,6 +24,7 @@ import TcType
 import TcSMonad as TcS
 import TcInteract 
 import Inst
+import FunDeps  ( growThetaTyVars )
 import Type     ( classifyPredType, PredTree(..), getClassPredTys_maybe )
 import Class    ( Class )
 import Var
@@ -342,8 +344,39 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
 
        ; return ( qtvs_to_return, minimal_bound_ev_vars
                 , mr_bites,  TcEvBinds ev_binds_var) } }
+
+quantifyPred :: TyVarSet           -- Quantifying over these
+	     -> PredType -> Bool   -- True <=> quantify over this wanted
+quantifyPred qtvs pred
+  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
+  | otherwise	  = tyVarsOfType pred `intersectsVarSet` qtvs
 \end{code}
 
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+
+	f x = (x::Int) + ?y
+
+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:
+
+	f :: Int -> Int
+
+(so we get ?y from the context of f's definition), or
+
+	f :: (?y::Int) => Int -> Int
+
+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.
+
+BOTTOM LINE: when *inferring types* you *must* quantify 
+over implicit parameters. See the predicate isFreeWhenInferring.
+
 Note [Quantification with errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we find that the RHS of the definition has some absolutely-insoluble
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index abc6bae4ef..24ca540dbc 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -35,6 +35,7 @@ import TcEnv
 import TcValidity
 import TcHsSyn
 import TcBinds( tcRecSelBinds )
+import FunDeps( growThetaTyVars )
 import TcTyDecls
 import TcClassDcl
 import TcHsType
diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
index 83f31af3af..abaf7dde71 100644
--- a/compiler/types/Coercion.lhs
+++ b/compiler/types/Coercion.lhs
@@ -142,10 +142,13 @@ data Coercion
 
   -- These are special
   | CoVarCo CoVar
-  | AxiomInstCo (CoAxiom Branched) Int [Coercion]
-     -- The coercion arguments always *precisely* saturate arity of CoAxiom.
-     -- See [Coercion axioms applied to coercions]
+  | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
      -- See also [CoAxiom index]
+     -- The coercion arguments always *precisely* saturate 
+     -- arity of (that branch of) the CoAxiom.  If there are
+     -- any left over, we use AppCo.  See 
+     -- See [Coercion axioms applied to coercions]
+
   | UnsafeCo Type Type
   | SymCo Coercion
   | TransCo Coercion Coercion
@@ -1162,12 +1165,11 @@ coercionKind co = go co
     go (CoVarCo cv)         = toPair $ coVarKind cv
     go (AxiomInstCo ax ind cos)
       | CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
-      , (cos1, cos2) <- splitAtList tvs cos
-      , Pair tys1 tys2 <- sequenceA (map go cos1)
-      = mkAppTys 
-        <$> Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
-                 (substTyWith tvs tys2 rhs)
-        <*> sequenceA (map go cos2)
+      , Pair tys1 tys2 <- sequenceA (map go cos)
+      = ASSERT( cos `equalLength` tvs )  -- Invariant of AxiomInstCo: cos should 
+                                         -- exactly saturate the axiom branch
+        Pair (substTyWith tvs tys1 (mkTyConApp (coAxiomTyCon ax) lhs))
+             (substTyWith tvs tys2 rhs)
     go (UnsafeCo ty1 ty2)   = Pair ty1 ty2
     go (SymCo co)           = swap $ go co
     go (TransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)
diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs
index b64d9148a0..617cfa0b3a 100644
--- a/compiler/types/FamInstEnv.lhs
+++ b/compiler/types/FamInstEnv.lhs
@@ -918,7 +918,7 @@ topNormaliseType env ty
         | isNewTyCon tc         -- Expand newtypes
         = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
           then Nothing
-          else let nt_co = mkUnbranchedAxInstCo (newTyConCo tc) tys
+          else let 
                in add_co nt_co rec_nts' nt_rhs
 
         | isFamilyTyCon tc              -- Expand open tycons
@@ -930,7 +930,8 @@ topNormaliseType env ty
         , not (isReflCo co)
         = add_co co rec_nts ty
         where
-          nt_rhs = newTyConInstRhs tc tys
+          nt_co  = mkUnbranchedAxInstCo (newTyConCo tc) tys
+          nt_rhs = newTyConInstRhs      tc              tys
           rec_nts' | isRecursiveTyCon tc = tc:rec_nts
                    | otherwise           = rec_nts
 
diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs
index fe8781b1f8..8ad91ceab0 100644
--- a/compiler/types/FunDeps.lhs
+++ b/compiler/types/FunDeps.lhs
@@ -18,9 +18,9 @@ It's better to read it as: "if we know these, then we're going to know these"
 module FunDeps (
         FDEq (..),
  	Equation(..), pprEquation,
-	oclose, improveFromInstEnv, improveFromAnother,
+	improveFromInstEnv, improveFromAnother,
 	checkInstCoverage, checkInstLiberalCoverage, checkFunDeps,
-	pprFundeps
+	growThetaTyVars, pprFundeps
     ) where
 
 #include "HsVersions.h"
@@ -51,8 +51,8 @@ import Data.Maybe	( isJust )
   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
-		using all conceivable links from C.
+  growThetaTyVars(C,vs)	 The result of extend the set of tyvars vs
+                         using all conceivable links from C.
 
 		E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
 		Then grow(vs,C) = {a,b,c}
@@ -61,11 +61,11 @@ import Data.Maybe	( isJust )
 		That is, simplfication can only shrink the result of grow.
 
 Notice that
-   oclose is conservative 	v `elem` oclose(vs,C)
-          one way:     		 => v is definitely fixed by vs
+   oclose is conservative 		 v `elem` oclose(vs,C)
+          one way:     			  => v is definitely fixed by vs
 
-   grow is conservative		if v might be fixed by vs 
-          the other way:	=> v `elem` grow(vs,C)
+   growThetaTyVars is conservative	 if v might be fixed by vs 
+          the other way:	         => v `elem` grow(vs,C)
 
 ----------------------------------------------------------
 (oclose preds tvs) closes the set of type variables tvs, 
@@ -76,94 +76,16 @@ then
 	oclose [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
 because if we know x and y then that fixes z.
 
-oclose is used (only) when generalising a type T; see extensive
-notes in TcSimplify.
-
-Note [Important subtlety in oclose]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (oclose (C Int t) {}), where class C a b | a->b
-Then, since a->b, 't' is fully determined by Int, and the
-uniform thing is to return {t}.
-
-However, consider
-	class D a b c | b->c
-	f x = e	  -- 'e' generates constraint (D s Int t)
-		  -- \x.e has type s->s
-Then, if (oclose (D s Int t) {}) = {t}, we'll make the function
-monomorphic in 't', thus
-	f :: forall s. D s Int t => s -> s
-
-But if this function is never called, 't' will never be instantiated;
-the functional dependencies that fix 't' may well be instance decls in
-some importing module.  But the top-level defaulting of unconstrained
-type variables will fix t=GHC.Prim.Any, and that's simply a bug.
-
-Conclusion: oclose only returns a type variable as "fixed" if it 
-depends on at least one type variable in the input fixed_tvs.
-
-Remember, it's always sound for oclose to return a smaller set.
-An interesting example is tcfail093, where we get this inferred type:
-    class C a b | a->b
-    dup :: forall h. (Call (IO Int) h) => () -> Int -> h
-This is perhaps a bit silly, because 'h' is fixed by the (IO Int);
-previously GHC rejected this saying 'no instance for Call (IO Int) h'.
-But it's right on the borderline. If there was an extra, otherwise
-uninvolved type variable, like 's' in the type of 'f' above, then
-we must accept the function.  So, for now anyway, we accept 'dup' too.
+We also use equality predicates in the predicates; if we have an
+assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
+also know `t2` and the other way.
+  eg    oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
+
+oclose is used (only) when checking functional dependencies
 
 \begin{code}
 oclose :: [PredType] -> TyVarSet -> TyVarSet
 oclose preds fixed_tvs
-  | null tv_fds 	    = fixed_tvs	   -- Fast escape hatch for common case
-  | isEmptyVarSet fixed_tvs = emptyVarSet  -- Note [Important subtlety in oclose]
-  | otherwise 		    = loop fixed_tvs
-  where
-    loop fixed_tvs
-	| new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
-	| otherwise		  	      = loop new_fixed_tvs
-	where
-	  new_fixed_tvs = foldl extend fixed_tvs tv_fds
-
-    extend fixed_tvs (ls,rs) 
-	| not (isEmptyVarSet ls)	-- Note [Important subtlety in oclose]
-	, ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
-	| otherwise		   = fixed_tvs
-
-    tv_fds  :: [(TyVarSet,TyVarSet)]
-	-- In our example, tv_fds will be [ ({x,y}, {z}), ({x,p},{q}) ]
-	-- Meaning "knowing x,y fixes z, knowing x,p fixes q"
-    tv_fds  = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
-	      | (cls, tys) <- concatMap classesOfPredTy preds,  -- Ignore implicit params
-		let (cls_tvs, cls_fds) = classTvsFds cls,
-		fd <- cls_fds,
-		let (xs,ys) = instFD fd cls_tvs tys
-	      ]
-     
-    classesOfPredTy :: PredType -> [(Class, [Type])]
-    classesOfPredTy pred
-       = case classifyPredType pred of
-            ClassPred cls tys -> [(cls, tys)]
-            TuplePred ts      -> concatMap classesOfPredTy ts
-            _                 -> []
-
--- An alternative implementation of `oclose`. Differences:
---  1. The empty set of variables is allowed to determine stuff,
---  2. We also use equality predicates as FDs.
---
--- I (Iavor) believe that this is the correct implementation of oclose.
--- For 1: the above argument about `t` being monomorphic seems incorrect.
---    The correct behavior is to quantify over `t`, even though we know that
---    it may be instantiated to at most one type.  The point is that we might
---    only find out what that type is later, at the call site to the function.
---    In general, we should be quantifying all variables that are (i) not in
---    mentioned in the environment, and (ii) not FD-determined by something in
---    the environment.
--- For 2: This is just a nicity, but it makes things a bit more general:
---    if we have an assumption `t1 ~ t2`, then we use the fact that if we know
---    `t1` we also know `t2` and the other way.
-
-oclose1 :: [PredType] -> TyVarSet -> TyVarSet
-oclose1 preds fixed_tvs
   | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
   | otherwise   = loop fixed_tvs
   where
@@ -178,22 +100,51 @@ oclose1 preds fixed_tvs
 
     tv_fds  :: [(TyVarSet,TyVarSet)]
     tv_fds  = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
-              | (xs, ys) <- concatMap deterimned preds
+              | (xs, ys) <- concatMap determined preds
               ]
 
-    deterimned :: PredType -> [([Type],[Type])]
-    deterimned pred
+    determined :: PredType -> [([Type],[Type])]
+    determined pred
        = case classifyPredType pred of
             ClassPred cls tys ->
                do let (cls_tvs, cls_fds) = classTvsFds cls
                   fd <- cls_fds
                   return (instFD fd cls_tvs tys)
             EqPred t1 t2      -> [([t1],[t2]), ([t2],[t1])]
-            TuplePred ts      -> concatMap deterimned ts
+            TuplePred ts      -> concatMap determined ts
             _                 -> []
 
 \end{code}
 
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growThetaTyVars insts tvs) is the result of extending the set 
+    of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then growThetaTyVars preds tvs = {a,b,c}
+
+\begin{code}
+growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
+-- See Note [Growing the tau-tvs using constraints]
+growThetaTyVars theta tvs
+  | null theta = tvs
+  | otherwise  = fixVarSet mk_next tvs
+  where
+    mk_next tvs = foldr grow_one tvs theta
+    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
+
+growPredTyVars :: PredType
+               -> TyVarSet	-- The set to extend
+	       -> TyVarSet	-- TyVars of the predicate if it intersects the set, 
+growPredTyVars pred tvs 
+   | isIPPred pred                   = pred_tvs   -- Always quantify over implicit parameers
+   | pred_tvs `intersectsVarSet` tvs = pred_tvs
+   | otherwise                       = emptyVarSet
+  where
+    pred_tvs = tyVarsOfType pred
+\end{code}
+
     
 %************************************************************************
 %*									*
@@ -533,7 +484,7 @@ checkInstLiberalCoverage clas theta inst_taus
   = all fundep_ok fds
   where
     (tyvars, fds) = classTvsFds clas
-    fundep_ok fd = tyVarsOfTypes rs `subVarSet` oclose1 theta (tyVarsOfTypes ls)
+    fundep_ok fd = tyVarsOfTypes rs `subVarSet` oclose theta (tyVarsOfTypes ls)
                     where (ls,rs) = instFD fd tyvars inst_taus
 \end{code}
 
diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index b16e1aae5f..d01291610e 100644
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -10,7 +10,7 @@
 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
 -- for details
 
-module OptCoercion ( optCoercion ) where 
+module OptCoercion ( optCoercion, checkAxInstCo ) where 
 
 #include "HsVersions.h"
 
@@ -28,6 +28,8 @@ import Pair
 import Maybes( allMaybes )
 import FastString
 import Util
+import Unify
+import InstEnv
 \end{code}
 
 %************************************************************************
@@ -288,21 +290,37 @@ opt_trans_rule is co1 co2
 -- Push transitivity inside axioms
 opt_trans_rule is co1 co2
 
-  -- TrPushAxR/TrPushSymAxR
+  -- TrPushSymAxR
   | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
   , Just cos2 <- matchAxiom sym con ind co2
-  = fireTransRule "TrPushAxR" co1 co2 $
-    if sym 
-    then SymCo $ AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
-    else         AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , True <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
 
-  -- TrPushAxL/TrPushSymAxL
+  -- TrPushAxR
+  | Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
+  , Just cos2 <- matchAxiom sym con ind co2
+  , False <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushAxR" co1 co2 newAxInst
+
+  -- TrPushSymAxL
+  | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
+  , Just cos1 <- matchAxiom (not sym) con ind co1
+  , True <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
+
+  -- TrPushAxL  
   | Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
   , Just cos1 <- matchAxiom (not sym) con ind co1
-  = fireTransRule "TrPushAxL" co1 co2 $
-    if sym 
-    then SymCo $ AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
-    else         AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , False <- sym
+  , let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
+  , Nothing <- checkAxInstCo newAxInst
+  = fireTransRule "TrPushAxL" co1 co2 newAxInst
 
   -- TrPushAxSym/TrPushSymAx
   | Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
@@ -338,6 +356,54 @@ fireTransRule _rule _co1 _co2 res
   = -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
     Just res
 
+\end{code}
+
+Note [Conflict checking with AxiomInstCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following type family and axiom:
+
+type family Equal (a :: k) (b :: k) :: Bool
+type instance where
+  Equal a a = True
+  Equal a b = False
+--
+Equal :: forall k::BOX. k -> k -> Bool
+axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
+           ; forall k::BOX. forall a::k. forall b::k. Equal k a b ~ False }
+
+We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is 0-based,
+so this is the second branch of the axiom.) The problem is that, on the surface, it
+seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) and that all is
+OK. But, all is not OK: we want to use the first branch of the axiom in this case,
+not the second. The problem is that the parameters of the first branch can unify with
+the supplied coercions, thus meaning that the first branch should be taken. See also
+Note [Instance checking within groups] in types/FamInstEnv.lhs.
+
+\begin{code}
+-- | Check to make sure that an AxInstCo is internally consistent.
+-- Returns the number of the conflicting branch, if it exists
+-- See Note [Conflict checking with AxiomInstCo]
+checkAxInstCo :: Coercion -> Maybe Int
+-- defined here to avoid dependencies in Coercion
+checkAxInstCo (AxiomInstCo ax ind cos)
+  = let branch = coAxiomNthBranch ax ind
+        tvs = coAxBranchTyVars branch
+        tys = map (pFst . coercionKind) cos 
+        subst = zipOpenTvSubst tvs tys
+        lhs' = Type.substTys subst (coAxBranchLHS branch) in
+    check_no_conflict lhs' (ind-1)
+  where
+    check_no_conflict :: [Type] -> Int -> Maybe Int
+    check_no_conflict _ (-1) = Nothing
+    check_no_conflict lhs' j
+      | SurelyApart <- tcApartTys instanceBindFun lhs' lhsj
+      = check_no_conflict lhs' (j-1)
+      | otherwise
+      = Just j
+      where
+        (CoAxBranch { cab_lhs = lhsj }) = coAxiomNthBranch ax j
+checkAxInstCo _ = Nothing
+
 -----------
 wrapSym :: Bool -> Coercion -> Coercion
 wrapSym sym co | sym       = SymCo co
diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
index bc161b6697..86202a3ef5 100644
--- a/compiler/types/TyCon.lhs
+++ b/compiler/types/TyCon.lhs
@@ -57,7 +57,8 @@ module TyCon(
         tyConUnique,
         tyConTyVars,
         tyConCType, tyConCType_maybe,
-        tyConDataCons, tyConDataCons_maybe, tyConSingleDataCon_maybe,
+        tyConDataCons, tyConDataCons_maybe, 
+        tyConSingleDataCon_maybe, tyConSingleAlgDataCon_maybe,
         tyConFamilySize,
         tyConStupidTheta,
         tyConArity,
@@ -1400,6 +1401,13 @@ tyConSingleDataCon_maybe (TupleTyCon {dataCon = c})                            =
 tyConSingleDataCon_maybe (AlgTyCon {algTcRhs = DataTyCon { data_cons = [c] }}) = Just c
 tyConSingleDataCon_maybe (AlgTyCon {algTcRhs = NewTyCon { data_con = c }})     = Just c
 tyConSingleDataCon_maybe _                                                     = Nothing
+
+tyConSingleAlgDataCon_maybe :: TyCon -> Maybe DataCon
+-- Returns (Just con) for single-constructor *algebraic* data types
+-- *not* newtypes
+tyConSingleAlgDataCon_maybe (TupleTyCon {dataCon = c})                            = Just c
+tyConSingleAlgDataCon_maybe (AlgTyCon {algTcRhs = DataTyCon { data_cons = [c] }}) = Just c
+tyConSingleAlgDataCon_maybe _                                                     = Nothing
 \end{code}
 
 \begin{code}
diff --git a/compiler/utils/Platform.hs b/compiler/utils/Platform.hs
index 76c9fa3c3c..090ce41f30 100644
--- a/compiler/utils/Platform.hs
+++ b/compiler/utils/Platform.hs
@@ -69,6 +69,8 @@ data OS
         | OSKFreeBSD
         | OSHaiku
         | OSOsf3
+        | OSQNXNTO
+        | OSAndroid
         deriving (Read, Show, Eq)
 
 -- | ARM Instruction Set Architecture, Extensions and ABI
@@ -110,6 +112,8 @@ osElfTarget OSKFreeBSD  = True
 osElfTarget OSHaiku     = True
 osElfTarget OSOsf3      = False -- I don't know if this is right, but as
                                 -- per comment below it's safe
+osElfTarget OSQNXNTO    = False
+osElfTarget OSAndroid   = True
 osElfTarget OSUnknown   = False
  -- Defaulting to False is safe; it means don't rely on any
  -- ELF-specific functionality.  It is important to have a default for