Coherence between lifts and returns

[erivas]

When defining a layered effect, we have to provide both a return and a lift to lift "pure" values to computations. After discussing with @mtzguido and @aseemr , it seems that return is being used for type-checking but the lift is being used for reification. If lift is not coherent with return (different action, for example), it seems that something bad could happen:

module Reify

open FStar.Error
open FStar.Tactics

type option' a = optResult bool a

let conv (#a:Type) (v : optResult bool a) (w : optResult bool unit) : bool =
  match v , w with
  | Error true , Error true -> true
  | Error false , Error false -> true
  | Correct _ , Correct _ -> true
  | _ , _ -> false

type erepr (a:Type) (b : optResult bool unit) = unit -> Pure (option' a) True (fun x -> conv x b)

let ereturn (a:Type) (x:a) : erepr a (Correct ()) = fun _ -> Correct x

let ebind (a:Type) (b:Type) wp_f wp_g (f:erepr a wp_f) (g:(x:a -> erepr b wp_g))
: erepr b (
   match wp_f with
   | Error e -> Error e
   | Correct () -> wp_g)
= fun _ ->
  let r = f () in
  match r with
  | Error e -> Error e
  | Correct x -> g x ()

let esubcomp (a:Type) wp_f (f:erepr a wp_f) : erepr a wp_f = f

let eif_then_else (a:Type) (wp_f) (f:erepr a wp_f) (g:erepr a wp_f) (p:Type0) : Type
  = erepr a wp_f

total reifiable reflectable
layered_effect {
  EXN : a:Type -> optResult bool unit -> Effect
  with
  repr = erepr;
  return = ereturn;
  bind = ebind;
  subcomp = esubcomp;
  if_then_else = eif_then_else
}

let lift_pure_exn (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp) : erepr a (Error false) = fun _ -> Error false

sub_effect PURE ~> EXN = lift_pure_exn

let net () : EXN unit (Error true) = EXN?.reflect (fun _ -> Error true) <: EXN unit (Error true)

let r () : EXN unit (Error true) = let j = () in net ()

let bleh2 () : PURE (option' unit) (fun p -> p (Error true)) = reify (r ()) ()

let falso () : Lemma False by (unfold_def (`bleh2); unfold_def (`r); norm [reify_]) = let x = bleh2 () in ()

cc @aseemr

[aseemr]

Thanks for the report. I think this discrepancy got introduced recently when I introduced the use of returns for binding with pure computations. We didn't notice because existing code is using consistent returns and lifts.

I will fix it soon.

EDIT: this is not the reason, we expect lift to be a monad morphism, here is it not, and F* is not checking it either.

[aseemr]

This no longer verifies in F*, since we don't allow reification of layered effects for proofs anymore. Therefore, removing the unsoundness label for now. The file adapted to the latest layered effects syntax etc. is as follows.

module Test

open FStar.Error
open FStar.Tactics

type unit : Type = unit
type bool : Type = bool

type option' a = optResult bool a

let conv (#a:Type) (v : optResult bool a) (w : optResult bool unit) : bool =
  match v , w with
  | Error true , Error true -> true
  | Error false , Error false -> true
  | Correct _ , Correct _ -> true
  | _ , _ -> false

type repr (a:Type) (b : optResult bool unit) = unit -> Pure (option' a) True (fun x -> b2t (conv x b))

let return (a:Type) (x:a) : repr a (Correct ()) = fun _ -> Correct x

let bind (a:Type) (b:Type) wp_f wp_g (f:repr a wp_f) (g:(x:a -> repr b wp_g))
: repr b (
   match wp_f with
   | Error e -> Error e
   | Correct () -> wp_g)
= fun _ ->
  let r = f () in
  match r with
  | Error e -> Error e
  | Correct x -> g x ()

let subcomp (a:Type) wp_f (f:repr a wp_f) : repr a wp_f = f

let if_then_else (a:Type) (wp_f) (f:repr a wp_f) (g:repr a wp_f) (p:bool) : Type
  = repr a wp_f

[@@ allow_informative_binders]
total reifiable reflectable
effect {
  EXN (a:Type) (_:optResult bool unit)
  with {repr; return; bind; subcomp; if_then_else}
}

let lift_pure_exn (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp) : repr a (Error false) = fun _ -> Error false

sub_effect PURE ~> EXN = lift_pure_exn

let net () : EXN unit (Error true) = EXN?.reflect (fun _ -> Error true) <: EXN unit (Error true)

let r () : EXN unit (Error true) = let j = () in net ()

let bleh2 () : PURE (option' unit) (fun p -> p (Error true)) = reify (r ()) ()

[@@ expect_failure]
let falso () : Lemma False by (unfold_def (`bleh2); unfold_def (`r); norm [reify_]) = let x = bleh2 () in ()

We disallow reification of layered effects for proofs for a different reason though. Currently the (inferred) arguments to the layered effect combinators are not persisted in the AST. As a result, during reification we cannot reproduce their values. Until we fix this properly, we have disallowed reification for proofs. (@tahina-pro had some examples where he was able to prove False if we allowed this.)

Coming to this bug specifically, if we allowed reification, the proof of False goes through because when we typecheck the definition of r, its body let j = () in net () is typechecked using the bind Tot EXN rule, which simply uses substitution. However, the body is elaborated to Meta_monadic (EXN, let x = Meta_monadic_lift (()) in net ()) (roughly), inserting a lift_PURE_EXN before binding the two computations. As a result, when reification happens, we normalize using the lift, and that introduces the consistency.

One solution here is to make sure that the body of r is elaborated in a manner consistent with how it is typechecked. Something like Meta_Tot_application (let x = () in net ()), so that the normalization during reification also happens by substitution.

More generally, the typechecking of monadic let and their elaboration into Meta nodes has gone out-of-sync in the typechecker. Earlier two monadic computation could only be combined by lift and bind. But now we have polymonadic binds, return and then bind, etc. So I am doing a proper cleanup when the elaboration happens in the bind routines in a manner consistent with how typechecking proceeds.

cc @nikswamy , @erivas for comments.