[GHC] #8391: FunDeps coverage condition check failure with PolyKinds

[GHC]

#8391: FunDeps coverage condition check failure with PolyKinds
----------------------------+----------------------------------------------
       Reporter:  sbarclay  |             Owner:
           Type:  bug       |            Status:  new
       Priority:  normal    |         Milestone:
      Component:  Compiler  |           Version:  7.7
       Keywords:            |  Operating System:  Unknown/Multiple
   Architecture:            |   Type of failure:  GHC rejects valid program
  Unknown/Multiple          |         Test Case:
     Difficulty:  Unknown   |          Blocking:
     Blocked By:            |
Related Tickets:  #8356     |
----------------------------+----------------------------------------------
 The following code:

 {{{
 #!haskell
 {-# LANGUAGE FunctionalDependencies, FlexibleInstances,
 UndecidableInstances,
              TypeFamilies,
              PolyKinds #-}

 module FunDepsIssue where

 type Foo a = a

 class Foo a ~ b => Bar a b | a -> b

 instance Foo a ~ b => Bar a b
 }}}

 results in:

 {{{
     Illegal instance declaration for ?Bar k a b?
       Multiple uses of this instance may be inconsistent
       with the functional dependencies of the class.
     In the instance declaration for ?Bar a b?
 }}}

 This appears to be a regression from 7.6.3, where it compiles OK.

 The same error occurs when the type synonym is replaced with a type family
 (which is the case I was originally interested in) or a type constructor
 like `Data.Proxy`, as long as it's poly-kinded it seems. So the following
 cases also fail to compile:

 {{{
 #!haskell
 type family Foo (a :: k) :: *
 type family Foo (a :: *) :: k
 type family Foo (a :: k) :: k
 type family Foo (a :: k) :: k'
 }}}

 Looking through the source code, I think that the issue is that the
 coverage condition check doesn't close over kind variables, when it
 compares the vars on each side of the functional dependency. But `Foo a`
 has a hidden kind variable, so the l.h. varset `{a}` is insufficient to
 fix `b` using `Foo a ~ b`.

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