>  Given that R7RS Large is developing powerful macro facilities (
procedural macros ) , I wonder whether the checking in SRFI-273 could be
performed at macro-expansion time. Could lambda-checked,
declare-checked, and the other forms be implemented as macros that
verify types during expansion?

One thing that Racket has that R7RS Large doesn't is #%app. This has
compatibility issues and some composability issues ([1] and [2] for the
very long WG2 discussion). This means that one cannot add a custom macro
transformer for a bare procedure application, so one cannot type-check a
procedure application.

Capy[3] and Gerbil[4] support #%app to some extent, and Capy supports
most of the R7RS Large macro system.

[1]: https://codeberg.org/scheme/r7rs/issues/86
[2]: https://codeberg.org/scheme/r7rs/issues/244
[3]:
https://codeberg.org/playXE/capy/src/branch/stage/lib/boot/psyntax.scm#L42
[4]: Sadly their website is down. I don't know if it is still being
actively developed anymore.

-- Peter McGoron