#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