Untouchable higher-kinded type variable in connection with RankNTypes, ConstraintKinds and TypeFamilies

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 (closed). That's why I tested with HEAD, but while #8985 (closed) 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.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture