Spec: Refine the opt rule (dfinity#246)

* SpeC: Refine the opt rule

this writes the rules out as described in
dfinity#168 (comment)

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 dfinity#239.

* null <: t'

Co-authored-by: Yan Chen <yan.chen@dfinity.org>
Co-authored-by: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com>

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'>
@@ -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 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'>
+```
 
-Coercing a non-null, non-optional and non-reserved value at an option type treats it as an optional value:
+Any other type goes to `null`:
 ```
-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
+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: