[ fix ] Fix issue with eager evaluation of crashing functions (fixes #3003)

[dunhamsteve]

Issue #3003 observes that the eager evaluation of zero-argument functions can cause crashes at startup. PR #3002 triggers this issue by erasing void and unit parameters. It is particularly evident when incremental compilation is on, because inlined or unused functions are still emitted during codegen.

This PR addresses the issue by removing from the list of "constant" functions any functions that are defined to be NmCrash _ _ or that call such a function. So constants that crash or that call crashing functions will lazy after this change.

The two test cases come from #3003, and I've also checked that it unblocks #3002. Per a comment on #3003, I think Stefan Hoeck has some reservations over whether this needs to be fixed, so this change may need further discussion before merging.

[stefan-hoeck]

I'm perfectly fine with this fix, mainly because the issue at hand can be very confusing for newcomers especially so once #3002 gets merged. Thanks for looking into this!

[Z-snails]

Thanks for doing this, I have some comments, in no particular order:

I think this should also check for the Crash PrimFn

import System

partial
unreachable : a
unreachable = idris_crash "unreachable"

main : IO Int
main = do
    exitSuccess
    assert_total unreachable

This currently crashes with unreachable rather than exiting, like I would expect.

Edit: Stefan Höck pointed out the following isn't an issue
In the following code:

foo, bah : Int
foo = ?hole
bah = foo

Depending on the order in which foo and bah are processed, this could result in bah being treated as safe to eagerly evaluate, when it isn't. This is a trickier problem to solve, so I'd be ok if you leave that as future work (which I'd probably do soon anyway).
If you do want to solve this, I suggest use Libraries.Data.Graph.tarjan to split functions into mutually recursive groups, then if any function in a group calls crash then treat the whole group as calling crash.

[stefan-hoeck]

If you do want to solve this, I suggest use Libraries.Data.Graph.tarjan to split functions into mutually recursive groups, then if any function in a group calls crash then treat the whole group as calling crash.

The optimizer generating toplevel constants already runs trajan and ignores groups of mutually recursive functions, because it is not clear in which order they should appear in the generated code when they are being eagerly evaluated.

[dunhamsteve]

Yeah, I'm relying on the fact that the code is visiting the functions from the leaves up.

I've added a check for calls to unsafe primitives. I thought to initialize nonconsts with [ Builtin.idris_crash ], but saw isUnsafeBuiltin in Name.idr and figured that would be more complete.

Note that this still doesn't see an NmCrash in the middle of a function. I don't think this is needed for the original issue. I had a branch that did do that, and it got false positives for NmCrash _ "Nat case not covered" (when you convince Idris a number is zero, it emits the case statement anyway and puts that in the other branch).

[Z-snails]

I don't think this will catch all cases, because those functions should already have been inlined and replaced with the appropriate NmOp. I suggest adding a check for NmOp _ Crash _ in the same way as you currently check for NmCrash.

[dunhamsteve]

Both approaches handle your test case, but I think your proposal will be more robust. And it turns out that isUnsafeBuiltin included believe_me, which doesn't crash - it's just identity.