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".