Opened 4 years ago

Closed 4 years ago

Last modified 2 years ago

#10797 closed bug (invalid)

Kind-level functional dependencies are not resolved properly

Reported by: danilo2 Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: FunDeps Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by danilo2)

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?

Change History (6)

comment:1 Changed 4 years ago by danilo2

Description: modified (diff)

comment:2 Changed 4 years ago by danilo2

As an related question - I'm trying to determine the "base type" of a value. I mean, for Proxy Int I want to get Proxy Int but for something like Proxy :: Maybe a (for a known a) I want to get Proxy :: Maybe. I was trying to do this using closed Type Families as well, but without success:

type family BaseTypeTF (t :: *) where
    BaseTypeTF (Proxy ( (a :: k -> l) (b :: k) )) = BaseTypeTF (Proxy (a :: k -> l) )
    BaseTypeTF (Proxy (a :: x) ) = Proxy (a :: x)

error:

    Family instance purports to bind type variable ‘k’
      but the real LHS (expanding synonyms) is:
        BaseTypeTF (Proxy (a b)) = ...
    In the equations for closed type family ‘BaseTypeTF’
    In the type family declaration for ‘BaseTypeTF’

That could be understandable for two reasons (but I'm not sure if that are good guesses): 1) We've go no mechanism like OverlappingInstances in TypeFamilies, but on the other hand closed type families provides us with similar functionality, but for a closed world, which is fine in this case 2) We've got no syntax to explicitly type the result of this family, because it's kind is *, but it is in fact Proxy :: something, which we are impossible to type if GHC has any ambiguity (which again maybe not related to this question).

comment:3 Changed 4 years ago by danilo2

Here is even simpler example:

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

instance {-# OVERLAPPABLE #-} BaseType (( (a :: l -> x) (t :: l)) ) (a :: l -> x) where baseType _ = Proxy

error:

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

where it seems again, that GHC cannot infer funded between l -> x and l -> x, "thinking" that LHS of funded is x instead of l -> x

comment:4 Changed 4 years ago by danilo2

And one more additional fact. We can implement what I want creating some boilerplate. I'm sure there should be way to avoid it (without using TemplateHaskell):

class BaseType a b | a -> b where
    baseType :: a -> b

instance {-# OVERLAPPABLE #-} out ~ (Proxy a) => BaseType (Proxy a) out
instance {-# OVERLAPPABLE #-} out ~ (Proxy a) => BaseType (Proxy (a t1)) out
instance {-# OVERLAPPABLE #-} out ~ (Proxy a) => BaseType (Proxy (a t1 t2)) out
instance {-# OVERLAPPABLE #-} out ~ (Proxy a) => BaseType (Proxy (a t1 t2 t3)) out
instance {-# OVERLAPPABLE #-} out ~ (Proxy a) => BaseType (Proxy (a t1 t2 t3 t4)) out
instance {-# OVERLAPPABLE #-} out ~ (Proxy a) => BaseType (Proxy (a t1 t2 t3 t4 t5)) out
...

comment:5 Changed 4 years ago by simonpj

Resolution: invalid
Status: newclosed

Let's take your simpler example:

class BaseType @k @l (a :: k) (b :: l)
    | a -> b, k -> l where ...

I have added in the (invisible in source code) kind parameters to BaseType.

Now the instance:

instance BaseType @x @(y->x)
                  (( (v :: y -> x) (t :: y)) ) (v :: y -> x) 
   where ...

Again I have added in the invisible kind parameters, and I've changed variable names to avod name clashes. In this instance we see the following instantiation of the class variables:

  Class variable     Instantiated by
        k                x
        l                y->x
        a::k             ((v::y->x) (t::y)) :: x
        b::l             t :: y

Now look at the fundeps.

  • a -> b: Does the type that instantiates a::k (namely ((v::y->x) (t::y)) :: x) determine the type that instantiates b::l (namely t::y)? Yes, both t and y appear in the lhs type.
  • k->l: Does the kind that instantiates k (namely x) determin the kind that instantiates l (namely y->x)? Obviously not. So the instance is rejected.

If you omit the fundep k->l you'll be fine, and indeed all your examples work then.

Simon

comment:6 Changed 2 years ago by simonpj

Keywords: FunDeps added
Note: See TracTickets for help on using tickets.