Problem compiling with idris-0.9.17

[mietek]

Is this related to #14?

Type checking ./IQuery/State.idr
./IQuery/State.idr:30:7:
When elaborating right hand side of isObj:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign
./IQuery/State.idr:39:16:
When elaborating right hand side of stateVarExists:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign
./IQuery/State.idr:44:14:
When elaborating right hand side of initStateVar:
No such variable mkForeign
./IQuery/State.idr:48:3:
When elaborating right hand side of IQuery.State.case block in getStateVar:
When elaborating an application of function Prelude.Functor.map:
        No such variable mkForeign
./IQuery/State.idr:57:14:
When elaborating right hand side of stateCExists:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign
./IQuery/State.idr:62:10:
When elaborating right hand side of incCount:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign
./IQuery/State.idr:87:8:
When elaborating right hand side of access:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign
./IQuery/State.idr:94:12:
When elaborating right hand side of fromState':
No such variable mkForeign
./IQuery/State.idr:116:9:
When elaborating right hand side of toState:
No such variable mkForeign
./IQuery/State.idr:140:10:
When elaborating right hand side of newState:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign
./IQuery/State.idr:149:14:
When elaborating right hand side of destroyState:
When elaborating an application of function Prelude.Monad.>>=:
        No such variable mkForeign

[BartAdv]

I haven't checked it, but I think there was some great renaming in Idris lately, and all constructors are now upper case. Try it.

[puffnfresh]

FFI completely changed in Idris. There's a paper which describes the new FFI:

http://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf

I imagine the changes will be pretty significant for IQuery.

[puffnfresh]

Looks like the FFI made it to the Idris docs, too:

http://docs.idris-lang.org/en/latest/reference/ffi.html

[david-christiansen]

Yes, but on the other hand, it's a fairly straightforward change to make. /David (from phone)

[foolswood]

Looks like someone's had a go at this: #17

[ericoporto]

@puffnfresh sorry for Necro-commenting but the link you posted is forbidden, do you know if it's available somewhere, maybe you have a backup? I am trying to find this paper. Thanks.

[gallais]

@ericoporto You can find it on the wayback machine: http://web.archive.org/web/20220430094757/https://eb.host.cs.st-andrews.ac.uk/drafts/compile-idris.pdf