#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 LeanderK): You are right, the issue mostly stems from the fact (I think? At least that is the most common problem where it all breaks down) that I can't convince the typechecker that things defined by induction (through 0 and (n+1)) are valid and hold for every n. I have no idea what the best technical solution would be. I am just a user. Here's a related issue: https://github.com/clash-lang/ghc-typelits- natnormalise/issues/13, which is very similar to the usual pains when I use type-level nats. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15322#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler