Add strict-inference specification

[srawlins]

We need a formal specification for "strict-inference", so that it can be properly implemented and
tested (e.g. two in progress CRs, 112142 and 111740). @leafpetersen wrote that we can land a spec in this language repository.

Fixes #508

[bwilkerson]

How many of these cases are covered by NNBD? Are there any incompatibilities between this proposal and NNBD?

[bwilkerson]

... whose type cannot be inferred from downwards inference ...

I think you intended to say a little more than that (here and elsewhere). Specifically "inferred as something other than dynamic".

[srawlins]

Even dynamic would be fine. For example:

fn(void callback(dynamic x), dynamic x) { callback(x); }
fn((var x) => print(x));

Strict inference will not report any inference failures; the parameter type on the second line is inferred to be dynamic. The first line is filled with explicit dynamics.

Or the method case:

class C {
  void f2(dynamic a) => print(a);
}

class D extends C {
  @override
  void f2(a) => print(a); // OK; inherits dynamic type
}

[srawlins]

@leafpetersen @munificent I'd love a review from one of you, as you've reviewed previous iterations.

How many of these cases are covered by NNBD?

Do you mean in terms of "Extended Type promotion, Definite Assignment, and Definite Completion"? I don't think these have been specified yet. I see a 9-month old proposal from you and Bob. Should I look at this to see how it would interact?

Are there any incompatibilities between this proposal and NNBD?

I don't think so; not as NNBD is written today, since the type promotion stuff isn't in the spec yet. If, e.g. top-level return types are to be inferred under NNBD, then we could relax that inference failure.

[leafpetersen]

This isn't quite an accurate description of what happens. What happens is that the downwards context provides no information. Upwards inference constrains T to be a super type of bool from the first argument. For the second argument, inference assumes that s and x have type dynamic, and hence infers dynamic Function(dynamic, int) as the type of the function literal. This in turn constraints T to be a supertype of dynamic. The LUB of bool and dynamic is dynamic, and so that is what is chosen for T.

[srawlins]

OK that makes sense. I think I've corrected my paragraph.

I'm hesitant to use the word "assumes" here, as I don't think that's defined :). But I think I understand that this is merely another round of inference, where inference says "I need to know the type of (s, x) => s + x and all I know is ? Function(?, int) so you don't get anything from above" and this new round of inference says "Well garbage in, garbage out, friend; I've got nothing either, so you get dynamic Function(dynamic, int)", and I assume they both have New York accents.