Use GLB for function parameters when doing LUB in strong mode.

Use GLB for function parameters when doing LUB in strong mode.

R=leafp@google.com

Committed: https://github.com/dart-lang/sdk/commit/c55e9ef20bbfb7b884034eb5192fb3a7ec5e6f5a

[Bob Nystrom, 2016-03-18 22:36:43]

rnystrom@google.com changed reviewers:
+ leafp@google.com

[Bob Nystrom, 2016-03-18 22:36:43]

I still need to do better LUB for generics, but this was a nice standalone piece
of work.

[Leaf, 2016-03-22 00:02:20]

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
File pkg/analyzer/lib/src/generated/type_system.dart (right):

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:467: if (type1.isVoid ||
type2.isVoid) {
This seems wrong.  void isn't really in the same category of types as the rest,
but I don't *think* it hurts to have it here.  In the subtype code, we really
only allow it in function subtying.  However, it should presumably only arise
(in well-formed code at least) via taking the GLB of two function return types. 


In any case, while we only allow returns of null values from void functions,
we've defined subtyping to allow non-void functions to be a subtype of void
functions.  If I recall correctly this was to support the common idiom of
passing functions returning dynamic where functions returning void were
expected.  This means the that GLB of a function returning void and a function
returning T should be a function returning T.

The dual will be true for LUB, of course.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:473: type2 =
type2.resolveToBound(provider.objectType);
These look wrong.  I think these methods are wrong even in the spec mode
implementation of LUB, actually.  But here, I think this gives GLB(S, T) ==
Object (when S and T are type variables with no bounds), and GLB(S, T) == T when
S is a type variable with no bound and T is not.  In neither case is the result
even a lower bound.  In the case that the variables have bounds it's slightly
more complicated, but still wrong.

We could try to do something here to take into account parameter bounds into
account - we're basically in a closed world with respect to the sub-typing
hierarchy induced by parameter bounds.  For now though, I'd suggest just letting
this fall through to the subtyping cases below.  This will, I think, catch the
common cases (e.g. S, T extends S) without pulling you down the rabbit hole.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:544: parameters.add(new
ParameterElementImpl.synthetic(
Why not re-use addParameter here?

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:646: }
Might be worth checking for object here, just to cut out the long search below
in the case that one of the types is object.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:665: type2 =
type2.resolveToBound(typeProvider.objectType);
This is kind of weird, and not right even for spec mode in the case that both
are type variables.  I filed a bug here:

https://github.com/dart-lang/sdk/issues/26054

It does at least give *an* upper bound, but it won't be the least, and in many
common cases won't be the useful one (e.g. T, S extends T).

The spec definition is pretty unhelpful.

I suspect that a reasonable algorithm is to expand the innermost type variable
first.  Alternatively, you could probably choose to treat it as just an instance
of the interface type upper bound problem, with the "inheritance" chain extended
by the bounds placed on the variables.

In the short term, in the case that both are type variables you could check if
either is a subtype of the other, and if so use the supertype, and otherwise
fall back to expanding both.  This should catch many of the interesting cases
without getting too involved.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/generated...
File pkg/analyzer/test/generated/type_system_test.dart (right):

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/generated...
pkg/analyzer/test/generated/type_system_test.dart:968: FunctionType
_functionType(List<DartType> required,
There's another version of this code in the TypeBuilder class below, probably
worth combining if possible.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/generated...
pkg/analyzer/test/generated/type_system_test.dart:1408: * Tests defined in this
class are ones whose behavior is spec mode-specific.
s/spec/strong/

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/generated...
pkg/analyzer/test/generated/type_system_test.dart:1414: void setUp() {
Can you add tests to both of these checking LUB and GLB for () => void, () =>
int?

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/generated...
pkg/analyzer/test/generated/type_system_test.dart:1580:
_checkGreatestLowerBound(typeParam, simpleFunctionType, simpleFunctionType);
This should be bottom.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/generated...
pkg/analyzer/test/generated/type_system_test.dart:1597:
_checkGreatestLowerBound(typeParam, interfaceType, interfaceType);
Should be bottom.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/src/task/...
File pkg/analyzer/test/src/task/strong/checker_test.dart (left):

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/test/src/task/...
pkg/analyzer/test/src/task/strong/checker_test.dart:39: _Predicate<Object> v =
/*warning:DOWN_CAST_COMPOSITE*/(isValidKey != null)
\o/

[Bob Nystrom, 2016-03-22 21:35:00]

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
File pkg/analyzer/lib/src/generated/type_system.dart (right):

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:467: if (type1.isVoid ||
type2.isVoid) {
On 2016/03/22 00:02:20, Leaf wrote:
> However, it should presumably only arise
> (in well-formed code at least) via taking the GLB of two function return
types. 

Yeah, I think that's right.

> In any case, while we only allow returns of null values from void functions,
> we've defined subtyping to allow non-void functions to be a subtype of void
> functions.  If I recall correctly this was to support the common idiom of
> passing functions returning dynamic where functions returning void were
> expected.  This means the that GLB of a function returning void and a function
> returning T should be a function returning T.

So treat void like a top type for GLB? If I do that, then I think that implies
type errors on the marked lines here:

takeVoidFn(void fn()) { print(fn()); }
takeIntFn(int fn()) { print(fn()); }

void returnVoid() => null;
int returnInt() => 123;

main(bool b) {
  takeIntFn(returnVoid); // <--
  takeVoidFn(returnInt);

  (b ? takeVoidFn : takeIntFn)(returnVoid); // <--
  (b ? takeVoidFn : takeIntFn)(returnInt);
}

The first one isn't GLB, of course, and seems reasonable if a little
pessimistic.

But it seems a little strange to me to have the type error on the second marked
line. Is that what you had in mind? If so, I'm OK with it, I guess. We are way
off in the weeds of code that no sane person would likely write anyway.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:473: type2 =
type2.resolveToBound(provider.objectType);
On 2016/03/22 00:02:20, Leaf wrote:
> These look wrong.  I think these methods are wrong even in the spec mode
> implementation of LUB, actually.

Honestly, I didn't understand exactly what it accomplished there either.

> For now though, I'd suggest just letting
> this fall through to the subtyping cases below.  This will, I think, catch the
> common cases (e.g. S, T extends S) without pulling you down the rabbit hole.

Done. Took me a while to think through it, but it makes sense.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:544: parameters.add(new
ParameterElementImpl.synthetic(
On 2016/03/22 00:02:20, Leaf wrote:
> Why not re-use addParameter here?

Oops. Done.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:665: type2 =
type2.resolveToBound(typeProvider.objectType);
On 2016/03/22 00:02:20, Leaf wrote:
> This is kind of weird, and not right even for spec mode in the case that both
> are type variables.  I filed a bug here:
> 
> https://github.com/dart-lang/sdk/issues/26054
> 
> It does at least give *an* upper bound, but it won't be the least, and in many
> common cases won't be the useful one (e.g. T, S extends T).
> 
> The spec definition is pretty unhelpful.
> 
> I suspect that a reasonable algorithm is to expand the innermost type variable
> first.  Alternatively, you could probably choose to treat it as just an
instance
> of the interface type upper bound problem, with the "inheritance" chain
extended
> by the bounds placed on the variables.
> 
> In the short term, in the case that both are type variables you could check if
> either is a subtype of the other, and if so use the supertype, and otherwise
> fall back to expanding both.  This should catch many of the interesting cases
> without getting too involved.  

For what it's worth, this code is unchanged. I just moved it up from
TypeSystemImpl into here so it's accessible to StrongModeTypeSystem too. Is it
OK if I just add TODO mentioning the bug and leave it alone for now?

[Leaf, 2016-03-23 05:33:39]

lgtm

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
File pkg/analyzer/lib/src/generated/type_system.dart (right):

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:467: if (type1.isVoid ||
type2.isVoid) {
On 2016/03/22 21:35:00, Bob Nystrom wrote:
> On 2016/03/22 00:02:20, Leaf wrote:
> > However, it should presumably only arise
> > (in well-formed code at least) via taking the GLB of two function return
> types. 
> 
> Yeah, I think that's right.
> 
> > In any case, while we only allow returns of null values from void functions,
> > we've defined subtyping to allow non-void functions to be a subtype of void
> > functions.  If I recall correctly this was to support the common idiom of
> > passing functions returning dynamic where functions returning void were
> > expected.  This means the that GLB of a function returning void and a
function
> > returning T should be a function returning T.
> 
> So treat void like a top type for GLB? If I do that, then I think that implies
> type errors on the marked lines here:
> 
> takeVoidFn(void fn()) { print(fn()); }
> takeIntFn(int fn()) { print(fn()); }
> 
> void returnVoid() => null;
> int returnInt() => 123;
> 
> main(bool b) {
>   takeIntFn(returnVoid); // <--
>   takeVoidFn(returnInt);
> 
>   (b ? takeVoidFn : takeIntFn)(returnVoid); // <--
>   (b ? takeVoidFn : takeIntFn)(returnInt);
> }

Yes, that's right.  The issue is that subtyping defines what GLB and LUB need to
be.   The most basic correctness condition for GLB and LUB is that what they
compute should be at least lower bounds and upper bounds respectively.  We're
being loosey-goosey about the G and L part, but we should at least get the LB
and UB part right.  So:

> The first one isn't GLB, of course, and seems reasonable if a little
> pessimistic.

If you consider this example, you'll see why it has to be this way:

takeVoidFn(void fn()) { takeIntFn(fn); }
takeIntFn(int fn()) { print(fn() + 1); }

void returnVoid() => null;
int returnInt() => 123;
bool returnBool() => true;

takeVoidFn(returnBool);

We allow () -> something to subtype () -> void.  If we allow you to go the other
way as well, then you break the type system entirely.

We could consider only allowing () -> dynamic to subtype () -> void.  This would
probably allow most of the cases that we were trying to support, and induce a
different LUB/GLB.  But it kind of makes sense to me that you can pass any
function returning something into a context expecting a function that returns
nothing, since you can count on the context to ignore the result (and on all of
our current platforms at least the calling conventions are compatible).

Once you accept this though (if you do accept it), then the GLB just falls out. 


> But it seems a little strange to me to have the type error on the second
marked
> line. Is that what you had in mind? If so, I'm OK with it, I guess. We are way
> off in the weeds of code that no sane person would likely write anyway.

In order to satisfy the basic correctness condition I describe above, the LUB of
the types of takeVoidFn and takeIntFn must be a supertype of each of their
types, which means that GLB(() -> void, () -> int) <: () -> void and () -> int
must be true.  That means that GLB(void, int) <: void and int must be true. 
Bottom would work here, but it's not greatest.  Choosing int gives you a greater
lower bound (in fact, in this case, it gives you the actual greatest lower bound
as induced by this subtyping relation.).

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:665: type2 =
type2.resolveToBound(typeProvider.objectType);
On 2016/03/22 21:35:00, Bob Nystrom wrote:
> On 2016/03/22 00:02:20, Leaf wrote:
> > This is kind of weird, and not right even for spec mode in the case that
both
> > are type variables.  I filed a bug here:
> > 
> > https://github.com/dart-lang/sdk/issues/26054
> > 
> > It does at least give *an* upper bound, but it won't be the least, and in
many
> > common cases won't be the useful one (e.g. T, S extends T).
> > 
> > The spec definition is pretty unhelpful.
> > 
> > I suspect that a reasonable algorithm is to expand the innermost type
variable
> > first.  Alternatively, you could probably choose to treat it as just an
> instance
> > of the interface type upper bound problem, with the "inheritance" chain
> extended
> > by the bounds placed on the variables.
> > 
> > In the short term, in the case that both are type variables you could check
if
> > either is a subtype of the other, and if so use the supertype, and otherwise
> > fall back to expanding both.  This should catch many of the interesting
cases
> > without getting too involved.  
> 
> For what it's worth, this code is unchanged. I just moved it up from
> TypeSystemImpl into here so it's accessible to StrongModeTypeSystem too. Is it
> OK if I just add TODO mentioning the bug and leave it alone for now?

Sure, but I'd like it to be one of those TODOs that actually gets TODONE at some
point. :)

Can you summarize (or just copy) my suggestions above into the TODO (or into a
bug) so that the context doesn't get lost - I did put a certain amount of
thought into it, and will have forgotten it all by the time we come back to
this.

[Bob Nystrom, 2016-03-23 20:50:53]

Description was changed from

==========
Use GLB for function parameters when doing LUB in strong mode.
==========

to

==========
Use GLB for function parameters when doing LUB in strong mode.

R=leafp@google.com

Committed:
https://github.com/dart-lang/sdk/commit/c55e9ef20bbfb7b884034eb5192fb3a7ec5e6f5a
==========

[Bob Nystrom, 2016-03-23 20:50:54]

Committed patchset #3 (id:40001) manually as
c55e9ef20bbfb7b884034eb5192fb3a7ec5e6f5a (presubmit successful).

[Bob Nystrom, 2016-03-23 20:51:37]

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
File pkg/analyzer/lib/src/generated/type_system.dart (right):

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:467: if (type1.isVoid ||
type2.isVoid) {
On 2016/03/23 05:33:39, Leaf wrote:
> On 2016/03/22 21:35:00, Bob Nystrom wrote:
> > On 2016/03/22 00:02:20, Leaf wrote:
> > > However, it should presumably only arise
> > > (in well-formed code at least) via taking the GLB of two function return
> > types. 
> > 
> > Yeah, I think that's right.
> > 
> > > In any case, while we only allow returns of null values from void
functions,
> > > we've defined subtyping to allow non-void functions to be a subtype of
void
> > > functions.  If I recall correctly this was to support the common idiom of
> > > passing functions returning dynamic where functions returning void were
> > > expected.  This means the that GLB of a function returning void and a
> function
> > > returning T should be a function returning T.
> > 
> > So treat void like a top type for GLB? If I do that, then I think that
implies
> > type errors on the marked lines here:
> > 
> > takeVoidFn(void fn()) { print(fn()); }
> > takeIntFn(int fn()) { print(fn()); }
> > 
> > void returnVoid() => null;
> > int returnInt() => 123;
> > 
> > main(bool b) {
> >   takeIntFn(returnVoid); // <--
> >   takeVoidFn(returnInt);
> > 
> >   (b ? takeVoidFn : takeIntFn)(returnVoid); // <--
> >   (b ? takeVoidFn : takeIntFn)(returnInt);
> > }
> 
> Yes, that's right.  The issue is that subtyping defines what GLB and LUB need
to
> be.   The most basic correctness condition for GLB and LUB is that what they
> compute should be at least lower bounds and upper bounds respectively.  We're
> being loosey-goosey about the G and L part, but we should at least get the LB
> and UB part right.  So:
> 
> > The first one isn't GLB, of course, and seems reasonable if a little
> > pessimistic.
> 
> If you consider this example, you'll see why it has to be this way:
> 
> takeVoidFn(void fn()) { takeIntFn(fn); }
> takeIntFn(int fn()) { print(fn() + 1); }
> 
> void returnVoid() => null;
> int returnInt() => 123;
> bool returnBool() => true;
> 
> takeVoidFn(returnBool);
> 
> We allow () -> something to subtype () -> void.  If we allow you to go the
other
> way as well, then you break the type system entirely.
> 
> We could consider only allowing () -> dynamic to subtype () -> void.  This
would
> probably allow most of the cases that we were trying to support, and induce a
> different LUB/GLB.  But it kind of makes sense to me that you can pass any
> function returning something into a context expecting a function that returns
> nothing, since you can count on the context to ignore the result (and on all
of
> our current platforms at least the calling conventions are compatible).
> 
> Once you accept this though (if you do accept it), then the GLB just falls
out. 
> 
> 
> > But it seems a little strange to me to have the type error on the second
> marked
> > line. Is that what you had in mind? If so, I'm OK with it, I guess. We are
way
> > off in the weeds of code that no sane person would likely write anyway.
> 
> In order to satisfy the basic correctness condition I describe above, the LUB
of
> the types of takeVoidFn and takeIntFn must be a supertype of each of their
> types, which means that GLB(() -> void, () -> int) <: () -> void and () -> int
> must be true.  That means that GLB(void, int) <: void and int must be true. 

Ah, got it. Took me a while to work through it (so many nested function types!)
but I think it makes sense.

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:646: }
On 2016/03/22 00:02:20, Leaf wrote:
> Might be worth checking for object here, just to cut out the long search below
> in the case that one of the types is object.

I'm trying to get out of the habit of speculative optimization because I think
analyzer is rife with it (so many cached list lengths!), and it's not clear to
me that it adds performance value. Definitely up for optimizing this case if we
see it show up in a profile. :)

https://codereview.chromium.org/1807213005/diff/1/pkg/analyzer/lib/src/genera...
pkg/analyzer/lib/src/generated/type_system.dart:665: type2 =
type2.resolveToBound(typeProvider.objectType);
On 2016/03/23 05:33:39, Leaf wrote:
> On 2016/03/22 21:35:00, Bob Nystrom wrote:
> > On 2016/03/22 00:02:20, Leaf wrote:
> > > This is kind of weird, and not right even for spec mode in the case that
> both
> > > are type variables.  I filed a bug here:
> > > 
> > > https://github.com/dart-lang/sdk/issues/26054
> > > 
> > > It does at least give *an* upper bound, but it won't be the least, and in
> many
> > > common cases won't be the useful one (e.g. T, S extends T).
> > > 
> > > The spec definition is pretty unhelpful.
> > > 
> > > I suspect that a reasonable algorithm is to expand the innermost type
> variable
> > > first.  Alternatively, you could probably choose to treat it as just an
> > instance
> > > of the interface type upper bound problem, with the "inheritance" chain
> > extended
> > > by the bounds placed on the variables.
> > > 
> > > In the short term, in the case that both are type variables you could
check
> if
> > > either is a subtype of the other, and if so use the supertype, and
otherwise
> > > fall back to expanding both.  This should catch many of the interesting
> cases
> > > without getting too involved.  
> > 
> > For what it's worth, this code is unchanged. I just moved it up from
> > TypeSystemImpl into here so it's accessible to StrongModeTypeSystem too. Is
it
> > OK if I just add TODO mentioning the bug and leave it alone for now?
> 
> Sure, but I'd like it to be one of those TODOs that actually gets TODONE at
some
> point. :)
> 
> Can you summarize (or just copy) my suggestions above into the TODO (or into a
> bug) so that the context doesn't get lost - I did put a certain amount of
> thought into it, and will have forgotten it all by the time we come back to
> this.

Done!

[Jennifer Messerly, 2016-03-23 21:43:36]

jmesserly@google.com changed reviewers:
+ jmesserly@google.com

[Jennifer Messerly, 2016-03-23 21:43:36]

FYI, I'm seeing test failures from this. Reproduced with:

./tools/test.py --checked -m release pkg/analyzer

example stack trace:

  Caused by 'package:analyzer/src/generated/type_system.dart': Failed assertion:
line 373 pos 12: '!t1.isVoid' is not true.
  #0      _AssertionError._throwNew (dart:core-patch/errors_patch.dart:27)
  #1      StrongTypeSystemImpl._isSubtypeOf
(package:analyzer/src/generated/type_system.dart:373:12)
  #2      StrongTypeSystemImpl.isSubtypeOf
(package:analyzer/src/generated/type_system.dart:259:12)
  #3      CodeChecker._checkDowncast
(package:analyzer/src/task/strong/checker.dart:705:15)
  #4      CodeChecker.checkAssignment
(package:analyzer/src/task/strong/checker.dart:148:7)
  #5      CodeChecker.visitVariableDeclarationList
(package:analyzer/src/task/strong/checker.dart:573:11)


Is that assertion obsolete?