#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