[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
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by danilo2:

Old description:

> 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?

New description:

 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler