Make Typeable track kind information better

(EDIT: My long rambling seems to have been confusing, so a summary:

I think that the type inference and runtime representation should support constructing Typeable (T :: k), even when k contains kind variables that are only mentioned in other Typeable constraints not necessarily involving the type constructor T. This will allow simple composition with polymorphic type constructors like Proxy and Typeable to work more naturally, but also more complicated things.)

With all the apparent exploitable bugs now fixed, #9858 (closed) 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 KindReps 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 TypeReps of the parts are known. For this, the internal Typeable constraint solver only ever needs to combine TypeReps, never decompose them.

Since no one else complained in #9858 (closed), 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:

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 TypeReps 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

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 [ticket:9858#comment:95886] (this example was made up as a test case before I knew what the new solver would support):

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