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

Failure to report escaping type variable. #7741

Closed
vicuna opened this issue Feb 21, 2018 · 5 comments
Closed

Failure to report escaping type variable. #7741

vicuna opened this issue Feb 21, 2018 · 5 comments
Assignees
Labels

Comments

@vicuna
Copy link

vicuna commented Feb 21, 2018

Original bug ID: 7741
Reporter: @Drup
Status: new
Resolution: open
Priority: normal
Severity: minor
Category: typing
Related to: #6744
Monitored by: @Drup @gasche

Bug description

The attached file fails with

The implementation blurb.ml
does not match the interface (inferred signature):
Values do not match:
val x : 'a bla t
is not included in
val x : 'a bla t

Regardless of how confusing that error message is, I'm pretty sure this code should fail with an error of the type "The universal variable 'a would escape its scope".

I'm not sure you can break soudness like that, but it seems very sketchy.

Similar to #6744

File attachments

@vicuna
Copy link
Author

vicuna commented Feb 21, 2018

Comment author: @lpw25

Here is a simplified version:

  type 'a s = S

  class type ['x] c = object
   method x : 'x list
  end

  let x : 'a c = object
     method x : 'b . 'b s list = [S]
   end

@vicuna
Copy link
Author

vicuna commented Feb 22, 2018

Comment author: @lpw25

I think this comes from the following lines in occur_univar:

  List.iter2
    (fun t v ->
       if Variance.(mem May_pos v || mem May_neg v)
       then occur_rec bound t)

which originate from a commit labelled "allow for phantom univars".

So it would appear this bug is deliberate. However, I really think that those lines should be replaced by something that expands the alias in the null variance case rather than just letting the universal variable escape.

This is basically a variant on the issue being discussed in this GPR: #1588

@github-actions
Copy link

github-actions bot commented May 7, 2020

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 7, 2020
@lpw25
Copy link
Contributor

lpw25 commented May 7, 2020

Despite #9040 this issue still exists. Univars are allowed to escape their scope through "bivariant" type parameters in Ctype.occur_univar and Ctype.univars_escape. @garrigue would there be any problem with changing those functions to expand type constructors when a univar would otherwise escape? This is what normal occur does and it prevents us from allowing ill-formed types.

@lpw25 lpw25 removed the Stale label May 7, 2020
@lpw25 lpw25 self-assigned this May 7, 2020
@garrigue
Copy link
Contributor

garrigue commented May 9, 2020

I'm not sure I understand your analysis.
Concerning occur_univar, it seems that I forgot the injective case.
So I should check for any of May_pos, May_neg or Inj.
(This is is sufficient because abstract types cannot be invariant.)

garrigue added a commit to garrigue/ocaml that referenced this issue May 9, 2020
garrigue added a commit to garrigue/ocaml that referenced this issue May 25, 2020
garrigue added a commit to garrigue/ocaml that referenced this issue May 29, 2020
garrigue added a commit to garrigue/ocaml that referenced this issue Jun 3, 2020
garrigue added a commit that referenced this issue Jun 3, 2020
garrigue added a commit that referenced this issue Jun 3, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants