Haskell Program Coverage
[ghc-hetmet.git] / compiler / simplCore / Simplify.lhs
index b30ed04..b3e6bf7 100644 (file)
@@ -13,7 +13,7 @@ import DynFlags       ( dopt, DynFlag(Opt_D_dump_inlinings),
                        )
 import SimplMonad
 import SimplEnv        
                        )
 import SimplMonad
 import SimplEnv        
-import SimplUtils      ( mkCase, mkLam,
+import SimplUtils      ( mkCase, mkLam, 
                          SimplCont(..), DupFlag(..), LetRhsFlag(..), 
                          mkRhsStop, mkBoringStop,  mkLazyArgStop, pushContArgs,
                          contResultType, countArgs, contIsDupable, contIsRhsOrArg,
                          SimplCont(..), DupFlag(..), LetRhsFlag(..), 
                          mkRhsStop, mkBoringStop,  mkLazyArgStop, pushContArgs,
                          contResultType, countArgs, contIsDupable, contIsRhsOrArg,
@@ -26,17 +26,12 @@ import Id           ( Id, idType, idInfo, idArity, isDataConWorkId,
                          idNewDemandInfo, setIdInfo, 
                          setIdOccInfo, zapLamIdInfo, setOneShotLambda
                        )
                          idNewDemandInfo, setIdInfo, 
                          setIdOccInfo, zapLamIdInfo, setOneShotLambda
                        )
-import MkId            ( eRROR_ID )
-import Literal         ( mkStringLit )
-import IdInfo          ( OccInfo(..), isLoopBreaker,
-                         setArityInfo, zapDemandInfo,
-                         setUnfoldingInfo, 
-                         occInfo
+import IdInfo          ( OccInfo(..), setArityInfo, zapDemandInfo,
+                         setUnfoldingInfo, occInfo
                        )
 import NewDemand       ( isStrictDmd )
                        )
 import NewDemand       ( isStrictDmd )
-import Unify           ( coreRefineTys, dataConCanMatch )
-import DataCon         ( DataCon, dataConTyCon, dataConRepStrictness, isVanillaDataCon,
-                         dataConInstArgTys, dataConTyVars )
+import TcGadt          ( dataConCanMatch )
+import DataCon         ( dataConTyCon, dataConRepStrictness )
 import TyCon           ( tyConArity, isAlgTyCon, isNewTyCon, tyConDataCons_maybe )
 import CoreSyn
 import PprCore         ( pprParendExpr, pprCoreExpr )
 import TyCon           ( tyConArity, isAlgTyCon, isNewTyCon, tyConDataCons_maybe )
 import CoreSyn
 import PprCore         ( pprParendExpr, pprCoreExpr )
@@ -45,24 +40,24 @@ import CoreUtils    ( exprIsDupable, exprIsTrivial, needsCaseBinding,
                          exprIsConApp_maybe, mkPiTypes, findAlt, 
                          exprType, exprIsHNF, findDefault, mergeAlts,
                          exprOkForSpeculation, exprArity, 
                          exprIsConApp_maybe, mkPiTypes, findAlt, 
                          exprType, exprIsHNF, findDefault, mergeAlts,
                          exprOkForSpeculation, exprArity, 
-                         mkCoerce, mkCoerce2, mkSCC, mkInlineMe, applyTypeToArg
+                         mkCoerce, mkSCC, mkInlineMe, applyTypeToArg,
+                          dataConRepInstPat
                        )
 import Rules           ( lookupRule )
 import BasicTypes      ( isMarkedStrict )
 import CostCentre      ( currentCCS )
 import Type            ( TvSubstEnv, isUnLiftedType, seqType, tyConAppArgs, funArgTy,
                        )
 import Rules           ( lookupRule )
 import BasicTypes      ( isMarkedStrict )
 import CostCentre      ( currentCCS )
 import Type            ( TvSubstEnv, isUnLiftedType, seqType, tyConAppArgs, funArgTy,
-                         splitFunTy_maybe, splitFunTy, coreEqType, splitTyConApp_maybe,
-                         isTyVarTy, mkTyVarTys
+                         coreEqType, splitTyConApp_maybe,
+                         isTyVarTy, isFunTy, tcEqType
                        )
                        )
-import Var             ( tyVarKind, mkTyVar )
+import Coercion         ( Coercion, coercionKind,
+                          mkTransCoercion, mkSymCoercion, splitCoercionKind_maybe, decomposeCo  )
 import VarEnv          ( elemVarEnv, emptyVarEnv )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
 import VarEnv          ( elemVarEnv, emptyVarEnv )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
 import BasicTypes      ( TopLevelFlag(..), isTopLevel, 
-                         RecFlag(..), isNonRec
+                         RecFlag(..), isNonRec, isNonRuleLoopBreaker
                        )
                        )
-import Name            ( mkSysTvName )
-import StaticFlags     ( opt_PprStyle_Debug )
 import OrdList
 import List            ( nub )
 import Maybes          ( orElse )
 import OrdList
 import List            ( nub )
 import Maybes          ( orElse )
@@ -375,7 +370,6 @@ completeNonRecX env is_strict old_bndr new_bndr new_rhs thing_inside
   | otherwise
   =    -- Make the arguments atomic if necessary, 
        -- adding suitable bindings
   | otherwise
   =    -- Make the arguments atomic if necessary, 
        -- adding suitable bindings
-    -- pprTrace "completeNonRecX" (ppr new_bndr <+> ppr new_rhs) $
     mkAtomicArgsE env is_strict new_rhs                $ \ env new_rhs ->
     completeLazyBind env NotTopLevel
                     old_bndr new_bndr new_rhs  `thenSmpl` \ (floats, env) ->
     mkAtomicArgsE env is_strict new_rhs                $ \ env new_rhs ->
     completeLazyBind env NotTopLevel
                     old_bndr new_bndr new_rhs  `thenSmpl` \ (floats, env) ->
