More robust reification in normalizer

[mtzguido]

Mostly copied from FStar.DM4F.Exceptions:

module Bug

let ex (a:Type) = unit -> M (either a exn)

val return_ex : (a:Type) -> (x:a) -> ex a
let return_ex a x = fun _ -> Inl x

val bind_ex : (a:Type) -> (b:Type) -> (f:ex a) -> (g:a -> ex b) -> ex b
let bind_ex a b f g = fun _ ->
  let r = f () in
  match r with
  | Inr e -> Inr e
  | Inl x -> g x ()

let raise0 (a:Type) (e:exn) : ex a = fun _ -> Inr e

reifiable reflectable new_effect {
  EXN : (a:Type) -> Effect
  with repr     = ex
     ; bind     = bind_ex
     ; return   = return_ex
     ; raise (#a:Type) = raise0 a
}

let raise = EXN?.raise

exception EE

let _ = assert_norm (reify (raise #int EE) () == Inr EE)

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Impossible: missing universe instantiation on __proj__EXN__item__raise")

Although I'm confused, since even specializing raise0, EXN?.raise and raise to Type0 also exhibits this behaviour.

[mtzguido]

I'm sorry, that crash was only on a crappy state of mine.

The real problem is that they are not reified since when we look at the normalizer stack we see a UnivArgs, and not an App with a reify. Ignoring the UnivArgs is what messes this up, and it's wrong. Perhaps we want a reifying flag as the NBE has.

The problem can be seen here:

module Bug

let ex (a:Type) = unit -> M (either a exn)

val return_ex : (a:Type) -> (x:a) -> ex a
let return_ex a x = fun _ -> Inl x

val bind_ex : (a:Type) -> (b:Type) -> (f:ex a) -> (g:a -> ex b) -> ex b
let bind_ex a b f g = fun _ ->
  let r = f () in
  match r with
  | Inr e -> Inr e
  | Inl x -> g x ()

let raise0 (a:Type) (e:exn) : ex a = fun _ -> Inr e

reifiable reflectable new_effect {
  EXN : (a:Type) -> Effect
  with repr     = ex
     ; bind     = bind_ex
     ; return   = return_ex
     ; raise (#a:Type) = raise0 a
}

let ret (#a:Type0) (x:a) : EXN a (fun () p -> p (Inl x)) = x

let raise : #a:Type -> e:exn -> EXN a (fun () p -> p (Inr e)) = EXN?.raise

exception EE

#set-options "--debug Bug --debug_level SMTQuery"

let _ = assert_norm (normalize_term (reify (ret 1) ()) == Inl 1)

let _ = assert_norm (reify (raise #int EE) () == Inr EE)

The first query is Inl 1 == Inl 1, while the second one is reify (EXN?.raise EE) () == Inr EE, when it should really be Inr EE == Inr EE.

[mtzguido]

Fixed this in 4a2e9860130f1876d6ead9ebf9fe4c0ff7629965, but I still think we need a reifying flag so these things don't pop up again. Keeping open marked as an enhancement.