F* should disallow degenerate effects

[857b]

F* (https://github.com/FStarLang/FStar/commit/5bcd16865e5161ccbc7b2b9ead96ba099618adf8) does not seem to retypecheck the parameters of the effect combinators when they are used. This is probably intentional since it notably avoids rechecking the monotonicity of pure_wp (for instance in Steel's polymonadic bind). However I found that it is unsound, because of implicit dependencies (similary to https://github.com/FStarLang/FStar/issues/2635). Here is an example, using a bind combinator:

module S0

[@@ erasable]
noeq type bool0 = | BT | BF

[@@ erasable]
noeq type index : (b : bool0) -> Type =
  | IT : index BT

let elim_index_BF (i : index BF) : Lemma False
  = ()

type repr0 (a : Type) (b : bool0) (p : index b)
  = eqtype_as_type unit

let return0 (a : Type) (x : a) : repr0 a BT IT
  = ()

let bind0
      (a0 a1 : Type) (b0 b1 : bool0)
      (p0 : index b0)
      (p1 : index b1) // no dependency in a0
      (r0 : repr0 a0 b0 p0) (r1 : a0 -> repr0 a1 b1 p1)
  : repr0 a1 b1 p1
  = ()

total reflectable effect {
  E0 (a : Type) (b : bool0) (p : index b)
  with {
    repr   = repr0;
    return = return0;
    bind   = bind0;
  }
}

let lift_tot_e0 (a : Type) (wp : pure_wp a) (f : eqtype_as_type unit -> PURE a wp)
  : repr0 a BT IT
  = ()

sub_effect PURE ~> E0 = lift_tot_e0


let repr1 (a : Type) (b : bool0)
  = index b

let return1 (a : Type) (x : a) : repr1 a BT
  = IT

let bind1
      (a0 a1 : Type) (b0 b1 : bool0)
      (r0 : repr1 a0 b0) (r1 : a0 -> repr1 a1 b1)
  : Pure (repr1 a1 b1) False (fun _ -> True)
  = false_elim ()

// getting a warning (330) here since https://github.com/FStarLang/FStar/pull/2654
// but recovering an element of the representation type is enough to conclude here
total reifiable effect {
  E1 (a : Type) (b : bool0)
  with {
    repr   = repr1;
    return = return1;
    bind   = bind1;
  }
}

let lift_tot_e1 (a : Type) (wp : pure_wp a) (f : eqtype_as_type unit -> PURE a wp)
  : repr1 a BT
  = IT

sub_effect PURE ~> E1 = lift_tot_e1


let lift_e0_e1
      (a : Type) (b : bool0) (p : index b)
      (r : repr0 a b p)
  : repr1 a b
  = p

sub_effect E0 ~> E1 = lift_e0_e1


let return_False () : E0 (squash False) BT IT
  = E0?.reflect ()

let make_BF (f : squash False) : unit -> E0 unit BF (false_elim ())
  = false_elim ()

// This definition in E0 is ill-typed:
// by binding on the right-hand-side:
//   [(f : squash False) -> make_BF f () : E0 unit BF (false_elim ())]
// we obtain a term of effect [E0 unit BF (false_elim ())] (in a context without [f : squash False]).
// We cannot directly obtain this at top-level since the [false_elim ()] would be retypechecked.
// The purpose of E1 is to remove this term from the index of the effect.
let absurd_e1 () : E1 unit BF
  = let f = return_False () in
    make_BF f ()

// Using the reification of E1
let absurd () : Lemma False
  = elim_index_BF (reify (absurd_e1 ()))

There are many administrative definitions but the key points are:

• We define a bind combinator bind0 where the indices of the right-hand-side (in particular p1) are not allowed to depend on the bound variable.
• In absurd_e1, we use this combinator with a rhs whose indices implicitly depends (because of subtyping) on the bound variable f. We obtain an ill-typed effect index. This is the point where F* is unsound.
• From there we can obtain a term in an effect that should be non-inhabited, and a proof of ⊥ using reification.

This issue probably also affects the polymonadic bind combinators and the if-then-else combinators (because the indexes of the branches can depend on the guard).

[857b]

I just observed that in the if-then-else case, F* may in fact introduce the hypothesis in the branches. So the if-then-else is maybe still sound.

[aseemr]

Related to #2635.

[857b]

In fact, it seems that the lift (or polymonadic bind) of PURE produces some ill-typed use of effect combinators for standard effects. For instance:

module S1
open Steel.Effect

let call_nat_req (n : nat) = True
assume val call_nat (n : nat) : Steel unit emp (fun _ -> emp) (fun _ -> call_nat_req n) (fun _ _ _ -> True)

#push-options "--print_bound_var_types"

let test (i : int)
  : Steel unit emp (fun _ -> emp) (requires fun _ -> i >= 0) (ensures fun _ _ _ -> True)
  by FStar.Tactics.(norm []; Tactics.fail "VC")
  = call_nat i

Yields a VC that contains:

forall (n: nat). ...
    (bind_pure_steel__req (pure_assume_wp0 (i == n)) (fun _ _ -> call_nat_req i))

Which is ill-typed since the type of bind_pure_steel__req does not allow the req of the Steel computation to assume the wp: at this point one cannot justify that i >= 0. The VC becomes well-typed after some unfolding because call_nat_req will only appear under wp.

[aseemr]

The issue was automatically closed but #2760 fixes it only partially, we still need to implement the check for degenerate effects.