From 3d131c44f5e89e8d5d761c6a034b15fb89b79595 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 25 Jun 2026 14:33:28 +0200 Subject: [PATCH] emit error when overrinding a subtype with a type that is not a subtype with compatible base type and predicate --- src/ecCoreSubst.ml | 7 +++++++ src/ecCoreSubst.mli | 9 +++++---- src/ecThCloning.ml | 2 ++ src/ecThCloning.mli | 2 ++ src/ecTheoryReplay.ml | 23 ++++++++++++++++++++--- src/ecUserMessages.ml | 11 +++++++++++ tests/subtype-override.ec | 15 +++++++++++++++ 7 files changed, 62 insertions(+), 7 deletions(-) create mode 100644 tests/subtype-override.ec diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index cb99d5b5f2..5df52665e9 100644 --- a/src/ecCoreSubst.ml +++ b/src/ecCoreSubst.ml @@ -738,4 +738,11 @@ module Tvar = struct let f_subst ~(freshen : bool) (lv : ident list) (lt : ty list) : form -> form = Fsubst.f_subst_tvar ~freshen (init lv lt) + + let sty_subst ~(freshen : bool) (lv : ident list) (lt : ty list) : (ty * form) option -> (ty * form) option = + let tsubst = init lv lt in + Option.map + (fun (ty, f) -> + ( subst tsubst ty, + Fsubst.f_subst_tvar ~freshen tsubst f )) end diff --git a/src/ecCoreSubst.mli b/src/ecCoreSubst.mli index f829b8d387..7743ee4526 100644 --- a/src/ecCoreSubst.mli +++ b/src/ecCoreSubst.mli @@ -44,10 +44,11 @@ end (* -------------------------------------------------------------------- *) module Tvar : sig - val init : EcIdent.t list -> ty list -> ty Mid.t - val subst1 : (EcIdent.t * ty) -> ty -> ty - val subst : ty Mid.t -> ty -> ty - val f_subst : freshen:bool -> EcIdent.t list -> ty list -> form -> form + val init : EcIdent.t list -> ty list -> ty Mid.t + val subst1 : (EcIdent.t * ty) -> ty -> ty + val subst : ty Mid.t -> ty -> ty + val f_subst : freshen:bool -> EcIdent.t list -> ty list -> form -> form + val sty_subst : freshen:bool -> EcIdent.t list -> ty list -> (ty * form) option -> (ty * form) option end (* -------------------------------------------------------------------- *) diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 121a108580..c84c8ed026 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -15,6 +15,8 @@ type incompatible = | DifferentType of EcTypes.ty * EcTypes.ty | OpBody (* of (EcPath.path * EcDecl.operator) * (EcPath.path * EcDecl.operator) *) | TyBody (* of (EcPath.path * EcDecl.tydecl) * (EcPath.path * EcDecl.tydecl) *) +| SubtypeType of (EcTypes.ty * EcTypes.ty option) +| SubtypePred of (EcAst.form * EcAst.form) type ovkind = | OVK_Type diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli index 4720f2cbcd..9b36f67884 100644 --- a/src/ecThCloning.mli +++ b/src/ecThCloning.mli @@ -9,6 +9,8 @@ type incompatible = | DifferentType of EcTypes.ty * EcTypes.ty | OpBody (* of (EcPath.path * EcDecl.operator) * (EcPath.path * EcDecl.operator) *) | TyBody (* of (EcPath.path * EcDecl.tydecl) * (EcPath.path * EcDecl.tydecl) *) +| SubtypeType of (EcTypes.ty * EcTypes.ty option) +| SubtypePred of (EcAst.form * EcAst.form) type ovkind = | OVK_Type diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 9d2e25be3b..1dd4e9ecc9 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -187,12 +187,22 @@ end = struct let tparams = List.map tvar params in let ty_body1 = tyd1.tyd_type in let ty_body2 = EcSubst.open_tydecl tyd2 tparams in + let subtype1 = CS.Tvar.sty_subst ~freshen:false tyd1.tyd_params tparams tyd1.tyd_subtype in + let subtype2 = CS.Tvar.sty_subst ~freshen:false tyd2.tyd_params tparams tyd2.tyd_subtype in let hyps = EcEnv.LDecl.init env params in match ty_body1, ty_body2 with - | Abstract, _ -> () - + | Abstract, _ -> begin + match subtype1, subtype2 with + | Some (ty1, f1), Some (ty2, f2) -> + if not (EcReduction.EqTest.for_type (toenv hyps) ty1 ty2) then + raise (Incompatible (SubtypeType (ty1, Some ty2))); + if not (EcReduction.is_conv ~ri:ri_compatible hyps f1 f2) then + raise (Incompatible (SubtypePred (f1, f2))) + | Some (ty1, _), None -> raise (Incompatible (SubtypeType (ty1, None))) + | _, _ -> () + end | _, _ -> tybody hyps ty_body1 ty_body2 with CoreIncompatible -> raise (Incompatible TyBody) @@ -428,12 +438,18 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd nargs in let ue = EcUnify.UniEnv.create (Some nargs) in let ntyd = EcTyping.transty EcTyping.tp_tydecl env ue ntyd in + let subtype = + match ntyd.ty_node with + | Tconstr (p, tys) -> + let reftyd = EcEnv.Ty.by_path p env in + CS.Tvar.sty_subst ~freshen:false reftyd.tyd_params tys reftyd.tyd_subtype + | _ -> None in let decl = { tyd_params = nargs; tyd_type = Concrete ntyd; tyd_loca = otyd.tyd_loca; tyd_clinline = (mode <> `Alias); - tyd_subtype = None; } + tyd_subtype = subtype; } in (decl, ntyd) @@ -459,6 +475,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | `Direct ty -> begin assert (List.is_empty otyd.tyd_params); + assert (otyd.tyd_subtype = None); let decl = { tyd_params = []; tyd_type = Concrete ty; diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index dc8e0947d1..763bec43a8 100644 --- a/src/ecUserMessages.ml +++ b/src/ecUserMessages.ml @@ -839,6 +839,17 @@ end = struct Format.fprintf fmt "incompatible body" | TyBody -> Format.fprintf fmt "incompatible type declaration" + | SubtypeType (ty1, None) -> + Format.fprintf fmt "incompatible type. Not a subtype of %a" + (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty1 + | SubtypeType (ty1, Some ty2) -> + Format.fprintf fmt "incompatible type. The type is a subtype of %a instead of %a" + (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty2 + (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty1 + | SubtypePred (f1, f2) -> + Format.fprintf fmt "incompatible predicate for subtypes. The predicate for the subtype is %a instead of %a" + (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv env)) f2 + (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv env)) f1 let pp_clone_error env fmt error = let msg x = Format.fprintf fmt x in diff --git a/tests/subtype-override.ec b/tests/subtype-override.ec new file mode 100644 index 0000000000..f27b7b3013 --- /dev/null +++ b/tests/subtype-override.ec @@ -0,0 +1,15 @@ +require Subtype. + +theory T1. + subtype s = {b: bool | b}. + realize inhabited by exists true. +end T1. + +subtype s = {b: bool | !b}. +realize inhabited by exists false. + +fail clone T1 as T2 with +type s <- s, +op insub <- insub, +op val <- val +proof *.