[plt-scheme] The perfect teaching language--Is this too much to ask for?

I'm starting to get really frustrated, because there are lots of
languages that have some of what I want in a beginning language, but
nothing that has everything. I'm beginning to worry that I'm going to
have to design my own language--worry because I have neither the time
nor background to do a good job of it. Here's what I'm looking for and
I'm beginning to be afraid that the intersection of this set is empty,
not just because no one's thought to do it, but because I'm
convoluting language layers in an impossible way.

Here are my desiderata for a language to teach introductory
programming, through at least data structures:

-------------------------

1. Language Levels
The PLT/HtDP people are the only group I've seen who realize how
important this is, especially with sufficiently powerful languages,
and after seeing how useful it is for my students, I wouldn't trade
the idea for anything. Giving students access to only the stuff they
understand and tailoring error messages for the kinds of programs that
they should be writing is just too useful. This, of course, leaves out
every language but Scheme and Java as implemented in the HtDP and HtDC
language levels.

2. Types in the Language
Here's a sample Python interaction:
(For the uninitiated, >>> is the Python REPL prompt, the next line is
the result.)

>>> int
<type 'int'>
>>> type(int)
<type 'type'>
>>> type(3)
<type 'int'>
>>> isinstance(3, int)
True
>>> isinstance(3, float)
False
>>> class Foo:
...     pass
...
>>> Foo
<class __main__.Foo at 0xb7db262c>
>>> x = Foo()
>>> isinstance(x, Foo)
True
>>> type(isinstance)
<type 'builtin_function_or_method'>

OK, the last line is not particularly useful, but every Python value
knows what it is, these types are real objects in the language, and
programs can manipulate and ask questions about them.

The contract is the first step of the design recipe for a very good
reason--students need to think about what kinds of values a function
consumes and what kind(s) of value it should produce. The problem is
that, in HtDP, contracts are just comments, and students figure this
out very quickly. I want types to impact students' programming,
because a huge proportion of the mistakes my students make have to do
with muddy thinking about types, and I think the programming
environment should make them be explicit about what they think is
going on and help them when they're wrong. Too many type-caused errors
don't get caught until several layers of redirection, leaving students
with stack traces that are, if not hard to follow, at least
intimidating. Even if Typed Scheme were all done and perfect, it
wouldn't provide this kind of support, mostly because that's not what
it's designed to do.

3. Static Typing
Yea for Python--I can play with types in the language. Boo for
Python--I can only find typing problems once I let the program run and
only if I happen to create a type problem. A program could be
completely brittle in terms of types and I'd never realize it. This is
exactly what statically-typed languages are designed to prevent, and
what Typed Scheme seems to be doing a really good job of.
(Unfortunately, I'm discovering just how many unfounded assumptions
about types I make as I'm writing in Typed Scheme, but I'm sure it's
on a par with how many unfounded assumptions I make in general.) I
want a language that screams bloody murder if the pieces don't fit
together right, even if some lazy student hasn't provided test cases
that trigger a problem.

-----------------------

There are lots of others--easily grokked syntax, a REPL, good
libraries that let students explore stuff if they want to, etc.--but I
think these three meet a need that I feel somewhere deep inside my
innermost being. (You know, the place where butterflies and rainbows
live...)

So, are two and three mutually incompatible? Does the ability to
define new types, to write functions on types, to create new types
programmatically make it impossible to do static type checking, even
if you force the programmer to declare types? If so, does it make it
impossible generally, but still make it possible to write the kinds of
programs that first-year students should write or is it just
impossible for any useful subset of languages?

I hesitate to ask this, given an audience of people who really like at
least one dynamically-typed language, but am I just assigning too much
importance to static/declared types? Should I stop worshipping at the
altar of types and realize that, even if my students could get their
types checked by the language, the ones with muddy thinking would just
transfer the scene of their confusion to some other step in the design
process?

School ended a week ago, and I'm trying to plan out next year. I get
philosophical at this point every year and start re-questioning all my
assumptions. I thought Typed Scheme would be a way to get types into
my intro class, but then I realized it tackles 3 really well, but not
2. What I'd really like to be able to do in Beginning Student Scheme
is something like:

> N
N
> (type-of 3)
N
> (type-of -4)
Integer
> (is-of-type 3 Integer)
true
> (type N)
Type
> (U N Integer)
Integer
> (U true false)
Boolean

and then be able to use these types--and others that students could
define--to statically type programs in the vein of Typed Scheme.

So, back to the subject line: Is this too much to ask for?

Todd