Replacement Rule not applying "in time"

So, the problem seems to be that the particular rule (an inequation replacement rule) doesn't apply when you expect it. The issue here is that the order, in which rules are applied, is not specified by the semantics of type inference engine, and there are reasons for that. But there might be a way to solve your problem if you do away with type inference where it’s enough to check the constraints.

Here’s what is happening, as I see it, when your problematic code is analysed.

First, parameters X and Y are processed, which adds inequalities s <= Top and r <= s. Then an inequality involving two function types is added. This system of inequalities is then solved for variables s and r, and only then “replacement rules” are processed. I assume this is in accordance with your observations as well.

But what if there were no inequalities involving s and r in the first place? What is the reason for the constraints on type parameters to be used in type inference? Isn’t it enough if these constraints are only “checked”? So, instead of adding an “infer” type inequation you could add a “when concrete” block and *check* if the types are correct.

I hope this helps.

Thanks for your reply!

In our case, we actually do perform a lot of inference. For example, given the following program:

/*
  NOTE: The following is a property of our language, not of this program. I wanted to state it for clarity.
 *typedef number = real
 *typedef integer = natural
 *integer :<=: number
 */

function foo(a: Set<SomeClass>): integer = {
  let val = sum(a, (it) => it.getSomeIntegerValue())
  return val + 5
}

function <A extends AnyClass, B extends number> sum(set: Set<A>, sumFunc: (A) => B) : B = set.fold(0, (it, accum) => accum + sumFunc.invoke(it))

There is a lot of inference happening to make foo such a simple function.

• "let val" - variable types are inferred based on their right-hand-side. Also, in some cases, they are inferred based on their usage. This example doesn't necessarily reflect that use case, but I could come up with an example of such.
• "sum(...)" - There is a *lot* of inference happening here. The type parameters A and B are inferred based on the arguments passed to sum. Additionally, this is where a rule comparing the lambda's function type to the function's expected parameter type is added.
• "(it) => it.getSomeIntegerValue()" - The lambda's type is not known at declaration time, it is effectively "(tv1) => tv2" (tv = type var). The type of "it" is inferred based on the context in which the lambda is used. The concrete typevar of A is eventually bound to `SomeClass` for this invocation. Additionally, the function's return type is inferred based on the type of its body.

In many other cases, this works exactly as expected. We are thorough about adding inference rules where necessary, and we are comfortable with the fact that there may be *some* user programs that have indeterminate type. Those will likely be very rare, and there are always options to provide static types to assist the type engine.

However, this fails in some situations when the Function <: Function comparison does not invoke the replacement rule before other assumptions have been made.

Given our typesystem, we avoid `when concrete` whenever possible as it prevents inference from working properly. We haven't been able to successfully replace Operator types with inference yet, but I have some ideas around using meet/join types to turn overloads into inference rules. In those few cases, however, using user-defined types solves the problem (and is acceptable). We had previously used a shallow when-concrete to facilitate function type comparison, though this was replaced in favor of the replacement rule as that when-concrete would've needed to be present for *any* inference that could have contained function types.

May I inquire why is my suggestion to replace inference with checking on already calculated types does not work for you?

Also, when it comes to higher order functions, one has to be very careful in order to not make the typesystem undecidable. I'm afraid the inference rules for your language can be broken fundamentally, as I couldn't not re-create a working sample with this logic in either Kotlin or Java 8, both of which have very strong type inference. 

As to the original issue, there is very little we can do at the moment, save for rewriting the inference engine with new semantics, which would likely break compatibility with all the typing rules written so far by all of our clients.