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.
I _just_ read that. Let's see how I do:
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.
I will go out on a limb and guess that GHC accepts your uses of the instances below for reasons similar to the fact that GHC sometimes accepts overlapping instances. GHC only lazily reports an overlapping instances error when it detect concrete usage of the instances that fall into the overlapping "zone". Note that Hugs checks eagerly. (I ran into this difference in the older version of regex-base's RegexContext instances. GHC was okay but Hugs complained). My guess is that: if every time GHC sees a == () you also always use the same type 't' then GHC might not complain about it. If you _actually_ fool GHC then you should file a bug.
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.
I'm starting to this this is an example of using functional dependencies that has no translation to type families. Can anyone free me of such thoughts?
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
I have never used associated types or type families. I assume you cannot rely
on GHC lazy goodwill for the a->t constraint. You will have to be explicit.
Not using associated types but type families I think the syntax should be:
-- No obvious need for kind annotations, so this is
type family A_T a
type family A_B_C a b
type family A_C_B a c
-- The name are
-- You need to help GHC more here:
type instance A_T () =