Open tripack45 opened 3 years ago
Thanks for reporting this! To set expectations:
Finally, please be patient with the core team. They are trying their best with limited resources.
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.
Hi !
It looks like it's related to the fact that both
Float
andInt
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.
Strange that v : T { x : String } \n v = { x = I }
even compiles !
here is what I tried:
The type checker behaves inconsistently in the following example, for values
u
andv
, the type checker in some cases treats them as the same type but in other cases treats them as different types.SSCCE
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
withT b
by unifyinga
withb
, even whenT
is a type alias. This is of course in general incorrect, as definitions such astype alias T a = Int
exists, and thereforeT a = T b
for arbitrarya
andb
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 thenT a
andT 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 rowsa
with fieldx : Int
, it may also update fieldx
ina
ifx
happens to also exists ina
. 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.