From 77421e7f8c5419ec194e682f6a3450d8f0eb8bc9 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 16 Jun 2021 09:37:57 +0200
Subject: [PATCH 1/2] SpeC: Refine the opt rule
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

this writes the rules out as described in
https://github.com/dfinity/candid/pull/168#discussion_r609353518

I believe that this is necessary for completeness, as shown by this
table, which checks that `t <: opt t'` is covered:

```
| null <: t | null <: t' | t <: t' | Rule?
| --- | --- | --- | --- |
| no | no | no | second rule
| no | no | yes | first rule
| no | yes | no | third rule
| no | yes | yes | third rule
| yes | no | no | second rule
| yes | no | yes | impossible (<: is transitive)
| yes | yes | no | see rules for  `t = null`, `t = opt …` or `t = reserved`
| yes | yes | yes | see rules for  `t = null`, `t = opt …` or `t = reserved`
```

Remember that `null <: t` implies that `t = null`, `t = opt …` or `t =
reserved`, and these cases have their own rules.

Fixes #239.
---
 spec/Candid.md | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 72f0c4d3e..288cb7431 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -915,7 +915,7 @@ C[vec <t> <: vec <t'>]( vec { <v>;* } ) = vec { C[<t> <: <t'>](<v>);* }
 
 #### Options
 
-The null type coerces into any option type:
+The null type and the reserved type coerce into any option type:
 ```
 C[null <: opt <t>](null) = null
 ```
@@ -927,15 +927,20 @@ C[opt <t> <: opt <t'>](opt <v>) = opt C[<t> <: <t'>](v)  if <t> <: <t'>
 C[opt <t> <: opt <t'>](opt <v>) = null                   if not(<t> <: <t'>)
 ```
 
-NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation at runtime.
-
-Coercing a non-null, non-optional and non-reserved value at an option type treats it as an optional value:
+Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it has a suitable type:
 ```
 C[<t> <: opt <t'>](<v>) = opt C[<t> <: <t'>](v)  if not (null <: <t>) and <t> <: <t'>
-C[<t> <: opt <t'>](_)   = null                   if not (null <: <t>) and not (<t> <: <t'>)
-C[reserved <: opt <t'>](_) = null
 ```
 
+Any other type goes to `null`:
+```
+C[reserved <: opt <t>](_) = null
+C[<t> <: opt <t'>](_) = null  if not (null <: <t'>) and not (<t> <: <t'>)
+C[<t> <: opt <t'>](_) = null  if null <: <t'> and not (null <: <t>)
+```
+
+NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation at runtime.
+
 #### Records
 
 In the following rule:

From 36d30183ddfbce5b6f799806a009295d1595de3e Mon Sep 17 00:00:00 2001
From: Yan Chen <yan.chen@dfinity.org>
Date: Sun, 29 Aug 2021 13:24:47 -0700
Subject: [PATCH 2/2] null <: t'

---
 spec/Candid.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 288cb7431..29859d7e8 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -791,7 +791,7 @@ not (<datatype> <: opt <datatype'>)
 ---------------------------------
 opt <datatype> <: opt <datatype'>
 
-not (null <: <datatype>)
+not (null <: <datatype'>)
 not (<datatype> <: <datatype'>)
 ---------------------------------
 opt <datatype> <: opt <datatype'>
@@ -929,7 +929,7 @@ C[opt <t> <: opt <t'>](opt <v>) = null                   if not(<t> <: <t'>)
 
 Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it has a suitable type:
 ```
-C[<t> <: opt <t'>](<v>) = opt C[<t> <: <t'>](v)  if not (null <: <t>) and <t> <: <t'>
+C[<t> <: opt <t'>](<v>) = opt C[<t> <: <t'>](v)  if not (null <: <t'>) and <t> <: <t'>
 ```
 
 Any other type goes to `null`: