Original bug ID: 1968
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Full_Name: Jacek Chrzaszcz
Version: 3.07+2
OS: Redhat Linux 7.3
Submission from: fw-gw-atm.mimuw.edu.pl (193.0.96.15)

Hello Camlers!

While testing Coq modules with some insane examples I discovered
a malicious bug in a dark corner of the Caml module system.

Jacek

module type SIG = sig
type t
type u = t
val x:t
val f:t->t
module M : sig end
end

module N : SIG = struct
type t = int
type u = int
let x = 1
let f y = y+1
module M = struct end
end

module type SIGM = SIG with module M=N

module type SIGMt = SIGM with type t=string

(* I suspect that in SIGM (and hence SIGMt) both toplevel t and t in the
signature of
M (and also u and M.u) have the same ident (name and stamp).

Consequently while subtyping the submodule M during
SIGMt/Mt <: SIGKILL below
we get t=u wrongly and the subtyping succeeds *)

module Mt : SIGMt = struct
type t = string
type u = string
let x = "foo"
let f y = y^"bar"
module M = N
end

module type SIGKILL = sig
type t
type u = t
val x:t
val f:t->t
module M : sig type t = u type u = t val x:t val f:t->t end
end

module K:SIGKILL=Mt

let _ = K.f K.M.x (* K.f : string -> string, K.M.x : int *)

(* Here: seqfault *)