Multiple map key patterns raise an unexpected type check error

[javiergarea]

Current behaviour

Given the following spec and implementation:

-spec check(Input :: #{binary() => integer()}) -> integer() | error.
check(#{<<"a">> := A}) ->
    A;
check(#{<<"b">> := B}) ->
    B;
check(_Other) ->
    error.

gradualizer raises a The expression <<"b">> on line 13 at column 9 is not a valid key in the map type #{}.

Expected behaviour

No type check errors.

Notes

• Minimal repo to reproduce the issue: here.

[erszcz]

Thanks for raising this, @javiergarea!

This is a problem caused by refining a map key with a match-all binary() even though the matched pattern is just a singleton binary. With some print-debugging, we see it clearly:

$ ~/work/erszcz/gradualizer/bin/gradualizer src/gradualizer_maps.erl
assoc_tys: [{type,0,map_field_assoc,[{var,0,'_'},{type,0,integer,[]}]}]
assoc_tys: []
src/gradualizer_maps.erl: The expression <<"b">> on line 13 at column 9 is not a valid key in the map type #{}

I think we'll have to drop exhaustiveness checking on maps to solve this, at least in the short/mid term.

[zuiderkwast]

I agree with the analysis @erszcz. Since <<"a">> doesn't exhaust the key type binary(), the map type shouldn't be refined to the empty map for the next clause. I'm not sure how complicated this would be to fix though.

[zuiderkwast]

@javiergarea To show how to reproduce a problem, I recommend adding the example module under test/known_problems/. This is hopefully easier than setting up a separate application.

[javiergarea]

@zuiderkwast You are totally right! #508