Untouchable error arises from type equality, but not equivalent program with fundeps
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 |