Effects typechecking fixes

[rajdakin]

This PR fixes two issues:

• If one kind of unification issue related to effects occurs, the old links tries to generate an error message but the content of that error message generates an internal error;
• If linearity is not tracked, lindo should be parsed exactly the same as do and case <Foo =@ k> like case <Foo => k>.

MWE:

sig f : () {A:() =@ Bool|_}~> Bool
fun f() { lindo A() }

This MWE generates the error in the old links when it is supposed to be correct.
Note that removing the signature of f makes it work regardless of the fix, as the type will be automatically inferred with a linear effect before linearity is dropped.

sig f : (s) {A:(s) {}-> () |_}-> ()
fun f(st) {do A(st)}

This MWE generates an internal error in the old links. The proposed fix transforms this internal error into the expected normal error:

test.links:2: Type error: Invocation of the operation
    `A(st)'
requires an effect context
    `() => (a) {}-> ()'
but, the currently allowed effect is
    `(a) => (a) {}-> ()'
In expression: do A(st).

[thwfhk]

This PR looks good to me. I'm not entirely sure about the second MVE. I think (s) {}-> () is an old-fashioned way of writing effect signatures in Links, which used to be understood as an operation that takes an argument of type s and returns unit. @dhil is this feature completely discarded now?

[rajdakin]

I think (s) {}-> () is an old-fashioned way of writing effect signatures in Links,

It looks like the current parser reads this as () => (s) {}-> (), possibly due to some default sugar settings. Regardless, another MVE would be:

sig f : (s) {A:(Int) => () |_}-> ()
fun f(st) {do A(st)}

The main issue is that the effect arguments are not what is expected (here s instead of Int), so an error is generated, which then triggers an internal error due to the wrong value being passed as the argument to an internal function.

[thwfhk]

That makes sense to me. I agree with you that these are two orthogonal issues.