Comment author: @garrigue

(Copied from 7381)

You're using a nested immediate object referring to the outer self.
This is probably not well supported at this point (independently of commit babad14).
I'm not sure I will be able to fix it for 4.04.

A workaround for this example is to move the inner object outside, so that its parameter is generalized:

let _ =
let child self =
object
inherit child1 self
inherit child2
end
in
object(self)
method previous = None
method child = child self
end

Comment author: @garrigue

Fixed for this specific example by commit 36563ea in 4.04.

I keep this PR open, as the problem of using self in nested objects is probably not completely solved: one is going to get an error with
method child () = object ... end
for instance.

Comment author: @alainfrisch

Thanks Jacques! I just wanted to report that we (=LexiFi) use this style quite a bit in a specific part of our code base. Are there theoretical difficulties in supporting "nested immediate object referring to the outer self"?

Comment author: @garrigue

First, we should be a bit clearer on the problem here: not only self is used in an inner object, but it captures the self type of that inner object too, so that they are in mutual recursion.

Currently, the way to detect that self escapes requires that its level is never lowered.
So in this case this means that the level of the two self types must me identical, i.e. that the level where the inner object is created is the same as the outer object.

My workaround code avoids this problem by first generalizing the self type of the inner object, so that it can then be instantiated at the right level in the outer object when creating the mutual recursion.

Synchronizing the levels without generalization seems difficult, so I do not see an easy solution in general.

Comment author: @nojb

Hi Jacques,

Do you see any workaround for the case of methods with parameters ? We use this style heavily in our codebase and we are stuck due to this regression .

For reference, this is the example:

let _ =
object(self)
method previous = None
method child () =
object
inherit child1 self
inherit child2
end
end

Comment author: @alainfrisch

Jacques: I fail to see the deep difference between type-checking

object(self)
method previous = None
method child = fun () -> object .... end
end

(which doesn't work)

and

object(self)
method previous = None
method child = object .... end
end

(which does)

Was #7381 about fixing some soundness bug, or just turning internal compiler errors (which have been present for some time) into proper typing error? If the latter, may I suggest that reverting the fix could be a good idea. Breaking user code so close from a release date seems worse than leaving the previous bug (again, assuming it was not affecting soundness).

Comment author: @garrigue

@Frisch: I have no concrete example immediately, but this could be a soundness bug (some missing case going undetected because typing erroneously fails). Basically, the problem is that the new splitting exhaustiveness check for GADT types means that it is very hard to know in advance whether a pattern-matching may involve GADTs or not. The only case where we know for sure that there is no need to prepare for GADTs is when the pattern is just a variable or an underscore. This makes the difference between methods which take no arguments (which only have a variable to get self internally), and receiving (), which is internally a constructor.
Note that it has some advantages too: I didn't turn on type-based disambiguation for GADT constructors yet, but this should actually be OK now.

@nojebar I have modified the code (commit 9a2015d) so that now type constraints are also allowed. Could you try modifying your code, replacing [method child () = ...] with [method child (_ : unit) = ...].

For both, handling "()" unmodified is a real problem, because internally it is just a constructor, and type directed disambiguation could turn it into a constructor of a type containing also GADT cases...

Comment author: @garrigue

I have also added more examples.
For instance, the following small variation didn't work in 4.03, and shows why this pattern is inherently fragile.

let _ =
object(self)
method previous = None
method child =
let o =
object
inherit child1 self
inherit child2
end
in o
end;;

Comment author: @nojb

Hi Jacques,

Thanks for the quick reply. Indeed 9a2015d fixes the case for (). In our own code we have methods with many different arguments, i.e.

object (self)
method f p1 p2 p3 =
object
.... self ...
end
end

where p1, p2, p3 are patterns matching various types (records mostly). Re-reading your explanation I could make our code typecheck by

1. lifting the inner objects to a top-level function, and
2. replacing the patterns by variables and using a let just before constructing the object to deconstruct the arguments, i.e.

let f self x1 x2 x3 =
let p1 = x1 in
let p2 = x2 in
let p3 = x3 in
object
... self ...
end

object (self)
method f = f self
end

Maybe this way of rewriting things could offer a hint to a possible solution ? At the very least if the problem arises only with gadts, it seems that the check in is_var could be made to walk through the pattern recursively to handle a couple more kinds of patterns (tuples & records not involving gadts) ?

Comment author: @garrigue

Good news: I could fix this in commit 7365a2f.

The idea is to only raise the level either when there are actually GADTs in the pattern (which is not your case) or only during exhaustiveness/redundancy check (which only involves patterns, not expressions). This removes completely the regression.

Comment author: @alainfrisch

That's great news Jacques, thanks! We'll sync again our version with this commit and see how it goes.

Comment author: @nojb

I confirm that the regression is fixed! Thanks!

Comment author: @nojb

Commit 9a2015 seems to have caused a small regression: #7395.