Взаимно индуктивные типы данных с параметрами типа

Question

Я пытаюсь написать объявление двух взаимно индуктивных типов данных, которые оба принимают параметр типа в качестве аргументов следующим образом:

noeq
type foo 'a =
    | FooA: x: 'a -> foo 'a
    | Foob: y: bar 'a -> foo 'a
and bar 'b =
    | BarA: x: int -> bar 'b
    | BarF: y: foo 'b -> bar 'b

Я получаю следующее сообщение об ошибке:

LabeledStates.fst(59,0-64,31): (Ошибка 67) Не удалось решить неравенства юниверсов для индуктивностей. Сообщалось об ошибке 1 (см. Выше)

(где строка 59 - это строка, которая включает "type foo 'a")

Что означает эта ошибка и что я могу сделать, чтобы ее исправить?

Если я удалю параметры типа (и дам foo.x, например, тип int), я больше не получу ошибок. Точно так же, если я просто дам одному из типов параметр типа, но не другому, у меня также не будет ошибок.

Answer 1

F* не может вывести вселенные в подобных случаях. Однако вы можете предоставить явные экземпляры юниверса. Например, вот три возможных решения:

Во-первых, полиморфная двойная вселенная, наиболее общая, но, возможно, и довольно громоздкая в использовании.

noeq
type foo (a:Type u#a) : Type u#(max a b) =
   | FooA: x: a -> foo a
   | Foob: y: bar u#b u#a a -> foo a
and bar (b:Type u#b) : Type u#(max a b) =
   | BarA: x: int -> bar b
   | BarF: y: foo u#b u#a b -> bar b

Полиморфное решение для одной вселенной, возможно, немного более простое, но менее общее:

noeq
type foo1 (a:Type u#a) : Type u#a =
   | Foo1A: x: a -> foo1 a
   | Foo1b: y: bar1 u#a a -> foo1 a
and bar1 (b:Type u#a) : Type u#a =
   | Bar1A: x: int -> bar1 b
   | Bar1F: y: foo1 u#a b -> bar1 b

И, наконец, версия, специализированная для вселенной 0, вероятно, самая простая в использовании, если она соответствует вашим потребностям, но также наименее общая:

noeq
type foo0 (a:Type u#0) : Type u#0 =
   | Foo0A: x: a -> foo0 a
   | Foo0b: y: bar0 a -> foo0 a
and bar0 (b:Type u#0) : Type u#0 =
   | Bar0A: x: int -> bar0 b
   | Bar0F: y: foo0 b -> bar0 b