Why does this Haskell code typecheck with fundeps but produce an untouchable error with type families?

Question

Given some type definitions:

data A
data B (f :: * -> *)
data X (k :: *)

…and this typeclass:

class C k a | k -> a

…these (highly contrived for the purposes of a minimal example) function definitions typecheck:

f :: forall f. (forall k. (C k (B f)) => f k) -> A
f _ = undefined

g :: (forall k. (C k (B X)) => X k) -> A
g = f

However, if we use a type family instead of a class with a functional dependency:

type family F (k :: *)

…then the equivalent function definitions fail to typecheck:

f :: forall f. (forall k. (F k ~ B f) => f k) -> A
f _ = undefined

g :: (forall k. (F k ~ B X) => X k) -> A
g = f

• Couldn't match type ‘f0’ with ‘X’
    ‘f0’ is untouchable
      inside the constraints: F k ~ B f0
      bound by a type expected by the context:
                 F k ~ B f0 => f0 k
  Expected type: f0 k
    Actual type: X k
• In the expression: f
  In an equation for ‘g’: g = f

I read Section 5.2 of the OutsideIn(X) paper, which describes touchable and untouchable type variables, and I sort of understand what’s going on here. If I add an extra argument to f that pushes the choice of f outside the inner forall, then the program typechecks:

f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A
f _ _ = undefined

g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A
g = f

However, what specifically has me so confused in this particular example is why the functional dependency has different behavior. I have heard people claim at various times that functional dependencies like this one are equivalent to a type family plus an equality, but this demonstrates that isn’t actually true.

What information does the functional dependency provide in this case that allows f to be instantiated in a way that the type family does not?

Answer 1

I don't know if I should post this as an answer because it's still pretty hand-wavey, but I do think this is what's essentially going on:

To evaluate a (C k (B X)) => X k value, you have to choose a concrete type for k, and point to the instance C k (B X) that fulfills the constraints. To do that, you must phrase out that the typeclass' a argument has the form B f, from which the compiler can extract the f type (and find out that it's X in this case) – importantly, it can do this before actually looking at the instance, which would be the point at which f would become untouchable.

To evaluate a (F k ~ B X) => X k, it's a bit different. Here you don't need to point to a concrete instance, you merely need to guarantee that if the compiler looked up the typefamily for F k, then this type would be the same type as B X. But before actually looking up the instance, the compiler cannot here infer that F k has the form B f, and hence also not use this to unify f with the outer quantification argument because of untouchable.

Therefore, GHC's behaviour is at least not completely unreasonable. I'm still not sure if it should behave this way.

Answer 2

OK I've had a chance to play with this. There's several distractions:

In the Type Family version, just the definition for f gives error 'f0' is untouchable. (You can suppress that with AllowAmbiguousTypes; that just postpones the error to appear against g.) Let's ignore g here on.

Then without AllowAmbiguousTypes, the error message for f gives more info:

• Couldn't match type ‘f0’ with ‘f’
    ‘f0’ is untouchable
      inside the constraints: F k ~ B f0
      bound by the type signature for:
                 f :: F k ~ B f0 => f0 k
  ‘f’ is a rigid type variable bound by
    the type signature for:
      f :: forall (f :: * -> *). (forall k. F k ~ B f => f k) -> A
  Expected type: f0 k
    Actual type: f k

Aha! a rigid type variable problem. I guess because f is fixed by the equality constraint from k, which is also rigid because ...

Turning to the FunDep version without g, at what types can we call f? Try

f (undefined undefined :: X a)           -- OK
f (undefined "string"  :: X String)      -- rejected
f  Nothing                               -- OK
f (Just 'c')                             -- rejected

The rejection message (for the X String example) is

• Couldn't match type ‘k’ with ‘String’
  ‘k’ is a rigid type variable bound by
    a type expected by the context:
      forall k. C k (B X) => X k
  Expected type: X k
    Actual type: X String
• In the first argument of ‘f’, namely
    ‘(undefined "string" :: X String)’

Note the message is about k, not f which is determined from the FunDep -- or would be if we could find a suitable k.

Explanation

The signature for function f says k is existentially quantified/higher ranked. Then we can't allow any type information about k to escape into the surrounding context. We can't supply any (non-bottom) value for k, because its type would invade the forall.

Here's a simpler example:

f2 :: forall f. (forall k. f k) -> A
f2 _ = undefined

f2 Nothing                                 -- OK
f2 (Just 'c')                              -- rejected rigid type var

So that the original FunDep version compiles is a distraction: it can't be inhabited. (And that's a common symptom with FunDeps, as per my earlier suspicion.)