Why have two incompatible Bytes modules (FStar.Bytes and Platform.Bytes) and do they need to be named the same way?

[catalin-hritcu]

Type-checking the following code:

val code_length : ss:(list (symbol * pos)) -> cs:(list bytes) -> Pure nat
  (requires (sorted ss /\ List.Tot.length cs == List.Tot.length ss))
  (ensures (fun _ -> True))
let code_length ss cs =
  fold_left2 (fun (a:nat) (sw:symbol*pos) c ->
              let (s,w) = sw in a + w `op_Multiply` (Bytes.length c)) 0 ss cs

is giving me a dubious typing error:

[hritcu@detained algorithms]$ fstar.exe --include ../../ucontrib/Platform/fst --print_implicits --print_universes --log_queries Huffman.fst
./Huffman.fst(19,75-19,77) : (Error) Expected expression of type "(Prims.list<?151930> FStar.Bytes.bytes)"; got expression "cs" of type "(Prims.list<0> Platform.Bytes.bytes)"

So I looked in the debugger and it seems the error is still bogus, but a bit more explicit before the normalization the printing now does by default.

The computed type of the expression (Prims.list<?151930> ((fun ss cs -> (FStar.Bytes.bytes $$ Tot Type(?151930))) ss cs)) is 2 eta reduction steps away from the required type Prims.list<0> Platform.Bytes.bytes), but F* only eta reduces this when printing the error message.

At least this is my understanding of this after staring at it for a while.

[catalin-hritcu]

Just realized that Bytes.length was pointing to FStar.Bytes and that removing the Bytes prefix makes the error go away. To my surprise F* has two incompatible modules called Bytes: Platform.Bytes.bytes and FStar.Bytes.bytes. Moreover, FStar.Bytes.bytes seems to be automatically imported? [Edited to remove my feelings about this]

[andreasdotorg]

I joined the club today. One of those bytes needs to die.

[wintersteiger]

Bumping this to high priority. I think this is particularly important right now, as we start rolling out the new parser combinators, which operate mainly on bytes (but currently neither Platform.Bytes.bytes nor FStar.Bytes.bytes).

[nikswamy]

Platform.Bytes is now moved out to ucontrib. Perhaps we should now remove it altogether