Subtype corner case with `None`-continuations trips the IR-typechecker

[ggreif]

Type checking continuations after async-lowering fails for unusual code:

Ill-typed intermediate code after Async Lowering (use -v to see dumped IR):
(unknown location): IR type error [M0000], subtype violation:
  (() -> (), Error -> ())
  (None -> (), Error -> ())

Raised at Ir_def__Check_ir.error.(fun) in file "ir_def/check_ir.ml", line 95, characters 30-92
Called from Ir_def__Check_ir.check_exp.(<:) in file "ir_def/check_ir.ml" (inlined), line 369, characters 6-32
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 411, characters 10-27
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 704, characters 4-23
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 704, characters 4-23
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 704, characters 4-23
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 704, characters 4-23
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 786, characters 4-40
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 399, characters 4-32
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 799, characters 4-48
Called from Ir_def__Check_ir.check_dec in file "ir_def/check_ir.ml", line 1100, characters 4-21
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 703, characters 4-22
Called from Ir_def__Check_ir.check_exp in file "ir_def/check_ir.ml", line 786, characters 4-40
Called from Ir_def__Check_ir.check_dec in file "ir_def/check_ir.ml", line 1100, characters 4-21
Called from Stdlib__list.iter in file "list.ml", line 110, characters 12-15
Called from Ir_def__Check_ir.check_comp_unit in file "ir_def/check_ir.ml", line 1159, characters 4-23
Called from Ir_def__Check_ir.check_prog in file "ir_def/check_ir.ml", line 1178, characters 6-28

The error message is bogus! () -> () is subtype of None -> () because None is subtype of ().

Here is the repro:

import { debugPrint; error } =  "mo:⛔";

actor {

      func t8() : async () {
        try {
            debugPrint "IN8";
            await* async* throw error "IN8";
        }
        catch _ { debugPrint "CAUGHT8" }
    };
}

[ggreif]

It turns out that this is an old bug. The check_sub check uses the relational infrastructure from module Type. Type.sub descends into the tuple components and then applies the relation to the codomain and domain of the function type sequences. When doing this, it uses List.for_all2 which throws Invalid_argument when the argument sequences are of different lengths, resulting in false. This is the case here, as length () = 0 but length (Non) = 1.

Currently I have no idea how to make a special case for Type.Non (bottom) that fits into the relational subtype check.

Also, I could not come up with an example that triggers this bug from Motoko directly, as the interpreter accepts this:

> let cont : (None -> (), Int -> (), () -> ()) = (func () {}, func (i : Int) {}, func () {});

gets accepted 😲

UPDATE: Here is an interpreter example:

> let cont : (() -> (), Int -> (), () -> ()) = (func () {}, func (i : Int) {}, func () {});
> let contA : (None -> (), Int -> (), () -> ()) = cont;
stdin:13.49-13.53: type error [M0096], expression of type
  (() -> (), Int -> (), () -> ())
cannot produce expected type
  (None -> (), Int -> (), () -> ())