anchor.diff:      let b, u_b = fresh_a_and_u_a "b" in
       let rest_bs =
         match (SS.compress ty).n with
  -      | Tm_arrow ((a', _)::(b', _)::bs, _) when List.length bs >= 2 ->
  -        let bs, _ = List.splitAt (List.length bs - 2) bs in
  -        let substs = [NT (a', bv_to_name (fst a)); NT (b', bv_to_name (fst b))] in
  -        SS.subst_binders substs bs
  +      | Tm_arrow (bs, _) when List.length bs >= 4 ->
  +        (match SS.open_binders bs with
  +         | (a', _)::(b', _)::bs ->
  +           let bs, _ = List.splitAt (List.length bs - 2) bs in
  +           let substs = [NT (a', bv_to_name (fst a)); NT (b', bv_to_name (fst b))] in
  +           SS.subst_binders substs bs
  +         | _ -> failwith "Impossible!")
         | _ -> raise_error (Errors.Fatal_UnexpectedEffect, "") r in  //AR: TODO: FIXME
       let bs = a::b::rest_bs in
       let f, g_f =
  
positive.code:         ed.mname.str s
          (Print.tscheme_to_string (us, t)) (Print.tscheme_to_string (us, ty)) in
    
    //AR: TODO: FIXME: check that it is of the form a:Type -> ...is... -> Effect, also in tc_eff_decl
    let signature = check_and_gen' "signature" 1 None ed.signature in
  
    log_combinator "signature" signature;
  
    //AR: TODO: FIXME: check that repr has the type a:Type -> ...is... -> Type
    let repr = check_and_gen' "repr" 1 None ed.repr in
  
    log_combinator "repr" repr;
  
    let fresh_a_and_u_a (a:string) = U.type_u () |> (fun (t, u) -> S.gen_bv a None t |> S.mk_binder, u) in
    let fresh_x_a (x:string) (a:binder) = S.gen_bv x None (a |> fst |> S.bv_to_name) |> S.mk_binder in
  
    let fresh_repr (r:Range.range) env u (a_bv:bv) : term * guard_t =
      let signature = let us, t, ty = signature in (us, t) in
      let fail t = raise_error (Err.unexpected_signature_for_monad env0 ed.mname t) (snd ed.signature).pos in
      let _, signature = Env.inst_tscheme signature in
      match (SS.compress signature).n with
      | Tm_arrow (bs, _) ->
        let bs = SS.open_binders bs in
        (match bs with
         | a::is ->
           let is, g, _ = List.fold_left (fun (is, g, substs) (b, _) ->
             let t, _, g_t = TcUtil.new_implicit_var "" r env (SS.subst substs b.sort) in
             is @ [t], Env.conj_guard g g_t, substs @ [NT (b, t)]
           ) ([], Env.trivial_guard, [NT (fst a, bv_to_name a_bv)]) is in
           
           let repr_ts = let us, t, _ = repr in (us, t) in
           let repr = Env.inst_tscheme_with repr_ts [u] |> snd in
  
negative.code:     let x_a = fresh_x_a "x" a in
      let rest_bs =
        match (SS.compress ty).n with
        | Tm_arrow (bs, _) when List.length bs >= 2 ->
          (match SS.open_binders bs with
           | (a', _)::(x_a', _)::bs ->
             let substs = [NT (a', bv_to_name (fst a)); NT (x_a', bv_to_name (fst x_a))] in
             SS.subst_binders substs bs
           | _ -> failwith "Impossible!")
        | _ -> raise_error (Errors.Fatal_UnexpectedEffect, "") r in  //AR: TODO: FIXME
      let bs = a::x_a::rest_bs in
      let repr, g = fresh_repr r (Env.push_binders env bs) u_a (fst a) in
      let k = U.arrow bs (S.mk_Total' repr (Some u_a)) in
      let g_eq = Rel.teq env ty k in
      Rel.force_trivial_guard env (Env.conj_guard g g_eq);
      ret_us, ret_t, SS.close_univ_vars us (N.normalize [Beta] env k) in
  
    log_combinator "return_repr" return_repr;
  
  