[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:  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):

 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).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10797#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler