Pattern match capture bug: captured variables become unresolved dup variables when match arms diverge

[gavlooth]

Summary

When a lambda captures a variable and is passed to a function that uses pattern matching, the captured variable can become an unresolved dup variable if the subsequent evaluations take different pattern match arms.

Minimal Reproduction

@unwrap = λ&v. λ{#Cst: λ&n. n; _: λ&u_. 0}(v)

@eval = λ&k. λ&expr.
  λ{
    #Cst: λ&n. (k(#Cst{n}))
    #Wrap: λ&inner. (k(inner))
    #Add: λ&a. λ&b.
      @eval(λ&va.
        @eval(λ&vb.
          (k(#Cst{(@unwrap(va) + @unwrap(vb))}))
        )(b)
      )(a)
  }(expr)

// All 4 combinations of #Cst and #Wrap
@test_cc = @eval(λ&x. x)(#Add{#Cst{5}, #Cst{3}})         // Works
@test_cw = @eval(λ&x. x)(#Add{#Cst{5}, #Wrap{#Cst{3}}})  // FAILS
@test_wc = @eval(λ&x. x)(#Add{#Wrap{#Cst{5}}, #Cst{3}})  // FAILS
@test_ww = @eval(λ&x. x)(#Add{#Wrap{#Cst{5}}, #Wrap{#Cst{3}}})  // Works

@main = #CON{@test_cc, #CON{@test_cw, #CON{@test_wc, #CON{@test_ww, #NIL}}}}

Expected Output

[#Cst{8},#Cst{8},#Cst{8},#Cst{8}]

Actual Output

[#Cst{8},#Cst{(A₀ + 3)},#Cst{(B₀ + 3)},#Cst{8}]

Pattern

The bug occurs when:

1. The first operand (a) and second operand (b) take different pattern match arms
2. The captured variable va from evaluating the first operand is referenced in the continuation for the second operand

It works when both operands take the same arm (both #Cst or both #Wrap).

Analysis

Looking at the step-by-step trace (-D flag), the issue appears to stem from how DUP-LAM and APP-MAT-SUP interact:

1. The lambda λ&va. @eval(λ&vb. ...)(b) captures va
2. DUP-LAM duplicates this lambda, creating a SUP for the captured va
3. APP-MAT-SUP propagates the SUP through the pattern match
4. When the two branches take different match arms, the SUP elements diverge
5. The captured variable ends up as an unresolved dup variable

Use Case

This pattern is common in CPS-style evaluators and effect handlers, where captured values need to be threaded through pattern matching dispatch.

Workaround

Defunctionalize continuations to avoid capturing variables in lambdas - store values in data structures instead:

// Instead of:
@eval(λ&va. @eval(λ&vb. (va + vb))(b))(a)

// Use:
@eval(#KAdd1{k, b})(a)  // Continuation data with stored values

Questions

1. Is this expected behavior according to the interaction calculus semantics?
2. If it's a bug, is there a fix that doesn't break lazy evaluation guarantees?
3. If it's by design, should it be documented as a limitation?