How do you get and use the dependent type from a type class with functional dependencies?

Question

How do you get and use the dependent type from a type class with functional dependencies?

To clarify and give an example of my latest attempt (minimised from actual code I was writing):

class Identifiable a b | a -> b where  -- if you know a, you know b
    idOf :: a -> b

instance Identifiable Int Int where
    idOf a = a

f :: Identifiable Int b => Int -> [b]  -- Does ghc infer b from the functional dependency used in Identifiable, and the instance?
f a = [5 :: Int]

But ghc does not infer b, it seems, as it prints this error:

Couldn't match expected type ‘b’ with actual type ‘Int’
  ‘b’ is a rigid type variable bound by
      the type signature for f :: Identifiable Int b => Int -> [b]
      at src/main.hs:57:6
Relevant bindings include
  f :: Int -> [b] (bound at src/main.hs:58:1)
In the expression: 5 :: Int
In the expression: [5 :: Int]
In an equation for ‘f’: f a = [5 :: Int]

For context, here's a less minimised example:

data Graph a where
    Graph :: (Identifiable a b) => GraphImpl b -> Graph a

getImpl :: Identifiable a b => Graph a -> GraphImpl b
getImpl (Graph impl) = impl

The workaround here would be to add b as type arg to Graph:

data Graph a b | a -> b where
    Graph :: (Identifiable a b) => GraphImpl b -> Graph a

The full context: I have a Graph of entities that each have an id, each entity is assigned to 1 node. You can look up a node by entity. I also have a Graph'which consists of nodes (which can be assigned an entity), and to lookup a node you need to provide the node's id, which is an Int. Graph uses Graph' internally. I have an IdMap which maps ids of entities to ids of nodes in Graph'. This is my Graph definition:

data Graph a where
    Graph  :: (Identifiable a b) => {
    _idMap :: IdMap b,
    _nextVertexId :: Int,
    _graph :: Graph' a
} -> Graph a

---

Answer: Use type families, see Daniel Wagner's answer. For the full story, see Reid Barton's answer.

Answer 1

In GHC's implementation, functional dependencies can constrain the values of type variables that would otherwise be ambiguous (in the show . read sense). They cannot be used to provide evidence that two types are equal, in the way that equality constraints can. My understanding is that functional dependencies predate the addition of coercions to GHC's intermediate Core language, and these coercions are needed in general in order to translate the kinds of programs you are expecting to work into well-typed Core programs.

(This situation is arguably for the best, since GHC does not really enforce the functional dependency condition globally and it would be easy to break type safety if programs like your first one were accepted. On the other hand, GHC could also do a better job of enforcing global consistency of instances.)

The short version of this is that the type checker's logic around functional dependencies is not as strong as you might expect, especially in conjunction with newer type system features like GADTs. I recommend using type families in these situations instead, as exemplified by Daniel Wagner's answer.

https://ghc.haskell.org/trac/ghc/ticket/345 is an old ticket on a similar theme, so you can see that this is a long-standing known issue with functional dependencies and that using type families instead is the officially recommended solution.

If you want to retain the style in which Identifiable has two type arguments, you can also set up your program in the form

type family IdOf a
class (b ~ IdOf a) => Identifiable a b where
    idOf :: a -> b

type instance IdOf Int = Int
instance Identifiable Int Int where
    idOf a = a

f :: Identifiable Int b => Int -> [b]
f a = [5 :: Int]