[Haskell] closure of coercions with classes

[Matthew Fluet]

[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.