From 5d1aa54005915044c3b1c01d2260ff267c927dba Mon Sep 17 00:00:00 2001
From: Claudio Russo <claudio@dfinity.org>
Date: Mon, 16 Oct 2023 16:30:22 +0100
Subject: [PATCH] bug: fix and repro for issue-4236 (bad renaming of
 `or`-patterns) (#4244)

Fix `ir_def/rename.ml`, for renaming bound variables, to properly handle our newly extended `or`-patterns.

With `or`-patterns, the same variable may have several binding occurrences, so renaming has to treat all of these consistently.
Instead of renaming variables on the fly, for `or`-patterns, we now determine the set of bound identifiers bound by all the
patterns beneath the `or`, rename them, and substitute consistently within the `or`-pattern to produce the renamed `or`-pattern.
---
 Changelog.md                            |  4 +-
 src/ir_def/rename.ml                    | 79 ++++++++++++++++++-------
 test/run-drun/issue-4236.mo             | 24 ++++++++
 test/run-drun/ok/issue-4236.drun-run.ok |  2 +
 4 files changed, 87 insertions(+), 22 deletions(-)
 create mode 100644 test/run-drun/issue-4236.mo
 create mode 100644 test/run-drun/ok/issue-4236.drun-run.ok

diff --git a/Changelog.md b/Changelog.md
index cd09f045d60..5d9dfe26835 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -2,7 +2,9 @@
 
 * motoko (`moc`)
 
-  * bugfix: Unsuccessful Candid decoding of an optional array now default to null instead of crashing (#4240).
+  * bugfix: fix assertion failure renaming `or`-patterns (#4236, #4224).
+
+  * bugfix: unsuccessful Candid decoding of an optional array now defaults to null instead of crashing (#4240).
 
   * bugfix: Candid decoding of an optional, unknown variant with a payload now succeeds instead of crashing (#4238).
 
diff --git a/src/ir_def/rename.ml b/src/ir_def/rename.ml
index cd7cd43e540..0a14e5da22a 100644
--- a/src/ir_def/rename.ml
+++ b/src/ir_def/rename.ml
@@ -15,6 +15,12 @@ let id_bind rho i =
   let i' = fresh_id i in
   (i', Renaming.add i i' rho)
 
+let rec ids_bind rho = function
+  | [] -> rho
+  | i::is' ->
+    let (i', rho') = id_bind rho i in
+    ids_bind rho' is'
+
 let arg_bind rho a =
   let i' = fresh_id a.it in
   ({a with it = i'}, Renaming.add a.it i' rho)
@@ -81,37 +87,68 @@ and args rho as_ =
      (a'::as_', rho'')
 
 and pat rho p =
-    let p',rho = pat' rho p.it in
-    {p with it = p'}, rho
+  let p', rho = pat' rho p.it in
+  {p with it = p'}, rho
 
 and pat' rho = function
   | WildP as p    -> (p, rho)
-  | VarP i        ->
+  | VarP i ->
     let i, rho' = id_bind rho i in
-     (VarP i, rho')
-  | TupP ps       -> let (ps, rho') = pats rho ps in
-                     (TupP ps, rho')
-  | ObjP pfs      ->
+    (VarP i, rho')
+  | TupP ps ->
+    let (ps, rho') = pats rho ps in
+    (TupP ps, rho')
+  | ObjP pfs ->
     let (pats, rho') = pats rho (pats_of_obj_pat pfs) in
     (ObjP (replace_obj_pat pfs pats), rho')
-  | LitP _ as p   -> (p, rho)
-  | OptP p        -> let (p', rho') = pat rho p in
-                     (OptP p', rho')
-  | TagP (i, p)   -> let (p', rho') = pat rho p in
-                     (TagP (i, p'), rho')
-  | AltP (p1, p2) -> assert(Freevars.(M.is_empty (pat p1)));
-                     assert(Freevars.(M.is_empty (pat p2)));
-                     let (p1', _) = pat rho p1 in
-                     let (p2' ,_) = pat rho p2 in
-                     (AltP (p1', p2'), rho)
+  | LitP _ as p ->
+    (p, rho)
+  | OptP p ->
+    let (p', rho') = pat rho p in
+    (OptP p', rho')
+  | TagP (i, p) ->
+    let (p', rho') = pat rho p in
+    (TagP (i, p'), rho')
+  | AltP (p1, p2) ->
+    let is1 = Freevars.M.keys (Freevars.pat p1) in
+    assert begin
+      let is2 = Freevars.M.keys (Freevars.pat p1) in
+      List.compare String.compare is1 is2 = 0
+    end;
+    let rho' = ids_bind rho is1 in
+    (AltP (pat_subst rho' p1, pat_subst rho' p2), rho')
 
 and pats rho ps  =
   match ps with
-  | [] -> ([],rho)
+  | [] -> ([], rho)
   | p::ps ->
-     let (p', rho') = pat rho p in
-     let (ps', rho'') = pats rho' ps in
-     (p'::ps', rho'')
+    let (p', rho') = pat rho p in
+    let (ps', rho'') = pats rho' ps in
+    (p'::ps', rho'')
+
+and pat_subst rho p =
+    let p'  = pat_subst' rho p.it in
+    {p with it = p'}
+
+and pat_subst' rho = function
+  | WildP as p -> p
+  | VarP i ->
+    VarP (id rho i)
+  | TupP ps ->
+    TupP (pats_subst rho ps)
+  | ObjP pfs ->
+    let pats = pats_subst rho (pats_of_obj_pat pfs) in
+    ObjP (replace_obj_pat pfs pats)
+  | LitP _ as p -> p
+  | OptP p ->
+    OptP (pat_subst rho p)
+  | TagP (i, p) ->
+    TagP (i, pat_subst rho p)
+  | AltP (p1, p2) ->
+    AltP (pat_subst rho p1, pat_subst rho p2)
+
+and pats_subst rho ps =
+  List.map (pat_subst rho) ps
 
 and case rho (c : case) =
   {c with it = case' rho c.it}
diff --git a/test/run-drun/issue-4236.mo b/test/run-drun/issue-4236.mo
new file mode 100644
index 00000000000..dc2b5064141
--- /dev/null
+++ b/test/run-drun/issue-4236.mo
@@ -0,0 +1,24 @@
+// crashes in renaming of or-pattern
+// (NB: renaming itself only forced by actor class (to avoid capture when class arg binds parameters)
+actor class () {
+  type Account = {
+          holder : Principal;
+          balance : Nat;
+  };
+  type Amount = {
+          amount : Nat
+  };
+  type Movement = {
+          #deposit : Account and Amount;
+          #withdraw : Account and Amount;
+  };
+
+  func getAccount(m : Movement) : Account =
+        switch m {
+          case (#deposit accnt or #withdraw accnt) accnt
+        }
+}
+
+//SKIP run
+//SKIP run-ir
+//SKIP run-low
diff --git a/test/run-drun/ok/issue-4236.drun-run.ok b/test/run-drun/ok/issue-4236.drun-run.ok
new file mode 100644
index 00000000000..a6f776f43c6
--- /dev/null
+++ b/test/run-drun/ok/issue-4236.drun-run.ok
@@ -0,0 +1,2 @@
+ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101
+ingress Completed: Reply: 0x4449444c0000