anchor.diff:  //   - [match e0 with xi -> ei] is translated as [match e0* with xi -> ei*]
   //   - for all other expressions: if the type provided from the context is [M _]
   //     then this is understood to be a [return], otherwise, recursively descend
  -type mode = InMonad | InPure
  -
  -let rec star_expr (e: term) (t: typ) (m: mode) =
  +type mode = InMonad of typ | InPure
  +
  +let wrap_if (m: mode) (e: term) =
  +  let mk x = mk x None e.pos in
  +  let mk_star_to_type = mk_star_to_type mk in
  +  match m with
  +  | InPure ->
  +      e
  +  | InMonad t ->
  +      let p_type = mk_star_to_type t in
  +      let p = S.gen_bv "p" None p_type in
  +      let body = mk (Tm_app (mk (Tm_bvar p), [ e, S.as_implicit false ])) in
  +      U.abs [ S.mk_binder p ] body None
  +
  +let rec star_expr (e: term) (m: mode) =
     let mk x = mk x None e.pos in
     let mk_star_to_type = mk_star_to_type mk in
     match (SS.compress e).n with
  
positive.code:   match (SS.compress e).n with
    | Tm_abs (_, _, what) ->
        if is_monadic what then
          star_expr e t InPure
        else
          raise (Err (Util.format2 "The following effect combinator should return in [M]: %s; \
            instead, it has type: %s\n" (Print.term_to_string e) (Print.term_to_string t)))
  
negative.code:       let x_binders, e2 = SS.open_term x_binders e2 in
        // Two cases.
        if is_monadic then begin
          match m with
            | InPure ->
                raise (Err ("monadic [let] in a context that does not return [M]"))
            | InMonad t ->
                // p: A* -> Type
                let p_type = mk_star_to_type t in
                let p = S.gen_bv "p" None p_type in
                // e1*
                let e1 = star_expr e1 InPure in
                // e2*
                let e2 = star_expr e2 m in
                // e2* p
                let e2 = mk (Tm_app (e2, [ mk (Tm_bvar p), S.as_implicit false ])) in
                // fun x -> e2* p; this takes care of closing [x].
                let e2 = U.abs x_binders e2 None in
                // e1* (fun x -> e2* p)
                let body = mk (Tm_app (e1, [ e2, S.as_implicit false ])) in
                U.abs [ S.mk_binder p ] body None
        end else
          let e1 = star_expr e1 InPure in
          let e2 = star_expr e2 InPure in
          mk (Tm_let ((false, [ { binding with lbdef = e1 } ]), SS.close x_binders e2))
  
    | Tm_let _ ->
        raise (Err ("[let rec] and [let and] not supported in the definition
  