[GHC] #10797: Kind-level functional dependencies are not resolved properly

[GHC]

#10797: Kind-level functional dependencies are not resolved properly
-------------------------------------+-------------------------------------
              Reporter:  danilo2     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.2
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Hello! Let's consider such funny class and its instances.

 {{{
 {-# LANGUAGE PolyKinds #-}
 ...

 class BaseType (a :: k) (b :: l) | a -> b, k -> l where
     baseType :: Proxy a -> Proxy b

 instance           BaseType (a :: j -> k) (out :: l) => BaseType (a (t ::
 j) :: k) (out :: l)
 }}}

 The instance does not compile:
 {{{
     Illegal instance declaration for ‘BaseType (a t) out’
       The liberal coverage condition fails in class ‘BaseType’
         for functional dependency: ‘k -> l’
       Reason: lhs type ‘k’ does not determine rhs type ‘l’
     In the instance declaration for
       ‘BaseType (a (t :: j) :: k) (out :: l)’
 }}}

 While the LHS determines the RHS. The problem is that it seems, that GHC
 doesn't infer the functional dependency of {{{k ~> l}}} from the
 dependency {{{j -> k ~> l}}}.. I've used a {{{~>}}} arrow to indicate
 fundeps. Is this a bug or am I missing something?

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