[GHC] #9223: Type equality makes type variable untouchable

[GHC]

#9223: Type equality makes type variable untouchable
-------------------------------------------+-------------------------------
       Reporter:  Feuerbach                |             Owner:
           Type:  bug                      |            Status:  new
       Priority:  normal                   |         Milestone:
      Component:  Compiler (Type checker)  |           Version:  7.8.2
       Keywords:                           |  Operating System:
   Architecture:  Unknown/Multiple         |  Unknown/Multiple
     Difficulty:  Unknown                  |   Type of failure:
     Blocked By:                           |  None/Unknown
Related Tickets:                           |         Test Case:
                                           |          Blocking:
-------------------------------------------+-------------------------------
 This doesn't look right:

 {{{
 {-# LANGUAGE RankNTypes, TypeFamilies #-}

 type family TF (m :: * -> *)

 run1 :: (forall m . Monad m => m a) -> a
 run1 = undefined

 run2 :: (forall m . (Monad m, TF m ~ ()) => m a) -> a
 run2 = undefined

 -- this works
 x1 = run1 (return ())

 -- this fails
 x2 = run2 (return ())
 {-
     Couldn't match expected type ‘a’ with actual type ‘()’
       ‘a’ is untouchable
         inside the constraints (Monad m, TF m ~ ())
         bound by a type expected by the context:
                    (Monad m, TF m ~ ()) => m a
         at untouchable.hs:15:6-21
       ‘a’ is a rigid type variable bound by
           the inferred type of x2 :: a at untouchable.hs:15:1
     Relevant bindings include x2 :: a (bound at untouchable.hs:15:1)
     In the first argument of ‘return’, namely ‘()’
     In the first argument of ‘run2’, namely ‘(return ())’
 -}
 }}}

 I would expect x2 to type check just like x1 does.

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