Dot: Enable syntactic values in types

[Blaisorblade]

Goal: Enable writing syntactic values in types, for examples such as F.F (\nu z. { A = Int }) (aka, F Int).

To give semantics to such types, we'll use guarded recursion, as in DSub; but we'll combine it with stamping + higher-order ghost state.

Steps:

• Use guarded recursion (Dot: Use guarded recursion to enable syntactic values in types #385)
• Prove extra typing rules
• Encode example? (See below).

[Blaisorblade]

@stuckintheory suggests that this is needed even to write flatten : ∀ x : {A : *}, List x -> List (List x) we can't use let and we need these "inline" types. (flatMap would also work, but map wouldn't trigger it).

There might be DOT-like encoding alternatives, but they won't work if type constructor is abstract.