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
Comments
Comment author: @garrigue (Copied from 7381) You're using a nested immediate object referring to the outer self. A workaround for this example is to move the inner object outside, so that its parameter is generalized: let _ = |
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. 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 _ = |
Comment author: @alainfrisch Jacques: I fail to see the deep difference between type-checking object(self) (which doesn't work) and object(self) (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. @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. let _ = |
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) where p1, p2, p3 are patterns matching various types (records mostly). Re-reading your explanation I could make our code typecheck by
let f self x1 x2 x3 = object (self) 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! |
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
The text was updated successfully, but these errors were encountered: