Старое неверное в выводе типов

Уравнения, порождаемые подстановкой фактических параметров вместо формальных S ↪ T

Рассмотрим подробно, какие уравнения возникают при подстановке фактических параметров вместо формальных S ↪ T.

Далее X - конкретный тип (класс), T - типовая переменная, V - вектор типовых переменных или конкретных типов, C<V> - обобщенный класс, I - интерфейс (возможно, обобщенный, т.е. I<V>).

Возможны следующие варианты:

• I ↪ C<V>
• I ↪ T
• I ↪ X

Ошибка. Интерфейс нельзя подставить вместо типа

• X ↪ C<V>

Ошибка. Конкретный тип нельзя подставить вместо обобщенного типа

• C<V> ↪ X

Это сделать можно если C<V> является наследником конкретного типа X (если контекст Γ содержит ограничение C<V> <: X). Никаких уравнений при этом не генерируется.

• X ↪ I<V>

Ошибка. Конкретный тип нельзя подставить вместо обобщенного интерфейса

• T ↪ C<V>

Если в ограничениях where есть T <: C<V> (правильнее говорить - если контекст Γ содержит ограничение T <: C<V>), то просто пропускаем эту подстановку - уравнения при этом не генерируются. В противном случае - ошибка

• C<V> ↪ T

Обобщенный класс можно подставить вместо типовой переменной. Это дает новое уравнение

T = C<V> 

• T ↪ I<V>

Если контекст Γ содержит ограничение T <: I<V>, то это дает уравнение

T = I<V> 

В противном случае - ошибка

• C<V> ↪ I<V1>

• C<V> ↪ C1<V1>

Это возможно в двух ситуациях:

если C<V> <: C1<VV> тогда надо положить

V1 = VV (вектор уравнений).

иначе если C = C1, то

V = V1 

иначе - ошибка

• I ↪ I1

Необходимо проверить, есть ли в контексте I <: I1. Если нет - ошибка.

• I<V> ↪ I1<V1>

Если I<V> <: I1<VV> то

V1 = VV 

иначе если I = I1, то

V = V1 

иначе ошибка