Type-checking bug: comparable vs. number

[jvoigtlaender]

Short version:

Should the following program type-check?

f : comparable -> comparable
f _ = 0

I don't think so, but the current compiler accepts that program.

Long version:

If I have a module B defining and exporting some function f : comparable -> comparable, should I be able to use it as follows in another module?

module A where

import B exposing (f)

test = f 'a'

I think so. After all, 'a' is a Char, and type Char is comparable, so 'a' should be a valid input for any function of type comparable -> comparable. However, the following module breaks that expectation:

module B where

f : comparable -> comparable
f _ = 0

And down goes separate compilation. (Module B on its own compiles, so the compiler asserts that the f in there really has type comparable -> comparable. Module A should compile under the assumption that f has type comparable -> comparable. But modules A and B together do not compile.)

[jvoigtlaender]

It's possible that this is somehow the same bug, or has the same root cause, as #1268.

[mgold]

What should happen is that 0 : number is unified with the second comparable, which causes the first comparable to be unified with number, resulting in an inferred type of number -> number. The annotation should then be rejected as too general.

I think the larger problem is that we have these three not-quite-type-classes hacked into the language, and so edge cases like this one arise. It might have to wait until implicit parameters or whatever not-type-classes language feature comes along. That is, even if you manage to fix this bug without causing regressions, it might not be worth it if something big comes along in 0.19.

[jvoigtlaender]

For a start, I'd like to know whether @evancz agrees this is a bug.

[evancz]

I think so. comparable should be too general.

[evancz]

Centralizing into #1373, will track from there.