Kind-level functional dependencies are not resolved properly
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?