#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 simonpj): Richard is spot on. For (1), really `A` and `'A` are entirely different, and should not compare as equal. That is probably easy to fix, by changing the fingerprint we generate for `'A`. For (2), yes absolultely, just as `Maybe Int` and `Maybe Bool` should have non-equal `TypeRep`s, so should `B 'Ordering` and `B 'Bool`. The fact that is's a kind application isn't important. The ''reason'' that bug (2) happens is, I think, that the `Typeable` instance of `B` is generated by an instance declaration: {{{ instance Typeable B where typeRep# _ = ...the TyCon for B.... }}} This instance declaration is treated as ''source code'', and source code does implicit kind instantiation. So we actually get {{{ dfun :: forall k. Typeable (B k) dfun = /\k. MkTypeableDict (...TyCon for B....) }}} We don't want this! Instead we want to treat `(B 'Bool)` just like `Maybe Bool`, using the application instance (in `Data.Typeable.Internals`), which looks roughly like this: {{{ instance (Typeable s, Typeable a) => Typeable (s a) where -- See Note [The apparent incoherence of Typable] typeRep# _ = typeRep a `mkAppTy` typeRep b }}} We would like this to be done for ''kind'' applications as well as ''type'' applications. So we need two changes * For type constructors, we need an instance that truly matches on `B` not on `B k` * We need to decompose kind applications as we do type applications. To me it seems clear that we should move to treating `Typeable` more like we treat `Coercible`, i.e. as a built-in type class that the constraint solver knows how to solve, rather than as something handed with source- level instance declarations. That would imply: * There would be no `Typeable` instances in the instance environment (which itself would be a modest saving). * Either 1. every data type constructor automatically has a `Typeable` instance (which I favour), or 1. we'd need a tiresome separate mechanism (a flag in the `TyCon`) to say whether it does or does not have a `Typeable` instance. Note that this path might ultimately allow us to have a `TypeRep` for a polymorphic type, which we can't do right now. What do people feel about (1) vs (2)? Why would we ever want a type ''not'' to be `Typeable`? Note that the code-size overhead is modest: a single top-level definition of a record defining the `TyCon`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9858#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler