[Apologies for the slightly long setup. The guts of the question is: can one use the class system to code up the reflexive, transitive closure of a set of dynamic (but contextually implied) coercions? I'm coming to the conclusion that the answer is no, but I'm interested in a good explaination of why things don't work out.] Imagine an extension of the ST monad that gives nested scope [1]; that is, I add the following: blockST :: (forall s2. ST (s1, s2) a) -> ST s1 a liftST :: ST s1 a -> ST (s1, s2) a The first encapsulates the nested scope much as runST encapsulates the entire computation; the second imports computations from the outer scope to the inner scope. Now suppose I want to write a function that pairs the contents of two references into a new reference; furthermore, the function should be polymorphic in the scope of each of the input references, the output reference, and the final computation. That is, I'd like the type to be: pair :: STRef s1 a -> STRef s2 b -> ST s4 (STRef s3 (a, b)) The simplest definition clearly doesn't have enough polymorphism. If I write: pair v w = do a <- readSTRef v b <- readSTRef w newSTRef (v, w) then the function has the type: pair :: STRef s a -> STRef s b -> ST s (STRef s (a, b)) Now, there is no way to write pair with liftST terms that will result in sufficient polymorphism over scopes. For example, if I write: pair v w = do a <- readSTRef v b <- liftST (readSTRef w) liftST (liftST (newSTRef (v, w))) then the function has the type: pair :: STRef ((s1, s2), s3) a -> STRef (s1, s2) b -> ST (((s1, s2), s3), s4) (STRefr1 (a, b)) which isn't as general as I would like, as it imposes a particular order on the nested scopes. The only requirement is that scopes of the input refs and the output refs are nested inside the scope of the resulting computation. I can abstract the liftST applications and pass evidence that witnesses the correct scope nesting: pair :: (ST s1 a -> ST s4 a) -> (ST s2 a -> ST s4 b) -> (ST s3 (STRef s3 (a, b)) -> ST s4 (STRef s3 (a, b))) -> STRef s1 a -> STRef s2 b -> ST s4 (STRef s3 (a, b) pair lift1 lift2 lift3 v w = do a <- lift1 (readSTRef v) b <- lift2 (readSTRef w) lift3 (newSTRef (v, w)) Since evidence is really assembled from liftST terms, it is parametric in the return type. So, it make sense to give pair the more general type: pair :: (forall c. ST s1 c -> ST s4 c) -> (forall c. ST s2 c -> ST s4 c) -> (forall c. ST s3 c -> ST s3 c) -> STRef s1 a -> STRef s2 b -> ST s4 (STRef s3 (a, b)) Now, for the most part, it is obvious how to construct this evidence. My driving question is whether or not there is a way of moving it to the class system. That is, can some variation of the following be made to work: class AutoLiftST s1 s2 where autoLiftST :: ST s1 a -> ST s2 b instance AutoLiftST s1 (s1, s2) where autoLiftST = liftST pair :: (AutoLiftST s1 s4) -> (AutoLiftST s2 s4) -> (AutoLiftST s3 s4) -> STRef s1 a -> STRef s2 b -> ST s4 (STRef s3 (a, b)) pair v w = do a <- autoLiftST (readSTRef v) b <- autoLiftST (readSTRef w) autoLiftST (newSTRef (v, w)) where I could then write: test :: ST s0 (STRef s0 (Integer, Integer)) test = blockST (do v <- newSTRef 1 blockST (do w <- newSTRef 2 blockST (gpair v w))) and have the appropriate instances be derived/inferred. Note that this is basically boils down to choosing the appropriate elements from the reflexive, transitive closure of the liftST's implied by each blockST. Clearly, blindly throwing in reflexive and transitive instances of AutoLiftST leads to overlapping and undecidable instances. (OTOH, if one anticipates that blockST and liftST are operationally identity functions, then all of the instances of autoLiftST correspond to identity functions, and it doesn't matter which instance is chosen.) I've experimented with a few different attempts, but in the best case succeeded only in exhausting stack space while searching for satisfying instances. My gut feeling is that the search space is just too unconstrained; I'd be just as happy to hear a good explaination of exactly _what_ aspect of the problem makes it difficult, if not impossible. Finally, note that the type of liftST and the tuple type are just one way of connecting the inner and outer scopes. I'd actually prefer to dispense with liftST and make the evidence part of blockST. In explicit evidence style: blockST :: (forall s2. (forall b. ST s1 b -> ST s2 b) -> ST s2 a) -> ST s1 a while in the implicit evidence style: blockST :: (forall s2. AutoLiftST s1 s2 => ST s2 a) -> ST s1 a Now the atomic coercions are all implicitly introduced in the body of a blockST by the AutoLiftST s1 s2 class constraint. This leads to the interesting situation where _all_ AutoLiftST instances are of variables. On the other hand, it seem clear that within a nesting of blockST, we accumulate the constraints (AutoLiftST s1 s2, AutoLiftST s2 s3, ..., AutoLiftST sn-1 sn) and it is "obvious" how to compose AutoLiftST si sj for i <= j. [1] John Launchbury and Amr Sabry. Monadic State: Axiomatization and Type Safety. ICFP'97.