Thanks for this interesting example. Just le me say up front that I regard any FD program that you cannot translate to type families as a bug in the TF implementation. To qualify this a little, this is definitely so for programs that do not require undecidable instances. With undecidable instances, it is anybodys guess what the actual semantics of the FD program is, so trying to approximate that unknown behaviour with an TF program is necessarily partly guesswork, or a matter of reading GHC source code. Chris Smith wrote,
The following code builds and appears to work great (assuming one allows undecidable instances). I have tried both a natural translation into type synonym families, and also the mechanical transformation in http://www.cse.unsw.edu.au/~chak/papers/tyfuns.pdf -- but I can't get either to work.
The two fishy things are:
1. There is a functional dependency (a -> t) in the original. Actually, this isn't always true since t is sometimes not uniquely determined by a; but GHC always seems to do the right thing anyway. There doesn't seem to be any way to "cheat" like this with type families.
From your example code, it is entirely unclear why you need the (a -> t) dependence at all. You only provided the class and instances declarations, and those (not surprisingly) compile fine without that dependency. Can you give an example that does not work if we leave that dependency out?
2. In the second and fourth instances, the type variable x appears twice in the parameters of the type function built from the fundep (a b -> c). This causes an error. If I try adding (x ~ x') to the context and making one of them x' instead of x, I get different errors.
Currently, the TF implementation requires type instances to be left-linear (ie, no repeated type variables in the head). I actually think we can lift that restriction, but for the time being adding an equality to the context is a sensible work around. Leaving out the (a -> t) dependency (whose purpose I don't understand) and using equalities to circumvent the restriction to left-linear heads, the program translates to data Var a = Var Int (Maybe String) data RHS a b = RHS a b class (C a b ~ c, B a c ~ b) => Action t a b c where type C a b type B a c instance Action t () y y where type C () y = y type B () y = y instance (x ~ x') => Action t (Var x) (x' -> y) y where type C (Var x) (x' -> y) = y type B (Var x) y = x -> y instance Action t [t] y y where type C [t] y = y type B [t] y = y instance (Action t a b c, x ~ x') => Action t (RHS (Var x) a) (x' -> b) c where type C (RHS (Var x) a) (x' -> b) = C a b type B (RHS (Var x) a) c = x -> B a c instance (Action t a b c) => Action t (RHS [t] a) b c where type C (RHS [t] a) b = C a b type B (RHS [t] a) c = B a c This program is currently also rejected due to a bug in the treatment of equalities in superclass constraints. We already tripped over that in the context of another program, and I believe Tom Schrijvers is currently working at fixing it. A nice aspect of the above TF version of this code is that (if I am not mistaken) it does *not* require undecidable instances. Manuel
Code with fundeps is:
data Var a = Var Int (Maybe String) data RHS a b = RHS a b
class Action t a b c | a -> t, a b -> c, a c -> b instance Action t () y y instance Action t (Var x) (x -> y) y instance Action t [t] y y instance (Action t a b c) => Action t (RHS (Var x) a) (x -> b) c instance (Action t a b c) => Action t (RHS [t] a) b c