What is a type error?

[Joachim Durchholz]

Marshall schrieb:
> David Hopwood wrote:
>> This property is, after all, not something that the program should depend on.
>> It is determined by how good the static checker currently is, and we want to be
>> able to improve checkers (and perhaps even allow them to regress slightly in
>> order to simplify them) without changing programs.
> 
> Hmmm. I have heard that argument before and I'm conflicted.

I'd want several things.

A way for me to indicate what assertions must be proven statically.
Highlighting (be it compiler messages or flashing colors in an IDE) that 
marks assertions that *will* break.
And highlighting for assertions that *may* break.
In the language, a (possibly) simplicistic inference engine definition 
that gives me minimum guarantees about the things that it will be able 
to prove; if something is out of the reach of the engine, a 
straightforward way to add intermediate assertions until the inference 
succeeds.

(Plus diagnostics that tell me where the actual error may be, whether 
it's a bug in the code or an omission in the assertions. That's probably 
the hardest part of it all.)

Regards,
Jo