Fix soundness bug with clone overrides of subtypes

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

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
 
 (* -------------------------------------------------------------------- *)

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

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

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;

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

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