anchor.diff:                      (N.comp_to_string env c);
     c
   
  -
   (* private *)
  +
  +
  +let effect_args_from_repr (repr:term) (is_layered:bool) (r:Range.range) : list<term> =
  +  let err () =
  +    raise_error (Errors.Fatal_UnexpectedEffect,
  +      BU.format2 "Could not get effect args from repr %s with is_layered %s"
  +        (Print.term_to_string repr) (string_of_bool is_layered)) r in
  +  let repr = SS.compress repr in
  +  if is_layered
  +  then match repr.n with
  +       | Tm_app (_, _::is) -> is |> List.map fst
  +       | _ -> err ()
  +  else match repr.n with 
  +       | Tm_arrow (_, c) -> c |> U.comp_to_comp_typ |> (fun ct -> ct.effect_args |> List.map fst)
  +       | _ -> err ()
   
   
   (*
  
positive.code:         let bs, c = SS.open_comp bs c in
          let bs_subst = NT (List.hd bs |> fst, x_a |> fst |> S.bv_to_name) in
          let c = SS.subst_comp [bs_subst] c in
          (match (SS.compress (U.comp_result c)).n with
           | Tm_app (_, _::is) ->
             is |> List.map fst |> List.map (SS.subst subst)
           | _ -> raise_error (bind_t_shape_error "g's type is not a repr type") r1)
        | _ -> raise_error (bind_t_shape_error "g's type is not an arrow") r1 in
  
      let env_g = Env.push_binders env [x_a] in
      List.fold_left2
  
negative.code: 
    let r = Env.get_range env in
  
    let ct = U.comp_to_comp_typ c in
  
    let u, a, c_is = List.hd ct.comp_univs, ct.result_typ, ct.effect_args |> List.map fst in
  