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

Jump to bottom

GADT matching allows dummy method to escape #7298

Closed
vicuna opened this issue Jul 20, 2016 · 4 comments
Closed

GADT matching allows dummy method to escape #7298

vicuna opened this issue Jul 20, 2016 · 4 comments
Assignees
@garrigue
Labels
bug typing
Milestone
4.05.0

Comments

@vicuna
Copy link

vicuna commented Jul 20, 2016

Original bug ID: 7298
Reporter: @lpw25
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-10-20T02:27:46Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.0 +dev / +beta1 / +beta2
Target version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Related to: #7381

Bug description

The following code fails to type-check:

type t = T : t

module M : sig
type free = < bar : t -> unit; foo : free -> unit >
end = struct

class free = object (self : 'self)

  method foo self = ()

  method bar T =
    self#foo self

  end

end

with the error:

Error: Signature mismatch:
...
Type declarations do not match:
type free =
< bar : t -> unit;
foo : (< bar : t -> unit; foo : 'a -> unit > as 'a) -> unit >
is not included in
type free = < bar : t -> unit; foo : free -> unit >

but if we use non-GADT syntax for the definition of [T] then there is no error.

I'm not sure how exactly it is happening, but the issue is that one of the dummy_method fields is being duplicated and allowed to escape from the class definition.

(This is similar to #7293 but different as this bug is still present on trunk)
@vicuna
Copy link
Author

vicuna commented Aug 3, 2016

Comment author: @garrigue

This one is a but different.
The dummy method does not escape, it is only believed to escape: i.e. the logic in update_level used to check that the type of self does not escape is wrongly activated.
Would probably need to find a different way to check that.
Bu this is not high priority as the number of features required to cause this (completeness) problem is large (GADTs + binary methods).

@vicuna
Copy link
Author

vicuna commented Aug 3, 2016

Comment author: @lpw25

The dummy method does not escape, it is only believed to escape: i.e. the logic in update_level used to check that the type of self does not escape is wrongly activated.

I'm slightly confused by this. When the module inclusion check is done -- so after the escape logic has been run -- the internal free type still contains a dummy method, and that is what causes the inclusion check to fail. Am I misunderstanding something, or did it behave differently when you ran it?

Bu this is not high priority as the number of features required to cause this (completeness) problem is large (GADTs + binary methods).

The reason I came across this bug is that I am trying to evaluate turning on GADT-style matching for all matches that contain a variant constructor, rather than just those matches that obviously contain a GADT. This would allow disambiguation of GADTs in pattern matching (of course it may have too much of a compile-time performance cost, but that is what I was trying to evaluate). In that context, this bug becomes a bit of a show stopper as it basically happens for any binary method.

@vicuna
Copy link
Author

vicuna commented Aug 3, 2016

Comment author: @garrigue

OK, merging GADT matching with normal case is indeed a goal.
But I think that a first step would be to get rid of all the hackery in type_cases.
This mechanism of synchronization between ids and levels is weird.
Same thing for the dummy method: the current approach is too brittle.
Have to understand better how it works.

@vicuna
Copy link
Author

vicuna commented Oct 20, 2016

Comment author: @garrigue

Fixed in 4.04 by commit 911b874.

In subst.ml, do not copy the type of self when it is not generalized.

@vicuna vicuna closed this as completed Oct 20, 2016
@vicuna vicuna added the typing label Mar 14, 2019
@vicuna vicuna added this to the 4.05.0 milestone Mar 14, 2019
@vicuna vicuna mentioned this issue Mar 14, 2019
Closed
@vicuna vicuna added the bug label Mar 20, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@garrigue garrigue

Labels
bug typing
Projects
None yet
Milestone
4.05.0
Development

No branches or pull requests
2 participants
@garrigue @vicuna