Confluence? Oh, you mean a distributive law between Promonads! https://elk.zone/types.pl/@totbwf/110712999795376253

Confluence.hs

{-# LANGUAGE RankNTypes, GADTs, TypeOperators #-}
import Data.Profunctor

data Exists2 f g where
  Exists2 :: f x -> g x -> Exists2 f g

data Confluence p = Confluence (forall a b c. (p a b, p a c) -> Exists2 (p b) (p c))

newtype Op p a b = Op { runOp :: p b a }

type p ~~> q = forall a b. p a b -> q a b

data Procompose p q b c where
  Procompose :: p x c -> q b x -> Procompose p q b c

type Dist p q = Procompose p q ~~> Procompose q p

dist :: Confluence p -> Dist p (Op p)
dist (Confluence c) (Procompose pac (Op pab)) = case c (pab, pac) of Exists2 pbd pcd -> Procompose (Op pcd) pbd

conf :: Dist p (Op p) -> Confluence p
conf dist = Confluence (\(pab, pac) -> case dist (Procompose pab (Op pac)) of Procompose (Op pbd) pcd -> Exists2 pbd pcd)