anchor.diff:              end
             | _ -> bopt) None
       in
  -    match join_opt with
  +    match k_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 \
  +      (*
  +       * 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)) env.range
  +               (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
   
  
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:   env
  
  let push_new_effect env (ed, quals) =
    let effects = {env.effects with decls=env.effects.decls@[(ed, quals)]} in
    {env with effects=effects}
  
  let exists_polymonadic_bind env m n =
  