From bcdb0608dd18c691c9fabcff9d01edc6a222b29a Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 15 Jan 2025 14:28:39 -0500 Subject: [PATCH 1/2] Fix bug in test-and-diff.sh. Need to use the 'g' flag for multiple substitutions in the seddery for pruning the absolute paths to the test files from the test outputs. Otherwise messages that have multiple copies on the same line don't get handled correctly. --- intTests/support/test-and-diff.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. From a72e7adf24c2d580556e985db8d83be4baec8065 Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 8 Jan 2025 16:18:42 -0500 Subject: [PATCH 2/2] Add more typechecker tests. This includes one test for each print, additional tests for several of the common cases that we want to print comprehensibly, and additionally a separate set of tests for each call to unify that is supposed to make sure the found/expected types don't get swapped. (Which is extremely easy to have happen, because conceptually unification is symmetric but the found/expected reporting isn't.) Also add some notes to the typechecker code, because it turns out some of the typechecker messages are currently unreachable. --- intTests/test_type_errors/err013.log.good | 9 +++ intTests/test_type_errors/err013.saw | 9 +++ intTests/test_type_errors/err014.log.good | 12 ++++ intTests/test_type_errors/err014.saw | 12 ++++ intTests/test_type_errors/err015.log.good | 54 +++++++++++++++++ intTests/test_type_errors/err015.saw | 65 +++++++++++++++++++++ intTests/test_type_errors/err016.log.good | 12 ++++ intTests/test_type_errors/err016.saw | 5 ++ intTests/test_type_errors/err017.log.good | 12 ++++ intTests/test_type_errors/err017.saw | 28 +++++++++ intTests/test_type_errors/err018.log.good | 15 +++++ intTests/test_type_errors/err018.saw | 27 +++++++++ intTests/test_type_errors/err019.log.good | 12 ++++ intTests/test_type_errors/err019.saw | 5 ++ intTests/test_type_errors/err020.log.good | 5 ++ intTests/test_type_errors/err020.saw | 3 + intTests/test_type_errors/err021.log.good | 5 ++ intTests/test_type_errors/err021.saw | 8 +++ intTests/test_type_errors/err022.log.good | 5 ++ intTests/test_type_errors/err022.saw | 3 + intTests/test_type_errors/err023.log.good | 5 ++ intTests/test_type_errors/err023.saw | 5 ++ intTests/test_type_errors/err024.log.good | 6 ++ intTests/test_type_errors/err024.saw | 3 + intTests/test_type_errors/err025.log.good | 3 + intTests/test_type_errors/err025.saw | 3 + intTests/test_type_errors/err026.log.good | 3 + intTests/test_type_errors/err026.saw | 5 ++ intTests/test_type_errors/err027.log.good | 3 + intTests/test_type_errors/err027.saw | 9 +++ intTests/test_type_errors/err028.log.good | 3 + intTests/test_type_errors/err028.saw | 9 +++ intTests/test_type_errors/err029.log.good | 3 + intTests/test_type_errors/err029.saw | 9 +++ intTests/test_type_errors/err030.log.good | 3 + intTests/test_type_errors/err030.saw | 9 +++ intTests/test_type_errors/err031.log.good | 3 + intTests/test_type_errors/err031.saw | 9 +++ intTests/test_type_errors/err032.log.good | 3 + intTests/test_type_errors/err032.saw | 10 ++++ intTests/test_type_errors/err033.log.good | 3 + intTests/test_type_errors/err033.saw | 7 +++ intTests/test_type_errors/err034.log.good | 3 + intTests/test_type_errors/err034.saw | 7 +++ intTests/test_type_errors/err035.log.good | 3 + intTests/test_type_errors/err035.saw | 7 +++ intTests/test_type_errors/err036.log.good | 12 ++++ intTests/test_type_errors/err036.saw | 9 +++ intTests/test_type_errors/err037.log.good | 12 ++++ intTests/test_type_errors/err037.saw | 9 +++ intTests/test_type_errors/err038.log.good | 12 ++++ intTests/test_type_errors/err038.saw | 10 ++++ intTests/test_type_errors/err039.log.good | 12 ++++ intTests/test_type_errors/err039.saw | 7 +++ intTests/test_type_errors/err040.log.good | 15 +++++ intTests/test_type_errors/err040.saw | 8 +++ intTests/test_type_errors/err041.log.good | 15 +++++ intTests/test_type_errors/err041.saw | 9 +++ intTests/test_type_errors/err042.log.good | 5 ++ intTests/test_type_errors/err042.saw | 7 +++ intTests/test_type_errors/err043.log.good | 5 ++ intTests/test_type_errors/err043.saw | 9 +++ intTests/test_type_errors/err044.log.good | 1 + intTests/test_type_errors/err044.saw | 12 ++++ intTests/test_type_errors/unify000.log.good | 1 + intTests/test_type_errors/unify000.saw | 11 ++++ intTests/test_type_errors/unify001.log.good | 12 ++++ intTests/test_type_errors/unify001.saw | 8 +++ intTests/test_type_errors/unify002.log.good | 18 ++++++ intTests/test_type_errors/unify002.saw | 8 +++ intTests/test_type_errors/unify003.log.good | 1 + intTests/test_type_errors/unify003.saw | 12 ++++ intTests/test_type_errors/unify004.log.good | 12 ++++ intTests/test_type_errors/unify004.saw | 10 ++++ intTests/test_type_errors/unify005.log.good | 12 ++++ intTests/test_type_errors/unify005.saw | 11 ++++ intTests/test_type_errors/unify006.log.good | 12 ++++ intTests/test_type_errors/unify006.saw | 11 ++++ intTests/test_type_errors/unify007.log.good | 12 ++++ intTests/test_type_errors/unify007.saw | 7 +++ intTests/test_type_errors/unify008.log.good | 12 ++++ intTests/test_type_errors/unify008.saw | 16 +++++ intTests/test_type_errors/unify009.log.good | 12 ++++ intTests/test_type_errors/unify009.saw | 23 ++++++++ intTests/test_type_errors/unify010.log.good | 18 ++++++ intTests/test_type_errors/unify010.saw | 10 ++++ intTests/test_type_errors/unify011.log.good | 14 +++++ intTests/test_type_errors/unify011.saw | 12 ++++ intTests/test_type_errors/unify012.log.good | 15 +++++ intTests/test_type_errors/unify012.saw | 14 +++++ src/SAWScript/MGU.hs | 27 ++++++++- 91 files changed, 941 insertions(+), 1 deletion(-) create mode 100644 intTests/test_type_errors/err013.log.good create mode 100644 intTests/test_type_errors/err013.saw create mode 100644 intTests/test_type_errors/err014.log.good create mode 100644 intTests/test_type_errors/err014.saw create mode 100644 intTests/test_type_errors/err015.log.good create mode 100644 intTests/test_type_errors/err015.saw create mode 100644 intTests/test_type_errors/err016.log.good create mode 100644 intTests/test_type_errors/err016.saw create mode 100644 intTests/test_type_errors/err017.log.good create mode 100644 intTests/test_type_errors/err017.saw create mode 100644 intTests/test_type_errors/err018.log.good create mode 100644 intTests/test_type_errors/err018.saw create mode 100644 intTests/test_type_errors/err019.log.good create mode 100644 intTests/test_type_errors/err019.saw create mode 100644 intTests/test_type_errors/err020.log.good create mode 100644 intTests/test_type_errors/err020.saw create mode 100644 intTests/test_type_errors/err021.log.good create mode 100644 intTests/test_type_errors/err021.saw create mode 100644 intTests/test_type_errors/err022.log.good create mode 100644 intTests/test_type_errors/err022.saw create mode 100644 intTests/test_type_errors/err023.log.good create mode 100644 intTests/test_type_errors/err023.saw create mode 100644 intTests/test_type_errors/err024.log.good create mode 100644 intTests/test_type_errors/err024.saw create mode 100644 intTests/test_type_errors/err025.log.good create mode 100644 intTests/test_type_errors/err025.saw create mode 100644 intTests/test_type_errors/err026.log.good create mode 100644 intTests/test_type_errors/err026.saw create mode 100644 intTests/test_type_errors/err027.log.good create mode 100644 intTests/test_type_errors/err027.saw create mode 100644 intTests/test_type_errors/err028.log.good create mode 100644 intTests/test_type_errors/err028.saw create mode 100644 intTests/test_type_errors/err029.log.good create mode 100644 intTests/test_type_errors/err029.saw create mode 100644 intTests/test_type_errors/err030.log.good create mode 100644 intTests/test_type_errors/err030.saw create mode 100644 intTests/test_type_errors/err031.log.good create mode 100644 intTests/test_type_errors/err031.saw create mode 100644 intTests/test_type_errors/err032.log.good create mode 100644 intTests/test_type_errors/err032.saw create mode 100644 intTests/test_type_errors/err033.log.good create mode 100644 intTests/test_type_errors/err033.saw create mode 100644 intTests/test_type_errors/err034.log.good create mode 100644 intTests/test_type_errors/err034.saw create mode 100644 intTests/test_type_errors/err035.log.good create mode 100644 intTests/test_type_errors/err035.saw create mode 100644 intTests/test_type_errors/err036.log.good create mode 100644 intTests/test_type_errors/err036.saw create mode 100644 intTests/test_type_errors/err037.log.good create mode 100644 intTests/test_type_errors/err037.saw create mode 100644 intTests/test_type_errors/err038.log.good create mode 100644 intTests/test_type_errors/err038.saw create mode 100644 intTests/test_type_errors/err039.log.good create mode 100644 intTests/test_type_errors/err039.saw create mode 100644 intTests/test_type_errors/err040.log.good create mode 100644 intTests/test_type_errors/err040.saw create mode 100644 intTests/test_type_errors/err041.log.good create mode 100644 intTests/test_type_errors/err041.saw create mode 100644 intTests/test_type_errors/err042.log.good create mode 100644 intTests/test_type_errors/err042.saw create mode 100644 intTests/test_type_errors/err043.log.good create mode 100644 intTests/test_type_errors/err043.saw create mode 100644 intTests/test_type_errors/err044.log.good create mode 100644 intTests/test_type_errors/err044.saw create mode 100644 intTests/test_type_errors/unify000.log.good create mode 100644 intTests/test_type_errors/unify000.saw create mode 100644 intTests/test_type_errors/unify001.log.good create mode 100644 intTests/test_type_errors/unify001.saw create mode 100644 intTests/test_type_errors/unify002.log.good create mode 100644 intTests/test_type_errors/unify002.saw create mode 100644 intTests/test_type_errors/unify003.log.good create mode 100644 intTests/test_type_errors/unify003.saw create mode 100644 intTests/test_type_errors/unify004.log.good create mode 100644 intTests/test_type_errors/unify004.saw create mode 100644 intTests/test_type_errors/unify005.log.good create mode 100644 intTests/test_type_errors/unify005.saw create mode 100644 intTests/test_type_errors/unify006.log.good create mode 100644 intTests/test_type_errors/unify006.saw create mode 100644 intTests/test_type_errors/unify007.log.good create mode 100644 intTests/test_type_errors/unify007.saw create mode 100644 intTests/test_type_errors/unify008.log.good create mode 100644 intTests/test_type_errors/unify008.saw create mode 100644 intTests/test_type_errors/unify009.log.good create mode 100644 intTests/test_type_errors/unify009.saw create mode 100644 intTests/test_type_errors/unify010.log.good create mode 100644 intTests/test_type_errors/unify010.saw create mode 100644 intTests/test_type_errors/unify011.log.good create mode 100644 intTests/test_type_errors/unify011.saw create mode 100644 intTests/test_type_errors/unify012.log.good create mode 100644 intTests/test_type_errors/unify012.saw 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: 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 "" (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 + 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 "" (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)