Merge pull request #204 from Nadrieril/source-id

21 files changed, 1038 insertions, 581 deletions

diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index 1b4f9a3..1e9cfbc 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -21,6 +21,7 @@ path = "tests/spec.rs"
 
 [dependencies]
 annotate-snippets = "0.9.0"
+elsa = "1.3.2"
 hex = "0.4.2"
 itertools = "0.9.0"
 lazy_static = "1.4.0"
diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs
index cc426dd..123e03d 100644
--- a/dhall/src/builtins.rs
+++ b/dhall/src/builtins.rs
@@ -2,15 +2,13 @@ use std::collections::{BTreeMap, HashMap};
 use std::convert::TryInto;
 
 use crate::operations::{BinOp, OpKind};
-use crate::semantics::{
-    nze, skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv,
-    VarEnv,
-};
+use crate::semantics::{nze, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv};
 use crate::syntax::Const::Type;
 use crate::syntax::{
     Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label,
     NaiveDouble, NumKind, Span, UnspannedExpr, V,
 };
+use crate::{Ctxt, Parsed};
 
 /// Built-ins
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
@@ -89,23 +87,23 @@ impl Builtin {
 /// A partially applied builtin.
 /// Invariant: the evaluation of the given args must not be able to progress further
 #[derive(Debug, Clone)]
-pub struct BuiltinClosure {
-    env: NzEnv,
+pub struct BuiltinClosure<'cx> {
+    env: NzEnv<'cx>,
     b: Builtin,
     /// Arguments applied to the closure so far.
-    args: Vec<Nir>,
+    args: Vec<Nir<'cx>>,
 }
 
-impl BuiltinClosure {
-    pub fn new(b: Builtin, env: NzEnv) -> NirKind {
+impl<'cx> BuiltinClosure<'cx> {
+    pub fn new(b: Builtin, env: NzEnv<'cx>) -> NirKind<'cx> {
         apply_builtin(b, Vec::new(), env)
     }
-    pub fn apply(&self, a: Nir) -> NirKind {
+    pub fn apply(&self, a: Nir<'cx>) -> NirKind<'cx> {
         use std::iter::once;
         let args = self.args.iter().cloned().chain(once(a)).collect();
         apply_builtin(self.b, args, self.env.clone())
     }
-    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
+    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind<'cx> {
         HirKind::Expr(self.args.iter().fold(
             ExprKind::Builtin(self.b),
             |acc, v| {
@@ -178,7 +176,7 @@ macro_rules! make_type {
     };
 }
 
-pub fn type_of_builtin(b: Builtin) -> Hir {
+pub fn type_of_builtin<'cx>(cx: Ctxt<'cx>, b: Builtin) -> Hir<'cx> {
     use Builtin::*;
     let expr = match b {
         Bool | Natural | Integer | Double | Text => make_type!(Type),
@@ -253,7 +251,10 @@ pub fn type_of_builtin(b: Builtin) -> Hir {
             forall (A: Type) -> Optional A
         ),
     };
-    skip_resolve_expr(&expr).unwrap()
+    Parsed::from_expr_without_imports(expr)
+        .resolve(cx)
+        .unwrap()
+        .0
 }
 
 // Ad-hoc macro to help construct closures
@@ -307,19 +308,28 @@ macro_rules! make_closure {
 }
 
 #[allow(clippy::cognitive_complexity)]
-fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
+fn apply_builtin<'cx>(
+    b: Builtin,
+    args: Vec<Nir<'cx>>,
+    env: NzEnv<'cx>,
+) -> NirKind<'cx> {
+    let cx = env.cx();
     use NirKind::*;
     use NumKind::{Bool, Double, Integer, Natural};
 
     // Small helper enum
-    enum Ret {
-        NirKind(NirKind),
-        Nir(Nir),
+    enum Ret<'cx> {
+        NirKind(NirKind<'cx>),
+        Nir(Nir<'cx>),
         DoneAsIs,
     }
     let make_closure = |e| {
-        typecheck(&skip_resolve_expr(&e).unwrap())
+        Parsed::from_expr_without_imports(e)
+            .resolve(cx)
+            .unwrap()
+            .typecheck(cx)
             .unwrap()
+            .as_hir()
             .eval(env.clone())
     };
 
@@ -486,7 +496,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
                     let mut kts = HashMap::new();
                     kts.insert(
                         "index".into(),
-                        Nir::from_builtin(Builtin::Natural),
+                        Nir::from_builtin(cx, Builtin::Natural),
                     );
                     kts.insert("value".into(), t.clone());
                     let t = Nir::from_kind(RecordType(kts));
@@ -516,7 +526,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
             }
         }
         (Builtin::ListBuild, [t, f]) => {
-            let list_t = Nir::from_builtin(Builtin::List).app(t.clone());
+            let list_t = Nir::from_builtin(cx, Builtin::List).app(t.clone());
             Ret::Nir(
                 f.app(list_t)
                     .app(
@@ -543,7 +553,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
             _ => Ret::DoneAsIs,
         },
         (Builtin::NaturalBuild, [f]) => Ret::Nir(
-            f.app(Nir::from_builtin(Builtin::Natural))
+            f.app(Nir::from_builtin(cx, Builtin::Natural))
                 .app(make_closure(make_closure!(
                     λ(x : Natural) ->
                     1 + var(x)
@@ -554,7 +564,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
         (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
             Num(Natural(0)) => Ret::Nir(zero.clone()),
             Num(Natural(n)) => {
-                let fold = Nir::from_builtin(Builtin::NaturalFold)
+                let fold = Nir::from_builtin(cx, Builtin::NaturalFold)
                     .app(Num(Natural(n - 1)).into_nir())
                     .app(t.clone())
                     .app(succ.clone())
@@ -572,12 +582,12 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
     }
 }
 
-impl std::cmp::PartialEq for BuiltinClosure {
+impl<'cx> std::cmp::PartialEq for BuiltinClosure<'cx> {
     fn eq(&self, other: &Self) -> bool {
         self.b == other.b && self.args == other.args
     }
 }
-impl std::cmp::Eq for BuiltinClosure {}
+impl<'cx> std::cmp::Eq for BuiltinClosure<'cx> {}
 
 impl std::fmt::Display for Builtin {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
diff --git a/dhall/src/ctxt.rs b/dhall/src/ctxt.rs
new file mode 100644
index 0000000..aad1a1b
--- /dev/null
+++ b/dhall/src/ctxt.rs
@@ -0,0 +1,211 @@
+use elsa::vec::FrozenVec;
+use once_cell::sync::OnceCell;
+use std::marker::PhantomData;
+use std::ops::{Deref, Index};
+
+use crate::semantics::{Import, ImportLocation, ImportNode};
+use crate::syntax::Span;
+use crate::Typed;
+
+/////////////////////////////////////////////////////////////////////////////////////////////////////
+// Ctxt
+
+/// Implementation detail. Made public for the `Index` instances.
+#[derive(Default)]
+pub struct CtxtS<'cx> {
+    imports: FrozenVec<Box<StoredImport<'cx>>>,
+    import_alternatives: FrozenVec<Box<StoredImportAlternative<'cx>>>,
+    import_results: FrozenVec<Box<StoredImportResult<'cx>>>,
+}
+
+/// Context for the dhall compiler. Stores various global maps.
+/// Access the relevant value using `cx[id]`.
+#[derive(Copy, Clone)]
+pub struct Ctxt<'cx>(&'cx CtxtS<'cx>);
+
+impl Ctxt<'_> {
+    pub fn with_new<T>(f: impl for<'cx> FnOnce(Ctxt<'cx>) -> T) -> T {
+        let cx = CtxtS::default();
+        let cx = Ctxt(&cx);
+        f(cx)
+    }
+}
+impl<'cx> Deref for Ctxt<'cx> {
+    type Target = &'cx CtxtS<'cx>;
+    fn deref(&self) -> &&'cx CtxtS<'cx> {
+        &self.0
+    }
+}
+impl<'a, 'cx, T> Index<&'a T> for CtxtS<'cx>
+where
+    Self: Index<T>,
+    T: Copy,
+{
+    type Output = <Self as Index<T>>::Output;
+    fn index(&self, id: &'a T) -> &Self::Output {
+        &self[*id]
+    }
+}
+
+/// Empty impl, because `FrozenVec` does not implement `Debug` and I can't be bothered to do it
+/// myself.
+impl<'cx> std::fmt::Debug for Ctxt<'cx> {
+    fn fmt(&self, _: &mut std::fmt::Formatter) -> std::fmt::Result {
+        Ok(())
+    }
+}
+
+/////////////////////////////////////////////////////////////////////////////////////////////////////
+// Imports
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
+pub struct ImportId<'cx>(usize, PhantomData<&'cx ()>);
+
+/// What's stored for each `ImportId`. Allows getting and setting a result for this import.
+pub struct StoredImport<'cx> {
+    cx: Ctxt<'cx>,
+    pub base_location: ImportLocation,
+    pub import: Import,
+    pub span: Span,
+    result: OnceCell<ImportResultId<'cx>>,
+}
+
+impl<'cx> StoredImport<'cx> {
+    /// Get the id of the result of fetching this import. Returns `None` if the result has not yet
+    /// been fetched.
+    pub fn get_resultid(&self) -> Option<ImportResultId<'cx>> {
+        self.result.get().copied()
+    }
+    /// Store the result of fetching this import.
+    pub fn set_resultid(&self, res: ImportResultId<'cx>) {
+        let _ = self.result.set(res);
+    }
+    /// Get the result of fetching this import. Returns `None` if the result has not yet been
+    /// fetched.
+    pub fn get_result(&self) -> Option<&'cx StoredImportResult<'cx>> {
+        let res = self.get_resultid()?;
+        Some(&self.cx[res])
+    }
+    /// Get the result of fetching this import. Panicx if the result has not yet been
+    /// fetched.
+    pub fn unwrap_result(&self) -> &'cx StoredImportResult<'cx> {
+        self.get_result()
+            .expect("imports should all have been resolved at this stage")
+    }
+    /// Store the result of fetching this import.
+    pub fn set_result(
+        &self,
+        res: StoredImportResult<'cx>,
+    ) -> ImportResultId<'cx> {
+        let res = self.cx.push_import_result(res);
+        self.set_resultid(res);
+        res
+    }
+}
+impl<'cx> Ctxt<'cx> {
+    /// Store an import and the location relative to which it must be resolved.
+    pub fn push_import(
+        self,
+        base_location: ImportLocation,
+        import: Import,
+        span: Span,
+    ) -> ImportId<'cx> {
+        let stored = StoredImport {
+            cx: self,
+            base_location,
+            import,
+            span,
+            result: OnceCell::new(),
+        };
+        let id = self.0.imports.len();
+        self.0.imports.push(Box::new(stored));
+        ImportId(id, PhantomData)
+    }
+}
+impl<'cx> Index<ImportId<'cx>> for CtxtS<'cx> {
+    type Output = StoredImport<'cx>;
+    fn index(&self, id: ImportId<'cx>) -> &StoredImport<'cx> {
+        &self.imports[id.0]
+    }
+}
+
+/////////////////////////////////////////////////////////////////////////////////////////////////////
+// Import alternatives
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
+pub struct ImportAlternativeId<'cx>(usize, PhantomData<&'cx ()>);
+
+/// What's stored for each `ImportAlternativeId`.
+pub struct StoredImportAlternative<'cx> {
+    pub left_imports: Box<[ImportNode<'cx>]>,
+    pub right_imports: Box<[ImportNode<'cx>]>,
+    /// `true` for left, `false` for right.
+    selected: OnceCell<bool>,
+}
+
+impl<'cx> StoredImportAlternative<'cx> {
+    /// Get which alternative got selected. `true` for left, `false` for right.
+    pub fn get_selected(&self) -> Option<bool> {
+        self.selected.get().copied()
+    }
+    /// Get which alternative got selected. `true` for left, `false` for right.
+    pub fn unwrap_selected(&self) -> bool {
+        self.get_selected()
+            .expect("imports should all have been resolved at this stage")
+    }
+    /// Set which alternative got selected. `true` for left, `false` for right.
+    pub fn set_selected(&self, selected: bool) {
+        let _ = self.selected.set(selected);
+    }
+}
+impl<'cx> Ctxt<'cx> {
+    pub fn push_import_alternative(
+        self,
+        left_imports: Box<[ImportNode<'cx>]>,
+        right_imports: Box<[ImportNode<'cx>]>,
+    ) -> ImportAlternativeId<'cx> {
+        let stored = StoredImportAlternative {
+            left_imports,
+            right_imports,
+            selected: OnceCell::new(),
+        };
+        let id = self.0.import_alternatives.len();
+        self.0.import_alternatives.push(Box::new(stored));
+        ImportAlternativeId(id, PhantomData)
+    }
+}
+impl<'cx> Index<ImportAlternativeId<'cx>> for CtxtS<'cx> {
+    type Output = StoredImportAlternative<'cx>;
+    fn index(
+        &self,
+        id: ImportAlternativeId<'cx>,
+    ) -> &StoredImportAlternative<'cx> {
+        &self.import_alternatives[id.0]
+    }
+}
+
+/////////////////////////////////////////////////////////////////////////////////////////////////////
+// Import results
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
+pub struct ImportResultId<'cx>(usize, PhantomData<&'cx ()>);
+
+type StoredImportResult<'cx> = Typed<'cx>;
+
+impl<'cx> Ctxt<'cx> {
+    /// Store the result of fetching an import.
+    pub fn push_import_result(
+        self,
+        res: StoredImportResult<'cx>,
+    ) -> ImportResultId<'cx> {
+        let id = self.0.import_results.len();
+        self.0.import_results.push(Box::new(res));
+        ImportResultId(id, PhantomData)
+    }
+}
+impl<'cx> Index<ImportResultId<'cx>> for CtxtS<'cx> {
+    type Output = StoredImportResult<'cx>;
+    fn index(&self, id: ImportResultId<'cx>) -> &StoredImportResult<'cx> {
+        &self.import_results[id.0]
+    }
+}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 6747eff..ad16a24 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -5,17 +5,18 @@
     clippy::needless_lifetimes,
     clippy::new_ret_no_self,
     clippy::new_without_default,
+    clippy::try_err,
     clippy::useless_format
 )]
 
 pub mod builtins;
+pub mod ctxt;
 pub mod error;
 pub mod operations;
 pub mod semantics;
 pub mod syntax;
 pub mod utils;
 
-use std::fmt::Display;
 use std::path::Path;
 use url::Url;
 
@@ -26,6 +27,8 @@ use crate::semantics::resolve::ImportLocation;
 use crate::semantics::{typecheck, typecheck_with, Hir, Nir, Tir, Type};
 use crate::syntax::Expr;
 
+pub use ctxt::*;
+
 #[derive(Debug, Clone)]
 pub struct Parsed(Expr, ImportLocation);
 
@@ -33,20 +36,20 @@ pub struct Parsed(Expr, ImportLocation);
 ///
 /// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
 #[derive(Debug, Clone)]
-pub struct Resolved(Hir);
+pub struct Resolved<'cx>(Hir<'cx>);
 
 /// A typed expression
 #[derive(Debug, Clone)]
-pub struct Typed {
-    pub hir: Hir,
-    pub ty: Type,
+pub struct Typed<'cx> {
+    pub hir: Hir<'cx>,
+    pub ty: Type<'cx>,
 }
 
 /// A normalized expression.
 ///
 /// This is actually a lie, because the expression will only get normalized on demand.
 #[derive(Debug, Clone)]
-pub struct Normalized(Nir);
+pub struct Normalized<'cx>(Nir<'cx>);
 
 /// Controls conversion from `Nir` to `Expr`
 #[derive(Copy, Clone, Default)]
