What is the correct way to do this?

What is the correct way to do this?

[Jacques Carette]

I am trying to define a complex AST via polymorphic variants and 
constraints.  I want to encode my static knowledge of the AST into the 
types as much as possible.  I have gotten 'close', but not 'close 
enough'.  

Any help would be most appreciated.  Note that I do mean
Jacques

type symbol = S of string

  (* translation of kind[] *)
type 't prekind = KType | KFormula | Kind of 't
  (* Needed for P-Expr-2 *)
type  ('t,'f,'p) prekinded =
      KDType of 't
    | KDFormula of 'f
    | KDTerm of 'p * 't

type ('t,'f,'p) pretyp =
    [ `TypeBase of symbol
    | `TypeApplyTerm of symbol * ('t,'f,'p) prekinded list (* 
specialization of P-Expr-2 *)
    | `TypeApp of 't * 'p (* P-Expr-4 *)
    | `TypeDepFun of symbol * 't * 't ] (* expanded P-Expr-5 *)

type  't preoperator = [`Operator of (symbol * 't prekind list *
't prekind)] (* P-Expr-1 *)

type ('t,'f,'p) preformula =
     [ `FBase of symbol
     | `FApplyTerm of symbol * ('t,'f,'p) prekinded list (* 
specialization of P-Expr-2 *)
     | `FExists of symbol * 't * 'f ]

(* for improper expressions [S-expressions or raw symbols] *)
type  'e preunknown = [ `UE of 'e list | `US of symbol]

type  ('t,'e,'f,'p) preterm =
     [ `TermBase of symbol
     | `ApplyTerm of symbol * ('t,'f,'p) prekinded list * 't (* P-Expr-2 *)
     | `TermVar of symbol * 't (* P-Expr-3 *)
     | `FunApp of 'p * 'p (* P-Expr-6 *)
     | `FunAbs of symbol * 't * 'p (* P-Expr-7 *)
     | `IfTerm of 'f * 'p * 'p (* P-Expr-8 *)
     | `DefDescr of symbol * 't * 'f (* P-Expr-10 *)
     | `IndefDescr of symbol * 't * 'f (* P-Expr-11 *)
     | `Quote of 'e (* P-Expr-12 *)
     | `Eval of 'p  (* P-Expr-13 *)
     | `OrderedPair of 'e * 'e ]

(* translation of p-expr[], four sorts of p-expr *)
type ('t,'e,'f,'p) preproper = 'p
    constraint 't = [< ('t,'f,'p) pretyp]
    constraint 'f = [< ('t,'f,'p) preformula]
    constraint 'p = [< ('t,'f,'p) pretyp     | ('t,'f,'p) preformula
                     | ('t,'e,'f,'p) preterm | 't preoperator ]
    constraint 'e = [< ('t,'f,'p) pretyp     | ('t,'f,'p) preformula
                     | ('t,'e,'f,'p) preterm | 't preoperator
                     | 'e preunknown ]

type ('t,'e,'f,'p) preexpression = 'e
    constraint 't = [< ('t,'f,'p) pretyp]
    constraint 'e = [< ('t,'f,'p) pretyp     | ('t,'f,'p) preformula
                     | ('t,'e,'f,'p) preterm | 't preoperator
                     | 'e preunknown ]
    constraint 'f = [< ('t,'f,'p) preformula]
    constraint 'p = [< ('t,'f,'p) pretyp     | ('t,'f,'p) preformula
                     | ('t,'e,'f,'p) preterm | 't preoperator ]

(* here is where things fail -- I want to define convenient short-forms 
for the types to that
   I can annotate my code. *)
type proper     = 'p
    constraint 'p = ('t,'e,'f,'p) preproper

The compiler then complains with [where line 81 is the defining line for 
'proper' above:
File "types.ml", line 81, characters 4-65:
A type variable is unbound in this type declaration.
In definition
  [< `ApplyTerm of
       symbol *
       ([< ('b, [< ('b, 'c, 'a) preformula ] as 'c, 'a) pretyp ] as 'b, 'c,
        'a)
       prekinded list * 'b
   | `DefDescr of symbol * 'b * 'c
   | `Eval of 'a
   | `FApplyTerm of symbol * ('b, 'c, 'a) prekinded list
   | `FBase of symbol
   | `FExists of symbol * 'b * 'c
   | `FunAbs of symbol * 'b * 'a
   | `FunApp of 'a * 'a
   | `IfTerm of 'c * 'a * 'a
   | `IndefDescr of symbol * 'b * 'c
   | `Operator of symbol * 'b prekind list * 'b prekind
   | `OrderedPair of
       ([< `ApplyTerm of symbol * ('b, 'c, 'a) prekinded list * 'b
         | `DefDescr of symbol * 'b * 'c
         | `Eval of 'a
         | `FApplyTerm of symbol * ('b, 'c, 'a) prekinded list
         | `FBase of symbol
         | `FExists of symbol * 'b * 'c
         | `FunAbs of symbol * 'b * 'a
         | `FunApp of 'a * 'a
         | `IfTerm of 'c * 'a * 'a
         | `IndefDescr of symbol * 'b * 'c
         | `Operator of symbol * 'b prekind list * 'b prekind
         | `OrderedPair of 'd * 'd
         | `Quote of 'd
         | `TermBase of symbol
         | `TermVar of symbol * 'b
         | `TypeApp of 'b * 'a
         | `TypeApplyTerm of symbol * ('b, 'c, 'a) prekinded list
         | `TypeBase of symbol
         | `TypeDepFun of symbol * 'b * 'b
         | `UE of 'd list
         | `US of symbol ]
        as 'd) *
       'd
   | `Quote of 'd
   | `TermBase of symbol
   | `TermVar of symbol * 'b
   | `TypeApp of 'b * 'a
   | `TypeApplyTerm of symbol * ('b, 'c, 'a) prekinded list
   | `TypeBase of symbol
   | `TypeDepFun of symbol * 'b * 'b ]
  as 'a the variable 'a is unbound

I can 'fix' that by changing the first line to
type 'p proper = 'p
but that kind-of defeats the point, doesn't it?