Dead code in compile data

[nukisman]

Compiler.Common.getCompileDataWith produces unused top-level definitions (at least for some primitive and prelude functions).

Steps to Reproduce

Compile some program

module Main

main : IO ()
main = do
  putStrLn "HelloWorld"

with dump compile data option

mkdir -p build/dump && \
time idris2 \
    --source-dir src \
    --dumpcases build/dump/def.named \
    --dumplifted build/dump/def.lifted \
    --dumpanf build/dump/def.anf \
    --dumpvmcode build/dump/def.vmcode \
    src/Main.idr && \

See some of dumps or result executable code cat build/dump/def.named

Expected Behavior

No unused top-level definitions in dumped compile data and result executable:

Main.main = [{ext:0}]: (Prelude.IO.prim__putStr ["HelloWorld\n", !{ext:0}])
Prelude.IO.prim__putStr = Foreign call ["C:idris2_putStr, libidris2_support, idris_support.h", "node:lambda:x=>process.stdout.write(x)", "browser:lambda:x=>console.log(x)"] [String, %World] -> IORes Unit
PrimIO.unsafePerformIO = [{arg:1}]: (PrimIO.unsafeCreateWorld [(%lam w (%let {eff:0} (!{arg:1} [!w]) !{eff:0}))])
PrimIO.unsafeCreateWorld = [{arg:1}]: (!{arg:1} [%MkWorld])

Observed Behavior

Unused top-level definitions:

prim__sub_Integer = [{arg:0}, {arg:1}]: (-Integer [!{arg:0}, !{arg:1}])
Main.main = [{ext:0}]: (Prelude.IO.prim__putStr ["HelloWorld\n", !{ext:0}])
Prelude.Types.prim__integerToNat = [{arg:0}]: (%case (<=Integer [0, !{arg:0}]) [(%constcase 0 0)] Just !{arg:0})
Prelude.EqOrd.compare = [{arg:0}, {arg:1}]: (%case (Prelude.EqOrd.< [!{arg:0}, !{arg:1}]) [(%constcase 1 0), (%constcase 0 (%case (Prelude.EqOrd.== [!{arg:0}, !{arg:1}]) [(%constcase 1 1), (%constcase 0 2)] Nothing))] Nothing)
Prelude.EqOrd.== = [{arg:0}, {arg:1}]: (%case (==Integer [!{arg:0}, !{arg:1}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd.< = [{arg:0}, {arg:1}]: (%case (<Integer [!{arg:0}, !{arg:1}]) [(%constcase 0 0)] Just 1)
Prelude.EqOrd.compareInteger = [{ext:0}, {ext:1}]: (Prelude.EqOrd.compare [!{ext:0}, !{ext:1}])
Prelude.IO.prim__putStr = Foreign call ["C:idris2_putStr, libidris2_support, idris_support.h", "node:lambda:x=>process.stdout.write(x)", "browser:lambda:x=>console.log(x)"] [String, %World] -> IORes Unit
PrimIO.unsafePerformIO = [{arg:1}]: (PrimIO.unsafeCreateWorld [(%lam w (%let {eff:0} (!{arg:1} [!w]) !{eff:0}))])
PrimIO.unsafeCreateWorld = [{arg:1}]: (!{arg:1} [%MkWorld])

[eayus]

After some digging, it seems these names are generated from the code that deals with the so-called "Nat hack".

https://github.com/idris-lang/Idris2/blob/3e24119f0caa999f0a49b833b9ed9e576694f4ba/src/Compiler/Common.idr#L323C1-L323C75

Seems plausible that these names could be included only if the user actually uses the corresponding function on Nat.

[gallais]

Definitely a low priority thing given most realistic programs will probably involve Nats.