Plan: Fix ephemeral type argument soundness hole (#1931)

[SeanTAllen]

Issue #1931 has been open for nearly nine years. It describes a soundness hole in how ephemeral types interact with generic constraints. I've been digging into it and have a concrete plan for fixing it. This discussion lays out the analysis, the proposed approach, and the places where I'd like input from the community.

The Bug

Ephemeral types like iso^ and trn^ can be used as type arguments for generic types even when the constraint doesn't account for ephemerality. This lets you violate isolation guarantees. Here's the simplest demonstration:

interface Default
    new default()

class A
    new default() => None

class Cell[X: Default #any]
    var x: X
    new create() =>
        this.x = recover X.default() end

actor Main
    new create(env: Env) =>
        let cell : Cell[A iso^] = Cell[A iso^].create()
        let x : A iso = cell.x   // alias 1
        let y : A iso = cell.x   // alias 2

Both x and y are A iso references to the same object. That's two iso aliases, which is exactly what the capability system is supposed to prevent. This compiles and runs on the current compiler.

There's a second variant that doesn't even need #any. Unconstrained type parameters get desugared to X: X (a self-referential constraint), which trivially satisfies itself when the type argument is reified into it. So class Cell[X] with Cell[A iso^] also compiles and runs.

Root Causes

The constraint checking function is_cap_sub_cap_constraint() in cap.c has a shortcut at line 181: if((sub == super) || (super == TK_CAP_ANY)) return true. This accepts any capability against #any without checking the ephemeral flag. The function already checks one direction (if the constraint is ephemeral, the argument must be too) but never checks the reverse: if the argument is ephemeral, should the constraint be too?

The self-referential default makes it worse. sugar_typeparam() desugars unconstrained X to X: X. When you instantiate Cell[A iso^], the constraint gets reified to A iso^, and the check becomes is_subtype_constraint(A iso^, A iso^) which trivially passes.

There's also a shortcut in check_constraints (reify.c line 429) that skips constraint checking entirely when the type argument is a TYPEPARAMREF pointing to the same type parameter. This means Cell[X^] inside Cell's own body bypasses the constraint check too. That shortcut needs to be restricted to non-ephemeral cases.

Why You Can't Just Reject Ephemeral Type Arguments

The obvious fix — reject ephemeral capabilities against non-ephemeral constraints — breaks the stdlib. Ephemeral type arguments are used everywhere, and for good reason. Iterator[A^] appears in Seq's append and concat, in Array, List, Map, Set, in PonyCheck's generators, in FileLines, in itertools. These are safe uses because Iterator's type parameter only appears in output position. The unsound uses are specifically when the type parameter ends up in a stored field.

So the fix needs two things: make constraint checking actually enforce ephemerality, and give types a way to opt into accepting ephemeral type arguments.

Proposed Approach

This draws on the sync call discussion from 2017 in the original issue. The idea: #any stays as it is (stable capabilities only), and #any^ in constraint position means "stable and ephemeral." The user-facing syntax is familiar. The complexity lives in the compiler.

Internally, two new cap tokens represent the expanded sets:

Token	Set	Source
TK_CAP_ANY	{iso, trn, ref, val, box, tag}	#any
TK_CAP_ANY_ALL	{iso^, iso, trn^, trn, ref, val, box, tag}	#any^ in constraint
TK_CAP_SEND	{iso, val, tag}	#send
TK_CAP_SEND_ALL	{iso^, iso, val, tag}	#send^ in constraint

Only #any and #send need the ALL variants. The other gencaps (#read, #share, #alias) don't because cap_aliasing strips the ephemeral flag for all caps in those sets. ref^ is just ref, val^ is just val, and so on.

The sugar pass converts source #any^ on a constraint to TK_CAP_ANY_ALL + TK_NONE (and likewise for #send^). The parser doesn't change. No new user-facing syntax. Per Pony's philosophy: "It is more important for the interface to be simple than the implementation."

The Fix, Step by Step

Default constraint: Change unconstrained X from X: X to X: Any #any. This makes the safe choice the default. Explicit self-referential constraints (class Cell[X: X]) get detected after name resolution and replaced with the default.

Constraint checking: Add an ephemeral guard to is_cap_sub_cap_constraint — if the argument is ephemeral and the constraint is not, reject it unless the constraint is an ALL variant. Fix the check_constraints shortcut so X^ doesn't bypass constraint checking when forwarded as a type argument.

Stdlib updates: Types that need to accept ephemeral type arguments get #any^ on their constraints. The primary targets are Iterator, ReadElement, and the PonyCheck generator types. Collection types that store their type parameter in fields (Array, List, Map, Set, Seq, Heap) keep the default #any. Their methods using Iterator[A^] still work because A^ where A has #any constraint produces a type satisfying Iterator's #any^ constraint.

Compiler plumbing: The new tokens need handling across the capability infrastructure. cap_aliasing (ALL aliases to its base: #any_all aliased is #any, not #alias), viewpoint reification (ANY_ALL expands to all 8 members including iso^ and trn^), alias functions, compatibility checks, union/intersection constraint computation. About a dozen compiler files touched, mostly adding the new tokens alongside their base variants in switch statements.

Breaking Change

Code that passes ephemeral type arguments to generics with non-ephemeral constraints will fail to compile. The migration is straightforward: add ^ to the constraint. #any becomes #any^.

What I'd Like Input On

1. Does #any^ in constraint position feel right as the syntax? The 2017 discussion floated #any* as an alternative, but #any^ avoids introducing new syntax and ^ already means "ephemeral" to Pony users.

2. The default constraint changes from self-referential X: X to X: Any #any. This means unconstrained type parameters reject ephemeral type arguments by default. The rationale is safety: if your type stores the parameter in a field, ephemeral instantiation is unsound. Types that handle ephemerals safely (iterators, generators) opt in with #any^.

3. Anything I'm missing? I spent hours going around with Claude on this (Claude is remarkably good at type system stuff). This analysis went through three rounds of review with Claude beating on it, but nine years of open issue suggests there might be subtleties I haven't caught.

[jasoncarr0]

1. I think the surprising behavior with #any^ is that includes {iso}
2. [numbering]
3. That cap_aliasing rule isn't sound! Since it might be instantiated with iso and thus need to become tag
   The issue is possibly in part that aliasing is not idempotent (iso^ -> iso -> tag), but I don't think there's a fix here without changing the type system presentation so that moving/consuming is the identity, instead of what it is currently which is "borrowing" so to speak. This could also be a failure mode for Claude since the aliasing in Pony is very non-standard compared to move semantics.

Also a few edge cases with intersections that can give caps that are technically sound for expressions but are not "stable" and can't be the type of a variable, like (A ref & A val), which again might be hidden behind indirections, and this ought not match against #any

In any case, there should be a predicate already in the caps file for checking stability which is soundness to be a field.

[jasoncarr0]

Actually, I'm not certain whether it's sound without knowing how exactly it's used. Generics are always a big muddy, and so I suppose #any is weaker than #alias, so maybe it is okay

[SeanTAllen]

The #any^ set in the proposal is {iso^, iso, trn^, trn, ref, val, box, tag} — all 8 forms. Lietar 2017 defines #any^ as {iso^, trn^, ref, val, box, tag} — 6 forms, replacing iso/trn with their ephemerals rather than adding them.

The expanded set is necessary. If Iterator has Lietar's #any^ as its constraint and someone writes Iterator[A] where A: #any, then when A = iso the constraint check fails — plain iso isn't in {iso^, trn^, ref, val, box, tag}. The constraint needs to accept both ephemeral forms (from A^ where A: #any) and non-ephemeral forms (from plain A), so it has to be the union of #any and #any^.

Same applies to #send^ — Lietar has {iso^, val, tag}, the proposal needs {iso^, iso, val, tag}.

Worth noting this divergence explicitly in the discussion so it's clear this is an intentional extension of the paper's definition, not a restatement of it.

[SeanTAllen]

On the +#any_all = #any soundness concern @jasoncarr0 raised:

#any on +X is a derived upper bound, not an operational claim that +X could be iso. Partial reification checks each concrete instantiation exhaustively (Lietar §3.3) — when X = iso, the compiler verifies that +X = tag works in every position where +X is used; when X = iso^, it verifies that +X = iso works. No instantiation can "see" the wrong aliased capability.

The aliasing chain also holds through a second alias: +#any_all = #any, then +#any = #alias = {ref, val, box, tag}. Each step checks out against the aliasing table, and partial reification ensures the concrete capability at each instantiation is used for type checking, not the constraint bound.

[SeanTAllen]

Open question: does the compiler already reject ephemeral capabilities as field types? If it does, then class Foo[X: #any^] with var x: X where X = iso^ is already caught — the field type iso^ ("zero stable aliases") contradicts the field being a stable alias. If it doesn't, that's a second soundness hole that needs fixing alongside the constraint check.

I believe it does, but I'll confirm.

[SeanTAllen]

It doesn't.

The compiler rejects assignment to fields with direct iso^ or trn^ types, but there is no syntax-level or type-declaration-level check. The rejection happens indirectly in consume_type() (alias.c:205-213): when processing the assignment, consume_type tries to make the field type ephemeral. Since iso^ is already ephemeral, this would produce iso^^ (double-ephemeral).

For iso and trn, consume_single returns NULL, which triggers the "Invalid type for field of assignment" error in operator.c:390-401.

For ref^, val^, box^, tag^ — the compiler accepts them because ^ on those capabilities aliases to the base capability (they're already sendable/shareable), so consume_type succeeds.

[SeanTAllen]

I asked some claude's in a loop to evaluate what it would mean to add this (which I think is a good check to have)

1. The check must be recursive — walk into tuples, unions, intersections, arrow types (right-hand side), and TYPEPARAMREF nodes. An
   ephemeral anywhere in the field's type structure is problematic.
2. Lambda types: check the outer ephemeral modifier but do NOT recurse into parameter/return types (those describe the function
   signature, not what's stored).
3. Must run after type alias expansion — otherwise type Foo is A iso^ then var x: Foo bypasses it.
4. A post-reification field check is worth considering as a backstop for the constraint fix. Given this bug has been open nine years
   across multiple interacting compiler paths, cheap insurance against an incomplete constraint fix is valuable.

[SeanTAllen]

@jasoncarr0's point about intersection types is a gap in the proposal. (A ref & A val) can produce capabilities that are technically sound for expressions but aren't stable and shouldn't satisfy #any in constraint checking. Same class of problem as the ephemeral one — a capability slipping through constraint checking that shouldn't be a valid type argument for stored fields.

The proposal needs to address this: either a section on how intersection types interact with the new constraint checking, or an explicit scoping-out with reasoning. I'll look into this and come back with more.

[SeanTAllen]

I'm going to point some Claude's at this. I've trained claude with a lot of materials and techniques to be pretty darn good at this.

[SeanTAllen]

I dug into how intersection types interact with constraint checking. The short version: intersections as type arguments are a pre-existing type system gap, but they're not a soundness hole and they don't affect the #any^ proposal. Here's the long version.

How intersections flow through constraint checking

When the compiler checks (T1 & T2) <: Constraint, is_isect_sub_x in subtype.c asks: does ANY element of the intersection satisfy the constraint? So Cell[(A ref & A val)] with constraint #any passes because A ref satisfies #any. The check is lenient in the "sub is intersection" direction.

Incompatible intersections are uninhabited

ref and val are not compatible in is_cap_compat_cap (ref means local read-write aliases exist, val means nobody can write, ever). No value can satisfy both simultaneously. Same for ref & iso, ref & trn, val & iso, val & trn, iso & trn.

These pass constraint checking but you can never construct a value of the type. Empirically on 0.61.0:

• Cell[(A ref & A val)].create(A) — constraint check passes, then fails with "parameter type is illegal" because the reified parameter type (A ref & A val) can't accept any value.
• Cell[(B ref & B val)] with a X.default() constructor — constraint check passes, codegen proceeds, compiler crashes (segfault in LLVM during the Functions phase). The compiler can't resolve constructor dispatch on an intersection type.

You can't exploit what you can't construct. The "parameter type is illegal" error and the codegen crash both prevent you from ever getting a value of an uninhabited intersection type into a field.

I also checked whether values could be fabricated through FFI. FFI functions return concrete types with specific capabilities, not intersection types. You'd have to explicitly lie about the return type, which is the general FFI "trust the programmer" boundary, not an intersection-specific concern.

Compatible intersections are safe

The compatible pairs all have a "stronger" cap that subsumes the "weaker":

• iso & tag ≡ iso
• trn & box ≡ trn
• ref & box ≡ ref
• val & box ≡ val

These work fine as type arguments. Viewpoint adaptation handles them correctly:

• box->(iso & tag) = (tag & tag) = tag — safe, freely aliasable
• box->(trn & box) = (box & box) = box — safe
• ref->(trn & box) = (box & box) = box — safe

I also checked the iso receiver case, since iso->(trn & box) = (trn & val) produces an incompatible intersection through viewpoint adaptation. But to read through an iso receiver you'd consume the iso. The resulting (A trn & A val) is uninhabited — you can't assign it to anything. Useless but not unsound.

Verified empirically: Cell[(A iso & A tag)].create(recover A end) compiles and runs. Reading the field gives tag. Reading twice gives two tag references. Sound.

cap_isect_constraint has bugs but they don't affect soundness

cap_isect_constraint in typeparam.c is the function that computes the effective capability when a type parameter is constrained by an intersection. It has two bugs:

1. Wrong fallback: cap_isect_constraint(TK_REF, TK_VAL) returns TK_CAP_ANY because the pair isn't handled. The intersection of {ref} and {val} should be empty.

2. Missing break: At line 266, the TK_CAP_SHARE case falls through into TK_CAP_ALIAS. This produces specific wrong answers — cap_isect_constraint(TK_CAP_SHARE, TK_REF) returns TK_REF (via the TK_CAP_ALIAS handler) when it should return empty (ref is not in {val, tag}).

Neither bug affects soundness. I traced every caller of cap_isect_constraint (via cap_from_constraint → typeparam_set_cap):

• flatten.c: Syntactic validation only (checking explicit cap annotation matches computed constraint cap).
• subtype.c is_fun_sub_fun: Synthesizes a typearg for method reification, then runs full is_reified_fun_sub_fun().
• subtype.c is_typeparam_sub_x: Computes upper bound, then passes it to is_x_sub_x() which calls is_x_sub_isect() for intersections.
• matchtype.c (two call sites): Computes bounds for pattern matching, then runs full is_x_match_x().

Every caller feeds the result into further validation. The wrong capability from cap_isect_constraint never makes a soundness-critical decision on its own.

Nested generics re-check constraints

I verified that constraints are checked at each level of generic nesting. Wrapper[T: Any #any] with var inner: Cell[T] where Cell requires MyIface #any is correctly rejected — the compiler checks T's constraint against Cell's constraint.

The check_constraints shortcut at reify.c:429 only fires when the typearg is a TYPEPARAMREF pointing to the same type parameter definition (i.e., Cell[X] inside Cell's own body). It does not fire for cross-generic forwarding.

#any^/#send^ don't change the intersection story

Ephemeral intersections either reduce to the ephemeral field problem or are uninhabited:

• (A iso^ & A tag): iso^ is a subtype of tag, so this is inhabited and equivalent to A iso^. That's the ephemeral field type problem, handled by the constraint check fix and the field-level ephemeral rejection.
• (A iso^ & A iso): No value is simultaneously iso^ and plain iso in the same reference position. Uninhabited.
• (A trn^ & A box): Equivalent to A trn^. Same ephemeral field problem.

No new soundness issues from the intersection of ephemeral caps with #any^.

Generic cap constraint intersections

For completeness, each constraint group:

Constraint	Possible intersections	Result
#read = {ref, val, box}	ref & val: incompatible. ref & box ≡ ref. val & box ≡ val.	Safe
#send = {iso, val, tag}	iso & val: incompatible. iso & tag ≡ iso. val & tag ≡ val.	Safe
#share = {val, tag}	val & tag ≡ val.	Safe
#alias = {ref, val, box, tag}	ref & val: incompatible. ref & box ≡ ref. val & box ≡ val. box & tag ≡ box. ref & tag ≡ ref. val & tag ≡ val.	Safe

Recommendation

Intersection types as type arguments are a pre-existing gap. The compiler accepts type arguments it shouldn't (uninhabited intersections), and cap_isect_constraint has bugs. But none of this is exploitable for unsound behavior, and none of it is introduced or worsened by the #any^ proposal.

The proposal should note the gap and move on. The cap_isect_constraint bugs and the codegen crash for intersection type arguments should be filed as separate issues.

[jasoncarr0]

FWIW this is technically a little bit off, but correct that it's rejected by the compiler.
Incompatible intersections can be inhabited, in that there is a value which can typecheck as both sides (for instance anything iso^ or trn^ checks as both ref and val), and they are also sound, in that you effectively have to choose a side, and they are already rejected as parameters where they are equivalent to ephemeral types.

I recall I left in the option to disallow them entirely the last time I touched that system, if need be.
https://playground.ponylang.io/?gist=0475e62dcc425eb2db07bd217455d14f

(And actually iso->(trn & box) = (trn & val) is demonstrative, but that's also why incompatible intersections should be allowed, so you don't get a random type-error for just accidentally expressing a type you don't necessarily need)

The only reason it's affected by this proposal is that we might have for instance: [T1 #any, T2 #any] and (T1 & T2) but in retrospect the only way you could actually fill that type anyway is that you'd have to be getting a T1&T2 from some argument, so there's no real risk.

[jasoncarr0]

Which is to say that it should just be a test case:
C[T1 #any, T2 #any]
shouldn't be able to have a field or a var of type (T1 & T2)

[jasoncarr0]

Ah or sorry the more correct one is that T1 & T2 should not be valid for T #any