+1. The current situation is pretty weird. We also really should make the SNat carried in the KnownNat dictionary hold a Natural rather than an Integer, but we'll need to watch out for backwards compatibility with anyone using unsafeCoerce on those dictionaries. On Sun, Jan 22, 2017 at 7:10 PM, Oleg Grenrus wrote:

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.

---

This change would propagate to give more precise type to someNatVal:

someNatVal :: Natural -> SomeNat

which is currently someNatVal :: Integer -> Maybe SomeNat

---

The alternative would be to change the types in GHC.TypeLits, but

- it would be breaking change - hard to shim (where new module is implementable for older base, in e.g. base-compat) - we lose opportunity to separate Nat and Symbol data kinds

---

Additionally we'd deprecate the GHC.TypeLits natVal, natVal' and someNatVal

---

As related "nice to know", `Nat` and `Natural` "agree" on negation:

...

(1 - 2) :: Natural *** Exception: arithmetic underflow

...

natVal (Proxy :: Proxy (1 - 2))

<interactive>:9:1: error: • No instance for (KnownNat (1 - 2)) arising from a use of ‘natVal’ • In the expression: natVal (Proxy :: Proxy (1 - 2)) In an equation for ‘it’: it = natVal (Proxy :: Proxy (1 - 2))

---

The change is quite straightforward to do, and I'm willing to implement it even for GHC 8.2

Oleg Grenrus

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries