Spurious hint about inferred type argument `dynamic` using strict-inference?

[eernstg]

Cf. https://github.com/dart-lang/sdk/issues/50390. Consider the following program:

class MyClass<A> {}

void myFunction<A, B extends MyClass<A>>(B instance) {
  print('A: $A, B: $B'); // 'dynamic, MyClass<double>'.
}

void main() => myFunction(MyClass<double>());

When analysis_options.yaml contains the following:

analyzer:
  language:
    strict-inference: true

the analyzer (from commit c387068e00bdb6411a1c6e20d62b2ec046b5c499) reports the following hint:

Analyzing n004.dart...                 2.1s

   info • n004.dart:6:16 • The type argument(s) of the function 'myFunction'
          can't be inferred. Use explicit type argument(s) for 'myFunction'.
          • inference_failure_on_function_invocation

1 issue found.

Actually, the program runs and prints dynamic, MyClass<double>, and I believe this choice of actual type arguments is a solution to the given constraints. In other words, it looks like the 'strict-inference' behavior includes reporting some situations where inference did succeed, and something else was true (e.g., one of the inferred parameters is a top type).

Is it the intention that this program should give rise to that hint? It would seem more reasonable to me if that hint were only emitted in a situation where type inference actually failed (perhaps in the sense that one or more type arguments got the value dynamic and this choice gave rise to a dynamic type check at some point in the execution of the enclosing expression).

[bwilkerson]

@srawlins Because you might have more context about strict-inference.

[srawlins]

some situations where inference did succeed, and something else was true (e.g., one of the inferred parameters is a top type).

Is it the intention that this program should give rise to that hint?

I think so. I certainly understand that "inference failure" is a very loose, vague, and probably wrong term for this. The docs say:

when there is not enough information available to infer an expression's type, where inference "falls back" to dynamic (or the type's bound), inference is considered to have failed, and an analyzer "Hint" is reported at the location of the expression. The expression is said to contain an "inference failure."

[eernstg]

[Oops, edit: The second example does give rise to the same hint about a failing inference. Adjusted the text below.]

where inference "falls back" to dynamic (or the type's bound), inference is considered to have failed

But I can't see any "falling back" here. Can we actually say that inference has failed in a situation where all constraints have been satisfied?

In the example, myFunction(MyClass<double>()) is inferred as myFunction<dynamic, MyClass<double>>(MyClass<double>()). The type parameter bound is satisfied (MyClass<double> <: MyClass<dynamic>), and the actual argument type is assignable to the inferred type of the parameter (both are MyClass<double>). No downcasts from dynamic were added as a consequence of inference.

So I'm just wondering whether the logic that makes the decision "this inference has failed" has a bug.

Here is another case where all constraints are satisfied by the inferred type argument (there are no constraints), there is no information to constrain the type variable, and the inferred type argument is dynamic:

class A<X> {
  A() { print(X); }
}

void main() {
  A(); // Inferred as `A<dynamic>()`, also reports that the inference failed.
}

It is again surprising to me that this example causes the 'can't be inferred' hint (because nothing failed). Here's another variant:

class A<X extends Object?> {
  A() { print(X); }
}

void main() {
  A(); // Inferred as `A<Object?>()`, no problems.
}

This seems to imply that inference may proceed, it may satisfy all constraints and produce an expression that does not have any casts-from-dynamic-caused-by-inference, it may have some type variables for which the expression and its context type do not produce any constraints, and yet there's something else that determines whether inference is considered to have failed or not.

Perhaps the inference is considered failing if and only if the actual type arguments added by inference do not include one whose value is dynamic?

In that case it might be useful to update that documentation. ;-)

[srawlins]

Here is another case where all constraints are satisfied by the inferred type argument (there are no constraints), there is no information to constrain the type variable, and the inferred type argument is dynamic:

This is intentional. This mode does not concern itself with constraints being satisfied or not.

Perhaps the inference is considered failing if and only if the actual type arguments added by inference do not include one whose value is dynamic?

I think that is the case. I intend for it catch when there is a bound other than dynamic is specified, but I think that is not implemented yet.

In that case it might be useful to update that documentation. ;-)

I don't think so. The docs for instance creation say:

Instantiating a generic class without explicit type argument(s), in which one or more type arguments cannot be inferred from downwards or upwards inference is considered an inference failure. This includes type parameters with an explicit bound.

So there is a bug in the implementation. In your class A<X extends Object?> example, a failure should be reported.

If you take issue with the word "failure," I'm happy to use another word.

[eernstg]

It sounds like the 'strict-inference' check has nothing to do with inference failure at all, it's checking whether or not each type variable has a constraint which is derived from some other source than the declared bound: Iff there is no constraint on a given type variable X, then inference for X is considered as evidence that this was not a successful 'strict-inference'. It doesn't matter that there are no errors, no failures of any kind, we just want to flag the situation where there were no constraints.

Sorry about pushing on this several times, but I can't help asking: Why would anyone want to flag that situation as problematic?

[srawlins]

It doesn't matter that there are no errors, no failures of any kind, we just want to flag the situation where there were no constraints.

Yeah that's fair. Maybe "unconstrained inference" is a better name.

Sorry about pushing on this several times, but I can't help asking: Why would anyone want to flag that situation as problematic?

There are motivations in the doc. The general idea is that users don't know that they've just constructed an object of type dynamic or perhaps C<dynamic> or perhaps List<dynamic> and 99.9% of the time, they don't want dynamic. And choosing dynamic can mask other static analysis issues below, since dynamic has fields and methods for every possible name.

[eernstg]

@srawlins wrote:

There are motivations in the doc

I read the whole thing in order to understand this better. I noted some parts in need of updates, so I'll just mention them here:

In section 'Motivation':

It is possible to write Dart code that passes all static analysis and compile-time checks that is guaranteed to result in runtime errors. ... The strict inference mode aims to highlight such code during static analysis

This seems to imply that it is a false positive when a location in code is flagged, and there is no justification to claim that any run-time error can occur, let alone will occur (of course, errors like out-of-memory are always possible).

Presumably this should be reworded such that it says nothing about run-time errors. It could then say that 'strict-inference' flags locations in code where an inferred type was chosen to be a default value.

Details: 'Default value' is very vague, but a more precise definition is somewhat verbose. More precisely, the inferred type was chosen based on an empty set of local constraints. And then we may need to define a few other things:

An inferred type can be an actual type argument in an instance creation, an invocation of a generic function, an actual type argument in a collection literal, the type of a formal parameter, or a return type.

The local constraints are the ones that arise from the analysis of the entity which is subject to type inference, that is, an expression, or a function declaration or function literal where some type annotations have been omitted. So, in the case of an actual type argument to an invocation of a generic function: we may have found and satisfied a constraint which is a bound on the corresponding type variable declaration, or we might use a top type because there is no constraint at all on the given type variable, but we did not encounter any constraints on the given type variable during the traversal of the function call.

In 'Example: under-constrained list literals' we have a bit of obsolete text:

the last line will result in a runtime error

This is not true today, there will be a compile-time error at fn(numbers) because the static type of numbers is List<dynamic>, which is not assignable to List<int>. Here is the same issue once more:

Static analysis allows a List<dynamic> argument for a List<int>, as an implicit cast.

The section about inference of invocations of List.fold needs to be updated: The new feature known as 'horizontal inference' makes everything in there obsolete.

In section 'Instance creation' there is yet a tiny thing which is obsolete:

var l = List();

This constructor is not available today. We should probably just delete that line.

@srawlins wrote:

Maybe "unconstrained inference" is a better name.

Definitely! And if it isn't possible to rename the feature then it would still be helpful if those references to run-time errors were removed from the documentation.