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

unterminating type checking for recursive modules #3674

Open
vicuna opened this issue Jun 7, 2005 · 4 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented Jun 7, 2005

Original bug ID: 3674
Reporter: administrator
Status: acknowledged
Resolution: won't fix
Priority: normal
Severity: feature
Target version: later
Category: typing
Tags: recmod
Related to: #3935
Monitored by: "Julien Signoles" "Keiko NAKATA"

Bug description

Full_Name: Keiko NAKATA
Version: 3.08.2
OS: FreeBSD
Submission from: orion.kurims.kyoto-u.ac.jp (130.54.16.5)

Type checking does not terminate against the following program:

module type M = sig
module rec F : functor (X : sig type t end) -> sig type t = F(F(X)).t end

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 29, 2005

Comment author: administrator

Tough example. Will not fix in 3.08.

@vicuna

This comment has been minimized.

Copy link
Author

commented Sep 11, 2012

Comment author: @damiendoligez

Still present in 4.00.1+dev

@vicuna

This comment has been minimized.

Copy link
Author

commented Dec 4, 2015

Comment author: runhang

I am very interesting in why type checking this code will not terminate. Would someone like to spare some time to give a basic explanation?

@vicuna

This comment has been minimized.

Copy link
Author

commented Mar 15, 2017

Comment author: @garrigue

Move it to feature since we have no way to solve this with the current approach.

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.