#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature | Status: new request | Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- See [https://mail.haskell.org/pipermail/libraries/2017-January/027615.html libraries thread] Currently we have in the GHC.TypeLits module {{{ natVal :: forall n proxy. KnowNat n => proxy n -> Integer }}} However, the result integer is never negative. Numeric.Natural module is in base since base-4.8.0.0. --- I propose that we introduce new module GHC.TypeNats with natVal and natVal' {{{ natVal :: forall n proxy. KnownNat n => proxy n -> Natural }}} and {{{ natVal' :: forall n. KnownNat n => Proxy# n -> Natural }}} and other KnownNat related terms and type families. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13181 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler