Invalid polymorphic code accepted

[erszcz]

The following code is correctly rejected by Gradualizer:

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

However, the following code is not rejected:

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

while by itself it seems harmless. We could argue whether the above code is valid or not based on polymorphism rank we'd like to support (rank-1 - invalid, rank-2 - valid). However, an invalid application like the following should be rejected in any case, whereas it's not:

-gradualizer([solve_constraints]).

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

-spec take_boolean(boolean()) -> boolean().
take_boolean(B) -> B.

-spec should_be_rejected() -> {integer(), integer()}.
should_be_rejected() ->
    poly_2(fun take_boolean/1).

See WhatsApp/eqwalizer#33 for the original issue where this was spotted.

[xxdavid]

Hi @erszcz and thanks for your investigation!

Maybe I'm wrong but I think we have to stick to rank-1 polymorphism as we don't even have syntax for higher-rank polymorphism in the Erlang typespecs. To support rank-2 polymorphism, you would have to be able to specify the "scope" in which type variables are bound and quantified.

For example, in System F, this is done via the for-all sign. Take for example these two types: ∀A. (A → A) → integer() and (∀A. A → A) → integer(). They are similar but different. The first type corresponds to a function that takes a function that always takes some type and outputs the same type (e.g. the successor function, logical negation, or even the identity function). The second one corresponds to a function that takes a function that can take any type and always outputs the same type that it inputs (e.g. the identity function). In programming languages, the outer for-all is typically implicit, e.g. (a -> a) -> Integer in Haskell means actually ∀A. (A → A) → Integer. If you want to have the for-all inside (i.e. use higher-rank types), you have to be explicit, for example (forall a. a -> a) -> Integer (Haskell with RankNTypes extension enabled) which naturally translates to the (∀A. A → A) → Integer type.

But AFAIK in typespecs we don't have any way ho to specify the scopes in which type variables are bound and quantified, and thus all type variables are implicitly quantified over the whole term (i.e. rank-1). It is true that the runtime can handle higher-rank polymorphic functions. But I think this is true for any dynamically typed language.

What do you think?

I agree that the second snippet

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

should be rejected as the type variable A could be instantiated to anything, and the callee (poly_2) has no guarantee that it is indeed a supertype of 42 | 84. Even in Haskell, the following snippet is ill-typed:

poly_2 :: (a -> a) -> (Integer, Integer)
poly_2 f = (f 42, f 84)

In the last snippet, I think the issue is again in the function poly_2, as its spec is incorrect. The call poly_2(fun take_boolean/1) is alright given the spec -spec poly_2(fun((A) -> A)) -> {integer(), integer()} which says that poly_2 takes any function that takes some value and returns a value of the same type (which take_boolean does).

Maybe I was needlessly explaining something you know well, I just wanted to be sure that we all have the same understanding of it.

[erszcz]

Hi, @xxdavid!

Maybe I'm wrong but I think we have to stick to rank-1 polymorphism as we don't even have syntax for higher-rank polymorphism [...]

Good thinking. We're generally on the same page here.

If we really, really wanted to work around the existing syntax, we could introduce some abomination like when A :: gradualizer:forall(A) to denote that the first occurrence of A should be treated as though it had a nested quantifier. That is, keep the syntax, add extra semantics. But I really don't think we need it. We should stick to rank-1 types. I mentioned both rank-1 and rank-2, since I don't think it was ever stated anywhere what Gradualizer's goal in this regard is.

I agree that the second snippet [...] should be rejected [...]

I'm not sure if that's strictly necessary, but it would make sense. After all the caller could pass in a fun(integer()) -> integer(), so we don't know until poly_2 is called. Definitely, though, we should register a constraint A :: integer(), and therefore the only accepted function should be fun(integer()) -> integer(). There are ToDo items in the source to do it properly:

Gradualizer/src/typechecker.erl

Line 3839 in 01fb022

%% TODO: don't drop the constraints!

Gradualizer/src/typechecker.erl

Line 3875 in 01fb022

%% TODO: return the right constraints - we should store them in Acc

If we registered these constraints above, I think should_be_rejected/0 would actually be rejected, but the definition of poly_2:

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

would not, given the current constraint solving logic. The solver currently throws an error if constraints conflict. In case of poly_2 we would have:

• A :> 42 | 84
• A <: integer()

which do not conflict.

These are not the only places where we don't registers/pass constraints, but these seem relevant to this bug.