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?

Note that g = f @ X also type checks. It seems that the inference algorithm does not commit to choosing the type variable f as X. I can't see why -- usually, it's because there could be another value of f making the type (forall k. (F k ~ B f) => f k) -> A equal to (forall k. (F k ~ B X) => X k) -> A. Here, f ~ X seems to be the unique solution to me (isn't it?). Interesting. — chi
@chi I think so, too, but I don’t know enough about this particular case of the typechecker to confidently open a bug. Perhaps I ought to open a ticket anyway, and if it’s intended behavior, I will at least probably learn why? — Alexis King
Interesting indeed! I've now twice cycled my opinion as to whether this should actually typecheck with neither fundeps not type families, or only with fundeps, or with both. I just don't understand well enough how the constraints are resolved to decide. But at least I don't consider it implausible that only the fundep version should work: the crucial difference seems to be that typeclasses with their superclasses can be “unravelled” (the f be extracted out of B f), but from an equality constraint this is not possible. — leftaroundabout
Not an answer, but on your point "I have heard people claim that functional dependencies like this one are equivalent to a type family plus an equality" - yeah, it's a bit of an oversimplification. When you think about Core, you can see where the semantic differences come from. Type family instances are expressed as top-level coercions, so type instance F Int = Bool gets turned into f_int :: F Int ~ Bool. Fundeps just show up as constraints during unification, they don't affect coercions. That's why it's hard to convert between them. — Benjamin Hodgson
Sorry, I don't have an answer either, but a beware: you haven't shown the FunDep version "allows f to be instantiated." Because you haven't declared any instances for C (and got f to work with them). Type family validation is more eager than for FunDeps. So you might have that actually the two forms are equivalent in the sense: the Type family form doesn't compile; the FunDep form has no inhabited instantiations for f. Perhaps that's why you can define only f _ = undefined. So declare an instance for C; try to apply f to something. Similarly try to apply g. — AntC

leftaroundabout leftaroundabout · Accepted Answer · 2017-12-10T03:17:14

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.

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

2 Answers