Полиморфные варианты и сигнатуры типов

Question

(Это расширение / дистилляция полиморфных вариантов и допускает ошибку типа% связывания)

Рассмотрим следующий код:

Версия 1:

let x : [> `Error1 ] = (`Error1 : [> `Error1 ])
let y : [> `Error1 | `Error2 ] = x

Версия 2:

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])
let y : [> `Error1 | `Error2 ] = x

Версия 1 проверяет типы, но версия 2 не работает (я компилирую с 4.09.0):

File "test.ml", line 2, characters 33-34:
2 | let y : [> `Error1 | `Error2 ] = x
                                     ^
Error: This expression has type [ `Error1 ]
       but an expression was expected of type [> `Error1 | `Error2 ]
       The first variant type does not allow tag(s) `Error2

Обратите внимание, что эта ошибка возникает в определении y, но подпись xодинаково в обоих случаях! Как этоy можно увидеть внутри определения x? Есть ли дополнительная информация о проверке типовx чем его подпись?

Answer 1

Короче говоря, явные аннотации типов не являются сигнатурами типов. В частности, в

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])

тип x является [ `Error1 ].

Корень проблемы в том, что переменные типа объединения в явных аннотациях типов могут быть объединены с конкретными типами.

Более простой пример вашей проблемы:

let f: 'a -> 'a = fun x -> x + 1

Здесь 'a -> 'a аннотация унифицирована с реальным типом int->intи таким образом этот код проверяет типы. Если вы хотите сделать переменную типа'a универсальный, вам нужно быть более точным, добавив явное универсальное количественное определение

let f: 'a. 'a -> 'a = fun x -> x + 1

Error: This definition has type int -> int which is less general than
'a. 'a -> 'a

То же самое происходит с вашим кодом с неявной переменной строки:

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])

Эта аннотация не гарантирует, что тип x является [> `Error1] но только то, что он может быть объединен с [> `Error1]. А поскольку тип[ `Error1 ] может быть объединен с [> `Error1 ], нет причин выдавать ошибку.

Как и раньше, если вы хотите избежать этой проблемы, вам необходимо четко указать, какие переменные универсально количественно определены в вашей аннотации:

let x : 'row. ([> `Error1 ] as 'row) = (`Error1 : [ `Error1 ])

Error: This expression has type [ `Error1 ]
      but an expression was expected of type [> `Error1 ]
      The second variant type is bound to the universal type variable 'a,
      it cannot be closed