Haskell type family error

Question

Sorry to bother you with this simple problem. I'm trying to learn how the type family extension works. When I fool around with it I encountered an error I couldn't figure out why.

class Foo a b c where
    data T a b c :: *

    f :: a -> T a b c

    g :: T a b c -> b

    h :: c -> a -> b
    h c a = g $ f a

Error message:

    Could not deduce (Foo a b c0) arising from a use of ‘g’
from the context (Foo a b c)
  bound by the class declaration for ‘Foo’
  at DB/Internal/Typecast.hs:(17,1)-(25,19)
The type variable ‘c0’ is ambiguous
Relevant bindings include
  a :: a (bound at DB/Internal/Typecast.hs:25:9)
  h :: c -> a -> b (bound at DB/Internal/Typecast.hs:25:5)
In the expression: g
In the expression: g $ f a
In an equation for ‘h’: h c a = g $ f a

I don't understand how is c ambiguous in T a b c for g. Can't the compiler get the type of c from the T a b c of f?

I just want the composite of g . f

Answer 1

Note that in the definition

h :: c -> a -> b
h c a = g $ f a

there is no restriction that f and g refer to the same instance that you are defining h for. (And this flexibility is often useful for defining instances.)

From type inference, the result of g is restricted to be of the same type b, and the argument of f is restricted to be of type a, but there's nothing saying that the T a b c passed from one to the other is using the same c!

To fix this in this case, you can enable ScopedTypeVariables and do

    h c a = g (f a :: T a b c)

Note that this works because data families are "injective" (the type arguments of a data family can be deduced from the final type). If you had used a type family instead, even this wouldn't work, since then T a b c would not necessarily determine c at all.