[GHC] #15322: `KnownNat` does not imply `Typeable` any more when used with plugin
GHC
ghc-devs at haskell.org
Fri Jun 29 18:16:09 UTC 2018
#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
More information about the ghc-tickets
mailing list