From c00f5569d8feaad09ed7181100a4bfc744e27470 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sun, 12 Feb 2023 22:35:20 +0100
Subject: [PATCH] include all Infer errors in the testsuite
---
client/test/suite.t/error-cycle.midml | 1 +
client/test/suite.t/error-unbound.midml | 1 +
client/test/suite.t/error-unify-app-arg.midml | 2 +
client/test/suite.t/error-unify-app-fun.midml | 2 +
client/test/suite.t/error-unify-letprod.midml | 2 +
.../suite.t/error-variable-scope-escape.midml | 2 +
client/test/suite.t/run.t | 82 +++++++++++++++++--
7 files changed, 87 insertions(+), 5 deletions(-)
create mode 100644 client/test/suite.t/error-cycle.midml
create mode 100644 client/test/suite.t/error-unbound.midml
create mode 100644 client/test/suite.t/error-unify-app-arg.midml
create mode 100644 client/test/suite.t/error-unify-app-fun.midml
create mode 100644 client/test/suite.t/error-unify-letprod.midml
create mode 100644 client/test/suite.t/error-variable-scope-escape.midml
diff --git a/client/test/suite.t/error-cycle.midml b/client/test/suite.t/error-cycle.midml
new file mode 100644
index 0000000..c3f189f
--- /dev/null
+++ b/client/test/suite.t/error-cycle.midml
@@ -0,0 +1 @@
+let self_app = fun x -> x x
diff --git a/client/test/suite.t/error-unbound.midml b/client/test/suite.t/error-unbound.midml
new file mode 100644
index 0000000..1d840c8
--- /dev/null
+++ b/client/test/suite.t/error-unbound.midml
@@ -0,0 +1 @@
+let x = (fun y -> z)
diff --git a/client/test/suite.t/error-unify-app-arg.midml b/client/test/suite.t/error-unify-app-arg.midml
new file mode 100644
index 0000000..f6c72f5
--- /dev/null
+++ b/client/test/suite.t/error-unify-app-arg.midml
@@ -0,0 +1,2 @@
+let x =
+ (fun y z -> y z) ()
diff --git a/client/test/suite.t/error-unify-app-fun.midml b/client/test/suite.t/error-unify-app-fun.midml
new file mode 100644
index 0000000..495dd5c
--- /dev/null
+++ b/client/test/suite.t/error-unify-app-fun.midml
@@ -0,0 +1,2 @@
+let app_error = fun x ->
+ (x, x) (fun y -> y)
diff --git a/client/test/suite.t/error-unify-letprod.midml b/client/test/suite.t/error-unify-letprod.midml
new file mode 100644
index 0000000..64ae2f0
--- /dev/null
+++ b/client/test/suite.t/error-unify-letprod.midml
@@ -0,0 +1,2 @@
+let letprod_error =
+ let (x, y) = (fun z -> z) in x
diff --git a/client/test/suite.t/error-variable-scope-escape.midml b/client/test/suite.t/error-variable-scope-escape.midml
new file mode 100644
index 0000000..5c4ec49
--- /dev/null
+++ b/client/test/suite.t/error-variable-scope-escape.midml
@@ -0,0 +1,2 @@
+let rigid_escape = fun f ->
+ (fun x -> f x : for 'a . 'a -> 'a)
diff --git a/client/test/suite.t/run.t b/client/test/suite.t/run.t
index 5ba32dc..8b8ef78 100644
--- a/client/test/suite.t/run.t
+++ b/client/test/suite.t/run.t
@@ -1,4 +1,4 @@
-Basics
+# Basics
$ cat id.midml
let id =
@@ -63,7 +63,79 @@ Basics
File "test", line 2, characters 10-10:
Syntax error.
-Option type
+# Errors
+
+Unbound variables.
+
+ $ cat error-unbound.midml
+ let x = (fun y -> z)
+
+ $ midml error-unbound.midml
+ Type inference and translation to System F...
+ File "test", line 1, characters 18-19:
+ Type error: unbound variable "z".
+
+Some unification errors (not exhaustive!)
+
+ $ cat error-unify-letprod.midml
+ let letprod_error =
+ let (x, y) = (fun z -> z) in x
+
+ $ midml error-unify-letprod.midml
+ Type inference and translation to System F...
+ File "test", line 2, characters 16-26:
+ Type error: mismatch between the type:
+ {r2*r4}
+ and the type:
+ r8 -> r10
+
+ $ cat error-unify-app-fun.midml
+ let app_error = fun x ->
+ (x, x) (fun y -> y)
+
+ $ midml error-unify-app-fun.midml
+ Type inference and translation to System F...
+ File "test", line 2, characters 2-8:
+ Type error: mismatch between the type:
+ r8 -> r4
+ and the type:
+ {r12*r14}
+
+ $ cat error-unify-app-arg.midml
+ let x =
+ (fun y z -> y z) ()
+
+ $ midml error-unify-app-arg.midml
+ Type inference and translation to System F...
+ File "test", line 2, characters 19-21:
+ Type error: mismatch between the type:
+ r12 -> r14
+ and the type:
+ {}
+
+Cycles
+
+ $ cat error-cycle.midml
+ let self_app = fun x -> x x
+
+ $ midml error-cycle.midml
+ Type inference and translation to System F...
+ File "test", line 1, characters 15-27:
+ Type error: a cyclic type arose.
+ mu a0. a0 -> r4
+
+Variable scope escape
+
+ $ cat error-variable-scope-escape.midml
+ let rigid_escape = fun f ->
+ (fun x -> f x : for 'a . 'a -> 'a)
+
+ $ midml error-variable-scope-escape.midml
+ Type inference and translation to System F...
+ File "test", line 2, characters 2-36:
+ A rigid variable escapes its scope.
+
+# Option type
$ cat none.midml
#use option.midml
@@ -108,7 +180,7 @@ Option type
Converting the System F term to de Bruijn style...
Type-checking the System F term...
-List type
+# List type
$ cat nil.midml
#use list.midml
@@ -178,7 +250,7 @@ List type
Converting the System F term to de Bruijn style...
Type-checking the System F term...
-Annotations
+# Annotations
$ cat nat-annot.midml
type nat = | Zero | Succ of nat
@@ -192,7 +264,7 @@ Annotations
Converting the System F term to de Bruijn style...
Type-checking the System F term...
-Pattern-matching
+# Pattern-matching
$ cat match-tuple.midml
let _ =
--
GitLab