Fixing mistaken erasure of effectful type applications #3518
Conversation
|
I have a check-world green with this: https://github.com/FStarLang/FStar/actions/runs/11153756864 |
| val push_unit (ts : mltyscheme) : mltyscheme | ||
| val pop_unit (ts : mltyscheme) : mltyscheme | ||
| val push_unit (eff:e_tag) (ts : mltyscheme) : mltyscheme | ||
| val pop_unit (ts : mltyscheme) : e_tag & mltyscheme |
There was a problem hiding this comment.
push_unit is called when replacing the type arguments of a function with a unit.
pop_unit is the converse, eliminating a polymorphic function with a type application where the type argument is extracted as unit.
We now record the effect of type application as an e_tag, i.e., Pure, Erasable, Impure
| | None -> bs, U.comp_result c | ||
| | Some (bs, b, rest) -> bs, U.arrow (b::rest) c in | ||
|
|
||
| | None -> bs, etag_of_comp c, U.comp_result c |
There was a problem hiding this comment.
record the effect of the type instantiation
| fun ctr -> | ||
| let n = FStar_HyperStack_ST.op_Bang ctr in | ||
| FStar_HyperStack_ST.testify () |
There was a problem hiding this comment.
interestingly, this was being dropped previously (testify: ((heap -> Type) -> ST unit))
| let recall : 'p . unit -> unit = fun uu___ -> FStar_ST.gst_recall () | ||
| let witness : 'p . unit -> unit = fun uu___ -> FStar_ST.gst_witness () |
There was a problem hiding this comment.
Both of these are really noops, but they are effectful type applications in F* and should not have been dropped
Fixes issue #3473
An effectful polymorphic function
fat typea:Type -> Dv twas typed in the ML extraction asunit -> t.This fix types it now as
unit -Impure-> t, ensuring that an applicationf ais extracted asf ()with effect Impure and so is ineligible for erasure, even iftis an erasable type.