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

応答のためのGabriel Scherer caml-list。

この種の抽象型定義は使用しないでください。 （あなたは何のために彼らのコンストラクタを使用しない場合でも）の代わりに使用します（およびエクスポート）の具体的な定義を

type 'a s = S of 'a 

（または単にtype 'a s = S）

彼らは「より良い」単射特性を有します。メーリングリストについては数回言及しています.9月のOCamlワークショップでJacques Garrigueの講演会からの「簡単なテイクアウェイレッスン」です。

問題があると私には恥知らずです。正確な問題は次のとおりです。GADTs : a type variable cannot be deduced