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

[Henning Thielemann]

On Fri, 13 Jan 2023, 石井大海 wrote:

> Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code:
>
> https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger
>
> Formally, this augments GHC's type checker with Presburger Arithmetic Solver.

This sounds promising!

I know that Iavor Diatchki implemented a Presburger Arithmetic Solver for 
GHC type checking many years ago, but when I asked last time, he 
recommended ghc-typelits-natnormalise.

> Although there indeed be some propositions that this plugin cannot 
> solve, but together with ghc-typelits-natnormalise and 
> ghc-typelits-knownnat, relatively wide range of propositions can be 
> solved automatically in my experiences.

It is good to know that I can combine different type checker plugins.