Subtyping: Transitivity of opt-to-constituent rule

[nomeata]

I started to do some baby steps in formalizing a “mini candid” in Coq, starting with the rules that seem safe.

But adding the “specialize to constituent type” rule is causing problems:

If the rule is

not (null <: t2)     t1 <: t2
--------------------------------
        t1 <: opt t2

as it is now, then this is not transitive. We have int <: opt int (by this rule), opt int <: opt opt int (by the normal rule), but not int <: opt opt int (because of the not (null <: t2) restriction).

This restriction was added in #135, upon my suggestion. Without that restriction, we have the problems described in #135, i.e. bad interaction with the “catch decoding rule”, and the problem that

    t1 <: t2
------------------
  t1 <: opt t2

doesn't make progress if t2 = opt t2.

Or, to respond to @rossberg says in #135 (comment)

Interesting suggestion. I suppose options of options are not something you would see often in an interface, so limiting their evolution might be okay. How confident can we be that this has no problems?

I wish we had spare cycles to mechanise this, and prevent further holes.

I am no longer confident that this has no problems.

One way to maybe! taper over the problem is to restrict the other rule as well:

not (null <: t2)     t1 <: t2
--------------------------------
     opt  t1 <: opt t2

so that you can’t go from opt int to opt opt int… but that essentially disallows evolution under opt opt and might be better served by disallowing opt opt… probably not nice. Or maybe this rule:

(null <: t1) iff (null <: 2)      t1 <: t2
---------------------------------------
             opt  t1 <: opt t2

which rules out opt int <: opt opt int without ruling out opt nat <: opt int nor opt opt nat <: opt opt int ?

[nomeata]

Maybe this is all fine together with the other special behavior for opt (the opportunistic decoding). But that one is dubious for other reasons, see #141. And even if it is fine, I wonder if we get weird transitive behavior.

[nomeata]

With the extra (null <: t1) iff (null <: 2) restriction, I can prove transitivity, see #147. Hmm, not sure I like that.

[crusso]

What if you have (dynamic) maybe and vanilla opt and restrict maybe to be invariant. That rules out the counterexample, I think, but maybe too much else...

[nomeata]

This issue here isn't really about the dynamic aspects of opt, it already arises with the desire to do t <: opt t. A separate type constructor might help if we forbid its immediate nesting (no maybe maybe t).

[nomeata]

Closing this; the narrow issue of this issue only applies to a variant of the formalism that we are not using right now, as the Coq profs in #147 shows (i.e. the opportunistic subtyping rule tapers over this problem.)