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:        else "path in the effect lattice") in
  
    if exists_polymonadic_bind 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
         && not (lid_equals m n)
    then raise_error (Errors.Fatal_PolymonadicBind_conflict, (err_msg false)) env.range
    else { env with
           effects = ({ env.effects with polymonadic_binds = (m, n, p, ty)::env.effects.polymonadic_binds }) }
  
  
negative.code:             end
            | _ -> bopt) None
      in
      match k_opt with
      | None -> []
      | Some (k, e1, e2) ->
        (*
         * AR: we computed k as the least upper bound of i and j
         *     if there exists polymonadic binds i, j or j, i
         *     then there are multiple ways to bind i, j or j, i computations now
         *     so error out
         *)
        if exists_polymonadic_bind env i j |> is_some ||
           exists_polymonadic_bind env j i |> is_some
        then raise_error (Errors.Fatal_Effects_Ordering_Coherence,
               BU.format5 "Updating effect lattice with a lift between %s and %s \
                 induces a least upper bound %s of %s and %s, 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) (Ident.string_of_lid k)) env.range
        else let j_opt = join_opt env i j in
             if j_opt |> is_some && not (lid_equals k (j_opt |> must |> (fun (l, _, _) -> l)))
             then raise_error (Errors.Fatal_Effects_Ordering_Coherence, BU.format6
               "Updating effect lattice with %s ~> %s makes the least upper bound of \
               %s and %s as %s, whereas earlier it was %s"
               (Ident.string_of_lid src) (Ident.string_of_lid tgt)
               (Ident.string_of_lid i) (Ident.string_of_lid j)
               (Ident.string_of_lid k)
               (j_opt |> must |> (fun (l, _, _) -> l) |>  Ident.string_of_lid)) env.range
        else [(i, j, k, e1.mlift, e2.mlift)]))
    in
  
  