writing functions in haskell that work on associated types only

Question

I'm trying to find a more elegant way to write the following code.

class C c where
    type E c :: * -> *

class C c => A c where
    g :: E c a -> E c a

class (C c, A c) => D c where
    f :: E c a -> E c a

instance A c => D c where
    f = g

This produces an error.

Test.hs:58:9:
    Could not deduce (E c0 ~ E c)
    from the context (A c)
      bound by the instance declaration at Test.hs:57:10-19
    NB: `E' is a type function, and may not be injective
    Expected type: E c a
      Actual type: E c0 a
    Expected type: E c a -> E c a
      Actual type: E c0 a -> E c0 a
    In the expression: g
    In an equation for `f': f = g
Failed, modules loaded: none.

My current solution is to add a dummy variable, from which it can derive which particular C is in use.

class C c where
    type E c :: * -> *

class C c => A c where
    g_inner :: c -> E c a -> E c a
g = g_inner undefined

class (C c, A c) => D c where
    f_inner :: c -> E c a -> E c a
f = f_inner undefined

instance A c => D c where
    f_inner = g_inner

I know this is another instance of associated types not being injective, but I can't quite figure it out. Sure, E might not be injective, but it seems somewhere the information that g will work on the particular (E c) referenced in class D has been lost.

Any explanation, and more importantly better workarounds would be much appreciated. Thanks!

edit

Okay, I see switching type to data makes the code work.

I'm trying to sound out how this might work. Each c creates a new data type E c. In the instance context, we have to match forall a. ((E) c) a -> ((E) c) a with forall a. ((E) c) a -> ((E) c) a. Denoting F = E c, we are then matching forall a. F a -> F a with itself.

I'm having trouble seeing where things break with the type synonyms (associated types) case. Sure, one could define two instances of A which both have signature (E c) a -> (E c) a. But, why would it be wrong to use the definition from the instance A c which is in scope?

Thanks!!

Answer 1

The problem is that, from just E c a -> E c a, the compiler doesn't know which instance C to choose.

Associated type families are just type synonyms. So the class

class C c => A c where
    g :: E c a -> E c a

from the typechecker's perspective may as well be

class C c => A c where
    g :: m a -> m a

As the class variable c isn't mentioned, there's no way to determine which instance dictionary should be used to select the function. Although this is because type families aren't injective, I agree that it isn't obvious from the error message that this is the problem.

Using a data family as Daniel Wagner suggests may be the most elegant solution. I've sometimes been able to invert my type families, so that instead of getting an E c for a particular c, I instead choose c based on E c. In this case, that would give:

class E (e :: * -> *) where
    type C e :: *

class E e => A e where
    g :: e a -> e a

class (A e) => D e where
    f :: e a -> e a

instance A e => D e where
    f = g

Depending on what else you're doing, this may work for you.

This problem aside, having a separate instance doesn't make much sense. Since A is available as a super class constraint, you can just set f = g as a default method. Doing so will be much less trouble; you probably don't actually want an instance D e where ....