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

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