From 5bd279c972edb14b66278c97a6d4b904fed6c2e4 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 4 Nov 2020 10:34:35 +0100
Subject: [PATCH] More decoding: reserved ~> null : opt _
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

I won’t believe in this system until we have a formal proof… anyways,
still finding holes.

Imagine the sender evolves as follows:
```
record {} <: record { foo : reserved }
```
and the receiver evolves (using fancy new opt field rules) as follows:
```
record {} :> record { foo : opt bool }
```

Both are allowed, so decoding must not fail. One way to fix that is to
add
```
(null : reserved) ~> null : opt <t>
```
to the rules.
---
 spec/Candid.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index e54267556..1322159ef 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -944,11 +944,14 @@ An optional value coerces at an option type, if the constituent value coerces at
 opt <v> ~> opt <v'> : opt <t>
 ```
 
-If an optional value _fails_ to coerce at an optional type, the result is `null`, not failure:
+If an optional value _fails_ to coerce at an optional type, or the value is `reserved`, the result is `null`, not failure:
 ```
 not (<v> ~> _ : <t>)
 -------------------------
 opt <v> ~> null : opt <t>
+
+-----------------------------------
+(null : reserved) ~> null : opt <t>
 ```
 
 Coercing a non-null, non-optional and non-reserved value at an option type treats it as an optional value: