summaryrefslogtreecommitdiff
path: root/dhall/tests/type-inference
diff options
context:
space:
mode:
authorNadrieril Feneanar2020-03-05 16:20:07 +0000
committerGitHub2020-03-05 16:20:07 +0000
commit3f9194f47185fe30c9e410aa7c5e651df9694b3f (patch)
tree6d24b2e824822134da4976b65b413dc09ca4e567 /dhall/tests/type-inference
parent2ca97e97f1718141d826a78ab3da8197b2d55c69 (diff)
parent8e6b020ba1426c215382a81395b809b688fa7726 (diff)
Merge pull request #139 from Nadrieril/missing-features
Implement a bunch of missing features
Diffstat (limited to 'dhall/tests/type-inference')
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt7
-rw-r--r--dhall/tests/type-inference/failure/unit/LetInSort.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/LetInSort.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/MergeBool.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/MergeBool.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall1
-rw-r--r--dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt6
-rw-r--r--dhall/tests/type-inference/success/CacheImportsA.dhall6
-rw-r--r--dhall/tests/type-inference/success/CacheImportsB.dhall1
-rw-r--r--dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall5
-rw-r--r--dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/TodoA.dhall1
-rw-r--r--dhall/tests/type-inference/success/regression/TodoB.dhall1
22 files changed, 57 insertions, 0 deletions
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall
new file mode 100644
index 0000000..94b32f9
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.dhall
@@ -0,0 +1 @@
+Bool -> 1
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt
new file mode 100644
index 0000000..bcc44a5
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeOutputTypeNotAType.txt
@@ -0,0 +1,7 @@
+Type error: error: Expected a type, found: `1`
+ --> <current file>:1:8
+ |
+1 | Bool -> 1
+ | ^ this has type: `Natural`
+ |
+ = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/LetInSort.dhall b/dhall/tests/type-inference/failure/unit/LetInSort.dhall
new file mode 100644
index 0000000..125ab28
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/LetInSort.dhall
@@ -0,0 +1 @@
+\(x: let x = 0 in Sort) -> 1
diff --git a/dhall/tests/type-inference/failure/unit/LetInSort.txt b/dhall/tests/type-inference/failure/unit/LetInSort.txt
new file mode 100644
index 0000000..07be298
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/LetInSort.txt
@@ -0,0 +1,6 @@
+Type error: error: Sort does not have a type
+ --> <current file>:1:18
+ |
+1 | \(x: let x = 0 in Sort) -> 1
+ | ^^^^ Sort does not have a type
+ |
diff --git a/dhall/tests/type-inference/failure/unit/MergeBool.dhall b/dhall/tests/type-inference/failure/unit/MergeBool.dhall
new file mode 100644
index 0000000..01e7e3f
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeBool.dhall
@@ -0,0 +1 @@
+\(x: { True: Natural, False: Natural }) -> merge x True
diff --git a/dhall/tests/type-inference/failure/unit/MergeBool.txt b/dhall/tests/type-inference/failure/unit/MergeBool.txt
new file mode 100644
index 0000000..209def1
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/MergeBool.txt
@@ -0,0 +1,6 @@
+Type error: error: Merge2ArgMustBeUnionOrOptional
+ --> <current file>:1:43
+ |
+1 | \(x: { True: Natural, False: Natural }) -> merge x True
+ | ^^^^^^^^^^^^ Merge2ArgMustBeUnionOrOptional
+ |
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall
new file mode 100644
index 0000000..7e5c8ec
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.dhall
@@ -0,0 +1 @@
+(0 : Bool) : Natural
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt
new file mode 100644
index 0000000..b56db54
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotInnerWrong.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: Natural != Bool
+ --> <current file>:1:1
+ |
+1 | (0 : Bool) : Natural
+ | ^ annot mismatch: Natural != Bool
+ |
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall
new file mode 100644
index 0000000..67a1526
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.dhall
@@ -0,0 +1 @@
+(0 : Natural) : Bool
diff --git a/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt
new file mode 100644
index 0000000..2f07b8d
--- /dev/null
+++ b/dhall/tests/type-inference/failure/unit/NestedAnnotOuterWrong.txt
@@ -0,0 +1,6 @@
+Type error: error: annot mismatch: Natural != Bool
+ --> <current file>:1:1
+ |
+1 | (0 : Natural) : Bool
+ | ^^^^^^^^^^^ annot mismatch: Natural != Bool
+ |
diff --git a/dhall/tests/type-inference/success/CacheImportsA.dhall b/dhall/tests/type-inference/success/CacheImportsA.dhall
new file mode 100644
index 0000000..7180b19
--- /dev/null
+++ b/dhall/tests/type-inference/success/CacheImportsA.dhall
@@ -0,0 +1,6 @@
+{-
+ This URL returns (probably) a different result for each request. This test
+ ensures that import results for a given URL are correctly cached within an
+ execution of dhall.
+-}
+let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text in 0
diff --git a/dhall/tests/type-inference/success/CacheImportsB.dhall b/dhall/tests/type-inference/success/CacheImportsB.dhall
new file mode 100644
index 0000000..2f184a4
--- /dev/null
+++ b/dhall/tests/type-inference/success/CacheImportsB.dhall
@@ -0,0 +1 @@
+Natural
diff --git a/dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall b/dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall
new file mode 100644
index 0000000..e7f4dcd
--- /dev/null
+++ b/dhall/tests/type-inference/success/CacheImportsCanonicalizeA.dhall
@@ -0,0 +1,5 @@
+{-
+ This URL returns (probably) a different result for each request. This test
+ ensures that import locations are canonicalized before being cached.
+-}
+let _ = assert : https://csrng.net/csrng/csrng.php?min=0&max=1000 as Text === https://csrng.net/csrng/../csrng/csrng.php?min=0&max=1000 as Text in 0
diff --git a/dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall b/dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall
new file mode 100644
index 0000000..2f184a4
--- /dev/null
+++ b/dhall/tests/type-inference/success/CacheImportsCanonicalizeB.dhall
@@ -0,0 +1 @@
+Natural
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall
new file mode 100644
index 0000000..72f866f
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1A.dhall
@@ -0,0 +1 @@
+let T = 0 in λ(T : Type) → λ(x : T) → 1
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall
new file mode 100644
index 0000000..42bfeec
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping1B.dhall
@@ -0,0 +1 @@
+∀(T : Type) → ∀(x : T) → Natural
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall
new file mode 100644
index 0000000..30fd03c
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2A.dhall
@@ -0,0 +1 @@
+(λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
diff --git a/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall
new file mode 100644
index 0000000..20aa0d3
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/LambdaInLetScoping2B.dhall
@@ -0,0 +1 @@
+∀(T : Type) → ∀(x : T) → T
diff --git a/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall
new file mode 100644
index 0000000..c7b7fb4
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionA.dhall
@@ -0,0 +1 @@
+{ x : { a : Bool } } ⩓ { x : { b : Bool } } ⩓ { x : { c : Bool } }
diff --git a/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall
new file mode 100644
index 0000000..245bc9d
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/RecursiveRecordTypeMergeTripleCollisionB.dhall
@@ -0,0 +1 @@
+Type
diff --git a/dhall/tests/type-inference/success/regression/TodoA.dhall b/dhall/tests/type-inference/success/regression/TodoA.dhall
new file mode 100644
index 0000000..9d5ef34
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/TodoA.dhall
@@ -0,0 +1 @@
+λ(todo : ∀(a : Type) → a) → todo
diff --git a/dhall/tests/type-inference/success/regression/TodoB.dhall b/dhall/tests/type-inference/success/regression/TodoB.dhall
new file mode 100644
index 0000000..e0091f2
--- /dev/null
+++ b/dhall/tests/type-inference/success/regression/TodoB.dhall
@@ -0,0 +1 @@
+∀(todo : ∀(a : Type) → a) → ∀(a : Type) → a