Comment author: @garrigue

The current specification is that type variables that appear only in method types are quantified universally at the method level. We cannot change that lightly (lablgtk relies on this a lot).

If you want to obtain the desired behavior, you just have to write the desired type:
class type ['a] c = object ('a) constraint 'a = < m : 'b; .. > method m : 'b end
Another trick is to add a dummy constraint on 'b:
class type ['a] c = object ('a) constraint 'b = 'b method m : 'b end

Comment author: pveber

That's indeed written explicitely in the manual, sorry for missing it! The second trick comes handy, I'll definitely use it. If this is not too much trouble, could you provide a place in lablgtk where the default behaviour helps? I went through a dozen modules, but all polymorphic methods I found were explicitely annotated as such.

Comment author: @garrigue

Actually, this was the case in older versions of lablgtk, and I tried to avoid public polymorphic methods in lablgtk2, as this requires type annotations when using the object sometimes.
There are still some instances in GAction.action_group#add_action and GButton.toolbar#insert (the short syntax is mostly useful when you are using row polymorphism, as it is verbose otherwise).
An example for normal polymorphism is GText.tag (but here being explicit would not be particularly heavy).

Comment author: pveber

Thanks for the references! I think I now have a better understanding of it. Basically you can write:

class action_group : ([> Gtk.action_group ] as 'a) obj -> object
...
method add_action : #action_skel -> unit
...
end

instead of:

class action_group : ([> Gtk.action_group ] as 'a) obj -> object
...
method add_action : 'b. (#action_skel as 'b) -> unit
...
end

Indeed this convention comes handy and is more readable in the most frequent case where you want polymorphism at the method level (notably with several polymorphic arguments). This is at the expense of making the other use case (giving self a unique type parameter that captures all remaining polymorphism) less practicable, but adding the dummy constraints is not so terrible after all. And now that I have a bit more context, this choice feels more natural too.

I guess the ticket can be closed now. Thanks for all the explanations!