Instantiation of mutable type symbol when cloning
There are several problems in cloning when dealing with mutable type symbols.
- One cannot instantiate a private mutable type with a type application:
module A0
type t = private mutable {}
end
module A1
use import ref.Ref
clone A0 with type t = ref int
end
fail with error Illegal instantiation for symbol t
. However, replacing ref int
by an alias works. This problem only arises for abstract mutable types.
- If one instantiate a private mutable type
t
with a non-mutable type in a module which also contains aval
taking an element oft
as argument:
module A0
type t = private mutable {}
val g (x:t) : unit
end
module A1
use import list.List
type u = list int
clone A0 with type t = u
end
why3 crash with exception Invalid_argument("Ity.create_region")
.
- If one attempt to instantiate a non-mutable type with a mutable one, why3 silently accept the substitution by transforming the mutable type into its snapshot. This lead to unexpected type errors in other places:
module A0
type t
val g (x:t) : unit
end
module A1
use import ref.Ref
type u = ref int
let g (x:u) : unit = x := 0
clone A0 with type t = u, val g = g
end
result in an error when instantiating A0.g
by A1.g
:
This application expects a mutable type but receives {ref int}
.