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.

[oskgo]

That's one resolution. Another is to accept it, but add it as a parameter to the appropriate lemmas operators and types. We can already do parametric subtypes using sections, so it doesn't matter much which one we go for, though it would be a bit weird to have a feature that's only accessible using sections.

[oskgo]

On second thought, I guess you already need to use sections to inject type parameters into clones, so that's a very weak argument.