[GHC] #9858: Typeable instances should be kind-aware (was: Typeable instance for datatype and its promoted constructor is the same)

[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 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