Allow type variables to be introduced by global let bindings.

This was technically allowed previously but the rules for type
variable names in function types were too strict so it didn't work.

Also fixed a bug where Nexp_app constructors were never considered identical

and fixed a bug where top-level let bindings got annotated with the
wrong environment

7 files changed, 105 insertions, 0 deletions

diff --git a/test/typecheck/pass/global_type_var.sail b/test/typecheck/pass/global_type_var.sail
new file mode 100644
index 00000000..215907b4
--- /dev/null
+++ b/test/typecheck/pass/global_type_var.sail
@@ -0,0 +1,21 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
new file mode 100644
index 00000000..67355f59
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -0,0 +1,6 @@
+Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15
+
+let _ = test(32)
+
+Tried performing type coercion on 32
+Failed because atom<32> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
diff --git a/test/typecheck/pass/global_type_var/v1.sail b/test/typecheck/pass/global_type_var/v1.sail
new file mode 100644
index 00000000..f2b2f89a
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v1.sail
@@ -0,0 +1,23 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
+
+let _ = test(32)
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
new file mode 100644
index 00000000..fb31fbed
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -0,0 +1,6 @@
+Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15
+
+let _ = test(64)
+
+Tried performing type coercion on 64
+Failed because atom<64> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
diff --git a/test/typecheck/pass/global_type_var/v2.sail b/test/typecheck/pass/global_type_var/v2.sail
new file mode 100644
index 00000000..e8340978
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v2.sail
@@ -0,0 +1,23 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
+
+let _ = test(64)
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
new file mode 100644
index 00000000..a01f3eec
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23
+
+val test : forall 'size. atom('size) -> unit
+
+Kind identifier 'size is already bound
diff --git a/test/typecheck/pass/global_type_var/v3.sail b/test/typecheck/pass/global_type_var/v3.sail
new file mode 100644
index 00000000..274490ff
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v3.sail
@@ -0,0 +1,21 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : forall 'size. atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size