`:refer-all` chains don't establish type identity for spec-level type-name resolution

[kumavis]

Summary

When module M3 imports M2 with :refer-all, and M2 imports M1 with :refer-all, and M1 defines a type T, M3 can use T in function specs and bodies via the transitive chain. But the elaborator treats the spec's unqualified T and a body expression's fully-qualified prologos::M1::T (e.g. from a function call returning T) as DIFFERENT types — same definition, different name resolution path.

The fix is to add an explicit :refer [T] in M3 even though :refer-all transitively re-exports it. Specs and bodies then both resolve T to the same fully-qualified name.

Pitfall write-up at docs/tracking/2026-04-27_GOBLIN_PITFALLS.md entry #33.

Repro

In OCapN Phase 25.4 (commit f633e5a):

• prologos::ocapn::promise defines PromiseState
• prologos::ocapn::vat defines lookup-promise : Nat Vat -> Option PromiseState (imports promise via :refer-all)
• prologos::ocapn::captp-bridge does require [prologos::ocapn::promise :refer-all] AND require [prologos::ocapn::vat :refer-all]
• prologos::ocapn::bridge-interop-helpers does require [prologos::ocapn::captp-bridge :refer-all] (transitive chain to promise)

The failing function in bridge-interop-helpers.prologos:

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

Elaborator output:

Type mismatch
  expected: [Pi [x BridgeStep] [Pi [y Nat] [Option PromiseState]]]
  got:      [Pi [x BridgeStep] [Pi [y Nat]
              [Option prologos::ocapn::promise::PromiseState]]]

The spec's [Option PromiseState] resolves PromiseState via the :refer-all chain — but apparently NOT to the same fully-qualified binding as the body's lookup-promise return type. The elaborator's type-equality check is name-based and fails.

Workaround

Add an explicit :refer [PromiseState ...] to bridge-interop-helpers:

require [prologos::ocapn::promise
         :refer [PromiseState pst-unresolved pst-fulfilled pst-broken]]

After this, the spec's PromiseState resolves to the fully-qualified name and matches the body's. Function compiles cleanly.

Hypothesis

The :refer-all import re-exports terms but doesn't re-establish bindings in the importing module's "type-name resolution table" used by the spec parser. Specs are processed earlier than function bodies and may use a different name-lookup scope. The transitive case (M1 :refer-all chained through M2 :refer-all) compounds the issue: M3's spec parser doesn't see T as a known type until an explicit :refer [T] is added.

Why it's worth filing

1. Confusing error message: "Type mismatch [Pi T] vs [Pi qualified::T]" looks like a tautology at first glance. The qualifier is the only difference.
2. :refer-all chains are common in Prologos library modules — every multi-module library hits this when the chain crosses 2+ modules.
3. Fix would make :refer-all behave as users expect — the term-vs-type asymmetry is surprising.

Frequency

Hit once in OCapN Phase 25.4 (during the workaround for #60). Will likely hit more often as protocol bridges and other library modules grow chains of :refer-all. Lower impact than #60 (the workaround is one line) but worth fixing.

Cross-references

• Pitfall ffi: marshal Posit8/16/32/64, Int, and List across the Racket FFI #33 in docs/tracking/2026-04-27_GOBLIN_PITFALLS.md
• Discovered alongside Multi-constructor data types break cross-module inference for callers using bound vars #60 (multi-constructor cross-module inference); the two issues are independent — different mechanism, different fix.
• Fix commit using the workaround: f633e5a (added explicit refer line to bridge-interop-helpers.prologos)