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:       t
  
    | Tm_abs (binders, repr, something) ->
        // For parameterized data types... check that this only appears at
        // top-level
        let subst = SS.opening_of_binders binders in
        let repr = SS.subst subst repr in
        let env = { env with env = push_binders env.env binders } in
        let repr = star_type env repr in
        let repr = SS.close binders repr in
        mk (Tm_abs (binders, repr, something)
  
    | Tm_abs _
    | Tm_uinst _
  
negative.code:   definitions: list<(lid * typ)>;
  }
  
  type nm = | N of typ | M of typ
  
  let 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"
  
  let is_monadic_arrow n =
    match n with
    | Tm_arrow (_, { n = n}) ->
        nm_of_comp n
    | _ ->
        failwith "unexpected_argument: [is_monadic_arrow]"
  
  