type refinement of comparison guards with integer types

[berbiche]

Hi,

I didn't want to divert #258 with my question so I used the new discussions thingy.

With the PR addressing #258's first step, is the type of Int in the following example correctly refined to non_neg_integer()?

Int =
  case binary_to_integer(SomeBinary) of
    Int_ when Int_ < 0 -> throw('an error');
    Int_ -> Int_
  end,
some_function_expecting_non_neg_integer(Int).

[zuiderkwast]

Yes, Int :: non_neg_integer() should be correct here. Why wouldn't it be? The throw?

Does it work like this now?

[zuiderkwast]

There may be some problem with Int = ..., some_function(Int) so if you put the case directly in the function call, it might work differently (type_check_expr vs type_check_expr_in). It has to do with bidirectional typechecking, but it's not working correctly, I think. There's an idea of unifying the two parallel structures (somewhere in the comments of some issue or PR).

[berbiche]

I think the throw makes Int have type integer() instead of non_neg_integer() but I'm not sure.

[zuiderkwast]

Interesting. I guess it's the same in this situation:

Int = binary_to_integer(SomeBinary),
if Int < 0 -> throw(' an error');
   true    -> ok
end,
some_function_expecting_non_neg_integer(Int).

Perhaps we need some new kind of refinement....?