diff --git a/src/main.rs b/src/main.rs
index b13312f..c32d67e 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,10 +1,28 @@
-use crate::sgir::Binding;
+use crate::sgir::{Binding, TypeBinding};
 
 mod sgir;
 
 fn main() {
     use sgir::Expression::*;
-    use sgir::Type;
+    use sgir::{Kind, Type};
+
+    let identity = Quantify {
+        parameters: vec![TypeBinding { id: "X".to_owned(), kind: Kind::Star }],
+        body: Box::new(Function {
+            parameters: vec![Binding { id: "x".to_owned(), typ: Type::Variable("X".to_owned()) }],
+            body: Box::new(Variable("x".to_owned())),
+        }),
+    };
+
+    let application = Application {
+        function: Box::new(Instantiate {
+            function: Box::new(identity),
+            arguments: vec![Type::Number]
+        }),
+        arguments: vec![
+            Number(11)
+        ],
+    };
 
     let prog = Application {
         function: Box::new(Function {
@@ -15,18 +33,30 @@ fn main() {
                 Binding { id: "j".to_owned(), typ: Type::Number },
             ],
             body: Box::new(Variable("alex!".to_owned())),
-        }),
+        }), // (number, boolean, number, number) -> number
         arguments: vec![
-            Number(420),
-            Boolean(true),
-            Function {
-                parameters: vec![Binding { id: "x".to_owned(), typ: Type::Number }],
-                body: Box::new(Variable("x".to_owned())),
-            },
-            Number(694208008135),
+            application, // : number
+            Boolean(true), // : boolean
+            Application {
+                function: Box::new(Function {
+                    parameters: vec![Binding { id: "x".to_owned(), typ: Type::Number }],
+                    body: Box::new(Variable("x".to_owned())),
+                }), // : (number) -> number
+                arguments: vec![Number(42)], // : number
+            }, // : number
+            Number(694208008135), // : number
         ]
     };
 
+    let typ = match sgir::check(prog.clone()) {
+        Ok(typ) => typ,
+        Err(type_error) => {
+            eprintln!("[ERROR] {:?}", type_error);
+            return
+        },
+    };
+    println!("TYPE: {:?}", typ);
+
     let result = sgir::run(prog);
     println!("{:?}", result);
 }
diff --git a/src/sgir/mod.rs b/src/sgir/mod.rs
index 039fc17..85f35e1 100644
--- a/src/sgir/mod.rs
+++ b/src/sgir/mod.rs
@@ -1,3 +1,7 @@
+//! This module implements `sgir`, an intermediate representation for sanguinello.
+//!
+//! It is based on System Fω with explicit typing.
+
 use std::collections::HashMap;
 use thiserror::Error;
 
