On Sun, Jan 22, 2006 at 01:23:49PM +0100, Andrej Bauer wrote:
> There may be special cases where compiler can determine whether the
> index is ok. 
> [...]
> I am sure
> people have looked into this sort of thing. Good luck!

Yes.  One might be interested in Dependent ML, or the references at the bottom
of the page.

http://www.cs.bu.edu/~hwxi/DML/DML.html

- Kenn