[GHC] #13655: Spurious untouchable type variable in connection with rank-2 type and constraint family

[GHC]

#13655: Spurious untouchable type variable in connection with rank-2 type and
constraint family
-------------------------------------+-------------------------------------
           Reporter:  jeltsch        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 The following code cannot be compiled:
 {{{#!hs
 {-# 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
 }}}

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