A host can be destroyed while a guest names it: §2.8.1's two fates are not exhaustive

[TheLazyCat00]

Split out from the discussion on #153. That issue and #160 close the relocation axis — a value can no longer be raised above what its guests name. This is the other axis, untouched by either: a host can simply die while a guest is still on it, with nothing moving.

The defect

memory.md §2.8.1 enumerates what can happen to a hosted object once a guest names it:

The object is moved … The object is destroyed by an overwrite of the slot it lived in … The two cases never compete, because an object cannot both leave and die in the same step.

That is true and it is not exhaustive. Both listed fates leave the guest somewhere to land — a move carries the object, an overwrite leaves a successor occupant in the same slot. There is a third fate that leaves nothing, and the section has no answer for it.

Route A — container element removal

players List<Player>                  // Player has a `weapon Weapon` field
weapon &Weapon = players[100].weapon  // §2.8: field access on a place — a guest source
players!remove(Int(100))              // player 100 destroyed, its weapon with it
weapon:damage()                       // dangling

Every rule passes. weapon is an ordinary & local, so §1.10 does not apply; players outlives weapon, so §1.1 is satisfied and stays satisfied; nothing moves, so §1.4 and §1.11 never fire.

Note the mint is not blocked by the [] exclusion. §2.8 refuses players[100] itself as a guest source, but players[100].weapon is a field access whose base is a place, which the same section admits.

Part of why this went unnoticed: container removal is not specified anywhere in spec/. There is no rule saying what becomes of an element that leaves a container, so there is currently nothing for §2.8.1 to contradict.

Route B — a #variant case change

e Expr.flip(...)      // some guest names the flip payload
e = Expr.intLit("0")  // the flip payload is destroyed; no successor occupant

A struct field overwrite keeps the slot's identity and carries guests to the replacement. A case change destroys the payload slot itself, so there is no replacement of the same kind to carry forward to. Whether this is reachable depends on something §2.8 does not say: adt.md §3 makes a variant member read an abortable access, but nothing states whether such a read counts as "a field access whose base is a place" for guest-source purposes. Given the struct/variant symmetry adt.md §3.1 leans on, it probably does.

Candidate fixes

For route A — exclude [] from a guest source's whole path, not just its last step. Today the ban is on players[100]; extend it so no guest source may have a [] anywhere in its base chain, which kills players[100].weapon at the mint.

This was raised and argued against earlier in the #153 discussion, on the grounds that [] is not a containment boundary: a method on the element type mints this.weapon with no subscript in sight, so the ban would cost the legal cases and stop nothing. That objection is no longer live. With §1.10 (#160) in place, a guest minted through this inside an element can only be stored into this-rooted storage — the element's own tree — where it dies with the element. The route that defeated the ban is closed by a rule that has since landed.

Alternative for route A — removal relays rather than destroys. Make removal the inverse of append: a move out of the container. Then the third fate collapses into the first, which §2.8.1 already specifies — the object moved, and guests follow it.

p Player = players!remove(Int(100))   // bound: the caller hosts the player
players!remove(Int(100))              // unbound: floats (§1.9)

One refinement is needed for the unbound case: §1.9 floats a result to the statement's enclosing scope, which is not enough —

weapon &Weapon = players[100].weapon
{ players!remove(Int(100)) }   // floats into this block, dies at the brace
weapon:damage()                // dangling again

— so a removed element must float to the container's host scope. That is sound on an argument already in the spec: §1.1 guaranteed the container's scope is at or above every guest minted through it, so the removed element outlives all of them. The bound form needs no new rule, since treating the container as the source host makes §1.4 forbid sinking it into a lower scope.

The two are not exclusive. The relay answer also settles what remove means, which is unspecified either way.

Route B needs its own answer. An assignment has no return path, so nothing can be relayed out of a case change. The likelier shape is a source restriction: a guest may be minted only from a permanent slot. A struct field is permanent — everything that can happen to it is one of §2.8.1's two existing fates. A container index and a variant case are contingent: which object is at index 100, and whether the flip case is live at all, change without any move or overwrite. Stated that way it covers both routes and gives the existing [] ban the reason it currently lacks (§2.8's present justification — "those stored guests are stable because the language does not let [] mint guests from host storage in the first place" — is circular).

Relationship to other issues

• Moving an object that holds a guest can raise it above the guest's target #153 / docs(lifetimes): one owner comparison in place of the raise enumeration #160 — the relocation axis. Closed there, and no rule in that change reaches this one. §1.10's guarantee is explicitly scoped to relocation for this reason.
• Forwarding anchors, guest sources, and what a moved-from symbol becomes #152 — independent. That issue is about two live anchor identities resolving to one payload after a move with anchored objects on both sides; this is about a host dying under a guest with no move at all.