diff --git a/kernel/src/type_checker.rs b/kernel/src/type_checker.rs
index ac495e1355c3ebc4a22d90724460ce2d597bfec8..eb9737ba8a6c898768499973d226b77b4eb23820 100644
--- a/kernel/src/type_checker.rs
+++ b/kernel/src/type_checker.rs
@@ -177,6 +177,10 @@ impl<'arena> Declaration<'arena> {
         self.0.infer(arena)?;
         Ok(())
     }
+
+    pub fn check(self, ty: Self, arena: &mut Arena<'arena>) -> Result<'arena, ()> {
+        self.0.check(ty.0, arena)
+    }
 }
 
 #[cfg(test)]
diff --git a/parser/src/parser.rs b/parser/src/parser.rs
index af63350c17af09fd6a2ccf9d495312a91e3d2928..12186bcd2d3679d96f4296012043c1d4de31c68c 100644
--- a/parser/src/parser.rs
+++ b/parser/src/parser.rs
@@ -176,7 +176,7 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
             let mut iter = pair.into_inner();
             let mut string_decl = iter.next().unwrap().into_inner();
             let s = string_decl.next().unwrap().as_str();
-            let vars = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+            let vars : Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
             let body = iter.next().map(parse_term).unwrap();
 
             Command::Declaration(s, None, declaration::Builder::Decl(box body, vars))
@@ -184,8 +184,10 @@ fn parse_expr(pair: Pair<Rule>) -> Command {
 
         Rule::DeclarationCheckType => {
             let mut iter = pair.into_inner();
-            let s = iter.next().unwrap().as_str();
-            let vars: Vec<&str> = iter.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+            let mut string_decl = iter.next().unwrap().into_inner();
+            let s = string_decl.next().unwrap().as_str();
+            let vars : Vec<&str> = string_decl.next().unwrap().into_inner().map(|name| name.as_str()).collect();
+            
             let t = parse_term(iter.next().unwrap());
             let body = iter.next().map(parse_term).unwrap();
 
diff --git a/proost/src/evaluator.rs b/proost/src/evaluator.rs
index 407b3bf3fc5c1c0e990fe95aef34426396279f62..a5e49ffeccf4111e2cc193d4e5caa18ae15ef378 100644
--- a/proost/src/evaluator.rs
+++ b/proost/src/evaluator.rs
@@ -6,7 +6,6 @@ use colored::Colorize;
 use derive_more::Display;
 use kernel::location::Location;
 use kernel::memory::arena::Arena;
-use kernel::memory::declaration::InstantiatedDeclaration;
 use kernel::memory::term::Term;
 use parser::command::Command;
 use parser::{parse_file, parse_line};
@@ -185,12 +184,9 @@ impl<'arena> Evaluator {
 
             Command::Declaration(s, Some(t), decl) => {
                 let decl = decl.realise(arena)?;
-                let t = t.realise(arena)?;
+                let ty = t.realise(arena)?;
                 if arena.get_binding(s).is_none() {
-                    decl.infer(arena)?;
-                    InstantiatedDeclaration::instantiate_with_self(decl, arena)
-                        .get_term(arena)
-                        .check(InstantiatedDeclaration::instantiate_with_self(t, arena).get_term(arena), arena)?;
+                    decl.check(ty,arena)?;
                     arena.bind_decl(s, decl);
                     Ok(None)
                 } else {