Тут надо дать одно пояснение. В .net используется система типов поддерживающая наследование и интерфейсы. Nemerle выводит ближайший общий тип. Например, если у нас есть массив и список, то ближайшим общим типом для них будет IEnumerable[T] (интерфейс реализуемый обоими типами). Если же взять массив и класс динамически расширяемого массива List[T], то ближайшим общим типом для них будет IList[T], а не IEnumerable[T], так как IList[T] унаследован от IEnumerable[T], а значит является более частным (или большим или максимальным).

Есть два вида переменных типов:
* свободные переменные типов (free type variables) с ассоциированными верхней и нижней границей типа VladD2: Верхняя граница задает тип, которым как максимум должен являться тип переменной, а нижняя тип, которым как минимум должен являться тип переменной (т.е. абстрактнее которого не может быть тип переменной).
* фиксированная переменная типа, которая сопоставлена с конкретным типом.
Решатель ограничений (constraint solver) поддерживает граф переменных типов (вершин) и отношений подтипов/наследования (ребер). Граф следует нескольким инвариантам:
1. В нем есть только свободные переменные типов.
2. В нем нет циклов. В случае появления цикла, все переменные типов, вовлеченные в него, сливаются в одну переменную типа. Таким образом, граф является DAG-ом (направленным ациклическим графом).
3. Граф транзитивно замкнут, то есть, если A :> B и B :> C, то A :> C, где X :> Y означает ребро графа от X к Y.
4. Нижняя и верхняя граница также транзитивно замкнуты, то есть если t :> A, A :> B, B :> t', то t :> t', где :> означает отношения наследования (subtyping relation).
5. Если t :> A и A :> t', то t :> t' (то есть верхняя граница должна быть больше нижней). Если t = t', то тип t становится подстановкой для переменной А, поскольку есть только один тип, соответствующий и верхней, и нижней границе. При этом А становится фиксированной. Чтобы выполнялось правило 1, переменная удаляется из графа.
Иногда важно сохранить текущее состояние графа и затем вернуться к нему. Это делается с помощью методов PushState и PopState – они поддерживают стек отображений идентификаторов переменных типов на сами переменные типов.

  /// Определяет, что с этого времени @type, и this будет представлять 
  /// тот же самый тип. 
  public Unify(@type : VarType ) : bool;
  /// Тоже самое, что и Unify, но в случае неудачи не портит значения
  /// переменной типа и не влияет на состояние компилятора.
  public TryUnify(t : VarType ) : bool;

  /// Требовать чтобя this бытл по крайней мере типом [t] (или его 
  /// наследником). Вызывайте этот метод если требуется некоторое ограничение
  /// нижней границы типа.
  /// Возвращает true, если это возможно.
  /// Если это невозможно, то значение переменной типа будет испорчено и 
  /// может появиться сообщение об ошибке компилятора. Так что если нужно
  /// только только проверить возможность данной операции, то нужно 
  /// воспользоваться методом TryRequire
  public virtual Require(@type : VarType ) : bool;
  /// Тоже самое, что и Require, но в случае неудачи не портит значения
  /// переменной типа и не влияет на состояние компилятора.
  public TryRequire (@type : VarType ) : bool;

  /// Задать тип @type как максимальный тип для this.
  public virtual Provide (t : VarType ) : bool;
  /// Тоже самое, что и Provide, но в случае неудачи не портит значения
  /// переменной типа и не влияет на состояние компилятора.
  public TryProvide (@type : VarType ) : bool;

  /// Нижняя граница типа.  
  public LowerBound : option [FixedType];
  /// Верхняя граница типа.  
  public UpperBound : option [FixedType]

    mutable a = System.Collections.Generic.List.[int]();
    mutable b = [1, 2] : System.Collections.IEnumerable;

a is 'System.Collections.Generic.List[int]-'
   LowerBound: 'None'
   UpperBound: 'Some (System.Collections.Generic.List[int])'

public macro Macro1(arg1, arg2)
{
  Impl.Macro1(Nemerle.Macros.ImplicitCTX(), arg1, arg2)
}

module Impl
{
  public Macro1(typer : Typer, arg1 : PExpr, arg2 : PExpr) : PExpr
  {
    def printInfo(expr : PExpr, ty : TyVar) : void
    {
      Message.Hint($"$expr is '$ty'");
      
      Message.Hint($"  LowerBound: '$(ty.LowerBound)'");
      Message.Hint($"  UpperBound: '$(ty.UpperBound)'");
    }
  
    def tExpr1 = typer.TypeExpr(arg1);
    def tExpr2 = typer.TypeExpr(arg2);

    printInfo(arg1, tExpr1.Type);
    printInfo(arg2, tExpr2.Type);
    
    _ = tExpr2.Type.Unify(tExpr1.Type);
    
    Message.Hint("После Unify:");
    
    printInfo(arg1, tExpr1.Type);
    printInfo(arg2, tExpr2.Type);
    
    tExpr1.Type.Fixate();
    tExpr2.Type.Fixate();

    Message.Hint("После Fixate:");
    
    printInfo(arg1, tExpr1.Type);
    printInfo(arg2, tExpr2.Type);

     <[ () ]>
  }
}

    mutable a = System.Collections.Generic.List.[int]();
    mutable b = [1, 2] : System.Collections.IEnumerable;
    
    Macro1(a, b);

a is 'System.Collections.Generic.List[int]-'
  LowerBound: 'None'
  UpperBound: 'Some (System.Collections.Generic.List[int])'
b is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
После Unify:
a is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
b is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
После Fixate:
a is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
b is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'

 a is 'System.Collections.Generic.List[int]-'
   LowerBound: 'None'
   UpperBound: 'Some (System.Collections.Generic.List[int])'
 b is 'System.Collections.IEnumerable'
   LowerBound: 'Some (System.Collections.IEnumerable)'
   UpperBound: 'Some (System.Collections.IEnumerable)'
 После Require:
 a is '(System.Collections.IEnumerable TILL System.Collections.Generic.List[int])'
   LowerBound: 'Some (System.Collections.IEnumerable)'
   UpperBound: 'Some (System.Collections.Generic.List[int])'
 b is 'System.Collections.IEnumerable'
   LowerBound: 'Some (System.Collections.IEnumerable)'
   UpperBound: 'Some (System.Collections.IEnumerable)'
 После Fixate:
 a is 'System.Collections.Generic.List[int]'
   LowerBound: 'Some (System.Collections.Generic.List[int])'
   UpperBound: 'Some (System.Collections.Generic.List[int])'
 b is 'System.Collections.IEnumerable'
   LowerBound: 'Some (System.Collections.IEnumerable)'
   UpperBound: 'Some (System.Collections.IEnumerable)'

a is 'System.Collections.Generic.List[int]-'
  LowerBound: 'None'
  UpperBound: 'Some (System.Collections.Generic.List[int])'
b is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
После Require:
a is 'System.Collections.IEnumerable-'
  LowerBound: 'None'
  UpperBound: 'Some (System.Collections.IEnumerable)'
b is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
После Fixate:
a is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'
b is 'System.Collections.IEnumerable'
  LowerBound: 'Some (System.Collections.IEnumerable)'
  UpperBound: 'Some (System.Collections.IEnumerable)'

if (tyVar.UpperBound.IsSome)
  tyVar.UpperBound
else if (tyVar.LowerBound.IsSome)
  tyVar.LowerBound
else
  None()

let invoke = \lambda x. x.some_method_of_foo() in
let a_list = [make_foo(1), make_foo(2), make_foo(3)] in
List.Map(a_list, invoke)

kl>let invoke = \lambda x. x.some_method_of_foo() in
kl>let a_list = [make_foo(1), make_foo(2), make_foo(3)] in
kl>List.Map(a_list, invoke)
kl>

def invoke = x => x.some_method_of_foo(); // аналог: def invoke(x) { x.some_method_of_foo() }
def a_list = [make_foo(1), make_foo(2), make_foo(3)];
a_list.Map(invoke) // аналог: List.Map(a_list, invoke)

mutable z;
x.a(y.b(x));
z = "str";

class X
{
  public a(i : int)    : void { ... }
  public a(s : string) : void { ... }
}
class Y
{
  public b(i : int)    : string { ... }
  public b(s : string) : int    { ... }
  public b : dioble = 1.1.
}

kl>Пока все, на выходных попробую почитать дальше (чувствую, правда, придется Немерле изучать ).

kl>>let invoke = \lambda x. x.some_method_of_foo() in
kl>>let a_list = [make_foo(1), make_foo(2), make_foo(3)] in
kl>>List.Map(a_list, invoke)
kl>>

a
|-X-b
|   |-X-c
|   |   |...
|   |-Y-c
|   |   |...
|   |-Z-c
|       |...
|-Y-b
|   |...
...
|-Z-b
    |...