anchor.diff:          M t2, (pat, guard, mk_return env t2 body)
       | M _, false ->
           failwith "impossible"
  -  ) nms branches;
  +  ) nms branches) in
     let branches = List.map close_branch branches in
     (if has_m then M t1 else N t1), mk (Tm_match (e0, branches))
   
   
  -and mk_let env binding e2 f =
  -    let e1 = binding.lbdef in
  -    // This is [let x = e1 in e2]. Open [x] in [e2].
  -    let x = Util.left binding.lbname in
  -    let x_binders = [ S.mk_binder x ] in
  -    let x_binders, e2 = SS.open_term x_binders e2 in
  -    begin match infer env e1 with
  -    | N t1, e1 ->
  -        // Simple case: just a regular let-binding. We defer checks to e2.
  -        let nm_rec, e2 = infer env e2 in
  -        nm_rec, mk (Tm_let ((false, [ { binding with lbdef = e1 } ]), SS.close x_binders e2))
  -    | M t1, e1 ->
  -        let t2, e2 = f env e2 in
  -        // Now, generate the bind.
  -        // p: A* -> Type
  -        let p_type = mk_star_to_type env t2 in
  -        let p = S.gen_bv "p" None p_type 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
  -        M t2, mk (U.abs [ S.mk_binder p ] body None)
  -    end
  -
  -
  -and check_n env e =
  +and mk_let (env: env) (binding: letbinding) (e2: term)
  +    (proceed: env -> term -> nm * term)
  +    (ensure_m: env -> term -> term * term) =
  +  let mk x = mk x None e2.pos in
  +  let e1 = binding.lbdef in
  +  // This is [let x = e1 in e2]. Open [x] in [e2].
  +  let x = Util.left binding.lbname in
  +  let x_binders = [ S.mk_binder x ] in
  +  let x_binders, e2 = SS.open_term x_binders e2 in
  +  begin match infer env e1 with
  +  | N t1, e1 ->
  +      let env = { env with env = push_bv env.env { x with sort = t1 } } in
  +      // Simple case: just a regular let-binding. We defer checks to e2.
  +      let nm_rec, e2 = proceed env e2 in
  +      nm_rec, mk (Tm_let ((false, [ { binding with lbdef = e1 } ]), SS.close x_binders e2))
  +  | M t1, e1 ->
  +      let t2, e2 = ensure_m env e2 in
  +      // Now, generate the bind.
  +      // p: A* -> Type
  +      let p_type = mk_star_to_type mk env t2 in
  +      let p = S.gen_bv "p" None p_type 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
  +      M t2, U.abs [ S.mk_binder p ] body None
  +  end
  +
  +
  +and check_n (env: env) (e: term): typ * term =
     let mn = N (mk Tm_unknown None e.pos) in
     match check env e mn with
     | N t, e -> t, e
     | _ -> failwith "[check_n]: impossible"
   
  -and check_m env e =
  +and check_m (env: env) (e: term): typ * term =
     let mn = M (mk Tm_unknown None e.pos) in
     match check env e mn with
     | M t, e -> t, e
     | _ -> failwith "[check_m]: impossible"
   
  -and comp_of_nm = function
  +and comp_of_nm (nm: nm): comp =
  +  match nm with
     | N t -> mk_Total t
     | M t -> mk_M t
   
  -and nm_of_comp = function
  -  | Total t ->
  -      N t
  -  | Comp c when lid_equals c.effect_name Const.monadic_lid ->
  -      M c.result_typ
  -  | _ ->
  -      failwith "[nm_of_comp]: impossible"
  -
  -and mk_M t =
  +and mk_M (t: typ): comp =
     mk_Comp ({
       effect_name = Const.monadic_lid;
       result_typ = t;
  -    effect_args = [ t ];
  +    effect_args = [ t, S.as_implicit false ];
       flags = []
     })
   
   
   let star_expr_definition env t =
  -  star_definition env t star_expr
  +  star_definition env t (fun env e _ ->
  +    let t, e = check_n env e in
  +    t, e)
  
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:   | Tm_name bv ->
        N (lookup_bv env.env bv), e
  
    | 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 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 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 (if is_monadic what then M t else N t), body
        in
  
        let body = close binders body 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 t_head, head = check_n env head in
        begin match (SS.compress t_head).n with
        | Tm_arrow (binders, comp) ->
            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))
        | _ ->
            raise (Err ("Not a function"))
        end
  
    | Tm_let ((false, [ binding ]), e2) ->
        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 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 (function | M _ -> true | _ -> false) nms in
    let nms, branches = List.split (List.map2 (fun nm (pat, guard, body) ->
      let check t t' =
        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
  