nbe fails on `reify` terms

[amosr]

Trying to apply normalize-by-evaluation to a reified effect fails with Failure("NBE ill-typed application: Meta …").

I was hoping to use the effects to build up a complex datastructure (an AST), then use a tactic to simplify the effect machinery away. NBE seems to be getting stuck on it.

It looks like the combination of nbe with delta is doing something strange. If I run them separately it's OK, but together I get an ill-typed term. In this example with definitions from TacticReify.fst (attached):

let run_eff (e: unit -> Eff 'a) : 'a = reify (e ()) ()
let eff_int (): Eff int = 1

let test_run_reify_ok (): unit =
  let xe = run_eff eff_int in
  assert (xe == 1) by (
    T.norm [primops; iota; delta; zeta];
    T.norm [nbe];
    T.dump "ok")

The above succeeds and dumps return int 1 () == 1. But if we do nbe + delta on the second step:

let test_run_reify_bad (): unit =
  let xe = run_eff eff_int in
  assert (xe == 1) by (
    T.norm [primops; iota; delta; zeta];
    T.norm [nbe; delta];
    T.dump "bad")

I get the goal int 1 () == 1!

TacticReify.fst.txt

There is an existing issue related to normalizing reify https://github.com/FStarLang/FStar/issues/2568 but in this case we get an error or ill-typed goals rather than just refusing to normalize.

[amosr]

TacticReify.fst:

module TacticReify

module Pure = FStar.Monotonic.Pure
module T = FStar.Tactics

(* Simple reader-style monad *)
type state = unit

// -> GTot Type0?
let eff_pre = Type0
let eff_post (a: Type) = a -> Type0
let eff_wp0 (a: Type) = eff_post a -> eff_pre

unfold
let eff_wp_monotonic (a: Type) (wp: eff_wp0 a) =
  forall (p q: eff_post a).
    (forall x. p x ==> q x) ==>
    (wp p ==> wp q)

let eff_wp (a: Type) = wp: eff_wp0 a { eff_wp_monotonic a wp }

type repr (a: Type) (wp: eff_wp a) =
  unit -> PURE a (Pure.as_pure_wp (fun p -> wp (fun r -> p r)))

unfold
let return_wp (a: Type) (x: a) (post: eff_post a) = post x

let return (a: Type) (x: a): repr a (return_wp a x) =
  fun s -> x

unfold
let bind_wp (a b: Type)
  (wp1: eff_wp a) (wp2: a -> eff_wp b)
  (post: eff_post b) =
 wp1 (fun a -> wp2 a post)

let bind (a b: Type)
  (wp_f: eff_wp a)
  (wp_g: a -> eff_wp b)
  (f: repr a wp_f)
  (g: (x: a -> repr b (wp_g x))):
    repr b (bind_wp a b wp_f wp_g) =
  fun s ->
    let x = f s in
    g x s

// let subcomp (a: Type)
//   (wp_f wp_g: eff_wp a)
//   (f: repr a wp_f):
//     Pure (repr a wp_g)
//   (requires forall p. wp_g p ==> wp_f p)
//   (ensures fun _ -> True) = f

// unfold
// let if_then_else (a: Type)
//   (wp_f wp_g: eff_wp a)
//   (f: repr a wp_f)
//   (g: repr a wp_g)
//   (p: bool): Type =
//   repr a (fun post -> (p ==> wp_f post) /\ ((~ p) ==> wp_g post))

total reifiable reflectable
effect {
  EFF (a: Type) (_: eff_wp a)
  with {
    repr;
    return;
    bind;
    // subcomp;
    // if_then_else
  }
}

unfold
let lift_pure_wp (#a: Type) (wp: pure_wp a): eff_wp a =
  Pure.elim_pure_wp_monotonicity wp;
  fun p -> wp (fun x -> p x)

let lift_pure_stream (a: Type) (wp: pure_wp a) (f: unit -> PURE a wp):
  repr a (lift_pure_wp wp) =
 Pure.elim_pure_wp_monotonicity wp;
 fun s -> f ()

sub_effect PURE ~> EFF = lift_pure_stream

effect EffH (a: Type) (pre: eff_pre) (post: eff_post a) = EFF a (fun post' -> pre /\ (forall (x: a). post x ==> post' x))

effect Eff (a: Type) = EffH a (requires True) (ensures (fun a -> True))


let run_eff (e: unit -> Eff 'a) : 'a =
  let a = reify (e ()) () in
  a

let test_run_repr_ok (): unit =
  let r: repr int (fun p -> forall (x: int). p x) = (fun () -> 1) in
  let xe: int = r () in
  assert (xe == 1) by (T.norm [primops; iota; delta; nbe])

[@@expect_failure]
let test_run_reify_fails (): unit =
  let xe = run_eff (fun () -> 1) in
  assert (xe == 1) by (T.norm [primops; iota; delta; nbe])