Elab script fails even when all names are imported

[Z-snails]

This might be related to #2158. Sometimes elab scripts fail, even when everything has been imported. Unfortunately I haven't got a minimised example, only the entire TyRE package: https://github.com/Z-snails/TyRE/tree/zs-bug-report

The script fails with

Error: While processing right hand side of simple. Bad elaborator
script traverse (genArm (compile Empty) (IVar EmptyFC (UN (Basic "c")))) ((compile Empty) .enumerate) (script is not a data value).

Test:26:10--26:34
 22 | 
 23 | %language ElabReflection
 24 | 
 25 | simple : CompiledSM Unit
 26 | simple = %runElab doCompile Empty
               ^^^^^^^^^^^^^^^^^^^^^^^^

when run from Test.idr, but the same script, with the same imports run from TyRE/Parser/Compile.idr fails works fine.

Steps to Reproduce

src> idris2 --find-ipkg Test.idr
src> idris2 --find-ipkg TyRE/Parser/Compile.idr

Expected Behavior

Both compile fine.

Observed Behavior

The first one fails and the second one works.

[buzden]

Is this related to #2439?

[Z-snails]

Is this related to #2439?

Possibly, although in this case the error still occurs even with everything imported