Solving T? == Null for T yields Null, not Never

[lrhn]

Extended example below.

Take:

extension Example<T> on C<T?> {
  C<T> get nn => C<T>();
}
class C<T> {}
void main() {
  var v = C<Null>().nn;
}

The result v becomes a C<Null>.
I would have expected it to become C<Never>, since NonNull(Null) is Never.

All other types I've tried work fine, but they're all either of the form SomeType?, or they are top-types that solves as Object.

Larger example:

import 'dart:async';

// C<S>.nn tries to find R s.t. `C<S>` is `C<R?>`.
extension Example<T> on C<T?> {
  C<T> get nn => C<T>();
}

void main<T>() {
  C<int>().nn.st<EC<int>>();
  C<int?>().nn.st<EC<int>>();
  C<Never>().nn.st<EC<Never>>();
  C<Never?>().nn.st<EC<Never>>();
  C<dynamic>().nn.st<EC<Object>>();
  C<Object?>().nn.st<EC<Object>>();
  C<FutureOr<Object?>>().nn.st<EC<FutureOr<Object?>>>();
  C<Ext>().nn.st<EC<Ext>>();
  C<Ext?>().nn.st<EC<Ext>>();
  C<T>().nn.st<EC<T>>();
  C<T?>().nn.st<EC<T>>();
  // But
  C<Null>().nn.st<EC<Null>>(); // Not never!
}

extension type Ext(Object _) {}

extension<T> on T {
  void st<X extends E<T>>() {}
}

typedef E<T> = T Function(T);

typedef EC<T> = E<C<T>>;

class C<T> {
  void get log {
    print(T);
  }
}

@stereotype441 @eernstg
Is this intended, or is it a bug in NonNull?

[eernstg]

I think it's working as specified (in this section).

We're trying to match C<Null> with C<T?> with respect to T, which means matching Null with T? with respect to T? which means matching Null with T, which yields the constraint Null <: T <: _.

The crucial rule is this one:

• If Q is Q0? the match holds under constraint set C:
  • If P is P0? and P0 is a subtype match for Q0 under
    constraint set C.
  • Or if P is dynamic or void and Object is a subtype match for Q0
    under constraint set C.
  • Or if P is a subtype match for Q0 under non-empty constraint set
    C.
  • Or if P is a subtype match for Null under constraint set C.
  • Or if P is a subtype match for Q0 under empty constraint set
    C.

We choose "Or if P is a subtype match for Q0 under non-empty constraint set C" because that yields Null <: T.

It seems sound to change this to "Or if NonNull(P) is a subtype match for Q0 under non-empty constraint set C", but even tiny changes in the type inference rules can have massive implications, so that might be a good idea or a really bad one. We could try it out. ;-)

[lrhn]

It worries me whenever Never? and Null behave differently.
One is UnitOfUnionType | Null and the other is Null, so they should be mostly indistinguishable.

Except that's just not necessarily true in general. We distinguish Object and FutureOr<Object> too in several cases, and even wrt. NonNull we distinguish Object? and FutureOr<Object?> (the former gives Object, the latter FutureOr<Object?>), so we're not always respecting union-type equivalences.

So it's probably more that I expect NonNull to be used here, and I know that NonNull(Null) is Never, whereas I don't expect NonNull to remove a FutureOr.

Could we perhaps add one extra clause, just before the one we would otherwise take:

• ...
  • If P is Null and Never is a subtype match for Q0 under constraint set C.

That only handles Null, but Null might be the only non-top, non-T? type whose NonNull is not itself.
(If that's crazy-talk, then it's because I have no clue how to read these rules.)