Stream: bugs

Topic: Weird bug with type inference/unification


view this post on Zulip Ian McLerran (Feb 03 2025 at 16:52):

So I have a weird bug with type checking:

I have a collection of parsers of various types. I have another parser which combines two other types of parsers in a list passed to the one_of combinator.

The parsers passed to one_of each returns a Tag type, so they should be able to unify in a list as a Tag union. This was working just fine previously, however I replaced one of the parsers in the list with another parser of the IDENTICAL type signature to the parser it replaced. Now it refuses to type check, saying the items in the list do not have the same type.

Here is a sample of the original, working code:

unescaped_character : Parser [Char U8] [CharNotFound]
character_range : Parser [CharRange (U8, U8)] [InvalidCharacterRange]

character_group_item : Parser [Char U8, CharRange(U8, U8)] [InvalidCharacterGroupItem]
character_group_item = |str|
    parser = one_of([character_range, unescaped_character])
    # List above is infered as:
    # List (Parser.Parser [Char U8, CharRange ( U8, U8 )*] [CharNotFound, InvalidCharacterRange])
    parser(str) |> Result.map_err(|_| InvalidCharacterGroupItem)

but if I replace unescaped_character with character:

character : Parser [Char U8] [CharNotFound]

In the call to one_of, I get a type mismatch error in the list, even though character has the identical type signature to unescaped_character

view this post on Zulip Brendan Hansknecht (Feb 03 2025 at 17:13):

Either would be an issue with the underlying lambdaset or an issue with tag unification/being open vs closed.

view this post on Zulip Brendan Hansknecht (Feb 03 2025 at 17:13):

At least that is my guess

view this post on Zulip Ian McLerran (Feb 03 2025 at 17:20):

I thought it might have to do with tag unions being open or closed, as I encountered a similar issue, where I had to make one specific Parser in a list of parsers use an open tag union for it's second type parameter in order for the list to unify.

view this post on Zulip Ian McLerran (Feb 03 2025 at 17:20):

However in this case, I tried using underscores to open up every tag union involved, however this didn't help in this case. So maybe its something to do with the lambda set? Not sure if that info eliminates the possibility of an issue with open/closed tag unions, but seems like it should...

view this post on Zulip Brendan Hansknecht (Feb 03 2025 at 17:29):

What is the actual printed error?

view this post on Zulip Ian McLerran (Feb 03 2025 at 17:30):

Okay, I was able to rectify the issue. There was an open Tag union return type up the call chain inside character. This should have been closed by Result.map_err, in character, which mapped all errors to a singular type, but apparently it was still being considered an open type, even though it didn't complain about my use of a closed tag union for the err type in character's type signature.

view this post on Zulip Ian McLerran (Feb 03 2025 at 17:42):

Okay, now this is really strange - this was the root of the problem:

The following works fine:

character_excluding_escaped : Parser Character [CharNotFound]
character_excluding_escaped = |str|
    parser = character_excluding(['.', '^', '$', '*', '+', '?', '(', ')', '[', ']', '{', '}', '|', '\\', '/', '-', ' '])
    parser(str)

However, this does not:

character_excluding_escaped : Parser Character [CharNotFound]
character_excluding_escaped =
    character_excluding(['.', '^', '$', '*', '+', '?', '(', ')', '[', ']', '{', '}', '|', '\\', '/', '-', ' '])

Despite the fact that character_excluding returns a closed Tag union error type of [CharNotFound], and despite the fact that I have not even called Result.map_err, or done anything else to close the tag union in the second version, just used a def before calling character_excluding, the second version here shows in type inference that it returns an additional error type in its tag union, despite the fact that character_excluding is annotated as a closed type, and uses map_err to ensure that it only ever returns one error type.

view this post on Zulip Brendan Hansknecht (Feb 03 2025 at 18:05):

Returned tags are always open

view this post on Zulip Ian McLerran (Feb 03 2025 at 19:04):

Hmm… that makes sense, I guess I actually knew that. Although why parser : Parser ok [ErrTag] didn’t work in a list with other parser types, but parser : Parser ok [ErrTag]_ was accepted is unclear to me… (similar but different upstream issue from my original post issue).

view this post on Zulip Brendan Hansknecht (Feb 03 2025 at 19:23):

Cause if the tag is wrapped in a type, it is closed....real struggle/inconsistency


Last updated: Jul 26 2025 at 12:14 UTC