Spurious untouchable type variable in connection with rank-2 type and constraint family

The following code cannot be compiled:

{-# LANGUAGE ConstraintKinds, Rank2Types, TypeFamilies #-}

import GHC.Exts (Constraint)

type family F a b :: Constraint

data T b c = T

f :: (forall b . F a b => T b c) -> a
f _ = undefined

GHC outputs the following error message:

Untouchable.hs:9:6: error:
    • Couldn't match type ‘c0’ with ‘c’
        ‘c0’ is untouchable
          inside the constraints: F a b
          bound by the type signature for:
                     f :: F a b => T b c0
          at Untouchable.hs:9:6-37
      ‘c’ is a rigid type variable bound by
        the type signature for:
          f :: forall a c. (forall b. F a b => T b c) -> a
        at Untouchable.hs:9:6
      Expected type: T b c0
        Actual type: T b c
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: (forall b. F a b => T b c) -> a

Trac metadata

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