From 41a84c8d6b9eac9456da9f51dcf67ee9fa99b951 Mon Sep 17 00:00:00 2001
From: Yan Chen <yan.chen@dfinity.org>
Date: Tue, 11 Jan 2022 17:04:49 -0800
Subject: [PATCH 1/6] spec: subtype checking only for reference types

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

diff --git a/spec/Candid.md b/spec/Candid.md
index 576ac1c68..a6d5db56e 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -1,8 +1,8 @@
 # Candid Specification
 
-Version: 0.1.3
+Version: 0.1.4
 
-Date: February 3, 2021
+Date: January 11, 2022
 
 ## Motivation
 
@@ -885,63 +885,61 @@ service { <name> : <functype>; <methtype>;* } <: service { <name> : <functype'>;
 
 This subtyping is implemented during the deserialisation of Candid at an expected type. As described in [Section Deserialisation](#deserialisation), the binary value is conceptually first _decoded_ into the actual type and a value of that type, and then that value is _coerced_ into the expected type.
 
-To model this, we define, for every `t1, t2` with `t1 <: t2`, a function `C[t1<:t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`, and is indeed total.
+To model this, we define a partial coercion function `C[t1 ~> t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`. For every `t1, t2` with `t1 <: t2`, the function is always defined, but not every `t1, t2` has a coercion.
 
-to describe these values, we re-use the syntax of the textual representation, and use the the `<annval>` syntax (i.e. `(v : t)`) if necessary to resolve overloading.
+To describe these values, we re-use the syntax of the textual representation, and use the the `<annval>` syntax (i.e. `(v : t)`) if necessary to resolve overloading.
 
 #### Primitive Types
 
 On primitve types, coercion is the identity:
 ```
-C[<t> <: <t>](x) = x    for every <t> ∈ <numtype>, bool, text, null
+C[<t> ~> <t>](x) = x     for every <t> ∈ <numtype>, bool, text, null
 ```
 
 Values of type `nat` coerce at type `int`:
 ```
-C[nat <: int](<nat>) = <nat>
+C[nat ~> int](<nat>) = <nat>
 ```
 
 Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`):
 ```
-C[<t> <: reserved](_) = null
+C[<t> ~> reserved](_) = null
 ```
-NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `C[empty <: <t>]` is the unique function on the empty domain.
+NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `C[empty ~> <t>]` is the unique function on the empty domain.
 
 #### Vectors
 
 Vectors coerce pointwise:
 ```
-C[vec <t> <: vec <t'>]( vec { <v>;* } ) = vec { C[<t> <: <t'>](<v>);* }
+C[vec <t> ~> vec <t'>]( vec { <v>;* } ) = vec { C[<t> ~> <t'>](<v>);* }
 ```
 
 #### Options
 
 The null type and the reserved type coerce into any option type:
 ```
-C[null <: opt <t>](null) = null
+C[null ~> opt <t>](null) = null
 ```
 
 An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`:
 ```
-C[opt <t> <: opt <t'>](null) = null
-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'>)
+C[opt <t> ~> opt <t'>](null) = null
+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')
 ```
 
 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`:
 ```
-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>)
+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:
@@ -951,8 +949,8 @@ In the following rule:
  * the `<nat3>*` field names are those only in the expected type, which therefore must be of optional or reserved type. The `null` value is used for these.
 
 ```
-C[record { <nat1> = <t1>;* <nat2> = <t2>;* } <: record { <nat1> = <t1'>;* <nat3> = <t3>;* }](record { <nat1> = <v1>;* <nat2> = <v2>;* })
-    = record { <nat1> = C[<t1> <: <t1'>](<v1>);* <nat3> = null;* }
+C[record { <nat1> = <t1>;* <nat2> = <t2>;* } ~> record { <nat1> = <t1'>;* <nat3> = <t3>;* }](record { <nat1> = <v1>;* <nat2> = <v2>;* })
+    = record { <nat1> = C[<t1> ~> <t1'>](<v1>);* <nat3> = null;* }
 ```
 
 #### Variants
