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".