Re: [Caml-list] Request for feedback: A problem with injectivity and GADTs

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/04/30, at 14:45, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:

> I have now committed in trunk a fix to PR#5985.
> You can use it to test whether your codebase runs into problems.
> You can either obtain it from subversion directly
> 	svn checkout http://caml.inria.fr/svn/ocaml/trunk
> or use opam to do it for you.
> 
> I checked that at least Core itself compiles without problems.

Ironically, I have just found that lablgtk2 does not compile with the fixed version.
lablgtk2 does not use GADTs, but it uses constrained type parameters in classes.

The problem is as follows:

gobject.mli:
type -'a gobj

gContainer.mli:
class virtual ['a] item_container :
  object
    constraint 'a = < as_item : [>`widget] obj; .. >
    method add : 'a -> unit
    …
  end

File "gContainer.mli", line 126, characters 6-665:
Error: In this definition, a type variable cannot be deduced
       from the type parameters.

It is a bit surprising, since the said variable is the row variable
of the above [> `widget], and it is only referred through 'a.
The reason there is an error is that the checkability requirements
for the body of types and constrained type parameters differ:
to allow the row variable to appear in a position potentially
contravariant, we need it to know from the constraint that it
appears for sure in a negative or invariant position.
One way to solve this is to check that the type identified by 'a can
actually be handled as a real variable (its internal variables do
not occur out of it), which would solve the discrepancy.
However, checking this is going to be a pain.
And making gobj injective immediately solves the problem.

In the midtime, the problem is fixed in the git version of
lablgtk2 by pretending that gobj is a private sum type (whose
contents are abstract).

This also empasizes that the new restriction does not impact
only GADTs: all constrained type parameters are also concerned.

	Jacques Garrigue