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

[GHC]

#10343: Make Typeable track kind information better
-------------------------------------+-------------------------------------
              Reporter:  oerjan      |             Owner:
                  Type:  feature     |            Status:  new
  request                            |         Milestone:
              Priority:  normal      |           Version:  7.10.1
             Component:  Compiler    |  Operating System:  Unknown/Multiple
              Keywords:              |   Type of failure:  None/Unknown
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:  9858
             Test Case:  typeOf ::   |
  Typeable (a::k) => Proxy a ->      |
  TypeRep                            |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 With all the apparent exploitable bugs now fixed, #9858 seems to be
 settling down.  Simon P.J. asked me to make a new ticket for some quibbles
 I still have with limitations of the new design.  These started with some
 examples that I discussed there pre-implementation with Richard Eisenberg,
 and which he concluded could be supported by a "sufficently smart solver".

 In the new (current) design, a `TypeRep` ''does'' contain kind
 information, which as I understand it is a list of `KindRep`s for the
 explicit kind parameters applied to the type constructor after type
 inference.  This is sufficient to prevent confusing the same type
 constructor used at different kinds, and also easily supports type
 application ''provided'' the `TypeRep`s of the parts are known. For this,
 the internal `Typeable` constraint solver only ever needs to combine
 `TypeRep`s, never decompose them.

 Since no one else complained in #9858, I assume this is enough for what
 people are currently using `Typeable` for. However:

 I think the current `TypeRep` representation for `Typeable (a :: k)`
 doesn't contain enough information to generally extract the `KindRep` for
 `k` itself, much less to decompose it, even if the internal `Typeable`
 solver were to try.  This prevents some polykinded code that is
 intuitively sound, and which "worked" in the old system, although if only
 because it didn't try to track kinds at all.

 For example, the following expression, with `PolyKinds` enabled:

 {{{#!hs
 typeOf :: Typeable a => Proxy a -> TypeRep
 }}}

 In the old system, this worked simply by combining the `TypeRep` for
 `Proxy` with the `TypeRep` for `a`.  But in the new system, it fails,
 because the `TypeRep` for `Proxy` needs to know the kind of `a`, which is
 neither statically known nor available from the `TypeRep` of `a`. You
 would need to have compile-time information about the type constructor of
 `a` to even know how to build the `KindRep` from the kind arguments.

 This problem with constructing `TypeRep`s would arise whenever a
 polykinded type constructor is applied to a type whose kind is not a known
 monomorphic one.  The second similar one I can think of is

 {{{#!hs
 typeRep :: Typeable a => Proxy (Typeable a) -> TypeRep
 }}}

 In an ideal system, we can also find use cases that require not just
 extracting the `KindRep` for a type, but also decomposing it. Here is my
 very hypothetical kitchen sink example from [comment:46:ticket:9858] (this
 example was made up as a test case before I knew what the new solver would
 support):

 {{{#!hs
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE AutoDeriveTypeable #-}

 import Data.Typeable

 newtype C a b = C ()

 step :: Proxy (a :: [k] -> *) -> Proxy (C a :: [k -> *] -> *)
 step Proxy = Proxy

 nest :: Typeable (a :: [k] -> *) => Int -> Proxy a -> TypeRep
 nest 0 x = typeRep x
 nest n x = nest (n-1) (step x)

 main = print $ nest 10 (Proxy :: Proxy (C () :: [()] -> *))
 }}}

 Here, to make this compile, the solver would need to derive `Typeable (C a
 :: [k -> *] -> *]` from `Typeable (a :: [k] -> *)`, which at runtime
 requires first extracting the `KindRep` of `k` from the `TypeRep` of `a`,
 and then building the `TypeRep` for the correctly kinded `C`.  At least
 the former part seems essentially impossible with the current `TypeRep`
 representation, even with a more clever solver.

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