[GHC] #9858: Typeable instances should be kind-aware

[GHC]

#9858: Typeable instances should be kind-aware
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:
            Type:  bug               |                  Status:  new
        Priority:  highest           |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.9
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:  Phab:D652
-------------------------------------+-------------------------------------

Comment (by oerjan):

 Replying to [comment:45 goldfire]:
 > I believe a sufficiently smart solver should be able to do this without
 difficulty.

 After all the discussion way above, I'll just point out now that the
 current implementation isn't one of those. I guess it was too much to hope
 for in such a hurried situation. For example, it breaks on the following
 expression (with `PolyKinds`, thanks to Shachaf):

 {{{
 typeOf :: Typeable a => Proxy a -> TypeRep
 }}}

 It seems here that it cannot deduce `Typeable (Proxy a)` from `Typeable a`
 when the kind isn't known at compile time.

 More seriously, I think the current `TypeRep` for `Typeable (a :: k)`
 doesn't contain enough information to extract the `KindRep` for `k`, much
 less to decompose it, even if the solver were to try. It seems to have
 been designed such that type application of known `Typeable` types (with
 known kinds) will work almost effortlessly, but anything fancier is
 impossible.

 Ironically I thought (with my convoluted attempts to represent everything
 in 7.8 types) that type application would be the main thing forcing kind
 decomposition to be implemented for handling currently existing code, but
 this representation simply bypasses that. And I guess if no one else has
 complained then that is currently enough for people's needs.

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