[Haskell-cafe] checking types with type families

[Simon Peyton-Jones]

|  Here's a concrete case I recently ran into:
|  
|  type family SomeOtherTypeFamily a
|  class SomeClass a where type SomeType a
|  instance a ~ SomeOtherTypeFamily b => SomeClass a where 
|    type SomeType a = (b,Int)  
|        --  (error) Not in scope: type variable `b'
|  
|  The same thing with fundeps:
|  
|  class SomeClass a b | a -> b
|  instance a ~ SomeOtherTypeFamily b => SomeClass a (b,Int) 
|      -- works fine

It's not the same thing at all!  The code you give certainly should fail.

Suppose you use fundeps thus:
   class C a b | a->b where
     op :: a -> b -> b

The idiomatic way to replace this with type functions is to remove the 'b' parameter, thus:
   class C a where
     type B a 
     op :: a -> B a -> B a

Sometimes you don't want to do this.  For example, you might have a bidirectional fundep.  Then you can (or rather will be able to) use a superclass thus:
   class (B a ~ b) => C a b where
      type B a

The superclass says that you can only instantiate this class with a second argument b that is equal to (B a).  Thus you might have an instance
   instance C Int Bool where
     type B Int = Bool

Meanwhile we are working hard on the new type inference engine, which will allow superclass equalities like these.

Simon