False negatives for `A = B` expressions

[albsch]

Describe the bug

ELP has trouble finding type spec violations when using A = B expressions.

To Reproduce

Here are three equivalent code snippets in a module example.erl, only the error in t3 is detected.

-module(example).
-compile([export_all, nowarn_export_all]).

-spec t1() -> ok.
t1() ->
  [] = foo.

-spec t2() -> ok.
t2() ->
  case foo of
    A = [] -> A
  end.

-spec t3() -> ok.
t3() ->
  case foo of
    [] -> []
  end.

Expected behavior

Similar to t3, a type error in t2 and t1 should be detected.

Actual behavior

Only a type error in t3 is detected.

> ./elp eqwalize-all                                                                                 
Loading build info                                                                                      
Loading applications      ████████████████████                                                          
Seeding database                                                                                        
Compiling dependencies                                                                                  
Gathering modules         ████████████████████ 3/3                                                      
Parsing modules                                                                                         
EqWAlizing                                                                                            
error: incompatible_types (See https://fb.me/eqwalizer_errors#incompatible_types)
   ┌─ src/example.erl:19:11
   │
19 │     [] -> []
   │           ^^ [].
Expression has type:   []
Context expected type: 'ok'

1 ERROR

Context

ELP release with eqwalizer support enabled, and VS code plugin.

./elp version
elp 1.1.0+build-2025-11-04

Example project attached.

example.zip

Is there a reason why type information is lost for the bound variable A in t2 or why [] is not used as the return type for the expression [] = foo in t1?

[VLanvin]

Thanks for the report.

t1 looks like a bug in eqWAlizer in how we handle patterns. [] should indeed be used as return type.

t2 is an edge-case: since the type of A must be both [] and foo to match, it computes it as none() (greatest common subtype), which typechecks. As of now eqWAlizer does not report patterns that cannot match in case expressions, but we're exploring adding support for it. So it will correctly report an error in this case. As a side-note, it will also report an additionnal error for t1 and t3 saying that the patterns cannot match.