[GHC] #9090: Untouchable higher-kinded type variable in connection with RankNTypes, ConstraintKinds and TypeFamilies

[GHC]

#9090: Untouchable higher-kinded type variable in connection with RankNTypes,
ConstraintKinds and TypeFamilies
-------------------------------------+-------------------------------------
       Reporter:  kosmikus           |             Owner:
           Type:  bug                |            Status:  new
       Priority:  normal             |         Milestone:
      Component:  Compiler (Type     |           Version:  7.8.2
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 I have the following module
 {{{
 {-# LANGUAGE RankNTypes, ConstraintKinds, TypeFamilies #-}

 import GHC.Exts (Constraint)

 type family D (c :: Constraint) :: Constraint
 type instance D (Eq a) = Eq a

 -- checks
 f :: Eq b => (forall a. D (Eq a) => f a -> Bool) -> f b -> Bool
 f g x = g x

 -- checks
 f' :: Eq b => (forall a. Eq a => f a -> Bool) -> f b -> Bool
 f' = f

 -- checks, so GHC seems to think that both types are interchangeable
 f'' :: Eq b => (forall a. D (Eq a) => f a -> Bool) -> f b -> Bool
 f'' = f'

 -- checks
 test' y = f' (\ (Just x) -> x /= x) y

 -- fails
 test y = f (\ (Just x) -> x /= x) y

 -- fails too, unsurprisingly
 test'' y = f'' (\ (Just x) -> x /= x) y
 }}}

 The module checks with GHC-7.6.3, but fails in GHC-7.8.2 and
 GHC-7.9.20140430 with
 {{{
 src/Test.hs:24:16:
     Couldn't match type ‘f’ with ‘Maybe’
       ‘f’ is untouchable
         inside the constraints (D (Eq a))
         bound by a type expected by the context: (D (Eq a)) => f a -> Bool
         at src/Test.hs:24:10-35
       ‘f’ is a rigid type variable bound by
           the inferred type of test :: Eq b => f b -> Bool
           at src/Test.hs:24:1
     Possible fix: add a type signature for ‘test’
     Expected type: f a
       Actual type: Maybe a
     Relevant bindings include
       y :: f b (bound at src/Test.hs:24:6)
       test :: f b -> Bool (bound at src/Test.hs:24:1)
     In the pattern: Just x
     In the first argument of ‘f’, namely ‘(\ (Just x) -> x /= x)’
     In the expression: f (\ (Just x) -> x /= x) y

 src/Test.hs:27:20:
     Couldn't match type ‘f’ with ‘Maybe’
       ‘f’ is untouchable
         inside the constraints (D (Eq a))
         bound by a type expected by the context: (D (Eq a)) => f a -> Bool
         at src/Test.hs:27:12-39
       ‘f’ is a rigid type variable bound by
           the inferred type of test'' :: Eq b => f b -> Bool
           at src/Test.hs:27:1
     Possible fix: add a type signature for ‘test''’
     Expected type: f a
       Actual type: Maybe a
     Relevant bindings include
       y :: f b (bound at src/Test.hs:27:8)
       test'' :: f b -> Bool (bound at src/Test.hs:27:1)
     In the pattern: Just x
     In the first argument of ‘f''’, namely ‘(\ (Just x) -> x /= x)’
     In the expression: f'' (\ (Just x) -> x /= x) y
 }}}

 I'd expect it to typecheck.

 At first, I thought this might be related in some way to #8985. That's why
 I tested with HEAD, but while #8985 seems indeed to be fixed, this is
 still a problem there.

 Also, while my simplified test case compiles with GHC-7.6.3, my original
 more complicated program does not, so there might be another report
 forthcoming if I manage to isolate the difference.

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