Cannot export mutable field 'x' without revealing its enclosing class 'A'

An example of this error is the code

module M {
    export
        provides A, 
                 A.foo, // want to export foo, which refers to x
                 A.x    // to make export set self-consistent, need to export x

    class A {
        var x: int
        function method foo(): int
          reads this
        {
            x
        }
    }
}

which produces the error

ERROR_MutableField.dfy(5,19): Error: Cannot export mutable field 'x' without revealing its enclosing class 'A'
1 resolution/type errors detected in ERROR_MutableField.dfy

By only providing A, importers will know that A is a type, but won’t know that it is a reference type (here, a class). This makes it illegal to refer to a mutable field such as in the reads clause. So, you have to export A by revealing it.

Note, export reveals A does not export the members of A (except, it does export the anonymous constructor of A, if there is one). So, you still have control over which members of A to export.

The following code verifies without error:

module M {
    export
        reveals A
        provides  
                 A.foo, // want to export foo, which refers to x
                 A.x    // to make export set self-consistent, need to export x

    class A {
        var x: int
        function method foo(): int
          reads this
        {
            x
        }
    }
}