GADT определение

Question

Это просто тест, так что я не очень понимаю, но у меня есть эти определения:

type z 
type _ s 
type (_, _, _) balance = 
    | Less : (*∀'a.*) ('a, 'a s, 'a s) balance 
    | Same : (*∀'b.*) ('b, 'b, 'b) balance 
    | More : (*∀'a.*) ('a s, 'a, 'a s) balance 
type _ aVL = 
    | Leaf : z aVL 
    | Node : (*∀'a, 'b, 'c.*)('a, 'b, 'c) balance * 'a aVL * int * 'b aVL -> 
    ('c s) aVL 

и я получаю сообщение об ошибке для «типа _ AVL =»:

Error: In this definition, a type variable cannot be deduced 
     from the type parameters. 

Что делать?

Answer 1

H/T Gabriel Scherer для ответа на caml-list.

Не используйте такое определение абстрактного типа. Вместо этого (и экспорт) конкретные определения (даже если вы не используете их конструктор для чего-нибудь)

type 'a s = S of 'a 

(или просто type 'a s = S)

Они имеют «лучшее» свойство инъективности. Мы упомянули в рассылке пару раз, и это также «легкий урок» от Жака Гаррига, который мы поговорим на семинаре OCaml в сентябре.

Позор для меня не для поиска по проблеме. Здесь задается точная проблема: GADTs : a type variable cannot be deduced