Closes #214. Builds on #213 (now on main).

What

reduceKnownConstructor (#177) only fires on a constructor that is syntactically in place, and a scrutinee read more than once is never in place. Beta reduction Let-binds a non-trivial argument rather than substitute it into every occurrence (the #167 discipline), and a dictionary method reads its scrutinee several times: a tag test, a payload read, a fallthrough tag test. So an inlined and beta-reduced method lands on

let v = Just (x + 1) in
  if justTag == ReflectCtor v then … v.value0 …
  else if nothingTag == ReflectCtor v then Nothing else …

and nothing folds. The rules see ReflectCtor (Ref v) and ObjectProp (Ref v) "value0", never the constructor, so the whole match stays opaque behind the Let. That is a near-zero win for exactly the multiply-read-scrutinee methods (bind, apply), which are most of them.

How

propagateKnownCtorThroughLet propagates a known constructor from a Standalone Let binding into the binder's reads. When the RHS is a saturated Ctor application and the binder is read only through constructor-eliminating reads:

• each ReflectCtor v folds to the tag string (sum types only, as in reduceKnownConstructor);
• each field read (ObjectProp v "valueᵢ", DataArgumentByIndex i v) folds to a fresh field-binder bound once to the iᵗʰ argument, GHC's case-binder to field-binder split, so a non-trivial argument read at several sites is evaluated once rather than copied to each site;
• the binding is dropped, its unread arguments discarded with the same licence reduceKnownConstructor has for a field read's siblings.

Trivial and dead field-binders then inline or DCE away, and with the reads folded the surrounding Eq/if meets constant folding and the unreachable-branch rules, collapsing the decision tree to its live arm. That is the case-of-known-constructor payoff of #177, now reached through the Let.

The rule declines when the binder is read as a whole value anywhere (a sibling binding, or a non-eliminating position such as an argument to a function): dropping it would dangle the reference, and keeping it while binding the fields would duplicate the arguments. A product-type ReflectCtor read has no tag row to fold to, so it too leaves a whole-value read and the rule declines. It also guards against a self-referencing RHS, which cannot arise under the global uniqueness condition but can on the non-GUC input optimizedExpression is exercised on directly.

Why now

This is the enabler that makes dictionary-method inlining (#180) pay off. Once #180 inlines a method and beta reduction Let-binds the dictionary value, the payload is read through exactly this Let-bound shape; without this rule #180 would inline the method but leave the match opaque. #180 stacks on this branch.

Verification

New optimizer specs cover the fold and its refusals: the tag fold unlocking the live branch, the payload dropped when only the tag is read, a field read at several sites bound once (proving no duplication), the whole-value and partial-application declines, and an end-to-end collapse to straight-line code run through the checked pipeline so a GUC or scoping violation would fail rather than pass silently. A randomized property stresses the fold across scalar payloads, checking the binder is eliminated and the free-reference multiset never grows.

Full suite green (cabal test all): 702 examples, 0 failures, and the IR optimizer specs stay green across several seeds. No structural golden moved and no eval oracle moved, matching the near-zero standalone impact the issue predicts, since the shape appears once method inlining lands. fourmolu and hlint clean, warning-free build.