Allow hidden proof RHS lookups without forcing naive rules

[saulshanabrook]

Summary

• Carry FunctionDecl.internal_hidden onto FuncType so generated proof/term-encoding functions keep their hidden metadata after typechecking.
• Allow RHS lookup detection to ignore only internal-hidden generated custom-function lookups.
• Keep ordinary user-visible RHS function lookups rejected, with focused regression coverage for both cases.

Motivation

This is the mainline RHS lookup/typechecking slice motivated by eggcc proof-mode performance. In coordinator verification on 2026-06-24, forcing generated proof-action rules with RHS proof lookups to :naive made the eggcc 2mm proof-mode export run for about 589s before manual termination. Preserving seminaive execution on the composed stack completed the same 2mm proof run in about 18s.

This branch contains only the RHS lookup/typechecking slice. It does not include the container PR work, PR #930 changes, set validators, Maybe/Either support, eggcc changes, or experimental changes.

Tests

• cargo test -p egglog proofs::proof_tests::tests -- --nocapture
• cargo fmt --check
• git diff --check
• cargo test -p egglog --test files calc_proofs
• cargo test -p egglog --test files fail-typecheck/looking_up_nonconstructor_in_action_case_set

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 86.54%. Comparing base (7d102db) to head (99cb079).

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #931   +/-   ##
=======================================
  Coverage   86.54%   86.54%           
=======================================
  Files          89       89           
  Lines       26804    26810    +6     
=======================================
+ Hits        23197    23203    +6     
  Misses       3607     3607           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[saulshanabrook]

Closing as superseded by #912. I verified the downstream stack without this PR: container PR #927 merged with current main (including #912), plus the container follow-up, #928, #929, and #930, with no #931/internal_hidden changes. egglog-experimental and eggcc both built, the regenerated eggcc 2mm export was byte-identical to the prior export, and completed in real 15.56s.

[saulshanabrook]

Correction to the close comment: the verified command was /Users/saul/p/wt/egglog-experimental/eager-merge-primitives/target/release/egglog-experimental --proofs .tmp/2mm-no-931.egg, which completed in real 15.56s. The verification stack did not include PR #931/internal_hidden changes; it used PR #927 merged with current main/#912, plus the container follow-up, #928, #929, and #930.

[codspeed-hq]

Merging this PR will not alter performance

✅ 29 untouched benchmarks
⏩ 219 skipped benchmarks¹

---

_{Comparing saulshanabrook:codex/rhs-proof-action-lookups (99cb079) with main (7d102db)}

Footnotes

1. 219 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