On 2/28/07, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> From: "Geoffrey Romer" <geoff.romer@gmail.com>
> >
> > I'm trying to create a polymorphic class 'a foo which has a
> > polymorphic method that takes as a parameter another foo object, but
> > one with arbitrary type. In other words, something like this:
> >
> > class virtual ['a] foo =
> > object (self)
> >   method virtual bar : 'b. 'b foo -> unit
> > end;;
> >
> > When I try to compile this, though, I get a warning that I "cannot
> > quantify 'b because it escapes this scope". When I drop the " 'b. " it
> > compiles fine, but the reported type for bar is 'a foo -> unit; i.e.
> > it's no longer polymorphic.
> >
> > Is there a problem with trying to make a method polymorphic with
> > respect to the class type in this way? How can I make this work?
>
> The reason it does not work is that recursive object types have to be
> regular. That is, when using foo inside its own definition, the
> parameters must be the same. Since 'a <> 'b, this fails.
>
> This restriction is due to the structural typing of objects, and as
> such it does not apply to records, which are nominal. So you can
> write:
>   type 'a foo = { bar : 'b. 'b foo -> unit; }
> which has basically the same meaning.
>
Thank you for the answer. Let's play the dual of this game:

# type 'a sty = [`Foo of (int * 'a) sty | `Bar];;
Characters 4-45:
  type 'a sty = [`Foo of (int * 'a) sty | `Bar];;
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
In the definition of sty, type (int * 'a) sty should be 'a sty
# type 'a nty = Foo of (int * 'a) nty | Bar;;
type 'a nty = Foo of (int * 'a) nty | Bar

(I wonder if this is the reason when people rant that structural types
are a weaker form of type control... ;) Recently I've started using
closed polymorphic variant types to build subtyping hierarchies and
this gives more type control to me, I think.)