Hi Diego,

> My question is: Could this checking model be implemented using Scheme's macro system, instead of requiring a custom-built compiler pass?

Sample implementation is actually all portable syntax-rules. With some
quirks (like literal matching of identifiers that was discussed as
problematic elsewhere,) but overall it’s implementable.

Having underlying implementation do the type-checking is the preferred
way, and that’s what SRFI-253 does on Chicken and Kawa—delegating most
types to the compiler.

However, most of the checks on most implementations are run-time and not
compile-time.

> 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?

This is definitely possible! For check-arg and values-checked, at
least. For define-checked—not sure, because the checking is happening
later down the line and not at the moment of define-checked expansion.
But yeah, it’s possible—just not implemented yet.

> Are there other ways we could benefit from Racket's experience

There should be. I haven’t researched Racket’s side of typing much, but
things like dependent types and type variables are two things missing
from 253/273 that programmers might’ve benefited from.

So yeah, sorry if that’s an unsatisfactory answer: things are possible,
but no one got to that yet. I myself am focused on bringing 253/273 with
at least basic runtime checking to as many implementations as possible
(help appreciated) and thus I didn’t yet explore things in depth on any
particular implementation beyond Chicken, Kawa, Chibi, and maybe STklos.

Best of luck,
--
Artyom Bologov
https://aartaka.me