anchor.diff:        (if poly then "polymonadic subcomp"
          else "path in the effect lattice") in
   
  -  if exists_polymonadic_subcomp env m n |> is_some
  -  then raise_error (Errors.Fatal_PolymonadicBind_conflict, (err_msg true)) env.range
  -  else if join_opt env m n |> is_some
  -  then raise_error (Errors.Fatal_PolymonadicBind_conflict, (err_msg false)) env.range
  +  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 }) }
  
positive.code:   //     (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 _ = 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
    let joins =
      ms |> List.collect (fun i ->
      ms |> List.collect (fun j ->
      let join_opt =
        if Ident.lid_equals i j then Some (i, id_edge i, id_edge i)
        else
          ms |> List.fold_left (fun bopt k ->
  
negative.code:        else "path in the effect lattice") in
  
    if exists_polymonadic_bind env m n |> is_some
    then raise_error (Errors.Fatal_Effects_Ordering_Coherence, (err_msg true)) env.range
    else if join_opt env m n |> is_some
         && not (lid_equals m n)  //AR: 07/09: TODO: this is a problem when m = n, we allow defining a polymonadic bind between m and m, but a bind between them already exists, so some code may use bind, some then mauy use the polymonadic bind
    then raise_error (Errors.Fatal_Effects_Ordering_Coherence, (err_msg false)) env.range
    else { env with
           effects = ({ env.effects with polymonadic_binds = (m, n, p, ty)::env.effects.polymonadic_binds }) }
  
  