Lambda Typing Bug

[DavePearce]

(see also #1049, #1025, #1012)

Compiling Web.wy at the moment produces this error:

src/whiley/web/io.whiley:91: expected method(&State<S>)->(Action<S>[]), found method(&State<S>)->(Action<any>[])
    return Action{apply: &(&State<S> st -> apply_alert(st->window,message))}
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[DavePearce]

Currently minimal example:

public type State<S> is { S field }

public type Action<S> is {
    method(&State<S>)->(Action<S>[]) apply
}

public function alert<S>(int message) -> Action<S>:
    return Action{apply: &(&State<S> st -> apply_alert(message))}

method apply_alert<S>(int message) -> Action<S>[]:
    return []

The issue is definitely related to the typing of lambda returns, as for #1025. Curiously, it requires the apply_alert() call though. Note also changing this to apply_alert<S>() and it works fine.

[DavePearce]

This is a slightly more minimal example:

public type Action<S> is method(S)->(Action<S>[])                                     
public function alert<S>() -> Action<S>:                                              
    return &(S st -> apply_alert())               

method apply_alert<S>() -> Action<S>[]:                                               
    return []                                                                         

public export method test():                                          
    Action<int> action = alert<int>()                                                 
    Action<int>[] result = action(0)                                                  
    assume |result| == 0 

[DavePearce]

The problem appears to be here:

private Typing pushLambdaDeclaration(int var, Decl.Lambda expr, Typing typing, Environment environment) {
    // Extract parameters from declaration
    Type params = Decl.Callable.project(expr.getParameters());
    // Allocate a finaliser for this expression
    typing.register(typeStandardExpression(expr, var));
    // Split out incoming lambda types
    Typing nTyping = typing.project(row -> forkOnLambda(row, var, params, environment));
    // Type check the body of the lambda using the expected return types
    Type returns = checkExpression(expr.getBody(), null, false, environment);

Questions:

1) It doesn't pass an expected return when typing the lambda (it passes null instead) 2) Why does checkExpression() return Action<any> rather than Action<S>?

Answers:

2) It returns Action<any> because there is no expected return and no parameters either to the call apply_alert().

Thoughts:

• Can we type the lambda body using pushExpression() rather than statically calling into checkExpression()? That would allow us to resolve cases where there are multiple target lambdas.

[DavePearce]

Replacing most of the above with this:

    // Report errors
    checkForError(expr, typing, nTyping, var, getNaturalType(expr, environment));
    // >>> Propagate forwards into children
    return pushExpression(expr.getBody(), r -> getLambdaReturn(r.get(var)), nTyping, environment);

Resolves the problem, but now other tests also. For example, Lambda_Valid_14:

type updater is method()

public method update(&int ptr):
    *ptr = 0

public export method test():
    &int p = new 123
    // create curried closure
    updater f = &( -> update(p))
    // Apply it
    f()
    // Check it
    assume *p == 0

The reported error is:

Lambda_Valid_14.whiley:9: expected void, found void
    updater f = &( -> update(p))
                      ^^^^^^^^^

Which seems a bit random! There error here is being reported in pushInvoke(). And that then leads me to this:

private static Typing.Row filterOnSubtype(Typing.Row row, int var, Type subtype, Environment environment) {
    Type supertype = row.get(var);
    if (supertype instanceof Type.Any) { ... }
    else if(subtype instanceof Type.Void) {
        // NOTE: This is an edge case when we try to use the return value from a
        // function which returns void. In such case, we want to kill the typing row
        // dead.
        return row.set(var, subtype);

That is some kind of separate check. Commenting this out, and all valid tests do now pass, but more invalid tests fail. For example, Function_Invalid_14:

function g() -> int:
    return f()

function f():
    return h()

function h()->int:
    return 0

[DavePearce]

Ok, have a possible fix with this:

else if(!(supertype instanceof Type.Void) && subtype instanceof Type.Void) {
        // NOTE: This is an edge case when we try to use the return value from a
        // function which returns void. In such case, we want to kill the typing row
        // dead.
        return row.set(var, subtype);
    }

All valid and invalid tests now pass ... just need to do some more sanity checking.