FStarLang / FStar

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

Extraction does not reduce projectors in types #3475

Closed gebner closed 2 months ago

gebner commented 2 months ago

When using records with type fields ("bundled types"), extraction does not realize that the type obtained using the projector is equal to the field. As a result, it inserts magic and this in turn causes karamel to fail.

module BundledType

noeq type btype = {
  t: Type;
}

let btype_nat: btype = { t = nat }

// creates one magic
let fourty_two : btype_nat.t = 42

// creates two magics
let thirteen : option btype_nat.t = Some 13

Ideally, this would extract the same as if you wrote nat instead of btype_nat.t everywhere.

gebner commented 2 months ago

Apparently you need to put inline_for_extraction on both btype_nat and btype.