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