FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Incorrect OCaml extraction #3307

Open R1kM opened 1 month ago

R1kM commented 1 month ago

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