From c4723c747fec4557776858641b03e1eb4a0a5878 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Mon, 23 Nov 2020 14:18:58 +0000
Subject: Don't allow type synonyms with the same name as existing types

---
 src/type_check.ml                         |  4 ++--
 test/typecheck/pass/poly_vector/v2.expect |  6 ++++++
 test/typecheck/pass/poly_vector/v2.sail   | 22 ++++++++++++++++++++++
 3 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 test/typecheck/pass/poly_vector/v2.expect
 create mode 100644 test/typecheck/pass/poly_vector/v2.sail

diff --git a/src/type_check.ml b/src/type_check.ml
index aeb9cf01..1ada515e 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -647,8 +647,8 @@ end = struct
     else typ_error env (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
   let add_typ_synonym id typq arg env =
-    if Bindings.mem id env.typ_synonyms then
-      typ_error env (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
+    if bound_typ_id env id then
+      typ_error env (id_loc id) ("Cannot define type synonym " ^ string_of_id id ^ ", as a type or synonym with that name already exists")
     else
       begin
         typ_print (lazy (adding ^ "type synonym " ^ string_of_id id));
diff --git a/test/typecheck/pass/poly_vector/v2.expect b/test/typecheck/pass/poly_vector/v2.expect
new file mode 100644
index 00000000..dfe0fae9
--- /dev/null
+++ b/test/typecheck/pass/poly_vector/v2.expect
@@ -0,0 +1,6 @@
+Type error:
+[poly_vector/v2.sail]:5:5-14
+5 |type bitvector('n, 'ord: Order) = vector('n, 'ord, bit)
+  |     ^-------^
+  | Cannot define type synonym bitvector, as a type or synonym with that name already exists
+  | 
diff --git a/test/typecheck/pass/poly_vector/v2.sail b/test/typecheck/pass/poly_vector/v2.sail
new file mode 100644
index 00000000..1b956748
--- /dev/null
+++ b/test/typecheck/pass/poly_vector/v2.sail
@@ -0,0 +1,22 @@
+default Order dec
+
+$include <prelude.sail>
+
+type bitvector('n, 'ord: Order) = vector('n, 'ord, bit)
+
+val "to_generic" : forall 'n. bitvector('n, dec) -> vector('n, dec, bit)
+
+val "print_endline" : string -> unit
+
+function my_length forall 'n ('a : Type). (xs: vector('n, dec, 'a)) -> int('n) = {
+  length(xs)
+}
+
+function main() -> unit = {
+  let xs : bits(32) = 0xFFFF_FFFF;
+  if my_length(to_generic(xs)) == 32 then {
+    print_endline("ok")
+  } else {
+    print_endline("false")
+  }
+}
-- 
cgit v1.2.3