[Haskell-cafe] Assorted AT fun and games

[Andrew Coppin]

It all began with

  class (Vector (Point x)) => HasSpace x where
    type Point x :: *

So far, so good.

I was rather surprised that you _can_ write

  class (Complete (Completed x)) => Incomplete x where
    type Completed x :: *
    complete :: x -> Completed x

I was almost as surprised to discover that you _cannot_ write

  class (HasSpace x, Complete (Completed x), HasSpace (Completed x), 
Point x ~ Point (Completed x)) => Incomplete where...

It just means that every time you write an Incomplete instance, you 
might have to add the Point constraint manually. Which is mildly irritating.

More worrying, adding Point foo ~ Point bar to an instance declaration 
causes GHC to demand that you turn on Undecidable Instances, for reasons 
beyond my comprehension.

It's also interesting that when you write a class instance that has some 
constraint on it, and then you try to write a subclass instance, you 
still have to repeat the exact same constraint, even though the 
superclass instance declaration implies it. The only reason I can think 
of is that theoretically somebody could add a new superclass instance 
without the constraint. (Wouldn't that be an overlapping instance though?)

And now things get *really* interesting. Consider this:

  data Foo x = Foo !x !(Point x)

Surprisingly, GHC accepts this. This despite the rather obvious fact 
that "Point x" can exist if and only if "x" has a HasSpace instance. And 
yet, the type definition appears to say that "x" is simply an 
unconstrained type variable. Intriguing...

Next, you can't derive Eq or Show for this type, but you *can* declare 
them manually:

  instance (Show x, Show (Point x)) => Show (Foo x) where
    show (Foo x px) = "Foo (" ++ show x ++ ") (" ++ show px ++ ")"

Again, no hint of the fact that this will only work if we have HasSpace 
x. And yet GHC happily accepts this.

I'm starting to think maybe I'm pushing the type system further than it 
can cope, and I should just completely redesign the whole thing...