@@ -494,8 +488,7 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
     else       
 
        -- ANF-ise a constructor or PAP rhs
     else       
 
        -- ANF-ise a constructor or PAP rhs
-    mkAtomicArgs False {- Not strict -} 
-                ok_float_unlifted rhs1                 `thenSmpl` \ (aux_binds, rhs2) ->
+    mkAtomicArgs ok_float_unlifted rhs1                `thenSmpl` \ (aux_binds, rhs2) ->
 
        -- If the result is a PAP, float the floats out, else wrap them
        -- By this time it's already been ANF-ised (if necessary)
 
        -- If the result is a PAP, float the floats out, else wrap them
        -- By this time it's already been ANF-ised (if necessary)
@@ -537,8 +530,8 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                -- we only float if (a) arg' is a WHNF, or (b) it's going to top level
                -- and so there can't be any 'will be demanded' bindings in the floats.
                -- Hence the warning
                -- we only float if (a) arg' is a WHNF, or (b) it's going to top level
                -- and so there can't be any 'will be demanded' bindings in the floats.
                -- Hence the warning
-        ASSERT2( is_top_level || not (any demanded_float (floatBinds floats)), 
-                ppr (filter demanded_float (floatBinds floats)) )
+        WARN( not (is_top_level || not (any demanded_float (floatBinds floats))), 
+             ppr (filter demanded_float (floatBinds floats)) )
 
        tick LetFloatFromLet                    `thenSmpl_` (
        addFloats env1 floats                   $ \ env2 ->
 
        tick LetFloatFromLet                    `thenSmpl_` (
        addFloats env1 floats                   $ \ env2 ->
@@ -603,15 +596,17 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
 
   |  otherwise
   = let
 
   |  otherwise
   = let
-               -- Add arity info
+       --      Arity info
        new_bndr_info = idInfo new_bndr `setArityInfo` exprArity new_rhs
 
        new_bndr_info = idInfo new_bndr `setArityInfo` exprArity new_rhs
 
+       --      Unfolding info
        -- Add the unfolding *only* for non-loop-breakers
        -- Making loop breakers not have an unfolding at all 
        -- means that we can avoid tests in exprIsConApp, for example.
        -- This is important: if exprIsConApp says 'yes' for a recursive
        -- thing, then we can get into an infinite loop
 
        -- Add the unfolding *only* for non-loop-breakers
        -- Making loop breakers not have an unfolding at all 
        -- means that we can avoid tests in exprIsConApp, for example.
        -- This is important: if exprIsConApp says 'yes' for a recursive
        -- thing, then we can get into an infinite loop
 
+       --      Demand info
        -- If the unfolding is a value, the demand info may
        -- go pear-shaped, so we nuke it.  Example:
        --      let x = (a,b) in
        -- If the unfolding is a value, the demand info may
        -- go pear-shaped, so we nuke it.  Example:
        --      let x = (a,b) in
@@ -622,7 +617,7 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
        -- and now x is not demanded (I'm assuming h is lazy)
        -- This really happens.  Similarly
        --      let f = \x -> e in ...f..f...
        -- and now x is not demanded (I'm assuming h is lazy)
        -- This really happens.  Similarly
        --      let f = \x -> e in ...f..f...
-       -- After inling f at some of its call sites the original binding may
+       -- After inlining f at some of its call sites the original binding may
        -- (for example) be no longer strictly demanded.
        -- The solution here is a bit ad hoc...
        info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
        -- (for example) be no longer strictly demanded.
        -- The solution here is a bit ad hoc...
        info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
@@ -637,10 +632,9 @@ completeLazyBind env top_lvl old_bndr new_bndr new_rhs
     final_id                                   `seq`
     -- pprTrace "Binding" (ppr final_id <+> ppr unfolding) $
     returnSmpl (unitFloat env final_id new_rhs, env)
     final_id                                   `seq`
     -- pprTrace "Binding" (ppr final_id <+> ppr unfolding) $
     returnSmpl (unitFloat env final_id new_rhs, env)
-
   where 
     unfolding    = mkUnfolding (isTopLevel top_lvl) new_rhs
   where 
     unfolding    = mkUnfolding (isTopLevel top_lvl) new_rhs
-    loop_breaker = isLoopBreaker occ_info
+    loop_breaker = isNonRuleLoopBreaker occ_info
     old_info     = idInfo old_bndr
     occ_info     = occInfo old_info
 \end{code}    
     old_info     = idInfo old_bndr
     occ_info     = occInfo old_info
 \end{code}    
@@ -715,7 +709,9 @@ simplExprF env (Var v)              cont = simplVar env v cont
 simplExprF env (Lit lit)       cont = rebuild env (Lit lit) cont
 simplExprF env expr@(Lam _ _)   cont = simplLam env expr cont
 simplExprF env (Note note expr) cont = simplNote env note expr cont
 simplExprF env (Lit lit)       cont = rebuild env (Lit lit) cont
 simplExprF env expr@(Lam _ _)   cont = simplLam env expr cont
 simplExprF env (Note note expr) cont = simplNote env note expr cont
-simplExprF env (App fun arg)    cont = simplExprF env fun (ApplyTo NoDup arg (Just env) cont)
+simplExprF env (Cast body co)   cont = simplCast env body co cont
+simplExprF env (App fun arg)    cont = simplExprF env fun 
+                                        (ApplyTo NoDup arg (Just env) cont)
 
 simplExprF env (Type ty) cont
   = ASSERT( contIsRhsOrArg cont )
 
 simplExprF env (Type ty) cont
   = ASSERT( contIsRhsOrArg cont )
@@ -768,6 +764,69 @@ simplType env ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
+simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont -> SimplM FloatsWithExpr
+simplCast env body co cont
+  = let
+       addCoerce co cont 
+         | (s1, k1) <- coercionKind co
+         , s1 `tcEqType` k1 = cont
+       addCoerce co1 (CoerceIt co2 cont)
+         | (s1, k1) <- coercionKind co1
+         , (l1, t1) <- coercionKind co2
+                --     coerce T1 S1 (coerce S1 K1 e)
+               -- ==>
+               --      e,                      if T1=K1
+               --      coerce T1 K1 e,         otherwise
+               --
+               -- For example, in the initial form of a worker
+               -- we may find  (coerce T (coerce S (\x.e))) y
+               -- and we'd like it to simplify to e[y/x] in one round 
+               -- of simplification
+         , s1 `coreEqType` t1  = cont           -- The coerces cancel out  
+         | otherwise           = CoerceIt (mkTransCoercion co1 co2) cont
+    
+       addCoerce co (ApplyTo dup arg arg_se cont)
+         | not (isTypeArg arg)    -- This whole case only works for value args
+                               -- Could upgrade to have equiv thing for type apps too  
+         , Just (s1s2, t1t2) <- splitCoercionKind_maybe co
+         , isFunTy s1s2
+                -- co : s1s2 :=: t1t2
+               --      (coerce (T1->T2) (S1->S2) F) E
+               -- ===> 
+               --      coerce T2 S2 (F (coerce S1 T1 E))
+               --
+               -- t1t2 must be a function type, T1->T2, because it's applied
+               -- to something but s1s2 might conceivably not be
+               --
+               -- When we build the ApplyTo we can't mix the out-types
+               -- with the InExpr in the argument, so we simply substitute
+               -- to make it all consistent.  It's a bit messy.
+               -- But it isn't a common case.
+         = result
+         where
+           -- we split coercion t1->t2 :=: s1->s2 into t1 :=: s1 and 
+           -- t2 :=: s2 with left and right on the curried form: 
+           --    (->) t1 t2 :=: (->) s1 s2
+           [co1, co2] = decomposeCo 2 co
+           new_arg    = mkCoerce (mkSymCoercion co1) arg'
+          arg'       = case arg_se of
+                         Nothing     -> arg
+                         Just arg_se -> substExpr (setInScope arg_se env) arg
+           result     = ApplyTo dup new_arg (Just $ zapSubstEnv env) 
+                               (addCoerce co2 cont)
+       addCoerce co cont = CoerceIt co cont
+    in
+    simplType env co           `thenSmpl` \ co' ->
+    simplExprF env body (addCoerce co' cont)
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+\subsection{Lambdas}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
 simplLam env fun cont
   = go env fun cont
   where
 simplLam env fun cont
   = go env fun cont
   where
@@ -829,56 +888,6 @@ mkLamBndrZapper fun n_args
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-simplNote env (Coerce to from) body cont
-  = let
-       addCoerce s1 k1 cont    -- Drop redundant coerces.  This can happen if a polymoprhic
-                               -- (coerce a b e) is instantiated with a=ty1 b=ty2 and the
-                               -- two are the same. This happens a lot in Happy-generated parsers
-         | s1 `coreEqType` k1 = cont
-
-       addCoerce s1 k1 (CoerceIt t1 cont)
-               --      coerce T1 S1 (coerce S1 K1 e)
-               -- ==>
-               --      e,                      if T1=K1
-               --      coerce T1 K1 e,         otherwise
-               --
-               -- For example, in the initial form of a worker
-               -- we may find  (coerce T (coerce S (\x.e))) y
-               -- and we'd like it to simplify to e[y/x] in one round 
-               -- of simplification
-         | t1 `coreEqType` k1  = cont                  -- The coerces cancel out
-         | otherwise           = CoerceIt t1 cont      -- They don't cancel, but 
-                                                       -- the inner one is redundant
-
-       addCoerce t1t2 s1s2 (ApplyTo dup arg mb_arg_se cont)
-         | not (isTypeArg arg),        -- This whole case only works for value args
-                                       -- Could upgrade to have equiv thing for type apps too  
-           Just (s1, s2) <- splitFunTy_maybe s1s2
-               --      (coerce (T1->T2) (S1->S2) F) E
-               -- ===> 
-               --      coerce T2 S2 (F (coerce S1 T1 E))
-               --
-               -- t1t2 must be a function type, T1->T2, because it's applied to something
-               -- but s1s2 might conceivably not be
-               --
-               -- When we build the ApplyTo we can't mix the out-types
-               -- with the InExpr in the argument, so we simply substitute
-               -- to make it all consistent.  It's a bit messy.
-               -- But it isn't a common case.
-         = let 
-               (t1,t2) = splitFunTy t1t2
-               new_arg = mkCoerce2 s1 t1 arg'
-               arg' = case mb_arg_se of
-                         Nothing -> arg
-                         Just arg_se -> substExpr (setInScope arg_se env) arg
-           in
-           ApplyTo dup new_arg Nothing (addCoerce t2 s2 cont)
-                       
-       addCoerce to' _ cont = CoerceIt to' cont
-    in
-    simplType env to           `thenSmpl` \ to' ->
-    simplType env from         `thenSmpl` \ from' ->
-    simplExprF env body (addCoerce to' from' cont)
 
                
 -- Hack: we only distinguish subsumed cost centre stacks for the purposes of
 
                
 -- Hack: we only distinguish subsumed cost centre stacks for the purposes of
@@ -902,6 +911,14 @@ simplNote env InlineMe e cont
 simplNote env (CoreNote s) e cont
   = simplExpr env e    `thenSmpl` \ e' ->
     rebuild env (Note (CoreNote s) e') cont
 simplNote env (CoreNote s) e cont
   = simplExpr env e    `thenSmpl` \ e' ->
     rebuild env (Note (CoreNote s) e') cont
+
+simplNote env note@(TickBox {}) e cont
+  = simplExpr env e    `thenSmpl` \ e' ->
+    rebuild env (Note note e') cont
+
+simplNote env note@(BinaryTickBox {}) e cont
+  = simplExpr env e    `thenSmpl` \ e' ->
+    rebuild env (Note note e') cont
 \end{code}
 
 
 \end{code}
 
 
@@ -916,7 +933,7 @@ simplVar env var cont
   = case substId env var of
        DoneEx e         -> simplExprF (zapSubstEnv env) e cont
        ContEx tvs ids e -> simplExprF (setSubstEnv env tvs ids) e cont
   = case substId env var of
        DoneEx e         -> simplExprF (zapSubstEnv env) e cont
        ContEx tvs ids e -> simplExprF (setSubstEnv env tvs ids) e cont
-       DoneId var1 occ  -> completeCall (zapSubstEnv env) var1 occ cont
+       DoneId var1      -> completeCall (zapSubstEnv env) var1 cont
                -- Note [zapSubstEnv]
                -- The template is already simplified, so don't re-substitute.
                -- This is VITAL.  Consider
                -- Note [zapSubstEnv]
                -- The template is already simplified, so don't re-substitute.
                -- This is VITAL.  Consider
@@ -930,7 +947,7 @@ simplVar env var cont
 ---------------------------------------------------------
 --     Dealing with a call site
 
 ---------------------------------------------------------
 --     Dealing with a call site
 
-completeCall env var occ_info cont
+completeCall env var cont
   =     -- Simplify the arguments
     getDOptsSmpl                                       `thenSmpl` \ dflags ->
     let
   =     -- Simplify the arguments
     getDOptsSmpl                                       `thenSmpl` \ dflags ->
     let
@@ -995,8 +1012,8 @@ completeCall env var occ_info cont
        interesting_cont = interestingCallContext (notNull args)
                                                  (notNull arg_infos)
                                                  call_cont
        interesting_cont = interestingCallContext (notNull args)
                                                  (notNull arg_infos)
                                                  call_cont
-       active_inline = activeInline env var occ_info
-       maybe_inline  = callSiteInline dflags active_inline occ_info
+       active_inline = activeInline env var
+       maybe_inline  = callSiteInline dflags active_inline
                                       var arg_infos interesting_cont
     in
     case maybe_inline of {
                                       var arg_infos interesting_cont
     in
     case maybe_inline of {
@@ -1005,7 +1022,7 @@ completeCall env var occ_info cont
                (if dopt Opt_D_dump_inlinings dflags then
                   pprTrace "Inlining done" (vcat [
                        text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
                (if dopt Opt_D_dump_inlinings dflags then
                   pprTrace "Inlining done" (vcat [
                        text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
-                       text "Inlined fn: " <+> ppr unfolding,
+                       text "Inlined fn: " $$ nest 2 (ppr unfolding),
                        text "Cont:  " <+> ppr call_cont])
                 else
                        id)             $
                        text "Cont:  " <+> ppr call_cont])
                 else
                        id)             $
@@ -1143,7 +1160,6 @@ N  Y      Non-top-level and non-recursive,        Bind args of lifted type, or
 Y  Y   Non-top-level, non-recursive,           Bind all args
                 and strict (demanded)
        
 Y  Y   Non-top-level, non-recursive,           Bind all args
                 and strict (demanded)
        
-
 For example, given
 
        x = MkC (y div# z)
 For example, given
 
        x = MkC (y div# z)
@@ -1156,13 +1172,44 @@ because the (y div# z) can't float out of the let. But if it was
 a *strict* let, then it would be a good thing to do.  Hence the
 context information.
 
 a *strict* let, then it would be a good thing to do.  Hence the
 context information.
 
+Note [Float coercions]
+~~~~~~~~~~~~~~~~~~~~~~
+When we find the binding
+       x = e `cast` co
+we'd like to transform it to
+       x' = e
+       x = x `cast` co         -- A trivial binding
+There's a chance that e will be a constructor application or function, or something
+like that, so moving the coerion to the usage site may well cancel the coersions
+and lead to further optimisation.  Example:
+
+     data family T a :: *
+     data instance T Int = T Int
+
+     foo :: Int -> Int -> Int
+     foo m n = ...
+        where
+          x = T m
+          go 0 = 0
+          go n = case x of { T m -> go (n-m) }
+               -- This case should optimise
+
 \begin{code}
 mkAtomicArgsE :: SimplEnv 
 \begin{code}
 mkAtomicArgsE :: SimplEnv 
-             -> Bool   -- A strict binding
-             -> OutExpr                                                -- The rhs
+             -> Bool           -- A strict binding
+             -> OutExpr        -- The rhs
              -> (SimplEnv -> OutExpr -> SimplM FloatsWithExpr)
              -> (SimplEnv -> OutExpr -> SimplM FloatsWithExpr)
+                               -- Consumer for the simpler rhs
              -> SimplM FloatsWithExpr
 
              -> SimplM FloatsWithExpr
 
+mkAtomicArgsE env is_strict (Cast rhs co) thing_inside
+  | not (exprIsTrivial rhs)
+       -- Note [Float coersions]
+       -- See also Note [Take care] below
+  = do { id <- newId FSLIT("a") (exprType rhs)
+       ; completeNonRecX env False id id rhs $ \ env ->
+         thing_inside env (Cast (substExpr env (Var id)) co) }
+
 mkAtomicArgsE env is_strict rhs thing_inside
   | (Var fun, args) <- collectArgs rhs,                                -- It's an application
     isDataConWorkId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
 mkAtomicArgsE env is_strict rhs thing_inside
   | (Var fun, args) <- collectArgs rhs,                                -- It's an application
     isDataConWorkId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
@@ -1181,7 +1228,18 @@ mkAtomicArgsE env is_strict rhs thing_inside
        | otherwise
        = do { arg_id <- newId FSLIT("a") arg_ty
             ; completeNonRecX env False {- pessimistic -} arg_id arg_id arg $ \env ->
        | otherwise
        = do { arg_id <- newId FSLIT("a") arg_ty
             ; completeNonRecX env False {- pessimistic -} arg_id arg_id arg $ \env ->
-              go env (App fun (Var arg_id)) args }
+              go env (App fun (substExpr env (Var arg_id))) args }
+               -- Note [Take care]:
+               -- If completeNonRecX was to do a postInlineUnconditionally
+               -- (undoing the effect of introducing the let-binding), we'd find arg_id had
+               -- no binding; hence the substExpr.  This happens if we see
+               --      C (D x `cast` g)
+               -- Then we start by making a variable a1, thus
+               --      let a1 = D x `cast` g in C a1
+               -- But then we deal with the rhs of a1, getting
+               --      let a2 = D x, a1 = a1 `cast` g in C a1
+               -- And now the preInlineUnconditionally kicks in, and we substitute for a1
+       
        where
          arg_ty = exprType arg
          no_float_arg = not is_strict && (isUnLiftedType arg_ty) && not (exprOkForSpeculation arg)
        where
          arg_ty = exprType arg
          no_float_arg = not is_strict && (isUnLiftedType arg_ty) && not (exprOkForSpeculation arg)
@@ -1189,14 +1247,20 @@ mkAtomicArgsE env is_strict rhs thing_inside
 
 -- Old code: consider rewriting to be more like mkAtomicArgsE
 
 
 -- Old code: consider rewriting to be more like mkAtomicArgsE
 
-mkAtomicArgs :: Bool   -- A strict binding
-            -> Bool    -- OK to float unlifted args
+mkAtomicArgs :: Bool   -- OK to float unlifted args
             -> OutExpr
             -> SimplM (OrdList (OutId,OutExpr),  -- The floats (unusually) may include
                        OutExpr)                  -- things that need case-binding,
                                                  -- if the strict-binding flag is on
 
             -> OutExpr
             -> SimplM (OrdList (OutId,OutExpr),  -- The floats (unusually) may include
                        OutExpr)                  -- things that need case-binding,
                                                  -- if the strict-binding flag is on
 
-mkAtomicArgs is_strict ok_float_unlifted rhs
+mkAtomicArgs ok_float_unlifted (Cast rhs co)
+  | not (exprIsTrivial rhs)
+       -- Note [Float coersions]
+  = do { id <- newId FSLIT("a") (exprType rhs)
+       ; (binds, rhs') <- mkAtomicArgs ok_float_unlifted rhs
+       ; return (binds `snocOL` (id, rhs'), Cast (Var id) co) }
+
+mkAtomicArgs ok_float_unlifted rhs
   | (Var fun, args) <- collectArgs rhs,                                -- It's an application
     isDataConWorkId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
   = go fun nilOL [] args       -- Have a go
   | (Var fun, args) <- collectArgs rhs,                                -- It's an application
     isDataConWorkId fun || valArgCount args < idArity fun      -- And it's a constructor or PAP
   = go fun nilOL [] args       -- Have a go
@@ -1218,14 +1282,13 @@ mkAtomicArgs is_strict ok_float_unlifted rhs
 
        | otherwise     -- Don't forget to do it recursively
                        -- E.g.  x = a:b:c:[]
 
        | otherwise     -- Don't forget to do it recursively
                        -- E.g.  x = a:b:c:[]
-       =  mkAtomicArgs is_strict ok_float_unlifted arg `thenSmpl` \ (arg_binds, arg') ->
-          newId FSLIT("a") arg_ty                      `thenSmpl` \ arg_id ->
+       =  mkAtomicArgs ok_float_unlifted arg   `thenSmpl` \ (arg_binds, arg') ->
+          newId FSLIT("a") arg_ty              `thenSmpl` \ arg_id ->
           go fun ((arg_binds `snocOL` (arg_id,arg')) `appOL` binds) 
              (Var arg_id : rev_args) args
        where
          arg_ty        = exprType arg
           go fun ((arg_binds `snocOL` (arg_id,arg')) `appOL` binds) 
              (Var arg_id : rev_args) args
        where
          arg_ty        = exprType arg
-         can_float_arg =  is_strict 
-                       || not (isUnLiftedType arg_ty)
+         can_float_arg =  not (isUnLiftedType arg_ty)
                        || (ok_float_unlifted && exprOkForSpeculation arg)
 
 
                        || (ok_float_unlifted && exprOkForSpeculation arg)
 
 
@@ -1249,7 +1312,7 @@ rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM FloatsWithExpr
 
 rebuild env expr (Stop _ _ _)                = rebuildDone env expr
 rebuild env expr (ArgOf _ _ _ cont_fn)       = cont_fn env expr
 
 rebuild env expr (Stop _ _ _)                = rebuildDone env expr
 rebuild env expr (ArgOf _ _ _ cont_fn)       = cont_fn env expr
-rebuild env expr (CoerceIt to_ty cont)       = rebuild env (mkCoerce to_ty expr) cont
+rebuild env expr (CoerceIt co cont)          = rebuild env (mkCoerce co expr) cont
 rebuild env expr (Select _ bndr alts se cont) = rebuildCase (setInScope se env) expr bndr alts cont
 rebuild env expr (ApplyTo _ arg mb_se cont)   = rebuildApp  env expr arg mb_se cont
 
 rebuild env expr (Select _ bndr alts se cont) = rebuildCase (setInScope se env) expr bndr alts cont
 rebuild env expr (ApplyTo _ arg mb_se cont)   = rebuildApp  env expr arg mb_se cont
 
@@ -1331,8 +1394,8 @@ try to eliminate uses of v in the RHSs in favour of case_bndr; that
 way, there's a chance that v will now only be used once, and hence
 inlined.
 
 way, there's a chance that v will now only be used once, and hence
 inlined.
 
-Note 1
-~~~~~~
+Note [no-case-of-case]
+~~~~~~~~~~~~~~~~~~~~~~
 There is a time we *don't* want to do that, namely when
 -fno-case-of-case is on.  This happens in the first simplifier pass,
 and enhances full laziness.  Here's the bad case:
 There is a time we *don't* want to do that, namely when
 -fno-case-of-case is on.  This happens in the first simplifier pass,
 and enhances full laziness.  Here's the bad case:
@@ -1343,6 +1406,15 @@ in action in spectral/cichelli/Prog.hs:
         [(m,n) | m <- [1..max], n <- [1..max]]
 Hence the check for NoCaseOfCase.
 
         [(m,n) | m <- [1..max], n <- [1..max]]
 Hence the check for NoCaseOfCase.
 
+Note [Case of cast]
+~~~~~~~~~~~~~~~~~~~
+Consider       case (v `cast` co) of x { I# ->
+               ... (case (v `cast` co) of {...}) ...
+We'd like to eliminate the inner case.  We can get this neatly by 
+arranging that inside the outer case we add the unfolding
+       v |-> x `cast` (sym co)
+to v.  Then we should inline v at the inner case, cancel the casts, and away we go
+       
 Note 2
 ~~~~~~
 There is another situation when we don't want to do it.  If we have
 Note 2
 ~~~~~~
 There is another situation when we don't want to do it.  If we have
@@ -1381,8 +1453,8 @@ eliminate the last case, we must either make sure that x (as well as
 x1) has unfolding MkT y1.  THe straightforward thing to do is to do
 the binder-swap.  So this whole note is a no-op.
 
 x1) has unfolding MkT y1.  THe straightforward thing to do is to do
 the binder-swap.  So this whole note is a no-op.
 
-Note 3
-~~~~~~
+Note [zapOccInfo]
+~~~~~~~~~~~~~~~~~
 If we replace the scrutinee, v, by tbe case binder, then we have to nuke
 any occurrence info (eg IAmDead) in the case binder, because the
 case-binder now effectively occurs whenever v does.  AND we have to do
 If we replace the scrutinee, v, by tbe case binder, then we have to nuke
 any occurrence info (eg IAmDead) in the case binder, because the
 case-binder now effectively occurs whenever v does.  AND we have to do
@@ -1408,23 +1480,31 @@ after the outer case, and that makes (a,b) alive.  At least we do unless
 the case binder is guaranteed dead.
 
 \begin{code}
 the case binder is guaranteed dead.
 
 \begin{code}
-simplCaseBinder env (Var v) case_bndr
-  | not (switchIsOn (getSwitchChecker env) NoCaseOfCase)
+simplCaseBinder env scrut case_bndr
+  | switchIsOn (getSwitchChecker env) NoCaseOfCase
+       -- See Note [no-case-of-case]
+  = do { (env, case_bndr') <- simplBinder env case_bndr
+       ; return (env, case_bndr') }
 
 
+simplCaseBinder env (Var v) case_bndr
 -- Failed try [see Note 2 above]
 --     not (isEvaldUnfolding (idUnfolding v))
 -- Failed try [see Note 2 above]
 --     not (isEvaldUnfolding (idUnfolding v))
-
-  = simplBinder env (zapOccInfo case_bndr)             `thenSmpl` \ (env, case_bndr') ->
-    returnSmpl (modifyInScope env v case_bndr', case_bndr')
+  = do { (env, case_bndr') <- simplBinder env (zapOccInfo case_bndr)
+       ; return (modifyInScope env v case_bndr', case_bndr') }
        -- We could extend the substitution instead, but it would be
        -- a hack because then the substitution wouldn't be idempotent
        -- any more (v is an OutId).  And this does just as well.
            
        -- We could extend the substitution instead, but it would be
        -- a hack because then the substitution wouldn't be idempotent
        -- any more (v is an OutId).  And this does just as well.
            
+simplCaseBinder env (Cast (Var v) co) case_bndr                -- Note [Case of cast]
+  = do { (env, case_bndr') <- simplBinder env (zapOccInfo case_bndr)
+       ; let rhs = Cast (Var case_bndr') (mkSymCoercion co)
+       ; return (addBinderUnfolding env v rhs, case_bndr') }
+
 simplCaseBinder env other_scrut case_bndr 
 simplCaseBinder env other_scrut case_bndr 
-  = simplBinder env case_bndr          `thenSmpl` \ (env, case_bndr') ->
-    returnSmpl (env, case_bndr')
+  = do { (env, case_bndr') <- simplBinder env case_bndr
+       ; return (env, case_bndr') }
 
 
-zapOccInfo :: InId -> InId
+zapOccInfo :: InId -> InId     -- See Note [zapOccInfo]
 zapOccInfo b = b `setIdOccInfo` NoOccInfo
 \end{code}
 
 zapOccInfo b = b `setIdOccInfo` NoOccInfo
 \end{code}
 
@@ -1505,6 +1585,7 @@ simplDefault :: SimplEnv
 
 simplDefault env case_bndr' imposs_cons cont Nothing
   = return []  -- No default branch
 
 simplDefault env case_bndr' imposs_cons cont Nothing
   = return []  -- No default branch
+
 simplDefault env case_bndr' imposs_cons cont (Just rhs)
   |    -- This branch handles the case where we are 
        -- scrutinisng an algebraic data type
 simplDefault env case_bndr' imposs_cons cont (Just rhs)
   |    -- This branch handles the case where we are 
        -- scrutinisng an algebraic data type
@@ -1536,7 +1617,11 @@ simplDefault env case_bndr' imposs_cons cont (Just rhs)
                                -- altogether if it can't match
 
        [con] ->        -- It matches exactly one constructor, so fill it in
                                -- altogether if it can't match
 
        [con] ->        -- It matches exactly one constructor, so fill it in
-                do { con_alt <- mkDataConAlt case_bndr' con inst_tys rhs
+                do { tick (FillInCaseDefault case_bndr')
+                    ; us <- getUniquesSmpl
+                    ; let (ex_tvs, co_tvs, arg_ids) =
+                              dataConRepInstPat us con inst_tys
+                    ; let con_alt = (DataAlt con, ex_tvs ++ co_tvs ++ arg_ids, rhs)
                    ; Just (_, alt') <- simplAlt env [] case_bndr' cont con_alt
                        -- The simplAlt must succeed with Just because we have
                        -- already filtered out construtors that can't match
                    ; Just (_, alt') <- simplAlt env [] case_bndr' cont con_alt
                        -- The simplAlt must succeed with Just because we have
                        -- already filtered out construtors that can't match
@@ -1544,40 +1629,17 @@ simplDefault env case_bndr' imposs_cons cont (Just rhs)
 
        two_or_more -> simplify_default (map DataAlt gadt_imposs ++ imposs_cons)
 
 
        two_or_more -> simplify_default (map DataAlt gadt_imposs ++ imposs_cons)
 
-  | otherwise
+  | otherwise 
   = simplify_default imposs_cons
   where
     cant_match tys data_con = not (dataConCanMatch data_con tys)
 
     simplify_default imposs_cons
   = simplify_default imposs_cons
   where
     cant_match tys data_con = not (dataConCanMatch data_con tys)
 
     simplify_default imposs_cons
-       = do { let env' = mk_rhs_env env case_bndr' (mkOtherCon imposs_cons)
+       = do { let env' = addBinderOtherCon env case_bndr' imposs_cons
                -- Record the constructors that the case-binder *can't* be.
             ; rhs' <- simplExprC env' rhs cont
             ; return [(DEFAULT, [], rhs')] }
 
                -- Record the constructors that the case-binder *can't* be.
             ; rhs' <- simplExprC env' rhs cont
             ; return [(DEFAULT, [], rhs')] }
 
-mkDataConAlt :: Id -> DataCon -> [OutType] -> InExpr -> SimplM InAlt
--- Make a data-constructor alternative to replace the DEFAULT case
--- NB: there's something a bit bogus here, because we put OutTypes into an InAlt
-mkDataConAlt case_bndr con tys rhs
-  = do         { tick (FillInCaseDefault case_bndr)
-       ; args <- mk_args con tys
-       ; return (DataAlt con, args, rhs) }
-  where
-    mk_args con inst_tys
-      = do { (tv_bndrs, inst_tys') <- mk_tv_bndrs con inst_tys
-          ; let arg_tys = dataConInstArgTys con inst_tys'
-          ; arg_ids <- mapM (newId FSLIT("a")) arg_tys
-          ; returnSmpl (tv_bndrs ++ arg_ids) }
-
-    mk_tv_bndrs con inst_tys
-      | isVanillaDataCon con
-      = return ([], inst_tys)
-      | otherwise
-      = do { tv_uniqs <- getUniquesSmpl
-          ; let new_tvs    = zipWith mk tv_uniqs (dataConTyVars con)
-                mk uniq tv = mkTyVar (mkSysTvName uniq FSLIT("t")) (tyVarKind tv)
-          ; return (new_tvs, mkTyVarTys new_tvs) }
-
 simplAlt :: SimplEnv
         -> [AltCon]    -- These constructors can't be present when
                        -- matching this alternative
 simplAlt :: SimplEnv
         -> [AltCon]    -- These constructors can't be present when
                        -- matching this alternative
@@ -1601,7 +1663,7 @@ simplAlt env handled_cons case_bndr' cont' (DEFAULT, bndrs, rhs)
     simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
     returnSmpl (Just (emptyVarEnv, (DEFAULT, [], rhs')))
   where
     simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
     returnSmpl (Just (emptyVarEnv, (DEFAULT, [], rhs')))
   where
-    env' = mk_rhs_env env case_bndr' (mkOtherCon handled_cons)
+    env' = addBinderOtherCon env case_bndr' handled_cons
        -- Record the constructors that the case-binder *can't* be.
 
 simplAlt env handled_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
        -- Record the constructors that the case-binder *can't* be.
 
 simplAlt env handled_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
@@ -1609,10 +1671,9 @@ simplAlt env handled_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
     simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
     returnSmpl (Just (emptyVarEnv, (LitAlt lit, [], rhs')))
   where
     simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
     returnSmpl (Just (emptyVarEnv, (LitAlt lit, [], rhs')))
   where
-    env' = mk_rhs_env env case_bndr' (mkUnfolding False (Lit lit))
+    env' = addBinderUnfolding env case_bndr' (Lit lit)
 
 simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
 
 simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
-  | isVanillaDataCon con
   =    -- Deal with the pattern-bound variables
        -- Mark the ones that are in ! positions in the data constructor
        -- as certainly-evaluated.
   =    -- Deal with the pattern-bound variables
        -- Mark the ones that are in ! positions in the data constructor
        -- as certainly-evaluated.
@@ -1622,52 +1683,12 @@ simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
     simplBinders env (add_evals con vs)                `thenSmpl` \ (env, vs') ->
 
                -- Bind the case-binder to (con args)
     simplBinders env (add_evals con vs)                `thenSmpl` \ (env, vs') ->
 
                -- Bind the case-binder to (con args)
-    let unf       = mkUnfolding False (mkConApp con con_args)
-       inst_tys' = tyConAppArgs (idType case_bndr')
-       con_args  = map Type inst_tys' ++ map varToCoreExpr vs' 
-       env'      = mk_rhs_env env case_bndr' unf
+    let inst_tys' = tyConAppArgs (idType case_bndr')
+       con_args  = map Type inst_tys' ++ varsToCoreExprs vs' 
+       env'      = addBinderUnfolding env case_bndr' (mkConApp con con_args)
     in
     simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
     returnSmpl (Just (emptyVarEnv, (DataAlt con, vs', rhs')))
     in
     simplExprC env' rhs cont'  `thenSmpl` \ rhs' ->
     returnSmpl (Just (emptyVarEnv, (DataAlt con, vs', rhs')))
-
-  | otherwise  -- GADT case
-  = let
-       (tvs,ids) = span isTyVar vs
-    in
-    simplBinders env tvs                       `thenSmpl` \ (env1, tvs') ->
-    case coreRefineTys con tvs' (idType case_bndr') of {
-       Nothing         -- Inaccessible
-           | opt_PprStyle_Debug        -- Hack: if debugging is on, generate an error case 
-                                       --       so we can see it
-           ->  let rhs' = mkApps (Var eRROR_ID) 
-                               [Type (substTy env (exprType rhs)),
-                                Lit (mkStringLit "Impossible alternative (GADT)")]
-               in 
-               simplBinders env1 ids           `thenSmpl` \ (env2, ids') -> 
-               returnSmpl (Just (emptyVarEnv, (DataAlt con, tvs' ++ ids', rhs'))) 
-
-           | otherwise -- Filter out the inaccessible branch
-           -> return Nothing ; 
-
-       Just refine@(tv_subst_env, _) ->        -- The normal case
-
-    let 
-       env2 = refineSimplEnv env1 refine
-       -- Simplify the Ids in the refined environment, so their types
-       -- reflect the refinement.  Usually this doesn't matter, but it helps
-       -- in mkDupableAlt, when we want to float a lambda that uses these binders
-       -- Furthermore, it means the binders contain maximal type information
-    in
-    simplBinders env2 (add_evals con ids)      `thenSmpl` \ (env3, ids') ->
-    let unf        = mkUnfolding False con_app
-       con_app    = mkConApp con con_args
-       con_args   = map varToCoreExpr vs'      -- NB: no inst_tys'
-       env_w_unf  = mk_rhs_env env3 case_bndr' unf
-       vs'        = tvs' ++ ids'
-    in
-    simplExprC env_w_unf rhs cont'     `thenSmpl` \ rhs' ->
-    returnSmpl (Just (tv_subst_env, (DataAlt con, vs', rhs'))) }
-
   where
        -- add_evals records the evaluated-ness of the bound variables of
        -- a case pattern.  This is *important*.  Consider
   where
        -- add_evals records the evaluated-ness of the bound variables of
        -- a case pattern.  This is *important*.  Consider
@@ -1699,8 +1720,13 @@ simplAlt env handled_cons case_bndr' cont' (DataAlt con, vs, rhs)
     zap_occ_info | isDeadBinder case_bndr' = \id -> id
                 | otherwise               = zapOccInfo
 
     zap_occ_info | isDeadBinder case_bndr' = \id -> id
                 | otherwise               = zapOccInfo
 
-mk_rhs_env env case_bndr' case_bndr_unf
-  = modifyInScope env case_bndr' (case_bndr' `setIdUnfolding` case_bndr_unf)
+addBinderUnfolding :: SimplEnv -> Id -> CoreExpr -> SimplEnv
+addBinderUnfolding env bndr rhs
+  = modifyInScope env bndr (bndr `setIdUnfolding` mkUnfolding False rhs)
+
+addBinderOtherCon :: SimplEnv -> Id -> [AltCon] -> SimplEnv
+addBinderOtherCon env bndr cons
+  = modifyInScope env bndr (bndr `setIdUnfolding` mkOtherCon cons)
 \end{code}
 
 
 \end{code}
 
 
@@ -1743,7 +1769,7 @@ knownCon env scrut con args bndr alts cont
                                  simplExprF env rhs cont
 
        (DataAlt dc, bs, rhs)  
                                  simplExprF env rhs cont
 
        (DataAlt dc, bs, rhs)  
-               -> ASSERT( n_drop_tys + length bs == length args )
+               -> -- ASSERT( n_drop_tys + length bs == length args )
                   bind_args env dead_bndr bs (drop n_drop_tys args)    $ \ env ->
                   let
                        -- It's useful to bind bndr to scrut, rather than to a fresh
                   bind_args env dead_bndr bs (drop n_drop_tys args)    $ \ env ->
                   let
                        -- It's useful to bind bndr to scrut, rather than to a fresh
@@ -1763,10 +1789,8 @@ knownCon env scrut con args bndr alts cont
                   simplNonRecX env bndr bndr_rhs               $ \ env ->
                   simplExprF env rhs cont
                where
                   simplNonRecX env bndr bndr_rhs               $ \ env ->
                   simplExprF env rhs cont
                where
-                  dead_bndr = isDeadBinder bndr
-                  n_drop_tys | isVanillaDataCon dc = tyConArity (dataConTyCon dc)
-                             | otherwise           = 0
-                       -- Vanilla data constructors lack type arguments in the pattern
+                  dead_bndr  = isDeadBinder bndr
+                  n_drop_tys = tyConArity (dataConTyCon dc)
 
 -- Ugh!
 bind_args env dead_bndr [] _ thing_inside = thing_inside env
 
 -- Ugh!
 bind_args env dead_bndr [] _ thing_inside = thing_inside env
@@ -1782,7 +1806,7 @@ bind_args env dead_bndr (b:bs) (arg : args) thing_inside
                -- Note that the binder might be "dead", because it doesn't occur 
                -- in the RHS; and simplNonRecX may therefore discard it via postInlineUnconditionally
                -- Nevertheless we must keep it if the case-binder is alive, because it may
                -- Note that the binder might be "dead", because it doesn't occur 
                -- in the RHS; and simplNonRecX may therefore discard it via postInlineUnconditionally
                -- Nevertheless we must keep it if the case-binder is alive, because it may
-               -- be used in teh con_app
+               -- be used in the con_app.  See Note [zapOccInfo]
     in
     simplNonRecX env b' arg    $ \ env ->
     bind_args env dead_bndr bs args thing_inside
     in
     simplNonRecX env b' arg    $ \ env ->
     bind_args env dead_bndr bs args thing_inside
@@ -2063,7 +2087,7 @@ mkDupableAlt env case_bndr' cont alt
        then newId FSLIT("w") realWorldStatePrimTy      `thenSmpl` \ rw_id ->
             returnSmpl ([rw_id], [Var realWorldPrimId])
        else 
        then newId FSLIT("w") realWorldStatePrimTy      `thenSmpl` \ rw_id ->
             returnSmpl ([rw_id], [Var realWorldPrimId])
        else 
-            returnSmpl (used_bndrs', map varToCoreExpr used_bndrs')
+            returnSmpl (used_bndrs', varsToCoreExprs used_bndrs')
     )                                                  `thenSmpl` \ (final_bndrs', final_args) ->
 
        -- See comment about "$j" name above
     )                                                  `thenSmpl` \ (final_bndrs', final_args) ->
 
        -- See comment about "$j" name above