josefs
Map showing multiple keys for documentation purpose.
I came along this example while playing with cowboy: https://github.com/ninenines/cowboy/blob/master/src/cowboy_http2.erl#L25-L68
I also recreated a simpler version:
-type one() :: #{
one => atom(),
two => atom()
}.
-type opts() :: one().
-spec test1(opts()) -> ok.
test1(Test) -> ok.
-spec test2() -> ok.
test2() ->
test1(#{two => two}).
We get this:
The map on line 15 at column 11 is expected to have type opts() but it has type #{two := two}
-spec test2() -> ok.
test2() ->
test1(#{two => two}).
^^^^^^^^^^^^^
I've boiled it down to this line in typechecker: https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L282
%% For M1 <: M2, mandatory fields in M2 must be mandatory fields in M1
I'm down to take care of this with a PR but before doing in, I'm wondering if this is what is expected. I've omitted the fact that in the cowboy version, the map signature has a _ => _ signature as well. I'm assuming all this does is allow any key to be in as well.
I would assume that writing a bunch of keys like so just means: here is all the possible key-value pairs you could put in the map. Should compat_ty here just try to find one matching pair?
That is not expected:
A map association has a key in AssociationList if it belongs to this type. AssociationList can contain both mandatory (:=) and optional (=>) association types. If an association type is mandatory, an association with that type needs to be present. In the case of an optional association type it is not required for the key type to be present.
So it's a bug? It's treating it as mandatory? I get this when I thread compat_ty
DEBUG: Ty1 = {type,0,map,
[{type,0,map_field_exact,[{atom,0,two},{atom,0,two}]}]}
DEBUG: Ty2 = {type,0,map,
[{type,0,map_field_assoc,[{atom,0,one},{type,0,atom,[]}]},
{type,0,map_field_assoc,[{atom,0,two},{type,0,atom,[]}]}]}
DEBUG: Ty1 = {type,0,map_field_assoc,[{atom,0,one},{type,0,atom,[]}]}
DEBUG: Ty2 = {type,0,map_field_exact,[{atom,0,two},{atom,0,two}]}
Yes, it's definitely a bug. Good report! We have several problems with map, perhaps even this one. Did you check for maps in known problems?
It seems that from the expression #{two => two} we infer the type #{two := two} and then check if it's a subtype of the expected type. Maybe we should instead infer the type {two => two} from this expression...? or perhaps we should check it in another way, without infering a type from the map expression..?
I checked and it's not in known problems as far as I can see. Good point about the wrong inference from #{two => two} to #{two := two}. Why would this happen, very weird. I'll take a look at that.
Isn't #{two := two} <: #{two => two, one => one}?
I think the current inference is correct. #{two => two} has the type #{two := two} since the key value pair is definitely (mandatorily) there.
So then this might be the problem: https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L271
It seems like in this case, the first type was the expression and the second was expected. We should always expect this order I assume. Then we just need to remove one of these clauses: https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L279-L281
The way map fields are checked in compat_ty is rather suboptimal. I think it'd be better to sort the fields on their keys. That way we can simply traverse the two lists of sorted assocs simultaneously and easily that all keys that should be present are there and have the proper subtypes.
@Zalastax
Isn't
#{two := two} <: #{two => two, one => one}?I think the current inference is correct.
#{two => two}has the type#{two := two}since the key value pair is definitely (mandatorily) there.
Yes, I agree, it's correct.
But I think @FrankBro is on the right track, almost. I think the maps might be swapped somehow... Why is assoc 2 before assoc 1? We need more extensive tests for subtype on maps! And some comments should be added to this code (https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L277-L285):
compat_ty({type, _, AssocTag2, [Key2, Val2]},
{type, _, AssocTag1, [Key1, Val1]}, A, TEnv)
when AssocTag2 == map_field_assoc, AssocTag1 == map_field_assoc;
AssocTag2 == map_field_exact, AssocTag1 == map_field_exact;
AssocTag2 == map_field_assoc, AssocTag1 == map_field_exact ->
%% For M1 <: M2, mandatory fields in M2 must be mandatory fields in M1
{A1, Cs1} = compat(Key1, Key2, A, TEnv),
{A2, Cs2} = compat(Val1, Val2, A1, TEnv),
{A2, constraints:combine(Cs1, Cs2)};
I think it'd be better to sort the fields on their keys. That way we can simply traverse the two lists of sorted assocs simultaneously and easily that all keys that should be present are there and have the proper subtypes.
@josefs They're not just atoms. The keys may be any type. We need to check that Key1 is a subtype of Key2 for some key types, which may not be easily sorted...
@josefs They're not just atoms. The keys may be any type. We need to check that Key1 is a subtype of Key2 for some key types, which may not be easily sorted...
Oh, right. Bollocks. There was a reason I wrote the code the way I did after all...
But I think @FrankBro is on the right track, almost. I think the maps might be swapped somehow... Why is assoc 2 before assoc 1? We need more extensive tests for subtype on maps! And some comments should be added to this code (https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L277-L285):
https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L110
%% The first argument is a "compatible subtype" of the second.
Actually I think it makes sense. The ResTy is always the second in all the usages I've checked. I think I'll just try to eliminate assoc one instead of doing it the other way around.
The problem seem to be that yes, it IS swapped: https://github.com/josefs/Gradualizer/blob/master/src/typechecker.erl#L273
{Ax, Cs2} = any_type(Assoc2, Assocs1, As, TEnv),
Assocs1 and Assocs2 are reverted there. I tried folding over Assocs1 instead of two. And changing the check right after to allow assoc on left and exact on right. Now my test case pass but a bunch of other tests don't.
The only other usage of any_type, the one for unions, respects having 1 on left and 2 on right so I'm assuming that's part of the problem.
I suggest checking the PR I just linked and checking the failing tests. One thing that's kinda funny, this used to pass but fail:
-spec union_value(#{a => b} | #{a => c}) -> #{a => b | c}.
union_value(M) -> M.
And this was a known problem but passes now:
-spec union_value2(#{a => b | c}) -> #{a => b} | #{a => c}.
union_value2(M) -> M.
Basically the opposite of each other.