weird behavior for "type alias of open record + extensions introducing field name overlap"

[tripack45]

The type checker behaves inconsistently in the following example, for values u and v, the type checker in some cases treats them as the same type but in other cases treats them as different types.

SSCCE

> type alias T a = { a | x : Int }
> u : T { x : Float }
| u = { x = 1 }
|
{ x = 1 } : T { x : Float }
> v : T { x : String }
| v = { x = 1 }
|
{ x = 1 } : T { x : String }
> u == v
-- TYPE MISMATCH ---------------------------------------------------------- REPL

I need both sides of (==) to be the same type:

10|   u == v
      ^^^^^^
The left side of (==) is:

    T { x : Float }

But the right side is:

    T { x : String }

Different types can never be equal though! Which side is messed up?

Hint: Want to convert a Float into a String? Use the String.fromFloat function!

> eq : { x : Int } -> { x : Int } -> Bool
| eq x y = x == y
|
<function> : { x : Int } -> { x : Int } -> Bool
> eq u v
True : Bool

• Elm: 0.19.1
• Browser: REPL
• Operating System: Ubuntu 20.04 WSL on Windows 10 20H2

Additional Details

I haven't looked at the compiler code but I believe the root cause lies in the fact that the Elm compiler tests type equality through structural equality even in the face of type aliases. In other words, the algorithm unifies T a with T b by unifying a with b, even when T is a type alias. This is of course in general incorrect, as definitions such as type alias T a = Int exists, and therefore T a = T b for arbitrary a and b in those cases.

Elm seems to be trying to get around it by banning phantom type variables, hoping that situation like the case above never arise, because the aliased type mentions a anywhere then T a and T b cannot be the same type because they will be different at the place where the type variable is mentioned.

Unfortunately this seems to break down in the face of row types. The type { a | x : Int } does not just extend rows a with field x : Int, it may also update field x in a if x happens to also exists in a. This creates a situation that violates the assumption above, causing the type checker to behave weirdly.

I believe the solution to the problem in general is to first normalize and substitute away all type aliases.

[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.

[Warry]

Hi !

It looks like it's related to the fact that both Float and Int can be inferred from a digit. Very spooky and edge-casey. This doesn't work with any other type overriding.

[tripack45]

Hi !

It looks like it's related to the fact that both Float and Int can be inferred from a digit. Very spooky and edge-casey. This doesn't work with any other type overriding.

I don't think this is the root cause. You can reproduce the same issue with completely unrelated types:

> type I = I
> type alias T a = { a | x : I }
> u : T { x : Float }
| u = { x = I }
|
{ x = I } : T { x : Float }
> v : T { x : String }
| v = { x = I }
|
{ x = I } : T { x : String }
> u == v
-- TYPE MISMATCH ---------------------------------------------------------- REPL

I need both sides of (==) to be the same type:

11|   u == v
      ^^^^^^
The left side of (==) is:

    T { x : Float }

But the right side is:

    T { x : String }

Different types can never be equal though! Which side is messed up?

Hint: Want to convert a Float into a String? Use the String.fromFloat function!

> eq : { x : I } -> { x : I } -> Bool
| eq x y = x == y
|
<function> : { x : I } -> { x : I } -> Bool
> eq u v
True : Bool

I believe the issue stems from the fact that Elm compiler does not normalize type aliases when testing type equality.

[Warry]

Strange that v : T { x : String } \n v = { x = I } even compiles !

here is what I tried: