So, I've been fiddling with an utterly random idea. What if I had a class: class Hom a b where data Rep a b hm :: Rep a b -> b im :: a -> Rep a b That is, all types that have some conversion between them (an isomorphism originally, then I thought homomorphism, now I'm not sure what the hell I'm talking about, so I've just stuck with Hom...) which preserves some sense of "structure" and "content", for instance data CouldBe a = Only a | Nada is _obviously_ the same type as `Maybe`. However, it can't be used transparently where `Maybe` can be used. That is, shouldn't I be able to define a 1-1, onto function `phi :: CouldBe a -> Maybe a` and as such another `pho :: Maybe a -> CouldBe a` such that phi . pho = pho . phi = phum ... errr. `id`? Hom a b represents one end of that (specifically `hm . im = phi`, and `hm . im` for the instance `Hom b a` would `pho`), then I could, instead of writing a type which expects maybe, simply expects anything _equivalent_ to a maybe, eg safeHead :: Hom (Maybe a) b => [c] -> Rep a (Maybe c) safeHead [] = im Nothing safeHead (x:_) = im (Just x) Though- I think this is a little bit off in terms of how it should work, perhaps this is my problem, but the idea is that instead of returning a Maybe, it returns something which can be converted _from_ a maybe. That is, a "generic" type like: data X1 a = X a | Y which is the "form" of any "maybe-like" type. In one sense, I'm almost trying to be polymorphic over the constructors of a given type, kindof, sortof, if you squint your eyes just right and try not to think too much. My problem comes when I try to do this: hom = hm . im eq x y = hom x == hom y Which, I reason, ought to satisfy the type: eq :: (Hom a b, Eq b) => a -> a -> Bool this assumes that hom defines a equality-preserving conversion. However, the type it infers is: eq :: (Hom a b, Hom a1 b, Eq b) => a -> a1 -> Bool Now, this makes sense, all my signature is is a special case of this type. Interesting consequence, this eq could compare a `Maybe a` and `CouldBe a` in a sensical way. Which is a nice benefit. However, here's where it gets weird, If I try to _provide_ this signature (the second, more general one, or the first, specific one, it doesn't matter), GHC gives me the following error: Iso.hs:29:10: Could not deduce (Hom a b) from the context (Hom a b1, Eq b1) arising from a use of `hom' at Iso.hs:29:10-14 Possible fix: add (Hom a b) to the context of the type signature for `eq' In the first argument of `(==)', namely `(hom x)' In the expression: (hom x) == (hom y) In the definition of `eq': eq x y = (hom x) == (hom y) Failed, modules loaded: none. for the latter and a similar one (but for each of the `Hom a b`, `Hom a1 b` cases. Punchline is this, I'm trying to write a generic equality that works for any two types with the same constructor-structure, when I try to write said function, GHC can infer but not Check (it seems, I'm not sure if that's the correct lingo) the type... My question is twofold. 1. Is this whole idea even possible? I mean- is there some limitation I'm going to run into, I have run into problems when trying to do: instance (Hom a b, Eq b) => Eq a where blah wrt UndecideableInstances. But it seems so _obvious_ what that means, I don't think I fully understand what's going on -- that is, whether I'm misunderstanding how class contexts work here, and why this (seemingly obvious) signature is undecidable, or whether I'm just mistaken in my type signature all together. (My goal is to say that anything which can be converted freely to and from something that is an instance of the Eq class, must preserve the equality relationships. 2. Why is GHC unable to check the types, but infer them. I always understood inferring to be the "hard" part of the problem, and checking to be the "easy" part. Is my intuition wrong? I've posted the code here[1] for your perusal. It's not particularly important that I get this solved, it's just a random idea I wanted to explore and thought the notion might appeal to some other Haskeller's around there who like to have self-documenting datatypes, but hate having to rewrite lots of simple utility functions as penance for our documentarian sins. /Joe