An inferred actual type argument should be a denotable type

[eernstg]

This issue proposes a principle which we could use as a guideline when decisions must be made about how to perform type inference. I believe that we are mostly following this guideline already, but see below for some 'interesting' cases.

Principle: If type inference transforms an expression e₁ by adding some actual type arguments T₁ .. T_k, yielding the expression e₂, then it must be true for each j in 1 .. k that there exists syntax which denotes T_j in the given scope.

The point is that it would be useful to have a clear limit on the expressive power of type inference of the form "you could have written it yourself", which helps keeping programs comprehensible, and helps us avoid situations where we have to say to developers "you must convince type inference to give you that type argument, because there is no way you could write it explicitly".

A similar principle would apply to the type of a variable when it is inferred, and the type of a formal parameter (of a function literal based on the context type, or of an instance member declaration which is receiving some type annotations in its signature from type inference, based on declarations that it overrides):

Principle: The type of a variable or parameter and the return type of a function must be denotable in the given scope, also when it is inferred.

We have some immediate issues:

• Generic function instantiation will pass type arguments to a generic function F, thus yielding a non-generic function whose type is a generic instantiation of the type of F. Problem: We do not have the syntactic support to pass those type arguments at all (f<int> is not an expression). Solution: We might be able to add support for this syntax, and we have already considered that for a while; so this issue may not be so serious.

• But privacy may be harder. Consider the following example, which shows that we already support giving a variable an inferred type that we cannot denote:

// Library lib.dart.
class A { foo() { print("foo"); } }
class _B extends A { bar() { print("bar"); } }
_B f() => _B();

// Library main.
import 'lib.dart';

main() {
  var x = f();
  x.foo(); 
  x.bar(); 
}

• The same treatment is given in a case where the type is reified, namely for function literal parameters:

// Library lib.dart.
class A { foo() { print("foo"); } }
class _B extends A { bar() { print("bar"); } }

void f(void Function(_B) g) {
  print(g.runtimeType); // Shows parameter type `_B`.
  g(_B());
}

// Library main.
import 'lib.dart';

main() {
  f((b) { b.foo(); b.bar(); });
}

• Considering an example like https://github.com/dart-lang/sdk/issues/36096, we probably want to specify that inference can pass a type argument which is not statically safe (example: passing num as the type argument to printT in t2.printT(), even though the bound is only known to be some subtype of num). So this is probably a non-problem, because we will pass num or make it an error, and those solutions will satisfy the principle that I'm proposing here. The derived principle (a special case of the main principle proposed here) would be that it is allowed for inference to provide certain type arguments which are not statically safe, namely in the case where the actual bound cannot be denoted, and neither can any of its useful (non-Null) subtypes. (Developers would, presumably, be able to add invariance to various parts of their typing, such that these situations do not occur any more, or at least only rarely.)

We might end up deciding that the principles must be weakened to allow for private types; or we might decide that the principles are useful, and the private types must be eliminated as inference results (possibly with a long transition period where they are only frowned upon, or possibly by approximating the private types from from above or below by public types, etc).

[munificent]

Even without private types, you can get into situations where inference may produce a type you can't write in the current scope:

// a.dart
class A {}

// b.dart
import 'a.dart';
A makeAnA() => A();

// my_app.dart
import 'b.dart';

main() {
  var a = makeAnA();
}

Here, there is no annotation you can write instead of var unless you also add an import. I think code like this feels very natural to Dart users (and users of other languages). Private types are a slightly harder one because then there isn't a library you can import, but I think it still roughly "feels the same" for most users — there is a type that could be written, you just can't write it here.

So I think the principle is too restrictive. I would rephrase it that every type created by inference should be denotable somewhere in the program. So a private or un-imported type is OK because you could denote it in that other library. But if, say, inference produced an intersection type and we don't add & type syntax, then the principle is violated.

[eernstg]

@munificent wrote:

you can get into situations where inference may produce a type you can't write

Right, I forgot to mention that, thanks!

every type created by inference should be denotable somewhere in the program

Agreed, that's certainly a point in the design space that we should keep in mind.

Still, I tend to think that the use of a private type from another library as the type of a variable/parameter is more of an encapsulation violation than the use of a public type that you can only reach if you traverse two imports.

We could simply say "any type which is denotable in the given scope, or which would be denotable with the addition of an import".

But if, say, inference produced an intersection type and we don't add & type syntax, then the principle is violated

That's one case that we actually have already:

void foo<X extends num>(X x) {
  if (x is int) {
    var y = x;
    print(y.isEven); // OK.
    X z = y; // OK.
  }
}

main() => foo(42);

The above example compiles and runs with no error, which shows that the variable y is given a type which is a non-Null/non-bottom subtype of int (which enables .isEven), and assignable to X (such that it can initialize z). Only the type X & int has those properties, and this implies that y has an inferred type that we cannot denote.