Hello, Since you're already using GADTs, why not also use them to witness type equality: import GHC.Exts data Patch a b = Patch Int Int data Sequential a c where Sequential :: Patch a b -> Patch b c -> Sequential a c data MaybeEq :: * -> * -> * where NotEq :: MaybeEq a b IsEq :: MaybeEq a a (=//=) :: Patch a b -> Patch c d -> MaybeEq b c Patch _ x =//= Patch y _ | x == y = unsafeCoerce# IsEq | otherwise = NotEq sequenceIfPossible :: Patch a b -> Patch c d -> Maybe (Sequential a d) sequenceIfPossible p q | IsEq <- p =//= q = Just $ Sequential p q | otherwise = Nothing Notice the usefulness of pattern guards. EqContext could be defined as data EqContext :: * -> * -> * where EqWitness :: EqContext a a (though I ususally prefer to just call both the data type and the constructor 'E'.) Thomas On Thu, 2005-12-08 at 09:23 -0500, David Roundy wrote:
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).