Infering type argument inside list

[FMorschel]

If you paste the following code into dartpad.dev:

class A<T extends num> {
  const A(this.list);
  final List<T> list;
}

void main() {
  const a = A([]);
}

I get the following errors for line 7 const a = A([]);:

Couldn't infer type parameter 'T'.

Tried to infer 'dynamic' for 'T' which doesn't work:
  Type parameter 'T' is declared to extend 'num' producing 'num'.
The type 'dynamic' was inferred from:
  Parameter 'list' declared as     'List<T>'
                   but argument is 'List<dynamic>'.

Consider passing explicit type argument(s) to the generic.

'dynamic' doesn't conform to the bound 'num' of the type parameter 'T'.

I'm not sure this is working as intended, but for me as a user, this is a little weird, since the type T as I understand has a lower-bound type attached to it (num), so why couldn't the List<T> be inferred to List<num>?

For example, when I do:

  late List<num> list; 
  list = [];

I get no errors.

[eernstg]

The ability to obtain num as the actual type argument for an expression like A(...) is based on a step which is called instantiation to bound. The basic idea is that A(...) becomes A<num>(...) when there are no other constraints on the actual type argument, because that type parameter is declared as T extends num.

If you want to know the details then instantiation to bound is specified here, which is the section 'The instantiation to bound algorithm' in the PDF). This algorithm will find a value for all the type arguments of the given expression. This is used, e.g., if you declare a variable to have type List (which then becomes List<dynamic>). Type inference uses a slightly more complex algorithm which is able to find a value for the remaining type arguments when some type arguments have already been determined by type inference. That's a small difference, though, so you will be able to understand instantiation to bound quite well by looking at said section.

In this context, the crucial point is that instantiation to bound is done at the very end.

Type inference proceeds by propagating information downward into the given expression (in order to choose actual type arguments matching the expectations of the context) and then performs type inference bottom-up based on the given expressions, and type parameters that haven't yet gotten any constraints will be chosen by instantiation to bound.

In the given example there are no constraints on T on the way down, no constraints on the list literal [], and then [] becomes <dynamic>[] going up again, and then we can't find a solution for T because <dynamic>[] must be an acceptable actual argument.

We have a request for passing additional information about type parameter bounds here. I think this issue is basically a case that serves as an argument in favor of pushing on that idea: If we pass down the constraint that T must be a subtype of num then we would presumably be able to turn [] into <num>[] such that the inference as a whole can succeed.

@leafpetersen, @natebosch, @stereotype441, do you have further comments?

[lrhn]

This keeps coming up (as the linked issues show, good sleuthing there), so it's probably worth trying to address.

I think we're shooting ourselves in the foot a little, by using _ when we have a bound.

To include the bound, we'd have to infer [] with a context of List<Something>, where Something is unspecified (not a type we'd lock in during downwards inference), but also not unbounded, so something like (_ extends num).

That means that we can safely infer <num>[] (we don't have to go for <Never>[], like we would if the context was an actual type variable with a bound).

So if we could we give _ a bound in general, and probably have more of them, like they were pseudo-type-variables, then we'd have more information available.

Take:

T id<T>(T value) => value;
void foo<K extends A, V extends B>(Map<K, V> _) {}
foo({"A": id(42));

where the context type of {} then becomes Map<(_$1 extends A), (_$2 extends B)>, which is still not a type that will be enforced during downwards inference, but does carry the upper bounds.

Then "A" is inferred with context type scheme ($1 extends A), to have type String. And id(42)is inferred with($2 extends B), and so is 42, because we will plug this type into Tofidduring inference of id(42), just as we would plug in today (if context type for call is, then Tis bound toduring inference, we just do the same for( extends A)`.)

Which means I've just (again) introduced context type hints, a context type that is a bound, but is not a requirement.
Maybe it's just because it's a good idea! 😁

With that, maybe we can even use (_$1 extends Foo) more than once, if we know two things need to have the same type, like we would if it was an actual type variable. Not sure if that's actually useful. Or decidable.

[FMorschel]

With that, maybe we can even use (_$1 extends Foo) more than once, if we know two things need to have the same type, like we would if it was an actual type variable. Not sure if that's actually useful. Or decidable.

What do you mean? Something like #1674? I could not follow.

[lrhn]

I'm considering cases where the context type contains the same type parameter more than once. Something like:

(T, T) maybeSwap<T>(bool swap, (T, T) pair) { 
  if (swap) return (pair.$2, pair.$1);
  return pair;
}
(S, T) createPair<S, T>(..) {...}

var v = swap(someBool, createPair(...));

Here the context type of createPair(...) would be (T, T) if we had passed a type parameter to swap.
Since we didn't, we currently use (_, _) as context, which doesn't show that it's supposed to be the same type.
If we number the separate _s, then the context type here would be (_$1, _$1) which doesn't say what the type is, but does say that it's the same type.

I have no idea whether that can actually make a difference. Probably not in an immediate function call like this, but maybe if it's a more complicated inlined expression. Or not.

[leafpetersen]

I don't think this has much to do directly with the matching and constraint solving part of inference. I think if you wanted to make progress with this you would want to look at the definitions of greatest and least closure, which is where I think you would use this information.

[leafpetersen]

I filed an issue with a description of the changes to the meta-theory that I believe would be required to improves this here.