Re: Proposal: Introduce GHC.TypeNats module with natVal :: forall n proxy. KnownNat n => proxy n -> Natural

I made a trac ticket for tracking the progress https://ghc.haskell.org/trac/ghc/ticket/13181 - Oleg On 24.01.2017 16:05, Ben Gamari wrote:

Oleg Grenrus writes:

...

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.

This sounds quite reasonable to me and given how many much larger 8.2 changes are still not in the tree, I think it is in-scope for the release. I agree with David that it would make sense if the evidence itself were a Natural.

I'm not terribly concerned about compatibility in the face of unsafeCoerce. We should be certain to clearly document the change though.

Cheers,

- Ben