Dangers in extending recursion safety check to more args?

[Pat-Lafon]

rbtree_gen has the following spec:

let[@assert] rbtree_gen =
  let inv = (v >= 0 : [%v: int]) [@over] in
  let color = (true : [%v: bool]) [@over] in
  let[@assert] h =
    (v >= 0 && if color then v + v == inv else v + v + 1 == inv
      : [%v: int])
      [@over]
  in
  ...

In the typing context of ??:

let rec rbtree_gen (inv : int) (color : bool) (h : int) : int rbtree =
  if sizecheck h then
    if color then Rbtleaf
    else if bool_gen () then Rbtleaf
    else Rbtnode (true, Rbtleaf, int_gen (), Rbtleaf)
  else
    ??

I've enumerated the following term:

rbtree_gen h color h

(*Less readable, Normalized form*)
let (_x32) = rbtree_gen h in
let (_x33) = _x32 color in 
let (_x34) = _x33 h in
_x34

Which passes the recursion check because h > 0 and inv == h + h || inv == h + h + 1 so h >= 0 && h < inv.

Ideally, I would like to reject this term because it violates the third arguments overapproximate refinement type. (Alternatively, maybe I can say something about this term's coverage?)

What would be the danger in extending the current hack for the recursive call's argument check to other function calls.

https://github.com/zhezhouzz/underapproximation_type/blob/94d0f056488c98bfd9177813c56237f8be466222/typing/termcheck.ml#L300-L317

[Pat-Lafon]

This seems useful for the STLC benchmarks as well because the recursion template takes into account 2 arguments instead of just 1.

[Pat-Lafon]

I've made this change and it both seems to work as expected and reduces the hackiness of the code base