#10343: Make Typeable track kind information better -------------------------------------+------------------------------------- Reporter: oerjan | Owner: goldfire Type: feature request | Status: new Priority: normal | Milestone: 7.12.1 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: -------------------------------------+------------------------------------- Comment (by oerjan): Replying to [comment:12 goldfire]:
This all continues to seem straightforward to me, but I maintain (in contrast to Simon's claim in comment:8) that this is separate from kind equalities.
Whew, I was starting to worry.
{{{ [G] Typeable (a :: k) [G] Typeable (k :: *) [W] Typeable (Proxy :: k -> *) -- the Typeable solver doesn't decompose kind applications [W] Typeable (a :: k) }}}
The wanteds are easily solved from the givens.
Looks good, although note that as we discussed in #9858, the kitchen sink example ''would'' require actually decomposing `Typeable` kinds. In principle so does normal type application, once you include `kindRep`: {{{ (Typeable (a :: k1 -> k2), Typeable (b :: k1)) => Typeable (a b :: k2) }}} The only plausible source for the `kindRep` of `a b` is to decompose the kind information in `Typeable a`. Although I guess type application can still be a special case.
Since I'm the one with the plan, sounds like I should be the one to execute the plan. But probably only after I merge, since this isn't something we need today.
:) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10343#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler