Разбираюсь тут по TAPL с Хиндли-Миллнером. Вроде бы осилил, но не вполне понятны некоторые аспекты, даже не в нем, а в процессе унификации.
Код из примера в TAPL (адаптированный и урезанный, что бы запускался):

(полный код — здесь)

let unify constr =
  let rec u constr = match constr with
      [] -> []
    | (tyS,TId(tyX)) :: rest ->
        if tyS = TId(tyX) then u rest
        else if occursin tyX tyS then raise Circular_constr
        else
          List.append (u (substinconstr tyX tyS rest)) 
                      [(TId(tyX),tyS)]
    | (TId(tyX),tyT) :: rest ->
        if tyT = TId(tyX) then u rest
        else if occursin tyX tyT then raise Circular_constr
        else
          List.append (u (substinconstr tyX tyT rest))
                      [(TId(tyX),tyT)]
    | (TInt,TInt) :: rest -> u rest
    | (TBool,TBool) :: rest -> u rest
    | (tyS,tyT)::rest -> raise Unsolvable
  in
    u constr

...
let s1 = [
        (TId("y"), TId("x")); 
        (TId("x"), TInt); 
        (TId("z"), TId("y")); 
]

let _ = 
    let    () = pconstr s1
    in let () = print_endline "solving..."
    in pconstr (unify s1)

результатом имеет:

y -> x
x -> TInt
z -> y
solving...
z -> TInt
y -> TInt
x -> y

ну то есть, x -> y не вывелось, хотя данных вроде как достаточно. Вопрос, собственно, вот в чем — это нормально вообще или нет? Баг или фича?


Т.е. если доработать алгоритм и зарядить его выход ему же на вход с проверкой, что количество решений увеличивается — то получаем вполне ожидаемый результат:

y -> x
x -> TInt
z -> y
solving...
z -> TInt
x -> TInt
y -> TInt

но, во-первых, не нравится то, что появилась функция проверки решений, и то, что вменяемые реализации на это решение не похожи (впрочем, там вообще нет двух похожих)