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

[GHC]

#10343: Make Typeable track kind information better
-------------------------------------+-------------------------------------
        Reporter:  oerjan            |                   Owner:
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:
       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:
-------------------------------------+-------------------------------------
Description changed by oerjan:

Old description:

> (EDIT: My long rambling seems to have been confusing, so a summary:
>
> I want 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 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.

New description:

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