number not accepted as comparable

[jvoigtlaender]

This program should successfully type-check:

import Dict exposing (Dict)

f : List (number, ()) -> Dict number ()
f = Dict.fromList

But it is rejected by 0.16 at http://elm-lang.org/try.

The error message is:

The type annotation is saying:

    List ( number, () ) -> Dict number ()

But I am inferring that the definition has this type:

    List ( comparable, a ) -> Dict comparable a

But numbers are comparable, so one should be allowed to specialize the latter type to the former.

[jvoigtlaender]

Here's an example not involving Dict:

g : comparable -> ()
g _ = ()

f : number -> ()
f = g

Should be accepted, but isn't.

[jvoigtlaender]

In some sense this error is dual to that reported in #1270. Maybe the "super/sub relationship" between number and comparable is implemented wrongly in the compiler?

We have that every number type is also a comparable type. So both the following should hold:

1. Whenever we have a polymorphic function of a type of the form ... -> comparable -> ... we should also be allowed to give it the type ... -> number -> ....
2. When the inferred type of a function is ... -> number -> ... we should not be allowed to give it the type ... -> comparable -> ... (since if the type-checker inferred number there, some number literals or arithmetic operations appeared in the function, so typing it to comparable will be wrong).

Now what the issue here shows is that 1. is violated by the compiler, while the issue #1270 shows that 2. is violated by the compiler.

So maybe somewhere in the compiler instead of "every number type is also a comparable type" it is implemented that "every comparable type is also a number type"?

[mgold]

A good theory, but this code seems correct. Unless there's some weird contravariance going on?

[mgold]

Wait, what about here? If I read it right, the result of combineSupers is only used if it is the same as the second argument. If we got rid of the guard, would it work?

[jvoigtlaender]

Do we know that that is the relevant code to look at? I don't know the structure of the compiler/type-checker well enough to judge. My question probably is: Is that code the code that runs when one has inferred a type for some function definition and is now checking whether the type annotation the programmer gave for that function definition is a specialization of the inferred type? Note that this is really about specialization, not about unification. The types a -> Int and Int -> b unify, but none is a specialization of the other. So if for a function definition one happens to infer a -> Int, but the annotated type is Int -> b, the type-checking should fail.

[mgold]

I'm also not too familiar with the compiler's structure, but search for "comparable" and there are only three source files that turn up. So I can be pretty confident that this function, for example, is why you can't write compappend in a type annotation.

I can try compiling from source with a change and see if it works.

[mgold]

It turns out that removing that guard does cause the original program to type check. But, what I didn't see in previous comments is that combineSupers is called in three places. Two of them, both in the context of Rigid types, use the guard; one of them does not and it's in the context of a Flexible type. I can guess that the guard is intended to allow some kind of contravariance, where a function that must accept any comparable should not be limited to numbers, or similar.

Having looked over the file for some time, my next question is, what's the difference between a flexible and a rigid type variable? After some googling I couldn't find a satisfactory answer.

[evancz]

This seems like the right direction.

A "rigid" variable is one that is given by the programmer in a type annotation. If someone says "the type is a -> String" the compiler will treat a as rigid, meaning that it cannot be unified with any concrete type (like Int or a record). If we had to unify the user-defined a with a concrete type, it would mean the type annotation was a lie.

A "flexible" variable is one that is created by the compiler. So the compiler may know that something has type a -> String but all that means is that we haven't pinned a down to anything more specific yet.

[mgold]

Thanks Evan, that's very helpful!

So in the example in the second post, both comparable and number are rigid type variables. Which would imply this is the code that needs to be looked at. I would probably need the guard to prevent a function on numbers being claimed to work for all comparables.

I'm not entirely confident in this though, because I'm not sure how a -> a is successfully typechecked, I'd imagine it would have to take the same path of unifying two rigid variables.

As much as I enjoy diving into this and would appreciate any other information Evan could offer, it's probably best just to wait for him to fix it.

[evancz]

When you use a value, it is "generalized" so you end up with all flexible variables. Rigid variables should only show up when you are checking type annotations, not at other times.

Ultimately, I'd need to dig into this directly to give any further insight, but at this point, I think it has been really narrowed down, so that should be pretty easy when I get a chance!

[mgold]

Thanks, glad I could help and learn something about type checking at the same time.

[mgold]

Here is an example of this bug "in the wild".

[evancz]

Centralizing into #1373, will track from there.

[jvoigtlaender]

Here is an example that seems related, maybe is an instance of this bug, but appears to be new with Elm 0.18:

f : number -> number -> Bool
f x y = x < y

Should be accepted by the compiler, but is not (http://elm-lang.org/try in 0.18 version).

According to a thread on the mailing list, https://groups.google.com/d/msg/elm-discuss/om6l_lvCr_4/uiA7zFcvBQAJ, by someone who encountered this in real code, the 0.17 version of the compiler handled this correctly.

[stevensonmt]

Has there been a regression in this bug since the May 11, 2017 fix referenced above? I am getting the following error message when trying to implement a comparison function with a number type:

The left argument of (<) is causing a type mismatch.

170|     score < 320
         ^^^^^
(<) is expecting the left argument to be a:

    comparable

But the left argument is:

    number

Hint: Only ints, floats, chars, strings, lists, and tuples are comparable.

[jvoigtlaender]

@stevensonmt, there hasn't been a release of the compiler between May 2017 and now (actually, between November 2016 and now), so unless you are using an unreleased version of the compiler, you are not having that fix in the compiler on your machine.

[stevensonmt]

ah, got it. Thanks.