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