Valid (or not?) polymorphic code rejected

[erszcz]

I've run this comparison between Gradualizer / Etylizer / Eqwalizer I mentioned in the other ticket and I'm now going through the cases where the type checkers' results differ on the same code snippets. Some differences are due to different interpretation of any() and dynamic(), the dynamic types in Gradualizer and Eqwalizer, respectively. Some are about handling of intersection/union types. The raw comparison results are available here. Apologies for not much commentary there - it's a work in progress.

To the point... Eqwalizer correctly rejects the below code:

-spec poly_2(fun((A) -> A)) -> {integer(), boolean()}.
poly_2(F) -> {F(42), F(false)}.

-spec poly_fail(fun((A) -> A), boolean(), integer()) -> {boolean(), integer()}.
poly_fail(F, B, I) -> {F(I), F(B)}.

With the assumption that only rank-1 types are supported (which does not really reflect the BEAM runtime), the constraints towards A in both cases lead to a conflict. However, there's no such conflict in the below case, which is also rejected by Eqwalizer:

-spec poly_2(fun((A) -> A)) -> {integer(), integer()}.
poly_2(F) -> {F(42), F(84)}.

-spec poly_pass(fun((A) -> A), boolean(), boolean()) -> {boolean(), boolean()}.
poly_pass(F, B1, B2) -> {F(B2), F(B1)}.

I'm running:

$ asdf current erlang
erlang          25.3.2          /Users/erszcz/.tool-versions
$ /Users/erszcz/work/erszcz/erlang-type-checker-comparison/elp version
elp 0.17.16

[VLanvin]

You're right that eqWAlizer only supports rank-1 polymorphism. All type variables are implicitly universally quantified at the outermost position. Which is also the reason the second example is rejected.

Consider your second poly_2 function:

-spec poly_2(fun((A) -> A)) -> {integer(), integer()}.
poly_2(F) -> {F(42), F(84)}.

Since A is externally quantified, the only constraint the spec imposes to the argument is that its return type is the same as its input type. It does not, in particular, state that it can be applied to any value (which would require an inner quantifier, with higher rank polymorphism). So in particular, a function of type fun(boolean()) -> boolean() can be passed to poly_2. Because such an application would lead to an ill-typed term, it's clear the spec should be rejected.

[erszcz]

Thanks, that's a convincing explanation, indeed! I guess we can close this ticket, then :)