Auto-dereferencing references:

    let &x = ... in                     let (x: ref ...) = ... in
    f x;                    ---->       f x.contents;
    x <- ...                            x.contents <- ...

  -- recommended sugar:

    let ref x = ...          ==>        let &x = ref ...

  The & marker adds the typing constraint (x: ref ...)

  Top-level "let/val ref" and "let/val &" are allowed.

  Auto-dereferencing works in logic, but such variables
  cannot be introduced inside logical terms.

Extension to pattern matching:

    match e with                        match e with
    | (x,&y) -> y           ---->       | (x,(y: ref ...)) -> y.contents
    end                                 end

Extension to function parameters and reference passing:

    let incr (&x: ref int) =            let incr (x: ref int) =
      x <- x + 1                          x.contents <- x.contents + 1
                            ---->
    let f () =                          let f () =
 ...