[GHC] #15322: `KnownNat` does not imply `Typeable` any more when used with plugin

[GHC]

#15322: `KnownNat` does not imply `Typeable` any more when used with plugin
-------------------------------------+-------------------------------------
        Reporter:  chshersh          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  typeable,knownnat
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #10348            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by diatchki):

 I don't think the apartness issue is specific to `KnownNat` or nats for
 that matter, it really is more about type functions.  From what I've seen,
 people tend to notice the issue more when working with nats for two
 reasons (1) they are used to `0` and `succ` being constructors, and so one
 can define things inductively using them; (2) when using type nats, one
 simply uses type functions a lot more than in ordinary code.

 I also think that it would be quite cool to work out a system for matching
 on type functions (at least in some special cases), but I'd rather not do
 it through plugins.

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