anchor.diff:    let t = SS.compress t in
     match t.n with
     | Tm_arrow (binders, _) ->
  -      // N-arrows and T-arrows
  +      // TODO: check that this is not a dependent arrow.
         let binders = List.map (fun (bv, aqual) ->
           { bv with sort = star_type env bv.sort }, aqual
         ) binders in
         begin match is_monadic_arrow t.n with
         | N hn ->
  -          (* Simple case:
  -           *   (H_0  -> ... -> H_n)* =
  -           *    H_0* -> ... -> H_n*
  -           *)
  +          // Simple case:
  +          //   (H_0  -> ... -> H_n)* = H_0* -> ... -> H_n*
             mk (Tm_arrow (binders, mk_Total (star_type env hn)))
  -      | T a ->
  -          (* F*'s arrows are n-ary (and the intermediary arrows are pure), so the rule is:
  -           *   (H_0  -> ... -> H_n  -t-> A)* =
  -           *    H_0* -> ... -> H_n* -> (A* -> Type) -> Type
  -           *)
  +      | M a ->
  +          // F*'s arrows are n-ary (and the intermediary arrows are pure), so the rule is:
  +          //   (H_0  -> ... -> H_n  -t-> A)* = H_0* -> ... -> H_n* -> (A* -> Type) -> Type
             mk (Tm_arrow (
               binders @ [ S.null_bv (mk_star_to_type env a), S.as_implicit false ],
               mk_Total Util.ktype))
         end
   
     | Tm_app (head, args) ->
  -      // Sums and products. TODO: do not treat known types (e.g. [st]) as
  -      // abstract symbols, but look them up in our own environment and reduce
  -      // them accordingly
  +      // Sums and products. TODO: re-use the cache in [env] to not recompute
  +      // (st a)* every time.
         let rec is_valid_application head =
           match (SS.compress head).n with
           | Tm_fvar fv when (
  
positive.code:   let body = mk (Tm_app (mk (Tm_bvar p), [ e, S.as_implicit false ])) in
    U.abs [ S.mk_binder p ] body None
  
  // [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.
  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 t2.n <> Tm_unknown && not (Rel.is_trivial (Rel.teq env t1 t2)) then
          raise (Err ("[check]: term does not have the expected type"));
      in
      match rec_nm, e, context_nm with
  
negative.code:   | Tm_app _ ->
        return_if (infer env e)
  
    | Tm_let ((false, [ binding ]), e2) ->
        mk_let env binding e2
          // Body of the let is pure: just defer the check to the continuation
          (fun env e2 -> check env e2 context_nm)
          // Body of the let is monadic: this is a bind, and we must strengthen
          // the check on the continuation to ensure it is a monadic computation
          (fun env e2 ->
            let strip_m = function
              | M t, e -> t, e
              | _ -> failwith "impossible"
            in
            match context_nm with
            | N t -> strip_m (check env e2 (M t))
            | M _ -> strip_m (check env e2 context_nm))
  
    | Tm_match (e0, branches) ->
        // This is similar to the [let] case above. The [match] checks that the
        // types of the branches work; it also demands that the scrutinee be a
        // non-monadic computation.
        mk_match env e0 branches (fun env body -> check env body context_nm)
  
    | _ ->
        failwith (Util.format1 "[check]: todo %s" (Print.term_to_string e))
  
  
  and infer (env: env) (e: term): nm * term =
  