Type inference for mutually recursive functions is actually quite a bit more complicated than you would think. For example, while thinking through how to implement mutually recursive functions in InforML, I came across something that I was confused about and wondered how we had handled it in AspectML. I spent some time meditating on the AspectML source and found that it didn't really address the issue. In particular, you can naïvely write

% fun f <a:*>(x : a) = 5
> and g <b:*>(y : b) = f y;

which you would think would be two functions »f« and »g« that given anything return 5. However, these functions are not accepted by the type checker

InferenceProcess Error: Error between [interactive]:0.2-[interactive]:1.22
Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
Non-unifiable type variables: b and a
while trying to unify types b and a
while checking that b is subsumed by a
inside (f y)
inside fun f <(a : *)>((x : a))  = 5 and g <(b : *)>((y : b))  = (f y)

The problem is that AspectML rightful decided that »f« could not be used recursively at a polymorphic type, because it didn't initially know the return type. However, this becomes a problem because the type variable a isn't actually in-scope inside of »g«, that is »f« has an invalid type in a sense that should be a »compiler« error, as is illustrated by this slightly more complex example

% fun f <a>(x : a) = 5
> and g <b>(f : b -> Int) : Int = 5
> and h y = g f;
fun f <(a : *)>((x : a)) : Int = 5
and g <(b : *)>((f : ((-> b) Int))) : Int = 5
and h <(b5933 : *)>(y) : Int = (g f)
TranslateProcess Error: Error between [interactive]:1.1-[interactive]:3.13
Error between frontend/to-source.sml:170.78-frontend/to-source.sml:170.85
Error between frontend/to-source.sml:607.85-frontend/to-source.sml:607.92
toTyp: Could not find type variable a. This should be impossible!
%

Of course, diagnosing the problem is the easy part. The difficult part will be figuring out which of the many possible fixes makes the most sense for InforML.