FStar
FStar copied to clipboard
Embedding error when using reflection on ML effect
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