#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): My thinking was as follows: we are treating `Nat` and `Symbol` as just infinite families of type constructors. This makes is tricky to define class instances involving them, as we essentially need to write infinitely many instances. For example: {{{ instance MyClass (T 0) where ... instance MyClass (T 1) where ... ...etc... }}} To avoid having to provide some special mechanism for declaring such instances, we just define one special class that captures this pattern, and the instances are "magically" provided by GHC. For `Nat` it is called `KnownNat`: {{{ instance KnownNat 0 where ... instance KnownNat 1 where ... ... etc .. }}} This makes it possible to define "infinite" instances for any class like this: {{{ instance KnownNat n => MyClass (T n) where ... }}} We do the exact same thing for `Typeable`: {{{ instance KnownNat n => Typeable (n :: Nat) where ... }}} The `KnownNat` constraint provides the run-time representation of the number, which is used to build the run-time representation of the type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler