10 files changed, 64 insertions, 1 deletions

diff --git a/src/lexer.mll b/src/lexer.mll
index cd82a3b9..21b70c5f 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -271,7 +271,7 @@ rule token = parse
                                             Lexing.lexeme_start_p lexbuf)) }
 
 and line_comment pos = parse
-  | "\n"                                { () }
+  | "\n"                                { Lexing.new_line lexbuf; () }
   | _                                   { line_comment pos lexbuf }
   | eof                                 { raise (LexError("File ended before newline in comment", pos)) }
 
diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail
new file mode 100644
index 00000000..44382213
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym.sail
@@ -0,0 +1,9 @@
+
+// Type synonym with a constraint.
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+
+// Existential with constrained type synonym.
+let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+
+// Valspec with constrained type synonym.
+val test : forall 'n, 0 <= 'n <= 4. regno('n) -> unit
\ No newline at end of file
diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect
new file mode 100644
index 00000000..05dc6d8e
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v1.expect
@@ -0,0 +1,6 @@
+Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, character 42
+
+let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
+
+Tried performing type coercion on 4
+Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 33)
diff --git a/test/typecheck/pass/exist_synonym/v1.sail b/test/typecheck/pass/exist_synonym/v1.sail
new file mode 100644
index 00000000..828be157
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v1.sail
@@ -0,0 +1,9 @@
+
+// Type synonym with a constraint.
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+
+// Existential with constrained type synonym.
+let x : {'n, 0 <= 'n <= 33. regno('n)} = 4
+
+// Valspec with constrained type synonym.
+val test : forall 'n, 0 <= 'n <= 4. regno('n) -> unit
\ No newline at end of file
diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect
new file mode 100644
index 00000000..5b8f58c9
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v2.expect
@@ -0,0 +1,6 @@
+Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, character 41
+
+let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+
+Tried performing type coercion on 4
+Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom<'n> with (0 <= 'n & 'n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v2.sail b/test/typecheck/pass/exist_synonym/v2.sail
new file mode 100644
index 00000000..c8a3f689
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v2.sail
@@ -0,0 +1,9 @@
+
+// Type synonym with a constraint.
+type regno ('n : Int), 0 <= 'n < 2 = atom('n)
+
+// Existential with constrained type synonym.
+let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+
+// Valspec with constrained type synonym.
+val test : forall 'n, 0 <= 'n <= 4. regno('n) -> unit
\ No newline at end of file
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
new file mode 100644
index 00000000..be1a92a1
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -0,0 +1,3 @@
+Type error at no location information available
+
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 100)
diff --git a/test/typecheck/pass/exist_synonym/v3.sail b/test/typecheck/pass/exist_synonym/v3.sail
new file mode 100644
index 00000000..e17a395c
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v3.sail
@@ -0,0 +1,9 @@
+
+// Type synonym with a constraint.
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+
+// Existential with constrained type synonym.
+let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+
+// Valspec with constrained type synonym.
+val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit
\ No newline at end of file
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
new file mode 100644
index 00000000..13edc200
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -0,0 +1,3 @@
+Type error at no location information available
+
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 2 & 2 <= 4)
diff --git a/test/typecheck/pass/exist_synonym/v4.sail b/test/typecheck/pass/exist_synonym/v4.sail
new file mode 100644
index 00000000..0b161ae7
--- /dev/null
+++ b/test/typecheck/pass/exist_synonym/v4.sail
@@ -0,0 +1,9 @@
+
+// Type synonym with a constraint.
+type regno ('n : Int), 0 <= 'n < 32 = atom('n)
+
+// Existential with constrained type synonym.
+let x : {'n, 0 <= 'n <= 8. regno('n)} = 4
+
+// Valspec with constrained type synonym.
+val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit
\ No newline at end of file