[MLton] it is necessary to manually make things tail-recursive?

[Michael Norrish]

Lots of HOL code traverses logic-terms in a resolutely
non-tail-recursive manner.  We were bitten by this recently when a
user created a list (in the logic) containing 150k elements.  This
created a very large, and very skewed tree, and we got lots of
stack-explosions.  

(Terms are basically binary trees with internal nodes representing
function application.  So a h::t list is represented as 

  APP(APP CONS h) t

So the tree is as deep as the list is long.)

Moscow ML doesn't handle this well (gives an exception rather than
seg-faulting though :-), and I manually rewrote the exploding bits of
source to be tail-recursive.  

But for these large-scale applications, I eventually want to give
people a HOL implemented in MLton.  So, I was wondering if, for this
sort of thing at least, MLton is one of those magical compilers that
sees the potential problems with user code and knows that it should
make it into an equivalent tail-recursive or CPS form...

If so, I can avoid rewriting everything in HOL to be tail-recursive
and just rest safe in the knowledge that when I port to MLton all that
code will be OK anyway.  

Michael.