foreign_impl with function application not being fully reduced

[ear7h]

Steps to Reproduce

Sorry again for not minimizing this, but I have the following function which generates scheme code given a type (specifically Struct types), ie. Type -> String:

https://github.com/ear7h/idris-webgpu/blob/96f45a0878c818cc30421c9f4b0476f0420564dc/src/Utils/CTypes.idr#L88-L145

It works on most inputs, but in combination with an data FTypeArray it seems to break down. Here's an example of a call which gives an error:

https://github.com/ear7h/idris-webgpu/blob/96f45a0878c818cc30421c9f4b0476f0420564dc/src/Graphics/GLFW/Sys.idr#L202

Expected Behavior

The function fully reduces to a string.

Observed Behavior

I modified the error message to show that the reduction leaves %NApp $resolved185 [2 closures]

rlwrap idris2 --repl idris-webgpu.ipkg
3/5: Building Graphics.GLFW.Sys (src/Graphics/GLFW/Sys.idr)
Error: %foreign calling convention must evaluate to a String (%NApp $resolved185 [2 closures])

Graphics.GLFW.Sys:202:50--202:89
 198 | 
 199 | -- struct here!!
 200 | %foreign ""
 201 | prim__allocStructGLFWgamepadstate : allocStructPrimType GLFWgamepadstate
 202 | %foreign_impl prim__allocStructGLFWgamepadstate (allocStructPrimCodegen GLFWgamepadstate)
                                                        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[ear7h]

I've hacked at the compiler and changing the nf in the following snippet to nfOpt withAll fixes the issue:

Idris2/src/TTImp/ProcessType.idr

Line 39 in b2d2cf4

case !(nf defs Env.empty etm) of

Based on the documentation, I thought this meant I was missing a public somewhere but adding it to all relevant definitions still caused the compiler to give an error (although I didn't try moving the defs out of the where in allocStructPrimCodegen).

[dunhamsteve]

Typically, you would use %foreign "scheme:..." on the function. %foreign_impl was intended to be use to add additional backends when you can't change the original source file where the %foreign was defined. (For a new backend or stubbing something out for javascript.)

It is expecting a string and getting an application of something (string append?) to two arguments.

To get a better error message: If you call toFullNames on the reduced expression, it will turn the $resolved into a name. And you might need to print it back to see the arguments ("e.g. ... \{show !(quote defs empty x >>= toFullNames)}). That might help sort out what it is getting stuck on.

[dunhamsteve]

I missed your comment because I'm on my phone, but it seems to me that withAll would be appropriate here. And runElab, a similar situation, uses withAll.

[ear7h]

Typically, you would use %foreign "scheme:..." on the function. %foreign_impl was intended to be use to add additional backends when you can't change the original source file where the %foreign was defined. (For a new backend or stubbing something out for javascript.)

Understood. I ended up down this path of using lisp to build structs instead of creating an ad hoc, informally-specified, bug-ridden, slow implementation of half of lisp. But I guess I've ended up with an ad hoc, informally-specified, bug-ridden, slow implementation of half of elab reflection.