fold_range type mismatch

[franziskuskiefer]

fn decompose(low: &mut [u8; 5]) {}

fn decompose_vector(low: &mut [[u8; 5]; 5]) {
    for i in 0..5 {
        decompose(&mut low[i]);
    }
}

Open this code snippet in the playground

* Error 12 at Playground.fst(20,4-50,19):
  - Expected type
        Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8
              (Rust_primitives.Integers.sz 5))
          (Rust_primitives.Integers.sz 5) &
        Prims.unit
    but
        Rust_primitives.Hax.Folds.fold_range (Rust_primitives.Integers.sz 0)
          (Rust_primitives.Integers.sz 5)
          (fun _ _ -> true)
          low
          (fun low i ->
              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize low
                i
                (decompose low.[ i ])
              <:
              Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8
                    (Rust_primitives.Integers.sz 5))
                (Rust_primitives.Integers.sz 5))
    has type
        result:
        Rust_primitives.Arrays.t_Array (Rust_primitives.Arrays.t_Array Rust_primitives.Integers.u8
              (Rust_primitives.Integers.sz 5))
          (Rust_primitives.Integers.sz 5) {true}
1 error was reported (see above)
make[1]: *** [Makefile:79: Playground.fst.checked] Error 1
make: *** [Makefile:12: all] Error 2

[karthikbhargavan]

Double return strikes again. See workaround:

https://hax-playground.cryspen.com/#fstar+tc/e4c6c2be1c/gist=82d4f54a2f7d9a72b3e756e85bcd792b

Shall we close this as a duplicate of #720?

[franziskuskiefer]

Ah, that was supposed to be mostly fixed. Then we can close this and update the other one that it's not working.