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

Infinite loop in type checker with module aliases #6954

vicuna opened this issue Aug 6, 2015 · 1 comment

Infinite loop in type checker with module aliases #6954

vicuna opened this issue Aug 6, 2015 · 1 comment


Copy link

@vicuna vicuna commented Aug 6, 2015

Original bug ID: 6954
Reporter: @mmottl
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-02-16T14:14:48Z)
Resolution: fixed
Priority: high
Severity: major
Version: 4.02.3
Fixed in version: 4.03.0+dev / +beta1
Category: typing
Monitored by: @hcarty @mmottl

Bug description

The following code snippet will make the type checker go into an infinite loop. Please disregard the Obj.magic, it's just for convenience to cut down the test case size. My original code (way too large to be helpful) does not use unsafe features.

module X = struct module Y = struct module type S = sig type t end end end

(* open X (* works! *) *)
module Y = X.Y

module type Arg = sig
module A : sig type 'a t constraint 'a = (module Y.S with type t = 'at) end

module MyA = struct
(* type 'a t = 'at constraint 'a = (module X.Y.S with type t = 'at) (* works! *) *)
type 'a t = 'at constraint 'a = (module Y.S with type t = 'at)

module Make (Arg : Arg with module A = MyA) = struct
type t = (module X.Y.S with type t = unit)
let x : t Arg.A.t = Obj.magic 0

The bug is triggered by the last "x" binding. Obviously, the object magic should always allow unification here so the problem is really on the left-hand side only. The constraint checking on "t" when applying "Arg.A.t" is the presumptive cause of the problem.

The bug is apparently related to module aliases for somewhat nested structures. Uncommenting one of the "works!" lines while commenting out the respective subsequent line will make the compiler accept the code again.

Copy link

@vicuna vicuna commented Oct 16, 2015

Comment author: @garrigue

Fixed in trunk at revision 16509.

Using a fixpoint for expansion was not a good idea...
Twice should be enough in practice.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
None yet

No branches or pull requests

2 participants