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:

https://github.com/idris-hackers/iQuery/pull/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.