Avoiding class constraint on type level naturals

Question

I am using the Nat type in from the GHC.TypeLits module, which admittedly says the programmer interface should be defined in a separate library. In any case, the GHC.TypeLits has a class KnownNat with a class function natVal which converts a compile time Nat into a runtime Integer. There's also a type function (+) which adds compile time Nats.

The problem is that given (KnownNat n1, KnownNat n2), GHC can't derive that KnownNat (n1 + n2).

This results in an explosion of constraints needed to be added whenever I add type level naturals.

One alternative would be to define Natural numbers myself like so:

data Nat = Zero | Succ Nat

Or perhaps use a library like type-natural. But it seems silly to not use the Nats which are built into GHC, which also allow you to nicely use literal numbers in types (i.e. 0, 1) instead of having to define:

N0 = Zero
N1 = Succ N0
etc...

Is there anyway around this issue with GHC KnownNat constraints being required all over the place? Or should I just ignore the GHC.TypeLits module for my problem?

Answer 1

This GHC type checker plugin does exactly that (derives "complex" KnownNat constraints from other ones already available): https://hackage.haskell.org/package/ghc-typelits-knownnat

If "type checker plugin" sounds a little intimidating (it did to me at first), it's actually very simple to use. Simply add it as a dependency in your package file (or cabal install it) like any other package, then either add:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

to the start of your source files (much like a LANGUAGE pragma), or add it as an option globally in your package file.

There's also another plugin by the same author that's very useful as well for working with typelit Nats: https://hackage.haskell.org/package/ghc-typelits-natnormalise. This one is able to infer equality of Nat type expressions that GHC on its own gives up on: things like n + (m + 1) ~ (n + 1) + m that come up all the time when GHC is trying to prove "expected" and "actual" types match.