[GHC] #14190: Typeable imposes seemingly redundant constraints on polykinded instances

[GHC]

#14190: Typeable imposes seemingly redundant constraints on polykinded instances
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  Typeable
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here's how I think of it:

 1. Given `r :: TypeRep (t :: k)`, can I somehow obtain `rk :: TypeRep k`?
 The current answer is "yes": use `typeRepKind r`.

 2. Given `d :: Typeable (t :: k)`, can I somehow obtain `dk :: Typeable
 k`?  The answer clearly should be "yes of course", because a `Typeable`
 dictionary is no more than a wrapper around a `TypeRep`.

 3. One way to achieve (2) would to make `Typeable k` a superclass of
 `Typeable (a::k)`.  But that would be stupid.
   * It'd mean that every `Typeable (t::k)` dictionary was represented as a
 pair of a dictionary for `Typeable k` and a `TypeRep t`.
   * But the latter already can provide a `TypeRep k`, via (1)
   * Moreover that `Typeable k` dictionary would itself be a pair, and so
 on infinitely.

 So, assuming we want to continue to have `typeRepKind`, the obvious way
 forward is to teach the solver that it behaves as a kind of virtual
 superclass of `Typeable`. That is, if you have `[G] Typeable (t::k)` then,
 when expanding superclasses, you can extract `Typeable k`.  Not terribly
 hard; we'd need a new `EvTerm` to express that extraction.  As with
 undecidable superclasses we'd only want to do one step at a time.

 Then, quite separately, we might like to think about how to make
 `typeRepKind` more efficient.

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