Compile time error is missing (opted out of null safety) or confusing (opted in to null safety) for generic type inference

[nshahan]

Updated to correct my description of the null safety modes.

NOTE: These are simplified reproductions from a real world issue with a missing compile time error and subsequent runtime error that appeared in a google3 application.

Consider:

class A {}

T fn<T extends A>(T x) => x;

void main() {
  var s = 'hello';
  s = fn(s);
}

With weak null safety When the file is opted out of null safety there is no compile time error (analyzer or CFE) and various errors at runtime in all backends. It seems like this should be a compile time error because there is no way type String could ever be passed as the type argument <T extends A>.

In sound mode When the file is opted into null safety this produces the compile time error The argument type 'String' can't be assigned to the parameter type 'Never'. I find this message confusing, where did the Never come from?

In a related example:

class A {}

T fn<T extends A>(T x) => x;

void main() {
  String s = fn('hello');
}

Here the analyzer and CFE do not agree.

With weak null safety When the file is opted out of null safety the analyzer produces the error The literal ''hello'' with type 'String' isn't of expected type 'Null'. The CFE gives no error and the code causes runtime exceptions.

With sound null safety When the file is opted into null safety the analyzer and CFE agree with the compile time error The argument type 'String' can't be assigned to the parameter type 'Never'.

The errors are still somewhat confusing. Where did the Null and Never come from? It appears there is some issue with the inference of the generic type argument that is either a bug or unspecified.

@leafpetersen @eernstg @stereotype441 @johnniwinther

[Levi-Lesches]

I was also confused, but apparently Never and Null are actually in the docs now.

As for your specific error, I think Dart is realizing that T must be a String, but it must also be an A, and since that conflict is unresolvable, it defaults to the bottom type, Never. But String isn't a Never, so you get the error.

[nshahan]

I agree, it looks like the inference is selecting the bottom type in some cases but I want to question if that is a good choice. I think it leads to a confusing error message for the author of the code because Never or Null don't appear in the method signature as it was written and they are not the types of the values being passed as arguments.

To me the more concerning cases are when there is no error at compile time because it seems that the compiler should be able to know that this code will never run without an error.

[Levi-Lesches]

I saw an error message once that said Type A (B & C) cannot be assigned to type D, where A wasn't in my code, but B, C, and D were. The error made clear that it inferred the type to be an A because that was the common type between B and C.

I forgot what the context was and I haven't been able to reproduce it since, but if that type of message can be applied here, it should make the Never and Null comments a bit clearer. Something like

The argument type 'String' can't be assigned to the parameter type 'Never', which is the common type between 'String' and 'A'.

[eernstg]

@nshahan wrote:

When the file is opted out of null safety there is no compile time error

That's because an actual argument with static type String can be passed to a formal parameter of type T as long as T <: String. That's true for Null in pre-null-safety Dart. Also, when Never occurs in a pre-null-safety Dart library, it is taken to mean Null.

So a type check is generated and no compile-time error is emitted. However, a dynamic error occurs when we execute the program and reach that point. So that's all working as intended.

With null safety, assignability is made more strict: A type S is assignable to a type T if S is dynamic or S <: T. So it's a compile-time error to pass an actual argument of type String to a formal parameter of type T unless T <: String or T is dynamic.

Inference chooses Never, because Never <: String and Never <: A (and there is no other type with those subtype relations), but that makes it a compile-time error to pass 'Hello' because it includes a downcast to Never.

Considering the other example:

When the file is opted out of null safety the analyzer produces the error
The literal ''hello'' with type 'String' isn't of expected type 'Null'.

The inference chooses Null as the actual type argument to the invocation of fn, because it satisfies Null <: String and Null <: A (and no other type does that).

The CFE generates code for a type check as before. But the analyzer uses the special case of a literal (here: a literal string) to conclude more about the type of the actual argument: It has type exactly String, and in particular it isn't null. We haven't specified exact types, so that's a kind of extra information that the analyzer delivers: In general we have to assume that an expression of type T evaluates to an object whose type could be any type S such that S <: T; but in these special cases we know exactly what the type will be at run time, and then we can predict a few errors that would otherwise only arise at run time.

With null safety, the analysis again infers the type argument Never to fn and reports a compile-time error at the downcast from String to Never.

