@@ -601,7 +601,9 @@ prune proj (Case n alts)
601601 -- | proj -> mkProj n 0 args (prune proj sc)
602602
603603 as@[SucCase cn sc]
604− | proj -> mkProj n (-1) [cn] (prune proj sc)
604+ | proj
605+ , not (cn `improjectibleSC` sc)
606+ -> projRep cn n (-1) $ prune proj sc
605607
606608 as@[ConstCase _ sc]
607609 -> prune proj sc
@@ -641,6 +643,21 @@ prune proj (Case n alts)
641643 = SucCase sn (mkForce n arg rhs)
642644 mkForceAlt n arg (DefaultCase rhs)
643645 = DefaultCase (mkForce n arg rhs)
646+
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
654+
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
644661
645662 forceTm n arg t = subst arg (forceArg n) t
646663