Stream: beginners

Topic: Function type annotation gets ignored


view this post on Zulip Ilya Shmygol (Apr 23 2025 at 20:01):

Again something I probably miss, but could you please help me with this one. The code below fails:

get_user : Result (List Str) _ -> Result Str _
get_user = |prev_result|
    when prev_result is
        Err(_) as err ->
            err
        Ok([]) ->
            Err(UserNotFound)
        Ok([user]) ->
            Ok(user)
        Ok([_, ..]) ->
            Err(MultipleUsersFound)

With the type mismatch error:

── TYPE MISMATCH in ./Delme.roc ────────────────────────────────────────────────

Something is off with the 3rd branch of this when expression:

 3│  get_user : Result (List Str) _ -> Result Str _
 4│  get_user = |prev_result|
 5│      when prev_result is
 6│          Err(_) as err ->
 7│              err
 8│          Ok([]) ->
 9│              Err(UserNotFound)
10│          Ok([user]) ->
11│              Ok(user)
                 ^^^^^^^^

This Ok tag application has the type:

    [Ok Str, …]

But the type annotation on get_user says it should be:

    [Ok (List Str), …]

────────────────────────────────────────────────────────────────────────────────

1 error and 1 warning found in 24 ms%

And the compiler seems to ignore the type annotation completely, because the error looks completely the same even if I put something obviously wrong in it like: get_user : Result (List Str) _ -> Result U8 _.

You know, it's very hard to get rid of a feeling, that it's something wrong with the compiler when it's in a premature state. :)

view this post on Zulip Brendan Hansknecht (Apr 23 2025 at 20:11):

Lack of gradual typing or automatic conversion of types strikes again ...we really need either better errors or better solutions around this

view this post on Zulip Brendan Hansknecht (Apr 23 2025 at 20:12):

Key insight is the type of err is Result (List Str) _. As such, the input and output type must both be Result (List Str) _.

view this post on Zulip Brendan Hansknecht (Apr 23 2025 at 20:13):

If you remove the as err and instead do Err(e) -> Err(e), it should all work.

view this post on Zulip Ilya Shmygol (Apr 23 2025 at 20:13):

I don't think it's graudal typing, because this code fails with the same error:

get_user : Result (List Str) _ -> Result Str _
get_user = |prev_result|
    when prev_result is
        Err(_) as err ->
            err
        # Ok([]) ->
        #     Err(UserNotFound)
        # Ok([user]) ->
        #     Ok(user)
        # Ok([_, ..]) ->
        #     Err(MultipleUsersFound)
        Ok(users) ->
            when users is
                [] ->
                    Err(UserNotFound)
                [user] ->
                    Ok(user)
                [_, ..] ->
                    Err(MultipleUsersFound)

view this post on Zulip Ilya Shmygol (Apr 23 2025 at 20:14):

Brendan Hansknecht said:

If you remove the as err and instead do Err(e) -> Err(e), it should all work.

It works indeed!

view this post on Zulip Ilya Shmygol (Apr 23 2025 at 20:16):

Ok, it is gradual typing, but in a different place. I see now. Thanks!

view this post on Zulip Brendan Hansknecht (Apr 23 2025 at 22:29):

Yeah, at a minimum, we need a better error/ux here

view this post on Zulip Brendan Hansknecht (Apr 23 2025 at 22:30):

Frankly, I would love for limited cases like this to just work, but I'm not sure that is viable without significant compiler effort/complexity (not really sure either way, don't work on the type checker much)

view this post on Zulip Richard Feldman (Apr 23 2025 at 23:27):

yeah Ayaz and someone else had a long exchange looking into this a month or two ago (I forget where the thread was) and as I recall the conclusion seemed to be that it couldn't work reliably in practice

view this post on Zulip Richard Feldman (Apr 23 2025 at 23:27):

or at least not without switching to a totally different type system :stuck_out_tongue:

view this post on Zulip Anthony Bullard (Apr 24 2025 at 00:52):

Ilya Shmygol said:

Brendan Hansknecht said:

If you remove the as err and instead do Err(e) -> Err(e), it should all work.

It works indeed!

Yeah that _ in the Err destructure in the first branch is probably not letting us be able to figure out what the type of the Result Err is, but Err(e) -> Err(e) gives us a variable that we can assign a free var to

view this post on Zulip Anthony Bullard (Apr 24 2025 at 00:53):

I don’t understand how we got that error though…

view this post on Zulip Brendan Hansknecht (Apr 24 2025 at 05:26):

I think we get the weird error cause it checks the branches for consistency first before checking if the branches match the out expression

view this post on Zulip Brendan Hansknecht (Apr 24 2025 at 05:27):

And the branches aren't consistent due to the first returning Result (List Str) _ and the last returning Result Str _

view this post on Zulip Ilya Shmygol (Apr 24 2025 at 07:57):

I actually get it often: if branches are not consistent the error message just ignores the function annotation and relies on the type inferenced from one of the branches.

view this post on Zulip Anthony Bullard (Apr 24 2025 at 10:10):

Ilya Shmygol said:

I actually get it often: if branches are not consistent the error message just ignores the function annotation and relies on the type inferenced from one of the branches.

I wonder if it changes if you assign the result of the when to a var and then return the var

view this post on Zulip Anthony Bullard (Apr 24 2025 at 10:12):

Brendan Hansknecht said:

And the branches aren't consistent due to the first returning Result (List Str) _ and the last returning Result Str _

Oh right since you are returning the Err as is from the arg type that means the value is the same. Constructing a new Err will ensure that it can be inferred as the annotated return type

view this post on Zulip Anthony Bullard (Apr 24 2025 at 10:20):

I think the non obvious part with us having fully inferred structural typing is that a value in a tagged union still carries with it the type of entire tag union it is apart of. Which is different than say TypeScripts unions where the values have their own type which is then checked where necessary to be part of some union. Err(_) isn’t just a value with an Err tag and some payload value here. It is a Result (List Str) _ value that happens to have been instantiated with the Err tag.

view this post on Zulip Ilya Shmygol (Apr 24 2025 at 10:22):

Anthony Bullard said:

I wonder if it changes if you assign the result of the when to a var and then return the var

Well if I put the result of the when block to a var the error is basically the same, but makes more sense, because it doesn't complain about get_user.

Without variable (pay attention to how is the error message wrong about get_user annotation):

This Ok tag application has the type:

    [Ok Str, …]

But the type annotation on get_user says it should be:

    [Ok (List Str), …]

With a variable the error message makes a bit more sense, because it complains about the when branches being inconsistent:

This Ok tag application has the type:

    [Ok Str, …]

But all the previous branches have type:

    [Ok (List Str), …]

All branches of a when must have the same type!

view this post on Zulip Anthony Bullard (Apr 24 2025 at 10:24):

Yeah since the offending expression is in return position it is the value of get_users and there the error is attributed to that binding

view this post on Zulip Anthony Bullard (Apr 24 2025 at 10:27):

I think a small improvement to the error handling here is to always attribute the error to the expression and then say since you have that problem with the return expression. Maybe say because of that you can’t unify with the return type

view this post on Zulip Brendan Hansknecht (Apr 24 2025 at 15:47):

I'm pretty sure the issue with the error message is that we do type checking from the inside out.

So you get the inner most error message even if a tiny bit of context from farther out could smek a better error message

view this post on Zulip Brendan Hansknecht (Apr 24 2025 at 15:48):

In this case, a statement in a function has a type error. So the functions type signature doesn't matter for the most part. Things are already broken before we even reach that.


Last updated: Jul 06 2025 at 12:14 UTC