golemcloud / golem

Golem is an open source durable computing platform that makes it easy to build and deploy highly reliable distributed systems.
https://learn.golem.cloud/
Apache License 2.0
530 stars 59 forks source link

Type checker: Fixes #791 and #784 #1005

Closed afsalthaj closed 1 month ago

afsalthaj commented 1 month ago

Fixes #791 and #784

We have tried level best to intercept phases of compilation to bring about maximum user friendly error messages. This task is estimated together as 10 , but I am closing it here, as we have progressed a lot with many improvements and also has a proper structure as a foundation for us to keep improving.

This interceptor is nothing but dedicated type_check module which itself has multiple phases such as the following

Before this PR, the above errors were leaked into type-unification which then produced lower-level compilation errors.

function-call type errors

The above listed phases are pretty much independent. Those functions can be called given a Rib Expr.

However, the first step of type-check is function-call type errors which internally calls the rest of the phases internally, because this phase (which knows about functions arguments and other metadata) has more context about expected types, and other details. Therefore, it can attach more details on top of the error messages produced by rest of the phases.

Independent phases of type-check

Although function-call type error phase internally calls rest of the phases, rest of the phases are called independently thereafter. They are independent of each other, however, we have a reasonable order to it in the code

Error Messages pointing to specific field or index

Invalid argument in `foo`: `{a: {ad: {ada: \"1\"}, ae: (1, \"foo\")}}`. 
Type mismatch for `a.ad.ada`. Expected `s32`"
Invalid argument in `foo`: `{a: { ae: (1, 2)}, b: 3, c: [1, 2, 3], d: {da: 4}}`. 
Type mismatch for `a.ae[1]`. Expected `st

Error Messages pointing to un-inferred types

Let's say you passed a field in record, which shouldn't have existed. This will produce the following error

Invalid argument in `foo`: `{x: 3, a: {aa: 1, ab: 2}`. Cannot infer the type of `3` in `x`. Expected type: `record<a: record<aa: s32, ab: s32>`

Exhaustive pattern matches for variants, option, result (and works for nested matches)


  let x = ok(ok("foo"));
   match x {
     ok(ok(a)) => a,
     err(_) => "bar"
   }

will produce

Error: Non-exhaustive pattern match. The following patterns are not covered: `ok(err)`. 
To ensure a complete match, add these patterns or cover them with a wildcard (`_`) or an identifier."

Dead Code

  let x = some("foo");
  match x {
     _ => "none",
     none => "a"
   }

will produce

Error: Dead code detected. 
The pattern `none` is unreachable due to the existence of the pattern `_` prior to it

Similarly,

   let x = some("foo");
   match x {
     something => "none",
     some(_) => a
   }

will produce

Error: Dead code detected. 
The pattern `some(_)` is unreachable due to the existence of the pattern `something` prior to it

Variant Exhaustivity

The same works for variants too. Here is 1 example which is the output when I didn't update the tests

Error: Non-exhaustive pattern match. 
The following patterns are not covered: `ok(case-f32), ok(case-option), ok(case-result), ok(case-tuple), ok(case-record), ok(case-s32), ok(case-f64), ok(case-u64), ok(case-bool), ok(case-list), ok(case-chr), ok(case-none)`. 
To ensure a complete match, add these patterns or cover them with a wildcard (`_`) or an identifier.

Many many bug fixes

On the pathway, we managed to fix a few more subtle logical bugs

afsalthaj commented 1 month ago

Fix #791

afsalthaj commented 1 month ago

Fix #784

afsalthaj commented 1 month ago

Unification clean up is not done in this PR, but I have moved to separate modules.