GitLab

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

I don’t know if this is actually a bug—it seems entirely reasonable to me that I don’t fully understand what is going on here—but I’m stumped as to why GHC rejects this program but accepts the one involving functional dependencies. I would expect it to either accept or reject both programs, given they seem equivalent.

Is this just an unfortunate infelicity of the differences between how functional dependencies and type equalities are internally solved? Or is there a deeper difference between these two programs?

,,(Note: This ticket is adapted from this Stack Overflow question.),,

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture