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?

Stereoscopic

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. – Cloistral

@Cloistral 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? – Stereoscopic

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. – Maverick

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. – Hypo

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. – Uncouth

@Uncouth This is a reduction of a larger actual example where C is actually Reifies from Data.Reflection. I assure you, it really does typecheck without any bottoms anywhere and after applying g. You can even get this example to typecheck without bottoms yourself by changing C to Reifies and changing f’s definition to f m = reify B (\(_ :: Proxy s) -> m @s seq` A)` (after making A and B inhabited, of course). – Stereoscopic

to answer @chi's first comment: with g = f, yes that fixes the types s.t. f ~ X. If you take out the definition for g, then f can be any constructor type -- such as Maybe. – Uncouth

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.

Maverick

While what you say makes some sense, I’m a little skeptical of this answer. Here’s why: if you change data B to type family B, the version with the functional dependency still typechecks! This seems like it would contradict your explanation for why the fundep version works the way it does, since B f ~ B X does not imply f ~ X if B is a type family. – Stereoscopic

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.)

Uncouth

BTW you get a similar f0 is untouchable rejection with this signature f :: forall f. (forall k. f ~ X => f k) -> A. No Type Family or FunDep in sight. – Uncouth