problem with type equality constraints

Hi, 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? Cheers, Ganesh

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

On Mon, 17 Mar 2008, Manuel M T Chakravarty wrote:
Your are completely right. Unfortunately, superclass equalities (ie, the Id a ~ ida in the class declaration of Foo) aren't fully implemented yet.
OK, thanks. Is there any rough idea of when they will be?
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.
Even with the rough edges, type families are really nice, thanks! Cheers, Ganesh

Ganesh Sittampalam:
On Mon, 17 Mar 2008, Manuel M T Chakravarty wrote:
Your are completely right. Unfortunately, superclass equalities (ie, the Id a ~ ida in the class declaration of Foo) aren't fully implemented yet.
OK, thanks. Is there any rough idea of when they will be?
That's a bit difficult to say. The main problem is that the current handling of evidence for classes and access to superclass evidence doesn't mix well with the fact that the evidence for equalities are coercions (ie, type-level things, rather than value level things). It's high up on the list, but some other things like the interaction between GADTs and type families (basically done now) were higher up. If its important to you, I'd try to get to it earlier than if nobody is really waiting for it. Manuel

On Tue, 18 Mar 2008, Manuel M T Chakravarty wrote:
Ganesh Sittampalam:
On Mon, 17 Mar 2008, Manuel M T Chakravarty wrote:
Your are completely right. Unfortunately, superclass equalities (ie, the Id a ~ ida in the class declaration of Foo) aren't fully implemented yet.
OK, thanks. Is there any rough idea of when they will be?
It's high up on the list, but some other things like the interaction between GADTs and type families (basically done now) were higher up. If its important to you, I'd try to get to it earlier than if nobody is really waiting for it.
Well, I am waiting for it, but I'm not exactly desperate. There are also other things restricting me from a wholesale conversion from fundeps which I'll write up into questions on here over the next few days. Cheers, Ganesh
participants (2)
-
Ganesh Sittampalam
-
Manuel M T Chakravarty