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

[OCaml] Typechecking limitation in presence of mutually recursive modules #7077

Closed
vicuna opened this issue Dec 7, 2015 · 5 comments
Closed

[OCaml] Typechecking limitation in presence of mutually recursive modules #7077

vicuna opened this issue Dec 7, 2015 · 5 comments
Labels
feature-wish recursive-modules Stale typing

Comments

@vicuna
Copy link

vicuna commented Dec 7, 2015

Original bug ID: 7077
Reporter: Iguernlala
Status: acknowledged (set by @damiendoligez on 2016-02-03T16:20:16Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.3
Target version: undecided
Category: typing
Tags: recmod

Bug description

The attached code does not typecheck unless type annotation is
put on line "L29", or lines "L29" and "L30" are swapped.

Maybe the information which says that "Th.term" and "term" are
equal is lost when comparing module's inferred signature with the
required one (?). Compiling with "-short-paths" to choose "term"
as a representative of "Th.term" does not resolve the problem.

File attachments
@vicuna
Copy link
Author

vicuna commented Mar 14, 2017

Comment author: @garrigue

Since there is no specification for recursive modules, there are no bugs :-)

@vicuna vicuna added the typing label Mar 14, 2019
@github-actions
Copy link

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 11, 2020
@jberdine
Copy link
Contributor

Still repros FWIW. Do I understand correctly that this is an instance of classic "double-vision"?

@lpw25
Copy link
Contributor

lpw25 commented May 11, 2020

This is worse than double-vision. In normal double-vision issues the compiler is not aware that a type and the same type accessed via recursion are the same. Here, we are getting some kind of principality failure because the type-checker is treating two types that are known to equal differently.

@github-actions github-actions bot removed the Stale label Jun 15, 2020
@github-actions
Copy link

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 Jun 16, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature-wish recursive-modules Stale typing
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@nojb @jberdine @lpw25 @vicuna