<div dir="ltr">Yeah the error message was really confusing. Install z3 solver fixed the issue.<div><br></div><div>- baojun</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, May 2, 2016 at 10:47 AM Kosyrev Serge <_<a href="mailto:deepfire@feelingofgreen.ru">deepfire@feelingofgreen.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Baojun Wang <<a href="mailto:wangbj@gmail.com" target="_blank">wangbj@gmail.com</a>> writes:<br>
> ghc-typelits-natnormalise worked for the example. Tried<br>
> type-nat-solver too, however, got bellow error (maybe just because my<br>
> cabal setup):<br>
><br>
> z3: runInteractiveProcess: runInteractiveProcess: exec: does not exist<br>
> (No such file or directory)<br>
<br>
These runInteractiveProcess errors are *notoriously* unintelligible,<br>
reliably confusing every single person seeing them for the first time..<br>
<br>
In this case the 'z3' executable is missing -- most likely due to the Z3<br>
solver not installed on your machine.<br>
<br>
--<br>
с уважениeм / respectfully,<br>
Косырев Сергей<br>
</blockquote></div>