Idris HEAD seems to require some hints to make toState' and fromState' type-check

[stepcut]

This patch fixes this error when using Idris from git HEAD

$ make
idris --build iquery.ipkg
Type checking ./IQuery/State.idr
./IQuery/State.idr:94:12:Can't convert
        State STInt
with
        State t
./IQuery/State.idr:116:9:Can't convert
        State STInt
with
        State t
make: *** [build] Error 1

[edwinb]

This shouldn't be necessary - I'll look into it. Plenty of tests should have caught this, so it's a bit mysterious...

[edwinb]

Oops, yes, found the problem (but not the solution yet...). Hopefully it'll be a quick fix!

[edwinb]

I've made a change to master to deal with function parameters properly, so this should be unnecessary now...

On 8 Aug 2014, at 05:52, stepcut [email protected] wrote:

This patch fixes this error when using Idris from git HEAD

$ make
idris --build iquery.ipkg
Type checking ./IQuery/State.idr
./IQuery/State.idr:94:12:Can't convert
State STInt
with
State t
./IQuery/State.idr:116:9:Can't convert
State STInt
with
State t
make: *** [build] Error 1

You can merge this Pull Request by running

git pull https://github.com/stepcut/iQuery master
Or view, comment on, or merge it at:

#14

Commit Summary

• Idris HEAD seems to require some hints to make toState' and fromState' type-check
File Changes

• M IQuery/State.idr (18)
Patch Links:

• https://github.com/idris-hackers/iQuery/pull/14.patch
• https://github.com/idris-hackers/iQuery/pull/14.diff
—
Reply to this email directly or view it on GitHub.