Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007391OCamltypingpublic2016-10-20 15:172016-10-27 23:09
Reporternojebar 
Assigned Togarrigue 
PrioritynormalSeverityblockReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version 
Target Version4.04.0 +dev / +beta1 / +beta2Fixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0007391: Nested immediate object referring to outer self does not typecheck
DescriptionThe 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
TagsNo tags attached.
Attached Files

- Relationships
related to 0007381resolvedgarrigue Assertion failure with refutation pattern 
parent of 0007395resolvedgarrigue polymorphism + phantom types regression 

-  Notes
(0016437)
garrigue (manager)
2016-10-20 15:22

(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
(0016439)
garrigue (manager)
2016-10-20 17:01

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.
(0016440)
frisch (developer)
2016-10-20 18:39

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"?
(0016441)
garrigue (manager)
2016-10-20 23:53

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.
(0016456)
nojebar (developer)
2016-10-27 13:38
edited on: 2016-10-27 13:52

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

(0016457)
frisch (developer)
2016-10-27 13:48
edited on: 2016-10-27 13:52

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

(0016458)
garrigue (manager)
2016-10-27 15:26

@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...
(0016459)
garrigue (manager)
2016-10-27 15:31

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;;
(0016464)
nojebar (developer)
2016-10-27 16:42

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) ?
(0016468)
garrigue (manager)
2016-10-27 16:59

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.
(0016469)
frisch (developer)
2016-10-27 17:11

That's great news Jacques, thanks! We'll sync again our version with this commit and see how it goes.
(0016472)
nojebar (developer)
2016-10-27 18:13

I confirm that the regression is fixed! Thanks!
(0016474)
nojebar (developer)
2016-10-27 18:18

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

- Issue History
Date Modified Username Field Change
2016-10-20 15:17 nojebar New Issue
2016-10-20 15:21 garrigue Relationship added related to 0007381
2016-10-20 15:22 garrigue Note Added: 0016437
2016-10-20 15:22 garrigue Assigned To => garrigue
2016-10-20 15:22 garrigue Status new => confirmed
2016-10-20 15:22 garrigue Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2016-10-20 17:01 garrigue Note Added: 0016439
2016-10-20 18:39 frisch Note Added: 0016440
2016-10-20 23:53 garrigue Note Added: 0016441
2016-10-27 13:38 nojebar Note Added: 0016456
2016-10-27 13:48 frisch Note Added: 0016457
2016-10-27 13:49 frisch Severity minor => block
2016-10-27 13:49 frisch Target Version 4.05.0 +dev/beta1/beta2/beta3/rc1 => 4.04.0 +dev / +beta1 / +beta2
2016-10-27 13:52 nojebar Note Edited: 0016456 View Revisions
2016-10-27 13:52 frisch Note Edited: 0016457 View Revisions
2016-10-27 15:26 garrigue Note Added: 0016458
2016-10-27 15:31 garrigue Note Added: 0016459
2016-10-27 16:42 nojebar Note Added: 0016464
2016-10-27 16:59 garrigue Note Added: 0016468
2016-10-27 16:59 garrigue Status confirmed => resolved
2016-10-27 16:59 garrigue Fixed in Version => 4.04.0 +dev / +beta1 / +beta2
2016-10-27 16:59 garrigue Resolution open => fixed
2016-10-27 17:11 frisch Note Added: 0016469
2016-10-27 18:13 nojebar Note Added: 0016472
2016-10-27 18:18 nojebar Note Added: 0016474
2016-10-27 23:09 garrigue Relationship added parent of 0007395
2017-02-23 16:45 doligez Category OCaml typing => typing


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker