Type parameter in subtype causes unbound type parameter

[oskgo]

Related to #1001, but without sections.

When using type parameters in subtypes this yields operators, types and lemmas that may use the parameter but where it is not bound by the operator, type or lemma in question.

MRE:

require Subtype.
theory T.
subtype s = {x: 'a | true}.
realize inhabited by exists witness.
end T.
print T.

Ideally this should do the same as if 'a was a type declared in a section that's closed after the definition, but if support for parametric subtypes without sections is postponed this should just be prevented.

As before there is also a variant of this issue with parametric predicate rather than type. MRE:

require Subtype.
theory T.
subtype s = {x: unit | if (forall (x, y: 'a), x = y) then true else x = witness}.
realize inhabited by exists witness.
end T.
print T.

EDIT: This does not seem to be a soundness issue. The unbound type parameter cannot be instantiated, so it behaves as a concrete type about which nothing is known.

[strub]

In fact, 'a should not even be accepted.