josefs / Gradualizer

A Gradual type system for Erlang
MIT License
609 stars 35 forks source link

Crash with Uncaught error: function_clause #530

Open ilya-klyuchnikov opened 1 year ago

ilya-klyuchnikov commented 1 year ago

Trying to run it on our code base:

===> Uncaught error: function_clause
===> Stack trace to the error location:
[{gradualizer_lib,pick_value,
  [{type,0,term,[]},
   {env,
     ..., omitting environment
    false}],
  [{file,
    "gradualizer/src/gradualizer_lib.erl"},
   {line,162}]},
 {gradualizer_lib,'-pick_values/2-lc$^0/1-0-',2,
  [{file,
    "gradualizer/src/gradualizer_lib.erl"},
   {line,156}]},
 {typechecker,check_clauses_intersection_throw_if_seen,5,
  [{file,
    "gradualizer/src/typechecker.erl"},
   {line,3892}]},
 {typechecker,check_clauses_intersection,5,
  [{file,
    "gradualizer/src/typechecker.erl"},
   {line,3830}]},
 {typechecker,check_clauses_fun,3,
  [{file,
    "gradualizer/src/typechecker.erl"},
   {line,3744}]},
 {typechecker,type_check_function,2,
  [{file,
    "gradualizer/src/typechecker.erl"},
   {line,4647}]},
 {typechecker,type_check_form,5,
  [{file,
    "gradualizer/src/typechecker.erl"},
   {line,5687}]},
 {typechecker,'-type_check_form_with_timeout/5-fun-0-',6,
  [{file,
    "gradualizer/src/typechecker.erl"},
   {line,5645}]}]

Looking into gradualizer_lib:pick_value - it doesn't expect term() type.

erszcz commented 1 year ago

Thanks, @ilya-klyuchnikov!

Can you share a (possibly minimised) snippet on which this happens? Generally, a denormalised type like term() should not reach pick_value because of these checks, specifically all_refinable:

https://github.com/josefs/Gradualizer/blob/01a19313b3931f8d4e78e4cc80130a214f3b6041/src/typechecker.erl#L3954-L3957

But, apparently, something's falling through the cracks 🤔

erszcz commented 1 year ago

For more context, simple examples like these don't trigger this:

$ cat test.erl
-module(test).

-spec f(term()) -> ok.
f(T) ->
    case T of
        1 -> ok
    end.

-spec g({a | b, term()}) -> ok.
g(T) ->
    case T of
        {a, 1} -> ok
    end.

And while a trivial patch like this should fix the problem, I'd be hesitant to merge it without understanding what expression leads to the crash in the first place.

ilya-klyuchnikov commented 1 year ago

I am trying to run gradualizer on a fairly large project. How do I find out what it analyzes when it fails?

erszcz commented 1 year ago

Please add

{gradualizer_opts, [
    verbose
]}.

to rebar.config or, if using the escript, --verbose to the list of command line arguments. Verbose logging should result in a log like this (but with lots of output for a large codebase):

Checking module rebar3_example
Spawning async task...
Checking function c/1
Pushing {clauses_controls,true}
6:1: Checking clause :: boolean()
7:5: Checking that X :: boolean()
Exhaustiveness checking: true
Popping clauses controls
Task returned from function c/1 with []

which should make it possible to pinpoint where the problem is. It might help to run Gradualizer app by app in a big umbrella repo, to limit the scope.

This use case is certainly not polished for large code bases yet, but with the available resources we have to pick our battles.

ilya-klyuchnikov commented 1 year ago

A minimized repro:

-module(gradualizer_repro).

-compile([export_all, nowarn_export_all]).

-spec to_i(term()) -> integer().
to_i(_) -> error(example).

-spec to_b(term()) -> boolean().
to_b(_) -> error(example).

-spec to_x
    (term(), to_i | i, Default) -> integer() | Default;
    (term(), to_b | b, Default) -> boolean() | Default.
to_x(Value, _, Default) when Value =:= Default ->
    Default;
to_x(Value, to_i, _) -> to_i(Value);
to_x(Value, i, _) -> to_i(Value);
to_x(Value, to_b, _) -> to_b(Value);
to_x(Value, b, _) -> to_b(Value).
erszcz commented 1 year ago

Thanks for the example, @ilya-klyuchnikov! It's most likely the case that spurious types reach gradualizer:pick_value/2 due to changes introduced in https://github.com/josefs/Gradualizer/pull/461, which introduces another call to pick_value than the one that's guarded with exhaustiveness checks. I'll have to investigate further how to prevent this from happening.