anchor.diff:    match (SS.compress e).n with
     | Tm_abs (_, _, what) ->
         if is_monadic what then
  -        star_expr e t InPure
  +        star_expr e 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)))
  
positive.code:       mk (Tm_match (e0, branches))
  
    | Tm_app (head, args) ->
        failwith "TODO: Tm_app"
  
  
    | Tm_bvar _ ->
        failwith "TODO: Tm_bvar"
    | Tm_name _ ->
        failwith "TODO: Tm_name"
    | Tm_fvar _ ->
        failwith "TODO: Tm_fvar"
    | Tm_uinst _ ->
        failwith "TODO: Tm_uinst"
    | Tm_constant _ ->
  
negative.code:       let body = SS.subst subst body in
  
        let ret_type =
          (* match (SS.compress t).n with
          | Tm_arrow (binders, comp) ->
              let binders, comp = open_comp binders comp in
              begin match comp.n with
              | Total t | GTotal t | Comp { result_typ = t } ->
                  t
              end *)
          match what with
          | Some (Inl { res_typ = t }) ->
              t
          | _ ->
              failwith "what impossible"
        in
  
        let binders = List.map (fun (bv, qual) ->
          let sort = star_type bv.sort in
          { bv with sort = sort }, qual
        ) binders in
        let body = star_expr body (if is_monadic what then InMonad ret_type else InPure) in
        let body = close binders body in
        let binders = close_binders binders in
        wrap_if m (mk (Tm_abs (binders, body, what)))
  
    | Tm_ascribed (e, _, _) ->
        star_expr e m
  
    | Tm_match (e0, branches) ->
        // TODO: currently, no one is checking that [e0] is a pure computation
        let e0 = star_expr e0 InPure in
        let branches = List.map (fun b ->
          match open_branch b with
          | pat, None, body ->
              let body = star_expr body m in
              close_branch (pat, None, body)
          | _ ->
              raise (Err ("No when clauses in the definition language"))
  