Untyped Scheme should be built on Typed Scheme? WAS: Re:[plt-scheme] macro question

In a truly functional language, there are procedures (or functions) that 
cannot even be proven to halt, let alone to halt with what kind of value. 
Although rather expensive in terms of processor cycles, PLT's contract 
system provides an acceptible compromise  (at least in theory). I guess that 
a typed scheme (whether being the root or the target of an untyped scheme 
does not concern me) I think a typed scheme should be implemented such as to 
admit that it cannot in all cases infer the types of the values produced by 
functions/procedures. I am not an expert in this area, but I guess that 
building a fully safe typed functional language is like bypassing the 
halting problem.
Jos