destructors: nothing moves out of a value with a drop: pop on an array with a drop, or on an array field of a value with a drop, is error: a: can't move out of a value with drop (fields were already borrowed projections); spec 6.15.5, four conformance programs

1 files changed, 1 insertions, 0 deletions

diff --git a/docs/SPEC.md b/docs/SPEC.md
index 8c2f5dc..dc4934a 100644
--- a/docs/SPEC.md
+++ b/docs/SPEC.md
@@ -997,6 +997,7 @@ let guard = drop(heap(0), fn() { unlock(); });                            // unl
 6.15.2 a value dies, and its drop runs, where 6.5 frees it: at the end of its owner's block or an early exit, at `rt.free`, when its owner is reassigned (6.8.5), or with its container, whose drop runs before its children's. a new value assigned to the owner can have its own drop set on the next statement, like a declaration's. a value with a drop that nothing holds (a temporary) dies at the end of its full statement, with hint: value with drop is never bound; it drops at the end of this statement. an owned local with a drop is not "never used" (6.5.2): holding it is its use.
 6.15.3 the collector runs the drop of an unreachable value after its sweep, never during it, and at most once: the value is kept until a later collection finds it unreachable again. a drop that stores `this` somewhere reachable keeps the value alive, and its drop does not run again. there is no collection at exit, so collector-owned values are not dropped then. a freed block forgets its drop, so a block reused at the same address has none.
 6.15.4 copying a value with a drop into an actor message is error: x: has drop and can't be copied into a message.
+6.15.5 nothing moves out of a value with a drop, whose drop may need what it holds. a field or element of it is a borrowed projection and can't be given away (error: a borrowed projection cannot transfer ownership; transfer its owner), and `pop` on an array that has a drop, or on an array field of a value with a drop, is error: a: can't move out of a value with drop. there is no `take`. borrowing a child is fine, and an array without a drop hands out its elements with `pop` as before, drops and all.
 
 ## 7. compile-time execution