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
Comments
Comment author: @lpw25 I'm not sure what the right solution is to this problem as I'm unsure why the call to |
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. |
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. |
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 |
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
It certainly fixes the example, but I'm not 100% sure that it is correct more generally. |
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)
end
but if I rename the
S
variant toT
:type t = T : t
type s = T
class c = object (self : '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.The text was updated successfully, but these errors were encountered: