[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:  8.0.1
       Component:  Compiler          |              Version:  7.10.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  typeOf ::
                                     |  Typeable (a::k) => Proxy a ->
                                     |  TypeRep
      Blocked By:                    |             Blocking:
 Related Tickets:  #9858             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by bgamari):

 I've been playing around with various ways that we could achieve this. As
 far as I can tell there are two options,

  * Encode type constructor kinds into `TyCon` and reconstruct applications
 from these at runtime. This would require that `TyCon` get a bit larger,
 and would need to include a `TypeRep`, which is unfortunate as this cost
 is paid by all users, regardless of whether they use `Typeable`.

  * Construct the kind representation at when we are asked to construct a
 `Typeable` dictionary.

 At the moment I'm leaning towards the second approach (and have a broken
 implementation in Phab:D1830).

 The trouble is that you need to be very careful when handling recursive
 kinding relationships. Consider, for instance, these examples:

 {{{#!hs
 (->) :: (->) * (* -> *)
 TYPE :: Levity -> TYPE 'Lifted
 }}}

 Here the types we are trying to derive kind representations for appear in
 their own kinds. This causes trouble in solving for these representations:

 Currently we construct `Typeable` evidence by decomposing type
 applications until we hit a tycon. One way to account for kind
 representations would be to require that when generating evidence for
 `Typeable (t :: k)` we also generate evidence for `Typeable k`. However,
 if we do this naively we end up sending the solver in a loop. Consider the
 case we are asked to solve for `Typeable (Int -> Bool)`. Evidence
 construction would roughly proceed as follows,
 {{{
 want (Typeable (Int -> Bool :: *))
     want (Typeable ((->) :: (* -> * -> *))        -- Normally this isn't a
 problem:
                                                   -- since (->) is a
 TyCon, we could
                                                   -- just stop here;
 but...
                                                   -- now we need a kind
 representation
         want (Typeable (* -> * -> *))
             want (Typeable ((->) * (* -> *)))     -- again we decompose
                 want (Typeable (->))
                     want (Typeable (* -> * -> *)) -- again solve for kind
 of (->)
                         ...                       -- now we are in a
 loop...
 }}}

 Likewise, we can also get non-trivial cycles,
 {{{#!hs
 Levity :: TYPE 'Lifted
 TYPE :: Levity -> TYPE 'Lifted
 'Lifted :: Levity
 }}}

 One way to address this issue would be to manually define these
 representations (just as we did before my recent solution to #11120),
 allowing us to tie the knot.

 It's possible, however, that I have fundamentally misunderstood something
 here. If so, please feel free to say so.

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