subtype: generalize over section-declared free types at section close

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) =

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

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

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 [

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 ->

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) =

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

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.