Could horizontal type inference handle this situation?

[eernstg]

Consider the following program:

void f<X>(X x, X Function(X) g) {}

void main() {
  f(1, (_) => 1.5); // `<num>` works, but inference can't find that solution.
}

This program is rejected by the analyzer as well as the CFE because type inference fails to find an actual type argument to the invocation of f that satisfies the constraints.

With f<num>(1, (_) => 1.5) is accepted with no issues, and <num> does indeed yield parameter types such that the expression has no errors (1 can be typed as num immediately, and (_) => 1.5 can be inferred to have parameter type num and return type num).

I believe horizontal type inference causes x in the first example to be processed in a first phase, thus determining the value of X without consideration of anything else than x and the actual argument 1, yielding X == int.

In the next phase, type inference can't find a way to annotate the function literal (_) => 1.5 with a parameter type and return type such that it gets the type int Function(int) or a subtype thereof, and inference fails.

As we'd expect, the following variant has no issues (because it doesn't cause horizontal type inference to kick in), and the type argument is inferred as num:

void f<X>(X x, X Function() g) {}

void main() {
  f(1, () => 1.5); // OK, uses `<num>`.
}

It is not obvious to me how we could improve on this situation. One random idea is that we might be able to generate a "global" constraint (before splitting arguments into phases) that double <: X <: _, based on the returned expression of the function literal. But that also seems like a very long shot, e.g., because it may require input from many sources to find the type of a return expression in a function literal.

[lrhn]

It's going to be very hard to do anything better here, and still only type-analyze each expression only once.

Short of assigning each expression an abstract type, gathering constraints, and then solving all the constraints in one go, but I don't think that will work with how context type can affect semantics of expressions. We don't know the constraints until we know the concrete context type. The moment we know the concrete context type, some type choices have already been made.