unicode string-length measuring in ATS

uni_stringlen.dats

fun string_length {n:nat}
	(str: string n): size_t n = let
	fun loop {i:nat | i <= n}
		(str: string n, i: size_t i): size_t (n) =
		if string_isnot_at_end (str, i) then loop (str, i+1) else i
in
	loop (str, 0)
end

implement main () = begin
	print( string_length("foo") );
	print( string_length("bar") );
	print( string_length("€") );
	print_newline();
end

(*
rsimoes@desktop:~/scratch/ats$ atscc uni_stringlen.dats 
/usr/lib/ats-anairiats-0.2.5/bin/atsopt --output uni_stringlen_dats.c --dynamic uni_stringlen.dats
gcc -I/usr/lib/ats-anairiats-0.2.5/ -I/usr/lib/ats-anairiats-0.2.5/ccomp/runtime/ -L/usr/lib/ats-anairiats-0.2.5/ccomp/lib64/ /usr/lib/ats-anairiats-0.2.5/ccomp/runtime/ats_prelude.c uni_stringlen_dats.c -lats 
rsimoes@desktop:~/scratch/ats$ ./a.out 
333
*)