One exception to this rule is the the result type in a non-recursive
function may contain regions coming the function's arguments (though
not from the context). It is sometimes useful to write a function
around a constructor or a projection: see function [create] in
verifythis_fm2012_LRS.mlw. For recursive functions we impose
the full non-alias discipline.

Now that ghost writes are checked via e_syms.syms_pv,
there is no use for read effects anymore.

This fixes one bug and several deficiencies in the previous
implementation, which was based on read effects. One caveat
about the current version is that we treat all type variables
in a polymorphic type as visible (= non-ghost) even if they
only occur in the ghost fields. For example, the following
code is rejected:

  type strange 'a = { ghost contents : 'a }

  let test () =
    let x = { contents = ref 0 } in
    x.contents := 42

Even though the field [contents] is ghost and cannot be reached
from the real-world code, the type of x is [strange (ref int)]
and the region of the reference is considered to be visible.
Thus the last assignment is seen as an illicit ghost write.

On the other hand,

  type strange 'a = { ghost contents : ref 'a }

and

  type strange 'a = { ghost mutable contents : 'a }

permit ghost writes into [contents] without problem.
Ghost writes into ghost variables are also okay.

keep the word reserved, though

this commit changes the way of tracking occurrences of regions
and type variables for the purposes of generalization, effect
filtering, and effect checks. It restricts the previous
implementation in two aspects:

- a psymbol p can be monomorphic (= non-generalizable) in an effect
  only if p depends (= is defined via) a pvsymbol whose type contains
  the affected region. See bench/programs/bad-typing/recfun.mlw
  for an example. This restriction is required for soundness.

- an argument of a psymbol cannot contain a region shared with
  another argument or an external pvsymbol. However, we do not
  require (so far) that the argument's type doesn't contain the same
  region twice and we allow the result type to contain known regions.
  This restriction is not necessary for soundness, and is introduced
  only to avoid some unintentional user errors and reduce the gap
  between the types that can be implemented in a "let" and the types
  that can be declared in a "val".