[GHC] #10343: Make Typeable track kind information better

[GHC]

#10343: Make Typeable track kind information better
-------------------------------------+-------------------------------------
        Reporter:  oerjan            |                   Owner:  goldfire
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.10.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:  typeOf ::
 Related Tickets:  #9858             |  Typeable (a::k) => Proxy a ->
                                     |  TypeRep
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by oerjan):

 Replying to [comment:12 goldfire]:
 > This all continues to seem straightforward to me, but I maintain (in
 contrast to Simon's claim in comment:8) that this is separate from kind
 equalities.

 Whew, I was starting to worry.

 > {{{
 > [G] Typeable (a :: k)
 > [G] Typeable (k :: *)
 > [W] Typeable (Proxy :: k -> *)  -- the Typeable solver doesn't decompose
 kind applications
 > [W] Typeable (a :: k)
 > }}}
 >
 > The wanteds are easily solved from the givens.

 Looks good, although note that as we discussed in #9858, the kitchen sink
 example ''would'' require actually decomposing `Typeable` kinds.

 In principle so does normal type application, once you include `kindRep`:

 {{{
 (Typeable (a :: k1 -> k2), Typeable (b :: k1)) => Typeable (a b :: k2)
 }}}

 The only plausible source for the `kindRep` of `a b` is to decompose the
 kind information in `Typeable a`.  Although I guess type application can
 still be a special case.

 > Since I'm the one with the plan, sounds like I should be the one to
 execute the plan. But probably only after I merge, since this isn't
 something we need today.

 :)

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