[Haskell-cafe] Fast times at Inferable-but-not-Checkable High.

[Joe Fredette]

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