From 8a6a38736e192d6ca727e5008d59ffb6f093ace8 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 11 Dec 2020 17:46:04 +0100
Subject: [PATCH] Spec: Change subtype-to-constituent rule
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

the coq formalization in #147 shows that the old rule didn’t quite work
(it was confused about `5 ~> ? : opt null` I believe), but this variant
does. I think all implemnetations do the right thing anways (so maybe
rewriting this as a partial coercion _function_ would be helpful)
---
 spec/Candid.md | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 96e69844..75c3c646 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -968,9 +968,18 @@ Coercing a non-null, non-optional and non-reserved value at an option type treat
 <v> ≠ (null : reserved)
 <v> ≠ opt _
 not (null <: <t>)
-opt <v> ~> <v'> : opt <t>
+<v> ~> <v'> : <t>
 -------------------------
-<v> ~> <v'> : opt <t>
+<v> ~> opt <v'> : opt <t>
+```
+Again, failure to coerce the value turns into `null`:
+```
+<v> ≠ null
+<v> ≠ (null : reserved)
+<v> ≠ opt _
+null <: <t> ∨ not (<v> ~> _ : <t>)
+----------------------------------
+<v> ~> null : opt <t>
 ```