@@ -601,7 +601,9 @@ prune proj (Case n alts)
601 -- | proj -> mkProj n 0 args (prune proj sc)
601 -- | proj -> mkProj n 0 args (prune proj sc)
603 as@[SucCase cn sc]
603 as@[SucCase cn sc]
605+ , not (cn `improjectibleSC` sc)
604− | proj -> mkProj n (-1) [cn] (prune proj sc)
606+ -> projRep cn n (-1) $ prune proj sc
606 as@[ConstCase _ sc]
608 as@[ConstCase _ sc]
607 -> prune proj sc
609 -> prune proj sc
@@ -641,6 +643,21 @@ prune proj (Case n alts)
641 = SucCase sn (mkForce n arg rhs)
643 = SucCase sn (mkForce n arg rhs)
642 mkForceAlt n arg (DefaultCase rhs)
644 mkForceAlt n arg (DefaultCase rhs)
643 = DefaultCase (mkForce n arg rhs)
645 = DefaultCase (mkForce n arg rhs)
647+ -- Figure out whether the SC is improjectible:
648+ -- For example, (Case n _) only admits /names/ as "n"
649+ -- so we cannot replace n with a projection of anything.
650+ improjectibleSC :: Name -> SC -> Bool
651+ n `improjectibleSC` Case x alts = n == x || (n `improjectibleAlt`) `any` alts
652+ n `improjectibleSC` ProjCase t alt = n `improjectibleAlt` alt
653+ n `improjectibleSC` _ = False -- we can replace freely in terms
655+ improjectibleAlt :: Name -> CaseAlt -> Bool
656+ n `improjectibleAlt` ConCase cn t args sc = n `improjectibleSC` sc
657+ n `improjectibleAlt` FnCase cn args sc = n `improjectibleSC` sc
658+ n `improjectibleAlt` ConstCase t sc = n `improjectibleSC` sc
659+ n `improjectibleAlt` SucCase cn sc = n `improjectibleSC` sc
660+ n `improjectibleAlt` DefaultCase sc = n `improjectibleSC` sc
645 forceTm n arg t = subst arg (forceArg n) t
662 forceTm n arg t = subst arg (forceArg n) t