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

Henning Thielemann lemming at henning-thielemann.de
Fri Jan 13 10:02:16 UTC 2023

On Fri, 13 Jan 2023, rowan goemans wrote:

> I'm a heavy user of ghc-typelits-natnormalise.
> I can feel your pain that it sometimes isn't able to solve seemingly "simple" 
> constraints. But not all is lost in those cases. The `constraints` package 
> allows one to solve `Nat` constraints out of thin air, provided you go 
> through a function to do it.
> nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0)
> nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))

Good to know that there are ways to add missing transformations.

Ideally there would be a way without unsafeCoerce, i.e. that I could prove 
a property manually using some proof steps expressed in functions.

Alternatively, maybe I can write missing steps in a custom type checker 

Has someone already tried to connect SBV to a type checker plugin?

More information about the Haskell-Cafe mailing list