Improved type inference

[supercooldave]

This PR relaxes the type checking in the compiler dealing with unknown information (BottomType), which arises for instance in expressions like Nothing where the parameter to Maybe[_] is not provided nor can be inferred from the context. This PR permits such code to compile because the presence of BottomType does not affect the compilation.

Some previously failing tests now pass.

The key test is in regressions/836.enc because this PR builds directly upon the PR that fixed that issue (#841).

Also, fixes #792

[EliasC]

I see the point of this and the changes are straightforward, but I'm wondering if we're optimising for toy programs rather than "real" code? For example, the following expression now compiles (which makes sense)

match Nothing with
  Nothing => 42
end

but at the same time, the following function (still) does not compile and arguably gives a worse error message than before:

fun lookup[k : Eq[k], v](key : k, arr : [(k, v)]) : Maybe[v]
  var elem = Nothing
  for e <- arr do
    if e.0.eq(key) then
      elem = Just(e.1)
    end
  end
  return elem
end

Not enough information to infer the type.
Try adding more type information.
In expression:
Just(e.1)
In expression:
elem = Just(e.1)

The function is fixed by adding type annotations, not where the typechecker is pointing, but where elem is declared. Before this PR, the typechecker would indeed fail at the declaration site.

Does it make sense to require type annotations for, say, variables and functions whose values (bodies) contain a bottom typed value?

[supercooldave]

@EliasC The situation you refer to involves multiple different statements, as opposed to a single expression. Checking of bottomness doesn't span different statements.
Of the top of my head, I'm not sure how best to handle this.
Perhaps the error message could include some better hints, such as where good places to add the type annotations are.

[EliasC]

We will most likely need this again :)

[supercooldave]

I thought we were finished with tracing. My bad.

[EliasC]

What I'm proposing is to disallow val x = Nothing and give the error about type annotations there, but still allow e.g. match Nothing with .... If you assign Nothing to a variable, chances are very high that you are planning to re-assign it, which will lead to an error. We should therefore catch this error as early as possible.

[supercooldave]

@EliasC Sounds complicated to check and awfully specific. Would [Nothing] be allowed? Or is the assignment of a bottom-typed value disallowed?

[EliasC]

I'll be more clear:

An assignment where the right-hand side has a type that contains the bottom type should not be allowed without type annotations. Similarly, I think that closure whose body has a type that contains the bottom type should not be allowed without type annotations. All other usages of the bottom type can be allowed.