SI-6923 Context now buffers warnings as well as errors

Code that was silently typed would not report warnings, even if it
returned a successful result.

This appeared in the following code which didn't show warnings even
with -Ywarn-adapted-args:

    def foo(a: Any) = a; foo(1, 2)

While the following would show the expected warning:

    def foo[A](a: Any) = a; foo(1, 2)
SI-6601 Publicise derived value contstructor after pickler

Otherwise the access restrictions are not enforced under
separate compilation.

See also SI-6608.
Merge pull request #1905 from adriaanm/ticket-6956

SI-6956 determine switchability by type, not tree
Merge pull request #1854 from pufuwozu/ticket-SI-6923

SI-6923 Context now buffers warnings as well as errors
Merge pull request #1914 from retronym/ticket/6601

SI-6601 Publicise derived value contstructor after pickler
SI-6942 more efficient unreachability analysis

Avoid blowing the stack/the analysis budget by more eagerly translating
the propositions that model matches to CNF.
First building a large proposition that represents the match,
and then converting to CNF tends to blow the stack.
Luckily, it's easy to convert to CNF as we go.

The optimization relies on `CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)`:

Normalizing a conjunction of propositions
    yields the same formula as
concatenating the normalized conjuncts.

CNF conversion is expensive for large propositions,
so we push it down into the conjunction and
then concatenate the resulting arrays of clauses (which is cheap).

(CNF converts a free-form proposition into an `Array[Set[Lit]]`, where:
 - the Array's elements are /\'ed together;
 - and the Set's elements are \/'ed;
 - a Lit is a possibly negated variable.)

NOTE: removeVarEq may throw an AnalysisBudget.Exception

use arraybuffer to build formula

interface work
use ArrayBuffer instead of Array to build Formulae