Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Nested immediate object referring to outer self does not typecheck #7391

Closed
vicuna opened this Issue Oct 20, 2016 · 13 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Oct 20, 2016

Original bug ID: 7391
Reporter: @nojb
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-10-27T14:59:26Z)
Resolution: fixed
Priority: normal
Severity: block
Target version: 4.04.0 +dev / +beta1 / +beta2
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Related to: #7381
Parent of: #7395

Bug description

The following style of code stopped working after commit babad14 (but @garrigue says that this failure is not necessarily related to the issue addressed by that commit).

class virtual child1 parent =
object
method private parent = parent
end

class virtual child2 =
object(_ : 'self)
constraint 'parent = < previous: 'self option; .. >
method private virtual parent: 'parent
end

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

Error: The method parent has type < child : 'a; previous : 'b option >
but is expected to have type < previous : < .. > option; .. >
Self type cannot escape its class

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

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"?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 20, 2016

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

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) ?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

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.

@vicuna vicuna closed this Oct 27, 2016

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

Comment author: @alainfrisch

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

Comment author: @nojb

I confirm that the regression is fixed! Thanks!

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Oct 27, 2016

Comment author: @nojb

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.