anchor.diff:              //              debug g (fun () -> printfn "Let %s at type %s; expected effect is %A\n" (Print.lbname_to_string lbname) (Print.typ_to_string t) f_e);
                 match t.n with
                   | Tm_arrow(bs, c) when (List.hd bs |> is_type_binder) ->
  +                   let bs, c = SS.open_comp bs c in
                     //need to generalize, but will erase all the type abstractions;
                     //If, after erasure, what remains is not a value, then add an extra unit arg. to preserve order of evaluation/generativity
                     //and to circumvent the value restriction
  +
  +                  //TODO: ERASE ONLY THOSE THAT ABSTRACT OVER PURE FUNCTIONS in Type(i), 
  +                  //      NOT, e.g., (x:int -> St Type)
                      let tbinders, tbody =
  -                        match Util.prefix_until (function (Inr _, _) -> true | _ -> false) bs with
  -                            | None -> bs, Util.comp_result c
  -                            | Some (bs, b, rest) -> bs, mk_Typ_fun(b::rest, c) None c.pos in
  -
  -                   let n = List.length tbinders in
  +                        match Util.prefix_until (not << is_type_binder) bs with
  +                            | None -> bs, U.comp_result c
  +                            | Some (bs, b, rest) -> bs, U.arrow (b::rest) c in
  +
  +                   let n_tbinders = List.length tbinders in
                      let e = normalize_abs e in
                      begin match e.n with
  -                      | Exp_abs(bs, body) ->
  -                        if n <= List.length bs
  -                        then let targs, rest_args = Util.first_N n bs in
  +                      | Tm_abs(bs, body, _) ->
  +                        if n_tbinders <= List.length bs
  +                        then let targs, rest_args = Util.first_N n_tbinders bs in
   //                             printfn "tbinders are %s\n" (tbinders |> (Print.binders_to_string ", "));
   //                             printfn "tbody is %s\n" (Print.typ_to_string tbody);
   //                             printfn "targs are %s\n" (targs |> Print.binders_to_string ", ");
  -                             let expected_t = match Util.mk_subst_binder targs tbinders with
  -                                | None -> failwith "Not enough type binders in the body of the let expression"
  -                                | Some s -> Util.subst_typ s tbody in
  +                             let expected_t = 
  +                                let s = List.map2 (fun (x, _) (y, _) -> S.NT(x, S.bv_to_name y)) tbinders targs in
  +                                SS.subst s tbody in
   //                             printfn "After subst: expected_t is %s\n" (Print.typ_to_string expected_t);
  -                             let targs = targs |> List.map (function (Inl a, _) -> a | _ -> failwith "Impossible") in
  -                             let env = List.fold_left (fun env a -> Env.extend_ty env a None) g targs in
  +                             let env = List.fold_left (fun env (a, _) -> UEnv.extend_ty env a None) g targs in
                                let expected_t = translate_typ env expected_t in
  -                             let polytype = targs |> List.map btvar_as_mltyvar, expected_t in
  +                             let polytype = targs |> List.map (btvar_as_mltyvar << fst), expected_t in
                                let add_unit = match rest_args with
                                   | [] -> not (is_value_or_type_app body) //if it's a pure type app, then it will be extracted to a value in ML; so don't add a unit
                                   | _ -> false in
                                let rest_args = if add_unit then (unit_binder::rest_args) else rest_args in
  -                             let body = match rest_args with | [] -> body | _ -> mk_Exp_abs(rest_args, body) None e.pos in
  +                             let body = match rest_args with 
  +                                | [] -> body 
  +                                | _ -> U.abs rest_args body None in
                                (lbname, f_e, (t, (targs, polytype)), add_unit, body)
   
                           else (* fails to handle:
  
positive.code:         let g, (p, whens) = extract_one_pat false g p in
          let when_clause = mk_when_clause whens in
          g, [(p, when_clause)] 
  
  let normalize_abs (t0:term) =
      let rec aux bs t =
          let t = SS.compress t in
          match t.n with
              | Tm_abs(bs', body, _) -> aux (bs@bs') body
              | _ ->
                let e' = U.unascribe t in
                if U.is_fun e'
                then aux bs e'
                else U.abs bs e' in
     aux [] t0
  
  let ffi_mltuple_mlp (n:int) : mlpath =
      let name = if (2<n && n<6) then ("mktuple"^(Util.string_of_int n)) else (if n=2 then "mkpair" else (failwith "NYI in runtime/allocator/camlstack.mli")) in
  
negative.code:             else e in
      (e, f, ty)
  
  (* maybe_coerce g e ty expect:
          Inserts an Obj.magic around e if ty </: expect
   *)
  let maybe_coerce (g:env) e ty (expect:mlty) : mlexpr  =
      let ty = eraseTypeDeep g ty in
      match type_leq_c g (Some e) ty expect with 
  