Fix soundness bug with clone overrides of subtypes

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

@@ -191,8 +191,16 @@ end = struct
       let hyps = EcEnv.LDecl.init env params in
 
       match ty_body1, ty_body2 with
-      | Abstract, _ -> ()
-
+      | Abstract, _ -> begin
+        match tyd1.tyd_subtype, tyd2.tyd_subtype 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)
@@ -427,13 +435,21 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
                           (fun x -> (EcIdent.create (unloc x)))
                           nargs in
             let ue    = EcUnify.UniEnv.create (Some nargs) in
+            let subtype =
+              match unloc ntyd with
+              | PTnamed (s) -> begin
+                match EcEnv.Ty.lookup_opt s.pl_desc env with
+                | Some (_, { tyd_subtype = Some (ty, f) }) -> Some (ty, f)
+                | _ -> None
+                end
+              | _ -> None in
             let ntyd  = EcTyping.transty EcTyping.tp_tydecl env ue ntyd 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 *.