[Haskell-cafe] how to nicely implement phantom type coersion?

[David Roundy]

Hello all,

I've been working on a sort of static consistency-checking framework for
darcs patches using GADTs and phantom existential types, and am looking for
a bit of advice on whether I might be able to create a class to avoid some
tedious coding overhead.

The basic idea is that a patch will have type (Patch a b) where "a" and "b"
are phantom types.  Sequential patches will have identical ending and
beginning types.  So that a sequential pair, for example, can be written as

data Sequential a c where
    Sequential :: Patch a b -> Patch b c -> Sequential a c

The trickiness is that we need to be able to check for equality of two
patches, and if they are truly equal, then we know that their ending states
are also equal.  We do this with a couple of operators:

    (=\/=) :: Patch a b -> Patch a c -> Maybe (EqContext b c)
    (=/\=) :: Patch a z -> Patch b z -> Maybe (EqContext a b)

data EqContext a b =
    EqContext { coerce_start :: Patch a z -> Patch b z,
                coerce_end :: Patch z a -> Patch z b,
                backwards_coerce_start :: Patch b z -> Patch a z,
                backwards_coerce_end :: Patch z b -> Patch z a
              }

where we use the EqContext to encapsulate unsafeCoerce so that it can only
be used safely.  The problem is that it's tedious figuring out whether to
use coerce_start or coerce_end, or backwards_coerce_end, etc.  Of course,
the huge advantage is that you can't use these functions to write buggy
code (at least in the sense of breaking the static enforcement of patch
ordering).

So I'm wondering if there might be some sort of multi-parameter class one
could define that would ease the use of an EqContext.  For example I can
imagine a (somewhat lame) class

class EqTypes a b where
   safe_coerce_end :: Patch x a -> Patch x b
   safe_coerce_start :: Patch x a -> Patch x b
   safe_coerce_start = invert $ safe_coerce_end $ invert p

(note that invert :: Patch a b -> Patch b a)

then we could perhaps write some template haskell to define a couple of
instances of EqTypes from a data type EqContext... except that I suspect
that this is isn't possible, since the EqContext only exists at runtime, so
unless one could define classes dynamically at runtime I'm out of luck.

So is there some other approach that I can use for easily coercing phantom
types based on runtime checks? Any suggestions?

What I'd really love would be to be able to create a function that is
polymorphic in kind rather than in type such as (inventing a rather poor
syntax off the top of my head):

data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }

where f(a,b) is a function of two types that returns a type, so the value
of f(a,b) might be (Patch a b) or (Patch x b) or something like that.

But I'm not sure if this is possible in Haskell, and if it is, then it
definitely requires some sort of tricky extension that I'm not familiar
with...
-- 
David Roundy
http://www.darcs.net