anchor.diff:      let t0 = Util.compress_typ t in
       match t0.n with 
         | Typ_btvar a -> 
  -        lookup_typ_var env a, [], []
  +        let t, c = lookup_typ_var env a in
  +        t, [c], []
   
         | Typ_const fv -> 
           lookup_free_tvar env fv, [], []
   
  -      | Typ_fun(binders, res) -> (* TODO: add sharing *)
  -        let doit binders (res:comp) =
  -            let tsym, ttm, fsym, f = fresh_vars "funtype" "f" in
  -            let pretype = mk_tester "Typ_fun" (mk_PreType f) in
  -            let t_has_kind = mk_HasKind ttm Term.mk_Kind_type in
  -            let f_hastype_t = mk_HasType f ttm in
  -            let guard, decls = 
  -                if not <| Absyn.Util.is_pure_comp res
  -                then pretype, [] 
  -                else let vars, guards, env', decls, _ = encode_binders None binders env in 
  -                     let app = mk_ApplyE f vars in
  -                     if Util.is_total_comp res
  -                     then let res_pred, decls' = encode_typ_pred' None (Util.comp_result res) env' app in
  -                          let app_pred = mkForall([app], vars, mkImp(mk_and_l guards, res_pred)) in
  -                          mkAnd(pretype, app_pred), decls@decls'
  -                     else pretype, decls in
  -            ttm, [tsym, Term.mkAnd(t_has_kind, mkForall_fuel([f_hastype_t], [fsym], mkImp(f_hastype_t, guard)))], decls in
  -
  -        begin match binders |> Util.prefix_until (function (Inr _, _) -> true | _ -> false) with 
  -            | Some (t_binders, first_v_binder, rest) -> //explicitly curry the type-binders, since partial type-applications arise via unification commonly in ML programs
  -              begin match t_binders with 
  -                | [] -> doit binders res
  -                | _ -> 
  -                  let res = mk_Typ_fun(first_v_binder::rest, res) (Some ktype) t0.pos |> Syntax.mk_Total in
  -                  doit t_binders res
  -             end
  -            | None -> doit binders res 
  -        end
  +      | Typ_fun(binders, res) -> 
  +        (* TODO: sharing; check that currying works properly; handling non-total functions *)
  +        if   Absyn.Util.is_total_comp res
  +        then let vars, cvars, guards, env', decls, _ = encode_binders None binders env in 
  +             let fsym = varops.fresh "f", Term_sort in
  +             let f = mkBoundV fsym in
  +             let app = mk_ApplyE f vars in      
  +             let res_pred, cvars', decls' = encode_typ_pred' None (Util.comp_result res) env' app in
  +
  +             let cvars = exclude_cvars binders (cvars@cvars') in
  +             let cvar_binders = cvar_binders cvars in
  +
  +             let tsym = varops.fresh "Typ_fun" in
  +             let tdecl = Term.DeclFun(tsym, cvar_sorts cvars, Type_sort, None) in
  +             let t = Term.mkApp(tsym, cvar_terms cvars) in
  +             let t_has_kind = mk_HasKind t Term.mk_Kind_type in
  +
  +
  +             let k_assumption = Term.Assume(Term.mkForall([t_has_kind], cvar_binders, t_has_kind), None) in
  +             let f_has_t = mk_HasType f t in
  +             let t_interp = Term.Assume(mkForall_fuel([f_has_t], fsym::cvar_binders, 
  +                                                      mkIff(f_has_t, 
  +                                                            mkAnd(mk_tester "Typ_fun" (mk_PreType f), 
  +                                                                  mkForall([app], vars,  
  +                                                                              mkImp(mk_and_l guards, res_pred))))), 
  +                                       Some (tsym ^ " interpretation")) in 
  +            
  +             t, cvars, decls@decls'@[tdecl; k_assumption; t_interp]              
  +
  +        else let tsym = varops.fresh "funtype" in
  +             let t = Term.mkFreeV(tsym, Type_sort) in
  +             let tdecl = Term.DeclFun(tsym, [], Type_sort, None) in
  +             t, [], [tdecl] (* TODO: At least preserve alpha-equivalence of non-pure function types *)
         
         | Typ_refine _ -> 
           let x, f = match Tc.Normalize.normalize_refinement env.tcenv t0 with 
  
positive.code:               encode_typ_term t env
          end
  
        | Typ_lam(bs, t) ->
          let vars, guards, env, decls, _ = encode_binders None bs env in
          let name = varops.fresh (Print.tag_of_typ t0), Type_sort in 
          let tag = mkBoundV name in 
          let ktm, decls'' = encode_knd (Tc.Recheck.recompute_kind t0) env tag in
          let app = mk_ApplyT tag vars in
          let body, vars_body, decls' = encode_typ_term t env in
          let eq = close_ex vars_body (mkEq(app, body)) in
          let guard = mkForall([app], vars, mkImp(mk_and_l guards, eq)) in
          tag, [(name, Term.mkAnd(ktm, guard))], decls@decls''@decls'
  
        | Typ_ascribed(t, _) -> 
          encode_typ_term t env
  
negative.code:                     if is_null_binder b   
                      then withenv env <| fresh_bvar "x" Term_sort
                      else gen_term_var env x in
                  let guard_x_t, cvars, decls' = encode_typ_pred' fuel_opt (norm_t env t) env xx in
                  (xxsym, Term_sort),
                  cvars, 
                  guard_x_t,
                  env', 
                  decls',
                  Inr x in
          v::vars, cvars@cvars', g::guards, env, decls@decls', n::names) ([], [], [], env, [], []) in
      List.rev vars,
      cvars,
      List.rev guards,
      env, 
      decls,
      List.rev names
  
  and encode_typ_pred' (fuel_opt:option<term>) (t:typ) (env:env_t) (e:term) : term * closure_vars * decls_t = 
      let t = Util.compress_typ t in 
      match (Util.unmeta_typ t).n with 
          | Typ_refine(x, f) -> 
  