Disable subtyping, introduce coercions, and type check core

[jiribenes]

See the PR comments.

[jiribenes]

The following program breaks down for reasons I don't understand:

effect Raise(msg: String): Unit

def main() = try {
  def block(msg: String): Unit / {} = { do Raise(msg) }

  val f: () => Unit at raise = {
    val thn = box { block("first") }
    val els = box { block("second") }

    if (true) { // <  error: 
      thn       // <      Not allowed {raise}
    } else {    // <
      els       // <
    }
  }
} with raise: Raise { msg => panic(msg) }

thn and els are both inferred to be () => Unit at raise

but the if-then-else stmt claims "Not allowed {raise}".

If I manually annotate the type of either thn or els with : () => Unit at raise, then everything works again. Strange.

[jiribenes]

The following commutation also works:

// [...]
    val thn = box { block("first") }
    val els = box { block("second") }

    def res() /* at raise */ = if (true) {
      thn()
    } else {
      els()
    }

    box res
  }
// [...]

[b-studios]

I disabled subtyping in contravariant positions, since there we cannot (easily) insert coercions. In particular, we do not want to eta-expand functions to insert coercions.

[b-studios]

Current plan to insert coercions:

1. since Typer annotated inferred all types but used subtyping in some positions, in the translation to core we now need to insert the coercions where necessary. In order to determine whether coercions are necessary, core-Transformer could pass down the expected return type of a statement / expression (hence only covariant coercions).
2. If there is a type mismatch between the expected (Core Type?) and the type of the generated core expression that can be resolved by coercions, insert them there.

[jiribenes]

btw, in case we'd want other names than isZeroLike and isOneLike, we could try borrowing names from type theory with isUninhabited and isContractible :^)

[b-studios]

Quick status report: yesterday night, I tried to thread the expected type through the core.Transformer in order to insert coercions. I am not happy with the result since I am partially reimplementing type checking.

So I am currently tempted to go back to my original idea where Typer detects coercions and annotates them in the DB (yes... more side channeling---broken window).

Ideally, typer would perform elaboration. However, if we have unification based (HM-like) type inference, this is a bit tricky to achieve in general. How do other languages (like Koka) implement elaboration if things might become known only much later (and non-locally)?

It seems an elaborating typer is easier to implement in a bidirectional setting.

[b-studios]

Note: of course we can collect coercions also by Source and then display them in LSP as inlay information. This way some errors might be less confusing. For example in the test case

def foo(): Option[Int] = if (true) Some(42)

we infer a coercion from Some(42) to Unit since the else branch is missing.

[b-studios]

TODOs

• Look into machine and LLVM at all.
• potentially drop type annotations on Val and Let in core since typing should be unique, now that Match is annotated.
• look into VMTests (I expect there are a lot of failing tests since we now add coercions regardless of the backend and I disabled some type-based optimizations)
• implement proper type comparison on core (alpha equivalence, etc)
• implement a proper type checker for core, now that the type system is simpler again.
• consider replacing <>: tpe by <> match [tpe] {} and assign Nothing as a type for all holes.

[b-studios]

Explicitly annotating match with the motif together with limited checks of type-correctness in core surfaced a few bugs:

A lot of times, transformations like Normalizer, RemoveTailResumptions, or DirectStyle change the result type and hence these transformations also need to change the motif annotated on the match. While this wasn't necessary before, this might have led to problems in PolymorphismBoxing, which we just haven't discovered yet.

[b-studios]

The VMTests look roughly ok with one exception: parsing_dollars that now suddenly has a lot of shifts and resumes that weren't there before.

   branches = 210,
-  pushedFrames = 68,
-  poppedFrames = 67,
+  pushedFrames = 1,
+  poppedFrames = 1,
   allocations = 0,
   variableWrites = 88,
-  resets = 2,
-  shifts = 68,
-  resumes = 66
+  resets = 1,
+  shifts = 1,
+  resumes = 0

Before we generated this code in core:

val v_r_7058: Nothing_383 = shift(p_7035) { {k_7106} =>
  return ()
};
v_r_7058 match {}

while now we generate

shift(p$14160: Prompt[Unit] @ {pCapt$14159}) { (){k$14237 @ resume$14236: Resume[Unit, Unit]} => 
  return ()
}

The former is arguably better, since it is trivially tail resumptive (empty match) in any continuation other than k_7106. Hence the other shift and resumes have been removed originally, but are now still there.

[b-studios]

we can delete those

[b-studios]

delete this

[phischu]

We fixed many things, this needs to be merged.

[b-studios]

We can merge but should investigate this.

[b-studios]

Again, let's merge but also investigate later whether we want to have coercions at all.

[b-studios]

If we do not insert coercions, we can also delete this duplicate check here, which improves errors.

[b-studios]

I like "motif" but of course we can also use the english term "motive" that Conor used.

[b-studios]

Do we want to keep these in "production" as well? This might be costly.

[b-studios]

We are not yet done here (but can complete this in a follow up PR)! We need to actually check whether the constraints hold when encountering the declarations.

[b-studios]

I'm leaving this here, since we will need a very similar logic when checking constraints at the declaration site.

[b-studios]

It is a bit sad that we need the type annotations here.

[b-studios]

@phischu once CI passes (which can take a time due to reparse tests), we can merge this

[b-studios]

I retract. The LLVM tests using files are still failing on my Mac M1. I would be nice to have an ARM runner; maybe we could set up one at some point.

[b-studios]

We should cherrypick / rebase the CI test added to master