search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Can't pass argument of type %World to foreign function #368

Open mokshasoft opened 4 years ago

mokshasoft commented 4 years ago

Error when compiling an FFI function with a callback function of type PrimIO (), using Gambit but not Chez. A callback function of String -> PrimIO () seems to work better.

https://gist.github.com/mokshasoft/e0d3b39b2be5bbd766d93605a4d7e48d

Steps to Reproduce

  1. Run the Makefile in the gist. 
    idris2 -c --cg chez NoBug1.idr
idris2 -c --cg gambit NoBug1.idr
idris2 -c --cg chez Bug1.idr
idris2 -c --cg gambit Bug1.idr
idris2 -c --cg chez NoBug1.idr -o c_nobug1
compiling <dir>/c_nobug1.ss with output to <dir>/c_nobug1.so
idris2 -c --cg gambit NoBug1.idr -o g_nobug1
sh: -exe: command not found
idris2 --cg chez Bug1.idr -o c_bug1
compiling <dir>/c_bug1.ss with output to <dir>/c_bug1.so
idris2 --cg gambit Bug1.idr -o g_bug1
Uncaught error: Bug1.idr:1:1--4:1:Can't pass argument of type %World to foreign function
make: *** [Makefile:10: bug1] Error 1

Expected Behavior

If passing functions of type String -> PrimIO () to an FFI works it seems like passing functions of type PrimIO () should also work.

Observed Behavior

Both files pass the --check compile step. The Gambit CG cannot handle FFI callbacks of PrimIO () and prints error "Uncaught error: Bug1.idr:1:1--4:1:Can't pass argument of type %World to foreign function".

edwinb commented 4 years ago

There's a few gaps in the gambit back end, and in fact it seems I've introduced a couple more now since moving some of the FFI code to C. I don't think it's able to deal with callbacks in general yet.

I'm not likely to spend much time maintaining the gambit back end for the moment (since I can't do everything, sorry!) but maybe @abdelq as the original author might be able to help?