I'm a bit unclear on one part of your proposal: is the type
declaration syntax merely a suggestion to the compiler, or does it
actually affect the semantics of a program?  That is, if I specify
that an expression's value is an IEEE double-precision flonum, do
arithmetic operations in that context 'become' IEEE 64-bit flonum
operations, with roundoff &c. as specified by IEEE, or may the system
actually do something else?  Would this be the case with the integer
declarations and n-bit modular arithmetic as well?

While type declarations are useful (though I *abhor* the :: syntax),
limiting declarations solely to types, I think, is not, and they do
not usefully subsume semantic distinctions, which may go deeper than
simply coercing values here & there, and which should be provided in
the form of different procedures with different semantics; e.g., the
(MODULAR-ADDER n) &c. procedures I suggested earlier.  Declarations
are useful to have, such as (DECLARE ARRAY-INDEX FOO BAR-ARRAY), but
I think they are really out of the scope of this SRFI.