summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs1
-rw-r--r--dhall/src/tests.rs3
2 files changed, 4 insertions, 0 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 9a1d0d8..11c07d8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -680,6 +680,7 @@ pub(crate) fn type_with(
val.clone()
};
let val = type_with(env, &val)?;
+ val.get_type()?; // Ensure val is not Sort
let val_nf = val.eval(&env.as_nzenv());
let body_env = env.insert_value(&binder, val_nf);
let body = type_with(&body_env, body)?;
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 8216243..8136625 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -179,6 +179,9 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
let file_path = PathBuf::from(file_path);
let error_file_path = file_path
.strip_prefix("../dhall-lang/tests/type-inference/failure/")
+ .or_else(|_| {
+ file_path.strip_prefix("tests/type-inference/failure/")
+ })
.unwrap();
let error_file_path =
PathBuf::from("tests/type-errors/").join(error_file_path);