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

GHC ghc-devs at haskell.org
Mon Jul 2 07:28:48 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 simonpj):

 >  This makes it possible to define "infinite" instances for any class
 like this:

 Well, how does the `KnownNat` constraint help in defining the instance for
 `MyClass (T n)`?  Presumably, because `KnownNat` lets you use `natSign`:
 {{{
 class KnownNat (n :: Nat) where
   natSing :: SNat n
 }}}
 If that's what you need for `instance MyClass (T n)`, then that makes
 perfect sense.

 But it makes no such sense for `Typeable`.  How does having `KnownNat n`
 available help you write the `Typeable` instance?

 I think we just need built-in behaviour for `Typeable (n :: Nat)`, without
 any reference to `KnownNat`, don't we?   There is ''some'' such built-in
 behaviour already, but I don't understand what it is, and it's clearly
 dodgy as this ticket shows.

 Would you like to elaborate your description of what happens now?

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


More information about the ghc-tickets mailing list