Extensible record fails to unify with full record

[gampleman]

Quick Summary: Using an extensible record wrapped in a custom type fails to unify once passed through a function.

SSCCE

type alias Foo a =
    { a | foo : Int }

type alias Bar =
    Foo { abc : String }

type alias Baz =
    Foo { abc : Maybe String }

type OneOrTheOther
    = BarBranch Bar
    | BazBranch Baz

map : (Foo a -> Foo a) -> OneOrTheOther -> OneOrTheOther
map fn thing =
    case thing of
        BarBranch f ->
            BarBranch (fn f)

        BazBranch f ->
            BazBranch (fn f)

fails with:

Type Mismatch
The 1st argument to `BarBranch` is not what I expect:

29|             BarBranch (fn f)
                           ^^^^
This `fn` call produces:

    Foo a

But `BarBranch` needs the 1st argument to be:

    { abc : String, foo : Int }

Hint: Looks like the abc field is missing.

Type Mismatch

The 1st argument to `fn` is not what I expect:

29|             BarBranch (fn f)
                              ^
This `f` value is a:

    Bar

But `fn` needs the 1st argument to be:

    { a | foo : Int }

Hint: Seems like a record field typo. Maybe abc should be foo?

Hint: Can more type annotations be added? Type annotations always help me give
more specific messages, and I think they could help a lot in this case!

See Ellie.

I suspected that this might just be a case of let polymorphism, so I tried this alternative version:

map : (Foo a -> Foo a) -> (Foo b -> Foo b) -> OneOrTheOther -> OneOrTheOther
map fn1 fn2 thing =
    case thing of
        BarBranch f ->
            BarBranch (fn1 f)

        BazBranch f ->
            BazBranch (fn2 f)

Which fails with basically the same error

``` Type Mismatch The 1st argument to `BazBranch` is not what I expect: 32| BazBranch (fn2 f) ^^^^^ This `fn2` call produces: Foo b But `BazBranch` needs the 1st argument to be: { abc : Maybe String, foo : Int } Hint: Looks like the abc field is missing. Type Mismatch [Line 32, Column 28](https://github.com/elm/compiler/issues/new) The 1st argument to `fn2` is not what I expect: 32| BazBranch (fn2 f) ^ This `f` value is a: Baz But `fn2` needs the 1st argument to be: { b | foo : Int } Hint: Seems like a record field typo. Maybe abc should be foo? Hint: Can more type annotations be added? Type annotations always help me give more specific messages, and I think they could help a lot in this case! Type Mismatch The 1st argument to `BarBranch` is not what I expect: 29| BarBranch (fn1 f) ^^^^^ This `fn1` call produces: Foo a But `BarBranch` needs the 1st argument to be: { abc : String, foo : Int } Hint: Looks like the abc field is missing. Type Mismatch The 1st argument to `fn1` is not what I expect: 29| BarBranch (fn1 f) ^ This `f` value is a: Bar But `fn1` needs the 1st argument to be: { a | foo : Int } Hint: Seems like a record field typo. Maybe abc should be foo? Hint: Can more type annotations be added? Type annotations always help me give more specific messages, and I think they could help a lot in this case! ```

See Ellie.

• Elm: 0.19.1
• Operating System: OSX 11.6

[github-actions[bot]]

Thanks for reporting this! To set expectations:

• Issues are reviewed in batches, so it can take some time to get a response.
• Ask questions in a community forum. You will get an answer quicker that way!
• If you experience something similar, open a new issue. We like duplicates.

Finally, please be patient with the core team. They are trying their best with limited resources.

[zwilias]

Consider the type signature:

map : (Foo a -> Foo a) -> OneOrTheOther -> OneOrTheOther

What if I defined this:

addABean : Foo { beans : Int } -> Foo { beans : Int }
addABean foo = { foo | beans = foo.beans + 1 }

The typesignature of map definitely allows me to pass addABean as the first argument. It doesn't say a should be unbound, it only need to have the "pattern" a -> a (whatever a may be!) Extensible record syntax makes this somewhat harder to wrap your mind around, but this isn't that different from something like this:

map : (a -> a) -> String -> String

Where you may wish for (a -> a) to be a stand-in for identity, but I can also pass (\x -> x + 1) : Int -> Int.

In order to specify that you want the a and b to be unbound, you need something known as higher ranked types, which Elm doesn't have. For example, in haskell.

[gampleman]

Ah gotcha so this is actually correct behaviour and I’m only making an incorrect closed world assumption.

The only issue here is perhaps the error message could be a bit better at explaining the situation.