Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007293OCamltypingpublic2016-07-19 17:082017-09-24 17:33
Reporterlpw25 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version4.03.0 
Target VersionFixed in Version4.04.0 +dev / +beta1 / +beta2 
Summary0007293: Matches with GADTs break the level check for self types
DescriptionThe following code successfully type-checks:

  type t = T : t

  type s = S

  class c = object (self : 'self)

    method foo : s -> 'self = function
      | S -> self#bar ()

    method bar : unit -> 'self = fun () -> self

  end

but if I rename the `S` variant to `T`:

  type t = T : t

  type s = T

  class c = object (self : 'self)

    method foo : s -> 'self = function
      | T -> self#bar ()

    method bar : unit -> 'self = fun () -> self

  end

then I get an error:

  Error: This expression has type < bar : unit -> 'a; foo : s -> 'a; .. > as 'a
         but an expression was expected of type
           < bar : unit -> 'a; foo : s -> 'a; .. > as 'a
         Self type cannot escape its class

The problem is that in the second case we type-check the case using the GADT-enabled code path. This code-path includes a call to `correct_levels` on the expected type of the method:

  if contains_gadt env pc_lhs then correct_levels ty_res

This call messes up the level of the `*dummy method*` field in the self type, leading to the spurious type error.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0016087)
lpw25 (developer)
2016-07-19 17:10

I'm not sure what the right solution is to this problem as I'm unsure why the call to `correct_levels` is needed. Should `correct_levels` treat `*dummy method*` fields specially like `update_levels` does?
(0016088)
lpw25 (developer)
2016-07-19 18:01

As a side-note, I wonder if it would be better to use a locally abstract type for the type of the dummy method. I believe that would produce the correct behaviour and remove one special case from the type-checker.
(0016089)
lpw25 (developer)
2016-07-19 18:12

Hmm, it seems that Subst already has some special handling of the dummy_method. I'm not sure why this isn't sufficient to avoid the problem. I'll investigate further.
(0016090)
lpw25 (developer)
2016-07-19 18:31

I see the issue: the special handling of the dummy_method in correct_levels is not sufficient if correct_levels is called multiple times. The first call to correct_levels (near the top of type_cases) avoids changing the level of the field type of the dummy_method, but it does change the level of the Tfield node itself to be generic_level. This means that the next call to correct_levels will not treat the dummy_method specially, as `ty.level < generic_level` is one of the conditions on the special handling.
(0016091)
lpw25 (developer)
2016-07-19 18:53
edited on: 2016-07-19 18:53

I'm not sure, but I think the following patch may be a reasonable fix for the issue:

diff --git a/typing/subst.ml b/typing/subst.ml
index 5ea5260..967ef6b 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -158,7 +158,8 @@ let rec typexp s ty =
                       | Some (p, tl) ->
                           Some (type_path s p, List.map (typexp s) tl)))
       | Tfield (m, k, t1, t2)
- when s == identity && ty.level < generic_level && m = dummy_method ->
+ when s == identity && (repr t1).level < generic_level
+ && m = dummy_method ->
           (* not allowed to lower the level of the dummy method *)
           Tfield (m, k, t1, typexp s t2)
       | Tvariant row ->

It certainly fixes the example, but I'm not 100% sure that it is correct more generally.

(0016096)
garrigue (manager)
2016-07-20 07:51

Actually, this was already fixed in trunk (where the bug didn't occur).
But thank you adding the repr which I had forgotten. Added in commit 7a9c88d.

- Issue History
Date Modified Username Field Change
2016-07-19 17:08 lpw25 New Issue
2016-07-19 17:10 lpw25 Note Added: 0016087
2016-07-19 18:01 lpw25 Note Added: 0016088
2016-07-19 18:12 lpw25 Note Added: 0016089
2016-07-19 18:31 lpw25 Note Added: 0016090
2016-07-19 18:53 lpw25 Note Added: 0016091
2016-07-19 18:53 lpw25 Note Edited: 0016091 View Revisions
2016-07-20 07:51 garrigue Note Added: 0016096
2016-07-20 07:51 garrigue Status new => resolved
2016-07-20 07:51 garrigue Fixed in Version => 4.04.0 +dev / +beta1 / +beta2
2016-07-20 07:51 garrigue Resolution open => fixed
2016-07-20 07:51 garrigue Assigned To => garrigue
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-09-24 17:33 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker