Multi-constructor `data` types break cross-module inference for callers using bound vars

[kumavis]

Summary

Adding a SECOND constructor to a data type in module M1 causes importing module M2 to fail elaboration with "Could not infer type" on multi-arg helpers that call a function returning that type — even though the same code works inside M1 itself, even though every relevant spec is concrete, and even with explicit type annotations on let bindings.

The defining module compiles fine. The failure is on the importing-module side, where 2+ bound function-arg variables cannot have their types propagated through a call that returns the multi-constructor type. Function-arg vars come back as <_> (uninferred metavars) in the elaborated form.

The full pitfall write-up is in docs/tracking/2026-04-27_GOBLIN_PITFALLS.md entry #32.

Repro skeleton

Inside module M1:

data Step
  step     : Vat -> State                  ;; ctor 1
  step-out : Vat -> State -> List String   ;; ctor 2

spec do-step Op Vat State -> Step
defn do-step | ... -> step v st           ;; or step-out v st bytes

Inside an importing module M2:

require [M1 :refer-all]

;; FAILS — "Could not infer type"
spec wrap Op Vat State -> Vat
defn wrap [op v st]
  let s := [do-step op v st]
    [step-vat s]

Real-world failure

Discovered in OCapN Phase 25 (handshake modelling, commit 4b92416). I extended BridgeStep with a second constructor bridge-step-out carrying immediate-outbound bytes:

data BridgeStep
  bridge-step     : Vat -> BridgeState                   ;; existing
  bridge-step-out : Vat -> BridgeState -> [List String]  ;; NEW

The defining module captp-bridge.prologos continued to compile cleanly — connection-step (which uses bridge-step-vat, bridge-step-state, bridge-step-immediate) was fine.

But the importing module bridge-interop-helpers.prologos failed to define EVERY multi-arg helper that called captp-incoming-with-state and unpacked the result. Failures persisted under:

• 1 let, 2 let, 3+ let chains
• Inline (no let)
• Explicit type annotation on the let binding (let s : BridgeStep := ...)
• Multi-arity defn syntax (| op v st ->) instead of bracket syntax ([op v st])
• Both bracket and bare-juxtaposition body shapes

Probe matrix

The probe matrix narrowed the trigger:

function shape	defines?
1-arg + let + captp-call (constants for other args)	yes
2-arg + let + captp-call (1 bound + 1 constant)	NO
3-arg + let + captp-call (3 bound)	NO
2-arg + INLINE + captp-call (all bound)	NO
Same shape, but BridgeStep has only 1 constructor	yes

So the trigger is: multi-constructor data type as the return type of an imported function whose call site has 2+ bound metavar args.

Hypothesis

The elaborator's bidirectional inference for function applications can't pin down the return type of a function returning a multi-constructor data type when the call's arguments include 2+ unsolved metavariables (function-arg vars whose types haven't been propagated from the spec yet). With a single-constructor return type, the constructor's signature uniquely determines the type, but with N constructors the elaborator may delay the choice in a way that fails to back-propagate through the let.

Workaround

Avoid multi-constructor data types when the constructor's primary use is "value with optional extra payload."

1. Single constructor with all fields. Add a [List X] or [Option X] field that's nil / none for the bare case. Trade-off: every accessor and update function gets an extra wildcard, but it's mechanical. This is what Phase 25 ended up using — pending-out : List String was added to BridgeState (single-constructor) instead of a second bridge-step-out constructor on BridgeStep.

2. Wrap the optional payload in a separate function. Instead of "constructor with X" + "constructor without X," have a single constructor + a separate accumulator (e.g. a list field or queue) that the producing function appends to.

The single-ctor workaround is uniformly applicable and clean. But it's a real expressivity gap — multi-constructor data types are fundamental.

Why filing this is worth it

1. Catastrophic failure mode: importing modules fail to compile. The error doesn't point to the data def — it points to the call site.
2. Far from surface cause: the data type definition is in a DIFFERENT module from where the failure surfaces. Diagnosis took ~1 hour of probing with shrinking test cases.
3. Workaround is invasive: moves what should be optional payload onto the parent type, with field plumbing through every accessor.
4. Fundamental expressivity gap: until fixed, the language can't easily express "this dispatch returns a value-with-or-without-extra-output" patterns naturally.

Cross-references

• Pitfall examples: EigenTrust on propagators via Racket FFI #32 in docs/tracking/2026-04-27_GOBLIN_PITFALLS.md
• Phase 25 commit that hit + worked around it: 4b92416
• Related (same elaborator subsystem, different trigger): Polymorphic partial application at def-binding site fails inference (let-generalization gap) #25 (polymorphic partial application at def-binding site fails inference), Improve error messages for common typo and inference-failure cases #27 (improve error messages for inference failures), pitfall Pattern-syntax asymmetry: [a] pattern doesn't match '[1] value (1-element list) #30 (match in deep let-chain triggers inference failure).

[kumavis]

Two more data points from Phase 25.4 of the OCapN questioner-side track (commit f633e5a). Both surfaced inside bridge-interop-helpers.prologos (importer of promise.prologos's PromiseState).

Data point #2: discriminating match on imported sum type

spec extract-fulfilled-value PromiseState -> [Option SyrupValue]
defn extract-fulfilled-value
  | pst-unresolved _ -> [none SyrupValue]
  | pst-fulfilled v  -> [some SyrupValue v]
  | pst-broken     _ -> [none SyrupValue]

Fails with Type mismatch ... could not infer. The body's elaborated form looks structurally fine:

[fn [x <PromiseState>] [reduce x | pst-unresolved y -> [none SyrupValue]
                                  | pst-fulfilled y  -> [some SyrupValue y]
                                  | pst-broken     y -> [none SyrupValue]]]

Surprising bit: a structurally-identical function with the SAME constructors but a non-Option return type works fine — unresolved? : PromiseState -> Bool (in the same promise.prologos defining module) compiles cleanly cross-module. So the trigger isn't "match on PromiseState" alone — it's "match on imported sum type AND construct an imported sum type return value".

Adding an explicit single-arg form defn extract-fulfilled-value [ps] (match ps ...) instead of the multi-arity defn made no difference. Annotating the let-binding type didn't help either.

Workaround: don't discriminate in-bridge. Return Option PromiseState directly and let the test fixture pattern-match on the pretty-print externally.

Data point #3: 4-arg helper calling captp-incoming-with-state with bound args

spec drive-and-lookup CapTPOp Vat BridgeState Nat -> [Option PromiseState]
defn drive-and-lookup [op v st pid]
  let step := [captp-incoming-with-state op v st]
    [lookup-promise pid [bridge-step-vat step]]

Fails. Same pattern as the original report (4 bound args, captp-incoming-with-state call with all bound, let-binding the result). The probe matrix from the original report applies unchanged: the cross-module inference failure is robust regardless of let depth, type annotation, or single-vs-multi-arity defn.

Workaround: 2-arg shape that takes BridgeStep directly, sidestepping the CapTPOp Vat BridgeState triple at the call site:

spec lookup-after-step BridgeStep Nat -> [Option PromiseState]
defn lookup-after-step [step pid]
  lookup-promise pid [bridge-step-vat step]

Then the caller passes [captp-incoming-with-state op v st] as the BridgeStep. Same trick used for drive-after-step1 in Phase 25 (commit b2b4a80).

Additional observations

Type-name aliasing trip-up: when working around data point #3, I initially got a different error — the spec's unqualified PromiseState came back as type-mismatched against the body's fully-qualified prologos::ocapn::promise::PromiseState. Both names refer to the same type, but the elaborator sees them as distinct. Fixed by adding an explicit [prologos::ocapn::promise :refer [PromiseState pst-unresolved pst-fulfilled pst-broken]] import even though :refer-all on captp-bridge should transitively re-export it.

This may be a separate pitfall worth filing — the :refer-all chain semantics differ from explicit :refer [Name] for type-equality purposes — but I'd want to confirm with another data point before splitting it out.

Frequency

Phase 25 needed the workaround four times in one track:

1. BridgeStep second-constructor attempt (originally fixed by reverting to single-constructor + pending-out field on BridgeState — commit 4b92416)
2. drive-after-step1 (Phase 25 earlier) — 2-arg workaround
3. extract-fulfilled-value (this comment)
4. drive-and-lookup (this comment)

The pattern's frequency in real protocol-bridge code suggests a fix would unblock substantial downstream work. Every protocol port (CapTP responder, CapTP questioner, future OCapN locator/listener implementations) hits the multi-arg-helper-around-imported-sum-type pattern.

---

Generated by Claude Code