From 47c5941497831ba49aed1c054eaacf9878c77d9b Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Tue, 1 Nov 2022 15:07:56 +0100
Subject: [PATCH] Fix : century-old bug in the type-checker
---
kernel/src/term.rs | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/kernel/src/term.rs b/kernel/src/term.rs
index bba9d852..f12f1ad4 100644
--- a/kernel/src/term.rs
+++ b/kernel/src/term.rs
@@ -130,6 +130,7 @@ mod tests {
// /!\ most of these tests are on ill-typed terms and should not be used for further testings
use super::Term::*;
use crate::term::Environment;
+ use crate::universe::UniverseLevel;
#[test]
fn simple_subst() {
@@ -334,4 +335,17 @@ mod tests {
assert_eq!(Const("foo".into()).beta_reduction(&env), id_prop);
}
+
+
+ #[test]
+ fn poly_univ_id(){
+ let id_ty = Prod(box Type(UniverseLevel::Var(0)),box Prod(box Var(1.into()),box Var(2.into())));
+ let id_te = Abs(box Type(UniverseLevel::Var(0)),box Abs(box Var(1.into()),box Var(1.into())));
+ let id_zero = Abs(box Type(0.into()),box Abs(box Var(1.into()),box Var(1.into())));
+ assert!(id_te.check(&id_ty, &Environment::new()).is_ok());
+ let env = Environment::new()
+ .insert("id".into(), id_te.clone().into(), id_ty.clone())
+ .unwrap();
+ assert!(Const("id".into(),vec![0.into()]).is_def_eq(&id_zero, &env).is_ok())
+ }
}
--
GitLab