FStar
FStar copied to clipboard
Incorrect OCaml extraction
Consider the following (minimized) F* code:
module State
noeq
type table_name (r: Type0) =
{ te: Type0; get: r -> Seq.seq te; }
let return_table (#t: Type0) (tabs: t) (tn: table_name t) : Seq.seq tn.te =
tn.get tabs
After extraction by running fstar.exe State.fst --codegen OCaml, F* returns the following OCaml code (omitting projectors for brevity):
open Prims
type 'r table_name = {
te: unit ;
get: 'r -> Obj.t FStar_Seq_Base.seq }
let return_table : 't . 't -> 't table_name -> unit FStar_Seq_Base.seq =
fun tabs -> fun tn -> tn.get tabs
Attempting to compile this yields the following type error:
12 | fun tabs -> fun tn -> tn.get tabs
^^^^^^^^^^^
Error: This expression has type Obj.t FStar_Seq_Base.seq
but an expression was expected of type Prims.unit FStar_Seq_Base.seq
Type Obj.t is not compatible with type Prims.unit = unit
This occurs with the following F* version:
F* 2024.01.13~dev
platform=Darwin_arm64
compiler=OCaml 4.14.0
date=2024-05-21 22:20:52 -0700
commit=8ec46c7eaa174fca284a6db50cf0db44f995b2d8