TC: Fix issue with type synonyms in sizeof rewrite

rems-project · Feb 13, 2025 · 0ec5dbf · 0ec5dbf
1 parent 1013bd2
commit 0ec5dbf
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git 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
@@ -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