diff --git a/intTests/support/test-and-diff.sh b/intTests/support/test-and-diff.sh
index a9f5391d2..31ebbad0f 100644
--- a/intTests/support/test-and-diff.sh
+++ b/intTests/support/test-and-diff.sh
@@ -110,7 +110,7 @@ run-tests() {
             /^\[[0-9][0-9]:[0-9][0-9]:[0-9][0-9]\.[0-9][0-9][0-9]\] /{
                 s/^..............//
             }
-            s,'"$CURDIR"'/,,
+            s,'"$CURDIR"'/,,g
         '
 
         # Check the output against the expected version.
diff --git a/intTests/test_type_errors/err013.log.good b/intTests/test_type_errors/err013.log.good
new file mode 100644
index 000000000..d1a7b8181
--- /dev/null
+++ b/intTests/test_type_errors/err013.log.good
@@ -0,0 +1,9 @@
+ Loading file "err013.saw"
+ err013.saw:9:33-9:35: Type mismatch.
+    Occurs check failure: the type at internal:1:2-1:3: Fresh type for this term appears within the type at internal:1:2-1:3: Fresh type for this term
+    Expected: [t.5]
+    Found:    [[t.5]]
+    
+    within "paste" (err013.saw:9:5-9:10)
+
+FAILED
diff --git a/intTests/test_type_errors/err013.saw b/intTests/test_type_errors/err013.saw
new file mode 100644
index 000000000..1fba7b195
--- /dev/null
+++ b/intTests/test_type_errors/err013.saw
@@ -0,0 +1,9 @@
+// Trigger the "occurs check failure" message
+//
+// This is produced if type inference results in a type that contains
+// itself.
+//
+// We can do this by doing something with a list and its element type
+// that require them to be the same.
+
+let paste xs = concat (head xs) xs;
diff --git a/intTests/test_type_errors/err014.log.good b/intTests/test_type_errors/err014.log.good
new file mode 100644
index 000000000..d4b9de741
--- /dev/null
+++ b/intTests/test_type_errors/err014.log.good
@@ -0,0 +1,12 @@
+ Loading file "err014.saw"
+ err014.saw:12:15-12:18: Type mismatch.
+    Record field names mismatch.
+    err014.saw:8:13-8:24: The type {a : Int} arises from this type annotation
+    err014.saw:10:25-10:34: The type {b : Int} arises from the type of this term
+    
+    Expected: {a : Int}
+    Found:    {b : Int}
+    
+    within "baz" (err014.saw:12:5-12:8)
+
+FAILED
diff --git a/intTests/test_type_errors/err014.saw b/intTests/test_type_errors/err014.saw
new file mode 100644
index 000000000..68aa27c37
--- /dev/null
+++ b/intTests/test_type_errors/err014.saw
@@ -0,0 +1,12 @@
+// Trigger the "Record field names mismatch" message.
+//
+// This is produced by trying to unify two record types with
+// different field names.
+//
+// Here just do a base case of that.
+
+let foo (x: { a : Int }) : { a : Int } = { a = x.a };
+
+let bar : { b : Int } = { b = 3 };
+
+let baz = foo bar;
diff --git a/intTests/test_type_errors/err015.log.good b/intTests/test_type_errors/err015.log.good
new file mode 100644
index 000000000..9aaccee42
--- /dev/null
+++ b/intTests/test_type_errors/err015.log.good
@@ -0,0 +1,54 @@
+ Loading file "err015.saw"
+ Type errors:
+  err015.saw:65:14-65:15: Type mismatch.
+    Record field names mismatch.
+    err015.saw:18:15-22:2: The type {amethyst : Int, moonstone : Int, obsidian : Int} arises from this type annotation
+    err015.saw:55:14-55:74: The type {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int} arises from the type of this term
+    
+    Expected: {amethyst : Int, moonstone : Int, obsidian : Int}
+    Found:    {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int}
+    
+    within "y" (err015.saw:65:5-65:6)
+
+  err015.saw:65:21-65:22: Type mismatch.
+    Record field names mismatch.
+    err015.saw:25:15-31:2: The type {amethyst : Int, moonstone : Int, obsidian : Int, sapphire : Int, turquoise : Int} arises from this type annotation
+    err015.saw:55:14-55:74: The type {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int} arises from the type of this term
+    
+    Expected: {amethyst : Int, moonstone : Int, obsidian : Int, sapphire : Int, turquoise : Int}
+    Found:    {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int}
+    
+    within "y" (err015.saw:65:5-65:6)
+
+  err015.saw:65:28-65:29: Type mismatch.
+    Record field names mismatch.
+    err015.saw:34:15-39:2: The type {amethyst : Int, moonstone : Int, obsidian : Int, tourmaline : Int} arises from this type annotation
+    err015.saw:55:14-55:74: The type {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int} arises from the type of this term
+    
+    Expected: {amethyst : Int, moonstone : Int, obsidian : Int, tourmaline : Int}
+    Found:    {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int}
+    
+    within "y" (err015.saw:65:5-65:6)
+
+  err015.saw:65:35-65:36: Type mismatch.
+    Record field names mismatch.
+    err015.saw:42:15-45:2: The type {amethyst : Int, obsidian : Int} arises from this type annotation
+    err015.saw:55:14-55:74: The type {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int} arises from the type of this term
+    
+    Expected: {amethyst : Int, obsidian : Int}
+    Found:    {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int}
+    
+    within "y" (err015.saw:65:5-65:6)
+
+  err015.saw:65:41-65:42: Type mismatch.
+    Record field names mismatch.
+    err015.saw:48:14-53:2: The type {anise : Int, cinnamon : Int, sage : Int, tarragon : Int} arises from this type annotation
+    err015.saw:55:14-55:74: The type {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int} arises from the type of this term
+    
+    Expected: {anise : Int, cinnamon : Int, sage : Int, tarragon : Int}
+    Found:    {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int}
+    
+    within "y" (err015.saw:65:5-65:6)
+
+
+FAILED
diff --git a/intTests/test_type_errors/err015.saw b/intTests/test_type_errors/err015.saw
new file mode 100644
index 000000000..15d6ae38d
--- /dev/null
+++ b/intTests/test_type_errors/err015.saw
@@ -0,0 +1,65 @@
+// Trigger the "Record field names mismatch" message.
+//
+// Exercise multiple more complicated cases:
+//    - lots of record fields with one missing
+//    - lots of record fields with one extra
+//    - lots of record fields with one different
+//    - lots of record fields with half missing
+//    - lots of record fields with all of them different
+
+typedef t1 = {
+   amethyst: Int,
+   moonstone: Int,
+   obsidian: Int,
+   turquoise: Int
+};
+
+// one missing
+typedef t1a = {
+   amethyst: Int,
+   moonstone: Int,
+   obsidian: Int
+};
+
+// one extra
+typedef t1b = {
+   amethyst: Int,
+   moonstone: Int,
+   obsidian: Int,
+   sapphire: Int,
+   turquoise: Int
+};
+
+// one different
+typedef t1c = {
+   amethyst: Int,
+   moonstone: Int,
+   obsidian: Int,
+   tourmaline: Int
+};
+
+// half missing
+typedef t1d = {
+   amethyst: Int,
+   obsidian: Int
+};
+
+// all different
+typedef t2 = {
+   anise: Int,
+   cinnamon: Int,
+   sage: Int,
+   tarragon: Int
+};
+
+let x : t1 = { amethyst = 3, moonstone = 3, obsidian = 3, turquoise = 3 };
+
+let f1a (x: t1a) = x.amethyst;
+let f1b (x: t1b) = x.amethyst;
+let f1c (x: t1c) = x.amethyst;
+let f1d (x: t1d) = x.amethyst;
+let f2 (x: t2) = x.anise;
+
+// produce a tuple so we get all the messages at once
+// (otherwise the interpreter apparently bails after one failed let)
+let y = (f1a x, f1b x, f1c x, f1d x, f2 x);
diff --git a/intTests/test_type_errors/err016.log.good b/intTests/test_type_errors/err016.log.good
new file mode 100644
index 000000000..c7c341581
--- /dev/null
+++ b/intTests/test_type_errors/err016.log.good
@@ -0,0 +1,12 @@
+ Loading file "err016.saw"
+ err016.saw:5:9-5:12: Type mismatch.
+    Term is not a function. (Maybe a function is applied to too many arguments?)
+    err016.saw:5:9-5:12: The type t.0 -> t.1 arises from the context of the term
+    err016.saw:5:11-5:12: The type Int arises from the type of this term
+    
+    Expected: t.0 -> t.1
+    Found:    Int
+    
+    within "y" (err016.saw:5:5-5:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err016.saw b/intTests/test_type_errors/err016.saw
new file mode 100644
index 000000000..0c4e7d050
--- /dev/null
+++ b/intTests/test_type_errors/err016.saw
@@ -0,0 +1,5 @@
+// Trigger the message "Term is not a function. (Maybe a function is
+// applied to too many arguments?)"
+
+let f x = x;
+let y = f 3 4;
diff --git a/intTests/test_type_errors/err017.log.good b/intTests/test_type_errors/err017.log.good
new file mode 100644
index 000000000..33ce2c216
--- /dev/null
+++ b/intTests/test_type_errors/err017.log.good
@@ -0,0 +1,12 @@
+ Loading file "err017.saw"
+ err017.saw:27:11-27:12: Type mismatch.
+    Mismatch of types.
+    err017.saw:20:13-23:2: The type {a : Int, b : Int} arises from this type annotation
+    err017.saw:27:11-27:12: The type Int arises from the type of this term
+    
+    Expected: {a : Int, b : Int}
+    Found:    Int
+    
+    within "y" (err017.saw:27:5-27:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err017.saw b/intTests/test_type_errors/err017.saw
new file mode 100644
index 000000000..85dccbcb5
--- /dev/null
+++ b/intTests/test_type_errors/err017.saw
@@ -0,0 +1,28 @@
+// Trigger the "Mismatch of types" message.
+//
+// Most type mismatches generate the "Mismatch of type constructors"
+// message; to fall through to the default case that produces this
+// message, you have to have two types where
+//    - neither is a TyUnifyVar
+//    - they aren't both TyRecord
+//    - they aren't both TyCon
+//    - they aren't the same TyVar
+// which leaves the following cases:
+//    - TyRecord vs. TyCon
+//    - TyVar vs. TyRecord or TyCon
+//    - different TyVars
+//
+// At the moment producing arbitrary TyVars is difficult (we no
+// longer allow making them up just by mentioning them, but we don't
+// yet have a syntax for forall-binding them in decls) so use the
+// TyRecord vs. TyCon case
+
+typedef t = {
+   a: Int,
+   b: Int
+};
+
+let f (x: t) = x.a;
+
+let y = f 3;
+
diff --git a/intTests/test_type_errors/err018.log.good b/intTests/test_type_errors/err018.log.good
new file mode 100644
index 000000000..64116cbba
--- /dev/null
+++ b/intTests/test_type_errors/err018.log.good
@@ -0,0 +1,15 @@
+ Loading file "err018.saw"
+ err018.saw:26:11-26:12: Type mismatch.
+    Mismatch of type constructors. Expected: String but got Int
+    err018.saw:16:14-16:20: The type String arises from this type annotation
+    err018.saw:23:25-23:26: The type Int arises from the type of this term
+    
+    Expected: String
+    Found:    Int
+    
+    Expected: {amethyst : String, moonstone : String, obsidian : String, turquoise : String}
+    Found:    {amethyst : Int, moonstone : Int, obsidian : Int, turquoise : Int}
+    
+    within "y" (err018.saw:26:5-26:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err018.saw b/intTests/test_type_errors/err018.saw
new file mode 100644
index 000000000..200a1f921
--- /dev/null
+++ b/intTests/test_type_errors/err018.saw
@@ -0,0 +1,27 @@
+// Trigger the message we get when records have the same fields
+// but not the same types.
+//
+// Currently this trips on the first inconsistent field and prints
+// "mismatch of type constructors" on it, which is not particularly
+// friendly.
+
+typedef t1 = {
+   amethyst: Int,
+   moonstone: Int,
+   obsidian: Int,
+   turquoise: Int
+};
+
+typedef t2 = {
+   amethyst: String,
+   moonstone: String,
+   obsidian: String,
+   turquoise: String
+};
+
+
+let x : t1 = { amethyst=3, moonstone=4, obsidian=5, turquoise=6 };
+let f (x: t2) = x.amethyst;
+
+let y = f x;
+
diff --git a/intTests/test_type_errors/err019.log.good b/intTests/test_type_errors/err019.log.good
new file mode 100644
index 000000000..03551ea0f
--- /dev/null
+++ b/intTests/test_type_errors/err019.log.good
@@ -0,0 +1,12 @@
+ Loading file "err019.saw"
+ err019.saw:5:11-5:12: Type mismatch.
+    Mismatch of type constructors. Expected: (,,,) but got (,,)
+    err019.saw:4:11-4:31: The type (Int, Int, Int, Int) arises from this type annotation
+    err019.saw:3:9-3:18: The type (Int, Int, Int) arises from the type of this term
+    
+    Expected: (Int, Int, Int, Int)
+    Found:    (Int, Int, Int)
+    
+    within "y" (err019.saw:5:5-5:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err019.saw b/intTests/test_type_errors/err019.saw
new file mode 100644
index 000000000..f33a61604
--- /dev/null
+++ b/intTests/test_type_errors/err019.saw
@@ -0,0 +1,5 @@
+// Trigger the message we get by unifying tuples of mismatched arity.
+
+let x = (1, 2, 3);
+let f (x: (Int, Int, Int, Int)) = x.0;
+let y = f x;
diff --git a/intTests/test_type_errors/err020.log.good b/intTests/test_type_errors/err020.log.good
new file mode 100644
index 000000000..e11391bf4
--- /dev/null
+++ b/intTests/test_type_errors/err020.log.good
@@ -0,0 +1,5 @@
+ Loading file "err020.saw"
+ err020.saw:3:20-3:33: Record lookup on non-record argument.
+Field name: nonexistent
+
+FAILED
diff --git a/intTests/test_type_errors/err020.saw b/intTests/test_type_errors/err020.saw
new file mode 100644
index 000000000..747fc5f1d
--- /dev/null
+++ b/intTests/test_type_errors/err020.saw
@@ -0,0 +1,3 @@
+// Trigger the "Record lookup on non-record argument" message.
+
+let foo (x: Int) = x.nonexistent;
diff --git a/intTests/test_type_errors/err021.log.good b/intTests/test_type_errors/err021.log.good
new file mode 100644
index 000000000..e69b74627
--- /dev/null
+++ b/intTests/test_type_errors/err021.log.good
@@ -0,0 +1,5 @@
+ Loading file "err021.saw"
+ err021.saw:8:18-8:31: Selecting a missing field.
+Field name: nonexistent
+
+FAILED
diff --git a/intTests/test_type_errors/err021.saw b/intTests/test_type_errors/err021.saw
new file mode 100644
index 000000000..e1e9d814b
--- /dev/null
+++ b/intTests/test_type_errors/err021.saw
@@ -0,0 +1,8 @@
+// Trigger the "Selecting a missing (record) field" message.
+
+typedef t = {
+   a: Int,
+   b: Int
+};
+
+let foo (x: t) = x.nonexistent;
diff --git a/intTests/test_type_errors/err022.log.good b/intTests/test_type_errors/err022.log.good
new file mode 100644
index 000000000..816b37509
--- /dev/null
+++ b/intTests/test_type_errors/err022.log.good
@@ -0,0 +1,5 @@
+ Loading file "err022.saw"
+ err022.saw:3:20-3:23: Tuple lookup on non-tuple argument.
+Given index 3
+
+FAILED
diff --git a/intTests/test_type_errors/err022.saw b/intTests/test_type_errors/err022.saw
new file mode 100644
index 000000000..620f4f4dd
--- /dev/null
+++ b/intTests/test_type_errors/err022.saw
@@ -0,0 +1,3 @@
+// Trigger the "Tuple lookup on non-tuple argument" message.
+
+let foo (x: Int) = x.3;
diff --git a/intTests/test_type_errors/err023.log.good b/intTests/test_type_errors/err023.log.good
new file mode 100644
index 000000000..3f479256d
--- /dev/null
+++ b/intTests/test_type_errors/err023.log.good
@@ -0,0 +1,5 @@
+ Loading file "err023.saw"
+ err023.saw:5:18-5:21: Tuple index out of bounds.
+Given index 3 is too large for tuple size of 2
+
+FAILED
diff --git a/intTests/test_type_errors/err023.saw b/intTests/test_type_errors/err023.saw
new file mode 100644
index 000000000..f5b050a8a
--- /dev/null
+++ b/intTests/test_type_errors/err023.saw
@@ -0,0 +1,5 @@
+// Trigger the "Tuple index out of bounds" message.
+
+typedef t = (Int, Int);
+
+let foo (x: t) = x.3;
diff --git a/intTests/test_type_errors/err024.log.good b/intTests/test_type_errors/err024.log.good
new file mode 100644
index 000000000..6ac17fe2e
--- /dev/null
+++ b/intTests/test_type_errors/err024.log.good
@@ -0,0 +1,6 @@
+ Loading file "err024.saw"
+ err024.saw:3:9-3:10: Unbound variable: "y" (err024.saw:3:9-3:10)
+Note that some built-in commands are available only after running
+either `enable_deprecated` or `enable_experimental`.
+
+FAILED
diff --git a/intTests/test_type_errors/err024.saw b/intTests/test_type_errors/err024.saw
new file mode 100644
index 000000000..0b339a115
--- /dev/null
+++ b/intTests/test_type_errors/err024.saw
@@ -0,0 +1,3 @@
+// Trigger the "Unbound variable" message
+
+let x = y;
diff --git a/intTests/test_type_errors/err025.log.good b/intTests/test_type_errors/err025.log.good
new file mode 100644
index 000000000..1be1f7e37
--- /dev/null
+++ b/intTests/test_type_errors/err025.log.good
@@ -0,0 +1,3 @@
+ Loading file "err025.saw"
+ err025.saw:3:9-3:14: do block must include at least one expression at "x" (err025.saw:3:5-3:6)
+FAILED
diff --git a/intTests/test_type_errors/err025.saw b/intTests/test_type_errors/err025.saw
new file mode 100644
index 000000000..11c1e2984
--- /dev/null
+++ b/intTests/test_type_errors/err025.saw
@@ -0,0 +1,3 @@
+// Trigger the "do block must include at least one expression" message
+
+let x = do {};
diff --git a/intTests/test_type_errors/err026.log.good b/intTests/test_type_errors/err026.log.good
new file mode 100644
index 000000000..a87edd080
--- /dev/null
+++ b/intTests/test_type_errors/err026.log.good
@@ -0,0 +1,3 @@
+ Loading file "err026.saw"
+ err026.saw:3:9-5:2: do block must end with expression at "x" (err026.saw:3:5-3:6)
+FAILED
diff --git a/intTests/test_type_errors/err026.saw b/intTests/test_type_errors/err026.saw
new file mode 100644
index 000000000..deb72a68f
--- /dev/null
+++ b/intTests/test_type_errors/err026.saw
@@ -0,0 +1,5 @@
+// Trigger the "do block must end with expression" message
+
+let x = do {
+   y <- llvm_assert {{ True }};
+};
diff --git a/intTests/test_type_errors/err027.log.good b/intTests/test_type_errors/err027.log.good
new file mode 100644
index 000000000..d670e91ef
--- /dev/null
+++ b/intTests/test_type_errors/err027.log.good
@@ -0,0 +1,3 @@
+ Loading file "err027.saw"
+ Parse error at err027.saw:7:10-7:11: Unexpected `]'
+FAILED
diff --git a/intTests/test_type_errors/err027.saw b/intTests/test_type_errors/err027.saw
new file mode 100644
index 000000000..fcdb4c690
--- /dev/null
+++ b/intTests/test_type_errors/err027.saw
@@ -0,0 +1,9 @@
+//
+// Not enough arguments for type constructor: arrays
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : [] = [];
+
+
diff --git a/intTests/test_type_errors/err028.log.good b/intTests/test_type_errors/err028.log.good
new file mode 100644
index 000000000..a6777556e
--- /dev/null
+++ b/intTests/test_type_errors/err028.log.good
@@ -0,0 +1,3 @@
+ Loading file "err028.saw"
+ Parse error at err028.saw:7:16-7:19: Unexpected `Int'
+FAILED
diff --git a/intTests/test_type_errors/err028.saw b/intTests/test_type_errors/err028.saw
new file mode 100644
index 000000000..cf6d55e59
--- /dev/null
+++ b/intTests/test_type_errors/err028.saw
@@ -0,0 +1,9 @@
+//
+// Too many arguments for type constructor: String
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : String Int = "abc";
+
+
diff --git a/intTests/test_type_errors/err029.log.good b/intTests/test_type_errors/err029.log.good
new file mode 100644
index 000000000..c57604ef7
--- /dev/null
+++ b/intTests/test_type_errors/err029.log.good
@@ -0,0 +1,3 @@
+ Loading file "err029.saw"
+ Parse error at err029.saw:7:14-7:17: Unexpected `Int'
+FAILED
diff --git a/intTests/test_type_errors/err029.saw b/intTests/test_type_errors/err029.saw
new file mode 100644
index 000000000..374feab46
--- /dev/null
+++ b/intTests/test_type_errors/err029.saw
@@ -0,0 +1,9 @@
+//
+// Too many arguments for type constructor: Term
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : Term Int = {{ 3 }};
+
+
diff --git a/intTests/test_type_errors/err030.log.good b/intTests/test_type_errors/err030.log.good
new file mode 100644
index 000000000..b94ddf2aa
--- /dev/null
+++ b/intTests/test_type_errors/err030.log.good
@@ -0,0 +1,3 @@
+ Loading file "err030.saw"
+ Parse error at err030.saw:7:14-7:17: Unexpected `Int'
+FAILED
diff --git a/intTests/test_type_errors/err030.saw b/intTests/test_type_errors/err030.saw
new file mode 100644
index 000000000..8ddae3f5f
--- /dev/null
+++ b/intTests/test_type_errors/err030.saw
@@ -0,0 +1,9 @@
+//
+// Too many arguments for type constructor: Type
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : Type Int = {| [8] |};
+
+
diff --git a/intTests/test_type_errors/err031.log.good b/intTests/test_type_errors/err031.log.good
new file mode 100644
index 000000000..81a1ff965
--- /dev/null
+++ b/intTests/test_type_errors/err031.log.good
@@ -0,0 +1,3 @@
+ Loading file "err031.saw"
+ Parse error at err031.saw:7:14-7:17: Unexpected `Int'
+FAILED
diff --git a/intTests/test_type_errors/err031.saw b/intTests/test_type_errors/err031.saw
new file mode 100644
index 000000000..1387a23e2
--- /dev/null
+++ b/intTests/test_type_errors/err031.saw
@@ -0,0 +1,9 @@
+//
+// Too many arguments for type constructor: Bool
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : Bool Int = false;
+
+
diff --git a/intTests/test_type_errors/err032.log.good b/intTests/test_type_errors/err032.log.good
new file mode 100644
index 000000000..0cc33e807
--- /dev/null
+++ b/intTests/test_type_errors/err032.log.good
@@ -0,0 +1,3 @@
+ Loading file "err032.saw"
+ Parse error at err032.saw:7:13-7:17: Unexpected `Bool'
+FAILED
diff --git a/intTests/test_type_errors/err032.saw b/intTests/test_type_errors/err032.saw
new file mode 100644
index 000000000..e8f560101
--- /dev/null
+++ b/intTests/test_type_errors/err032.saw
@@ -0,0 +1,10 @@
+//
+// Too many arguments for type constructor: Int
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : Int Bool = false;
+
+
+
diff --git a/intTests/test_type_errors/err033.log.good b/intTests/test_type_errors/err033.log.good
new file mode 100644
index 000000000..5af3320dd
--- /dev/null
+++ b/intTests/test_type_errors/err033.log.good
@@ -0,0 +1,3 @@
+ Loading file "err033.saw"
+ Parse error at err033.saw:7:18-7:19: Unexpected `='
+FAILED
diff --git a/intTests/test_type_errors/err033.saw b/intTests/test_type_errors/err033.saw
new file mode 100644
index 000000000..519689791
--- /dev/null
+++ b/intTests/test_type_errors/err033.saw
@@ -0,0 +1,7 @@
+//
+// Not enough arguments for type constructor: monads
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : TopLevel = false;
diff --git a/intTests/test_type_errors/err034.log.good b/intTests/test_type_errors/err034.log.good
new file mode 100644
index 000000000..e35031961
--- /dev/null
+++ b/intTests/test_type_errors/err034.log.good
@@ -0,0 +1,3 @@
+ Loading file "err034.saw"
+ Parse error at err034.saw:7:22-7:25: Unexpected `Int'
+FAILED
diff --git a/intTests/test_type_errors/err034.saw b/intTests/test_type_errors/err034.saw
new file mode 100644
index 000000000..29955c9a0
--- /dev/null
+++ b/intTests/test_type_errors/err034.saw
@@ -0,0 +1,7 @@
+//
+// Too many arguments for type constructor: monads
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : TopLevel Int Int = return 0;
diff --git a/intTests/test_type_errors/err035.log.good b/intTests/test_type_errors/err035.log.good
new file mode 100644
index 000000000..6a8f48e6b
--- /dev/null
+++ b/intTests/test_type_errors/err035.log.good
@@ -0,0 +1,3 @@
+ Loading file "err035.saw"
+ Parse error at err035.saw:7:20-7:23: Unexpected `Int'
+FAILED
diff --git a/intTests/test_type_errors/err035.saw b/intTests/test_type_errors/err035.saw
new file mode 100644
index 000000000..8d4d50d3e
--- /dev/null
+++ b/intTests/test_type_errors/err035.saw
@@ -0,0 +1,7 @@
+//
+// Too many arguments for type: records
+//
+// Currently this is a parser message; the kind mismatch message in
+// the typechecker is unreachable.
+
+let x : { a: Int } Int = { a = 3 };
diff --git a/intTests/test_type_errors/err036.log.good b/intTests/test_type_errors/err036.log.good
new file mode 100644
index 000000000..741f7ac4d
--- /dev/null
+++ b/intTests/test_type_errors/err036.log.good
@@ -0,0 +1,12 @@
+ Loading file "err036.saw"
+ err036.saw:9:17-9:18: Type mismatch.
+    Mismatch of type constructors. Expected: <Block> but got Int
+    err036.saw:9:9-9:14: The type Int Int arises from this type annotation
+    err036.saw:9:17-9:18: The type Int arises from the type of this term
+    
+    Expected: Int Int
+    Found:    Int
+    
+    within "x" (err036.saw:9:5-9:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err036.saw b/intTests/test_type_errors/err036.saw
new file mode 100644
index 000000000..76a029464
--- /dev/null
+++ b/intTests/test_type_errors/err036.saw
@@ -0,0 +1,9 @@
+//
+// Too many arguments for type: named type variables
+//
+// This is _not_ a parser message, unlike all the other cases of this
+// form, because the parser allows both the forms "t" and "t1 t2".
+
+typedef t = Int;
+
+let x : t Int = 3;
diff --git a/intTests/test_type_errors/err037.log.good b/intTests/test_type_errors/err037.log.good
new file mode 100644
index 000000000..11b83d5c6
--- /dev/null
+++ b/intTests/test_type_errors/err037.log.good
@@ -0,0 +1,12 @@
+ Loading file "err037.saw"
+ err037.saw:9:18-9:33: Type mismatch.
+    Mismatch of type constructors. Expected: ([]) but got (->)
+    err037.saw:9:10-9:15: The type [Int] arises from this type annotation
+    err037.saw:7:15-7:35: The type [Int] -> [Int] arises from the context of the term
+    
+    Expected: [Int]
+    Found:    [Int] -> [Int]
+    
+    within "xs" (err037.saw:9:5-9:7)
+
+FAILED
diff --git a/intTests/test_type_errors/err037.saw b/intTests/test_type_errors/err037.saw
new file mode 100644
index 000000000..a01a9760e
--- /dev/null
+++ b/intTests/test_type_errors/err037.saw
@@ -0,0 +1,9 @@
+//
+// Specifically check for not enough arguments to a function.
+//
+// This is (has to be) a slightly contrived case with explicit type
+// signatures in order to trigger an explicit mismatch.
+
+let f x y z = concat x (concat y z);
+
+let xs : [Int] = f [1, 2] [3, 4];
diff --git a/intTests/test_type_errors/err038.log.good b/intTests/test_type_errors/err038.log.good
new file mode 100644
index 000000000..09d05065a
--- /dev/null
+++ b/intTests/test_type_errors/err038.log.good
@@ -0,0 +1,12 @@
+ Loading file "err038.saw"
+ err038.saw:10:16-10:17: Type mismatch.
+    Mismatch of type constructors. Expected: ([]) but got (->)
+    internal:1:5-1:8: The type [t.4] arises from this type annotation
+    err038.saw:7:15-7:35: The type [Int] -> [Int] arises from the context of the term
+    
+    Expected: [t.4]
+    Found:    [Int] -> [Int]
+    
+    within "t" (err038.saw:10:5-10:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err038.saw b/intTests/test_type_errors/err038.saw
new file mode 100644
index 000000000..305ce8002
--- /dev/null
+++ b/intTests/test_type_errors/err038.saw
@@ -0,0 +1,10 @@
+//
+// Check for not enough arguments to a function.
+//
+// This is the general case (without explicit signatures) where you
+// get an expected/unwanted function type that fails downstream.
+
+let f x y z = concat x (concat y z);
+
+let s = f [1, 2] [3, 4];
+let t = concat s [5, 6];
diff --git a/intTests/test_type_errors/err039.log.good b/intTests/test_type_errors/err039.log.good
new file mode 100644
index 000000000..07462204a
--- /dev/null
+++ b/intTests/test_type_errors/err039.log.good
@@ -0,0 +1,12 @@
+ Loading file "err039.saw"
+ err039.saw:7:10-7:25: Type mismatch.
+    Term is not a function. (Maybe a function is applied to too many arguments?)
+    err039.saw:7:10-7:25: The type t.0 -> t.1 arises from the context of the term
+    internal:1:19-1:22: The type [Int] arises from this type annotation
+    
+    Expected: t.0 -> t.1
+    Found:    [Int]
+    
+    within "xs" (err039.saw:7:5-7:7)
+
+FAILED
diff --git a/intTests/test_type_errors/err039.saw b/intTests/test_type_errors/err039.saw
new file mode 100644
index 000000000..6f85a11af
--- /dev/null
+++ b/intTests/test_type_errors/err039.saw
@@ -0,0 +1,7 @@
+//
+// Check for too many arguments to a function.
+//
+
+let f x y = concat x y;
+
+let xs = f [1, 2] [3, 4] [5, 6];
diff --git a/intTests/test_type_errors/err040.log.good b/intTests/test_type_errors/err040.log.good
new file mode 100644
index 000000000..9492dc7f9
--- /dev/null
+++ b/intTests/test_type_errors/err040.log.good
@@ -0,0 +1,15 @@
+ Loading file "err040.saw"
+ err040.saw:8:11-8:26: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    err040.saw:7:23-7:26: The type Int arises from this type annotation
+    err040.saw:8:18-8:23: The type String arises from the type of this term
+    
+    Expected: Int
+    Found:    String
+    
+    Expected: (Int, Int, Int)
+    Found:    (Int, Int, String)
+    
+    within "x" (err040.saw:8:5-8:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err040.saw b/intTests/test_type_errors/err040.saw
new file mode 100644
index 000000000..ac60441ae
--- /dev/null
+++ b/intTests/test_type_errors/err040.saw
@@ -0,0 +1,8 @@
+//
+// Check what happens when tuple members don't match.
+//
+// (This is to specifically trigger the selective refinement of the
+// printed mismatch.)
+
+let f (x : (Int, Int, Int)) = (x.1, x.2, x.0);
+let x = f (1, 2, "three");
diff --git a/intTests/test_type_errors/err041.log.good b/intTests/test_type_errors/err041.log.good
new file mode 100644
index 000000000..0bfd1088d
--- /dev/null
+++ b/intTests/test_type_errors/err041.log.good
@@ -0,0 +1,15 @@
+ Loading file "err041.saw"
+ err041.saw:9:11-9:14: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    err041.saw:7:25-7:28: The type Int arises from this type annotation
+    err041.saw:5:31-5:37: The type String arises from this type annotation
+    
+    Expected: Int
+    Found:    String
+    
+    Expected: Int -> Int -> Int -> Int
+    Found:    Int -> Int -> String -> Int
+    
+    within "x" (err041.saw:9:5-9:6)
+
+FAILED
diff --git a/intTests/test_type_errors/err041.saw b/intTests/test_type_errors/err041.saw
new file mode 100644
index 000000000..f64585a4a
--- /dev/null
+++ b/intTests/test_type_errors/err041.saw
@@ -0,0 +1,9 @@
+//
+// Specifically trigger the selective refinement of the printed
+// mismatch of function types.
+
+let foo (a: Int) (b: Int) (c: String) : Int = a;
+
+let g (f: Int -> Int -> Int -> Int) (x: Int) = f x x x;
+
+let x = g foo 3;
diff --git a/intTests/test_type_errors/err042.log.good b/intTests/test_type_errors/err042.log.good
new file mode 100644
index 000000000..028977093
--- /dev/null
+++ b/intTests/test_type_errors/err042.log.good
@@ -0,0 +1,5 @@
+ Loading file "err042.saw"
+ Stack trace:
+Not a monomorphic type: [t.5]
+
+FAILED
diff --git a/intTests/test_type_errors/err042.saw b/intTests/test_type_errors/err042.saw
new file mode 100644
index 000000000..e2670d5fb
--- /dev/null
+++ b/intTests/test_type_errors/err042.saw
@@ -0,0 +1,7 @@
+//
+// Trigger the "Not a monomorphic type" message associated with
+// polymorphic binds.
+//
+// In this test, trigger it at the top level.
+
+_ <- return [];
diff --git a/intTests/test_type_errors/err043.log.good b/intTests/test_type_errors/err043.log.good
new file mode 100644
index 000000000..3ee943c6d
--- /dev/null
+++ b/intTests/test_type_errors/err043.log.good
@@ -0,0 +1,5 @@
+ Loading file "err043.saw"
+ Stack trace:
+Not a monomorphic type: t.7 -> t.7
+
+FAILED
diff --git a/intTests/test_type_errors/err043.saw b/intTests/test_type_errors/err043.saw
new file mode 100644
index 000000000..60b86b78f
--- /dev/null
+++ b/intTests/test_type_errors/err043.saw
@@ -0,0 +1,9 @@
+//
+// Trigger the "Not a monomorphic type" message associated with
+// polymorphic binds.
+//
+// In this test, trigger it in a top-level nested do-block.
+
+_ <- do {
+   return (\a -> a);
+};
diff --git a/intTests/test_type_errors/err044.log.good b/intTests/test_type_errors/err044.log.good
new file mode 100644
index 000000000..22d612ae8
--- /dev/null
+++ b/intTests/test_type_errors/err044.log.good
@@ -0,0 +1 @@
+ Loading file "err044.saw"
diff --git a/intTests/test_type_errors/err044.saw b/intTests/test_type_errors/err044.saw
new file mode 100644
index 000000000..4096c5066
--- /dev/null
+++ b/intTests/test_type_errors/err044.saw
@@ -0,0 +1,12 @@
+//
+// Trigger the "Not a monomorphic type" message associated with
+// polymorphic binds.
+//
+// In this test, attempt to trigger it inside a let-binding. It
+// does not fail, because the let-binding gets generalized and
+// the polymorphism gets bound there.
+
+let f = do {
+    x <- return (\a -> a);
+    return x;
+};
diff --git a/intTests/test_type_errors/unify000.log.good b/intTests/test_type_errors/unify000.log.good
new file mode 100644
index 000000000..7d197026f
--- /dev/null
+++ b/intTests/test_type_errors/unify000.log.good
@@ -0,0 +1 @@
+ Loading file "unify000.saw"
diff --git a/intTests/test_type_errors/unify000.saw b/intTests/test_type_errors/unify000.saw
new file mode 100644
index 000000000..759237078
--- /dev/null
+++ b/intTests/test_type_errors/unify000.saw
@@ -0,0 +1,11 @@
+//
+// Exercise failure of the unify call in the Index case of inferExpr.
+//
+// (XXX: we can't. There's no concrete syntax for it and no other
+// way to generate it. So this test will be a placeholder until
+// either we add a syntax or remove the construction.)
+//
+
+let x = [1,2,3];
+
+
diff --git a/intTests/test_type_errors/unify001.log.good b/intTests/test_type_errors/unify001.log.good
new file mode 100644
index 000000000..93293745b
--- /dev/null
+++ b/intTests/test_type_errors/unify001.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify001.saw"
+ unify001.saw:8:10-8:11: Type mismatch.
+    Mismatch of type constructors. Expected: String but got Int
+    unify001.saw:8:14-8:20: The type String arises from this type annotation
+    unify001.saw:8:10-8:11: The type Int arises from the type of this term
+    
+    Expected: String
+    Found:    Int
+    
+    within "x" (unify001.saw:8:5-8:6)
+
+FAILED
diff --git a/intTests/test_type_errors/unify001.saw b/intTests/test_type_errors/unify001.saw
new file mode 100644
index 000000000..b18f88b1c
--- /dev/null
+++ b/intTests/test_type_errors/unify001.saw
@@ -0,0 +1,8 @@
+//
+// Exercise failure of the unify call in the TSig (type signature)
+// case of inferExpr. This is the unification of the array value's
+// type with (Array t).
+//
+
+
+let x = (3 : String);
diff --git a/intTests/test_type_errors/unify002.log.good b/intTests/test_type_errors/unify002.log.good
new file mode 100644
index 000000000..10f2e3bed
--- /dev/null
+++ b/intTests/test_type_errors/unify002.log.good
@@ -0,0 +1,18 @@
+ Loading file "unify002.saw"
+ Type errors:
+  unify002.saw:7:13-7:16: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    unify002.saw:7:10-7:11: The type Int arises from the type of this term
+    unify002.saw:7:13-7:16: The type String arises from the type of this term
+    
+    Expected: Int
+    Found:    String
+    
+    within "x" (unify002.saw:7:5-7:6)
+
+  unify002.saw:7:23-7:27: Unbound variable: "True" (unify002.saw:7:23-7:27)
+Note that some built-in commands are available only after running
+either `enable_deprecated` or `enable_experimental`.
+
+
+FAILED
diff --git a/intTests/test_type_errors/unify002.saw b/intTests/test_type_errors/unify002.saw
new file mode 100644
index 000000000..eebddfb71
--- /dev/null
+++ b/intTests/test_type_errors/unify002.saw
@@ -0,0 +1,8 @@
+//
+// Exercise failure of the unify call (via checkExpr) in the Array
+// case of inferExpr. This is the check of the second and subsequent
+// elements against the first.
+//
+
+let x = [1, "abc", 2, True];
+
diff --git a/intTests/test_type_errors/unify003.log.good b/intTests/test_type_errors/unify003.log.good
new file mode 100644
index 000000000..e2338afc6
--- /dev/null
+++ b/intTests/test_type_errors/unify003.log.good
@@ -0,0 +1 @@
+ Loading file "unify003.saw"
diff --git a/intTests/test_type_errors/unify003.saw b/intTests/test_type_errors/unify003.saw
new file mode 100644
index 000000000..cd37109fb
--- /dev/null
+++ b/intTests/test_type_errors/unify003.saw
@@ -0,0 +1,12 @@
+//
+// Exercise failure of the unify call (via checkExpr) in the Index
+// case of inferExpr. This is the check of the index expression
+// against Int.
+//
+// (XXX: we can't. There's no concrete syntax for it and no other
+// way to generate it. So this test will be a placeholder until
+// either we add a syntax or remove the construction.)
+//
+
+let x = [1, 2, 3];
+
diff --git a/intTests/test_type_errors/unify004.log.good b/intTests/test_type_errors/unify004.log.good
new file mode 100644
index 000000000..efbda48ad
--- /dev/null
+++ b/intTests/test_type_errors/unify004.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify004.saw"
+ unify004.saw:8:9-8:10: Type mismatch.
+    Term is not a function. (Maybe a function is applied to too many arguments?)
+    unify004.saw:8:9-8:10: The type t.0 -> t.1 arises from the context of the term
+    unify004.saw:7:9-7:10: The type Int arises from the type of this term
+    
+    Expected: t.0 -> t.1
+    Found:    Int
+    
+    within "x" (unify004.saw:8:5-8:6)
+
+FAILED
diff --git a/intTests/test_type_errors/unify004.saw b/intTests/test_type_errors/unify004.saw
new file mode 100644
index 000000000..eeead5e5f
--- /dev/null
+++ b/intTests/test_type_errors/unify004.saw
@@ -0,0 +1,10 @@
+//
+// Exercise failure of the first unify call (via checkExpr) in the
+// Application case of inferExpr. This is the check of the function
+// against (->).
+//
+
+let q = 3;
+let x = q 6;
+
+
diff --git a/intTests/test_type_errors/unify005.log.good b/intTests/test_type_errors/unify005.log.good
new file mode 100644
index 000000000..5e4c4e4d6
--- /dev/null
+++ b/intTests/test_type_errors/unify005.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify005.saw"
+ unify005.saw:8:11-8:15: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got Bool
+    unify005.saw:7:12-7:15: The type Int arises from this type annotation
+    internal:1:1-1:5: The type Bool arises from this type annotation
+    
+    Expected: Int
+    Found:    Bool
+    
+    within "x" (unify005.saw:8:5-8:6)
+
+FAILED
diff --git a/intTests/test_type_errors/unify005.saw b/intTests/test_type_errors/unify005.saw
new file mode 100644
index 000000000..53a971830
--- /dev/null
+++ b/intTests/test_type_errors/unify005.saw
@@ -0,0 +1,11 @@
+//
+// Exercise failure of the second unify call (via checkExpr) in the
+// Application case of inferExpr. This is the check of the function
+// argument against the function's argument type.
+//
+
+let f (x : Int) = x;
+let x = f true;
+
+
+
diff --git a/intTests/test_type_errors/unify006.log.good b/intTests/test_type_errors/unify006.log.good
new file mode 100644
index 000000000..2f178a3d0
--- /dev/null
+++ b/intTests/test_type_errors/unify006.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify006.saw"
+ unify006.saw:7:22-7:23: Type mismatch.
+    Mismatch of type constructors. Expected: Bool but got Int
+    unify006.saw:7:22-7:23: The type Bool arises from the context of the term
+    unify006.saw:7:12-7:15: The type Int arises from this type annotation
+    
+    Expected: Bool
+    Found:    Int
+    
+    within "f" (unify006.saw:7:5-7:6)
+
+FAILED
diff --git a/intTests/test_type_errors/unify006.saw b/intTests/test_type_errors/unify006.saw
new file mode 100644
index 000000000..090047d21
--- /dev/null
+++ b/intTests/test_type_errors/unify006.saw
@@ -0,0 +1,11 @@
+//
+// Exercise failure of the first unify call (via checkExpr) in the
+// IfThenElse case of inferExpr. This is the check of the condition
+// against Bool.
+//
+
+let f (x : Int) = if x then 1 else 2;
+
+
+
+
diff --git a/intTests/test_type_errors/unify007.log.good b/intTests/test_type_errors/unify007.log.good
new file mode 100644
index 000000000..937a2adb5
--- /dev/null
+++ b/intTests/test_type_errors/unify007.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify007.saw"
+ unify007.saw:7:37-7:39: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    unify007.saw:7:30-7:31: The type Int arises from the type of this term
+    unify007.saw:7:37-7:39: The type String arises from the type of this term
+    
+    Expected: Int
+    Found:    String
+    
+    within "f" (unify007.saw:7:5-7:6)
+
+FAILED
diff --git a/intTests/test_type_errors/unify007.saw b/intTests/test_type_errors/unify007.saw
new file mode 100644
index 000000000..3e1d40fb2
--- /dev/null
+++ b/intTests/test_type_errors/unify007.saw
@@ -0,0 +1,7 @@
+//
+// Exercise failure of the second unify call (via checkExpr) in the
+// IfThenElse case of inferExpr. This is the consistency check for the
+// true and false branches.
+//
+
+let f (b : Bool) = if b then 1 else "hi";
diff --git a/intTests/test_type_errors/unify008.log.good b/intTests/test_type_errors/unify008.log.good
new file mode 100644
index 000000000..6e0707adb
--- /dev/null
+++ b/intTests/test_type_errors/unify008.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify008.saw"
+ unify008.saw:15:6-15:12: Type mismatch.
+    Mismatch of type constructors. Expected: String but got Int
+    unify008.saw:15:16-15:19: The type String arises from the type of this term
+    unify008.saw:15:9-15:12: The type Int arises from this type annotation
+    
+    Expected: String
+    Found:    Int
+    
+    within "x" (unify008.saw:15:6-15:7)
+
+FAILED
diff --git a/intTests/test_type_errors/unify008.saw b/intTests/test_type_errors/unify008.saw
new file mode 100644
index 000000000..67c148e63
--- /dev/null
+++ b/intTests/test_type_errors/unify008.saw
@@ -0,0 +1,16 @@
+//
+// Exercise failure of the unify call in checkPattern. This is for
+// checking a pattern against the thing it binds.
+//
+// There are two ways to get to this; for the sake of completeness
+// this case goes via inferDecl (a single let) and there's another one
+// that goes via inferRecDecls (a collection of mutually recursive
+// lets).
+//
+// There's also two forms of let (pure and monadic) but for the moment
+// at least the typechecker behavior is shared such that there's
+// nothing to be gained by testing both.
+//
+
+let (x: Int) = "abc";
+
diff --git a/intTests/test_type_errors/unify009.log.good b/intTests/test_type_errors/unify009.log.good
new file mode 100644
index 000000000..4a11d1eea
--- /dev/null
+++ b/intTests/test_type_errors/unify009.log.good
@@ -0,0 +1,12 @@
+ Loading file "unify009.saw"
+ unify009.saw:21:6-21:12: Type mismatch.
+    Mismatch of type constructors. Expected: String but got Int
+    unify009.saw:21:16-21:19: The type String arises from the type of this term
+    unify009.saw:21:9-21:12: The type Int arises from this type annotation
+    
+    Expected: String
+    Found:    Int
+    
+    within "x" (unify009.saw:20:6-20:7)
+
+FAILED
diff --git a/intTests/test_type_errors/unify009.saw b/intTests/test_type_errors/unify009.saw
new file mode 100644
index 000000000..b8cae9b48
--- /dev/null
+++ b/intTests/test_type_errors/unify009.saw
@@ -0,0 +1,23 @@
+//
+// Exercise failure of the unify call in checkPattern. This is for
+// checking a pattern against the thing it binds.
+//
+// There are two ways to get to this; for the sake of completeness
+// this case goes via inferRecDecls (a collection of mutually
+// recursive lets) and there's another one that goes via inferDecl (a
+// single let).
+//
+// There's also two forms of let (pure and monadic) but for the moment
+// at least the typechecker behavior is shared such that there's
+// nothing to be gained by testing both.
+//
+// We don't need to test all the different kinds of patterns here;
+// those differ _in_ unify but not in the call _to_ unify, and the
+// goal of this test set is to make sure that the calls to unify
+// are correct and don't e.g. have found/expected backwards.
+//
+
+rec (x: Int) = 3
+and (y: Int) = "abc";
+
+
diff --git a/intTests/test_type_errors/unify010.log.good b/intTests/test_type_errors/unify010.log.good
new file mode 100644
index 000000000..4a9f37a5a
--- /dev/null
+++ b/intTests/test_type_errors/unify010.log.good
@@ -0,0 +1,18 @@
+ Loading file "unify010.saw"
+ Type errors:
+  unify010.saw:9:17-9:27: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    unify010.saw:9:9-9:12: The type Int arises from this type annotation
+    unify010.saw:9:24-9:27: The type String arises from the type of this term
+    
+    Expected: Int
+    Found:    String
+    
+    Expected: t.0 Int
+    Found:    t.3 String
+    
+    within "_" (unify010.saw:8:5-8:6)
+
+  unify010.saw:8:9-10:2: do block must end with expression at "_" (unify010.saw:8:5-8:6)
+
+FAILED
diff --git a/intTests/test_type_errors/unify010.saw b/intTests/test_type_errors/unify010.saw
new file mode 100644
index 000000000..2f89d58cc
--- /dev/null
+++ b/intTests/test_type_errors/unify010.saw
@@ -0,0 +1,10 @@
+//
+// Exercise failure of the unify call in the correctly-typed case of
+// StmtBind in inferStmt.
+//
+// This checks the pattern against the value being bound to it.
+//
+
+let _ = do {
+   (x : Int) <- return "abc";
+};
diff --git a/intTests/test_type_errors/unify011.log.good b/intTests/test_type_errors/unify011.log.good
new file mode 100644
index 000000000..56790e78d
--- /dev/null
+++ b/intTests/test_type_errors/unify011.log.good
@@ -0,0 +1,14 @@
+ Loading file "unify011.saw"
+ unify011.saw:12:2-12:17: Warning: Monadic bind of non-monadic value; rewrite as let-binding or use return
+ unify011.saw:12:2-12:17: Warning: This will become an error in a future release of SAW
+ unify011.saw:12:14-12:17: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got String
+    unify011.saw:12:6-12:9: The type Int arises from this type annotation
+    unify011.saw:12:14-12:17: The type String arises from the type of this term
+    
+    Expected: Int
+    Found:    String
+    
+    within "<toplevel>" (unify011.saw:12:2-12:17)
+
+FAILED
diff --git a/intTests/test_type_errors/unify011.saw b/intTests/test_type_errors/unify011.saw
new file mode 100644
index 000000000..8808a3569
--- /dev/null
+++ b/intTests/test_type_errors/unify011.saw
@@ -0,0 +1,12 @@
+//
+// Exercise failure of the unify call in the incorrectly non-monadic
+// case of StmtBind in inferStmt. (This case was accepted prior to
+// December 2024 and now has its own special-cased unify call.
+//
+// The special case applies only at the syntactic top leel.
+//
+// This checks the pattern against the value being bound to it,
+// but allows it to not be in a monad.
+//
+
+(x : Int) <- "abc";
diff --git a/intTests/test_type_errors/unify012.log.good b/intTests/test_type_errors/unify012.log.good
new file mode 100644
index 000000000..77de307c2
--- /dev/null
+++ b/intTests/test_type_errors/unify012.log.good
@@ -0,0 +1,15 @@
+ Loading file "unify012.saw"
+ unify012.saw:14:2-14:14: Warning: Monadic bind with the wrong monad; found LLVMSetup but expected TopLevel
+ unify012.saw:14:2-14:14: Warning: This creates the action but does not execute it; if you meant to do that, prefix the expression with return
+ unify012.saw:14:2-14:14: Warning: This will become an error in a future release of SAW
+ unify012.saw:14:13-14:14: Type mismatch.
+    Mismatch of type constructors. Expected: () but got <Block>
+    unify012.saw:14:6-14:8: The type () arises from this type annotation
+    unify012.saw:14:2-14:14: The type LLVMSetup () arises from this type annotation
+    
+    Expected: ()
+    Found:    LLVMSetup ()
+    
+    within "<toplevel>" (unify012.saw:14:2-14:14)
+
+FAILED
diff --git a/intTests/test_type_errors/unify012.saw b/intTests/test_type_errors/unify012.saw
new file mode 100644
index 000000000..f0f6d8997
--- /dev/null
+++ b/intTests/test_type_errors/unify012.saw
@@ -0,0 +1,14 @@
+//
+// Exercise failure of the unify call in the incorrect wrong-monadic
+// case of StmtBind in inferStmt. (This case was accepted prior to
+// December 2024 and now has its own special-cased unify call.
+//
+// The special case applies only at the syntactic top leel.
+//
+// This checks the pattern against the value being bound to it,
+// but allows it to be in the wrong monad.
+//
+
+let m : LLVMSetup () = llvm_assert {{ True }};
+
+(x : ()) <- m;
diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs
index 94061899d..964884061 100644
--- a/src/SAWScript/MGU.hs
+++ b/src/SAWScript/MGU.hs
@@ -740,6 +740,19 @@ mgus t1s t2s = case (t1s, t2s) of
       -- XXX this is no good, it will always print one of the lengths as 0!
       -- (also, note that this is only reachable for type constructor args
       -- and not function args)
+      --
+      -- dholland 20250106: I believe this is currently unreachable.
+      -- mgus is called from two places above (record fields and type
+      -- constructor arguments); the record fields case always passes
+      -- lists of the same length. The situation with type constructor
+      -- arguments is murkier. However, there are only a handful of
+      -- builtin types whose constructors take arguments at all:
+      -- tuples, lists, functions, and monads/contexts/blocks. The
+      -- parser special-cases the syntax for all of these, so that you
+      -- apparently can't produce partially applied instances for
+      -- any. (And for tuples, the arity is part of the constructor,
+      -- so tuples of different arity won't get as far as trying to
+      -- unify the arguments.)
       failMGU' $ "Wrong number of arguments. Expected " ++ show (length t1s) ++
                  " but got " ++ show (length t2s)
 
@@ -923,6 +936,8 @@ inferExpr (ln, expr) = case expr of
        let ty = TyRecord (PosInferred InfTerm pos) $ M.fromList nts
        return (Record pos (M.fromList nes'), ty)
 
+  -- XXX this is currently unreachable because there's no concrete
+  -- syntax for it; the parser will never produce it.
   Index pos ar ix ->
     do (ar',at) <- inferExpr (ln,ar)
        ix'      <- checkExpr ln ix (tInt (PosInferred InfContext (getPos ix)))
@@ -1488,6 +1503,13 @@ checkType kind ty = case ty of
       let nparams = length params
           nargs = length args
           argsleft = kindNumArgs kind
+
+      -- XXX: the failures are all currently unreachable, because the
+      -- parser does not permit writing mis-kinded types. This should
+      -- probably be changed, both for ergonomic reasons (messages
+      -- about wrong type arguments are better than syntax errors) and
+      -- also because all the special cases in the parser are ugly.
+
       if nargs > nparams then do
           -- XXX special case for BlockCon (remove along with BlockCon)
           case (tycon, args) of
@@ -1507,11 +1529,14 @@ checkType kind ty = case ty of
                            " but found " ++ (pShow $ Kind (nparams - nargs)))
           getErrorTyVar pos
       else do
-          -- note that this will ignore the extra params
+          -- note that this will ignore the extra params, and return
+          -- a list of the same length as the args given
           args' <- zipWithM checkType params args
           return $ TyCon pos tycon args'
 
   TyRecord pos fields -> do
+      -- XXX as with TyCon the failure is currently unreachable
+      -- because the parser can't be made to produce mis-kinded types.
       if kind /= kindStar then do
           recordError pos ("Kind mismatch: expected " ++ pShow kind ++
                            " but found " ++ pShow kindStar)