Validation ticks error including andalso macro in ATS

Question

Here are two pieces of code that I think are equivalent, except for the second, which has more lines, then it should:

fun
move_ul
{i:nat}
(
  p: int(i) 
, ms: list0(Int)
): list0(Int) =
if p - 5 >= 0 andalso p % 4 != 0 then
  move_ul(p - 5, cons0(p - 5, ms))
else
  ms



fun
move_ul
{i:nat}
(
  p: int(i) 
, ms: list0(Int)
): list0(Int) =
if p % 4 != 0 then
  if p - 5 >= 0 then
    move_ul(p - 5, cons0(p - 5, ms))
  else
    ms
else
  ms

For some reason, the second is waiting for type checking, but the first is failing (inability to satisfy the constraints) ... can someone tell me why?

Answer 1

This is due to how it is defined andalso(like a macro that does not use dependent types). If you change andalsoto *(which overloads Boolean multiplication), the first version of your code should look like typecheck.

By the way, if used orelse, a similar situation can be simply solved by replacing orelsewith +(which overloads the Boolean addition).