anchor.diff:    | Tm_name bv ->
         N (lookup_bv env.env bv), e
   
  -  | Tm_abs (binders, term, what) ->
  +  | Tm_abs (binders, body, what) ->
         let binders = SS.open_binders binders in
         let subst = SS.opening_of_binders binders in
         let body = SS.subst subst body in
  -      let env = { env with env = push_binders env.env } in
  +      let env = { env with env = push_binders env.env binders } in
   
         let binders = List.map (fun (bv, qual) ->
           let sort = star_type env bv.sort in
           { bv with sort = sort }, qual
         ) binders in
  -      let ret_type, body =
  +      let comp, body =
           let check_what = if is_monadic what then check_m else check_n in
           let t, body = check_what env body in
  -        comp_of_nm t, body
  +        comp_of_nm (if is_monadic what then M t else N t), body
         in
   
         let body = close binders body in
  -      let binders = close_binders binders in
         let t =
           let binders = List.map (fun (bv, _) ->
             S.mk_binder (S.null_bv bv.sort)
           ) binders in
  +        let binders = close_binders binders in
           mk (Tm_arrow (binders, comp))
         in
  +      let binders = close_binders binders in
         N t, mk (Tm_abs (binders, body, what))
   
     | Tm_app (head, args) ->
         // TODO: hook up the lookup for already-defined combinators here
  -      let head, t_head = check_n env head in
  +      let t_head, head = check_n env head in
         begin match (SS.compress t_head).n with
         | Tm_arrow (binders, comp) ->
  -          // TODO: check that there is actually no dependency of any kind here,
  -          // no polymorphism whatsoever, and that I can actually return just the
  -          // result type...
  -          let args, t_args = List.split (List.map2 (fun ((bv, _), (arg, _)) ->
  -            let _, arg = check env arg bv.sort in
  -            arg, bv.sort
  -          ) (binders, args)) in
  -          nm_of_comp comp, mk (Tm_app (head, args))
  +          let binders, comp = SS.open_comp binders comp in
  +          // Return the starred argument (for elaboration) and a substitution to
  +          // apply on the computation to get the original return type
  +          let args, subst_elts = List.split (List.map2 (fun (bv, _) (arg, q) ->
  +            let _, starred_arg = check env arg (N bv.sort) in
  +            (starred_arg, q), NT (bv, arg)
  +          ) binders args) in
  +          let comp = SS.subst_comp subst_elts comp in
  +          nm_of_comp comp.n, mk (Tm_app (head, args))
         | _ ->
  -          failwith "Tm_app doesn't have Tm_arrow"
  +          raise (Err ("Not a function"))
         end
   
     | Tm_let ((false, [ binding ]), e2) ->
  -      // Check that the continuation of the let is a monadic computation but
  -      // infer the type
  -      mk_let env binding e2 check_m
  +      mk_let env binding e2 infer check_m
   
     | Tm_match (e0, branches) ->
         mk_match env e0 branches infer
   
  +  | _ ->
  +      failwith (Util.format1 "[infer]: todo %s" (Print.term_to_string e))
   
   and mk_match env e0 branches f =
  +  let mk x = mk x None e0.pos in
  +  // TODO: automatically [bind] when the scrutinee is monadic
     let _, e0 = check_n env e0 in
     let nms, branches = List.split (List.map (fun b ->
       match open_branch b with
       | pat, None, body ->
  -        let nm, body = f env body
  -        nm, body
  +        let env = { env with env = List.fold_left push_bv env.env (pat_bvs pat) } in
  +        let nm, body = f env body in
  +        nm, (pat, None, body)
       | _ ->
           raise (Err ("No when clauses in the definition language"))
     ) branches) in
     let t1 = match List.hd nms with M t1 | N t1 -> t1 in
  -  let has_m = List.existsb (fun M _ -> true | _ -> false) nms in
  -  let nms, branches = List.map2 (fun nm (pat, guard, body) ->
  +  let has_m = List.existsb (function | M _ -> true | _ -> false) nms in
  +  let nms, branches = List.split (List.map2 (fun nm (pat, guard, body) ->
       let check t t' =
  -      if t.n <> Tm_unknown && not (Rel.is_trivial (Rel.teq env t' t)) then
  +      if not (Rel.is_trivial (Rel.teq env.env t' t)) then
           raise (Err ("[infer]: branches do not have the same type"))
       in
       match nm, has_m with
  
positive.code:   definitions: list<(lid * typ)>;
  }
  
  let is_monadic_arrow n =
    match n with
    | Tm_arrow (_, { n = Comp c}) when lid_equals c.effect_name Const.monadic_lid ->
        T c.result_typ
    | Tm_arrow (_, { n = Total t}) ->
        N t
    | Tm_arrow _ ->
        raise (Err "Prims.M and Prims.Tot are the only possible effects in the \
          definition language")
    | _ ->
        failwith "unexpected_argument: [is_monadic_arrow]"
  
  
negative.code:   let body = mk (Tm_app (mk (Tm_bvar p), [ e, S.as_implicit false ])) in
    U.abs [ S.mk_binder p ] body None
  
  let is_unknown = function | Tm_unknown -> true | _ -> false
  
  // [check] ensures that the sub-term is of the desired effect (N or M) _and_
  // of the desired type. In case the type is [Tm_unknown], [check] skips the
  // latter check. It always returns the desired effect and the desired type or,
  // if it was unknown, the inferred type (pre star-transformation). Furthermore,
  // it returns a starred version of the (elaborated) term.
  let rec check (env: env) (e: term) (context_nm: nm): nm * term =
    let mk x = mk x None e.pos in
    let return_if (rec_nm, e) =
      let check t1 t2 =
        if not (is_unknown t2.n) && not (Rel.is_trivial (Rel.teq env.env t1 t2)) then
          raise (Err ("[check]: term does not have the expected type"));
      in
      match rec_nm, e, context_nm with
  