We may wish to specify exact types (cf. dart-lang/sdk#33307), but we should also be aware of the incomplete nature of this kind of analysis. Also, note that the very property of having an exact type is controversial, because it may be considered to be a violation of the encapsulation of the given object.

[nshahan]

I'm glad this broken code will be caught by a compile time error with null safe Dart. 🎉

Inference chooses Never, because Never <: String and Never <: A (and there is no other type with those subtype relations), but that makes it a compile-time error to pass 'Hello' because it includes a downcast to Never.

Do you think there is room for a better error from the inference algorithm?

Instead of working with the two constraints T <: A and T <: String and solving for the common subtype, would it be possible for the algorithm to fail earlier by recognizing that the constraints are invalid because the only common ancestor between A and String is the bottom type? Are there cases where the user would find inferring the bottom type from a set of constraints to be helpful?

For comparison if we simply remove the assignment of the return value (and that constraint along with it) we get a much more helpful message.

class A {}

T fn<T extends A>(T x) => x;
Null gn(Null x) => x;

void main() {
  var s = 'hello';
  fn(s);
}

test_05.dart:8:3: Error: Inferred type argument 'String' doesn't conform to the bound 'A' of the type variable 'T' on 'fn'.
 - 'A' is from 'test_05.dart'.
Try specifying type arguments explicitly so that they conform to the bounds.
  fn(s);
  ^
test_05.dart:3:6: Context: This is the type variable whose bound isn't conformed to.
T fn<T extends A>(T x) => x;
     ^

[eernstg]

Do you think there is room for a better error from the inference algorithm?

@stereotype441, WDYT? @bwilkerson, do you think this error message could be made more helpful?

[stereotype441]

@eernstg Yeah, I think there might be room for a better error from the inference algorithm here, at least for opted in code.

Before I go into detail about my idea, let me just clarify exactly what is happening in this example:

class A {}

T fn<T extends A>(T x) => x;

void main() {
  var s = 'hello';
  s = fn(s);
}

Here's what's going on (let's consider opted in code for the moment):

• When type inference encounters the line var s = 'hello'; it assigns the variable s the type String.
• When type inference proceeds to s = fn(s);, and tries to infer the type argument to fn, it has a context type of String because it knows the return value from calling fn will need to be assignable to s, and s has type String. It represents this as the constraint T <: String.
• Type inference also looks at the declaration of fn and sees that there's an extends clause, so it adds the constraint T <: A.
• At this point we've collected all the constraints we have for so-called "downwards" inference. The plan is, we'll try to infer types for all the type parameters we can using downwards inference. If we can come up with types, we'll use them; if we can't, then we'll visit the arguments (s in this case), and then use them to create more constaints and assign the remaining types at the time of upwards inference.
• Downwards inference combines T <: String and T <: A using the "greatest lower bound" algorithm, and winds up with T <: Never, so it assigns T to be Never.
• At that point we're done because downwards inference has assigned a type to T. No further inference happens.
• However, if we hadn't managed to come up with a type for T, we would have proceeded to evaluate the type of the argument s (its type is String), and then from that we would have come up with the additional constraint String <: T, and then tried to come up with a type for T based on this constraint as well.

Now, on to my idea. What if, after downwards inference assigns a type of Never to T, we went ahead and proceeded to the upwards inference phase, and added the constraint String <: T. Then we would have three constraints:

• (downwards) T <: String
• (downwards) T <: A
• (upwards) String <: T

At this point, rather than just shortcutting upwards inference entirely because we already have a type from downwards inference, we could take the type from downwards inference and ask if it satisfies all the constraints. If it does, then there's nothing further to do. But if it doesn't, then we know we're in an error condition (*), so we can do deeper analysis. The deeper analysis is to look through the constraints to try to find two constraints that are mutually incompatible. There are three possibilities:

• Maybe we can. That's what's happening in this example, because String <: T and T <: A together imply String <: A, which is manifestly not true. We can use this information to form an error message that precisely explains to the user why type inference failed.
• Maybe we can't, because the constraints are actually solvable (e.g. the constraints might have been (downwards) T <: A, (downwards) T <: B, and (upwards) C <: T, where C is a subtype of both A and B. In this case what's happened is that downwards inference wasn't smart enough to figure out that C was a possible solution to the constraints, so it chose T=Never. Then later, when the C <: T constraint appeared, it was too late to use that information. Here we have a choice: we could either make the inference algorithm give a detailed description to the user of why inference failed, or we could decide that upwards inference is allowed to override bad choices made by downwards inference, so we could accept that T=C and proceed.
• Finally, maybe we can't find two constraints that are mutually incompatible, however maybe there still is no solution. For example, the constraints could be A <: T, B <: T, T <: C, and T <: D, where types A and B each implement both C and D. In this case, we can't provide as nice an error message to the user but we could still dump out all the constraints and say "sorry, we couldn't find a type that satisfied them".

This would all be non-breaking because it would only happen in cases where we already are going to report a compile time error; we would just be replacing a confusing error about assignability with a more comprehensible message explaining that there was a type inference failure.

(* I told a little lie above when I said "we know we're in an error condition" if the constraints can't be satisfied. The fact is, constraints from upwards inference are softer thatn constraints from downwards inference, because if the type violates them, but the compiler can insert implicit downcasts, we may still be able to compile without error. For opted in code, we only allow impicit downcasts from dynamic; for opted out code, we allow implicit downcasts from any type to its subtypes. What I think what this means is that for opted in code, we could make this idea work, as long as we make some special exceptions for upwards inference constraints of the form dynamic <: T. For opted out code this whole idea might not be feasible. But that's ok; solving the problem for opted in code would still be a big win.)

Anyhow, that's all fairly brainstormy. What do y'all think? I can try to flesh this out into something more concrete if there's interest.

[eernstg]

Great explanation, @stereotype441, thanks!

As a somewhat general principle, I think it would indeed be helpful if we could stop early in every analysis process that turns out to end in failure (in particular, type inference). This might be achieved by running the analysis "as usual", using the results (the inferred types), detecting that there is a compile-time error in the inference result (but not reporting it to the user just yet), and then exploring some data produced by the analysis (or running a customized variant of the analysis), aiming to detect a minimal set of facts that suffice to produce the error.

In the concrete case, I think it would be useful if we could tell the developer that the type parameter bound and the context type interact to give T the value Never, and hence inference fails.

Perhaps we can just focus on this particular setup:

• Type inference on a generic function invocation fails, because some actual arguments have types that are not assignable to the corresponding formal parameters.
• Re-solve the set of constraints with reductions, yielding a minimal subset of the constraints that still produce the error (or some heuristically selected subset which is believed to be "nearly minimal").
• Report to the user that those constraints cause the inference to fail.

[nshahan]

Type inference on a generic function invocation fails, because some actual arguments have types that are not assignable to the corresponding formal parameters.

This point sound like a good idea to me. It seems that it would also help even in the case of legacy code that is opted out of null safety.