Skip to content

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?

Edited by danilo2
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information