From 4bb149e3107f97931dc01520c70d812ec476b60b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 8 May 2026 07:45:03 +0200 Subject: [PATCH] subtype: generalize over section-declared free types at section close MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit [subtype X = { x : T | P x }] declared inside [section. declare type c. ...] previously stayed monomorphic at section close. The cloned auto-axioms ([insubN], [insubT], [valP], [valK]) and the [val] / [insub] operators correctly gained a [c] tparam, but [X] itself didn't — the result was an inconsistent state where the operations were polymorphic over [c] but returned a single shared [X] type for every instantiation, a soundness gap flagged by [FIXME:SUBTYPE] at [add_subtype]. This patch threads the carrier and predicate through the subtype's [tydecl] so [tydecl_fv] picks up their dependency on section-declared free types and the existing [generalize_tydecl] machinery adds the right tparams at close. Tests in [tests/subtype-section-generalize.ec] cover three cases: 1. carrier mentions a section-declared free type — subtype is unary. 2. predicate mentions a section-declared free type (carrier doesn't) — same outcome via fv collected from the predicate. 3. nested sections, subtype declared in the inner one, depending on free types from both levels — subtype is binary after both closes. Each test instantiates [val] and [valP] at two distinct carriers in a single lemma; would fail to type-check if the cloned type or axiom had stayed monomorphic. --- src/ecDecl.ml | 12 ++-- src/ecDecl.mli | 15 +++- src/ecHiInductive.ml | 1 + src/ecScope.ml | 18 ++--- src/ecSection.ml | 10 ++- src/ecSubst.ml | 7 +- src/ecTheoryReplay.ml | 6 +- tests/subtype-section-generalize.ec | 104 ++++++++++++++++++++++++++++ 8 files changed, 154 insertions(+), 19 deletions(-) create mode 100644 tests/subtype-section-generalize.ec diff --git a/src/ecDecl.ml b/src/ecDecl.ml index 2dbd8b27c..42af1b670 100644 --- a/src/ecDecl.ml +++ b/src/ecDecl.ml @@ -35,9 +35,10 @@ type ty_body = type tydecl = { - tyd_params : ty_params; - tyd_type : ty_body; - tyd_loca : locality; + tyd_params : ty_params; + tyd_type : ty_body; + tyd_loca : locality; + tyd_subtype : (EcTypes.ty * EcCoreFol.form) option; } let tydecl_as_concrete (td : tydecl) = @@ -65,7 +66,10 @@ let abs_tydecl ?(params = `Int 0) lc = (EcUid.NameGen.bulk ~fmt n) in - { tyd_params = params; tyd_type = Abstract; tyd_loca = lc; } + { tyd_params = params; + tyd_type = Abstract; + tyd_loca = lc; + tyd_subtype = None; } (* -------------------------------------------------------------------- *) let ty_instantiate (params : ty_params) (args : ty list) (ty : ty) = diff --git a/src/ecDecl.mli b/src/ecDecl.mli index db24d1950..b121a50a6 100644 --- a/src/ecDecl.mli +++ b/src/ecDecl.mli @@ -30,9 +30,18 @@ type ty_body = type tydecl = { - tyd_params : ty_params; - tyd_type : ty_body; - tyd_loca : locality; + tyd_params : ty_params; + tyd_type : ty_body; + tyd_loca : locality; + (* For [subtype]-declared types: the carrier and the predicate. The + declared type itself stays [tyd_type = Abstract], because a + subtype is semantically a fresh abstract type — but its dependency + on free type variables (when declared inside a section) must be + visible to the section-close machinery. [tydecl_fv] unions the + carrier+predicate fv into the type's fv when this field is set, + so a subtype declared inside [section. declare type c.] gets the + section's tparams added at close, just like type aliases do. *) + tyd_subtype : (EcTypes.ty * EcCoreFol.form) option; } val tydecl_as_concrete : tydecl -> EcTypes.ty option diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml index 9084f1118..aa05ac3f3 100644 --- a/src/ecHiInductive.ml +++ b/src/ecHiInductive.ml @@ -86,6 +86,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) = tyd_params = EcUnify.UniEnv.tparams ue; tyd_type = Abstract; tyd_loca = lc; + tyd_subtype = None; } in EcEnv.Ty.bind (unloc name) myself env in diff --git a/src/ecScope.ml b/src/ecScope.ml index 989174512..28ad1a2f9 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -2296,20 +2296,14 @@ module Ty = struct record.ELI.rc_tparams, Record (scheme, record.ELI.rc_fields) in - bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; }) + bind scope (unloc name, + { tyd_params; tyd_type; tyd_loca; tyd_subtype = None; }) (* ------------------------------------------------------------------ *) let add_subtype (scope : scope) ({ pl_desc = subtype } : psubtype located) = let loced x = mk_loc _dummy x in let env = env scope in - let scope = - let decl = EcDecl.{ - tyd_params = []; - tyd_type = Abstract; - tyd_loca = `Global; (* FIXME:SUBTYPE *) - } in bind scope (unloc subtype.pst_name, decl) in - let carrier = let ue = EcUnify.UniEnv.create None in transty tp_tydecl env ue subtype.pst_carrier in @@ -2326,6 +2320,14 @@ module Ty = struct let fs = Tuni.subst uidmap in f_lambda [(x, GTty carrier)] (Fsubst.f_subst fs pred) in + let scope = + let decl = EcDecl.{ + tyd_params = []; + tyd_type = Abstract; + tyd_loca = `Global; + tyd_subtype = Some (carrier, pred); + } in bind scope (unloc subtype.pst_name, decl) in + let evclone = { EcThCloning.evc_empty with evc_types = Msym.of_list [ diff --git a/src/ecSection.ml b/src/ecSection.ml index 828baaf9e..901597418 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -730,6 +730,13 @@ let tydecl_fv tyd = | Record (_f, l) -> List.fold_left (fun fv (_, ty) -> EcIdent.fv_union fv (ty_fv_and_tvar ty)) Mid.empty l in + let fv = + match tyd.tyd_subtype with + | None -> fv + | Some (carrier, pred) -> + EcIdent.fv_union + (EcIdent.fv_union fv (ty_fv_and_tvar carrier)) + (fv_and_tvar_f pred) in List.fold_left (fun fv id -> Mid.remove id fv) fv tyd.tyd_params let op_body_fv body ty = @@ -863,7 +870,8 @@ let generalize_tydecl to_gen prefix (name, tydecl) = let to_gen = { to_gen with tg_subst} in let tydecl = { tyd_params; tyd_type; - tyd_loca = `Global; } in + tyd_loca = `Global; + tyd_subtype = tydecl.tyd_subtype; } in to_gen, Some (Th_type (name, tydecl)) | `Declare -> diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 107aba6e0..8bae12c68 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -868,10 +868,15 @@ let subst_tydecl_body (s : subst) (tyd : ty_body) = let subst_tydecl (s : subst) (tyd : tydecl) = let s, tparams = fresh_tparams s tyd.tyd_params in let body = subst_tydecl_body s tyd.tyd_type in + let subtype = + Option.map + (fun (carrier, pred) -> (subst_ty s carrier, subst_form s pred)) + tyd.tyd_subtype in { tyd_params = tparams; tyd_type = body; - tyd_loca = tyd.tyd_loca; } + tyd_loca = tyd.tyd_loca; + tyd_subtype = subtype; } (* -------------------------------------------------------------------- *) let rec subst_op_kind (s : subst) (kind : operator_kind) = diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index de60a2a63..8982a3493 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -431,7 +431,8 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd let decl = { tyd_params = nargs; tyd_type = Concrete ntyd; - tyd_loca = otyd.tyd_loca; } + tyd_loca = otyd.tyd_loca; + tyd_subtype = None; } in (decl, ntyd) @@ -451,7 +452,8 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd let decl = { tyd_params = []; tyd_type = Concrete ty; - tyd_loca = otyd.tyd_loca; } + tyd_loca = otyd.tyd_loca; + tyd_subtype = None; } in (decl, ty) end diff --git a/tests/subtype-section-generalize.ec b/tests/subtype-section-generalize.ec new file mode 100644 index 000000000..85aaaab4a --- /dev/null +++ b/tests/subtype-section-generalize.ec @@ -0,0 +1,104 @@ +require import AllCore. +require Subtype. + +(* Generic abstract predicates declared outside any section so they + stay polymorphic instead of being generalized when the section is + closed. *) +op P ['c] : int -> 'c -> bool. +op Q ['c] : int -> 'c -> bool. +op R ['o 'i] : 'o -> 'i -> bool. + +axiom P_sat ['c] : exists n, P<:'c> n witness. +axiom Q_sat ['c] : exists n, Q<:'c> n witness. +axiom R_sat ['o 'i] : R<:'o, 'i> witness witness. + + +(* -------------------------------------------------------------------- *) +(* Basic case: subtype inside a section with a single section-declared *) +(* free type. The subtype must be generalized over [c] at section *) +(* close so that [val]/[insub] (which gain a [c] tparam) and the type *) +(* itself stay coherent. *) +(* -------------------------------------------------------------------- *) +theory T1. +section. +declare type c. + +subtype carrier = { x : int * c | P x.`1 x.`2 }. + +realize inhabited. proof. by have [n hn] := P_sat<:c>; exists (n, witness). qed. + +end section. +end T1. + +(* After section close, [carrier] is unary. Using it at two distinct + carrier types in the same lemma produces two distinct types — would + fail to type-check if [carrier] had stayed monomorphic. *) +lemma test_basic_unary (x : bool T1.carrier) (y : int T1.carrier) : + T1.val x = (0, witness<:bool>) /\ T1.val y = (1, witness<:int>). +proof. admit. qed. + + +(* -------------------------------------------------------------------- *) +(* Predicate-only dependency: the carrier mentions no section-declared *) +(* type, but the predicate does (the polymorphic [Q] is instantiated at *) +(* the section's [c]). The fv collected from the predicate must trigger *) +(* the same generalization. *) +(* -------------------------------------------------------------------- *) +theory T2. +section. +declare type c. + +subtype only_pred = { x : int | Q<:c> x witness }. + +realize inhabited. proof. exact: Q_sat. qed. + +end section. +end T2. + +lemma test_pred_dep_unary (x : bool T2.only_pred) (y : int T2.only_pred) : + T2.val x = 0 /\ T2.val y = 1. +proof. +(* The subtype-cloned [valP] axiom must itself be polymorphic over the + carrier — instantiating it at two distinct types here would fail to + type-check if the generalization had not happened. *) +have hx : Q<:bool> (T2.val x) witness by exact: T2.valP. +have hy : Q<:int> (T2.val y) witness by exact: T2.valP. +admit. +qed. + + +(* -------------------------------------------------------------------- *) +(* Two nested sections. The subtype is declared in the inner section *) +(* and depends on free types from BOTH levels. After both closes, it *) +(* must be generalized over both [outer] and [inner]. *) +(* -------------------------------------------------------------------- *) +theory T3. +section Outer. +declare type outer. + +section Inner. +declare type inner. + +subtype pair_carrier = { x : outer * inner | R x.`1 x.`2 }. + +realize inhabited. +proof. by exists (witness, witness); exact: R_sat. qed. + +end section Inner. +end section Outer. +end T3. + +(* Now [pair_carrier] should be binary. *) +lemma test_nested_binary + (x : (int, bool) T3.pair_carrier) + (y : (bool, int) T3.pair_carrier) +: + T3.val x = (0, true) /\ T3.val y = (true, 0). +proof. +(* As in T2, instantiating [valP] at two distinct carrier pairs would + fail to type-check if the cloned axiom had not been generalized + over both [outer] and [inner]. *) +have hx : R<:int, bool> (T3.val x).`1 (T3.val x).`2 by exact: T3.valP. +have hy : R<:bool, int> (T3.val y).`1 (T3.val y).`2 by exact: T3.valP. +admit. +qed.