> type _ t =
>   | IntLit : int -> int t
>   | BoolLit : bool -> bool t
>   | Pair : 'a t * 'b t -> ('a * 'b) t
>   | App : ('a -> 'b) t * 'a t -> 'b t
>   | Abs : ('a -> 'b) -> ('a -> 'b) t 

> There's something "Haskellish" about this syntax, in the sense that type
> constructors are portrayed as being like functions.

Indeed IIRC OCaml does not accept "App" as an expression (you have to
provide arguments to the construct).  Maybe this is a good opportunity
to lift this restriction.

> While this does make sense in Haskell, in Ocaml it feels a bit out of
> place, because you cannot, for example, partially apply
> a type constructor.

The types above don't allow partial applications either.  They use the
OCaml/SML style of constructors were partial application is not possible
because the various arguments are not provided in a curried way.


        Stefan