Lost sort information in quantifier blocks causes problems later.

[MichaelRawson]

Filing an issue to track this on behalf of others: I might have this wrong.

QuantifiedFormula keeps an optional list of sorts for each variable in a quantifier block, otherwise the sorts have to be computed later. However, lots of inferences (e.g. rectification, theory normalisation) do not supply sort information where they could. This means that sorts have to be recomputed later, which may be pathological or even a bug in some cases.

To fix this, we should pass the sort information through where it's reasonably available.