Static typing error not caught by compiler (generic method, generic class)

[zathras]

Here's a fairly minimal program to reproduce the problem:

abstract class Foo<R, A> {
  const Foo();

  R frob(A arg);
}

class Bar extends Foo<int, String> {
  const Bar();

  int frob(String arg) => 42;
}

R select<R, A>(Foo<R, A> selector, A arg) => selector.frob(arg);

void main() {
  const b = Bar();
  final answer = select(b, 'How many roads must a man walk down?');
  print('');
  print('The answer is $answer.');
  print('');
  print("And here's the bug.  This shouldn't compile, but does.");
  print(select(b, 9));
}

Clearly, the argument "9" in the last print statement is a statically knowable typing error, but the compiler doesn't catch it, viz:

billf@zathras:~/tmp$ dart bug.dart

The answer is 42.

And here's the bug.  This shouldn't compile, but does.
Unhandled exception:
type 'int' is not a subtype of type 'String' of 'arg'
#0      Bar.frob (file:///home/billf/tmp/bug.dart)
#1      select (file:///home/billf/tmp/bug.dart:15:55)
#2      main (file:///home/billf/tmp/bug.dart:24:9)
#3      _delayEntrypointInvocation.<anonymous closure> (dart:isolate-patch/isolate_patch.dart:283:19)
#4      _RawReceivePortImpl._handleMessage (dart:isolate-patch/isolate_patch.dart:184:12)

This static typing error wasn't caught in the compiler, but the runtime of course did barf. I didn't probe too hard to see just how minimal this example is -- not sure if "const" has anything to do with it, for example.

This is on:

Dart SDK version: 2.12.2 (stable) (Wed Mar 17 10:30:20 2021 +0100) on "linux_x64"

[eernstg]

The invocation select(b, 9) is inferred as select<Object?, Object>(b, 9). b has type arguments int, String at Foo, so inference must satisfy int <: R and String <: A, and 9 introduces the constraint that int <: A. The constraints on A can be solved by A == Object. For R we infer Object? because that's the declared parameter type of print, and no other constraints contradict that (this is based on the basic property of Dart inference that the context type is given priority in many situations).

So the inference on select(b, 9) is working as intended.

However, this implies that selector.frob(arg) receives an argument of type A == Object where the receiver is typed as Foo<R, A> where R == Object?.

This fails at run time, because the actual type of is Foo<int, String>, and 9 isn't a String.

The reason why this error occurs at run time and not at compile time is that Dart uses dynamically checked covariance. The language was designed to do that from day one, and it amounts to the same trade-off between static and dynamic errors that Java and C# have made for arrays (it's the same kind of error as ArrayStoreException in Java, ArrayTypeMismatchException in C#).

It is quite likely that Dart will support statically checked variance, in particular, declaration-site variance (dart-lang/language#524), and we might also support some form of use-site variance (dart-lang/language#753).

[eernstg]

Given that sound variance is already discussed and handled in existing issues, and the example here does not raise any unknown malfunctions, I'll close this issue as working-as-intended.

[zathras]

Got it, thanks. In other words, it's a (somewhat subtle) consequence of allowing covariant assignment. And I totally get that allowing covariance to break soundess is a reasonable stance.

Just to establish a record, here's a clearer (at least to me!) illustration of what's going on:

abstract class Foo<R, A> {
  const Foo();

  R frob(A arg);
}

class Bar extends Foo<int, String> {
  const Bar();

  int frob(String arg) => 42;
}

R select<R, A>(Foo<R, A> selector, A arg) => selector.frob(arg);

void main() {
  const b = Bar();
  // This compiles, because Dart allows the unsound covariant assignment
  // of b, of type Foo<int, int>, to the argument of select, which is 
  // of type Foo<int, Object>.
  int result = select<int, Object>(b, 9);
}

[eernstg]

lndeed! Here's an even simpler example:

void main() {
  List<num> xs = <int>[];
  xs.add(3.14); // Dynamic type error: `3.14` is not an `int`.
}

[zathras]

Sure, that's the obvious textbook example of type parameter covariance breaking soundess. The observation I'm making (in part for a dartdoc comment, more or less for posterity) is that in this example, soundness is broken in a much less obvious way. The actual place this came up in code was in what could be considered a degenerate Visitor pattern.

Visitor being statically type-unsafe is a not-immediately-obvious outcome of allowing covariant assignment. It fooled me at first, anyway!