From 0ec5dbf63884156688bf61ea8ad96a66425676e5 Mon Sep 17 00:00:00 2001
From: Alasdair <alasdair.armstrong@cl.cam.ac.uk>
Date: Thu, 13 Feb 2025 12:04:27 +0000
Subject: [PATCH] TC: Fix issue with type synonyms in sizeof rewrite

---
 src/lib/type_check.ml             |  3 ++-
 test/typecheck/pass/issue984.sail | 10 ++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 test/typecheck/pass/issue984.sail

diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index 551540af8..089a40aa9 100644
--- a/src/lib/type_check.ml
+++ b/src/lib/type_check.ml
@@ -1136,7 +1136,8 @@ let rec rewrite_sizeof' l env (Nexp_aux (aux, _) as nexp) =
       in
       let locals = Env.get_locals env |> Bindings.bindings in
       let locals = move_to_front (fun local -> likely = string_of_id (fst local)) [] locals in
-      let same_size (_, (_, Typ_aux (aux, _))) =
+      let same_size (_, (_, typ)) =
+        let (Typ_aux (aux, _)) = Env.expand_synonyms env typ in
         match aux with
         | Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var v', _)), _)])
           when string_of_id id = "atom" && Kid.compare v v' = 0 ->
diff --git a/test/typecheck/pass/issue984.sail b/test/typecheck/pass/issue984.sail
new file mode 100644
index 000000000..6610066b5
--- /dev/null
+++ b/test/typecheck/pass/issue984.sail
@@ -0,0 +1,10 @@
+default Order dec
+$include <prelude.sail>
+
+val foo_0 : forall 'n, 'n in {32, 64}. bits('n) -> bool
+function foo_0(x : bits('n)) = 'n == 64
+
+function foo_1 forall 'n, 'n in {32, 64} . (x : bits('n)) -> bool = 'n == 64
+
+val foo_2 : forall 'n, 'n in {32, 64}. bits('n) -> bool
+function foo_2(x) = 'n == 64