Unexpected error when attempting tutorial

[createyourpersonalaccount]

Hello all, I like to convert all of my function declarations in the val ...; let ... = style, but doing so in a tutorial example (https://fstar-lang.org/tutorial/book/part1/part1_quicksort.html#generic-sorting) led to an unexpected error. Here is my fstar version:

fstar.exe --version
F* 0.9.8.0~dev
platform=Linux_x86_64
compiler=OCaml 4.11.1
date=unset 
commit= (dirty)

I'm on Linux fedora 5.15.6-100.fc34.x86_64 #1 SMP Wed Dec 1 13:41:51 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux and the offending source code follows (I have made a comment of what seems to be the issue).

module Bug

let rec length #a (l:list a)
  : nat
  = match l with
    | [] -> 0
    | _ :: tl -> 1 + length tl

let total_order (#a:Type) (f: (a -> a -> bool)) =
    (forall a. f a a)
    /\ (forall a1 a2. (f a1 a2 /\ a1=!=a2)  <==> not (f a2 a1))
    /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)
    /\ (forall a1 a2. f a1 a2 \/ f a2 a1)

let total_order_t (a:Type) = f:(a -> a -> bool) { total_order f }

let rec sorted #a  (f:total_order_t a) (l:list a)
  : bool
  = match l with
    | [] -> true
    | [x] -> true
    | x :: y :: xs -> f x y && sorted f (y :: xs)

let rec mem (#a:eqtype) (i:a) (l:list a)
  : bool
  = match l with
    | [] -> false
    | hd :: tl -> hd = i || mem i tl

let rec sort #a (f:total_order_t a) (l:list a)
  : Tot (list a) (decreases (length l))
  = admit()

val sort_correct (#a:eqtype) (f:total_order_t a) (l:list a)
  : Lemma (ensures (
           let m = sort f l in
           sorted f m /\
           (forall i. mem i l = mem i m)))
          (decreases (length l))
let rec sort_correct = admit() // Bug: Seems to be OK if I remove 'rec' here

The exact message I get is:

fstar.exe bug.fst 
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
"Match_failure src/ocaml-output/FStar_TypeChecker_Util.ml:267:21"
bug.fst(30,8-30,12): (Warning 328) Global binding Bug.sort is recursive but not used in its body
bug.fst(40,8-40,20): (Warning 328) Global binding Bug.sort_correct is recursive but not used in its body

[nikswamy]

Thanks for this report and sorry for the slow reply!

Things are going wrong because we're misinterpreting the expected arity of the recursive function.

This also works:

val sort_correct (#a:eqtype) (f:total_order_t a) (l:list a)
  : Lemma (ensures (
           let m = sort f l in
           sorted f m /\
           (forall i. mem i l = mem i m)))
          (decreases (length l))
let rec sort_correct #a f l = admit() // Bug: Seems to be OK if I remove 'rec' here

Will push a patch soon.

[createyourpersonalaccount]

@nikswamy Thanks for the response. Glad it got fixed.