Stream: beginners

Topic: Rank-2 limitation? (and an error message)

Jonathan (Aug 27 2026 at 10:48):

Apologies for the long post, my main questions are in some bullet points below if TL;DR :).
I was working on something I probably shouldn't have, and at some point the type-foo is a certain code smell, but I can't help but try because it's there. Anyhow, the problem distills to this example.

Mod :: [].{
    # Commented out type sig (for now)
    # f1 : List(U32) -> List(U64)
    f1 = |l| {
        l.map(|i| U32.to_u64(i))
    }
    f2 = |l| {
        l.map(|i| U32.to_u128(i))
    }

    g = |l| {
        a1 = f1(l)
        a2 = f2(l)  # -- Error --

        0 # (To give a return val)
    }
}

With this confusing error message about a2 = f2(l) that appears to show a failed unification between two ostensibly equal types:

This argument has the type:

    a where [a.map : a, (U32 -> U64) -> _ret]

But main.Mod.f2 needs the first argument to be:

    a where [a.map : a, (U32 -> U64) -> _ret]

That message isn't telling me what's wrong , but I can kind of see that we are passing the same l and using the same underlying map method, but using it in a different way (giving U128 or U64). As soon as there is the annotation that narrows it to, e.g., a list, the error disappears.

I am guessing that this is something to do with both/either rank-2 polymorphism (I think it would need existential quantifiers? Universal?) or higher-kinded types (something that holds an a that can map it to a b).

What surprised me though, is how such a simple example can trigger it. I know rank-2 is off the table, but this means that I can't pass a polymorphic method of a generic module down the call stack and use it with different types, at least without first explicitly narrowing it. The consequence is that any library that uses different instantiations of user provided types (e.g., custom containers) will be limited?

I guess what I'm wondering is

• Could that error message be made more clear?
• Is this a rank-1 limitation as I have understood it (or something more interesting? I'm curious)
• Would it be possible to have slightly more flexibility by delaying the specialisation of a generic member function included in a where-constraint until its use cases separately? I.e., the first l.map(...) is a different specialisation to the second l.map(...). Specifically, can the general non-receiver type parameters be preserved, rather than pinned on first use?

And also a thought that structural typing and static dispatch appears at first to be incredibly flexible, until you bounce against the underlying rank-1 HM inference.

The concrete (if ill-advisable) use-case I have right now is a little utility library for some sqlite queries in a project database. I can define each query relative to 'the receiver whose associated module defines query_many!', but I cannot use these helpers together without first providing the concrete basic-cli.Sqlite module, because the output type of query_many! varies with the decoder you provide, but the generic query_many! has already specialised to its first use.

I should really change this to be a module of an application, and have the application be the entry point to the scripts, but I think the questions above still stand.

## Planning stage of a reconciler. Determines the flow stages that need to
## be executed next.
# plan! : Query(sqlite, path) => List(a)
    #   where [
    # ...
    #       sqlite.query_many! : { path : path, query : Str, bindings : List({ name : Str, value : [Null, Real(F64), Integer(I64), String(Str), Bytes(List(U8))] }), rows : (cols -> (stmt => Try(row, derr))) } => Try(List(row), err),
    #   ]
plan! = |q| {
  # jobs referred to by I64 ids
  jobs = Query.Analyses.analyses_lacking_jobs_of_stage!(q, { experiment_id: 1, stage: "A", replica: 0, deps: [] })

  # batches referred to by string names
  batches = Query.Batches.batches_to_poll!(q, 5) # <-- Errors
  # Error : same as above essentially (reported types that look the same can't unify)
  # but I'm guessing it's because the second underlying `query_many!` returns and uses
  # decoders for Str not I64
}

# If I used this in application code not a library, it would be ok. The problem
# is that the module handle `q` is used under-the-hood for `query_many!`, returning
# different types, but is pinned after its first use to only work with I64.
# If I specify a `sqlite.query_many!` for some *generic* output decoder type (paramaterised
# by `row`) to a where constraint of plan!, I get an error saying ~
# It has the type (... decoder: I64 ...) but you are trying to use it as type (... decoder: row ...)

Richard Feldman (Aug 28 2026 at 00:44):

I think the error message is just wrong :sweat_smile:

Richard Feldman (Aug 28 2026 at 00:46):

it should say that main.Mod.f2 needs the map to do U32 -> U128 because that function returns U32.to_u128, which means that map function's return type should be U128 - but the error message claims it's U64

Richard Feldman (Aug 28 2026 at 00:47):

so maybe the error message is printing the same type twice - @Jonathan would you mind opening a GitHub issue for this?

Jonathan (Aug 28 2026 at 08:19):

Sure, can do - I think it's wrong too. But isn't the underlying reason for the message because map specialises on first use to something that accepts X, but then the second use of it tries it with Y?

Richard Feldman (Aug 28 2026 at 12:29):

it's nothing special - just that it's saying "this type has a map function with shape A" and also "that same type has a map function with shape B" and A and B are incompatible, so it's a type mismatch :smile:

Richard Feldman (Aug 28 2026 at 12:29):

the same type can't possibly have a map function with two different incompatible types, which is what this code is asking for

Jonathan (Aug 28 2026 at 12:38):

But when it is annotated as a list, there is no error and it satisfies both. I.e., there is a type that can satisfy both, it just requires map to be polymorphic and have separate instantiations for different type parameters?

Richard Feldman (Aug 28 2026 at 12:41):

if you add an annotation the type checker accepts it? What's the annotation? :thinking:

Jonathan (Aug 28 2026 at 12:42):

Yeh it's just the one I left commented out at the top of the first code block.

Jonathan (Aug 28 2026 at 12:43):

It pins l to be a list of U32. Then both f1 and f2 can work. But I think they can't when l is "something with a map".

Richard Feldman (Aug 28 2026 at 12:55):

oh I see, hm

Richard Feldman (Aug 28 2026 at 12:56):

ok I think I misunderstood the original error

Richard Feldman (Aug 28 2026 at 15:23):

ok, I may regret this later but I want to try it out :sweat_smile:

I'm gonna try out having this infer as:

g : a -> U8 where [
    a.map : a, (U32 -> U64) -> _b,
    a.map : a, (U32 -> U128) -> _c,
]

so basically, what this is saying is:

"a must have a map method which is compatible with both of these types"

Richard Feldman (Aug 28 2026 at 15:25):

in other words, "it's generic somehow but we don't know exactly how it's generic yet"

Richard Feldman (Aug 28 2026 at 16:44):

so without this, we don't have principal type inference - because you can (as demonstrated at the top of this thread) add a type annotation which increases flexibility, which should not be possible if we are inferring principal types

Richard Feldman (Aug 28 2026 at 16:44):

so this change means that the above should Just Work

Richard Feldman (Aug 28 2026 at 16:47):

I think it could potentially also lead to nicer error messages, because if you infer multiple conflicting constraints, we can remember where both of the constraints came from, so we can say like "we have Constraint A from this usage over here, and we have Constraint B from this other usage over here, and one of these is incompatible with how you're using it in this place"

Richard Feldman (Aug 28 2026 at 16:50):

downsides:

• it becomes possible to write a method constraint in a new way. I believe that in general, these offer less-nice ways to express your constraints than what's currently available; that is, I think there should always be a way to express a valid constraint more concisely than this, so I don't know why anyone would use this on purpose (as opposed to type inference inferring them because it doesn't know a better way to infer them, and then you can make it nicer with a more concise annotation)
• in theory it can lead to type constraints accumulating in un-annotated programs in a way that could make performance worse. I am not worried about this in practice, because it has taken this long to find a single example of two constraints on the same method coming up, so I suspect this will be one of those things where in theory it can be slow, but in practice nobody would use it in a way where it would be a problem in practice. (This is especially true because as soon as type annotations are in the mix, this no longer even comes up.)

Richard Feldman (Aug 28 2026 at 16:51):

there's also arguably a "learning curve" downside - but again, I don't think this will come up much in practice, and I wouldn't be surprised if most Roc programmers never even run into this, and are eventually surprised the first time it comes up

Jonathan (Aug 29 2026 at 01:54):

Yeh the way it came up was kind of cursed, but then it distilled to something that was actually quite simple. I imagined something that needed to be generic over a container, but I think it's uncommon to do multiple different things with the same generic variable.

Anyhow, that seems like quite a clean solution and kind of a sneaky end-run around rank-2 I think by not having to say "this works for all as" and instead "it needs to work for these specific as". I'm sure there'll be downstream effects so it'll be interesting to see how it plays out.

Jonathan (Aug 29 2026 at 01:55):

Thanks for taking a look and considering it :octopus:

Richard Feldman (Aug 29 2026 at 02:12):

thanks for the detailed report! :smiley:

Richard Feldman (Aug 30 2026 at 02:02):

@Jonathan can you try on current main? This pr implemented the fix I described above, so the original program should work now!

Jonathan (Aug 30 2026 at 10:14):

Will do! It might be a day or so until I'm back at the 'puter though. Quite excited!

Jonathan (Sep 01 2026 at 09:28):

Ok! Seems to work for the simple case with two different uses of map on a generic argument and inferred types, or with the function annotated as (f1 : a, (U32 -> U64) -> b etc.).

Outside of something more hairy that I haven't yet managed to minimise, I have two problems so far with variations of simple example above:

<removed here because I made a mistake and it was getting confusing>

Second problem is you can't annotate the inferred type conjunction manually. The following errors:

    # The below type was copied from the LSP hover
    g : a -> b where [a.map : a, (U32 -> U128) -> b, a.map : a, (U32 -> U64) -> _ret]
                                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    g = |l| {
        a1 = f1(l)
        a2 = f2(l)
        a2
    }

The error highlights the second map constraint in g's signature:

It has the type:
a, (U32 -> U64) -> _ret where [a.map : a, (U32 -> U128) -> _ret]
But you are trying to use it as:
a, (U32 -> U128) -> _ret where [a.map : a, (U32 -> U128) -> _ret2]

Jonathan (Sep 01 2026 at 12:31):

Sorry Richard, I was editing the prior comment because I thought I'd made a mistake, and indirectly made a new mistake. I've removed it for clarity from before and I'll add it below.

• You can't manually annotate the function with the separate uses (g) with the same conjunction type as is now inferred by the compiler (see prior message)
• Annotating the separate uses (f1 or f2) with the same type as inferred by the compiler leads to the following error

    f1 : a -> b where [a.map : a, (U32 -> U64) -> b]
    f1 = |l| {
        l.map(|i| U32.to_u64(i))
    }

    f2 : c -> d where [c.map : c, (U32 -> U128) -> d]
    f2 = |l| {
        l.map(|i| U32.to_u128(i))
    }

    g = |l| {
        a1 = f1(l)
        a2 = f2(l)
        a2
    }

Error

The first argument being passed to this function has the wrong type.

a2 = f2(l)
        ^

The type involved is:

    a where [a.map : a, (U32 -> U64) -> b]

The difference is inside this type, but it is not visible in this display.

Last updated: Sep 03 2026 at 15:16 UTC