Value restriction and effect signatures about links HOT 3 CLOSED

Unsurprisingly the example type checks when using flexible type variables

links> sig foo : () {Bar:%a|_}-> %a
...... fun foo() { var x = do Bar; x };
foo = fun : () {Bar:a|_}-> a

from links.

The issue is reproducible in the sessions branch using the built-in hear effect

links> sig foo : () {:a|_}~> a 
...... fun foo() { var x = recv(); x };
<stdin>:2: Type error: ...

from links.

The issue only occurs for non-recursive functions. The problem is that it is sometime necessary to propagate type information from the type signature to the body of the function (e.g. when we make use of recursive types which cannot be inferred), and yet for a non-recursive function it is unsound to add the function itself to the environment so type variables in the function signature do not occur anywhere in the environment. An easy hack is to add a fresh dummy variable with the type annotation to the environment.

from links.