[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:
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * owner:   => goldfire
 * milestone:   => 7.12.1


Comment:

 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.

 My implementation approach would be, as oerjan suggests, adding a
 `kindRep` field in `TypeRep`. This can be done today.

 Then, define

 {{{
 class Typeable k => Typeable (a :: k) where ...
    -- probably not possible until I merge
 }}}

 This appears to be a superclass cycle, but we know it doesn't induce
 infinite regress because the kind of a kind is always `*`. So, we arrange
 to have this definition accepted.

 Then, the solver will just do the right thing. When we have a given
 `Typeable (a :: k)` constraint, the solver will spit off a `Typeable (k ::
 *)` constraint. We may have to arrange for the solver not to then spit off
 a (harmless, but potentially confusing) `Typeable (* :: *)` constraint.

 To work with `typeOf :: Typeable a => Proxy a -> TypeRep`... well it will
 all just work. Typechecking this expression leads to

 {{{
 [G] Typeable (a :: k)
 [W] Typeable (Proxy (a :: k))
 }}}

 After a little work, the solver arrives at


 {{{
 [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.

 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:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler