[GHC] #13161: Unexpected error about untouchable variable

[GHC]

#13161: Unexpected error about untouchable variable
-------------------------------------+-------------------------------------
           Reporter:  danilo2        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13161>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler