@owickstrom I was going to add these, but I think there's some things to play with here, since you might not want to directly promote i and o while lifting, and instead re-map them to some composite index. Meaning we might need a definition more like this:
class IxMonadTrans t i o j p | i -> j, o -> p where
ilift ∷ forall m a. IxMonad m ⇒ m i o a → t m j p a
But I also need to get back to work, so will have to experiment more later :smile:
@owickstrom I was going to add these, but I think there's some things to play with here, since you might not want to directly promote
i
ando
while lifting, and instead re-map them to some composite index. Meaning we might need a definition more like this:But I also need to get back to work, so will have to experiment more later :smile: