Abstract unification problem regarding functions

[kevinresol]

class Main {
	static function main() {
		var value = 'foo';
		var f:Func<String> = (v:String) -> value = v; // String should be Unit
	}
}
abstract Func<T>(T->Unit) from T->Unit to T->Unit {
	@:from
	public static function fromFuncReturningSameType<T>(f:T->T):Func<T> {
		throw 'irrelevant';
	}
}
class Unit {}

Link: #8476

[kevinresol]

I guess that when the compiler tries to unify with the from clause, it encountered the said error but then somehow it fails to proceed to the other @:from casts

[back2dos]

For abstracts over functions top down inference always tries the underlying type. You can remove the from cast and get the same result (I've removed the arrow function, because that makes the behavior even more complicated):

class Test {
	static function main() {
		var value = 'foo';
		var f:Func<String> = function (v:String) return value = v; // String should be Unit
	}
}
abstract Func<T>(T->Unit) {
	@:from
	public static function fromFuncReturningSameType<T>(f:T->T):Func<T> {
		throw 'irrelevant';
	}
}
class Unit {}

This is somewhat related to #3525.

[kevinresol]

This is somewhat related to #3525.

and I just realized I have raised a very similar issue in #5857

[Simn]

This was originally implemented in 0c27980

At the very least we should not loop through the abstract if it has no from underlying. That would make @back2dos example work, but the original example here is a more general problem still.

[Simn]

This actually fixes both cases because top-down inference is only applied if there is exactly one from PLUS @:from.

This might cause some regressions if somebody relies on the inference against the underlying type situation, but I really consider this a bugfix either way.

[Simn]

Well... turns out stuff is failing. If I'm seeing this correctly, this comes from our Promise API:

abstract PromiseHandler<T, TOut>(T->Dynamic) // T->Dynamic, so the compiler always knows the type of the argument and can infer it for then/catch callbacks
	from T->Promise<TOut>
	from T->Thenable<TOut>
	from T->TOut
{}

[kevinresol]

Perhaps can we we have some sort of documentation to describe how these are expected to work? For example the following used to work but not in nightly

abstract Callback<T>(T->Void) from (T->Void) {
	// in nightly one has to comment out this @:from to make it compile
	@:from static function fromMany<A>(callbacks:Array<Callback<A>>):Callback<A>
		throw 0;
}

function main() {
	var cb:Callback<Foo> = foo -> trace(foo.value);
}

abstract Foo(Dynamic) {
	public var value(get, never):Int;
	inline function get_value() return 1;
}

[back2dos]

This actually fixes both cases because top-down inference is only applied if there is exactly one from PLUS @:from.

What? Why? I mean if there's a from, why would a @:from be needed? Especially if a @:from isn't even used in the presence of a compatible from: https://try.haxe.org/#b618C495

[back2dos]

I really consider this a bugfix either way.

As far as the part of inferring against the underlying type if there's no from is concerned, yeah, that was arguably a bug that needed fixing.

As for the rest, it's now really borked. I've even tried with from AND @:from and can't get things to work:

abstract Callback<T>(T->Void) from (T->Void) {
  @:from static function ofSingle<A>(cb:A->Void):Callback<A>
    return null;
  @:from static function fromMany<A>(callbacks:Array<Callback<A>>):Callback<A>
     throw 0;
}

function main() {
  var cb:Callback<String> = foo -> trace(foo.length);// compiles, but presumably because `{ length: Unknown<?> }` unifies with `String`
  var cb:Callback<Foo> = foo -> trace(foo.value);// fails, because  (foo : { value : Unknown<0> }) -> Void should be Callback<Foo>
}

abstract Foo(Dynamic) {
  public var value(get, never):Int;
  inline function get_value() return 1;
}

This breaks tink_core irreparably. Quite possibly other things, but I didn't get to check, because nothing compiles anymore :D

[Simn]

What? Why? I mean if there's a from, why would a @:from be needed? Especially if a @:from isn't even used in the presence of a compatible from

Well, this is how our top-down inference with regards to abstracts has always worked. But I agree that we're now having problems.

The thing with top-down inference is that we don't know about the "presence of a compatible from" until after typing, and then it might be too late. That's why we only apply it if there's exactly one from + @:from, because only then it is unambiguous.

But clearly we have to be more clever here.

[back2dos]

Well, this is how our top-down inference with regards to abstracts has always worked.

Hmm, not really. As far as I can tell, it relied on the underlying type. Which in general violates the abstraction. But not when there's a from for the underlying type.

What I don't get is how the current solution is even supposed to work. If there's only a from, it works. If there's the same @:from too, then it works too, but it is never executed, so it may as well not be there. If there's another @:from, the cast won't work.

Now, I think the simplest solution is to use any from types for top down inference (of which there's usually just one). Or if that's too messy, let's say if there's exactly one from type, then that should be used for top down inference. Any @:from should be ignored (since it won't execute anyway).

The thing with top-down inference is that we don't know about the "presence of a compatible from" until after typing.

Yes and no. Years ago I suggested syntax should be taken into account, which you were opposed to for unmemorable reasons.

Here's my thinking: If the expected type is an abstract and the expression is an EFunction, that information should be leveraged to narrow candidates to casts for function types. I would even go as far as considering arity for selection, e.g. if there's a trinary function expression and exactly one implicit cast from a trinary function type, that makes for a really good candidate for top down inference. There are some things to consider, like how to produce the most meaningful error when the available casts are unary and trinary function types and the provided expression is a binary function (although sticking to (X, Y)->Z should be SomeAbstract would definitely not be a degradation of current behavior).

Selecting by syntax could also be applicable for EObjectDecl and EArrayDecl. And even EConst(CIdent)) and ECall(EConst(CIdent))) if there's are @:from casts for enums (you really don't need to type the expression to check the ident against any of the potential enums). I'm not saying all of these are necessarily good ideas, but I think it's a line of thought that is worth considering. Perhaps at another time though. For now using a singular from for top down inference will do the trick ;)

[Simn]

See if that helped. I had actually implemented what you're describing, but it was cancelling everything upon encountering a non-function type. Now that I think about it, that doesn't make any sense.

[back2dos]

Hmm. The debate got spread out a bit. I'll try to bring it all together here, at the risk of being repetitive, lengthy and stating the obvious.

So what's currently wrong (up to 4.2.5)? In the words of Simn:

always inferring through the underlying type of an abstract breaks the abstraction.

There's no arguing about that. If the author of an abstract decides to change the underlying type, no code should be affected.

However, there's something quite strongly related to the underlying type, which are any from clauses. Any from clause establishes a direct and explicit type relationship as part of the abstraction:

class Test {
  static function main() {
    var i1:Iterable<String->Void> = [];
    var i2:Iterable<TransparentFoo> = i1;// just fine
    var i3:Iterable<OpaqueFoo> = i1;// String -> Void should be OpaqueFoo
  }
}
abstract TransparentFoo(String->Void) from String->Void {} 
abstract OpaqueFoo(String->Void) {
  @:from static function ofFunction(f:String->Void)
    return (cast f:OpaqueFoo);
}

Even though most of the time the underlying type and the from type are the same, this is not at all necessary (e.g. in the example above the underlying type could as well be Dynamic). While the compiler enforces a relationship between the underlying type and types in from clauses, that relationship is not part of the abstraction. What's really important is from.

The type system assigns a very strong meaning to from. Type inference should not ignore it. It should also not treat it as an equal of @:from casts, because in the type system the two are not equals either. But that's where we currently seem to be.

I guess there are two questions:

1. Should top down inference consider from clauses? If there is one, then I say definitely, due to the reasons outlined above. If there are multiple, then maybe. I'd say it should pick the first that matches the expression syntax.
2. Should top down inference consider @:from casts? Ideally, yes. But I think the situation we're in right now makes it clear that this is not so easily accomplished. I'd rather not consider them than have the situation we have right now: if the compiler sees an applicable from and @:from it treats this as an unresolvable ambiguity and bails out of top down inference altogether. I think that's just wrong. A possible solution would be to ignore @:from in the presence of an applicable from. Or infer against the first applicable from/@:from (kinda like implicit casts work anyway) where from has highest priority. Or maybe something smarter still.

---

To circle back to the issue that sparked this, I would say that it should infer against Unknown->Unit as follows from the from clause. The code can still be made to work, simply by turning Unit into an abstract that has an implicit cast from anything. Which kinda makes sense for a Unit type: if you typedef Unit = Void; the above code works fine too.

[Simn]

Thank you for the summary, this is quite helpful!

Just a quick note because I don't have time right now: One particular problem with your idea is that small "applicable from" part. We don't necessarily know if there's an applicable from until we know the type of the expression. There could be cases where using the from for top-down inference would change typing in a way that then makes a @:from cast not unify, even though it would unify if we had just typed the expression without top-down inference. I don't remember where exactly that came up, but I can try changing the compiler like that and see if there's a test that breaks.

[back2dos]

We don't necessarily know if there's an applicable from until we know the type of the expression

Well, I'm really thinking pure syntax here. In the case of functions perhaps even arity, as detailed in a previous comment.

There could be cases where using the from for top-down inference would change typing in a way that then makes a @:from cast not unify,

But until now such behavior was not supported in an official release. If you have a from it's probably the underlying type anyway and up until now things were top-down inferred against that.

[Simn]

Well, I'm really thinking pure syntax here. In the case of functions perhaps even arity, as detailed in a #10336 (comment).

We're already dealing with that by considering arity. The remaining cases are the ones where the arity is equal. See #10604.

But until now such behavior was not supported in an official release. If you have a from it's probably the underlying type anyway and up until now things were top-down inferred against that.

That's not true, before e134a97 the compiler would simply always use the underlying type and not even look at any from relations. This is even what the original example in this issue is about.

[back2dos]

That's not true [...]

Hmm, there seems to be a misunderstanding. I think you're saying what I'm saying, but obviously you seem to think we're saying different things :D

Let's reiterate the problem you've raised:

There could be cases where using the from for top-down inference would change typing in a way that then makes a @:from cast not unify,

There are two ways to read that statement:

1. Users might write code which causes an expression to be top-down inferred due to from to a type that is not compatible with the expected abstract type, but would have been, if it were bottom-up inferred. As in the introductory example.
2. Users may already have written code which relies on top-down inference not being applied so that the bottom-up inferred expression may unify via @:from.

I've chosen the second interpretation of the statement, because breaking existing code is more concerning. And in that context I have pointed out that we've been inferring against the underlying type and so if there's a from the behavior would not change, while if there's none, code might break - as it should, because it was piercing an abstraction barrier.

As for the question whether in the future we may wish to make the above example compile - which is what this issue was originally about - I'm leaning towards not supporting it. But I'm not sure that's what we're discussing ^^

[Simn]

See #10604