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

26 Aug 2015

      #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