Loop with side effect at the end of a function gives inconsistent type

[maximebuyse]

fn range() {
    let mut count = 0u8;
    for i in 0u8..10u8 {
        hax_lib::loop_invariant!(|i: u8| i <= 10);
        count = i;
    }
}

fn f() {
    range()
}

Open this code snippet in the playground

The produced F* for this:

let range (_: Prims.unit) : u8 =
  let count:u8 = 0uy in
  Rust_primitives.Hax.Folds.fold_range 0uy
    10uy
    (fun count i ->
        let count:u8 = count in
        let i:u8 = i in
        i <=. 10uy <: bool)
    count
    (fun count i ->
        let count:u8 = count in
        let i:u8 = i in
        let count:u8 = i in
        count)

let f (_: Prims.unit) : Prims.unit =
  range ()

The function range is typed as returning u8 but it should return unit.

[karthikbhargavan]

Is this solved by adding a () unit after the loop?

…

On Tue, Jan 14, 2025, 16:34 maximebuyse ***@***.***> wrote: fn range() { let mut count = 0u8; for i in 0u8..10u8 { hax_lib::loop_invariant!(|i: u8| i <= 10); count = i; }} fn f() { range()} Open this code snippet in the playground <https://hax-playground.cryspen.com/#fstar/98ded931ba/gist=12e92ab1d66e369d4961305aa6605231> The produced F* for this: let range (_: Prims.unit) : u8 = let count:u8 = 0uy in Rust_primitives.Hax.Folds.fold_range 0uy 10uy (fun count i -> let count:u8 = count in let i:u8 = i in i <=. 10uy <: bool) count (fun count i -> let count:u8 = count in let i:u8 = i in let count:u8 = i in count) let f (_: Prims.unit) : Prims.unit = range () The function range is typed as returning u8 but it should return unit. — Reply to this email directly, view it on GitHub <#1231>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABFUVS5GECFIW6GYVV3MAOT2KUU7JAVCNFSM6AAAAABVFFJ32CVHI2DSMVQWIX3LMV43ASLTON2WKOZSG44DONJRGMZDGOI> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[maximebuyse]

Is this solved by adding a () unit after the loop?

Yes, this works as a workaround, and the idea for the fix is to insert it. The problem is to do it only when necessary to avoid polluting the generated code.

[franziskuskiefer]

Here's another reproducer.
Never mind, it was using an outdated hax revision.