Inferred type of modulus is a bit odd?

[Timmmm]

This code works fine:

overload operator % = {emod_int}

function foo(x : range(0, 3)) -> unit = ()

function main() -> unit = {
  let test = (-10) % 4;
  foo(test);
  match test {
    0 => (),
    1 => (),
    2 => (),
    3 => (),
  };
}

Except it prints this warning:

Warning: Incomplete pattern match statement at main.sail:8.2-7:
8 |  match test {
  |  ^---^
  | 
The following expression is unmatched: -1

That's clearly not the case, and in fact if you just add an explicit type annotation the warning disappears:

  let test : range(0, 3) = (-10) % 4;

but I feel like that shouldn't be necessary and it's kind of weird that it makes a difference while being happy to pass test to foo() in both cases.

[bacam]

The type checker is inferring int(2) for test, and the problem appears to be that the pattern completeness checker doesn't know how to use a fixed value, but is happy using constraints for type variables. Thus any fancier but equivalent type, such as range(2,2) or { 'i, 'i == 2. int('i) } works. It shouldn't be too hard to fix, but I'll resist the temptation to mess up more of Alasdair's code...

[Alasdair]

This might be an unintentional side effect of trying to avoid spurious warnings on RISC-V, where xlen is ifdef'd between 32 and 64. We don't want to give a warning for every 64 case when in RV32 and vice versa, so I think there was some specific logic for matching on constant values.

[Alasdair]

The fix is probably to use the constants to check completeness, but then discard any redundant arm warnings if we did so.

[Timmmm]

I guess #534 might provide enough information that you don't need to discard redundant arm warnings?

[Alasdair]

Should be fixed by #665

We aren't actually being that clever about detecting redundant arms if they aren't obviously being caused by a combination of wildcard patterns, so spurious warnings shouldn't be an issue. If we were detecting redundant arms in a constraint-aware way (which we could do, but it might be slow as it would require using the SMT solver to check a constraint for each arm separately) then #534 would indeed help avoid any issues.

[Timmmm]

Sorry I may have oversimplified the example! The one I posted now works, but in my actual code the expression is not constant:

overload operator % = {emod_int}

val foo: forall 'n, 'n > 0. (int('n)) -> unit
function foo(n) = {
  foreach (i from 0 to ('n - 1)) {
    let component = i % 4;
    match component {
      0 => (),
      1 => (),
      2 => (),
      3 => (),
    };
  };
}

That still triggers the warning. component is inferred as int(mod('loop_i, 4)).

[Alasdair]

Looks like there's a difference when checking completeness for something like X: int(expr) |- match X ... and N = expr; X: int(N) |- match X .... I could either rewrite the first into the second or generalise the handling code to work with either case.