#13181: Introduce GHC.TypeNats module with natVal -------------------------------------+------------------------------------- Reporter: phadej | Owner: phadej Type: feature request | Status: patch Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3024 Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): This implementation is lacking motivation anywhere so I will add it in case anyone was wondering. One possible design choice would have been to keep the internal representation as an `Integer` and at the interface boundary do the error- checking when converting to a `Natural` once. Oleg preferred this implementation as it will cause the compiler to fail sooner if we accidentally do something like cause an interflow by subtracting or anything like that. The interface boundary is shifted to converting into `EvTerm`. There is a related ticket #13186 which talks about actually representing the evidence as `Natural` as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13181#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler