Merge pull request #2182 from GaloisInc/type-messages-tests

Add more typechecker tests

Author: sauclovian-g

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.

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

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;

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

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;

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

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);

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

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;

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

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;
+

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

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;
+

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

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;

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

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;

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

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;

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

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;

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

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;

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

intTests/test_type_errors/err024.saw

@@ -0,0 +1,3 @@
+// Trigger the "Unbound variable" message
+
+let x = y;

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

intTests/test_type_errors/err025.saw

@@ -0,0 +1,3 @@
+// Trigger the "do block must include at least one expression" message
+
+let x = do {};

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

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 }};
+};

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

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 : [] = [];
+
+

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