[Haskell-cafe] problem with type equality constraints

[Manuel M T Chakravarty]

Ganesh Sittampalam:
> When I try to compile this code with ghc-6.9.20080310:
>
> module Test2 where
>
> type family Id a
> type instance Id Int = Int
> type instance Id (a, b) = (Id a, Id b)
>
> class Id a ~ ida => Foo a ida
>
> instance Foo Int Int
> instance (Foo a ida, Foo b idb) => Foo (a, b) (ida, idb)
>
> I get these errors:
>
> Test2.hs:12:0:
>    Couldn't match expected type `ida' against inferred type `Id a'
>      `ida' is a rigid type variable bound by
>            the instance declaration at Test2.hs:12:16
>    When checking the super-classes of an instance declaration
>    In the instance declaration for `Foo (a, b) (ida, idb)'
>
> Test2.hs:12:0:
>    Couldn't match expected type `idb' against inferred type `Id b'
>      `idb' is a rigid type variable bound by
>            the instance declaration at Test2.hs:12:27
>    When checking the super-classes of an instance declaration
>    In the instance declaration for `Foo (a, b) (ida, idb)'
>
> It seems to me that since Foo a ida and Foo b idb are superclassess,  
> Id a ~ ida and Id b ~ idb should be known and so this should have  
> worked - am I missing something?

Your are completely right.  Unfortunately, superclass equalities (ie,  
the Id a ~ ida in the class declaration of Foo) aren't fully  
implemented yet.  If I am not mistaken, superclass equalities, class  
defaults for associated type families, and GADT data instances are the  
three major features of type families/equality constraint saga that  
aren't fully implemented yet.

Manuel