UPDATE: My initial investigation on the bus this morning was incomplete and wrong. The text of the first phase specification is correct. The implementation is correct.
The spec is wrong in that it gets the order of events wrong in the second phase. We should be specifying that we make output type inferences before we fix the non-dependent parameters.
Man, this stuff is complicated. I have rewritten this section of the spec more times than I can remember.
I have seen this problem before, and I distinctly recall making revisions such that the incorrect term “type variable” was replaced everywhere with “type parameter”. (Type parameters are not storage locations whose contents can vary, so it makes no sense to call them variables.) I think at the same time I noted that the ordering was wrong. Probably what happened was we accidentally shipped an older version of the spec on the web. Many apologies.
I will work with Mads to get the spec updated to match the implementation. I think the correct wording of the second phase should go something like this:
- If no unfixed type parameters exist then type inference succeeds.
- Otherwise, if there exists one or more arguments Ei with
corresponding parameter type Ti such that
the output type of Ei with type Ti contains at least one unfixed
type parameter Xj, and
none of the input types of Ei with type Ti contains any unfixed
type parameter Xj,
then an output type inference is made from all such Ei to Ti.Whether or not the previous step actually made an inference, we
must now fix at least one type parameter, as follows:
- If there exists one or more type parameters Xi such that
Xi is unfixed, and
Xi has a non-empty set of bounds, and
Xi does not depend on any Xj
then each such Xi is fixed. If any fixing operation fails then
type inference fails.- Otherwise, if there exists one or more type parameters Xi such that
Xi is unfixed, and
Xi has a non-empty set of bounds, and
there is at least one type parameter Xj that depends on Xi
then each such Xi is fixed. If any fixing operation fails then
type inference fails.- Otherwise, we are unable to make progress and there are
unfixed parameters. Type inference fails.If type inference neither fails nor succeeds then the second phase is repeated.
The idea here is that we want to ensure that the algorithm never goes into an infinite loop. At every repetition of the second phase it either succeeds, fails, or makes progress. It cannot possibly loop more times than there are type parameters to fix to types.
Thanks for bringing this to my attention.