Subtype inside a section is not generalized over section-declared free types at section close (soundness gap)

[strub]

Summary

When a subtype declaration appears inside a section and depends on a section-declared free type, the resulting type does not get generalized over that type at section close, even though the auto-generated operations and axioms are. The result is an inconsistent state where the operations/axioms are polymorphic but the underlying type is shared across all instantiations — a soundness gap.

Repro

section.
declare type c.

subtype carrier = { x : int * c | true }.

end section.

print carrier.
print to_carrier.

After section close:

• carrier is bound with tyd_params = [] — a single, shared type for all 'c.
• to_carrier / of_carrier / the auto-axioms (to_carrierN, of_carrierP, of_carrierK) are correctly polymorphic over 'c.

The same carrier type is shared across every instantiation of 'c, while the operations claim to take 'c as a parameter. The conjunction is unsound: from an axiom about carrier derived under one 'c you can specialise the operations at a different 'c.

Why

generalize_tydecl at section close uses tydecl_fv to find which section-declared types a tydecl depends on. For a subtype, tyd_type is an opaque Abstract marker — it does not contain the carrier expression or the predicate, so tydecl_fv returned an empty fv set. The auto-generated ops/axioms, in contrast, contain the carrier and predicate explicitly in their type/spec, so the section-close pass correctly added tparams to them.

Expected

After section close, the subtype is generalized over every section-declared free type its carrier or predicate mentions, matching the generalization of its auto-generated ops and axioms.

[oskgo]

This is the issue I mentioned in #275 (comment), right?

There's also the related issue mentioned in #275 (comment) when the predicate depends on the type parameter.

See MRE:

require Subtype.

op unital ['a] = forall (x y: 'a), x = y.

theory T.
section.
declare type c.

subtype carrier = { x : int | if unital<:c> then true else witness = x}.
realize inhabited by exists witness.

end section.
end T.

print T.

This currently makes the axioms parametric, but not the operators.