## 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 |