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

[GHC]

#9858: Typeable instances should be kind-aware
-------------------------------------+-------------------------------------
        Reporter:  dreixel           |                   Owner:  dreixel
            Type:  bug               |                  Status:  new
        Priority:  highest           |               Milestone:  7.10.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:
-------------------------------------+-------------------------------------

Comment (by goldfire):

 > {{{
 > f = \(p :: Proxy Proxy) -> typeRep p
 > }}}

 More fun test cases!

 Let's see what GHC will do. First, we must insert kind unification
 variables:

 {{{
 Proxy :: forall (k :: BOX). k -> *
 typeRep :: forall (k :: BOX) (proxy :: k -> *) (a :: k).
            Typeable <k> a => proxy a -> TypeRep

 f = \(p :: Proxy <k0 -> *> (Proxy <k0>)) ->
     typeRep <k0 -> *> <Proxy <k0 -> *>> <Proxy <k0>> <$dict> p
   where
     $dict :: Typeable <k0 -> *> (Proxy <k0>)
 }}}

 We find that `k0` isn't affected by any equality constraints, and so it
 can be generalized over. We can also generalize over the `Typeable`
 constraint:

 {{{
 f :: forall (k :: BOX). Typeable <k -> *> (Proxy <k>) => Proxy <k -> *>
 (Proxy <k>) -> TypeRep
 }}}

 In surface syntax, this looks like

 {{{
 f :: Typeable (Proxy :: k -> *) => Proxy (Proxy :: k -> *) -> TypeRep
 }}}

 Looks fine to me. Am I missing something? I agree that the solver can't
 decompose the `Proxy <k>` argument, but that should be OK. Finding
 `Typeable` instances (or `Kindable` instances) doesn't involve search, so
 GHC can look for the "`Kindable`" without decomposing first. If the
 `Kindable` isn't there, no decomposition.

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