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

Matches with GADTs break the level check for self types #7293

Closed
vicuna opened this Issue Jul 19, 2016 · 6 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

vicuna commented Jul 19, 2016

Original bug ID: 7293
Reporter: @lpw25
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:33:12Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.03.0
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Monitored by: @gasche

Bug description

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

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 19, 2016

Comment author: @lpw25

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?

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 19, 2016

Comment author: @lpw25

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 19, 2016

Comment author: @lpw25

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 19, 2016

Comment author: @lpw25

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 19, 2016

Comment author: @lpw25

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.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

vicuna commented Jul 20, 2016

Comment author: @garrigue

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.

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.