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
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)
end

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
end

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.