-
Andrei Paskevich authored
Type variables that appear in the result types of "pure" or logical functions are "spoiled" and cannot be instantiated with mutable types. Abstract program functions ("val") are assumed to not spoil type variables, and no explicit effect annotation is provided for this effect. Constructors, projections, and function application do not spoil type variables. This effect prevent unsoundness that results from instantiating [constant magic : 'a] with a mutable type in a program. It is, however, less precise than tracking of magic values using pure type variables. For example, the following program does typecheck with pure type variables but not with the spoil effects. use seq.Seq type ref_hist 'a = { mutable contents : 'a; ghost mutable history : Seq.seq {'a} } let (:=) (r : ref_hist 'a) (v : 'a) = r.history <- Seq.cons (pure { r.contents }) r.history; r.contents <- v let test (r : ref_hist (ref_hist unit)) = r := r.contents Indeed, (:=) spoils 'a, and precludes it from being instantiated with a mutable type in "test".
330bd7e5