Incorrect type inference for = ?

[ineol]

Equality does not imply the inequality of the types of the expressions that are compared.

eg the inferred type of

let f x y = x = y

is a -> b -> bool instead of a -> a -> bool

[matijapretnar]

Yes, just like #11, this is due to the complications with sub-typing - the types of the two arguments aren't comparable (none is smaller than the other), they just share a common supertype. I'm working on a new implementation of the effect system and hope to fix the issue soon.

[andrejbauer]

So you get x : a and y : b and a ≤ c‘ andb ≤ c`? Perhaps when the algorithm is not printing out the constraints, it should equate any two types that have a chain of inequalities between them?

[matijapretnar]

Yes, but the two constraints get garbage collected because c doesn't appear anywhere. The solution is to keep track of skeletons as well. The new effect system already does that. I just need to sort out the desugaring of types for the external definitions.

[andrejbauer]

Please do :-)

[matijapretnar]

Closed by #32.