#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

#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: -------------------------------------+------------------------------------- Comment (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}}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10797#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10797: Kind-level functional dependencies are not resolved properly -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.10.2 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10797#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler