[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 int-e):

 I'm wondering about the ramifications of this claim from [[Typeable
 #Medium-termsolution]]:
 > Although it is impossible to create all necessary Typeable instances for
 poly-kinded constructors at the definition site (there's an infinite
 number), it is possible to create Typeable "instances" on demand at use
 sites.

 Consider the following function:
 {{{
 f = \(p :: Proxy Proxy) -> typeRep p
 }}}
 Because the kind information of the `p` argument is not fully known at the
 site of definition, I surmise that the corresponding `Kindable` (to use
 oerjan's nomenclature) constraint gets propagated outward, meaning that at
 the core language level, `f` gets an extra argument for passing the
 `Kindable` evidence for the unknown kind argument of the second `Proxy`
 type constructor.

 It is my understanding that for the sake of backward compatibility, this
 argument is implicit and not visible (even as a constraint) in the
 Haskell-level type. Is that correct? I feel uncomfortable about this; I
 like to be able to see in the Haskell type of functions what kind of
 runtime evidence needs to be passed to a function to make it work.

 The second thing I'm wondering about is what happens when polymorphic
 kinds are never instantiated at all. Is the following program valid, and
 if so, what will the kind of the `Proxy` be at runtime?
 {{{
 {-# LANGUAGE PolyKinds, DataKinds #-}
 import Data.Typeable

 main :: IO ()
 main = print (typeRep (Proxy :: Proxy Proxy))
 }}}

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