FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Embedding error when using reflection on ML effect

Open TWal opened this issue 2 years ago • 0 comments

See these examples:

open FStar.All
open FStar.Tactics

let f (): ML bool = true

let fstar_all_ml_name: name = explode_qn "FStar.All.ML"

// Destructing a ML comp cause problems
[@@expect_failure]
let _ = run_tactic (fun () ->
  let t = (tc (top_env()) (`f)) in
  match inspect t with
    | Tv_Arrow x c -> (
      match inspect_comp c with
      | C_Eff w x y z -> (
        let bla = (List.Tot.length w) in
        dump (string_of_bool (x = fstar_all_ml_name)); // -> true (sanity check)
        //This dump is necessary for this example
        dump (if bla = 0 then "0 universes" else "n universes");
        ()
      )
      | _ -> ()
    )
    | _ -> ()
  )

// Constructing a ML comp causes problems
[@@expect_failure]
let _ = run_tactic (fun () ->
  let x = pack (Tv_Arrow (fresh_binder (`unit)) (pack_comp (C_Eff [] fstar_all_ml_name (`unit) []))) in
  ()
)

It looks similar to #2597

TWal avatar Jun 02 '22 20:06 TWal