Soundness bug with non-generalized type variable and functors

[vicuna]

Original bug ID: 7414
Reporter: @lpw25
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-11-21T13:22:14Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.04.0
Fixed in version: 4.05.0 +dev/beta1/beta2/beta3/rc1
Category: typing
Related to: #6752
Monitored by: @gasche @yallop

Bug description

The interplay between non-generalized type variables and functors seems ill defined and unsound. Using first-class modules we can get a segfault:

module type T = sig
type t
val x : t
val show : t -> string
end

module Int = struct
type t = int
let x = 0
let show x = string_of_int x
end

module String = struct
type t = string
let x = "Hello"
let show x = x
end

let switch = ref true

module Choose () = struct
module Choice =
(val if !switch then (module Int : T)
else (module String : T))
let r = ref (ref [])
end

module type S = sig
module Choice : T
val r : Choice.t list ref ref
end

module Force (X : functor () -> S) = struct end

module M = Choose ()

let () = switch := false

module N = Choose ()

let () = N.r := !M.r

module Ignore = Force(Choose)

module M' = (M : S)

let () = (!M'.r) := [M'.Choice.x]

module N' = (N : S)

let () = List.iter (fun x -> print_string (N'.Choice.show x)) !(!N'.r)

[vicuna]

Comment author: @garrigue

I've created a pull-request #929 with a fix.
Note that the current fix is not very efficient, so I will revise it before merging,
to use an iterator rather than Subst.modtype.

[vicuna]

Comment author: @garrigue

Merged the pull request in commit 2bd2296.
Now handled by a visit of the signature rather than by Subst.