Spurious warning on mutually recursive functions

[nikswamy]

  type value = bool

  let rec array_cmp (l1:list value) (l2:list value) : bool =
    match l1, l2 with
     | hd1::tl1, hd2::tl2  ->   array_cmp tl1 tl2
     | _ -> false

  and cmp (v1:value) (v2:value) : bool =
    false

Produces

(Warning 290) - SMT may not be able to prove the types of l1 at <input>(10,21-10,23)
    (Prims.list Value.value) and v1 at <input>(15,11-15,13) (Value.value) to be
    equal, if the proof fails, try annotating these with the same type
  - See also <input>(10,21-10,23)

I think I've noticed this before from inferred decreases clauses, but this warning remains even if you add explicit decreases annotations.

Thanks to @anakrish

[anakrish]

With

$ fstar.exe -v
F* 2024.01.13~dev
platform=Darwin_arm64
compiler=OCaml 4.14.1
date=2024-02-26 06:11:44 -0800
commit=a48722f90e14be69b850f093b41fbbdfee7f6eb9

the warnings go away if decreases clauses are added thus:

module Foo

  type value = bool

  let rec array_cmp (l1:list value) (l2:list value) : Tot bool (decreases l1)=
    match l1, l2 with
     | hd1::tl1, hd2::tl2  ->   array_cmp tl1 tl2
     | _ -> false

  and cmp (v1:value) (v2:value) : Tot bool (decreases v1)=
    false