@@ -960,8 +958,8 @@ C[record { <nat1> = <t1>;* <nat2> = <t2>;* } <: record { <nat1> = <t1'>;* <nat3>
 Only a variant value with an expected tag coerces at variant type.
 
 ```
-C[variant { <nat> = <t>; _;* } <: variant { <nat> = <t'>; _;* }](variant { <nat> = <v> })
-    = variant { <nat> = C[<t> <: <t'>](<v>) }
+C[variant { <nat> = <t>; _;* } ~> variant { <nat> = <t'>; _;* }](variant { <nat> = <v> })
+    = variant { <nat> = C[<t> ~> <t'>](<v>) }
 ```
 
 
@@ -970,18 +968,20 @@ C[variant { <nat> = <t>; _;* } <: variant { <nat> = <t'>; _;* }](variant { <nat>
 Function and services reference values are untyped, so the coercion function is the identity here:
 
 ```
-C[func <functype> <: func <functype'>](func <text>.<id>) = func <text>.<id>
-C[service <actortype> <: service <actortype'>](service <text>) = service <text>
-C[principal <: principal](principal <text>) = principal <text>
+C[func <functype> ~> func <functype'>](func <text>.<id>) = func <text>.<id>      if func <functype> <: func <functype'>
+C[service <actortype> ~> service <actortype'>](service <text>) = service <text>  if service <functype> <: service <functype'>
+C[principal ~> principal](principal <text>) = principal <text>
 ```
 
+NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation for reference types.
+
 #### Tuple types
 
 Whole argument and result sequences are coerced with the same rules as tuple-like records. In particular, extra arguments are ignored, and optional parameters read as as `null` if the argument is missing or fails to coerce:
 
 ```
-C[(<t>,*) <: (<t'>,*)]((<v>,*)) = (<v'>,*)
-    if C[record {<t>;*} <: record {<t'>,*}](record {<v>;*}) = record {<v'>;*}
+C[(<t>,*) ~> (<t'>,*)]((<v>,*)) = (<v'>,*)
+    if C[record {<t>;*} ~> record {<t'>,*}](record {<v>;*}) = record {<v'>;*}
 ```
 
 
@@ -1001,7 +1001,7 @@ The relations above have certain properties. As in the previous section, `<v> :
 
 * Roundtripping:
   ```
-  (<v> : <t>) ⟺ C[<t> <: <t>](<v>) = <v>
+  (<v> : <t>) ⟺ C[<t> ~> <t>](<v>) = <v>
   ```
 
 * Soundness of subtyping (or, alternatively, well-definedness of coercion)
@@ -1024,12 +1024,12 @@ The relations above have certain properties. As in the previous section, `<v> :
   ```
   does not imply
   ```
-  C[<t1> <: <t3>] = C[<t2> <: <t3>] ⚬ C[<t1> <: <t2>]
+  C[<t1> ~> <t3>] = C[<t2> ~> <t3>] ⚬ C[<t1> ~> <t2>]
   ```
 
   However, it implies
   ```
-  C[<t1> <: <t3>] ~ (C[<t2> <: <t3>] ⚬ C[<t1> <: <t2>])
+  C[<t1> ~> <t3>] ~ (C[<t2> ~> <t3>] ⚬ C[<t1> ~> <t2>])
   ```
   where ~ is the smallest homomorphic, reflexive, symmetric relation that satisfies `∀ v. opt v ~ null`.
 

From b4510275298d98f871c05c94ffa099ee654e29f9 Mon Sep 17 00:00:00 2001
From: Yan Chen <yan.chen@dfinity.org>
Date: Wed, 12 Jan 2022 19:22:14 -0800
Subject: [PATCH 2/6] use inference rule instead of partial function

---
 spec/Candid.md | 92 ++++++++++++++++++++++++++++++++++----------------
 1 file changed, 63 insertions(+), 29 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index a6d5db56e..85b9c138a 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -885,59 +885,80 @@ service { <name> : <functype>; <methtype>;* } <: service { <name> : <functype'>;
 
 This subtyping is implemented during the deserialisation of Candid at an expected type. As described in [Section Deserialisation](#deserialisation), the binary value is conceptually first _decoded_ into the actual type and a value of that type, and then that value is _coerced_ into the expected type.
 
-To model this, we define a partial coercion function `C[t1 ~> t2] : t1 -> t2`. This function maps values of type `t1` to values of type `t2`. For every `t1, t2` with `t1 <: t2`, the function is always defined, but not every `t1, t2` has a coercion.
-
-To describe these values, we re-use the syntax of the textual representation, and use the the `<annval>` syntax (i.e. `(v : t)`) if necessary to resolve overloading.
+This section describes the coercion, as a relation `V : T ~> V' : T'` to describe when a value `V` of type `T` can be coerced to a value `V'` of type `T'`. The fields `V`, `T` and `T'` can be understood as inputs and `V'` as the output of this relation.
+To describe these values, we re-use the syntax of the textual representation.
 
 #### Primitive Types
 
 On primitve types, coercion is the identity:
 ```
-C[<t> ~> <t>](x) = x     for every <t> ∈ <numtype>, bool, text, null
+<t> ∈ <numtype>, bool, text, null
+---------------------------------
+<v> : <t> ~> <v> : <t>
 ```
 
 Values of type `nat` coerce at type `int`:
 ```
-C[nat ~> int](<nat>) = <nat>
+--------------------------
+<nat> : nat ~> <nat> : int
 ```
 
 Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`):
 ```
-C[<t> ~> reserved](_) = null
+--------------------------
+_ : <t> ~> null : reserved
 ```
-NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `C[empty ~> <t>]` is the unique function on the empty domain.
+
+NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `<v> : <t> ~> _ : empty` will not hold.
 
 #### Vectors
 
 Vectors coerce pointwise:
 ```
-C[vec <t> ~> vec <t'>]( vec { <v>;* } ) = vec { C[<t> ~> <t'>](<v>);* }
+<v> : <t> ~> <v'> : <t'>
+----------------------------------------------------
+vec { <v>;* } : vec <t> ~> vec { <v'>;* } : vec <t'>
 ```
 
 #### Options
 
-The null type and the reserved type coerce into any option type:
+The null value coerces into any option type:
 ```
-C[null ~> opt <t>](null) = null
+-----------------------------
+null : _ ~> null : opt <t>
 ```
 
 An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`:
 ```
-C[opt <t> ~> opt <t'>](null) = null
-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')
+<v> : <t> ~> <v'> : <t'>
+----------------------------------------
+opt <v> : opt <t> ~> opt <v'> : opt <t'>
+
+not (<v> : <t> ~> _ : <t'>)
+----------------------------------------
+opt <v> : opt <t> ~> null : opt <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'>
+not (null <: <t'>)
+<v> : <t> ~> <v'> : <t'>
+--------------------------------
+<v> : <t> ~> opt <v'> : opt <t'>
 ```
 
-Any other type goes to `null`:
+Any other value 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>)
+
+not (null <: <t'>)
+not (<v> : <t> ~> _ : <t'>)
+--------------------------------
+<v> : <t> ~> null : opt <t'>
+
+null <: <t'>
+not (null <: <t>)
+----------------------------
+<v> : <t> ~> null : opt <t'>
 ```
 
 #### Records
@@ -949,8 +970,11 @@ In the following rule:
  * the `<nat3>*` field names are those only in the expected type, which therefore must be of optional or reserved type. The `null` value is used for these.
 
 ```
-C[record { <nat1> = <t1>;* <nat2> = <t2>;* } ~> record { <nat1> = <t1'>;* <nat3> = <t3>;* }](record { <nat1> = <v1>;* <nat2> = <v2>;* })
-    = record { <nat1> = C[<t1> ~> <t1'>](<v1>);* <nat3> = null;* }
+<v1> : <t1> ~> <v1'> : <t1'>
+opt empty <: <t3>
+-------------------------------------------------------------------------------------------
+record { <nat1> = <v1>;* <nat2> = <v2>;* } : record { <nat1> : <t1>;* <nat2> : <t2>;* } ~>
+record { <nat1> = <v1'>;* <nat3> = null;* } : record { <nat1> : <t1'>;* <nat3> : <t3>;* }
 ```
 
 #### Variants
@@ -958,8 +982,10 @@ C[record { <nat1> = <t1>;* <nat2> = <t2>;* } ~> record { <nat1> = <t1'>;* <nat3>
 Only a variant value with an expected tag coerces at variant type.
 
 ```
-C[variant { <nat> = <t>; _;* } ~> variant { <nat> = <t'>; _;* }](variant { <nat> = <v> })
-    = variant { <nat> = C[<t> ~> <t'>](<v>) }
+<v> : <t> ~> <v'> : <t'>
+----------------------------------------------------------
+variant { <nat> = <v>; } : variant { <nat> : <t>; _;* } ~>
+variant { <nat> = <v'> } : variant { <nat> : <t'>; _;* }
 ```
 
 
@@ -968,9 +994,16 @@ C[variant { <nat> = <t>; _;* } ~> variant { <nat> = <t'>; _;* }](variant { <nat>
 Function and services reference values are untyped, so the coercion function is the identity here:
 
 ```
-C[func <functype> ~> func <functype'>](func <text>.<id>) = func <text>.<id>      if func <functype> <: func <functype'>
-C[service <actortype> ~> service <actortype'>](service <text>) = service <text>  if service <functype> <: service <functype'>
-C[principal ~> principal](principal <text>) = principal <text>
+func <functype> <: func <functype'>
+---------------------------------------------------------------------
+func <text>.id : func <functype> ~> func <text>.id : func <functype'>
+
+service <actortype> <: service <actortype'>
+-----------------------------------------------------------------------------
+service <text> : service <actortype> ~> service <text> : service <actortype'>
+
+------------------------------------------------------------
+principal <text> : principal ~> principal <text> : principal
 ```
 
 NOTE: These rules above imply that a Candid decoder has to be able to decide the subtyping relation for reference types.
@@ -980,8 +1013,9 @@ NOTE: These rules above imply that a Candid decoder has to be able to decide the
 Whole argument and result sequences are coerced with the same rules as tuple-like records. In particular, extra arguments are ignored, and optional parameters read as as `null` if the argument is missing or fails to coerce:
 
 ```
-C[(<t>,*) ~> (<t'>,*)]((<v>,*)) = (<v'>,*)
-    if C[record {<t>;*} ~> record {<t'>,*}](record {<v>;*}) = record {<v'>;*}
+record { <v>;* } : record { <t>;* } ~> record { <v'>;* } : record { <t'>;* }
+----------------------------------------------------------------------------
+(<v>,*) : (<t>,*) ~> (<v'>,*) : (<t'>,*)
 ```
 
 
@@ -1001,12 +1035,12 @@ The relations above have certain properties. As in the previous section, `<v> :
 
 * Roundtripping:
   ```
-  (<v> : <t>) ⟺ C[<t> ~> <t>](<v>) = <v>
+  (<v> : <t>) ⟺ <v> : <t> ~> <v> : <t>
   ```
 
 * Soundness of subtyping (or, alternatively, well-definedness of coercion)
   ```
-  <t> <: <t'> ⇒ ∀ <v> : <t>. v[<t> <: <t'>](<v>) : <t'>
+  <t> <: <t'> ⇒ ∀ <v> : <t> ∃ <v'>. <v> : <t> ~> <v'> : <t'>
   ```
 
 * Higher-order soundness of subtyping

From fa36bc09e7d1ffc284c38cff5df6e3fb20a84be8 Mon Sep 17 00:00:00 2001
From: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com>
Date: Thu, 13 Jan 2022 13:45:51 -0800
Subject: [PATCH 3/6] Apply suggestions from code review

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
---
 spec/Candid.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 85b9c138a..8cae58ea9 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -909,7 +909,7 @@ Coercion into `reserved` is the constant map (this is arbitrarily using `null` a
 _ : <t> ~> null : reserved
 ```
 
-NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `<v> : <t> ~> _ : empty` will not hold.
+NB: No rule is needed for type `empty`, because there are no values of that type. By construction, `_ : empty ~> _ : _` will not hold.
 
 #### Vectors
 
@@ -939,7 +939,7 @@ not (<v> : <t> ~> _ : <t'>)
 opt <v> : opt <t> ~> null : opt <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:
+Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it can be decoded successfully:
 ```
 not (null <: <t'>)
 <v> : <t> ~> <v'> : <t'>
@@ -991,7 +991,7 @@ variant { <nat> = <v'> } : variant { <nat> : <t'>; _;* }
 
 #### References
 
-Function and services reference values are untyped, so the coercion function is the identity here:
+For function and services reference values, the coercion relation checks whether the given types are actually subtypes of the expected type, and fails else:
 
 ```
 func <functype> <: func <functype'>

From a9a03b4127f907f48b36efb05f377803271132d8 Mon Sep 17 00:00:00 2001
From: Yan Chen <yan.chen@dfinity.org>
Date: Thu, 13 Jan 2022 13:56:24 -0800
Subject: [PATCH 4/6] fix

---
 spec/Candid.md | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 8cae58ea9..1be9261a1 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -924,8 +924,9 @@ vec { <v>;* } : vec <t> ~> vec { <v'>;* } : vec <t'>
 
 The null value coerces into any option type:
 ```
+null <: <t>
 -----------------------------
-null : _ ~> null : opt <t>
+null : <t> ~> null : opt <t'>
 ```
 
 An optional value coerces at an option type, if the constituent value has a suitable type, and else goes to `null`:
@@ -949,6 +950,8 @@ not (null <: <t'>)
 
 Any other value goes to `null`:
 ```
+---------------------------------
+<v> : reserved ~> null : opt <t'>
 
 not (null <: <t'>)
 not (<v> : <t> ~> _ : <t'>)
@@ -1038,6 +1041,11 @@ The relations above have certain properties. As in the previous section, `<v> :
   (<v> : <t>) ⟺ <v> : <t> ~> <v> : <t>
   ```
 
+* Well-typedness:
+  ```
+  <v> : <t> ~> <v'> : <t'> ⇒ <v'> : <t'>
+  ```
+
 * Soundness of subtyping (or, alternatively, well-definedness of coercion)
   ```
   <t> <: <t'> ⇒ ∀ <v> : <t> ∃ <v'>. <v> : <t> ~> <v'> : <t'>
@@ -1054,17 +1062,16 @@ The relations above have certain properties. As in the previous section, `<v> :
 
 * NB: Transitive coherence does not hold:
   ```
-  <t1> <: <t2>, <t2> <: <t3>
+  <v1> : <t1> ~> <v2> : <t2>
+  <v2> : <t2> ~> <v3> : <t3>
+  <v1> : <t1> ~> <v3'> : <t3>
   ```
   does not imply
   ```
-  C[<t1> ~> <t3>] = C[<t2> ~> <t3>] ⚬ C[<t1> ~> <t2>]
+  <v3> = <v3'>
   ```
 
-  However, it implies
-  ```
-  C[<t1> ~> <t3>] ~ (C[<t2> ~> <t3>] ⚬ C[<t1> ~> <t2>])
-  ```
+  However, it implies `<v3> ~ <v3'>`, 
   where ~ is the smallest homomorphic, reflexive, symmetric relation that satisfies `∀ v. opt v ~ null`.
 
 The goal of “subtyping completeness” has not been cast into a formal formulation yet.

From c266c7558cee1f7774992ba85062d6381e469c68 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 8 Apr 2022 16:59:21 +0200
Subject: [PATCH 5/6] Update spec/Candid.md

Co-authored-by: Claudio Russo <claudio@dfinity.org>
---
 spec/Candid.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 1be9261a1..263240549 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -994,7 +994,7 @@ variant { <nat> = <v'> } : variant { <nat> : <t'>; _;* }
 
 #### References
 
-For function and services reference values, the coercion relation checks whether the given types are actually subtypes of the expected type, and fails else:
+For function and services reference values, the coercion relation checks whether the given types are actually subtypes of the expected type, and fails otherwise:
 
 ```
 func <functype> <: func <functype'>

From 7af2228959fad2740761ba10e1e098f6835c6632 Mon Sep 17 00:00:00 2001
From: Yan Chen <48968912+chenyan-dfinity@users.noreply.github.com>
Date: Sun, 4 Dec 2022 14:31:00 -0800
Subject: [PATCH 6/6] Apply suggestions from code review

Co-authored-by: Claudio Russo <claudio@dfinity.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
---
 spec/Candid.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 263240549..ed534532e 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -890,7 +890,7 @@ To describe these values, we re-use the syntax of the textual representation.
 
 #### Primitive Types
 
-On primitve types, coercion is the identity:
+On primitive types, coercion is the identity:
 ```
 <t> ∈ <numtype>, bool, text, null
 ---------------------------------
@@ -942,6 +942,7 @@ opt <v> : opt <t> ~> null : opt <t'>
 
 Coercing a non-null, non-optional and non-reserved type at an option type treats it as an optional value, if it can be decoded successfully:
 ```
+not (null <: <t>)
 not (null <: <t'>)
 <v> : <t> ~> <v'> : <t'>
 --------------------------------