@@ -8,7 +12,10 @@ type Identifier = String;
 
 #[derive(Clone, Debug, PartialEq)]
 pub enum Kind {
+    /// The type of types.
     Star,
+
+    /// A type constructor, or type function.
     Arrow {
         from: Vec<Kind>,
         to: Box<Kind>,
@@ -31,6 +38,7 @@ pub enum Type {
         parameters: Vec<TypeBinding>,
         typ: Box<Type>,
     },
+
     /// type instantiation, e.g. T<U...>
     Instantiate {
         typ: Box<Type>,
@@ -44,20 +52,84 @@ pub enum Type {
         arguments: Vec<Type>,
         result: Box<Type>,
     },
+
     /// a boolean
     Boolean,
+
     /// a number
     Number,
 }
 
+type TypeSubstitution = HashMap<Identifier, Type>;
+
+impl Type {
+    fn apply(self, subst: &TypeSubstitution) -> Type {
+        match self {
+            Type::Variable(id) => match subst.get(&id) {
+                Some(replacement) => replacement.clone(),
+                None => Type::Variable(id),
+            },
+
+            Type::ForAll { parameters, typ } => {
+                // to handle shadowing properly, we have to remove any occurrences
+                // of any of the `parameters` found in the substitution.
+                let mut extended_subst = subst.clone();
+                for TypeBinding { id, .. } in parameters.iter() {
+                    extended_subst.remove(id);
+                }
+
+                Type::ForAll {
+                    parameters,
+                    typ: Box::new(typ.apply(&extended_subst)),
+                }
+            },
+
+            Type::Instantiate { typ, arguments } => Type::Instantiate {
+                typ: Box::new(typ.apply(&subst)),
+                arguments: arguments.into_iter().map(|typ| typ.apply(&subst)).collect(),
+            },
+
+            Type::Function { arguments, result } => Type::Function {
+                arguments: arguments.into_iter().map(|typ| typ.apply(&subst)).collect(),
+                result: Box::new(result.apply(&subst)),
+            },
+
+            Type::Boolean => Type::Boolean,
+            Type::Number => Type::Number,
+        }
+    }
+}
+
 #[derive(Debug, Error, Clone, PartialEq)]
-enum TypeError {
+pub enum TypeError {
     #[error("kind mismatch: expected {expected:?}, found {found:?}")]
     KindMismatch {
         expected: Kind,
         found: Kind,
     },
 
+    #[error("type mismatch: expected {expected:?}, found {found:?}")]
+    TypeMismatch {
+        expected: Type,
+        found: Type,
+    },
+
+    #[error("arity mismatch: expected {expected} arguments, found {found}")]
+    ArityMismatch {
+        expected: usize,
+        found: usize,
+    },
+
+    #[error("cannot call a non-function: {found:?}")]
+    CannotCallNonFunction {
+        found: Type,
+    },
+
+    #[error("cannot instantiate a non-quantification: {found:?}")]
+    CannotCallNonQuantification {
+        found: Type,
+    },
+
     #[error("kind mismatch: expected a quantifier in type {found:?}")]
     ExpectedQuantifier {
         found: Type,
@@ -67,7 +139,7 @@ enum TypeError {
     UnboundIdentifier(Identifier),
 }
 
-type TC<T> = Result<T, TypeError>;
+pub type TC<T> = Result<T, TypeError>;
 
 type KindEnv = HashMap<Identifier, Kind>;
 
@@ -122,6 +194,18 @@ pub enum Expression {
     Boolean(bool),
     Number(i64), // haha, this should be a bignum
 
+    /// type quantification (i.e. \Lambda)
+    Quantify {
+        parameters: Vec<TypeBinding>,
+        body: Box<Expression>,
+    },
+
+    /// type instantiation (i.e. application of a \Lambda)
+    Instantiate {
+        function: Box<Expression>,
+        arguments: Vec<Type>,
+    },
+
     Function {
         parameters: Vec<Binding>,
         body: Box<Expression>,
@@ -133,6 +217,116 @@ pub enum Expression {
     },
 }
 
+type TypeEnv = HashMap<Identifier, Type>;
+
+fn check_type(tenv: &TypeEnv, kenv: &KindEnv, expr: Expression) -> TC<Type> {
+    match expr {
+        Expression::Variable(id) =>  match tenv.get(&id) {
+            Some(ty) => Ok(ty.clone()),
+            None => Err(TypeError::UnboundIdentifier(id.clone())),
+        },
+
+        Expression::Boolean(_) => Ok(Type::Boolean),
+
+        Expression::Number(_) => Ok(Type::Number),
+
+        Expression::Quantify { parameters, body } => {
+            let mut extended_kenv = kenv.clone();
+            extended_kenv.extend(parameters.clone().into_iter()
+                                 .map(|TypeBinding { id, kind }| (id, kind)));
+
+            let typ = check_type(tenv, &extended_kenv, *body)?;
+            match check_kinds(kenv, typ.clone())? {
+                // the resulting type is a type...
+                Kind::Star => Ok(Type::ForAll { parameters , typ: Box::new(typ) }),
+
+                // the resulting type is a type function...
+                kind => Err(TypeError::KindMismatch { expected: Kind::Star, found: kind }),
+            }
+        }
+
+        Expression::Instantiate { function, arguments } => {
+            match check_type(tenv, kenv, *function)? {
+                Type::ForAll { parameters, typ } => {
+                    if arguments.len() != parameters.len() {
+                        return Err(TypeError::ArityMismatch { expected: parameters.len(), found: arguments.len() })
+                    }
+
+                    let argument_kind_pairs = arguments.clone().into_iter()
+                                                       .zip(parameters.iter().map(|TypeBinding { kind, .. }| kind.clone()));
+
+                    for (argument, expected_kind) in argument_kind_pairs {
+                        let computed_kind = check_kinds(kenv, argument)?;
+
+                        if computed_kind != expected_kind {
+                            return Err(TypeError::KindMismatch { expected: expected_kind, found: computed_kind })
+                        }
+                    }
+
+                    // we have to substitute the types in `arguments` for the type parameters in `parameters`
+                    let subst: TypeSubstitution = parameters.into_iter()
+                                                            .map(|TypeBinding { id, .. }| id)
+                                                            .zip(arguments)
+                                                            .collect();
+
+                    Ok(typ.apply(&subst))
+                },
+
+                // Unexpected type here, it must be a forall!
+                found => Err(TypeError::CannotCallNonQuantification { found })
+            }
+        }
+
+        Expression::Function { parameters, body } => {
+            for Binding { typ, .. } in parameters.iter() {
+                if let kind@Kind::Arrow { .. } = check_kinds(kenv, typ.clone())? {
+                    return Err(TypeError::KindMismatch { expected: Kind::Star, found: kind })
+                }
+            }
+
+            let arguments = parameters.iter()
+                                      .map(|Binding { typ, .. }| typ.clone())
+                                      .collect();
+
+            let mut extended_tenv = tenv.clone();
+            extended_tenv.extend(parameters.into_iter()
+                                 .map(|Binding { id, typ }| (id, typ)));
+            let result = Box::new(check_type(&extended_tenv, &kenv, *body)?);
+
+            Ok(Type::Function { arguments, result })
+        },
+
+        Expression::Application { function, arguments } => {
+            match check_type(tenv, kenv, *function)? {
+                Type::Function { arguments: expected_types, result: result_type } => {
+                    if arguments.len() != expected_types.len() {
+                        return Err(TypeError::ArityMismatch { expected: expected_types.len(), found: arguments.len() })
+                    }
+
+                    for (argument, expected_type) in arguments.into_iter().zip(expected_types) {
+                        let computed_type = check_type(tenv, kenv, argument)?;
+
+                        if computed_type != expected_type {
+                            return Err(TypeError::TypeMismatch { expected: expected_type, found: computed_type })
+                        }
+                    }
+
+                    Ok(*result_type)
+                },
+
+                // Unexpected type here, it must be a function!
+                found => Err(TypeError::CannotCallNonFunction { found })
+            }
+        },
+    }
+}
+
+pub fn check(expr: Expression) -> TC<Type> {
+    let type_env = HashMap::new();
+    let kind_env = HashMap::new();
+    check_type(&type_env, &kind_env, expr)
+}
+
 #[derive(Clone, Debug)]
 pub enum Value {
     // Primitives
@@ -152,6 +346,10 @@ fn eval(subst: &Substitution, expr: Expression) -> Value {
         Expression::Variable(identifier) => subst[&identifier].clone(),
         Expression::Boolean(value) => Value::Boolean(value),
         Expression::Number(value) => Value::Number(value),
+        // quantification has no runtime semantics
+        Expression::Quantify { body, .. } => eval(subst, *body),
+        // instantiation has no runtime semantics
+        Expression::Instantiate { function, .. } => eval(subst, *function),
         Expression::Function { parameters, body } => Value::Function { parameters: parameters.clone(), body: body.clone() },
         Expression::Application { function, arguments } => match eval(subst, *function) {
             Value::Function { parameters, body } => {
diff --git a/src/sgir/tests.rs b/src/sgir/tests.rs
index 7dc76be..c0b54b4 100644
--- a/src/sgir/tests.rs
+++ b/src/sgir/tests.rs
@@ -9,19 +9,29 @@ fn test_kind_checking_trivial() {
 
 #[test]
 fn test_kind_checking_polymorphic_identity_function() {
-    let typ = Type::ForAll { parameters: vec![TypeBinding { id: "a".to_owned(), kind: Kind::Star }],
-                             typ: Box::new(Type::Function { arguments: vec![Type::Variable("a".to_owned())],
-                                                            result: Box::new(Type::Variable("a".to_owned())) }) };
+    let typ = Type::ForAll {
+        parameters: vec![TypeBinding { id: "a".to_owned(), kind: Kind::Star }],
+        typ: Box::new(Type::Function {
+            arguments: vec![Type::Variable("a".to_owned())],
+            result: Box::new(Type::Variable("a".to_owned()))
+        })
+    };
     let kind = check_kinds(&HashMap::new(), typ);
     assert_eq!(kind, Ok(Kind::Arrow { from: vec![Kind::Star], to: Box::new(Kind::Star) }));
 }
 
 #[test]
 fn test_kind_checking_instantiated_polymorphic_identity_function() {
-    let typ = Type::Instantiate { typ: Box::new(Type::ForAll { parameters: vec![TypeBinding { id: "a".to_owned(), kind: Kind::Star }],
-                                                               typ: Box::new(Type::Function { arguments: vec![Type::Variable("a".to_owned())],
-                                                                                              result: Box::new(Type::Variable("a".to_owned())) }) }),
-                                  arguments: vec![Type::Number] };
+    let typ = Type::Instantiate {
+        typ: Box::new(Type::ForAll {
+            parameters: vec![TypeBinding { id: "a".to_owned(), kind: Kind::Star }],
+            typ: Box::new(Type::Function {
+                arguments: vec![Type::Variable("a".to_owned())],
+                result: Box::new(Type::Variable("a".to_owned()))
+            })
+        }),
+        arguments: vec![Type::Number]
+    };
     let kind = check_kinds(&HashMap::new(), typ);
     assert_eq!(kind, Ok(Kind::Star));
 }
@@ -45,11 +55,184 @@ fn test_kind_checking_instantiated_monomorphic_type() {
 
 #[test]
 fn test_kind_checking_instantiated_polymorphic_function_with_type_constructor() {
-    let typ = Type::Instantiate { typ: Box::new(Type::ForAll { parameters: vec![TypeBinding { id: "a".to_owned(), kind: Kind::Star }],
-                                                               typ: Box::new(Type::Function { arguments: vec![Type::Variable("a".to_owned())],
-                                                                                              result: Box::new(Type::Variable("a".to_owned())) }) }),
-                                  arguments: vec![Type::ForAll { parameters: vec![TypeBinding { id: "b".to_owned(), kind: Kind::Star }],
-                                                                 typ: Box::new(Type::Variable("b".to_owned())) }] };
+    let typ = Type::Instantiate {
+        typ: Box::new(Type::ForAll {
+            parameters: vec![TypeBinding { id: "a".to_owned(), kind: Kind::Star }],
+            typ: Box::new(Type::Function {
+                arguments: vec![Type::Variable("a".to_owned())],
+                result: Box::new(Type::Variable("a".to_owned()))
+            })
+        }),
+        arguments: vec![Type::ForAll {
+            parameters: vec![TypeBinding { id: "b".to_owned(), kind: Kind::Star }],
+            typ: Box::new(Type::Variable("b".to_owned()))
+        }]
+    };
     let kind = check_kinds(&HashMap::new(), typ);
     assert_eq!(kind, Err(TypeError::KindMismatch { expected: Kind::Star, found: Kind::Arrow { from: vec![Kind::Star], to: Box::new(Kind::Star) }}));
 }
+
+#[test]
+fn test_type_check_basic_number() {
+    let expr = Expression::Number(42);
+
+    let typ = check(expr);
+    assert_eq!(typ, Ok(Type::Number));
+}
+
+#[test]
+fn test_type_check_basic_boolean() {
+    let expr = Expression::Boolean(true);
+
+    let typ = check(expr);
+    assert_eq!(typ, Ok(Type::Boolean));
+}
+
+#[test]
+fn test_type_check_identity_function() {
+    let expr = Expression::Function {
+        parameters: vec![Binding { id: "x".to_owned(), typ: Type::Number }],
+        body: Box::new(Expression::Variable("x".to_owned())),
+    };
+
+    let typ = check(expr);
+    assert_eq!(typ, Ok(Type::Function { arguments: vec![Type::Number], result: Box::new(Type::Number) }));
+}
+
+#[test]
+fn test_type_check_apply_identity_function() {
+    let identity = Expression::Function {
+        parameters: vec![Binding { id: "x".to_owned(), typ: Type::Number }],
+        body: Box::new(Expression::Variable("x".to_owned())),
+    };
+
+    let expr = Expression::Application {
+        function: Box::new(identity),
+        arguments: vec![
+            Expression::Number(42),
+        ],
+    };
+
+    let typ = check(expr);
+    assert_eq!(typ, Ok(Type::Number));
+}
+
+#[test]
+fn test_type_check_apply_identity_function_mismatch() {
+    let identity = Expression::Function {
+        parameters: vec![Binding { id: "x".to_owned(), typ: Type::Number }],
+        body: Box::new(Expression::Variable("x".to_owned())),
+    };
+
+    let expr = Expression::Application {
+        function: Box::new(identity),
+        arguments: vec![
+            Expression::Boolean(false),
+        ],
+    };
+
+    let typ = check(expr);
+    assert_eq!(typ, Err(TypeError::TypeMismatch { expected: Type::Number, found: Type::Boolean }));
+}
+
+#[test]
+fn test_type_checking_polymorphic_identity_function() {
+    let identity = Expression::Quantify {
+        parameters: vec![TypeBinding { id: "X".to_owned(), kind: Kind::Star }],
+        body: Box::new(Expression::Function {
+            parameters: vec![Binding { id: "x".to_owned(), typ: Type::Variable("X".to_owned()) }],
+            body: Box::new(Expression::Variable("x".to_owned())),
+        }),
+    };
+
+    let expected_type = Type::ForAll {
+        parameters: vec![TypeBinding { id: "X".to_owned(), kind: Kind::Star }],
+        typ: Box::new(Type::Function {
+            arguments: vec![Type::Variable("X".to_owned())],
+            result: Box::new(Type::Variable("X".to_owned())),
+        }),
+    };
+
+    let typ = check(identity);
+    assert_eq!(typ, Ok(expected_type));
+}
+
+#[test]
+fn test_type_checking_instantiated_polymorphic_identity_function() {
+    let identity = Expression::Quantify {
+        parameters: vec![TypeBinding { id: "X".to_owned(), kind: Kind::Star }],
+        body: Box::new(Expression::Function {
+            parameters: vec![Binding { id: "x".to_owned(), typ: Type::Variable("X".to_owned()) }],
+            body: Box::new(Expression::Variable("x".to_owned())),
+        }),
+    };
+
+    let expr = Expression::Instantiate { function: Box::new(identity), arguments: vec![Type::Number] };
+
+    let expected_type = Type::Function {
+        arguments: vec![Type::Number],
+        result: Box::new(Type::Number),
+    };
+
+    let typ = check(expr);
+    assert_eq!(typ, Ok(expected_type));
+}
+
+#[test]
+fn test_type_checking_instantiated_applied_polymorphic_identity_function() {
+    let identity = Expression::Quantify {
+        parameters: vec![TypeBinding { id: "X".to_owned(), kind: Kind::Star }],
+        body: Box::new(Expression::Function {
+            parameters: vec![Binding { id: "x".to_owned(), typ: Type::Variable("X".to_owned()) }],
+            body: Box::new(Expression::Variable("x".to_owned())),
+        }),
+    };
+
+    let expr = Expression::Application {
+        function: Box::new(Expression::Instantiate {
+            function: Box::new(identity),
+            arguments: vec![Type::Number]
+        }),
+        arguments: vec![
+            Expression::Number(11)
+        ],
+    };
+
+    let expected_type = Type::Number;
+
+    let typ = check(expr);
+    assert_eq!(typ, Ok(expected_type));
+}
+
+#[test]
+fn test_type_checking_and_running_instantiated_applied_polymorphic_identity_function() {
+    let identity = Expression::Quantify {
+        parameters: vec![TypeBinding { id: "X".to_owned(), kind: Kind::Star }],
+        body: Box::new(Expression::Function {
+            parameters: vec![Binding { id: "x".to_owned(), typ: Type::Variable("X".to_owned()) }],
+            body: Box::new(Expression::Variable("x".to_owned())),
+        }),
+    };
+
+    let expr = Expression::Application {
+        function: Box::new(Expression::Instantiate {
+            function: Box::new(identity),
+            arguments: vec![Type::Number]
+        }),
+        arguments: vec![
+            Expression::Number(11)
+        ],
+    };
+
+    let expected_type = Type::Number;
+
+    let typ = check(expr.clone());
+    assert_eq!(typ, Ok(expected_type));
+
+    match run(expr) {
+        Value::Number(n) => assert_eq!(n, 11),
+        value => {
+            assert!(false, "{:?} is not a number!", value);
+        }
+    }
+}