Behave differently from the type system

[aigarashi]

The following program is verified in the current implementation, (and it's logically correct)
but it's not type-checked in the type system.

{
    let x = mkref 1 in 
    let y = x in 
    let a = *y in
    let b = *y in  {
        x := 2; 
        assert(a = b)
    }
}