Spec: Refine the opt rule

[nomeata]

this writes the rules out as described in
#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 #239.

[nomeata]

Shall we get that in?

[chenyan-dfinity]

Fixed a typo for null <: t'. PTAL.

[nomeata]

Is it really a typo? Oh man, it’s always a knot in the brain to solve these, especially with the negations… but I think you are right, this way this matches the line

 C[<t> <: opt <t'>](_) = null  if not (null <: <t'>) and not (<t> <: <t'>)

in the rules for coercion.

I tried to peek into the Coq rules, but there we just have t <: opt t' without constraint, which is IMHO more honest, but I think Andreas didn’t want to simple write that in the Spec as it does not explain the fine points around subtyping well.

[chenyan-dfinity]

Yeah, the Rust implementation has this condition, and if I change it to null <: t, the test suite fails.