diff --git a/.hlint.yaml b/.hlint.yaml
index e7218f73..d7eadacf 100644
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -94,6 +94,10 @@
 # - ignore: {name: Use let}
 # - ignore: {name: Use const, within: SpecialModule} # Only within certain modules
 
+# Keep `\_whatIsBeingDiscarded → …` over `const …`: the named-but-ignored
+# binder documents *what* is being discarded, which `const` erases.
+- ignore: {name: Use const}
+
 # Define some custom infix operators
 # - fixity: infixr 3 ~^#^~
 
diff --git a/changelog.d/20260708_090000_unisay_case_of_known_constructor.md b/changelog.d/20260708_090000_unisay_case_of_known_constructor.md
new file mode 100644
index 00000000..1b841a51
--- /dev/null
+++ b/changelog.d/20260708_090000_unisay_case_of_known_constructor.md
@@ -0,0 +1,16 @@
+### Added
+
+- Case-of-known-constructor folds in the IR optimizer (#177): a tag read over a
+  saturated sum-type constructor application (`ReflectCtor (K a₁ … aₙ)`) folds
+  to `K`'s tag string, and a field read (`DataArgumentByIndex i (K a₁ … aₙ)`)
+  folds to `aᵢ` — the algebraic-type twin of the existing record-projection
+  fold (`reduceObjectProp`). The tag fold then meets constant folding and the
+  unreachable-branch rules, collapsing a decision tree over a known
+  constructor to its live branch. Discarded arguments are dropped with the same
+  discipline DCE applies to unused bindings (an unrun `Effect` thunk is never a
+  casualty — an effect that must run is the kept field, not a dropped one). The
+  fold fires only at exact saturation, so a partial application is left a
+  function, and only sum types get the tag fold, since product constructors
+  carry no tag row. Standalone impact is near zero — the shapes appear once
+  dictionary specialization (#178/#180) inlines a constructor into a match — so
+  this lands as the enabler those issues build on.
diff --git a/lib/Language/PureScript/Backend/IR.hs b/lib/Language/PureScript/Backend/IR.hs
index f50cc103..5804e44a 100644
--- a/lib/Language/PureScript/Backend/IR.hs
+++ b/lib/Language/PureScript/Backend/IR.hs
@@ -191,6 +191,7 @@ collectDataDeclarations cfnModules =
   -- A type is a product type iff it has exactly one constructor. Grouping the
   -- constructors by type first makes this independent of the order in which
   -- they appear in the module bindings.
+  classify ∷ Map k a → (AlgebraicType, Map k a)
   classify ctors =
     (if Map.size ctors == 1 then ProductType else SumType, ctors)
 
diff --git a/lib/Language/PureScript/Backend/IR/DCE.hs b/lib/Language/PureScript/Backend/IR/DCE.hs
index d204ee48..9570631f 100644
--- a/lib/Language/PureScript/Backend/IR/DCE.hs
+++ b/lib/Language/PureScript/Backend/IR/DCE.hs
@@ -327,6 +327,10 @@ eliminateDeadCode uber@UberModule {..} =
          where
           (scopeWithParams, paramNodes) =
             foldl' bindParam (scope, DL.empty) (toList params)
+          bindParam
+            ∷ (Scope, DList Node)
+            → Parameter (Id, b)
+            → (Scope, DList Node)
           bindParam (sc, nodes) = \case
             ParamUnused _ann' → (sc, nodes)
             ParamNamed (paramId, _ann') name →
diff --git a/lib/Language/PureScript/Backend/IR/Linker.hs b/lib/Language/PureScript/Backend/IR/Linker.hs
index 5b9b0a14..06390732 100644
--- a/lib/Language/PureScript/Backend/IR/Linker.hs
+++ b/lib/Language/PureScript/Backend/IR/Linker.hs
@@ -132,6 +132,7 @@ qualifyTopRefs moduleName = go
        where
         topNames' ∷ Set Name =
           foldl' shadowParam topNames parameters
+        shadowParam ∷ Set Name → Parameter ann → Set Name
         shadowParam names = \case
           ParamNamed _ann argName → Set.delete argName names
           ParamUnused _ann → names
diff --git a/lib/Language/PureScript/Backend/IR/MagicDo.hs b/lib/Language/PureScript/Backend/IR/MagicDo.hs
index e8b5c7a0..d87d5853 100644
--- a/lib/Language/PureScript/Backend/IR/MagicDo.hs
+++ b/lib/Language/PureScript/Backend/IR/MagicDo.hs
@@ -70,6 +70,7 @@ import Language.PureScript.Backend.IR.Types
   , noAnn
   , rewriteExpTopDownM
   , substituteMoveM
+  , unwindApp
   , pattern Abs
   , pattern App
   )
@@ -185,7 +186,7 @@ aliases, projecting fields out of literal dictionaries, and beta-reducing — an
 match once it is exposed as @bind dict action continuation@.
 -}
 classify ∷ (QName → Maybe Exp) → Exp → SupplyM (Maybe Node)
-classify resolve = go maxHops . spine
+classify resolve = go maxHops . unwindApp
  where
   go ∷ Int → (Exp, [Exp]) → SupplyM (Maybe Node)
   go fuel (hd, args)
@@ -228,7 +229,7 @@ classify resolve = go maxHops . spine
 
   -- Re-attach trailing arguments after a head reduction.
   reSpine ∷ Exp → [Exp] → (Exp, [Exp])
-  reSpine hd' extra = let (h, a) = spine hd' in (h, a <> extra)
+  reSpine hd' extra = let (h, a) = unwindApp hd' in (h, a <> extra)
 
 {- | Does the expression ultimately denote the given instance, possibly through
 module-local aliases?
@@ -250,14 +251,6 @@ isBindDict resolve dict =
 --------------------------------------------------------------------------------
 -- Helpers ---------------------------------------------------------------------
 
--- | Unwind an application into its head and arguments (left to right).
-spine ∷ Exp → (Exp, [Exp])
-spine = go []
- where
-  go ∷ [Exp] → Exp → (Exp, [Exp])
-  go acc (App _ f a) = go (a : acc) f
-  go acc h = (h, acc)
-
 {- | Run an Effect/ST computation: apply the thunk to no arguments. The
 synthetic @Prim.undefined@ argument is erased to an empty argument list by
 the Lua code generator, so this emits @m()@.
diff --git a/lib/Language/PureScript/Backend/IR/Optimizer.hs b/lib/Language/PureScript/Backend/IR/Optimizer.hs
index b7ae4003..29f87f12 100644
--- a/lib/Language/PureScript/Backend/IR/Optimizer.hs
+++ b/lib/Language/PureScript/Backend/IR/Optimizer.hs
@@ -28,7 +28,8 @@ import Language.PureScript.Backend.IR.Pass
   )
 import Language.PureScript.Backend.IR.Supply (SupplyM, runSupply)
 import Language.PureScript.Backend.IR.Types
-  ( Ann
+  ( AlgebraicType (SumType)
+  , Ann
   , Exp
   , Grouping (..)
   , Parameter (..)
@@ -38,6 +39,7 @@ import Language.PureScript.Backend.IR.Types
   , alphaEq
   , countFreeRef
   , countFreeRefs
+  , ctorId
   , getAnn
   , isForeignImport
   , isNonRecursiveLiteral
@@ -49,8 +51,7 @@ import Language.PureScript.Backend.IR.Types
   , substituteCopyM
   , substituteMoveM
   , thenRewrite
-  , pattern Abs
-  , pattern App
+  , unwindApp
   )
 import Language.PureScript.Backend.IR.Uncurry (uncurryWorkerWrapper)
 import Language.PureScript.Backend.IR.Uniquify (uniquifyNames)
@@ -373,6 +374,7 @@ optimizedExpressionM =
   rewriteExpBottomUpM
     ( constantFolding
         `thenRewrite` reduceObjectProp
+        `thenRewrite` reduceKnownConstructor
         `thenRewrite` betaReduce
         `thenRewrite` removeUnreachableThenBranch
         `thenRewrite` removeUnreachableElseBranch
@@ -439,6 +441,52 @@ reduceObjectProp =
         Nothing → ObjectProp ann obj prop
     _ → Nothing
 
+{- | Case-of-known-constructor for algebraic types (issue #177), the
+'reduceObjectProp' twin for data constructors:
+
+  * @ReflectCtor (K a₁ … aₙ)@ — a tag read over a saturated /sum-type/
+    constructor application — folds to @K@'s tag string. The surrounding
+    equality test then meets 'constantFolding' and
+    'removeUnreachableThenBranch' / 'removeUnreachableElseBranch', which
+    collapse the decision tree to its live branch.
+  * @DataArgumentByIndex i (K a₁ … aₙ)@ — a field read — folds to @aᵢ@.
+
+A constructor application is the curried unary-'App' spine
+@App (… (App (Ctor …) a₁) …) aₙ@ that translation and the pattern
+matcher build. The fold fires only when the spine is /saturated/ (as
+many arguments as the constructor declares fields), so a partial
+application — still a function — is left alone.
+
+'ReflectCtor' folds for 'SumType' only: product constructors omit the
+@$ctor@ tag row in the generated Lua (see the @Ctor@ case of
+'Language.PureScript.Backend.Lua.fromIR'), so reducing a product-type
+tag read to a string would invent a value the runtime reads as @nil@.
+Field reads fold for either shape, since @valueᵢ@ rows exist for both.
+
+Discarded arguments are dropped, not evaluated — the discipline
+'reduceObjectProp' applies to discarded record fields and DCE applies to
+unused bindings. A dropped argument cannot skip an 'Effect': effects are
+unrun thunks here, run only when applied, so an effect that must run is
+the /kept/ argument (the field a match actually binds), never a dropped
+one; the only casualties are the pure divergence or partiality that DCE
+already elides. The folded value takes the read node's own annotation,
+not the argument's, for the reason spelled out on 'reduceObjectProp'.
+-}
+reduceKnownConstructor ∷ Applicative m ⇒ RewriteRuleM m Ann
+reduceKnownConstructor =
+  pure . \case
+    ReflectCtor ann scrutinee
+      | (Ctor _ SumType modName tyName ctorName fields, args) ←
+          unwindApp scrutinee
+      , length args == length fields →
+          Just $ LiteralString ann (ctorId modName tyName ctorName)
+    DataArgumentByIndex ann index scrutinee
+      | (Ctor _ _ _ _ _ fields, args) ← unwindApp scrutinee
+      , length args == length fields
+      , Just arg ← viaNonEmpty head (List.genericDrop index args) →
+          Just (setAnn ann arg)
+    _ → Nothing
+
 {- Note [Beta reduction and local inlining share an inlining guard]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 'betaReduce' and 'inlineLocalBinding' decide whether to paste an expression
diff --git a/lib/Language/PureScript/Backend/IR/Types.hs b/lib/Language/PureScript/Backend/IR/Types.hs
index 76bcfdc6..0c97727d 100644
--- a/lib/Language/PureScript/Backend/IR/Types.hs
+++ b/lib/Language/PureScript/Backend/IR/Types.hs
@@ -137,6 +137,19 @@ later alternative. Every unary rule keeps using it unchanged.
 pattern App ∷ ann → RawExp ann → RawExp ann → RawExp ann
 pattern App ann f a = AppN ann f (a :| [])
 
+{- | Peel a curried unary-'App' spine into its head and its arguments,
+first-applied first: @App (App f a₁) a₂@ becomes @(f, [a₁, a₂])@. A
+genuinely n-ary 'AppN' node is not a spine link and stays in the head
+(see Note [n-ary application]).
+-}
+unwindApp ∷ ∀ ann. RawExp ann → (RawExp ann, [RawExp ann])
+unwindApp = go []
+ where
+  go ∷ [RawExp ann] → RawExp ann → (RawExp ann, [RawExp ann])
+  go acc = \case
+    App _ f a → go (a : acc) f
+    e → (e, acc)
+
 {- Note [n-ary abstraction]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The definition-side counterpart of Note [n-ary application].
@@ -611,6 +624,7 @@ countFreeRefs = fmap getSum . MMap.toMap . countFreeRefs' mempty
     AbsN _ann params body →
       countFreeRefs' (foldl' bindParam bound params) body
      where
+      bindParam ∷ Set Name → Parameter ann → Set Name
       bindParam names = \case
         ParamNamed _paramAnn name → Set.insert name names
         ParamUnused _paramAnn → names
@@ -856,6 +870,10 @@ freshenBinders = go Map.empty
       (renames', params') ← mapAccumM freshenParam renames params
       AbsN ann params' <$> go renames' body
      where
+      freshenParam
+        ∷ Map Name Name
+        → Parameter ann
+        → SupplyM (Map Name Name, Parameter ann)
       freshenParam rs = \case
         p@(ParamUnused _paramAnn) → pure (rs, p)
         ParamNamed paramAnn name → do
diff --git a/lib/Language/PureScript/Backend/IR/Uncurry.hs b/lib/Language/PureScript/Backend/IR/Uncurry.hs
index 87d38d9b..804749f6 100644
--- a/lib/Language/PureScript/Backend/IR/Uncurry.hs
+++ b/lib/Language/PureScript/Backend/IR/Uncurry.hs
@@ -110,8 +110,8 @@ import Language.PureScript.Backend.IR.Types
   , rewrittenIf
   , setAnn
   , subexpressions
+  , unwindApp
   , pattern Abs
-  , pattern App
   )
 
 {- | Split every qualifying binding into worker and wrapper and rewrite
@@ -359,16 +359,12 @@ taken: 'AppN' argument lists are not spines (Note [n-ary application]).
 -}
 saturatedSite
   ∷ Map (Qualified Name) Int → Exp → Maybe (Qualified Name, [Exp])
-saturatedSite arities e = case unwind e [] of
+saturatedSite arities e = case unwindApp e of
   (Ref _ann q, args)
     | Just arity ← Map.lookup q arities
     , length args == arity →
         Just (q, args)
   _ → Nothing
- where
-  unwind ∷ Exp → [Exp] → (Exp, [Exp])
-  unwind (App _ann fn a) acc = unwind fn (a : acc)
-  unwind hd acc = (hd, acc)
 
 {- | Count the saturated sites of each candidate within one expression.
 Absent keys have no sites.
diff --git a/lib/Language/PureScript/Backend/Lua/Printer.hs b/lib/Language/PureScript/Backend/Lua/Printer.hs
index 102dd862..dd64f678 100644
--- a/lib/Language/PureScript/Backend/Lua/Printer.hs
+++ b/lib/Language/PureScript/Backend/Lua/Printer.hs
@@ -47,6 +47,7 @@ printStatements statements =
     statements
     (fmap Just (drop 1 statements) <> [Nothing])
  where
+  separator ∷ Maybe (Annotated Comments StatementF) → ADoc
   separator = \case
     Just (Ann next) | startsWithOpenParen next → ";"
     _ → mempty
diff --git a/test/Language/PureScript/Backend/IR/FlattenDeepBinds/Spec.hs b/test/Language/PureScript/Backend/IR/FlattenDeepBinds/Spec.hs
index 50628600..74e35633 100644
--- a/test/Language/PureScript/Backend/IR/FlattenDeepBinds/Spec.hs
+++ b/test/Language/PureScript/Backend/IR/FlattenDeepBinds/Spec.hs
@@ -30,7 +30,6 @@ import Language.PureScript.Backend.IR.Types
   , refImported
   , refLocal
   , subexpressions
-  , pattern App
   )
 import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy)
 import Test.Hspec.Hedgehog.Extended (prop)
diff --git a/test/Language/PureScript/Backend/IR/Gen.hs b/test/Language/PureScript/Backend/IR/Gen.hs
index c169d13b..50aa171d 100644
--- a/test/Language/PureScript/Backend/IR/Gen.hs
+++ b/test/Language/PureScript/Backend/IR/Gen.hs
@@ -61,7 +61,31 @@ exp =
       , Gen.subtermM exp \e →
           (`IR.lets` e) <$> Gen.nonEmpty (Range.linear 1 5) binding
       )
+    , (3, genCtorApp)
+    , (2, IR.reflectCtor <$> genCtorApp)
+    ,
+      ( 2
+      , IR.dataArgumentByIndex
+          <$> Gen.integral (Range.linear 0 3)
+          <*> genCtorApp
+      )
     ]
+ where
+  -- A saturated constructor application: exactly one argument per field
+  -- (nullary ctor ⇒ a bare 'Ctor'). This is the shape the #177
+  -- case-of-known-constructor fold matches on, so the fold-firing input
+  -- reaches the 'exp'-based suites too.
+  genCtorApp = do
+    fields ← Gen.list (Range.linear 0 3) fieldName
+    ctorExp ←
+      IR.ctor
+        <$> Gen.enumBounded
+        <*> moduleName
+        <*> tyName
+        <*> ctorName
+        <*> pure fields
+    args ← forM fields \_field → exp
+    pure (foldl' IR.application ctorExp args)
 
 {- | A generation-time scope: the local names with an enclosing binder.
 Lets 'scopedExp' emit only references that resolve to a binder.
@@ -108,9 +132,33 @@ scopedExpIn scope =
             (Range.linear 1 4)
             ((,) <$> genPropName <*> scopedExpIn scope)
       )
+    , (3, genCtorApp)
+    , (2, IR.reflectCtor <$> genCtorApp)
+    ,
+      ( 2
+      , IR.dataArgumentByIndex
+          <$> Gen.integral (Range.linear 0 3)
+          <*> genCtorApp
+      )
     ]
  where
   scopedRef = IR.refLocal <$> Gen.element (Set.toList scope)
+  -- A saturated constructor application: exactly one argument per field
+  -- (nullary ctor ⇒ a bare 'Ctor'). A 'Ctor' node binds nothing and
+  -- references no 'Scope' entry, so every argument just reuses the
+  -- incoming scope — the same category as application / if / object.
+  -- This is the shape the #177 case-of-known-constructor fold matches on.
+  genCtorApp = do
+    fields ← Gen.list (Range.linear 0 3) fieldName
+    ctorExp ←
+      IR.ctor
+        <$> Gen.enumBounded
+        <*> moduleName
+        <*> tyName
+        <*> ctorName
+        <*> pure fields
+    args ← forM fields \_field → scopedExpIn scope
+    pure (foldl' IR.application ctorExp args)
   genAbs = do
     (param, body) ← genBinderBody
     pure (IR.abstraction param body)
diff --git a/test/Language/PureScript/Backend/IR/Optimizer/Spec.hs b/test/Language/PureScript/Backend/IR/Optimizer/Spec.hs
index b78a1c80..c641eaf9 100644
--- a/test/Language/PureScript/Backend/IR/Optimizer/Spec.hs
+++ b/test/Language/PureScript/Backend/IR/Optimizer/Spec.hs
@@ -4,6 +4,7 @@ import Data.Map qualified as Map
 import Data.Text qualified as Text
 import Hedgehog (PropertyT, annotateShow, diff, forAll, (===))
 import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
 import Language.PureScript.Backend.IR.Gen qualified as Gen
 import Language.PureScript.Backend.IR.Inliner (Annotation (Always, Never))
 import Language.PureScript.Backend.IR.Linker (LinkMode (..))
@@ -14,10 +15,13 @@ import Language.PureScript.Backend.IR.Linter
   , unboundLocals
   )
 import Language.PureScript.Backend.IR.Names
-  ( Name (..)
+  ( CtorName (..)
+  , FieldName (..)
+  , Name (..)
   , PropName (..)
   , QName (..)
   , Qualified (Local)
+  , TyName (..)
   , moduleNameFromString
   )
 import Language.PureScript.Backend.IR.Optimizer
@@ -28,7 +32,8 @@ import Language.PureScript.Backend.IR.Optimizer
   )
 import Language.PureScript.Backend.IR.Supply (runSupply)
 import Language.PureScript.Backend.IR.Types
-  ( Exp
+  ( AlgebraicType (ProductType, SumType)
+  , Exp
   , Grouping (..)
   , Module (..)
   , RawExp (..)
@@ -38,6 +43,10 @@ import Language.PureScript.Backend.IR.Types
   , application
   , applicationN
   , countFreeRef
+  , countFreeRefs
+  , ctor
+  , ctorId
+  , dataArgumentByIndex
   , eq
   , getAnn
   , ifThenElse
@@ -46,6 +55,7 @@ import Language.PureScript.Backend.IR.Types
   , literalBool
   , literalInt
   , literalObject
+  , literalString
   , noAnn
   , objectProp
   , objectUpdate
@@ -53,8 +63,10 @@ import Language.PureScript.Backend.IR.Types
   , paramUnused
   , refImported
   , refLocal
+  , reflectCtor
   , setAnn
   )
+import Language.PureScript.Backend.IR.Uniquify (uniquifyNamesInExpr)
 import Test.Hspec
   ( Spec
   , SpecWith
@@ -308,6 +320,113 @@ spec = describe "IR Optimizer" do
       annotateShow optimized
       addKept === [QName mainModule (Name "add")]
 
+  describe "folds case-of-known-constructor (#177)" do
+    let maybeMod = moduleNameFromString "Data.Maybe"
+        maybeTy = TyName "Maybe"
+        justName = CtorName "Just"
+        justCtor = ctor SumType maybeMod maybeTy justName [FieldName "value0"]
+        just = application justCtor
+        justTag = ctorId maybeMod maybeTy justName
+
+        tupleMod = moduleNameFromString "Data.Tuple"
+        tupleTy = TyName "Tuple"
+        tupleName = CtorName "Tuple"
+        tupleCtor =
+          ctor
+            ProductType
+            tupleMod
+            tupleTy
+            tupleName
+            [FieldName "value0", FieldName "value1"]
+        tuple a = application (application tupleCtor a)
+
+    it "reduces a saturated sum-type tag read to the tag string" do
+      optimizedExpression (reflectCtor (just (literalInt 1)))
+        `shouldBe` literalString justTag
+
+    it "reduces a field read to the constructor argument" do
+      optimizedExpression (dataArgumentByIndex 0 (just (literalInt 7)))
+        `shouldBe` literalInt 7
+
+    it "reads the second field of a saturated product application" do
+      optimizedExpression
+        (dataArgumentByIndex 1 (tuple (literalInt 1) (literalInt 2)))
+        `shouldBe` literalInt 2
+
+    it "collapses a tag-equality test into its result" do
+      -- The payoff cascade: the folded tag meets the surrounding Eq and
+      -- constant folding reduces the whole decision-tree test.
+      let original = eq (reflectCtor (just (literalInt 1))) (literalString justTag)
+      optimizedExpression original `shouldBe` literalBool True
+
+    it "declines a partially applied constructor" do
+      -- One argument against a two-field constructor: still a function,
+      -- so the field read must not fire.
+      let original = dataArgumentByIndex 0 (application tupleCtor (literalInt 1))
+      optimizedExpression original `shouldBe` original
+
+    it "declines a product-type tag read" do
+      -- Product constructors carry no $ctor row at runtime, so folding
+      -- the tag would invent a value the runtime reads as nil.
+      let original = reflectCtor (tuple (literalInt 1) (literalInt 2))
+      optimizedExpression original `shouldBe` original
+
+    it "drops the discarded arguments of a field read" do
+      -- Only the read field survives; the sibling is gone, not Let-bound.
+      optimizedExpression
+        (dataArgumentByIndex 0 (tuple (refLocal (Name "a")) (refLocal (Name "b"))))
+        `shouldBe` refLocal (Name "a")
+
+    -- A discarded field can hold a `Just Always`-annotated accessor (see
+    -- the record-projection block); the fold must take the read node's
+    -- own annotation, never the argument's, or the result becomes
+    -- unconditionally inlinable and duplicates across use sites.
+    let dictModule = moduleNameFromString "Dict"
+        accessor =
+          ObjectProp
+            (Just Always)
+            (refImported dictModule (Name "foreign"))
+            (PropName "value0")
+
+    it "does not leak the kept argument's annotation" do
+      let original = dataArgumentByIndex 0 (just accessor)
+      getAnn (optimizedExpression original) `shouldBe` Nothing
+
+    it "keeps the read node's own annotation on the folded field" do
+      let original = DataArgumentByIndex (Just Never) 0 (just accessor)
+      getAnn (optimizedExpression original) `shouldBe` Just Never
+
+    -- Randomized discard-semantics stress (the issue's explicit ask):
+    -- across arbitrary arity, algebraic type, and argument content, a
+    -- field read folds to exactly its argument with the siblings gone
+    -- (no residue), and a sum-type tag read folds to the tag string.
+    let trivialArg = Gen.choice [Gen.scalarExp, refLocal <$> Gen.name]
+
+    prop "folds a saturated field read to its argument at any arity" do
+      before ← forAll (Gen.list (Range.linear 0 3) trivialArg)
+      kept ← forAll trivialArg
+      after ← forAll (Gen.list (Range.linear 0 3) trivialArg)
+      algTy ← forAll (Gen.element [SumType, ProductType])
+      modName ← forAll Gen.moduleName
+      ty ← forAll Gen.tyName
+      cn ← forAll Gen.ctorName
+      let args = before <> [kept] <> after
+          fields = FieldName . show <$> [1 .. length args]
+          app = foldl' application (ctor algTy modName ty cn fields) args
+          index = fromIntegral (length before)
+      -- Equality to the kept argument alone proves the siblings are
+      -- dropped, not Let-bound or duplicated.
+      optimizedExpression (dataArgumentByIndex index app) === kept
+
+    prop "folds a saturated sum-type tag read to the tag string" do
+      args ← forAll (Gen.list (Range.linear 0 5) trivialArg)
+      modName ← forAll Gen.moduleName
+      ty ← forAll Gen.tyName
+      cn ← forAll Gen.ctorName
+      let fields = FieldName . show <$> [1 .. length args]
+          app = foldl' application (ctor SumType modName ty cn fields) args
+      optimizedExpression (reflectCtor app) === literalString (ctorId modName ty cn)
+
   describe "inlines expressions" do
     test "inlines literals" do
       name ← forAll Gen.name
@@ -660,6 +779,65 @@ spec = describe "IR Optimizer" do
       annotateShow original
       optimizedUberModule original === expected
 
+    -- The constructor twin of the record-projection test above (#177):
+    -- inlining a saturated constructor into its field read forms the
+    -- redex mid-fixpoint, the fold takes the argument, and DCE drops the
+    -- emptied binding.
+    test "constructor field read after inlining" do
+      name ← forAll Gen.name
+      let uberName = moduleNameFromString "Main"
+          linkMode = LinkAsModule uberName
+          mkUber = Linker.makeUberModule linkMode . pure . wrapInModule
+          boxCtor =
+            ctor
+              ProductType
+              uberName
+              (TyName "Box")
+              (CtorName "Box")
+              [FieldName "value0"]
+          original =
+            mkUber $
+              let1
+                name
+                (application boxCtor (literalInt 1))
+                (dataArgumentByIndex 0 (refLocal name))
+          expected =
+            Linker.UberModule
+              { uberModuleForeigns = []
+              , uberModuleBindings = []
+              , uberModuleExports = [(Name "main", literalInt 1)]
+              }
+      annotateShow original
+      optimizedUberModule original === expected
+
+    -- The tag twin: a single-use scrutinee lets inlining bring the
+    -- constructor to the tag read, which folds to the tag string and
+    -- collapses the surrounding equality — the payoff cascade end to end.
+    test "constructor tag read after inlining" do
+      name ← forAll Gen.name
+      let uberName = moduleNameFromString "Main"
+          linkMode = LinkAsModule uberName
+          mkUber = Linker.makeUberModule linkMode . pure . wrapInModule
+          maybeTy = TyName "Maybe"
+          justName = CtorName "Just"
+          justCtor =
+            ctor SumType uberName maybeTy justName [FieldName "value0"]
+          tag = ctorId uberName maybeTy justName
+          original =
+            mkUber $
+              let1
+                name
+                (application justCtor (literalInt 1))
+                (eq (reflectCtor (refLocal name)) (literalString tag))
+          expected =
+            Linker.UberModule
+              { uberModuleForeigns = []
+              , uberModuleBindings = []
+              , uberModuleExports = [(Name "main", literalBool True)]
+              }
+      annotateShow original
+      optimizedUberModule original === expected
+
   describe "scoping invariants" do
     -- Mimics issue #37: an inlined binding contains a let with a
     -- reference bound by an earlier sibling; inlining it under a binder
@@ -831,6 +1009,20 @@ spec = describe "IR Optimizer" do
       -- The full pipeline ends GUC-clean, not merely well-scoped:
       lintUniqueBinders optimized === []
 
+    -- Soundness of a single bottom-up 'optimizedExpression' pass over
+    -- generated input — which, since the shared generator emits
+    -- 'ReflectCtor' / 'DataArgumentByIndex' over saturated constructor
+    -- applications, actually fires the #177 case-of-known-constructor fold.
+    prop "optimizedExpression stays sound over generated expressions" do
+      e ← forAll (uniquifyNamesInExpr <$> Gen.scopedExp)
+      let once = optimizedExpression e
+      -- Never introduces a free reference; may drop them (the #177 fold,
+      -- DCE, beta, and unreachable-branch removal all shrink the ref set),
+      -- so this is a subset check, not FloatIn's equality.
+      Map.isSubmapOfBy (<=) (countFreeRefs once) (countFreeRefs e) === True
+      -- Stays well-scoped.
+      unboundLocals once === []
+
 --------------------------------------------------------------------------------
 -- Helpers ---------------------------------------------------------------------
 
diff --git a/test/Language/PureScript/Backend/IR/Spec.hs b/test/Language/PureScript/Backend/IR/Spec.hs
index 0459421f..c1d7e4f4 100644
--- a/test/Language/PureScript/Backend/IR/Spec.hs
+++ b/test/Language/PureScript/Backend/IR/Spec.hs
@@ -479,7 +479,7 @@ spec = describe "IR representation" do
 
   describe "collectDataDeclarations" do
     it "classifies data types regardless of constructor order" do
-      let ctor tyName ctorName =
+      let cfnCtor tyName ctorName =
             Cfn.Constructor
               ann
               (PS.ProperName tyName)
@@ -492,9 +492,9 @@ spec = describe "IR representation" do
           cfnMod =
             cfnModule
               { Cfn.moduleBindings =
-                  [ bind "A" (ctor "T" "A")
-                  , bind "C" (ctor "U" "C")
-                  , bind "B" (ctor "T" "B")
+                  [ bind "A" (cfnCtor "T" "A")
+                  , bind "C" (cfnCtor "U" "C")
+                  , bind "B" (cfnCtor "T" "B")
                   ]
               }
       collectDataDeclarations (Map.singleton (PS.ModuleName "M") cfnMod)
diff --git a/test/Language/PureScript/Backend/Lua/Spec.hs b/test/Language/PureScript/Backend/Lua/Spec.hs
index a22a87cb..0e92f401 100644
--- a/test/Language/PureScript/Backend/Lua/Spec.hs
+++ b/test/Language/PureScript/Backend/Lua/Spec.hs
@@ -1,7 +1,6 @@
 module Language.PureScript.Backend.Lua.Spec where
 
 import Control.Monad.Oops (Variant)
-import Control.Monad.Trans.Except (ExceptT, runExceptT)
 import Data.Tagged (Tagged (..))
 import Data.Text qualified as Text
 import Language.PureScript.Backend.IR qualified as IR