feat: newtype for (non-map) collection types

[RustanLeino]

Description

This PR adds support for a newtype to use set/iset/seq/multiset as its base type. This includes type inference/checking, verification, and compilation to all targets. For example, one can now declare types like

newtype FourInts = s: seq<int> | |s| == 4 && s[0] + s[1] == s[2] witness [2, 3, 5, 7]

newtype String = s: string | |s| < 0x8000_0000

using --type-system-refresh --general-newtypes.

• A newtype defined in this way obtains new versions of the constructors of the base type. For example, just like the constructor 7 of int also becomes a constructor for a newtype-int, the multiset{...} becomes a constructor for any newtype-multiset and "hello" becomes a constructor for newtype-seq<char>.

• Every built-in operator, say, of type B * B -> B, of the base type B becomes a built-in operator of type N * N -> N of the newtype-B N. For example, + becomes a operator on String above. As usual for newtypes, when the result of such an operator is a newtype, the constraint is checked.

• For these purposes, the subsequence expressions s[_.._] are operators (returning something of the same type as s) if the type of s is a sequence, and are constructors (returning any sequence type) if s is an array type.

• Built-in functions, like multiset(_), that take collections as inputs or outputs, are extended to work with newtypes as well.

• Other places where collections can be used (for example, frames and the argument to fresh) are extended to work with newtypes as well.

Not including in this PR (but in upcoming PRs) are support for:

• newtype based on map
• newtype with type parameters (but the base type can be a type with type parameters, provided they are filled in, like seq<int> in the example above)
• members of general newtypes (may work partially, but has not been tested)

Comments for reviewers

• In a great number of places, the change required to support these general newtypes was to change .NormalizeExpand() to .NormalizeToAncestorType(). For example, this occurs frequently in contexts like expr.Type.NormalizeToAncestorType().AsSeqType. It's possible that it would be better to change .AsSeqType to do the .NormalizeToAncestorType() internally (so that uses could look like expr.Type.AsSeqType). However, I'd rather hold off on such changes until all the newtype work is done. At that time, we can better evaluate how much of the uses of .AsSeqType need the ancestor type.

• Supporting the general newtypes during the type-adjustment phase required a new kind of flow, FlowFromComputedTypeIgnoreHeadTypes, as a variation of the existing FlowFromComputedType. The new flow works on the ancestor of the sink type (for example, it applies to seq<int> instead of FourInts).

• Arrow types are not supported as newtype base types (in fact, I'm wondering if they ever should be). This check was previously omitted.

• I improved printing of arrow types in pre-type error messages. It might seem that subset types like --> and -> should never need to be printed during pre-type inference, but they can appear if the user input declares the types as such.

• I split up the Advice class into two subclasses, CommonAdvice and TypeAdvice. The latter supports types other than built-in parameter-less types.

• I improved pre-type inference to make non-committal use of advice earlier.

• I fixed a bug (a glaring omission) in the MeetHeads method in PreTypeConstraints.cs.

• Saying that a result type is a collection type or newtype-collection type requires some setup. I did a little refactoring so that this new setup can share code.

• I fixed a bug in an error-message format string (that could cause a crash).

• I fixed two bugs in the type inference of - and >, where the result was not checked to be of an appropriate type.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

It would help me if we extend the text in docs/dev/TypeSystemRefresh.md to further elaborate on how things work and why.

I think I would prefer having a minimum set of example programs and how we want to infer types for them, as a way of explaining the requirements of the type inference system.

Next to that, if there's passes that can be described as constraint solving problems, it would help me to know what the possible states (type expressions) of the nodes (variables/expression) are.

Also, it might be good to describe the 'space' of types. For example, the pre-types might live in a lattice, and full types might be a generalization where each lattice node is a set of types that all have the same runtime type.

Lastly, have you considered renaming 'type adjustment' to 'type refinement' ? My impression is that this is a transformation that makes types strictly smaller, if you view them as sets of values.

[keyboardDrummer]

Could you add a comment to this class? What is advice for?