replay: redirect datatype constructors in match bodies too

src/ecSubst.ml

@@ -27,6 +27,7 @@ exception InconsistentSubst
 type subst = {
   sb_module   : EcPath.mpath Mid.t;
   sb_path     : EcPath.path Mp.t;
+  sb_ctor     : EcPath.path Mp.t;
   sb_tyvar    : ty Mid.t;
   sb_elocal   : expr Mid.t;
   sb_flocal   : EcCoreFol.form Mid.t;
@@ -40,6 +41,7 @@ type subst = {
 let empty : subst = {
   sb_module   = Mid.empty;
   sb_path     = Mp.empty;
+  sb_ctor     = Mp.empty;
   sb_tyvar    = Mid.empty;
   sb_elocal   = Mid.empty;
   sb_flocal   = Mid.empty;
@@ -52,6 +54,7 @@ let empty : subst = {
 let is_empty s =
   Mid.is_empty s.sb_module
   && Mp.is_empty s.sb_path
+  && Mp.is_empty s.sb_ctor
   && Mid.is_empty s.sb_tyvar
   && Mid.is_empty s.sb_elocal
   && Mid.is_empty s.sb_flocal
@@ -272,6 +275,10 @@ let add_path (s : subst) ~src ~dst =
   assert (Mp.find_opt src s.sb_path = None);
   { s with sb_path = Mp.add src dst s.sb_path }
 
+(* -------------------------------------------------------------------- *)
+let add_ctor (s : subst) ~src ~dst =
+  { s with sb_ctor = Mp.add src dst s.sb_ctor }
+
 let add_tydef (s : subst) p (ids, ty) =
   assert (Mp.find_opt p s.sb_tydef = None);
   { s with sb_tydef = Mp.add p (ids, ty) s.sb_tydef }
@@ -932,7 +939,15 @@ and subst_branches (s : subst) = function
   | OPB_Branch bs ->
       let for1 b =
         let (ctorp, ctori) = b.opb_ctor in
-          { opb_ctor = (subst_path s ctorp, ctori);
+        (* A branch constructor is stored as a bare path. When the datatype's
+           type has been overridden while cloning, it is redirected to the
+           target datatype's constructor, which is recorded separately from
+           the path substitution: the latter also rewrites the paths that its
+           entries qualify, which a constructor must not do. *)
+        let ctorp =
+          Option.value (Mp.find_opt ctorp s.sb_ctor)
+            ~default:(subst_path s ctorp) in
+          { opb_ctor = (ctorp, ctori);
             opb_sub  = subst_branches s b.opb_sub; }
       in
         OPB_Branch (Parray.map for1 bs)

src/ecSubst.mli

@@ -25,6 +25,7 @@ val is_empty : subst -> bool
 (* -------------------------------------------------------------------- *)
 val add_module   : subst -> EcIdent.t -> mpath -> subst
 val add_path     : subst -> src:path -> dst:path -> subst
+val add_ctor     : subst -> src:path -> dst:path -> subst
 val add_tydef    : subst -> path -> (EcIdent.t list * ty) -> subst
 val add_opdef    : subst -> path -> (EcIdent.t list * expr) -> subst
 val add_pddef    : subst -> path -> (EcIdent.t list * form) -> subst

src/ecTheoryReplay.ml

@@ -574,9 +574,15 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
                   List.map
                     (CS.Tvar.subst tysubst -| EcSubst.subst_ty subst)
                     tyargs in
-                EcSubst.add_opdef subst
-                  (xpath ove name)
-                  (newtparams, e_op np newtparams_ty (toarrow newtyargs newdtype))
+                let subst =
+                  EcSubst.add_opdef subst
+                    (xpath ove name)
+                    (newtparams, e_op np newtparams_ty (toarrow newtyargs newdtype)) in
+                (* The definition above rewrites the constructor where it
+                   occurs as an operator expression. The branches of a match
+                   body store it as a bare path, which is redirected through
+                   its own substitution. *)
+                EcSubst.add_ctor subst ~src:(xpath ove name) ~dst:np
                 ) subst octors
             | _ -> subst
           end

tests/clone-datatype-match.ec

@@ -0,0 +1,67 @@
+(* Regression test for issue #1046.
+
+   When a datatype's type is overridden during cloning, an operator whose
+   body pattern-matches on the datatype's constructors (i.e. compiles to
+   `OP_Fix`) used to crash with `anomaly: EcTheoryReplay.CoreIncompatible`.
+   The replay machinery redirects the source datatype's constructors to the
+   target datatype's constructors only through operator definitions
+   (`Fop`/`Eop` expression nodes), so the constructor *paths* stored in
+   `OP_Fix` match branches were left pointing at the source datatype and the
+   operator-compatibility check saw unequal constructor paths.
+
+   Both override modes must accept these clones. *)
+
+require import Int.
+
+theory Thy.
+  type ATy = [ CA | CB of int ].
+
+  op getit (x : ATy) =
+    with x = CA   => 0
+    with x = CB n => n.
+
+  op mk = CB 3.
+end Thy.
+
+clone Thy as Thy1.
+
+(* plain alias override *)
+clone Thy as Thy2 with
+  type ATy = Thy1.ATy,
+  op getit <= Thy1.getit,
+  op mk    <= Thy1.mk.
+
+(* inline override *)
+clone Thy as Thy3 with
+  type ATy <- Thy1.ATy,
+  op getit <= Thy1.getit,
+  op mk    <= Thy1.mk.
+
+(* No operator override: the replayed match operator must have its branch
+   constructors redirected to the target datatype, so it reduces on the
+   target's constructor applications. *)
+clone Thy as Thy4 with
+  type ATy = Thy1.ATy.
+
+lemma getit4 : Thy4.getit (Thy1.CB 5) = 5.
+proof. done. qed.
+
+(* Recursive match operator: exercises the recursive occurrence
+   (opf_recp) together with the constructor redirect. Only the inline
+   override is checked here: aliasing the type of a *recursive* datatype
+   is rejected by the type-compatibility check for an unrelated reason
+   (the constructor argument that mentions the datatype itself is not
+   redirected), independently of this fix. *)
+theory RThy.
+  type RTy = [ RNil | RCons of int & RTy ].
+
+  op total (x : RTy) =
+    with x = RNil       => 0
+    with x = RCons n xs => n + total xs.
+end RThy.
+
+clone RThy as RThy1.
+
+clone RThy as RThy2 with
+  type RTy <- RThy1.RTy,
+  op total <= RThy1.total.