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

[GHC]

#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