"F* may be in an inconsistent state" error when trying to define parameterized raise in DM4F effect

[klinvill]

I was working on parameterizing the RAND DM4F effect on a type. It seems to fail when I include the raise function with an error that reports:

ASSERTION FAILURE: Failed to find e@4
Env is (., dummy); (., dummy); (., dummy); (., dummy)

F* may be in an inconsistent state.
Please file a bug report, ideally with a minimized version of the program that triggered the error

Does anyone know why this is the case? I'm assuming I'm just overlooking something when defining raise, but if not is this an error with F* itself?

A minimal reproducible example is:

module Test

assume val tape (e:Type) : Type0
assume val id : eqtype

type store (e:Type) = id * tape e

(** Read-only tape with a pointer to the next unread position *)
type rand (e:Type) (a:Type) = (store e) -> M (option a * id)

let return (e:Type) (a:Type) (x:a) : rand e a = fun (next,_) -> Some x, next

let bind (e:Type) (a b:Type) (c:rand e a) (f:a -> rand e b) : rand e b =
  fun s ->
    let r, next' = c s in
    match r with
    | None   -> None, next'
    | Some x -> f x (next', snd s)

(** Raise exception *)
let raise (e:Type) (a:Type) () : rand e a = fun s -> None, fst s

total reifiable reflectable new_effect {
  RAND (e:Type) : a:Type -> Effect
  with repr   = rand e
     ; bind   = bind e
     ; return = return e
     ; raise = raise e
}

[nikswamy]

Hi Kirby,

I think the DM4Free feature does not handle polymorphic actions like raise. We should fail gracefully rather than crashing like this: That's a bug.

However, you can workaround this, at least in this case, like so:

module Test

assume val tape (e:Type) : Type0
assume val id : eqtype

type store (e:Type) = id * tape e

(** Read-only tape with a pointer to the next unread position *)
type rand (e:Type) (a:Type) = (store e) -> M (option a * id)

let return (e:Type) (a:Type) (x:a) : rand e a = fun (next,_) -> Some x, next

let bind (e:Type) (a b:Type) (c:rand e a) (f:a -> rand e b) : rand e b =
  fun s ->
    let r, next' = c s in
    match r with
    | None   -> None, next'
    | Some x -> f x (next', snd s)

(** Raise exception *)
let raisef (e:Type) () : rand e False = fun s -> None, fst s

total reifiable reflectable new_effect {
  RAND (e:Type) : a:Type -> Effect
  with repr   = rand e
     ; bind   = bind e
     ; return = return e
     ; raisef = raisef e
}

total reifiable reflectable
new_effect RAND_i = RAND int

let raise #a ()
  : RAND_i a (fun s post -> post (None, fst s))
  = let _ = RAND_i?.raisef () in
    false_elim ()

[klinvill]

Awesome thanks! That does indeed work for now. As per #343 it sounds like F* doesn't have support for effect polymorphism that would allow for writing the raise function generically outside of the effect. Is that correct? Ideally it would be nice to write something kind of like:

let raise #e #a ()
  : RAND e a (fun s post -> post (None, fst s))
  = let _ = RAND?.raisef () in
    false_elim ()

instead of instantiating it to create RAND_i and then writing a raise function for that instantiated effect. If I try this I get the error message that:

Effect template RAND should be applied to arguments for its binders ((e: Prims.eqtype)) before it can be used at an effect position

This seems like confirmation to me that this kind of effect polymorphism is not currently supported.

[nikswamy]

FYI, this kind of effect index polymorphism is supported using layered effects, but not with DM4F