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 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 (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 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
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.