...

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.

I also developed [type-natural] package, which comes with the showcase of arithmetic lemma. This builds on [equational-reasoning] package to make proof-writing easier. [type-natural]: https://hackage.haskell.org/package/type-natural [equational-reasoning]: https://hackage.haskell.org/package/equational-reasoning -- Hiromi ISHII konn.jinro@gmail.com

2023/01/13 19:02、Henning Thielemann のメール:

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 plugin.

Has someone already tried to connect SBV to a type checker plugin? _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.