Baojun Wang <wangbj@gmail.com> writes:
> ghc-typelits-natnormalise worked for the example. Tried
> type-nat-solver too, however, got bellow error (maybe just because my
> cabal setup):
>
> z3: runInteractiveProcess: runInteractiveProcess: exec: does not exist
> (No such file or directory)

These runInteractiveProcess errors are *notoriously* unintelligible,
reliably confusing every single person seeing them for the first time..

In this case the 'z3' executable is missing -- most likely due to the Z3
solver not installed on your machine.

--
с уважениeм / respectfully,
Косырев Сергей