Extraction don't extract values equal to `()` even if they are relevant in extraction

[TWal]

trafficstars

See the following code:

module UnitExtraction

let byte = n:nat{n < 256}
let lbytes (n:nat) = l:list byte{List.Tot.length l == n}

// In my real case, everything is well-encapsulated with a .fsti file
// The rest of the code treats a `randomness l` as a black box
val randomness: list nat -> Type0
let rec randomness l =
  match l with
  | [] -> unit
  | h::t -> lbytes h & randomness t

val mk_empty_randomness: randomness []
let mk_empty_randomness = ()

// You can stop reading here, I left the rest only to help see the "big picture" of why this type is useful
val mk_randomness: #head_size:nat -> #tail_size:list nat -> (lbytes head_size & randomness tail_size) -> randomness (head_size::tail_size)
let mk_randomness #head_size #tail_size (head_rand, tail_rand) =
  (head_rand, tail_rand)

val dest_randomness: #head_size:nat -> #tail_size:list nat -> randomness (head_size::tail_size) -> (lbytes head_size & randomness tail_size)
let dest_randomness #head_size #tail_size (head_rand, tail_rand) =
  (head_rand, tail_rand)

Extract the code with:

fstar.exe UnitExtraction.fst --codegen OCaml --extract_module UnitExtraction 

The extraction is:

open Prims
type byte = Prims.nat
type 'n lbytes = byte Prims.list
type 'l randomness = Obj.t

let (mk_randomness :
  Prims.nat -> Prims.nat Prims.list -> (unit lbytes * Obj.t) -> Obj.t) =
  fun uu___2 ->
    fun uu___1 ->
      fun uu___ ->
        (fun head_size ->
           fun tail_size ->
             fun uu___ ->
               match uu___ with
               | (head_rand, tail_rand) -> Obj.magic (head_rand, tail_rand))
          uu___2 uu___1 uu___
let (dest_randomness :
  Prims.nat -> Prims.nat Prims.list -> Obj.t -> (unit lbytes * Obj.t)) =
  fun head_size ->
    fun tail_size ->
      fun uu___ ->
        match Obj.magic uu___ with
        | (head_rand, tail_rand) -> (head_rand, tail_rand)

The mk_randomness is not extracted!