Retrieving strongly connected components without an additional pass

Algorithm W has difficulties with recursion due to parametric polymorphism. You can use fixed-point combinator and isolate strongly connected components from the call graph. Building up the call graph is an additional pass that has to traverse through the input.

Recursion with parametric polymorphism can be handled by creating a slack type variables for every variable in a strongly connected group of variables and passing that around instead of instantiating a type. When the inference finishes for a group, unify that variable with the result and generalize the slack type variables.

You can modify Tarjan's SCC algorithm to do this.

  1. Treat your inferencer as a depth-first traversal function.
  2. Number every variable you visit with a number that increases by order of visiting.
  3. Implement Tarjan as usual, except that if you find an object in a stack, create a slack type variable for it.
  4. When the algorithm produces a group, immeaditely generalize the type variables in that group.

You may find out that retrieving the call graph before doing the inference can turn out to be easier than doing this. So this is not something that'd be obviously better than the option it replaces.