Ah, I think Stephen meant to write the following: fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int { a := 10 b := 20 (!a + !b) } whe

Ah, I think Stephen meant to write the following: fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int { a := 10 b := 20 (!a + !b) } where indeed the effect is `st<h>` as the updates are observable. How the function was written before, the two arguments use a "rank-2" polymorphic type and the heaps are fully abstract -- in that case it would be unobservable but you cannot create such values :-)