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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> 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.

If I understand correctly, you are saying that this "constraint", in
absence of injectivity, could be handled semantically like GADTs with
non-injective equations, that is as quantifying locally on a ("true")
existential variable?

Handling existential variables (in fact local type constructors)
attached to GADT constructors is well-understood as they have clear
introduction sites and scopes, exactly where their constructor is
matched. When you say that checking the "constraint" case is painful,
is it related to the fact that there is no such corresponding
term-level marker?

On Sat, May 4, 2013 at 8:46 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> 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
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs