Hello Tomasz, Unfortunatelly I have only seen your message after Simon answered to it. I am sorry for the late answer!
| If there is another way to do this right now (conveniently, Oleg! ;-), I | would be more than happy to hear about it. | | If this worked, it would be a cool trick and a nice example for GADT | use. Let me know if it was proposed before.
Well, it is true that GADTs and type classes functional depencies do not work well, but there is no problem if you only use type classes. The first alternative would be using a multiple parameter type classes with functional dependencies. This would be something that Oleg would be likely to propose you. But I think you do not want this :) A second alternative would be to simulate your GADT with a type class and your constructors with the functions of that type class:
class Term g where lit :: F f Int int => Int -> g f int suc :: F f Int int => g f int -> g f int isZero :: (F f Int int, F f Bool bool) => g f int -> g f bool iff :: (F f Bool bool, F f a a') => g f bool -> g f a' -> g f a' -> g f a'
As a remark, this is a church encoding of the GADT. Your examples:
ex1 :: Term g => g Untyped () ex1 = iff (isZero (suc (lit 0))) (lit 1) (lit 2)
| the same as ex1, but Typed
ex1' :: Term g => g Typed Int ex1' = iff (isZero (suc (lit 0))) (lit 1) (lit 2)
| a term that has type bug, but will be accepted as Untyped
ex2 :: Term g => g Untyped () ex2 = iff (isZero (suc (lit 0))) (lit 1) (isZero (lit 2))
Now you can encode functions on the GADT as instances of this type class:
newtype Untype g b a = Untype {untype :: g Untyped ()}
instance Term g => Term (Untype g) where lit x = Untype (lit x) suc t = Untype (suc (untype t)) isZero t = Untype (isZero (untype t)) iff c t e = Untype (iff (untype c) (untype t) (untype e))
This should suffice for encoding your untype. Although this might look like a bit puzzling at first glance, the translation of the GADT code into the type class version (and vice versa) is quite straighforward and mechanical. The advantages of this encoding in relation to GADTs are that: 1) It does not have the GADTs <-> fundeps problem; 2) It does not require any heavy machinary from the compiler (if it would not be for your F class, it would be Haskell 98). The main disadvantage is that in some functions that you can define with GADT might not be easily definable with this encoding. I must say that, from my experience, that functions of this kind do not occur often. Until GHC fixes the problem of the interaction between fundeps and GADTs, you might want to consider using this. All code you develop with this encoding can be very easily translated to GADT form once the problem is solved. If you want further references to this technique check this: http://www.mail-archive.com/haskell-cafe@haskell.org/msg10047.html The original thread by Conor is: http://www.mail-archive.com/haskell-cafe@haskell.org/msg10033.html The discussion that derived from this thread is quite interesting. Cheers, Bruno