From 7783a4a7a41937eef304ef466dfdaabd117d6691 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 17 Nov 2020 15:16:18 +0100
Subject: [PATCH] Opt subtyping: Restrict going via constituent rule

this fixes #135
---
 spec/Candid.md | 25 +++++++++++++++++--------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/spec/Candid.md b/spec/Candid.md
index 1322159e..0232a034 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -751,32 +751,40 @@ Additional rules apply to `empty` and `reserved`, which makes these a bottom res
 empty <: <datatype>
 ```
 
-#### Options and Vectors
+#### Vectors
 
-An option or vector type can be specialised via its constituent type.
+A vector type can be specialised via its constituent type.
 ```
 <datatype> <: <datatype'>
 ---------------------------------
-opt <datatype> <: opt <datatype'>
+vec <datatype> <: vec <datatype'>
+```
 
+#### Options
+
+An option type can be specialised via its constituent type.
+```
 <datatype> <: <datatype'>
 ---------------------------------
-vec <datatype> <: vec <datatype'>
+opt <datatype> <: opt <datatype'>
 ```
-Furthermore, an option type can be specialised to either `null` or to its constituent type:
+
+Furthermore, an option type can be specialised to `null`:
 ```
 ------------------------
 null <: opt <datatype>
+```
 
-not (null <: <datatype>)
+It can also be specialised to its constituent type, unless that type is itself optional:
+
+```
+not (null <: <datatype'>)
 <datatype> <: <datatype'>
 -----------------------------
 <datatype> <: opt <datatype'>
 ```
 The premise means that the rule does not apply when the constituent type is itself `null`, an option or `reserved`. That restriction is necessary so that there is no ambiguity. For example, otherwise there would be two ways to interpret `null` when going from `opt nat` to `opt opt nat`, either as `null` or as `?null`.
 
-Q: The negated nature of this premise isn't really compatible with parametric polymorphism. Is that a problem? We could always introduce a supertype of all non-nullable types and rephrase it with that.
-
 Finally, in order to maintain *transitivity* of subtyping, two unusual rules allow, in fact, *any* type to be regarded as a subtype of an option.
 ```
 not (<datatype> <: opt <datatype'>)
@@ -959,6 +967,7 @@ Coercing a non-null, non-optional and non-reserved value at an option type treat
 <v> ≠ null
 <v> ≠ (null : reserved)
 <v> ≠ opt _
+not (null <: <t>)
 opt <v> ~> <v'> : opt <t>
 -------------------------
 <v> ~> <v'> : opt <t>