[Haskell-cafe] Current state of type-level natural number programming

[Henning Thielemann]

Almost ten years ago I tried to convert the package llvm-tf to use 
type-level naturals but it did not lead very far.

What is the current state of type-level natural number programming and 
reasoning?

I need type-level naturals for vectors of static size.
The type checker must know things like:

n+n ~ 2*n
n*m ~ m*n

(Pos - positive natural number)
n::Nat, m::Pos -> n+m :: Pos
n::Nat, m::Pos -> n*m :: Nat
n::Pos, m::Pos -> n*m :: Pos


I need to access an element from a heterogeneous list with a typenat 
index. That is, I need a kind of induction.


I know of ghc-typelits-natnormalise, but it has some problems with 
inequalities that I need:

"Could not deduce n~0 from the context n<=0"

https://github.com/clash-lang/ghc-typelits-natnormalise/issues/33


"Could not deduce: (n0 + 1) ~ m from the context: 1 <= m"

https://github.com/clash-lang/ghc-typelits-natnormalise/issues/59



So, what is the current state of the art? What libraries, what GHC 
extensions? Any tutorials?