anchor.diff:    //     (BU.dflt "none" (BU.map_opt l.mlift_term (fun l -> Print.term_to_string (l U_zero arg wp e))))
     // in
   
  -  let order = edge::env.effects.order in
  -  let ms = env.effects.decls |> List.map (fun (e, _) -> e.mname) in
  -
     let find_edge order (i, j) =
       if lid_equals i j
       then id_edge i |> Some
       else order |> BU.find_opt (fun e -> lid_equals e.msource i && lid_equals e.mtarget j) in
   
  -    (* basically, this is Warshall's algorithm for transitive closure,
  -       except it's ineffcient because find_edge is doing a linear scan.
  -       and it's not incremental.
  -       Could be made better. But these are really small graphs (~ 4-8 vertices) ... so not worth it *)
  -  let order =
  -    let fold_fun order k =
  -      order@(ms |> List.collect (fun i ->
  -                if lid_equals i k then []
  -                else ms |> List.collect (fun j ->
  -                  if lid_equals j k
  -                  then []
  -                  else match find_edge order (i, k), find_edge order (k, j) with
  -                       | Some e1, Some e2 -> [compose_edges e1 e2]
  -                       | _ -> [])))
  -    in ms |> List.fold_left fold_fun order
  -  in
  -  let order = BU.remove_dups (fun e1 e2 -> lid_equals e1.msource e2.msource
  -                                     && lid_equals e1.mtarget e2.mtarget) order in
  +  let ms = env.effects.decls |> List.map (fun (e, _) -> e.mname) in
  +
  +  (*
  +   * AR: we first compute all the new edges induced by the input edge
  +   *     for a new edge M ~> N
  +   *
  +   *     1. if there already exists an edge M ~> N, we ignore the new edge
  +   *        we should emit a warning but for now we don't
  +   *     2. if there exists a polymonadic subcomp M N, then we give an error
  +   *        since to decide M <: N, there are now two routes:
  +   *          polymonadic_subcomp or lift M to N and then use subcomp combinator of N
  +   *     3. if there exists a polymonadic subcomp N M, then also we give an error
  +   *        since it's a cycle
  +   *
  +   *     Conflicts with polymonadic binds will be checked later when we compute joins
  +   *)
  +
  +  //all nodes i such that i ~> src is an edge
  +  let all_i_src = ms |> List.fold_left (fun edges i ->
  +    match find_edge env.effects.order (i, edge.msource) with
  +    | Some e -> e::edges
  +    | None -> edges) [] in
  +
  +  //all nodes j such that tgt ~> j is an edge
  +  let all_tgt_j = ms |> List.fold_left (fun edges j ->
  +    match find_edge env.effects.order (edge.mtarget, j) with
  +    | Some e -> e::edges
  +    | None -> edges) [] in
  +
  +  let new_edges = List.fold_left (fun edges i_src ->
  +    List.fold_left (fun edges tgt_j ->
  +      let src = i_src.msource in
  +      let tgt = tgt_j.mtarget in
  +      if lid_equals src tgt
  +      then raise_error (Errors.Fatal_Effects_Ordering_Coherence,
  +             BU.format3 "Adding an edge %s~>%s induces a cycle %s"
  +               (Ident.string_of_lid edge.msource)
  +               (Ident.string_of_lid edge.mtarget)
  +               (Ident.string_of_lid src)) env.range;
  +      if find_edge env.effects.order (src, tgt) |> is_some
  +      then begin
  +        //AR: 07/09: TODO: enable this warning
  +        // log_issue env.range (Errors.Warning_BleedingEdge_Feature,
  +        //   BU.format4 "Adding an edge %s~>%s adds a second path for %s~>%s, ignoring this second path"
  +        //      (Ident.string_of_lid edge.msource)
  +        //      (Ident.string_of_lid edge.mtarget)
  +        //      (Ident.string_of_lid src)
  +        //      (Ident.string_of_lid tgt));
  +        edges
  +      end
  +      else if exists_polymonadic_subcomp env src tgt |> is_some ||
  +              exists_polymonadic_subcomp env tgt src |> is_some then
  +        raise_error (Errors.Fatal_Effects_Ordering_Coherence, BU.format4
  +          "Adding an edge %s~>%s induces an edge %s~>%s that conflicts with an existing polymonadic subcomp between them"
  +          (Ident.string_of_lid edge.msource)
  +          (Ident.string_of_lid edge.mtarget)
  +          (Ident.string_of_lid src)
  +          (Ident.string_of_lid tgt)) env.range
  +      else (compose_edges (compose_edges i_src edge) tgt_j)::edges) edges all_tgt_j) [] all_i_src in
  +  
  +
  +  let order = new_edges@env.effects.order in
  +  // let order = BU.remove_dups (fun e1 e2 -> lid_equals e1.msource e2.msource
  +  //                                    && lid_equals e1.mtarget e2.mtarget) order in
  +
  +  //   (* basically, this is Warshall's algorithm for transitive closure,
  +  //      except it's ineffcient because find_edge is doing a linear scan.
  +  //      and it's not incremental.
  +  //      Could be made better. But these are really small graphs (~ 4-8 vertices) ... so not worth it *)
  +  // let order =
  +  //   let fold_fun order k =
  +  //     order@(ms |> List.collect (fun i ->
  +  //               if lid_equals i k then []
  +  //               else ms |> List.collect (fun j ->
  +  //                 if lid_equals j k
  +  //                 then []
  +  //                 else match find_edge order (i, k), find_edge order (k, j) with
  +  //                      | Some e1, Some e2 -> [compose_edges e1 e2]
  +  //                      | _ -> [])))
  +  //   in ms |> List.fold_left fold_fun order
  +  // in
  +
     let _ = order |> List.iter (fun edge ->
       if Ident.lid_equals edge.msource Const.effect_DIV_lid
       && lookup_effect_quals env edge.mtarget |> List.contains TotalEffect
       then raise_error (Errors.Fatal_DivergentComputationCannotBeIncludedInTotal, (BU.format1 "Divergent computations cannot be included in an effect %s marked 'total'" (string_of_lid edge.mtarget))) (get_range env))
     in
  +
  +  //compute upper bounds now
     let joins =
       ms |> List.collect (fun i ->
       ms |> List.collect (fun j ->
  -    let join_opt =
  +    let k_opt =
         if Ident.lid_equals i j then Some (i, id_edge i, id_edge i)
         else
           ms |> List.fold_left (fun bopt k ->
  
positive.code:             end
            | _ -> bopt) None
      in
      match join_opt with
      | None -> []
      | Some (k, e1, e2) ->
        if exists_polymonadic_bind env i j |> is_some
        then raise_error (Errors.Fatal_PolymonadicBind_conflict,
               BU.format4 "Updating effect lattice with a lift between %s and %s \
                 induces a path from %s and %s in the effect lattice, and this \
                 conflicts with a polymonadic bind between them"
                 (Ident.string_of_lid src) (Ident.string_of_lid tgt)
                 (Ident.string_of_lid i) (Ident.string_of_lid j)) env.range
        else [(i, j, k, e1.mlift, e2.mlift)]))
    in
  
  
negative.code:       (if poly then "polymonadic subcomp"
         else "path in the effect lattice") in
  
    if exists_polymonadic_subcomp env m n |> is_some ||
       exists_polymonadic_subcomp env n m |> is_some
    then raise_error (Errors.Fatal_Effects_Ordering_Coherence, (err_msg true)) env.range
    else if monad_leq env m n |> is_some ||
            monad_leq env n m |> is_some
    then raise_error (Errors.Fatal_Effects_Ordering_Coherence, (err_msg false)) env.range
    else { env with
           effects = ({ env.effects with
                        polymonadic_subcomps = (m, n, ts)::env.effects.polymonadic_subcomps }) }
  