Make sure we correctly forbid recursive datatypes that we don't want to support

Ensure we give a nice error message that explains that recursive types are forbidden

```
Type error:
[struct_rec.sail]:3:10-11
3 |  field : S
  |          ^
  | Undefined type S
  | This error was caused by:
  | [struct_rec.sail]:2:0-4:1
  | 2 |struct S = {
  |   |^-----------
  | 4 |}
  |   |^
  |   | Recursive types are not allowed
```

The theorem prover backends create a special register_value union that
can be recursive, so we make sure to special case that.

14 files changed, 103 insertions, 5 deletions

diff --git a/test/typecheck/fail/struct_rec.expect b/test/typecheck/fail/struct_rec.expect
new file mode 100644
index 00000000..6daa067d
--- /dev/null
+++ b/test/typecheck/fail/struct_rec.expect
@@ -0,0 +1,13 @@
+Type error:
+[struct_rec.sail]:3:10-11
+3 |  field : S
+  |          ^
+  | Undefined type S
+  | This error was caused by:
+  | [struct_rec.sail]:2:0-4:1
+  | 2 |struct S = {
+  |   |^-----------
+  | 4 |}
+  |   |^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/struct_rec.sail b/test/typecheck/fail/struct_rec.sail
new file mode 100644
index 00000000..01c29d6d
--- /dev/null
+++ b/test/typecheck/fail/struct_rec.sail
@@ -0,0 +1,4 @@
+
+struct S = {
+  field : S
+}
diff --git a/test/typecheck/fail/synonym_rec.expect b/test/typecheck/fail/synonym_rec.expect
new file mode 100644
index 00000000..5d205606
--- /dev/null
+++ b/test/typecheck/fail/synonym_rec.expect
@@ -0,0 +1,11 @@
+Type error:
+[synonym_rec.sail]:2:9-10
+2 |type T = T
+  |         ^
+  | Undefined type T
+  | This error was caused by:
+  | [synonym_rec.sail]:2:0-10
+  | 2 |type T = T
+  |   |^--------^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/synonym_rec.sail b/test/typecheck/fail/synonym_rec.sail
new file mode 100644
index 00000000..54906418
--- /dev/null
+++ b/test/typecheck/fail/synonym_rec.sail
@@ -0,0 +1,2 @@
+
+type T = T
diff --git a/test/typecheck/fail/union_rec.expect b/test/typecheck/fail/union_rec.expect
new file mode 100644
index 00000000..2d50cea6
--- /dev/null
+++ b/test/typecheck/fail/union_rec.expect
@@ -0,0 +1,13 @@
+Type error:
+[union_rec.sail]:3:9-10
+3 |  Ctor : U
+  |         ^
+  | Undefined type U
+  | This error was caused by:
+  | [union_rec.sail]:2:0-4:1
+  | 2 |union U = {
+  |   |^----------
+  | 4 |}
+  |   |^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/union_rec.sail b/test/typecheck/fail/union_rec.sail
new file mode 100644
index 00000000..7ca7b8e9
--- /dev/null
+++ b/test/typecheck/fail/union_rec.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : U
+}
diff --git a/test/typecheck/fail/union_recf.expect b/test/typecheck/fail/union_recf.expect
new file mode 100644
index 00000000..b07910ba
--- /dev/null
+++ b/test/typecheck/fail/union_recf.expect
@@ -0,0 +1,13 @@
+Type error:
+[union_recf.sail]:3:9-10
+3 |  Ctor : U -> U
+  |         ^
+  | Undefined type U
+  | This error was caused by:
+  | [union_recf.sail]:2:0-4:1
+  | 2 |union U = {
+  |   |^----------
+  | 4 |}
+  |   |^
+  |   | Recursive types are not allowed
+  | 
diff --git a/test/typecheck/fail/union_recf.sail b/test/typecheck/fail/union_recf.sail
new file mode 100644
index 00000000..f64ca675
--- /dev/null
+++ b/test/typecheck/fail/union_recf.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : U -> U
+}
diff --git a/test/typecheck/pass/constrained_struct/v1.expect b/test/typecheck/pass/constrained_struct/v1.expect
index 8c95193d..bf498a36 100644
--- a/test/typecheck/pass/constrained_struct/v1.expect
+++ b/test/typecheck/pass/constrained_struct/v1.expect
@@ -3,4 +3,9 @@ Type error:
 10 |type MyStruct64 = MyStruct(65)
    |                  ^------^
    | Could not prove (65 == 32 | 65 == 64) for type constructor MyStruct
+   | This error was caused by:
+   | [constrained_struct/v1.sail]:10:0-30
+   | 10 |type MyStruct64 = MyStruct(65)
+   |    |^----------------------------^
+   |    | Recursive types are not allowed
    | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index ca83adb9..8d061933 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex273#)
+   | * datasize('ex276#)
    | 
diff --git a/test/typecheck/pass/reg_32_64/v2.expect b/test/typecheck/pass/reg_32_64/v2.expect
index 24439bed..90166904 100644
--- a/test/typecheck/pass/reg_32_64/v2.expect
+++ b/test/typecheck/pass/reg_32_64/v2.expect
@@ -5,7 +5,7 @@ Type error:
    | Tried performing type coercion from bitvector('d, dec) to bitvector((('d - 0) + 1), dec) on data
    | Coercion failed because:
    | Mismatched argument types in subtype check
-   | This error occured because of a previous error:
+   | This error was caused by:
    | [reg_32_64/v2.sail]:21:2-15
    | 21 |  (*R)['d .. 0] = data
    |    |  ^-----------^
diff --git a/test/typecheck/pass/union_recf_ok.sail b/test/typecheck/pass/union_recf_ok.sail
new file mode 100644
index 00000000..0f415601
--- /dev/null
+++ b/test/typecheck/pass/union_recf_ok.sail
@@ -0,0 +1,4 @@
+
+union U = {
+  Ctor : int -> U
+}
\ No newline at end of file
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index e5650646..adc30c42 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -87,6 +87,24 @@ do
     done
 done
 
+for file in $DIR/fail/*.sail;
+do
+    pushd $DIR/fail > /dev/null;
+    if $SAILDIR/sail -no_memo_z3 $(basename $file) 2> result
+    then
+        red "Expected failure, but $i $(basename $file) passed" "fail"
+    else
+        if diff ${file%.sail}.expect result;
+        then
+            green "failing $i $(basename $file)" "pass"
+        else
+            yellow "failing $i $(basename $file)" "unexpected error"
+        fi
+    fi;
+    rm -f result;
+    popd > /dev/null
+done
+
 finish_suite "Typechecking tests"
 
 printf "</testsuites>\n" >> $DIR/tests.xml
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
index ba436daf..1d174797 100755
--- a/test/typecheck/update_errors.sh
+++ b/test/typecheck/update_errors.sh
@@ -10,8 +10,15 @@ do
     shopt -s nullglob;
     for file in $DIR/pass/${i%.sail}/*.sail;
     do
-	pushd $DIR/pass > /dev/null;
-	$SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
-	popd > /dev/null
+        pushd $DIR/pass > /dev/null;
+        $SAILDIR/sail -no_memo_z3 ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+        popd > /dev/null
     done
 done
+
+for file in $DIR/fail/*.sail;
+do
+    pushd $DIR/fail > /dev/null;
+    $SAILDIR/sail -no_memo_z3 $(basename $file) 2> ${file%.sail}.expect || true;
+    popd > /dev/null
+done