Unexpected incompatible type

[gilbertwong96]

I wrote codes with the maybe feature like this:

-module(test_eqwalizer).

-feature(maybe_expr, enable).

-export([main/1]).

-spec main(Args :: list(binary())) -> {ok, binary()} | {error, any()}.
main(Args) ->
    maybe
        true ?= (length(Args) =/= 0) orelse {error, empty_args},
        true ?= is_binary(lists:last(Args)) orelse {error, badargs},
        {ok, <<"ok">>}
    end.

I suppose the type spec is correct. However, the eqwalizer reports the error incompatible_types.

The entire output is as below:

error: incompatible_types
   ┌─ src/test_eqwalizer.erl:11:17
   │
11 │         true ?= (length(Args) =/= 0) orelse {error, empty_args},
   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │                 │
   │                 _ orelse _.
Expression has type:   'true' | {'error', 'empty_args'}
Context expected type: {'ok', binary()} | {'error', term()}

See https://fb.me/eqwalizer_errors#incompatible_types
   │                 

  'true' | {'error', 'empty_args'} is not compatible with {'ok', binary()} | {'error', term()}
  because
  'true' is not compatible with {'ok', binary()} | {'error', term()}
  because
  'true' is not compatible with {'ok', binary()}

error: incompatible_types
   ┌─ src/test_eqwalizer.erl:12:17
   │
12 │         true ?= is_binary(lists:last(Args)) orelse {error, badargs},
   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │                 │
   │                 _ orelse _.
Expression has type:   'true' | {'error', 'badargs'}
Context expected type: {'ok', binary()} | {'error', term()}

See https://fb.me/eqwalizer_errors#incompatible_types
   │                 

  'true' | {'error', 'badargs'} is not compatible with {'ok', binary()} | {'error', term()}
  because
  'true' is not compatible with {'ok', binary()} | {'error', term()}
  because
  'true' is not compatible with {'ok', binary()}

2 ERRORS

Could you please give me an explanation ?

[VLanvin]

To support this example, we need complex reasoning about patterns and types to eliminate the types matched by the left hand side of ?= from the right hand side.

This is something we currently do not support but would like to, although it is very difficult in the general case (where the pattern is more complex than an atom).

I plan to investigate this during the coming year.

[cowang4]

I plan to investigate this during the coming year.

@VLanvin isn't this needed for maybe support? In the meantime should we have eqwalizer not run in maybe blocks? Or all maybe blocks will need % eqwalizer:fixme comments?

[VLanvin]

isn't this needed for maybe support? In the meantime should we have eqwalizer not run in maybe blocks? Or all maybe blocks will need % eqwalizer:fixme comments?

A lot can already be done with maybe blocks and eqWAlizer, such as binding variables via patterns, e.g., {ok, V} ?= foo(Arg). The type of V here will be correctly refined according to the spec of foo/1.

More complex behaviour that mixes predicates, patterns, and booleans such as what is being proposed here, is what is not supported currently.

I don't think it's worth disabling eqWAlizer in maybe blocks for such cases, as we can indeed use % eqwalizer:fixme comments. If the use-case becomes too frequent, then we can re-consider.