## Unexpected error about untouchable variable

Hello! I've got a strange error here. Let's consider the following code:

```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
data X
data Expr a = Expr Int
type family Sum a b
type instance Sum X X = X
app :: Expr l -> (Expr l') -> m (Expr (Sum l l'))
app = undefined
finish :: Builder (Expr l) -> Builder (Expr X)
finish = undefined
type family Foo (m :: * -> *) :: * -> *
class (Monad m, Foo (Foo m) ~ Foo m) => Ctx (m :: * -> *)
newtype Builder a = Builder (forall m. Ctx m => m a)
f :: Builder (Expr X) -> Builder (Expr X) -> Builder (Expr X) -> Builder (Expr X)
f mop ma mb = finish $ Builder $ app (undefined :: (Expr X)) (undefined :: (Expr X))
main :: IO ()
main = return ()
```

it results in error:

```
UT.hs:24:34: error:
• Couldn't match type ‘l0’ with ‘X’
‘l0’ is untouchable
inside the constraints: Ctx m
bound by a type expected by the context:
Ctx m => m (Expr l0)
at UT.hs:24:24-84
Expected type: m (Expr l0)
Actual type: m (Expr (Sum X X))
• In the second argument of ‘($)’, namely
‘app (undefined :: Expr X) (undefined :: Expr X)’
In the second argument of ‘($)’, namely
‘Builder $ app (undefined :: Expr X) (undefined :: Expr X)’
In the expression:
finish $ Builder $ app (undefined :: Expr X) (undefined :: Expr X)
```

And that's very interesting, because it should (according to my knowledge) not happen. It is caused by the line: `finish $ Builder $ app (undefined :: (Expr X)) (undefined :: (Expr X))`

.

And we can observe here couple of things. First of all `app :: Expr l -> (Expr l') -> m (Expr (Sum l l'))`

and `Sum X X = X`

, so `app (undefined :: (Expr X)) (undefined :: (Expr X)) :: Expr X`

- and GHC can clearly see it.

What is more interesting is that if we put this signature explicitly it works! So If we change the error line to:

```
...
f mop ma mb = finish $ (Builder $ app (undefined :: (Expr X)) (undefined :: (Expr X)) :: Builder (Expr X)
```

it compiles fine.

Another interesting fact is that if I remove the constraint `Foo (Foo m) ~ Foo m`

it also compiles fine, which is even more strange.

## Trac metadata

Trac field | Value |
---|---|

Version | 8.0.2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |