Polymorphic Channels and the Send Bound

Two episodes made the concurrency type system nearly whole: the predicates decide whether a value may cross a thread, and the flow pass tracks whether it already has. But a review found one gap left, and it is not about flow — it is about types the inference has not yet pinned down. A channel carries values of some element type, and that type must be Send. Checking that is easy when the element type is concrete. It is not easy when the element type is still a variable.

The hole in the polymorphic case

The first version checked the Send requirement in exactly the places it obviously arises: where a channel’s element type is written in an annotation, and where a send operation is applied to concrete arguments. For any program using channels at specific types, that catches everything. But consider a small wrapper — a function that takes a channel and sends something down it, written generically over the element type. Here the element type is a type variable that inference may never resolve to anything concrete, and the first version, meeting an unresolved variable, optimistically waved it through.

That optimism is unsound. A generic channel wrapper is a hole you can pour anything into: check it once, and then instantiate it at a non-sendable type, and a value the design forbids from crossing a thread boundary crosses inside the wrapper, its Send obligation never actually discharged. The gap is small and easy to miss — which is exactly why a review, not a test, is what surfaced it, the same way the Send structural hole surfaced two episodes ago.

The textbook fix, and why not

There is a well-known, fully general answer to “a type variable that must satisfy a predicate”: qualified types, the trait-constraint machinery of languages like Haskell and Rust. You attach the Send requirement to the type variable as a constraint, carry it around, discharge it when the variable resolves, and — the expensive part — when a definition is generalized into a reusable polymorphic scheme, you record the leftover constraints on the scheme, so every later use re-checks them. It is the right answer in general, and it is what a mature type system with type classes does.

Mere’s type checker does not have it, and adopting it here would mean building it. Its schemes carry no constraints at all — a polymorphic type is just a type with quantified variables, with no attached obligations — and there is no constraint solver anywhere in the system. Adding qualified types means adding a solver, threading constraints through generalization and instantiation, and touching every part of inference. That is a large new subsystem, and it would change the character of a type checker that was deliberately kept solver-less. The situation is the exact shape of the higher-order-functions choice from the effect system: the sophisticated general answer exists, and taking it would contradict a decision the type system already made about how heavy it wants to be.

The cheaper rule: don’t generalize what still owes Send

So the bound is enforced without a solver, by a targeted rule. As inference runs, a Send obligation is pushed onto a pending list wherever a channel or parallel-map element type appears. At each point where a definition would be generalized — and at the end of a top-level declaration — a discharge pass walks the pending obligations. For a concrete type, it just checks Send and reports an error if it fails. For a type variable that is still unresolved and about to be generalized — which is precisely the polymorphic-channel case — it applies one rule: do not generalize it.

Refusing to generalize the variable is what closes the hole. A generalized variable is one that can be instantiated at many different types, and that is exactly the freedom the smuggling attack needs — check the wrapper once, reuse it at a non-sendable type. A variable that is not generalized cannot be reused at a second type; the binding becomes a monomorphic channel function whose element type is fixed by its first concrete use. The route that let a non-sendable value ride through is gone, because the polymorphism that enabled it is simply declined. If such a variable is never pinned down by any use, it surfaces as an explicit error — the channel’s element type is ambiguous, annotate it — rather than silently passing.

This is a monomorphism restriction: when a variable still carries an unmet obligation at generalization time, keep it monomorphic. Restricting polymorphism to preserve soundness is a well-trodden move — the value restriction in ML, the monomorphism restriction in Haskell are the same instinct — and it buys soundness without any of the machinery a constraint solver would demand. The whole concurrency type story stays what the type system always was: Hindley–Milner inference plus a handful of ad-hoc structural predicates — Trivial, cleanup-needing, and now Send and Sync — with no general solver anywhere.

What it costs, and what waits

The price is a specific, narrow loss of expressiveness: you cannot write a truly polymorphic channel combinator and reuse it, in one program, at several different element types. The trial that guided this judged that pattern rare, and the fully general answer — qualified types — is not abandoned but deferred, filed as a future question to be taken up if a real program ever needs that reuse. This is the recurring discipline once more: build the sound minimal thing now, keep the general answer on the shelf, and let genuine demand, discovered by use, decide whether to pay for it.

With this, the type-system half of concurrency is complete. The design was narrowed, the predicates made sound, moves tracked across the control flow, and the last polymorphic gap closed — all of it within a solver-less Hindley–Milner core, consistent with the language built five parts before. What remains is to make it actually run: to turn spawn and channels into real threads and real shared memory, and to do it four times, once per backend, without any two of them disagreeing. Next: running concurrency on four backends.