@@ -56,6 +59,11 @@ pub struct ToExprOptions {
 }
 
 impl Parsed {
+    /// Construct from an `Expr`. This `Expr` will have imports disabled.
+    pub fn from_expr_without_imports(e: Expr) -> Self {
+        Parsed(e, ImportLocation::dhall_code_without_imports())
+    }
+
     pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
         parse::parse_file(f)
     }
@@ -73,11 +81,14 @@ impl Parsed {
         parse::parse_binary(data)
     }
 
-    pub fn resolve(self) -> Result<Resolved, Error> {
-        resolve::resolve(self)
+    pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result<Resolved<'cx>, Error> {
+        resolve::resolve(cx, self)
     }
-    pub fn skip_resolve(self) -> Result<Resolved, Error> {
-        resolve::skip_resolve(self)
+    pub fn skip_resolve<'cx>(
+        self,
+        cx: Ctxt<'cx>,
+    ) -> Result<Resolved<'cx>, Error> {
+        resolve::skip_resolve(cx, self)
     }
 
     /// Converts a value back to the corresponding AST expression.
@@ -86,59 +97,66 @@ impl Parsed {
     }
 }
 
-impl Resolved {
-    pub fn typecheck(&self) -> Result<Typed, TypeError> {
-        Ok(Typed::from_tir(typecheck(&self.0)?))
+impl<'cx> Resolved<'cx> {
+    pub fn typecheck(&self, cx: Ctxt<'cx>) -> Result<Typed<'cx>, TypeError> {
+        Ok(Typed::from_tir(typecheck(cx, &self.0)?))
     }
-    pub fn typecheck_with(self, ty: &Hir) -> Result<Typed, TypeError> {
-        Ok(Typed::from_tir(typecheck_with(&self.0, ty)?))
+    pub fn typecheck_with(
+        self,
+        cx: Ctxt<'cx>,
+        ty: &Hir<'cx>,
+    ) -> Result<Typed<'cx>, TypeError> {
+        Ok(Typed::from_tir(typecheck_with(cx, &self.0, ty)?))
     }
     /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr(&self) -> Expr {
-        self.0.to_expr_noopts()
+    pub fn to_expr(&self, cx: Ctxt<'cx>) -> Expr {
+        self.0.to_expr_noopts(cx)
     }
 }
 
-impl Typed {
-    fn from_tir(tir: Tir<'_>) -> Self {
+impl<'cx> Typed<'cx> {
+    fn from_tir(tir: Tir<'cx, '_>) -> Self {
         Typed {
             hir: tir.as_hir().clone(),
             ty: tir.ty().clone(),
         }
     }
     /// Reduce an expression to its normal form, performing beta reduction
-    pub fn normalize(&self) -> Normalized {
-        Normalized(self.hir.eval_closed_expr())
+    pub fn normalize(&self, cx: Ctxt<'cx>) -> Normalized<'cx> {
+        Normalized(self.hir.eval_closed_expr(cx))
     }
 
     /// Converts a value back to the corresponding AST expression.
-    fn to_expr(&self) -> Expr {
-        self.hir.to_expr(ToExprOptions { alpha: false })
+    fn to_expr(&self, cx: Ctxt<'cx>) -> Expr {
+        self.hir.to_expr(cx, ToExprOptions { alpha: false })
     }
 
-    pub fn ty(&self) -> &Type {
+    pub fn as_hir(&self) -> &Hir<'cx> {
+        &self.hir
+    }
+    pub fn ty(&self) -> &Type<'cx> {
         &self.ty
     }
-    pub fn get_type(&self) -> Result<Normalized, TypeError> {
+    pub fn get_type(&self) -> Result<Normalized<'cx>, TypeError> {
         Ok(Normalized(self.ty.clone().into_nir()))
     }
 }
 
-impl Normalized {
+impl<'cx> Normalized<'cx> {
     /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr(&self) -> Expr {
-        self.0.to_expr(ToExprOptions::default())
+    pub fn to_expr(&self, cx: Ctxt<'cx>) -> Expr {
+        self.0.to_expr(cx, ToExprOptions::default())
     }
     /// Converts a value back to the corresponding Hir expression.
-    pub fn to_hir(&self) -> Hir {
+    pub fn to_hir(&self) -> Hir<'cx> {
         self.0.to_hir_noenv()
     }
-    pub fn as_nir(&self) -> &Nir {
+    pub fn as_nir(&self) -> &Nir<'cx> {
         &self.0
     }
     /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process.
-    pub fn to_expr_alpha(&self) -> Expr {
-        self.0.to_expr(ToExprOptions { alpha: true })
+    pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr {
+        self.0.to_expr(cx, ToExprOptions { alpha: true })
     }
 }
 
@@ -170,38 +188,10 @@ impl From<Parsed> for Expr {
         other.to_expr()
     }
 }
-impl From<Normalized> for Expr {
-    fn from(other: Normalized) -> Self {
-        other.to_expr()
-    }
-}
-
-impl Display for Resolved {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.to_expr().fmt(f)
-    }
-}
-
-impl Eq for Typed {}
-impl PartialEq for Typed {
-    fn eq(&self, other: &Self) -> bool {
-        self.normalize() == other.normalize()
-    }
-}
-impl Display for Typed {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.to_expr().fmt(f)
-    }
-}
 
-impl Eq for Normalized {}
-impl PartialEq for Normalized {
+impl<'cx> Eq for Normalized<'cx> {}
+impl<'cx> PartialEq for Normalized<'cx> {
     fn eq(&self, other: &Self) -> bool {
         self.0 == other.0
     }
 }
-impl Display for Normalized {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.to_expr().fmt(f)
-    }
-}
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index 28375b2..6c68e7c 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -8,7 +8,7 @@ use crate::semantics::{
 };
 use crate::syntax::{ExprKind, Label, NumKind};
 
-fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret {
+fn normalize_binop<'cx>(o: BinOp, x: Nir<'cx>, y: Nir<'cx>) -> Ret<'cx> {
     use BinOp::*;
     use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
     use NumKind::{Bool, Natural};
@@ -119,7 +119,7 @@ fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret {
     }
 }
 
-fn normalize_field(v: &Nir, field: &Label) -> Ret {
+fn normalize_field<'cx>(v: &Nir<'cx>, field: &Label) -> Ret<'cx> {
     use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge};
     use NirKind::{Op, RecordLit, UnionConstructor, UnionType};
     use OpKind::{BinOp, Field, Projection};
@@ -187,7 +187,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Ret {
     }
 }
 
-pub fn normalize_operation(opkind: OpKind<Nir>) -> Ret {
+pub fn normalize_operation<'cx>(opkind: OpKind<Nir<'cx>>) -> Ret<'cx> {
     use self::BinOp::RightBiasedRecordMerge;
     use NirKind::{
         EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op,
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index bc0e864..9b19c84 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -13,9 +13,9 @@ use crate::syntax::{Const, ExprKind, Span};
 
 fn check_rectymerge(
     span: &Span,
-    env: &TyEnv,
-    x: Nir,
-    y: Nir,
+    env: &TyEnv<'_>,
+    x: Nir<'_>,
+    y: Nir<'_>,
 ) -> Result<(), TypeError> {
     let kts_x = match x.kind() {
         NirKind::RecordType(kts) => kts,
@@ -44,13 +44,14 @@ fn check_rectymerge(
     Ok(())
 }
 
-fn typecheck_binop(
-    env: &TyEnv,
+fn typecheck_binop<'cx>(
+    env: &TyEnv<'cx>,
     span: Span,
     op: BinOp,
-    l: Tir<'_>,
-    r: Tir<'_>,
-) -> Result<Type, TypeError> {
+    l: Tir<'cx, '_>,
+    r: Tir<'cx, '_>,
+) -> Result<Type<'cx>, TypeError> {
+    let cx = env.cx();
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
     use BinOp::*;
     use NirKind::{ListType, RecordType};
@@ -124,17 +125,20 @@ fn typecheck_binop(
             Type::from_const(Const::Type)
         }
         op => {
-            let t = Type::from_builtin(match op {
-                BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool,
-                NaturalPlus | NaturalTimes => Builtin::Natural,
-                TextAppend => Builtin::Text,
-                ListAppend
-                | RightBiasedRecordMerge
-                | RecursiveRecordMerge
-                | RecursiveRecordTypeMerge
-                | Equivalence => unreachable!(),
-                ImportAlt => unreachable!("ImportAlt leftover in tck"),
-            });
+            let t = Type::from_builtin(
+                cx,
+                match op {
+                    BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool,
+                    NaturalPlus | NaturalTimes => Builtin::Natural,
+                    TextAppend => Builtin::Text,
+                    ListAppend
+                    | RightBiasedRecordMerge
+                    | RecursiveRecordMerge
+                    | RecursiveRecordTypeMerge
+                    | Equivalence => unreachable!(),
+                    ImportAlt => unreachable!("ImportAlt leftover in tck"),
+                },
+            );
 
             if *l.ty() != t {
                 return span_err("BinOpTypeMismatch");
@@ -149,13 +153,13 @@ fn typecheck_binop(
     })
 }
 
-fn typecheck_merge(
-    env: &TyEnv,
+fn typecheck_merge<'cx>(
+    env: &TyEnv<'cx>,
     span: Span,
-    record: &Tir<'_>,
-    scrut: &Tir<'_>,
-    type_annot: Option<&Tir<'_>>,
-) -> Result<Type, TypeError> {
+    record: &Tir<'cx, '_>,
+    scrut: &Tir<'cx, '_>,
+    type_annot: Option<&Tir<'cx, '_>>,
+) -> Result<Type<'cx>, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
     use NirKind::{OptionalType, PiClosure, RecordType, UnionType};
 
@@ -287,11 +291,12 @@ fn typecheck_merge(
     })
 }
 
-pub fn typecheck_operation(
-    env: &TyEnv,
+pub fn typecheck_operation<'cx>(
+    env: &TyEnv<'cx>,
     span: Span,
-    opkind: OpKind<Tir<'_>>,
-) -> Result<Type, TypeError> {
+    opkind: OpKind<Tir<'cx, '_>>,
+) -> Result<Type<'cx>, TypeError> {
+    let cx = env.cx();
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
     use NirKind::{ListType, PiClosure, RecordType, UnionType};
     use OpKind::*;
@@ -347,7 +352,7 @@ pub fn typecheck_operation(
         }
         BinOp(o, l, r) => typecheck_binop(env, span, o, l, r)?,
         BoolIf(x, y, z) => {
-            if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
+            if *x.ty().kind() != NirKind::from_builtin(cx, Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
             if y.ty().ty().as_const().is_none() {
@@ -399,7 +404,7 @@ pub fn typecheck_operation(
                     return span_err(err_msg);
                 }
                 match kts.get("mapKey") {
-                    Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
+                    Some(t) if *t == Nir::from_builtin(cx, Builtin::Text) => {}
                     _ => return span_err(err_msg),
                 }
                 match kts.get("mapValue") {
@@ -418,9 +423,12 @@ pub fn typecheck_operation(
                 }
 
                 let mut kts = HashMap::new();
-                kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
+                kts.insert(
+                    "mapKey".into(),
+                    Nir::from_builtin(cx, Builtin::Text),
+                );
                 kts.insert("mapValue".into(), entry_type);
-                let output_type: Type = Nir::from_builtin(Builtin::List)
+                let output_type: Type = Nir::from_builtin(cx, Builtin::List)
                     .app(Nir::from_kind(RecordType(kts)))
                     .to_type(Const::Type);
                 if let Some(annot) = annot {
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index ec99dbe..30fa8af 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,5 @@
 use crate::semantics::{AlphaVar, Nir, NirKind};
+use crate::Ctxt;
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub enum NzVar {
@@ -9,19 +10,20 @@ pub enum NzVar {
 }
 
 #[derive(Debug, Clone)]
-enum EnvItem<Type> {
+enum EnvItem<'cx, T> {
     // Variable is bound with given type
-    Kept(Type),
+    Kept(T),
     // Variable has been replaced by corresponding value
-    Replaced(Nir, Type),
+    Replaced(Nir<'cx>, T),
 }
 
 #[derive(Debug, Clone)]
-pub struct ValEnv<Type> {
-    items: Vec<EnvItem<Type>>,
+pub struct ValEnv<'cx, T> {
+    cx: Ctxt<'cx>,
+    items: Vec<EnvItem<'cx, T>>,
 }
 
-pub type NzEnv = ValEnv<()>;
+pub type NzEnv<'cx> = ValEnv<'cx, ()>;
 
 impl NzVar {
     pub fn new(idx: usize) -> Self {
@@ -46,11 +48,17 @@ impl NzVar {
     }
 }
 
-impl<Type: Clone> ValEnv<Type> {
-    pub fn new() -> Self {
-        ValEnv { items: Vec::new() }
+impl<'cx, T: Clone> ValEnv<'cx, T> {
+    pub fn new(cx: Ctxt<'cx>) -> Self {
+        ValEnv {
+            cx,
+            items: Vec::new(),
+        }
+    }
+    pub fn cx(&self) -> Ctxt<'cx> {
+        self.cx
     }
-    pub fn discard_types(&self) -> ValEnv<()> {
+    pub fn discard_types(&self) -> ValEnv<'cx, ()> {
         let items = self
             .items
             .iter()
@@ -59,27 +67,27 @@ impl<Type: Clone> ValEnv<Type> {
                 EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
             })
             .collect();
-        ValEnv { items }
+        ValEnv { cx: self.cx, items }
     }
 
-    pub fn insert_type(&self, ty: Type) -> Self {
+    pub fn insert_type(&self, ty: T) -> Self {
         let mut env = self.clone();
         env.items.push(EnvItem::Kept(ty));
         env
     }
-    pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
+    pub fn insert_value(&self, e: Nir<'cx>, ty: T) -> Self {
         let mut env = self.clone();
         env.items.push(EnvItem::Replaced(e, ty));
         env
     }
-    pub fn lookup_val(&self, var: AlphaVar) -> NirKind {
+    pub fn lookup_val(&self, var: AlphaVar) -> NirKind<'cx> {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
             EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
             EnvItem::Replaced(x, _) => x.kind().clone(),
         }
     }
-    pub fn lookup_ty(&self, var: AlphaVar) -> Type {
+    pub fn lookup_ty(&self, var: AlphaVar) -> T {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
             EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
@@ -87,8 +95,8 @@ impl<Type: Clone> ValEnv<Type> {
     }
 }
 
-impl<'a> From<&'a NzEnv> for NzEnv {
-    fn from(x: &'a NzEnv) -> Self {
+impl<'cx, 'a> From<&'a NzEnv<'cx>> for NzEnv<'cx> {
+    fn from(x: &'a NzEnv<'cx>) -> Self {
         x.clone()
     }
 }
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 7bda836..8cf06c5 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -11,7 +11,7 @@ use crate::semantics::{
 use crate::syntax::{
     Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span,
 };
-use crate::ToExprOptions;
+use crate::{Ctxt, ToExprOptions};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<OnceCell> to share computation.
@@ -20,31 +20,31 @@ use crate::ToExprOptions;
 /// normalize as needed.
 /// Stands for "Normalized Intermediate Representation"
 #[derive(Clone)]
-pub struct Nir(Rc<lazy::Lazy<Thunk, NirKind>>);
+pub struct Nir<'cx>(Rc<lazy::Lazy<Thunk<'cx>, NirKind<'cx>>>);
 
 /// An unevaluated subexpression
 #[derive(Debug, Clone)]
-pub enum Thunk {
+pub enum Thunk<'cx> {
     /// A completely unnormalized expression.
-    Thunk { env: NzEnv, body: Hir },
+    Thunk { env: NzEnv<'cx>, body: Hir<'cx> },
     /// A partially normalized expression that may need to go through `normalize_one_layer`.
-    PartialExpr { env: NzEnv, expr: ExprKind<Nir> },
+    PartialExpr { expr: ExprKind<Nir<'cx>> },
 }
 
 /// An unevaluated subexpression that takes an argument.
 #[derive(Debug, Clone)]
-pub enum Closure {
+pub enum Closure<'cx> {
     /// Normal closure
-    Closure { env: NzEnv, body: Hir },
+    Closure { env: NzEnv<'cx>, body: Hir<'cx> },
     /// Closure that ignores the argument passed
-    ConstantClosure { body: Nir },
+    ConstantClosure { body: Nir<'cx> },
 }
 
 /// A text literal with interpolations.
 // Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
 // text values must be merged.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct TextLit(Vec<InterpolatedTextContents<Nir>>);
+pub struct TextLit<'cx>(Vec<InterpolatedTextContents<Nir<'cx>>>);
 
 /// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
 /// normalized up to the first constructor, but subexpressions may not be fully normalized.
@@ -54,67 +54,65 @@ pub struct TextLit(Vec<InterpolatedTextContents<Nir>>);
 /// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
 /// we only need to recursively normalize its sub-`Nir`s to get to the NF.
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum NirKind {
+pub enum NirKind<'cx> {
     /// Closures
     LamClosure {
         binder: Binder,
-        annot: Nir,
-        closure: Closure,
+        annot: Nir<'cx>,
+        closure: Closure<'cx>,
     },
     PiClosure {
         binder: Binder,
-        annot: Nir,
-        closure: Closure,
+        annot: Nir<'cx>,
+        closure: Closure<'cx>,
     },
-    AppliedBuiltin(BuiltinClosure),
+    AppliedBuiltin(BuiltinClosure<'cx>),
 
     Var(NzVar),
     Const(Const),
     Num(NumKind),
     // Must be a number type, Bool or Text
     BuiltinType(Builtin),
-    TextLit(TextLit),
-    EmptyOptionalLit(Nir),
-    NEOptionalLit(Nir),
-    OptionalType(Nir),
+    TextLit(TextLit<'cx>),
+    EmptyOptionalLit(Nir<'cx>),
+    NEOptionalLit(Nir<'cx>),
+    OptionalType(Nir<'cx>),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
-    EmptyListLit(Nir),
-    NEListLit(Vec<Nir>),
-    ListType(Nir),
-    RecordLit(HashMap<Label, Nir>),
-    RecordType(HashMap<Label, Nir>),
-    UnionConstructor(Label, HashMap<Label, Option<Nir>>),
-    UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
-    UnionType(HashMap<Label, Option<Nir>>),
-    Equivalence(Nir, Nir),
-    Assert(Nir),
+    EmptyListLit(Nir<'cx>),
+    NEListLit(Vec<Nir<'cx>>),
+    ListType(Nir<'cx>),
+    RecordLit(HashMap<Label, Nir<'cx>>),
+    RecordType(HashMap<Label, Nir<'cx>>),
+    UnionConstructor(Label, HashMap<Label, Option<Nir<'cx>>>),
+    UnionLit(Label, Nir<'cx>, HashMap<Label, Option<Nir<'cx>>>),
+    UnionType(HashMap<Label, Option<Nir<'cx>>>),
+    Equivalence(Nir<'cx>, Nir<'cx>),
+    Assert(Nir<'cx>),
     /// Invariant: evaluation must not be able to progress with `normalize_operation`.
     /// This is used when an operation couldn't proceed further, for example because of variables.
-    Op(OpKind<Nir>),
+    Op(OpKind<Nir<'cx>>),
 }
 
-impl Nir {
+impl<'cx> Nir<'cx> {
     /// Construct a Nir from a completely unnormalized expression.
-    pub fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+    pub fn new_thunk(env: NzEnv<'cx>, hir: Hir<'cx>) -> Self {
         Nir(Rc::new(lazy::Lazy::new(Thunk::new(env, hir))))
     }
     /// Construct a Nir from a partially normalized expression that's not in WHNF.
-    pub fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
-        // TODO: env
-        let env = NzEnv::new();
-        Nir(Rc::new(lazy::Lazy::new(Thunk::from_partial_expr(env, e))))
+    pub fn from_partial_expr(e: ExprKind<Self>) -> Self {
+        Nir(Rc::new(lazy::Lazy::new(Thunk::from_partial_expr(e))))
     }
     /// Make a Nir from a NirKind
-    pub fn from_kind(v: NirKind) -> Nir {
+    pub fn from_kind(v: NirKind<'cx>) -> Self {
         Nir(Rc::new(lazy::Lazy::new_completed(v)))
     }
     pub fn from_const(c: Const) -> Self {
         Self::from_kind(NirKind::Const(c))
     }
-    pub fn from_builtin(b: Builtin) -> Self {
-        Self::from_builtin_env(b, &NzEnv::new())
+    pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
+        Self::from_builtin_env(b, &NzEnv::new(cx))
     }
-    pub fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+    pub fn from_builtin_env(b: Builtin, env: &NzEnv<'cx>) -> Self {
         Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
     }
     pub fn from_text(txt: impl ToString) -> Self {
@@ -129,51 +127,54 @@ impl Nir {
     }
 
     /// This is what you want if you want to pattern-match on the value.
-    pub fn kind(&self) -> &NirKind {
+    pub fn kind(&self) -> &NirKind<'cx> {
         &*self.0
     }
 
     /// The contents of a `Nir` are immutable and shared. If however we happen to be the sole
     /// owners, we can mutate it directly. Otherwise, this clones the internal value first.
-    pub fn kind_mut(&mut self) -> &mut NirKind {
+    pub fn kind_mut(&mut self) -> &mut NirKind<'cx> {
         Rc::make_mut(&mut self.0).get_mut()
     }
     /// If we are the sole owner of this Nir, we can avoid a clone.
-    pub fn into_kind(self) -> NirKind {
+    pub fn into_kind(self) -> NirKind<'cx> {
         match Rc::try_unwrap(self.0) {
             Ok(lazy) => lazy.into_inner(),
             Err(rc) => (**rc).clone(),
         }
     }
 
-    pub fn to_type(&self, u: impl Into<Universe>) -> Type {
+    pub fn to_type(&self, u: impl Into<Universe>) -> Type<'cx> {
         Type::new(self.clone(), u.into())
     }
     /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> Expr {
-        self.to_hir_noenv().to_expr(opts)
+    pub fn to_expr(&self, cx: Ctxt<'cx>, opts: ToExprOptions) -> Expr {
+        self.to_hir_noenv().to_expr(cx, opts)
     }
-    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr {
         self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
 
-    pub fn app(&self, v: Nir) -> Nir {
+    pub fn app(&self, v: Self) -> Self {
         Nir::from_kind(self.app_to_kind(v))
     }
-    pub fn app_to_kind(&self, v: Nir) -> NirKind {
+    pub fn app_to_kind(&self, v: Self) -> NirKind<'cx> {
         apply_any(self, v)
     }
 
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
-        let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| {
-            ExprKind::UnionType(
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
-                    })
-                    .collect(),
-            )
-        };
+    pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
+        let map_uniontype =
+            |kts: &HashMap<Label, Option<Nir<'cx>>>| -> ExprKind<Hir<'cx>> {
+                ExprKind::UnionType(
+                    kts.iter()
+                        .map(|(k, v)| {
+                            (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
+                        })
+                        .collect(),
+                )
+            };
+        let builtin =
+            |b| Hir::new(HirKind::Expr(ExprKind::Builtin(b)), Span::Artificial);
 
         let hir = match self.kind() {
             NirKind::Var(v) => HirKind::Var(venv.lookup(*v)),
@@ -204,21 +205,21 @@ impl Nir {
                 NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
                 NirKind::Num(l) => ExprKind::Num(l.clone()),
                 NirKind::OptionalType(t) => ExprKind::Op(OpKind::App(
-                    Nir::from_builtin(Builtin::Optional).to_hir(venv),
+                    builtin(Builtin::Optional),
                     t.to_hir(venv),
                 )),
                 NirKind::EmptyOptionalLit(n) => ExprKind::Op(OpKind::App(
-                    Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
+                    builtin(Builtin::OptionalNone),
                     n.to_hir(venv),
                 )),
                 NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
                 NirKind::ListType(t) => ExprKind::Op(OpKind::App(
-                    Nir::from_builtin(Builtin::List).to_hir(venv),
+                    builtin(Builtin::List),
                     t.to_hir(venv),
                 )),
                 NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
                     HirKind::Expr(ExprKind::Op(OpKind::App(
-                        Nir::from_builtin(Builtin::List).to_hir(venv),
+                        builtin(Builtin::List),
                         n.to_hir(venv),
                     ))),
                     Span::Artificial,
@@ -276,52 +277,52 @@ impl Nir {
 
         Hir::new(hir, Span::Artificial)
     }
-    pub fn to_hir_noenv(&self) -> Hir {
+    pub fn to_hir_noenv(&self) -> Hir<'cx> {
         self.to_hir(VarEnv::new())
     }
 }
 
-impl NirKind {
-    pub fn into_nir(self) -> Nir {
+impl<'cx> NirKind<'cx> {
+    pub fn into_nir(self) -> Nir<'cx> {
         Nir::from_kind(self)
     }
 
-    pub fn from_builtin(b: Builtin) -> NirKind {
-        NirKind::from_builtin_env(b, NzEnv::new())
+    pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
+        NirKind::from_builtin_env(b, NzEnv::new(cx))
     }
-    pub fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+    pub fn from_builtin_env(b: Builtin, env: NzEnv<'cx>) -> Self {
         BuiltinClosure::new(b, env)
     }
 }
 
-impl Thunk {
-    fn new(env: NzEnv, body: Hir) -> Self {
+impl<'cx> Thunk<'cx> {
+    fn new(env: NzEnv<'cx>, body: Hir<'cx>) -> Self {
         Thunk::Thunk { env, body }
     }
-    fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
-        Thunk::PartialExpr { env, expr }
+    fn from_partial_expr(expr: ExprKind<Nir<'cx>>) -> Self {
+        Thunk::PartialExpr { expr }
     }
-    fn eval(self) -> NirKind {
+    fn eval(self) -> NirKind<'cx> {
         match self {
-            Thunk::Thunk { env, body } => normalize_hir(&env, &body),
-            Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
+            Thunk::Thunk { env, body, .. } => normalize_hir(&env, &body),
+            Thunk::PartialExpr { expr } => normalize_one_layer(expr),
         }
     }
 }
 
-impl Closure {
-    pub fn new(env: &NzEnv, body: Hir) -> Self {
+impl<'cx> Closure<'cx> {
+    pub fn new(env: &NzEnv<'cx>, body: Hir<'cx>) -> Self {
         Closure::Closure {
             env: env.clone(),
             body,
         }
     }
     /// New closure that ignores its argument
-    pub fn new_constant(body: Nir) -> Self {
+    pub fn new_constant(body: Nir<'cx>) -> Self {
         Closure::ConstantClosure { body }
     }
 
-    pub fn apply(&self, val: Nir) -> Nir {
+    pub fn apply(&self, val: Nir<'cx>) -> Nir<'cx> {
         match self {
             Closure::Closure { env, body, .. } => {
                 body.eval(env.insert_value(val, ()))
@@ -329,7 +330,7 @@ impl Closure {
             Closure::ConstantClosure { body, .. } => body.clone(),
         }
     }
-    fn apply_var(&self, var: NzVar) -> Nir {
+    fn apply_var(&self, var: NzVar) -> Nir<'cx> {
         match self {
             Closure::Closure { .. } => {
                 self.apply(Nir::from_kind(NirKind::Var(var)))
@@ -339,13 +340,13 @@ impl Closure {
     }
 
     /// Convert this closure to a Hir expression
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+    pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
         self.apply_var(NzVar::new(venv.size()))
             .to_hir(venv.insert())
     }
     /// If the closure variable is free in the closure, return Err. Otherwise, return the value
     /// with that free variable remove.
-    pub fn remove_binder(&self) -> Result<Nir, ()> {
+    pub fn remove_binder(&self) -> Result<Nir<'cx>, ()> {
         match self {
             Closure::Closure { .. } => {
                 let v = NzVar::fresh();
@@ -358,20 +359,20 @@ impl Closure {
     }
 }
 
-impl TextLit {
+impl<'cx> TextLit<'cx> {
     pub fn new(
-        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir<'cx>>>,
     ) -> Self {
         TextLit(squash_textlit(elts))
     }
-    pub fn interpolate(v: Nir) -> TextLit {
+    pub fn interpolate(v: Nir<'cx>) -> Self {
         TextLit(vec![InterpolatedTextContents::Expr(v)])
     }
-    pub fn from_text(s: String) -> TextLit {
+    pub fn from_text(s: String) -> Self {
         TextLit(vec![InterpolatedTextContents::Text(s)])
     }
 
-    pub fn concat(&self, other: &TextLit) -> TextLit {
+    pub fn concat(&self, other: &Self) -> Self {
         TextLit::new(self.iter().chain(other.iter()).cloned())
     }
     pub fn is_empty(&self) -> bool {
@@ -379,7 +380,7 @@ impl TextLit {
     }
     /// If the literal consists of only one interpolation and not text, return the interpolated
     /// value.
-    pub fn as_single_expr(&self) -> Option<&Nir> {
+    pub fn as_single_expr(&self) -> Option<&Nir<'cx>> {
         use InterpolatedTextContents::Expr;
         if let [Expr(v)] = self.0.as_slice() {
             Some(v)
@@ -398,43 +399,45 @@ impl TextLit {
             None
         }
     }
-    pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
+    pub fn iter(
+        &self,
+    ) -> impl Iterator<Item = &InterpolatedTextContents<Nir<'cx>>> {
         self.0.iter()
     }
 }
 
-impl lazy::Eval<NirKind> for Thunk {
-    fn eval(self) -> NirKind {
+impl<'cx> lazy::Eval<NirKind<'cx>> for Thunk<'cx> {
+    fn eval(self) -> NirKind<'cx> {
         self.eval()
     }
 }
 
 /// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Nir {
+impl<'cx> std::cmp::PartialEq for Nir<'cx> {
     fn eq(&self, other: &Self) -> bool {
         Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
     }
 }
-impl std::cmp::Eq for Nir {}
+impl<'cx> std::cmp::Eq for Nir<'cx> {}
 
-impl std::cmp::PartialEq for Thunk {
+impl<'cx> std::cmp::PartialEq for Thunk<'cx> {
     fn eq(&self, _other: &Self) -> bool {
         unreachable!(
             "Trying to compare thunks but we should only compare WHNFs"
         )
     }
 }
-impl std::cmp::Eq for Thunk {}
+impl<'cx> std::cmp::Eq for Thunk<'cx> {}
 
-impl std::cmp::PartialEq for Closure {
+impl<'cx> std::cmp::PartialEq for Closure<'cx> {
     fn eq(&self, other: &Self) -> bool {
         let v = NzVar::fresh();
         self.apply_var(v) == other.apply_var(v)
     }
 }
-impl std::cmp::Eq for Closure {}
+impl<'cx> std::cmp::Eq for Closure<'cx> {}
 
-impl std::fmt::Debug for Nir {
+impl<'cx> std::fmt::Debug for Nir<'cx> {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         if let NirKind::Const(c) = self.kind() {
             return write!(fmt, "{:?}", c);
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 62efc5f..59710d1 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -5,7 +5,7 @@ use crate::semantics::NzEnv;
 use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
 use crate::syntax::{ExprKind, InterpolatedTextContents};
 
-pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
+pub fn apply_any<'cx>(f: &Nir<'cx>, a: Nir<'cx>) -> NirKind<'cx> {
     match f.kind() {
         NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
         NirKind::AppliedBuiltin(closure) => closure.apply(a),
@@ -16,16 +16,16 @@ pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
     }
 }
 
-pub fn squash_textlit(
-    elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
-) -> Vec<InterpolatedTextContents<Nir>> {
+pub fn squash_textlit<'cx>(
+    elts: impl Iterator<Item = InterpolatedTextContents<Nir<'cx>>>,
+) -> Vec<InterpolatedTextContents<Nir<'cx>>> {
     use std::mem::replace;
     use InterpolatedTextContents::{Expr, Text};
 
-    fn inner(
-        elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+    fn inner<'cx>(
+        elts: impl Iterator<Item = InterpolatedTextContents<Nir<'cx>>>,
         crnt_str: &mut String,
-        ret: &mut Vec<InterpolatedTextContents<Nir>>,
+        ret: &mut Vec<InterpolatedTextContents<Nir<'cx>>>,
     ) {
         for contents in elts {
             match contents {
@@ -81,22 +81,22 @@ where
     kvs
 }
 
-pub type Ret = NirKind;
+pub type Ret<'cx> = NirKind<'cx>;
 
-pub fn ret_nir(x: Nir) -> Ret {
+pub fn ret_nir<'cx>(x: Nir<'cx>) -> Ret<'cx> {
     x.into_kind()
 }
-pub fn ret_kind(x: NirKind) -> Ret {
+pub fn ret_kind<'cx>(x: NirKind<'cx>) -> Ret<'cx> {
     x
 }
-pub fn ret_ref(x: &Nir) -> Ret {
+pub fn ret_ref<'cx>(x: &Nir<'cx>) -> Ret<'cx> {
     x.kind().clone()
 }
-pub fn ret_op(x: OpKind<Nir>) -> Ret {
+pub fn ret_op<'cx>(x: OpKind<Nir<'cx>>) -> Ret<'cx> {
     NirKind::Op(x)
 }
 
-pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
+pub fn normalize_one_layer<'cx>(expr: ExprKind<Nir<'cx>>) -> NirKind<'cx> {
     use NirKind::{
         Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType,
         UnionType,
@@ -106,15 +106,13 @@ pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
         ExprKind::Var(..)
         | ExprKind::Lam(..)
         | ExprKind::Pi(..)
-        | ExprKind::Let(..) => {
+        | ExprKind::Let(..)
+        | ExprKind::Builtin(..) => {
             unreachable!("This case should have been handled in normalize_hir")
         }
 
         ExprKind::Const(c) => ret_kind(Const(c)),
         ExprKind::Num(l) => ret_kind(Num(l)),
-        ExprKind::Builtin(b) => {
-            ret_kind(NirKind::from_builtin_env(b, env.clone()))
-        }
         ExprKind::TextLit(elts) => {
             let tlit = TextLit::new(elts.into_iter());
             // Simplify bare interpolation
@@ -154,10 +152,22 @@ pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
 }
 
 /// Normalize Hir into WHNF
-pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
+pub fn normalize_hir<'cx>(env: &NzEnv<'cx>, hir: &Hir<'cx>) -> NirKind<'cx> {
     match hir.kind() {
+        HirKind::MissingVar(..) => unreachable!("ruled out by typechecking"),
         HirKind::Var(var) => env.lookup_val(*var),
-        HirKind::Import(hir, _) => normalize_hir(env, hir),
+        HirKind::Import(import) => {
+            let typed = env.cx()[import].unwrap_result();
+            normalize_hir(env, &typed.hir)
+        }
+        HirKind::ImportAlternative(alt, left, right) => {
+            let hir = if env.cx()[alt].unwrap_selected() {
+                left
+            } else {
+                right
+            };
+            normalize_hir(env, hir)
+        }
         HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             NirKind::LamClosure {
@@ -178,9 +188,12 @@ pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
             let val = val.eval(env);
             body.eval(env.insert_value(val, ())).kind().clone()
         }
+        HirKind::Expr(ExprKind::Builtin(b)) => {
+            NirKind::from_builtin_env(*b, env.clone())
+        }
         HirKind::Expr(e) => {
             let e = e.map_ref(|hir| hir.eval(env));
-            normalize_one_layer(e, env)
+            normalize_one_layer(e)
         }
     }
 }
diff --git a/dhall/src/semantics/resolve/cache.rs b/dhall/src/semantics/resolve/cache.rs
index b00a2d5..1fc8dd3 100644
--- a/dhall/src/semantics/resolve/cache.rs
+++ b/dhall/src/semantics/resolve/cache.rs
@@ -5,7 +5,7 @@ use std::path::{Path, PathBuf};
 use crate::error::{CacheError, Error};
 use crate::parse::parse_binary;
 use crate::syntax::{binary, Hash};
-use crate::Typed;
+use crate::{Ctxt, Typed};
 use std::ffi::OsStr;
 use std::fs::File;
 
@@ -52,9 +52,13 @@ impl Cache {
         self.cache_dir.join(filename_for_hash(hash))
     }
 
-    pub fn get(&self, hash: &Hash) -> Result<Typed, Error> {
+    pub fn get<'cx>(
+        &self,
+        cx: Ctxt<'cx>,
+        hash: &Hash,
+    ) -> Result<Typed<'cx>, Error> {
         let path = self.entry_path(hash);
-        let res = read_cache_file(&path, hash);
+        let res = read_cache_file(cx, &path, hash);
         if res.is_err() && path.exists() {
             // Delete cache file since it's invalid. We ignore the error.
             let _ = std::fs::remove_file(&path);
@@ -62,14 +66,23 @@ impl Cache {
         res
     }
 
-    pub fn insert(&self, hash: &Hash, expr: &Typed) -> Result<(), Error> {
+    pub fn insert<'cx>(
+        &self,
+        cx: Ctxt<'cx>,
+        hash: &Hash,
+        expr: &Typed<'cx>,
+    ) -> Result<(), Error> {
         let path = self.entry_path(hash);
-        write_cache_file(&path, expr)
+        write_cache_file(cx, &path, expr)
     }
 }
 
 /// Read a file from the cache, also checking that its hash is valid.
-fn read_cache_file(path: &Path, hash: &Hash) -> Result<Typed, Error> {
+fn read_cache_file<'cx>(
+    cx: Ctxt<'cx>,
+    path: &Path,
+    hash: &Hash,
+) -> Result<Typed<'cx>, Error> {
     let data = crate::utils::read_binary_file(path)?;
 
     match hash {
@@ -81,12 +94,16 @@ fn read_cache_file(path: &Path, hash: &Hash) -> Result<Typed, Error> {
         }
     }
 
-    Ok(parse_binary(&data)?.skip_resolve()?.typecheck()?)
+    Ok(parse_binary(&data)?.resolve(cx)?.typecheck(cx)?)
 }
 
 /// Write a file to the cache.
-fn write_cache_file(path: &Path, expr: &Typed) -> Result<(), Error> {
-    let data = binary::encode(&expr.to_expr())?;
+fn write_cache_file<'cx>(
+    cx: Ctxt<'cx>,
+    path: &Path,
+    expr: &Typed<'cx>,
+) -> Result<(), Error> {
+    let data = binary::encode(&expr.to_expr(cx))?;
     File::create(path)?.write_all(data.as_slice())?;
     Ok(())
 }
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
index 29dd16b..bde99d1 100644
--- a/dhall/src/semantics/resolve/env.rs
+++ b/dhall/src/semantics/resolve/env.rs
@@ -1,9 +1,9 @@
 use std::collections::HashMap;
 
 use crate::error::{Error, ImportError};
-use crate::semantics::{AlphaVar, Cache, ImportLocation, VarEnv};
+use crate::semantics::{check_hash, AlphaVar, Cache, ImportLocation, VarEnv};
 use crate::syntax::{Hash, Label, V};
-use crate::Typed;
+use crate::{Ctxt, ImportId, ImportResultId, Typed};
 
 /// Environment for resolving names.
 #[derive(Debug, Clone, Default)]
@@ -11,14 +11,13 @@ pub struct NameEnv {
     names: Vec<Label>,
 }
 
-pub type MemCache = HashMap<ImportLocation, Typed>;
 pub type CyclesStack = Vec<ImportLocation>;
 
 /// Environment for resolving imports
-#[derive(Debug)]
-pub struct ImportEnv {
-    disk_cache: Option<Cache>, // Missing if it failed to initialize
-    mem_cache: MemCache,
+pub struct ImportEnv<'cx> {
+    cx: Ctxt<'cx>,
+    disk_cache: Option<Cache>, // `None` if it failed to initialize
+    mem_cache: HashMap<ImportLocation, ImportResultId<'cx>>,
     stack: CyclesStack,
 }
 
@@ -66,43 +65,61 @@ impl NameEnv {
     }
 }
 
-impl ImportEnv {
-    pub fn new() -> Self {
+impl<'cx> ImportEnv<'cx> {
+    pub fn new(cx: Ctxt<'cx>) -> Self {
         ImportEnv {
+            cx,
             disk_cache: Cache::new().ok(),
             mem_cache: Default::default(),
             stack: Default::default(),
         }
     }
 
+    pub fn cx(&self) -> Ctxt<'cx> {
+        self.cx
+    }
+
     pub fn get_from_mem_cache(
-        &mut self,
+        &self,
         location: &ImportLocation,
-    ) -> Option<Typed> {
-        Some(self.mem_cache.get(location)?.clone())
+    ) -> Option<ImportResultId<'cx>> {
+        Some(*self.mem_cache.get(location)?)
     }
 
     pub fn get_from_disk_cache(
-        &mut self,
+        &self,
         hash: &Option<Hash>,
-    ) -> Option<Typed> {
+    ) -> Option<Typed<'cx>> {
         let hash = hash.as_ref()?;
-        let expr = self.disk_cache.as_ref()?.get(hash).ok()?;
+        let expr = self.disk_cache.as_ref()?.get(self.cx(), hash).ok()?;
         Some(expr)
     }
 
+    pub fn check_hash(
+        &self,
+        import: ImportId<'cx>,
+        result: ImportResultId<'cx>,
+    ) -> Result<(), Error> {
+        check_hash(self.cx(), import, result)
+    }
+
     pub fn write_to_mem_cache(
         &mut self,
         location: ImportLocation,
-        expr: Typed,
+        result: ImportResultId<'cx>,
     ) {
-        self.mem_cache.insert(location, expr);
+        self.mem_cache.insert(location, result);
     }
 
-    pub fn write_to_disk_cache(&mut self, hash: &Option<Hash>, expr: &Typed) {
+    pub fn write_to_disk_cache(
+        &self,
+        hash: &Option<Hash>,
+        result: ImportResultId<'cx>,
+    ) {
         if let Some(disk_cache) = self.disk_cache.as_ref() {
             if let Some(hash) = hash {
-                let _ = disk_cache.insert(hash, &expr);
+                let expr = &self.cx()[result];
+                let _ = disk_cache.insert(self.cx(), hash, expr);
             }
         }
     }
@@ -110,8 +127,8 @@ impl ImportEnv {
     pub fn with_cycle_detection(
         &mut self,
         location: ImportLocation,
-        do_resolve: impl FnOnce(&mut Self) -> Result<Typed, Error>,
-    ) -> Result<Typed, Error> {
+        do_resolve: impl FnOnce(&mut Self) -> Result<Typed<'cx>, Error>,
+    ) -> Result<Typed<'cx>, Error> {
         if self.stack.contains(&location) {
             return Err(
                 ImportError::ImportCycle(self.stack.clone(), location).into()
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 8869915..8baad10 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,7 +1,7 @@
 use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
+use crate::semantics::{type_with, typecheck, NameEnv, Nir, NzEnv, Tir, TyEnv};
 use crate::syntax::{Expr, ExprKind, Span, V};
-use crate::ToExprOptions;
+use crate::{Ctxt, ImportAlternativeId, ImportId, ToExprOptions};
 
 /// Stores an alpha-normalized variable.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -10,19 +10,23 @@ pub struct AlphaVar {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub enum HirKind {
+pub enum HirKind<'cx> {
     /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
-    /// Result of resolving an import.
-    Import(Hir, Type),
+    /// A variable that couldn't be resolved. Detected during resolution, but causes an error during typeck.
+    MissingVar(V),
+    /// An import. It must have been resolved after resolution.
+    Import(ImportId<'cx>),
+    /// An import alternative. It must have been decided after resolution.
+    ImportAlternative(ImportAlternativeId<'cx>, Hir<'cx>, Hir<'cx>),
     // Forbidden ExprKind variants: Var, Import, Completion
-    Expr(ExprKind<Hir>),
+    Expr(ExprKind<Hir<'cx>>),
 }
 
 // An expression with resolved variables and imports.
 #[derive(Debug, Clone)]
-pub struct Hir {
-    kind: Box<HirKind>,
+pub struct Hir<'cx> {
+    kind: Box<HirKind<'cx>>,
     span: Span,
 }
 
@@ -35,15 +39,15 @@ impl AlphaVar {
     }
 }
 
-impl Hir {
-    pub fn new(kind: HirKind, span: Span) -> Self {
+impl<'cx> Hir<'cx> {
+    pub fn new(kind: HirKind<'cx>, span: Span) -> Self {
         Hir {
             kind: Box::new(kind),
             span,
         }
     }
 
-    pub fn kind(&self) -> &HirKind {
+    pub fn kind(&self) -> &HirKind<'cx> {
         &*self.kind
     }
     pub fn span(&self) -> Span {
@@ -51,59 +55,78 @@ impl Hir {
     }
 
     /// Converts a closed Hir expr back to the corresponding AST expression.
-    pub fn to_expr(&self, opts: ToExprOptions) -> Expr {
-        hir_to_expr(self, opts, &mut NameEnv::new())
+    pub fn to_expr(&self, cx: Ctxt<'cx>, opts: ToExprOptions) -> Expr {
+        hir_to_expr(cx, self, opts, &mut NameEnv::new())
     }
     /// Converts a closed Hir expr back to the corresponding AST expression.
-    pub fn to_expr_noopts(&self) -> Expr {
+    pub fn to_expr_noopts(&self, cx: Ctxt<'cx>) -> Expr {
         let opts = ToExprOptions { alpha: false };
-        self.to_expr(opts)
+        self.to_expr(cx, opts)
     }
-    pub fn to_expr_alpha(&self) -> Expr {
+    pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr {
         let opts = ToExprOptions { alpha: true };
-        self.to_expr(opts)
+        self.to_expr(cx, opts)
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
         let opts = ToExprOptions { alpha: false };
+        let cx = env.cx();
         let mut env = env.as_nameenv().clone();
-        hir_to_expr(self, opts, &mut env)
+        hir_to_expr(cx, self, opts, &mut env)
     }
 
     /// Typecheck the Hir.
     pub fn typecheck<'hir>(
         &'hir self,
-        env: &TyEnv,
-    ) -> Result<Tir<'hir>, TypeError> {
+        env: &TyEnv<'cx>,
+    ) -> Result<Tir<'cx, 'hir>, TypeError> {
         type_with(env, self, None)
     }
-    pub fn typecheck_noenv<'hir>(&'hir self) -> Result<Tir<'hir>, TypeError> {
-        self.typecheck(&TyEnv::new())
+    pub fn typecheck_noenv<'hir>(
+        &'hir self,
+        cx: Ctxt<'cx>,
+    ) -> Result<Tir<'cx, 'hir>, TypeError> {
+        typecheck(cx, self)
     }
 
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+    pub fn eval(&self, env: impl Into<NzEnv<'cx>>) -> Nir<'cx> {
         Nir::new_thunk(env.into(), self.clone())
     }
     /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
-    pub fn eval_closed_expr(&self) -> Nir {
-        self.eval(NzEnv::new())
+    pub fn eval_closed_expr(&self, cx: Ctxt<'cx>) -> Nir<'cx> {
+        self.eval(NzEnv::new(cx))
     }
 }
 
-fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
+fn hir_to_expr<'cx>(
+    cx: Ctxt<'cx>,
+    hir: &Hir<'cx>,
+    opts: ToExprOptions,
+    env: &mut NameEnv,
+) -> Expr {
     let kind = match hir.kind() {
         HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
         HirKind::Var(v) => ExprKind::Var(env.label_var(*v)),
-        HirKind::Import(hir, _) => {
-            return hir_to_expr(hir, opts, &mut NameEnv::new())
+        HirKind::MissingVar(v) => ExprKind::Var(v.clone()),
+        HirKind::Import(import) => {
+            let typed = cx[import].unwrap_result();
+            return hir_to_expr(cx, &typed.hir, opts, &mut NameEnv::new());
+        }
+        HirKind::ImportAlternative(alt, left, right) => {
+            let hir = if cx[alt].unwrap_selected() {
+                left
+            } else {
+                right
+            };
+            return hir_to_expr(cx, hir, opts, env);
         }
         HirKind::Expr(e) => {
             let e = e.map_ref_maybe_binder(|l, hir| {
                 if let Some(l) = l {
                     env.insert_mut(l);
                 }
-                let e = hir_to_expr(hir, opts, env);
+                let e = hir_to_expr(cx, hir, opts, env);
                 if l.is_some() {
                     env.remove_mut();
                 }
@@ -124,9 +147,9 @@ fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
     Expr::new(kind, hir.span())
 }
 
-impl std::cmp::PartialEq for Hir {
+impl<'cx> std::cmp::PartialEq for Hir<'cx> {
     fn eq(&self, other: &Self) -> bool {
         self.kind == other.kind
     }
 }
-impl std::cmp::Eq for Hir {}
+impl<'cx> std::cmp::Eq for Hir<'cx> {}
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 16987de..116e1a5 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -15,7 +15,10 @@ use crate::syntax::{
     Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span,
     UnspannedExpr, URL,
 };
-use crate::{Parsed, Resolved, Typed};
+use crate::{
+    Ctxt, ImportAlternativeId, ImportId, ImportResultId, Parsed, Resolved,
+    Typed,
+};
 
 // TODO: evaluate import headers
 pub type Import = syntax::Import<()>;
@@ -29,8 +32,10 @@ enum ImportLocationKind {
     Remote(Url),
     /// Environment variable
     Env(String),
-    /// Data without a location
+    /// Data without a location; chaining will start from current directory.
     Missing,
+    /// Token to signal that thi sfile should contain no imports.
+    NoImport,
 }
 
 /// The location of some data.
@@ -101,6 +106,7 @@ impl ImportLocationKind {
                 url = url.join(&path.file_path.join("/"))?;
                 ImportLocationKind::Remote(url)
             }
+            ImportLocationKind::NoImport => unreachable!(),
         })
     }
 
@@ -120,6 +126,7 @@ impl ImportLocationKind {
             ImportLocationKind::Missing => {
                 return Err(ImportError::Missing.into())
             }
+            ImportLocationKind::NoImport => unreachable!(),
         })
     }
 
@@ -134,6 +141,7 @@ impl ImportLocationKind {
             ImportLocationKind::Missing => {
                 return Err(ImportError::Missing.into())
             }
+            ImportLocationKind::NoImport => unreachable!(),
         })
     }
 
@@ -149,6 +157,7 @@ impl ImportLocationKind {
                 ("Environment", Some(name.clone()))
             }
             ImportLocationKind::Missing => ("Missing", None),
+            ImportLocationKind::NoImport => unreachable!(),
         };
 
         let asloc_ty = make_aslocation_uniontype();
@@ -171,6 +180,12 @@ impl ImportLocation {
             mode: ImportMode::Code,
         }
     }
+    pub fn dhall_code_without_imports() -> Self {
+        ImportLocation {
+            kind: ImportLocationKind::NoImport,
+            mode: ImportMode::Code,
+        }
+    }
     pub fn local_dhall_code(path: PathBuf) -> Self {
         ImportLocation {
             kind: ImportLocationKind::Local(path),
@@ -191,6 +206,10 @@ impl ImportLocation {
     fn chain(&self, import: &Import) -> Result<ImportLocation, Error> {
         // Makes no sense to chain an import if the current file is not a dhall file.
         assert!(matches!(self.mode, ImportMode::Code));
+        if matches!(self.kind, ImportLocationKind::NoImport) {
+            Err(ImportError::UnexpectedImport(import.clone()))?;
+        }
+
         let kind = match &import.location {
             ImportTarget::Local(prefix, path) => {
                 self.kind.chain_local(*prefix, path)?
@@ -227,30 +246,42 @@ impl ImportLocation {
     }
 
     /// Fetches the expression corresponding to this location.
-    fn fetch(&self, env: &mut ImportEnv, span: Span) -> Result<Typed, Error> {
-        let (hir, ty) = match self.mode {
+    fn fetch<'cx>(
+        &self,
+        env: &mut ImportEnv<'cx>,
+        span: Span,
+    ) -> Result<Typed<'cx>, Error> {
+        let cx = env.cx();
+        let typed = match self.mode {
             ImportMode::Code => {
                 let parsed = self.kind.fetch_dhall()?;
-                let typed = resolve_with_env(env, parsed)?.typecheck()?;
-                let hir = typed.normalize().to_hir();
-                (hir, typed.ty)
+                let typed = parsed.resolve_with_env(env)?.typecheck(cx)?;
+                Typed {
+                    // TODO: manage to keep the Nir around. Will need fixing variables.
+                    hir: typed.normalize(cx).to_hir(),
+                    ty: typed.ty,
+                }
             }
             ImportMode::RawText => {
                 let text = self.kind.fetch_text()?;
-                let hir = Hir::new(
-                    HirKind::Expr(ExprKind::TextLit(text.into())),
-                    span,
-                );
-                (hir, Type::from_builtin(Builtin::Text))
+                Typed {
+                    hir: Hir::new(
+                        HirKind::Expr(ExprKind::TextLit(text.into())),
+                        span,
+                    ),
+                    ty: Type::from_builtin(cx, Builtin::Text),
+                }
             }
             ImportMode::Location => {
                 let expr = self.kind.to_location();
-                let hir = skip_resolve_expr(&expr)?;
-                let ty = hir.typecheck_noenv()?.ty().clone();
-                (hir, ty)
+                Parsed::from_expr_without_imports(expr)
+                    .resolve(cx)
+                    .unwrap()
+                    .typecheck(cx)
+                    .unwrap()
             }
         };
-        Ok(Typed { hir, ty })
+        Ok(typed)
     }
 }
 
@@ -282,15 +313,21 @@ fn make_aslocation_uniontype() -> Expr {
     mkexpr(ExprKind::UnionType(union))
 }
 
-fn check_hash(import: &Import, typed: &Typed, span: Span) -> Result<(), Error> {
+pub fn check_hash<'cx>(
+    cx: Ctxt<'cx>,
+    import: ImportId<'cx>,
+    result: ImportResultId<'cx>,
+) -> Result<(), Error> {
+    let import = &cx[import];
     if let (ImportMode::Code, Some(Hash::SHA256(hash))) =
-        (import.mode, &import.hash)
+        (import.import.mode, &import.import.hash)
     {
-        let actual_hash = typed.hir.to_expr_alpha().sha256_hash()?;
+        let expr = cx[result].hir.to_expr_alpha(cx);
+        let actual_hash = expr.sha256_hash()?;
         if hash[..] != actual_hash[..] {
             mkerr(
                 ErrorBuilder::new("hash mismatch")
-                    .span_err(span, "hash mismatch")
+                    .span_err(import.span.clone(), "hash mismatch")
                     .note(format!("Expected sha256:{}", hex::encode(hash)))
                     .note(format!(
                         "Found    sha256:{}",
@@ -332,127 +369,204 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
     }
 }
 
-/// Traverse the expression, handling import alternatives and passing
-/// found imports to the provided function. Also resolving names.
-fn traverse_resolve_expr(
+/// Fetch the import and store the result in the global context.
+fn fetch_import<'cx>(
+    env: &mut ImportEnv<'cx>,
+    import_id: ImportId<'cx>,
+) -> Result<ImportResultId<'cx>, Error> {
+    let cx = env.cx();
+    let import = &cx[import_id].import;
+    let span = cx[import_id].span.clone();
+    let location = cx[import_id].base_location.chain(import)?;
+
+    // If the import is in the in-memory cache, or the hash is in the on-disk cache, return
+    // the cached contents.
+    if let Some(res_id) = env.get_from_mem_cache(&location) {
+        // The same location may be used with different or no hashes. Thus we need to check
+        // the hashes every time.
+        env.check_hash(import_id, res_id)?;
+        env.write_to_disk_cache(&import.hash, res_id);
+        return Ok(res_id);
+    }
+    if let Some(typed) = env.get_from_disk_cache(&import.hash) {
+        // No need to check the hash, it was checked before reading the file.
+        // We also don't write to the in-memory cache, because the location might be completely
+        // unrelated to the cached file (e.g. `missing sha256:...` is valid).
+        // This actually means that importing many times a same hashed import will take
+        // longer than importing many times a same non-hashed import.
+        let res_id = cx.push_import_result(typed);
+        return Ok(res_id);
+    }
+
+    // Resolve this import, making sure that recursive imports don't cycle back to the
+    // current one.
+    let res = env.with_cycle_detection(location.clone(), |env| {
+        location.fetch(env, span.clone())
+    });
+    let typed = match res {
+        Ok(typed) => typed,
+        Err(e) => mkerr(
+            ErrorBuilder::new("error")
+                .span_err(span.clone(), e.to_string())
+                .format(),
+        )?,
+    };
+
+    // Add the resolved import to the caches
+    let res_id = cx.push_import_result(typed);
+    env.check_hash(import_id, res_id)?;
+    env.write_to_disk_cache(&import.hash, res_id);
+    // Cache the mapping from this location to the result.
+    env.write_to_mem_cache(location, res_id);
+
+    Ok(res_id)
+}
+
+/// Part of a tree of imports.
+#[derive(Debug, Clone, Copy)]
+pub enum ImportNode<'cx> {
+    Import(ImportId<'cx>),
+    Alternative(ImportAlternativeId<'cx>),
+}
+
+/// Traverse the expression and replace each import and import alternative by an id into the global
+/// context. The ids are also accumulated into `nodes` so that we can resolve them afterwards.
+fn traverse_accumulate<'cx>(
+    env: &mut ImportEnv<'cx>,
     name_env: &mut NameEnv,
+    nodes: &mut Vec<ImportNode<'cx>>,
+    base_location: &ImportLocation,
     expr: &Expr,
-    f: &mut impl FnMut(Import, Span) -> Result<Typed, Error>,
-) -> Result<Hir, Error> {
+) -> Hir<'cx> {
+    let cx = env.cx();
     let expr = desugar(expr);
-    Ok(match expr.kind() {
+    let kind = match expr.kind() {
         ExprKind::Var(var) => match name_env.unlabel_var(&var) {
-            Some(v) => Hir::new(HirKind::Var(v), expr.span()),
-            None => mkerr(
-                ErrorBuilder::new(format!("unbound variable `{}`", var))
-                    .span_err(expr.span(), "not found in this scope")
-                    .format(),
-            )?,
+            Some(v) => HirKind::Var(v),
+            None => HirKind::MissingVar(var.clone()),
         },
         ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => {
-            match traverse_resolve_expr(name_env, l, f) {
-                Ok(l) => l,
-                Err(_) => {
-                    match traverse_resolve_expr(name_env, r, f) {
-                        Ok(r) => r,
-                        // TODO: keep track of the other error too
-                        Err(e) => return Err(e),
-                    }
-                }
-            }
+            let mut imports_l = Vec::new();
+            let l = traverse_accumulate(
+                env,
+                name_env,
+                &mut imports_l,
+                base_location,
+                l,
+            );
+            let mut imports_r = Vec::new();
+            let r = traverse_accumulate(
+                env,
+                name_env,
+                &mut imports_r,
+                base_location,
+                r,
+            );
+            let alt =
+                cx.push_import_alternative(imports_l.into(), imports_r.into());
+            nodes.push(ImportNode::Alternative(alt));
+            HirKind::ImportAlternative(alt, l, r)
         }
         kind => {
-            let kind = kind.traverse_ref_maybe_binder(|l, e| {
+            let kind = kind.map_ref_maybe_binder(|l, e| {
                 if let Some(l) = l {
                     name_env.insert_mut(l);
                 }
-                let hir = traverse_resolve_expr(name_env, e, f)?;
+                let hir =
+                    traverse_accumulate(env, name_env, nodes, base_location, e);
                 if l.is_some() {
                     name_env.remove_mut();
                 }
-                Ok::<_, Error>(hir)
-            })?;
-            let kind = match kind {
+                hir
+            });
+            match kind {
                 ExprKind::Import(import) => {
                     // TODO: evaluate import headers
-                    let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
-                    let imported = f(import, expr.span())?;
-                    HirKind::Import(imported.hir, imported.ty)
+                    let import = import.map_ref(|_| ());
+                    let import_id = cx.push_import(
+                        base_location.clone(),
+                        import,
+                        expr.span(),
+                    );
+                    nodes.push(ImportNode::Import(import_id));
+                    HirKind::Import(import_id)
                 }
                 kind => HirKind::Expr(kind),
-            };
-            Hir::new(kind, expr.span())
+            }
         }
-    })
+    };
+    Hir::new(kind, expr.span())
 }
 
-fn resolve_with_env(
-    env: &mut ImportEnv,
+/// Take a list of nodes and recursively resolve them.
+fn resolve_nodes<'cx>(
+    env: &mut ImportEnv<'cx>,
+    nodes: &[ImportNode<'cx>],
+) -> Result<(), Error> {
+    for &node in nodes {
+        match node {
+            ImportNode::Import(import) => {
+                let res_id = fetch_import(env, import)?;
+                env.cx()[import].set_resultid(res_id);
+            }
+            ImportNode::Alternative(alt) => {
+                let alt = &env.cx()[alt];
+                if resolve_nodes(env, &alt.left_imports).is_ok() {
+                    alt.set_selected(true);
+                } else {
+                    resolve_nodes(env, &alt.right_imports)?;
+                    alt.set_selected(false);
+                }
+            }
+        }
+    }
+    Ok(())
+}
+
+fn resolve_with_env<'cx>(
+    env: &mut ImportEnv<'cx>,
     parsed: Parsed,
-) -> Result<Resolved, Error> {
+) -> Result<Resolved<'cx>, Error> {
     let Parsed(expr, base_location) = parsed;
-    let resolved = traverse_resolve_expr(
+    let mut nodes = Vec::new();
+    // First we collect all imports.
+    let resolved = traverse_accumulate(
+        env,
         &mut NameEnv::new(),
+        &mut nodes,
+        &base_location,
         &expr,
-        &mut |import, span| {
-            let location = base_location.chain(&import)?;
-
-            // If the import is in the in-memory cache, or the hash is in the on-disk cache, return
-            // the cached contents.
-            if let Some(typed) = env.get_from_mem_cache(&location) {
-                // The same location may be used with different or no hashes. Thus we need to check
-                // the hashes every time.
-                check_hash(&import, &typed, span)?;
-                env.write_to_disk_cache(&import.hash, &typed);
-                return Ok(typed);
-            }
-            if let Some(typed) = env.get_from_disk_cache(&import.hash) {
-                // No need to check the hash, it was checked before reading the file. We also don't
-                // write to the in-memory cache, because the location might be completely unrelated
-                // to the cached file (e.g. `missing sha256:...` is valid).
-                // This actually means that importing many times a same hashed import will take
-                // longer than importing many times a same non-hashed import.
-                return Ok(typed);
-            }
-
-            // Resolve this import, making sure that recursive imports don't cycle back to the
-            // current one.
-            let res = env.with_cycle_detection(location.clone(), |env| {
-                location.fetch(env, span.clone())
-            });
-            let typed = match res {
-                Ok(typed) => typed,
-                Err(e) => mkerr(
-                    ErrorBuilder::new("error")
-                        .span_err(span.clone(), e.to_string())
-                        .format(),
-                )?,
-            };
-
-            // Add the resolved import to the caches
-            check_hash(&import, &typed, span)?;
-            env.write_to_disk_cache(&import.hash, &typed);
-            env.write_to_mem_cache(location, typed.clone());
-            Ok(typed)
-        },
-    )?;
+    );
+    // Then we resolve them and choose sides for the alternatives.
+    resolve_nodes(env, &nodes)?;
     Ok(Resolved(resolved))
 }
 
-pub fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
-    resolve_with_env(&mut ImportEnv::new(), parsed)
+/// Resolves all imports and names. Returns errors if importing failed. Name errors are deferred to
+/// typechecking.
+pub fn resolve<'cx>(
+    cx: Ctxt<'cx>,
+    parsed: Parsed,
+) -> Result<Resolved<'cx>, Error> {
+    parsed.resolve_with_env(&mut ImportEnv::new(cx))
 }
 
-pub fn skip_resolve_expr(expr: &Expr) -> Result<Hir, Error> {
-    traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import, _span| {
-        Err(ImportError::UnexpectedImport(import).into())
-    })
+/// Resolves names, and errors if we find any imports.
+pub fn skip_resolve<'cx>(
+    cx: Ctxt<'cx>,
+    parsed: Parsed,
+) -> Result<Resolved<'cx>, Error> {
+    let parsed = Parsed::from_expr_without_imports(parsed.0);
+    Ok(resolve(cx, parsed)?)
 }
 
-pub fn skip_resolve(parsed: Parsed) -> Result<Resolved, Error> {
-    let Parsed(expr, _) = parsed;
-    let resolved = skip_resolve_expr(&expr)?;
-    Ok(Resolved(resolved))
+impl Parsed {
+    fn resolve_with_env<'cx>(
+        self,
+        env: &mut ImportEnv<'cx>,
+    ) -> Result<Resolved<'cx>, Error> {
+        resolve_with_env(env, self)
+    }
 }
 
 pub trait Canonicalize {
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fa66f0..fdcc62d 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,5 +1,6 @@
 use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
 use crate::syntax::Label;
+use crate::Ctxt;
 
 /// Environment for indexing variables.
 #[derive(Debug, Clone, Copy, Default)]
@@ -9,9 +10,10 @@ pub struct VarEnv {
 
 /// Environment for typing expressions.
 #[derive(Debug, Clone)]
-pub struct TyEnv {
+pub struct TyEnv<'cx> {
+    cx: Ctxt<'cx>,
     names: NameEnv,
-    items: ValEnv<Type>,
+    items: ValEnv<'cx, Type<'cx>>,
 }
 
 impl VarEnv {
@@ -38,42 +40,48 @@ impl VarEnv {
     }
 }
 
-impl TyEnv {
-    pub fn new() -> Self {
+impl<'cx> TyEnv<'cx> {
+    pub fn new(cx: Ctxt<'cx>) -> Self {
         TyEnv {
+            cx,
             names: NameEnv::new(),
-            items: ValEnv::new(),
+            items: ValEnv::new(cx),
         }
     }
+    pub fn cx(&self) -> Ctxt<'cx> {
+        self.cx
+    }
     pub fn as_varenv(&self) -> VarEnv {
         self.names.as_varenv()
     }
-    pub fn to_nzenv(&self) -> NzEnv {
+    pub fn to_nzenv(&self) -> NzEnv<'cx> {
         self.items.discard_types()
     }
     pub fn as_nameenv(&self) -> &NameEnv {
         &self.names
     }
 
-    pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
+    pub fn insert_type(&self, x: &Label, ty: Type<'cx>) -> Self {
         TyEnv {
+            cx: self.cx,
             names: self.names.insert(x),
             items: self.items.insert_type(ty),
         }
     }
-    pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
+    pub fn insert_value(&self, x: &Label, e: Nir<'cx>, ty: Type<'cx>) -> Self {
         TyEnv {
+            cx: self.cx,
             names: self.names.insert(x),
             items: self.items.insert_value(e, ty),
         }
     }
-    pub fn lookup(&self, var: AlphaVar) -> Type {
+    pub fn lookup(&self, var: AlphaVar) -> Type<'cx> {
         self.items.lookup_ty(var)
     }
 }
 
-impl<'a> From<&'a TyEnv> for NzEnv {
-    fn from(x: &'a TyEnv) -> Self {
+impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv<'cx> {
+    fn from(x: &'a TyEnv<'cx>) -> Self {
         x.to_nzenv()
     }
 }
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index f34802c..7b04f57 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -2,6 +2,7 @@ use crate::builtins::Builtin;
 use crate::error::{ErrorBuilder, TypeError};
 use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
 use crate::syntax::{Const, Expr, Span};
+use crate::Ctxt;
 
 /// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
 #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
@@ -9,17 +10,17 @@ pub struct Universe(u8);
 
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Type {
-    val: Nir,
+pub struct Type<'cx> {
+    val: Nir<'cx>,
     univ: Universe,
 }
 
 /// A hir expression plus its inferred type.
 /// Stands for "Typed intermediate representation"
 #[derive(Debug, Clone)]
-pub struct Tir<'hir> {
-    hir: &'hir Hir,
-    ty: Type,
+pub struct Tir<'cx, 'hir> {
+    hir: &'hir Hir<'cx>,
+    ty: Type<'cx>,
 }
 
 impl Universe {
@@ -43,16 +44,16 @@ impl Universe {
     }
 }
 
-impl Type {
-    pub fn new(val: Nir, univ: Universe) -> Self {
+impl<'cx> Type<'cx> {
+    pub fn new(val: Nir<'cx>, univ: Universe) -> Self {
         Type { val, univ }
     }
     /// Creates a new Type and infers its universe by re-typechecking its value.
     /// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
     /// PiClosure.
     pub fn new_infer_universe(
-        env: &TyEnv,
-        val: Nir,
+        env: &TyEnv<'cx>,
+        val: Nir<'cx>,
     ) -> Result<Self, TypeError> {
         let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
         let u = match c {
@@ -67,14 +68,14 @@ impl Type {
     pub fn from_const(c: Const) -> Self {
         Self::new(Nir::from_const(c), c.to_universe().next())
     }
-    pub fn from_builtin(b: Builtin) -> Self {
+    pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
         use Builtin::*;
         match b {
             Bool | Natural | Integer | Double | Text => {}
             _ => unreachable!("this builtin is not a type: {}", b),
         }
 
-        Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
+        Self::new(Nir::from_builtin(cx, b), Universe::from_const(Const::Type))
     }
 
     /// Get the type of this type
@@ -82,60 +83,60 @@ impl Type {
         self.univ
     }
 
-    pub fn to_nir(&self) -> Nir {
+    pub fn to_nir(&self) -> Nir<'cx> {
         self.val.clone()
     }
-    pub fn as_nir(&self) -> &Nir {
+    pub fn as_nir(&self) -> &Nir<'cx> {
         &self.val
     }
-    pub fn into_nir(self) -> Nir {
+    pub fn into_nir(self) -> Nir<'cx> {
         self.val
     }
     pub fn as_const(&self) -> Option<Const> {
         self.val.as_const()
     }
-    pub fn kind(&self) -> &NirKind {
+    pub fn kind(&self) -> &NirKind<'cx> {
         self.val.kind()
     }
 
-    pub fn to_hir(&self, venv: VarEnv) -> Hir {
+    pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
         self.val.to_hir(venv)
     }
-    pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr {
         self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
     }
 }
 
-impl<'hir> Tir<'hir> {
-    pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+impl<'cx, 'hir> Tir<'cx, 'hir> {
+    pub fn from_hir(hir: &'hir Hir<'cx>, ty: Type<'cx>) -> Self {
         Tir { hir, ty }
     }
 
     pub fn span(&self) -> Span {
         self.as_hir().span()
     }
-    pub fn ty(&self) -> &Type {
+    pub fn ty(&self) -> &Type<'cx> {
         &self.ty
     }
-    pub fn into_ty(self) -> Type {
+    pub fn into_ty(self) -> Type<'cx> {
         self.ty
     }
 
-    pub fn to_hir(&self) -> Hir {
+    pub fn to_hir(&self) -> Hir<'cx> {
         self.as_hir().clone()
     }
-    pub fn as_hir(&self) -> &Hir {
-        &self.hir
+    pub fn as_hir(&self) -> &'hir Hir<'cx> {
+        self.hir
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+    pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
         self.as_hir().to_expr_tyenv(env)
     }
 
     /// Eval the Tir. It will actually get evaluated only as needed on demand.
-    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+    pub fn eval(&self, env: impl Into<NzEnv<'cx>>) -> Nir<'cx> {
         self.as_hir().eval(env.into())
     }
-    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+    pub fn ensure_is_type(&self, env: &TyEnv<'cx>) -> Result<(), TypeError> {
         if self.ty().as_const().is_none() {
             return mkerr(
                 ErrorBuilder::new(format!(
@@ -159,7 +160,10 @@ impl<'hir> Tir<'hir> {
         Ok(())
     }
     /// Evaluate to a Type.
-    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+    pub fn eval_to_type(
+        &self,
+        env: &TyEnv<'cx>,
+    ) -> Result<Type<'cx>, TypeError> {
         self.ensure_is_type(env)?;
         Ok(Type::new(
             self.eval(env),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 498bd76..23c2bd2 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,6 +5,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::operations::typecheck_operation;
 use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
 use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
+use crate::Ctxt;
 
 fn function_check(a: Const, b: Const) -> Const {
     if b == Const::Type {
@@ -28,11 +29,12 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 
 /// When all sub-expressions have been typed, check the remaining toplevel
 /// layer.
-fn type_one_layer(
-    env: &TyEnv,
-    ekind: ExprKind<Tir<'_>>,
+fn type_one_layer<'cx>(
+    env: &TyEnv<'cx>,
+    ekind: ExprKind<Tir<'cx, '_>>,
     span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<Type<'cx>, TypeError> {
+    let cx = env.cx();
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     Ok(match ekind {
@@ -50,18 +52,21 @@ fn type_one_layer(
 
         ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
-        ExprKind::Num(num) => Type::from_builtin(match num {
-            NumKind::Bool(_) => Builtin::Bool,
-            NumKind::Natural(_) => Builtin::Natural,
-            NumKind::Integer(_) => Builtin::Integer,
-            NumKind::Double(_) => Builtin::Double,
-        }),
+        ExprKind::Num(num) => Type::from_builtin(
+            cx,
+            match num {
+                NumKind::Bool(_) => Builtin::Bool,
+                NumKind::Natural(_) => Builtin::Natural,
+                NumKind::Integer(_) => Builtin::Integer,
+                NumKind::Double(_) => Builtin::Double,
+            },
+        ),
         ExprKind::Builtin(b) => {
-            let t_hir = type_of_builtin(b);
-            typecheck(&t_hir)?.eval_to_type(env)?
+            let t_hir = type_of_builtin(cx, b);
+            typecheck(cx, &t_hir)?.eval_to_type(env)?
         }
         ExprKind::TextLit(interpolated) => {
-            let text_type = Type::from_builtin(Builtin::Text);
+            let text_type = Type::from_builtin(cx, Builtin::Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -78,7 +83,7 @@ fn type_one_layer(
             }
 
             let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::Optional)
+            Nir::from_builtin(cx, Builtin::Optional)
                 .app(t)
                 .to_type(Const::Type)
         }
@@ -103,7 +108,9 @@ fn type_one_layer(
             }
 
             let t = x.ty().to_nir();
-            Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
+            Nir::from_builtin(cx, Builtin::List)
+                .app(t)
+                .to_type(Const::Type)
         }
         ExprKind::RecordLit(kvs) => {
             // An empty record type has type Type
@@ -170,14 +177,30 @@ fn type_one_layer(
 /// to compare with.
 // We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use
 // it to handle the annotations in merge/toMap/etc. uniformly.
-pub fn type_with<'hir>(
-    env: &TyEnv,
-    hir: &'hir Hir,
-    annot: Option<Type>,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn type_with<'cx, 'hir>(
+    env: &TyEnv<'cx>,
+    hir: &'hir Hir<'cx>,
+    annot: Option<Type<'cx>>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
     let tir = match hir.kind() {
         HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)),
-        HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
+        HirKind::MissingVar(var) => mkerr(
+            ErrorBuilder::new(format!("unbound variable `{}`", var))
+                .span_err(hir.span(), "not found in this scope")
+                .format(),
+        )?,
+        HirKind::Import(import) => {
+            let typed = env.cx()[import].unwrap_result();
+            Tir::from_hir(hir, typed.ty.clone())
+        }
+        HirKind::ImportAlternative(alt, left, right) => {
+            let hir = if env.cx()[alt].unwrap_selected() {
+                left
+            } else {
+                right
+            };
+            return type_with(env, hir, annot);
+        }
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
@@ -267,15 +290,19 @@ pub fn type_with<'hir>(
 
 /// Typecheck an expression and return the expression annotated with its type if type-checking
 /// succeeded, or an error if type-checking failed.
-pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
-    type_with(&TyEnv::new(), hir, None)
+pub fn typecheck<'cx, 'hir>(
+    cx: Ctxt<'cx>,
+    hir: &'hir Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
+    type_with(&TyEnv::new(cx), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub fn typecheck_with<'hir>(
-    hir: &'hir Hir,
-    ty: &Hir,
-) -> Result<Tir<'hir>, TypeError> {
-    let ty = typecheck(ty)?.eval_to_type(&TyEnv::new())?;
-    type_with(&TyEnv::new(), hir, Some(ty))
+pub fn typecheck_with<'cx, 'hir>(
+    cx: Ctxt<'cx>,
+    hir: &'hir Hir<'cx>,
+    ty: &Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
+    let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?;
+    type_with(&TyEnv::new(cx), hir, Some(ty))
 }
diff --git a/dhall/tests/import/success/unit/AlternativeWithWrongVariable1A.dhall b/dhall/tests/import/success/unit/AlternativeWithWrongVariable1A.dhall
new file mode 100644
index 0000000..e6fa8d5
--- /dev/null
+++ b/dhall/tests/import/success/unit/AlternativeWithWrongVariable1A.dhall
@@ -0,0 +1 @@
+\(x: Natural) -> x ? y
diff --git a/dhall/tests/import/success/unit/AlternativeWithWrongVariable1B.dhall b/dhall/tests/import/success/unit/AlternativeWithWrongVariable1B.dhall
new file mode 100644
index 0000000..04a1712
--- /dev/null
+++ b/dhall/tests/import/success/unit/AlternativeWithWrongVariable1B.dhall
@@ -0,0 +1 @@
+λ(x : Natural) → x
diff --git a/dhall/tests/import/success/unit/AlternativeWithWrongVariable2A.dhall b/dhall/tests/import/success/unit/AlternativeWithWrongVariable2A.dhall
new file mode 100644
index 0000000..8089500
--- /dev/null
+++ b/dhall/tests/import/success/unit/AlternativeWithWrongVariable2A.dhall
@@ -0,0 +1 @@
+\(x: Natural) -> (y + missing) ? x
diff --git a/dhall/tests/import/success/unit/AlternativeWithWrongVariable2B.dhall b/dhall/tests/import/success/unit/AlternativeWithWrongVariable2B.dhall
new file mode 100644
index 0000000..04a1712
--- /dev/null
+++ b/dhall/tests/import/success/unit/AlternativeWithWrongVariable2B.dhall
@@ -0,0 +1 @@
+λ(x : Natural) → x
diff --git a/dhall/tests/spec.rs b/dhall/tests/spec.rs
index 646083a..a0fe583 100644
--- a/dhall/tests/spec.rs
+++ b/dhall/tests/spec.rs
@@ -15,7 +15,7 @@ use walkdir::WalkDir;
 use dhall::error::Error as DhallError;
 use dhall::error::ErrorKind;
 use dhall::syntax::{binary, Expr};
-use dhall::{Normalized, Parsed, Resolved, Typed};
+use dhall::{Ctxt, Normalized, Parsed, Resolved, Typed};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 enum FileType {
@@ -108,16 +108,16 @@ impl TestFile {
         })
     }
     /// Parse and resolve the target file
-    pub fn resolve(&self) -> Result<Resolved> {
-        Ok(self.parse()?.resolve()?)
+    pub fn resolve<'cx>(&self, cx: Ctxt<'cx>) -> Result<Resolved<'cx>> {
+        Ok(self.parse()?.resolve(cx)?)
     }
     /// Parse, resolve and tck the target file
-    pub fn typecheck(&self) -> Result<Typed> {
-        Ok(self.resolve()?.typecheck()?)
+    pub fn typecheck<'cx>(&self, cx: Ctxt<'cx>) -> Result<Typed<'cx>> {
+        Ok(self.resolve(cx)?.typecheck(cx)?)
     }
     /// Parse, resolve, tck and normalize the target file
-    pub fn normalize(&self) -> Result<Normalized> {
-        Ok(self.typecheck()?.normalize())
+    pub fn normalize<'cx>(&self, cx: Ctxt<'cx>) -> Result<Normalized<'cx>> {
+        Ok(self.typecheck(cx)?.normalize(cx))
     }
 
     /// If UPDATE_TEST_FILES is `true`, we overwrite the output files with our own output.
@@ -160,8 +160,7 @@ impl TestFile {
     }
 
     /// Check that the provided expression matches the file contents.
-    pub fn compare(&self, expr: impl Into<Expr>) -> Result<()> {
-        let expr = expr.into();
+    pub fn compare(&self, expr: Expr) -> Result<()> {
         if !self.path().is_file() {
             return self.write_expr(expr);
         }
@@ -177,8 +176,7 @@ impl TestFile {
         Ok(())
     }
     /// Check that the provided expression matches the file contents.
-    pub fn compare_debug(&self, expr: impl Into<Expr>) -> Result<()> {
-        let expr = expr.into();
+    pub fn compare_debug(&self, expr: Expr) -> Result<()> {
         if !self.path().is_file() {
             return self.write_expr(expr);
         }
@@ -194,8 +192,7 @@ impl TestFile {
         Ok(())
     }
     /// Check that the provided expression matches the file contents.
-    pub fn compare_binary(&self, expr: impl Into<Expr>) -> Result<()> {
-        let expr = expr.into();
+    pub fn compare_binary(&self, expr: Expr) -> Result<()> {
         match self {
             TestFile::Binary(_) => {}
             _ => Err(TestError(format!("This is not a binary file")))?,
@@ -586,79 +583,81 @@ fn run_test(test: &SpecTest) -> Result<()> {
         output: expected,
         ..
     } = test;
-    match test.kind {
-        ParserSuccess => {
-            let expr = expr.parse()?;
-            // This exercices both parsing and binary decoding
-            expected.compare_debug(expr)?;
-        }
-        ParserFailure => {
-            use std::io;
-            let err = unwrap_err(expr.parse())?;
-            match err.downcast_ref::<DhallError>() {
-                Some(err) => match err.kind() {
-                    ErrorKind::Parse(_) => {}
-                    ErrorKind::IO(e)
-                        if e.kind() == io::ErrorKind::InvalidData => {}
-                    e => Err(TestError(format!(
-                        "Expected parse error, got: {:?}",
-                        e
-                    )))?,
-                },
-                None => {}
+    Ctxt::with_new(|cx| {
+        match test.kind {
+            ParserSuccess => {
+                let expr = expr.parse()?;
+                // This exercices both parsing and binary decoding
+                expected.compare_debug(expr.to_expr())?;
+            }
+            ParserFailure => {
+                use std::io;
+                let err = unwrap_err(expr.parse())?;
+                match err.downcast_ref::<DhallError>() {
+                    Some(err) => match err.kind() {
+                        ErrorKind::Parse(_) => {}
+                        ErrorKind::IO(e)
+                            if e.kind() == io::ErrorKind::InvalidData => {}
+                        e => Err(TestError(format!(
+                            "Expected parse error, got: {:?}",
+                            e
+                        )))?,
+                    },
+                    None => {}
+                }
+                expected.compare_ui(err)?;
+            }
+            BinaryEncoding => {
+                let expr = expr.parse()?;
+                expected.compare_binary(expr.to_expr())?;
+            }
+            BinaryDecodingSuccess => {
+                let expr = expr.parse()?;
+                expected.compare_debug(expr.to_expr())?;
+            }
+            BinaryDecodingFailure => {
+                let err = unwrap_err(expr.parse())?;
+                expected.compare_ui(err)?;
+            }
+            Printer => {
+                let parsed = expr.parse()?;
+                // Round-trip pretty-printer
+                let reparsed = Parsed::parse_str(&parsed.to_string())?;
+                assert_eq!(reparsed, parsed);
+                expected.compare_ui(parsed.to_expr())?;
+            }
+            ImportSuccess => {
+                let expr = expr.normalize(cx)?;
+                expected.compare(expr.to_expr(cx))?;
+            }
+            ImportFailure => {
+                let err = unwrap_err(expr.resolve(cx))?;
+                expected.compare_ui(err)?;
+            }
+            SemanticHash => {
+                let expr = expr.normalize(cx)?.to_expr_alpha(cx);
+                let hash = hex::encode(expr.sha256_hash()?);
+                expected.compare_ui(format!("sha256:{}", hash))?;
+            }
+            TypeInferenceSuccess => {
+                let ty = expr.typecheck(cx)?.get_type()?;
+                expected.compare(ty.to_expr(cx))?;
+            }
+            TypeInferenceFailure => {
+                let err = unwrap_err(expr.typecheck(cx))?;
+                expected.compare_ui(err)?;
+            }
+            Normalization => {
+                let expr = expr.normalize(cx)?;
+                expected.compare(expr.to_expr(cx))?;
+            }
+            AlphaNormalization => {
+                let expr = expr.normalize(cx)?.to_expr_alpha(cx);
+                expected.compare(expr)?;
             }
-            expected.compare_ui(err)?;
-        }
-        BinaryEncoding => {
-            let expr = expr.parse()?;
-            expected.compare_binary(expr)?;
-        }
-        BinaryDecodingSuccess => {
-            let expr = expr.parse()?;
-            expected.compare_debug(expr)?;
-        }
-        BinaryDecodingFailure => {
-            let err = unwrap_err(expr.parse())?;
-            expected.compare_ui(err)?;
-        }
-        Printer => {
-            let parsed = expr.parse()?;
-            // Round-trip pretty-printer
-            let reparsed = Parsed::parse_str(&parsed.to_string())?;
-            assert_eq!(reparsed, parsed);
-            expected.compare_ui(parsed)?;
-        }
-        ImportSuccess => {
-            let expr = expr.normalize()?;
-            expected.compare(expr)?;
-        }
-        ImportFailure => {
-            let err = unwrap_err(expr.resolve())?;
-            expected.compare_ui(err)?;
-        }
-        SemanticHash => {
-            let expr = expr.normalize()?.to_expr_alpha();
-            let hash = hex::encode(expr.sha256_hash()?);
-            expected.compare_ui(format!("sha256:{}", hash))?;
-        }
-        TypeInferenceSuccess => {
-            let ty = expr.typecheck()?.get_type()?;
-            expected.compare(ty)?;
-        }
-        TypeInferenceFailure => {
-            let err = unwrap_err(expr.typecheck())?;
-            expected.compare_ui(err)?;
-        }
-        Normalization => {
-            let expr = expr.normalize()?;
-            expected.compare(expr)?;
-        }
-        AlphaNormalization => {
-            let expr = expr.normalize()?.to_expr_alpha();
-            expected.compare(expr)?;
         }
-    }
-    Ok(())
+        Ok(())
+    })
 }
 
 fn main() {