Consider `(#%declare #:unsafe)` for Racket codegen

[LiberalArtist]

• I have read CONTRIBUTING.md.
• I have checked that there is no existing PR/issue about my proposal.

Summary

Generating Racket modules with (#%declare #:unsafe) might improve performance.

Motivation

The main benefit should be the speed of the generated code, and perhaps other aspects of performance. The change might also let you simplify other aspects of code generation, which could help avoid issues like #2279, IIUC.

The proposal

Racket 8.0 added the special form (#%declare #:unsafe), which is similar to compiling with Chez Scheme's (optimize-level 3). In a Racket module with (#%declare #:unsafe), functions like car and fx+ are compiled the same way as unsafe-car and unsafe-fx+: that is, there is no runtime check for pair? or fixnum?, and the result of applying the function to a bad argument is unspecified. In essence, (#%declare #:unsafe) provides access to the unsafe compilation mode used for the parts of the Racket runtime system that are implemented in Racket, like the expander, regexp, and "green" thread systems.

Possible advantages of using (#%declare #:unsafe) rather than explicitly using functions like unsafe-car:

• The compiler may be able to omit checks even for functions that don't have a corresponding public unsafe--prefixed version.
• Some low-level optimizations can't be expressed by substituting one function for another, such as omitting checks for use-before-definition errors or attempts to call non-procedure? values. (The compiler already does these things when it can statically detect that they are sound.)
• Any unsafe-mode optimizations added by Racket in the future will be used automatically, without needing to modify Idris2's code generation and consider compatibility with older Racket versions.
• For debugging, (#%declare #:unsafe) could provide a single point of control for switching to safe mode.

Some caveats:

• This is a relatively new feature and not extensively used (other than in the implementation of the Racket runtime system), so it's possible you could hit bugs.
• Optimizations could possibly have undesirable consequences like increasing code size. This could be considered a special case of "you could hit bugs".
• If you do want to use safe functions in particular places, that might become more complicated.

Conclusion

I haven't actually used Idris2; I'm just a Racketeer who's admired it from afar. While (#%declare #:unsafe) is a relatively obscure feature, it seems to me like a good fit for your use-case, so I wanted to bring it to your attention.