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.