anchor.diff:                match (SS.compress t_norm).n with
                 | Tm_arrow(formals, c) ->
                   let formals, c = SS.open_comp formals c in
  -                let tres = get_result_type c in
  -                let binders, body = eta_expand [] formals e tres in
  -                (binders, body, formals, tres), false
  +                let tres_comp = get_result_comp c in
  +                let binders, body = eta_expand [] formals e (U.comp_result tres_comp) in
  +                (binders, body, formals, tres_comp), false
                 | Tm_refine (bv, _) -> aux' bv.sort
  -              | _ -> ([], e, [], t_norm), false
  +              | _ -> ([], e, [], S.mk_Total t_norm), false
               in
               aux' t_norm
             end
  
positive.code:               let formals, c = SS.open_comp formals c in
                let nformals = List.length formals in
                let nbinders = List.length binders in
                let tres = get_result_type c in
                if nformals < nbinders && U.is_total_comp c (* explicit currying *)
                then let bs0, rest = BU.first_N nformals binders in
                        let c =
                            let subst = List.map2 (fun (x, _) (b, _) -> NT(x, S.bv_to_name b)) formals bs0 in
                            SS.subst_comp subst c in
                        let body = U.abs rest body lopt in
                        (bs0, body, bs0, get_result_type c), false
                else if nformals > nbinders (* eta-expand before translating it *)
                then let binders, body = eta_expand binders formals body tres in
                        (binders, body, formals, tres), false
                else (binders, body, formals, tres), false
  
              | Tm_refine(x, _) ->
                  fst (aux norm x.sort), true
  
negative.code:       : (S.binders    //arguments of the lambda abstraction
        * S.term        //body of the lambda abstraction
        * S.binders     //arguments of the function type, length of this component is equal to the first
        * S.comp)       //result comp
        * bool          //if set, we should generate a curried application of f
      =
        (* The input type [t_norm] might contain reifiable computation type which must be reified at this point *)
        let get_result_comp c =
            if is_reifiable_comp env.tcenv c
            then S.mk_Total <| reify_comp ({env.tcenv with lax = true}) c U_unknown
            else c
        in
  
        let rec aux norm t_norm =
  