diff --git a/fathom/Cargo.toml b/fathom/Cargo.toml
index 0c9be003b..c1f1f6603 100644
--- a/fathom/Cargo.toml
+++ b/fathom/Cargo.toml
@@ -27,7 +27,7 @@ lalrpop-util = "0.19.5"
 lasso = { version = "0.6.0", features = ["multi-threaded", "ahasher", "inline-more"] }
 levenshtein = "1.0.5"
 logos = "0.12"
-once_cell = { version = "1.17.0", features = ["parking_lot"] }
+once_cell = { version = "1.17.0", features = ["parking_lot"] } # TODO: remove once `std::cell::once_cell` is stabilized
 pretty = "0.11.2"
 rpds = "0.12.0"
 scoped-arena = "0.4.1"
diff --git a/fathom/src/core/binary.rs b/fathom/src/core/binary.rs
index 661f014e6..958167723 100644
--- a/fathom/src/core/binary.rs
+++ b/fathom/src/core/binary.rs
@@ -7,7 +7,8 @@ use std::fmt::Debug;
 use std::slice::SliceIndex;
 use std::sync::Arc;
 
-use crate::core::semantics::{self, ArcValue, Elim, Head, Value};
+use super::semantics::{EvalMode, LocalExprs};
+use crate::core::semantics::{self, ArcValue, Elim, Head, LazyValue, Value};
 use crate::core::{Const, Item, Module, Prim, Term, UIntStyle};
 use crate::env::{EnvLen, SharedEnv, UniqueEnv};
 use crate::source::{Span, Spanned};
@@ -254,8 +255,8 @@ impl fmt::Display for BufferError {
 impl std::error::Error for BufferError {}
 
 pub struct Context<'arena, 'data> {
-    item_exprs: UniqueEnv<ArcValue<'arena>>,
-    local_exprs: SharedEnv<ArcValue<'arena>>,
+    item_exprs: UniqueEnv<LazyValue<'arena>>,
+    local_exprs: LocalExprs<'arena>,
     initial_buffer: Buffer<'data>,
     pending_formats: Vec<(usize, ArcValue<'arena>)>,
     cached_refs: HashMap<usize, Vec<ParsedRef<'arena>>>,
@@ -283,7 +284,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
 
     fn eval_env(&mut self) -> semantics::EvalEnv<'arena, '_> {
         let elim_env = semantics::ElimEnv::new(&self.item_exprs, [][..].into());
-        semantics::EvalEnv::new(elim_env, &mut self.local_exprs)
+        semantics::EvalEnv::new(elim_env, &mut self.local_exprs).with_mode(EvalMode::Strict)
     }
 
     fn elim_env(&self) -> semantics::ElimEnv<'arena, '_> {
@@ -295,7 +296,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
         for item in module.items {
             match item {
                 Item::Def { expr, .. } => {
-                    let expr = self.eval_env().eval(expr);
+                    let expr = self.eval_env().delay_or_eval(expr);
                     self.item_exprs.push(expr);
                 }
             }
@@ -332,7 +333,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
                 let mut exprs = Vec::with_capacity(formats.len());
 
                 while let Some((format, next_formats)) = self.elim_env().split_telescope(formats) {
-                    let expr = self.read_format(reader, &format)?;
+                    let expr = LazyValue::eager(self.read_format(reader, &format)?);
                     exprs.push(expr.clone());
                     formats = next_formats(expr);
                 }
@@ -343,8 +344,10 @@ impl<'arena, 'data> Context<'arena, 'data> {
                 ))
             }
             Value::FormatCond(_label, format, cond) => {
-                let value = self.read_format(reader, format)?;
-                let cond_res = self.elim_env().apply_closure(cond, value.clone());
+                let value = self.read_format(reader, &self.elim_env().force_lazy(format))?;
+                let cond_res = self
+                    .elim_env()
+                    .apply_closure(cond, LazyValue::eager(value.clone()));
 
                 match cond_res.as_ref() {
                     Value::ConstLit(Const::Bool(true)) => Ok(value),
@@ -366,7 +369,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
                 while let Some((format, next_formats)) = self.elim_env().split_telescope(formats) {
                     let mut reader = reader.clone();
 
-                    let expr = self.read_format(&mut reader, &format)?;
+                    let expr = LazyValue::eager(self.read_format(&mut reader, &format)?);
                     exprs.push(expr.clone());
                     formats = next_formats(expr);
 
@@ -406,6 +409,8 @@ impl<'arena, 'data> Context<'arena, 'data> {
     ) -> Result<ArcValue<'arena>, ReadError<'arena>> {
         use crate::core::semantics::Elim::FunApp;
 
+        let force = |expr|  self.elim_env().force_lazy(expr);
+
         match (prim, slice) {
             (Prim::FormatU8, []) => read_const(reader, span, read_u8, |num| Const::U8(num, UIntStyle::Decimal)),
             (Prim::FormatU16Be, []) => read_const(reader, span, read_u16be, |num| Const::U16(num, UIntStyle::Decimal)),
@@ -425,22 +430,18 @@ impl<'arena, 'data> Context<'arena, 'data> {
             (Prim::FormatF32Le, []) => read_const(reader, span, read_f32le, Const::F32),
             (Prim::FormatF64Be, []) => read_const(reader, span, read_f64be, Const::F64),
             (Prim::FormatF64Le, []) => read_const(reader, span, read_f64le, Const::F64),
-            (Prim::FormatRepeatLen8, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatLen16, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatLen32, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatLen64, [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, len, format),
-            (Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, format),
-            (Prim::FormatLimit8, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLimit16, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLimit32, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLimit64, [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader, limit, format),
-            (Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, pos, format),
-            (Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(format, r#ref),
+            (Prim::FormatRepeatLen8| Prim::FormatRepeatLen16 | Prim::FormatRepeatLen32 | Prim::FormatRepeatLen64,
+                [FunApp(_, len), FunApp(_, format)]) => self.read_repeat_len(reader, span, &force(len), &force(format)),
+            (Prim::FormatRepeatUntilEnd, [FunApp(_,format)]) => self.read_repeat_until_end(reader, &force(format)),
+            (Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64,
+                [FunApp(_, limit), FunApp(_, format)]) => self.read_limit(reader,&force(limit) , &force(format)),
+            (Prim::FormatLink, [FunApp(_, pos), FunApp(_, format)]) => self.read_link(span, &force(pos), &force(format)),
+            (Prim::FormatDeref, [FunApp(_, format), FunApp(_, r#ref)]) => self.read_deref(&force(format), &force(r#ref)),
             (Prim::FormatStreamPos, []) => read_stream_pos(reader, span),
-            (Prim::FormatSucceed, [_, FunApp(_, elem)]) => Ok(elem.clone()),
+            (Prim::FormatSucceed, [_, FunApp(_, elem)]) => Ok(force(elem)),
             (Prim::FormatFail, []) => Err(ReadError::ReadFailFormat(span)),
-            (Prim::FormatUnwrap, [_, FunApp(_, option)]) => match option.match_prim_spine() {
-                Some((Prim::OptionSome, [_, FunApp(_, elem)])) => Ok(elem.clone()),
+            (Prim::FormatUnwrap, [_, FunApp(_, option)]) => match force(option).match_prim_spine() {
+                Some((Prim::OptionSome, [_, FunApp(_, elem)])) => Ok(force(elem)),
                 Some((Prim::OptionNone, [_])) => Err(ReadError::UnwrappedNone(span)),
                 _ => Err(ReadError::InvalidValue(span)),
             },
@@ -464,7 +465,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
         };
 
         let elem_exprs = (0..len)
-            .map(|_| self.read_format(reader, elem_format))
+            .map(|_| (self.read_format(reader, elem_format).map(LazyValue::eager)))
             .collect::<Result<_, _>>()?;
 
         Ok(Spanned::new(span, Arc::new(Value::ArrayLit(elem_exprs))))
@@ -481,7 +482,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
         loop {
             match self.read_format(reader, elem_format) {
                 Ok(elem) => {
-                    elems.push(elem);
+                    elems.push(LazyValue::eager(elem));
                     current_offset = reader.relative_offset();
                 }
                 Err(ReadError::BufferError(_, BufferError::UnexpectedEndOfBuffer)) => {
@@ -557,7 +558,7 @@ impl<'arena, 'data> Context<'arena, 'data> {
     fn lookup_ref<'context>(
         &'context self,
         pos: usize,
-        format: &ArcValue<'_>,
+        format: &ArcValue<'arena>,
     ) -> Option<&'context ParsedRef<'arena>> {
         // NOTE: The number of calls to `semantics::ConversionEnv::is_equal`
         // when looking up cached references is a bit of a pain. If this ever
diff --git a/fathom/src/core/prim.rs b/fathom/src/core/prim.rs
index e4e99808f..a4c126645 100644
--- a/fathom/src/core/prim.rs
+++ b/fathom/src/core/prim.rs
@@ -3,6 +3,7 @@ use std::sync::Arc;
 use fxhash::FxHashMap;
 use scoped_arena::Scope;
 
+use super::semantics::{LazyValue, LocalExprs};
 use crate::core::semantics::{ArcValue, Elim, ElimEnv, Head, Value};
 use crate::core::{self, Const, Plicity, Prim, UIntStyle};
 use crate::env::{self, SharedEnv, UniqueEnv};
@@ -508,8 +509,8 @@ struct EnvBuilder<'arena> {
     entries: FxHashMap<Symbol, (Prim, ArcValue<'arena>)>,
     scope: &'arena Scope<'arena>,
     meta_exprs: UniqueEnv<Option<ArcValue<'arena>>>,
-    item_exprs: UniqueEnv<ArcValue<'arena>>,
-    local_exprs: SharedEnv<ArcValue<'arena>>,
+    item_exprs: UniqueEnv<LazyValue<'arena>>,
+    local_exprs: LocalExprs<'arena>,
 }
 
 impl<'arena> EnvBuilder<'arena> {
@@ -577,13 +578,13 @@ macro_rules! step {
 // TODO: Should we merge the spans of the param idents to produce the body span?
 macro_rules! const_step {
     ([$($param:ident : $Input:ident),*] => $body:expr) => {
-        step!(_, [$($param),*] => match ($($param.as_ref(),)*) {
+        step!(env, [$($param),*] => match ($(env.force_lazy($param).as_ref(),)*) {
             ($(Value::ConstLit(Const::$Input($param, ..)),)*) => Spanned::empty(Arc::new(Value::ConstLit($body))),
             _ => return None,
         })
     };
     ([$($param:ident , $style:ident : $Input:ident),*] => $body:expr) => {
-        step!(_, [$($param),*] => match ($($param.as_ref(),)*) {
+        step!(env, [$($param),*] => match ($(env.force_lazy($param).as_ref(),)*) {
             ($(Value::ConstLit(Const::$Input($param, $style)),)*) => Spanned::empty(Arc::new(Value::ConstLit($body))),
             _ => return None,
         })
@@ -611,21 +612,18 @@ pub fn repr(prim: Prim) -> Step {
         Prim::FormatF32Le => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F32Type, [])))),
         Prim::FormatF64Be => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F64Type, [])))),
         Prim::FormatF64Le => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::F64Type, [])))),
-        Prim::FormatRepeatLen8 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array8Type, [len.clone(), env.format_repr(elem)])))),
-        Prim::FormatRepeatLen16 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array16Type, [len.clone(), env.format_repr(elem)])))),
-        Prim::FormatRepeatLen32 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array32Type, [len.clone(), env.format_repr(elem)])))),
-        Prim::FormatRepeatLen64 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array64Type, [len.clone(), env.format_repr(elem)])))),
-        Prim::FormatLimit8 => step!(env, [_, elem] => env.format_repr(elem)),
-        Prim::FormatLimit16 => step!(env, [_, elem] => env.format_repr(elem)),
-        Prim::FormatLimit32 => step!(env, [_, elem] => env.format_repr(elem)),
-        Prim::FormatLimit64 => step!(env, [_, elem] => env.format_repr(elem)),
-        Prim::FormatRepeatUntilEnd => step!(env, [elem] => Spanned::empty(Arc::new(Value::prim(Prim::ArrayType, [env.format_repr(elem)])))),
-        Prim::FormatLink => step!(_, [_, elem] => Spanned::empty(Arc::new(Value::prim(Prim::RefType, [elem.clone()])))),
-        Prim::FormatDeref => step!(env, [elem, _] => env.format_repr(elem)),
+        Prim::FormatRepeatLen8  => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array8Type,  [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))),
+        Prim::FormatRepeatLen16 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array16Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))),
+        Prim::FormatRepeatLen32 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array32Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))),
+        Prim::FormatRepeatLen64 => step!(env, [len, elem] => Spanned::empty(Arc::new(Value::prim(Prim::Array64Type, [env.force_lazy(len), env.format_repr(&env.force_lazy(elem))])))),
+        Prim::FormatLimit8 | Prim::FormatLimit16 | Prim::FormatLimit32 | Prim::FormatLimit64 => step!(env, [_, elem] => env.format_repr(&env.force_lazy(elem))),
+        Prim::FormatRepeatUntilEnd => step!(env, [elem] => Spanned::empty(Arc::new(Value::prim(Prim::ArrayType, [env.format_repr(&env.force_lazy(elem))])))),
+        Prim::FormatLink => step!(env, [_, elem] => Spanned::empty(Arc::new(Value::prim(Prim::RefType, [env.force_lazy(elem)])))),
+        Prim::FormatDeref => step!(env, [elem, _] => env.format_repr(&env.force_lazy(elem))),
         Prim::FormatStreamPos => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::PosType, [])))),
-        Prim::FormatSucceed => step!(_, [elem, _] => elem.clone()),
+        Prim::FormatSucceed => step!(env, [elem, _] => env.force_lazy(elem)),
         Prim::FormatFail => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::VoidType, [])))),
-        Prim::FormatUnwrap => step!(_, [elem, _] => elem.clone()),
+        Prim::FormatUnwrap => step!(env, [elem, _] => env.force_lazy(elem)),
         Prim::ReportedError => step!(_, [] => Spanned::empty(Arc::new(Value::prim(Prim::ReportedError, [])))),
         _ => |_, _| None,
     }
@@ -641,15 +639,49 @@ pub fn step(prim: Prim) -> Step {
         #[allow(unreachable_code)]
         Prim::Absurd => step!(_, [_, _] => panic!("Constructed an element of `Void`")),
 
-        Prim::FormatRepr => step!(env, [format] => env.format_repr(format)),
+        Prim::FormatRepr => step!(env, [format] => env.format_repr(&env.force_lazy(format))),
 
         Prim::BoolEq => const_step!([x: Bool, y: Bool] => Const::Bool(x == y)),
         Prim::BoolNeq => const_step!([x: Bool, y: Bool] => Const::Bool(x != y)),
         Prim::BoolNot => const_step!([x: Bool] => Const::Bool(bool::not(*x))),
-        Prim::BoolAnd => const_step!([x: Bool, y: Bool] => Const::Bool(*x && *y)),
-        Prim::BoolOr => const_step!([x: Bool, y: Bool] => Const::Bool(*x || *y)),
         Prim::BoolXor => const_step!([x: Bool, y: Bool] => Const::Bool(*x ^ *y)),
 
+        Prim::BoolAnd => |env: &ElimEnv, spine: &[Elim]| match spine {
+            [Elim::FunApp(_,x), Elim::FunApp(_, y)] => {
+                let x = env.force_lazy(x);
+                match x.as_ref() {
+                    Value::ConstLit(Const::Bool(false)) => Some(x),
+                    Value::ConstLit(Const::Bool(true)) => {
+                        let y = env.force_lazy(y);
+                        match y.as_ref() {
+                            Value::ConstLit(Const::Bool(_)) => Some(y),
+                            _ => None,
+                        }
+                    }
+                    _ => None,
+                }
+            }
+            _ => None,
+        },
+
+        Prim::BoolOr => |env: &ElimEnv, spine: &[Elim]| match spine {
+            [Elim::FunApp(_,x), Elim::FunApp(_, y)] => {
+                let x = env.force_lazy(x);
+                match x.as_ref() {
+                    Value::ConstLit(Const::Bool(true)) => Some(x),
+                    Value::ConstLit(Const::Bool(false)) => {
+                        let y = env.force_lazy(y);
+                        match y.as_ref() {
+                            Value::ConstLit(Const::Bool(_)) => Some(y),
+                            _ => None,
+                        }
+                    }
+                    _ => None,
+                }
+            }
+            _ => None,
+        },
+
         Prim::U8Eq => const_step!([x: U8, y: U8] => Const::Bool(x == y)),
         Prim::U8Neq => const_step!([x: U8, y: U8] => Const::Bool(x != y)),
         Prim::U8Gt => const_step!([x: U8, y: U8] => Const::Bool(x > y)),
@@ -775,22 +807,20 @@ pub fn step(prim: Prim) -> Step {
         Prim::S64UAbs => const_step!([x: S64] => Const::U64(i64::unsigned_abs(*x), UIntStyle::Decimal)),
 
         Prim::OptionFold => step!(env, [_, _, on_none, on_some, option] => {
-            match option.match_prim_spine()? {
+            match env.force_lazy(option).match_prim_spine()? {
                 (Prim::OptionSome, [_, Elim::FunApp(Plicity::Explicit, value)]) => {
-                    env.fun_app(Plicity::Explicit, on_some.clone(), value.clone())
+                    env.fun_app(Plicity::Explicit, env.force_lazy(on_some), value)
                 },
-                (Prim::OptionNone, [_]) => on_none.clone(),
+                (Prim::OptionNone, [_]) => env.force_lazy(on_none),
                 _ => return None,
             }
         }),
 
         Prim::Array8Find | Prim::Array16Find | Prim::Array32Find | Prim::Array64Find => {
-            step!(env, [_, elem_type, pred, array] => match array.as_ref() {
+            step!(env, [_, elem_type, pred, array] => match env.force_lazy(array).as_ref() {
                 Value::ArrayLit(elems) => {
                     for elem in elems {
-                        match env.fun_app(
-                            Plicity::Explicit,
-                            pred.clone(), elem.clone()).as_ref() {
+                        match env.fun_app(Plicity::Explicit, env.force_lazy(pred), elem).as_ref() {
                             Value::ConstLit(Const::Bool(true)) => {
                                 return Some(Spanned::empty(Arc::new(Value::Stuck(
                                     Head::Prim(Prim::OptionSome),
@@ -814,16 +844,16 @@ pub fn step(prim: Prim) -> Step {
         }
 
         Prim::Array8Index | Prim::Array16Index | Prim::Array32Index | Prim::Array64Index => {
-            step!(_, [_, _, index, array] => match array.as_ref() {
+            step!(env, [_, _, index, array] => match env.force_lazy(array).as_ref() {
                 Value::ArrayLit(elems) => {
-                    let index = match (index).as_ref() {
+                    let index = match env.force_lazy(index).as_ref() {
                         Value::ConstLit(Const::U8(index, _)) => Some(usize::from(*index)),
                         Value::ConstLit(Const::U16(index, _)) => Some(usize::from(*index)),
                         Value::ConstLit(Const::U32(index, _)) => usize::try_from(*index).ok(),
                         Value::ConstLit(Const::U64(index, _)) => usize::try_from(*index).ok(),
                         _ => return None,
                     }?;
-                    elems.get(index).cloned()?
+                    env.force_lazy(elems.get(index)?)
                 }
                 _ => return None,
             })
diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs
index 5be7f9dbe..4f6234b9d 100644
--- a/fathom/src/core/semantics.rs
+++ b/fathom/src/core/semantics.rs
@@ -1,9 +1,11 @@
 //! The semantics of the core language, implemented using [normalization by
 //! evaluation](https://en.wikipedia.org/wiki/Normalization_by_evaluation).
 
+use std::cell::RefCell;
 use std::panic::panic_any;
 use std::sync::Arc;
 
+use once_cell::sync::OnceCell;
 use scoped_arena::Scope;
 
 use crate::alloc::SliceVec;
@@ -16,6 +18,15 @@ use crate::symbol::Symbol;
 /// the amount of sharing we can achieve during evaluation.
 pub type ArcValue<'arena> = Spanned<Arc<Value<'arena>>>;
 
+pub type LocalExprs<'arena> = SharedEnv<LazyValue<'arena>>;
+pub type ItemExprs<'arena> = SliceEnv<LazyValue<'arena>>;
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum EvalMode {
+    Lazy,
+    Strict,
+}
+
 /// Values in weak-head-normal form, with bindings converted to closures.
 #[derive(Debug, Clone)]
 pub enum Value<'arena> {
@@ -29,22 +40,27 @@ pub enum Value<'arena> {
     Universe,
 
     /// Dependent function types.
-    FunType(Plicity, Option<Symbol>, ArcValue<'arena>, Closure<'arena>),
+    FunType(
+        Plicity,
+        Option<Symbol>,
+        Arc<LazyValue<'arena>>, // wrapped in `Arc` to keep size_of<Value> down
+        Closure<'arena>,
+    ),
     /// Function literals.
     FunLit(Plicity, Option<Symbol>, Closure<'arena>),
 
     /// Record types.
     RecordType(&'arena [Symbol], Telescope<'arena>),
     /// Record literals.
-    RecordLit(&'arena [Symbol], Vec<ArcValue<'arena>>),
+    RecordLit(&'arena [Symbol], Vec<LazyValue<'arena>>),
 
     /// Array literals.
-    ArrayLit(Vec<ArcValue<'arena>>),
+    ArrayLit(Vec<LazyValue<'arena>>),
 
     /// Record formats, consisting of a list of dependent formats.
     FormatRecord(&'arena [Symbol], Telescope<'arena>),
     /// Conditional format, consisting of a format and predicate.
-    FormatCond(Symbol, ArcValue<'arena>, Closure<'arena>),
+    FormatCond(Symbol, Arc<LazyValue<'arena>>, Closure<'arena>),
     /// Overlap formats, consisting of a list of dependent formats, overlapping
     /// in memory.
     FormatOverlap(&'arena [Symbol], Telescope<'arena>),
@@ -53,11 +69,58 @@ pub enum Value<'arena> {
     ConstLit(Const),
 }
 
+/// Initialization operation for lazy values.
+///
+/// We need to use a [defunctionalized] representation because Rust does not
+/// allow closures of type `dyn (Clone + FnOnce() -> Arc<Value>)`.
+///
+/// [defunctionalized]: https://en.wikipedia.org/wiki/Defunctionalization
+#[derive(Clone, Debug)]
+enum LazyInit<'arena> {
+    EvalTerm(LocalExprs<'arena>, &'arena Term<'arena>),
+    ApplyElim(Arc<LazyValue<'arena>>, Arc<Elim<'arena>>),
+}
+
+#[derive(Debug, Clone)]
+pub struct LazyValue<'arena> {
+    /// Initialization operation. Will be set to `None` if `cell` is forced.
+    init: RefCell<Option<LazyInit<'arena>>>,
+    /// A once-cell to hold the lazily initialized value.
+    cell: OnceCell<ArcValue<'arena>>,
+}
+
+impl<'arena> LazyValue<'arena> {
+    /// Eagerly construct the lazy value.
+    pub fn eager(value: ArcValue<'arena>) -> Self {
+        LazyValue {
+            init: RefCell::new(None),
+            cell: OnceCell::from(value),
+        }
+    }
+
+    /// Create a delayed LazyValue which, when forced, will evaluate `term` in
+    /// `local_exprs`
+    pub fn delay(local_exprs: LocalExprs<'arena>, term: &'arena Term<'arena>) -> Self {
+        LazyValue {
+            init: RefCell::new(Some(LazyInit::EvalTerm(local_exprs, term))),
+            cell: OnceCell::new(),
+        }
+    }
+
+    /// Lazily apply an elimination.
+    pub fn apply_elim(head: Arc<LazyValue<'arena>>, elim: Elim<'arena>) -> Self {
+        LazyValue {
+            init: RefCell::new(Some(LazyInit::ApplyElim(head, Arc::new(elim)))),
+            cell: OnceCell::new(),
+        }
+    }
+}
+
 impl<'arena> Value<'arena> {
     pub fn prim(prim: Prim, params: impl IntoIterator<Item = ArcValue<'arena>>) -> Value<'arena> {
         let params = params
             .into_iter()
-            .map(|arg| Elim::FunApp(Plicity::Explicit, arg))
+            .map(|arg| Elim::FunApp(Plicity::Explicit, LazyValue::eager(arg)))
             .collect();
         Value::Stuck(Head::Prim(prim), params)
     }
@@ -98,7 +161,7 @@ pub enum Head {
 #[derive(Debug, Clone)]
 pub enum Elim<'arena> {
     /// Function applications.
-    FunApp(Plicity, ArcValue<'arena>),
+    FunApp(Plicity, LazyValue<'arena>),
     /// Record projections.
     RecordProj(Symbol),
     /// Match on a constant.
@@ -111,17 +174,14 @@ pub struct Closure<'arena> {
     /// Local environment where the closed [term][Self.term] is bound. A new
     /// entry will need to be pushed to this environment before evaluating the
     /// term.
-    local_exprs: SharedEnv<ArcValue<'arena>>,
+    local_exprs: LocalExprs<'arena>,
     /// The term that is closed over.
     term: &'arena Term<'arena>,
 }
 
 impl<'arena> Closure<'arena> {
     /// Construct a closure.
-    pub fn new(
-        local_exprs: SharedEnv<ArcValue<'arena>>,
-        term: &'arena Term<'arena>,
-    ) -> Closure<'arena> {
+    pub fn new(local_exprs: LocalExprs<'arena>, term: &'arena Term<'arena>) -> Closure<'arena> {
         Closure { local_exprs, term }
     }
 
@@ -140,7 +200,7 @@ impl<'arena> Closure<'arena> {
 #[derive(Debug, Clone)]
 pub struct Telescope<'arena> {
     /// Local environment where the telescope's [terms][Self.terms] are bound.
-    local_exprs: SharedEnv<ArcValue<'arena>>,
+    local_exprs: LocalExprs<'arena>,
     /// `Repr` should be applied to each term in the telescope.
     apply_repr: bool,
     /// The terms in the telescope.
@@ -150,7 +210,7 @@ pub struct Telescope<'arena> {
 impl<'arena> Telescope<'arena> {
     /// Construct a telescope.
     pub fn new(
-        local_exprs: SharedEnv<ArcValue<'arena>>,
+        local_exprs: LocalExprs<'arena>,
         terms: &'arena [Term<'arena>],
     ) -> Telescope<'arena> {
         Telescope {
@@ -177,7 +237,7 @@ impl<'arena> Telescope<'arena> {
 /// The branches of a single-level pattern match.
 #[derive(Debug, Clone)]
 pub struct Branches<'arena, P> {
-    local_exprs: SharedEnv<ArcValue<'arena>>,
+    local_exprs: LocalExprs<'arena>,
     pattern_branches: &'arena [(P, Term<'arena>)],
     default_branch: Option<(Option<Symbol>, &'arena Term<'arena>)>,
 }
@@ -185,7 +245,7 @@ pub struct Branches<'arena, P> {
 impl<'arena, P> Branches<'arena, P> {
     /// Construct a single-level pattern match.
     pub fn new(
-        local_exprs: SharedEnv<ArcValue<'arena>>,
+        local_exprs: LocalExprs<'arena>,
         pattern_branches: &'arena [(P, Term<'arena>)],
         default_branch: Option<(Option<Symbol>, &'arena Term<'arena>)>,
     ) -> Branches<'arena, P> {
@@ -245,26 +305,43 @@ impl Error {
 /// Like the [`ElimEnv`], this allows for the running of computations, but
 /// also maintains a local environment, allowing for evaluation.
 pub struct EvalEnv<'arena, 'env> {
+    mode: EvalMode,
     elim_env: ElimEnv<'arena, 'env>,
-    local_exprs: &'env mut SharedEnv<ArcValue<'arena>>,
+    local_exprs: &'env mut LocalExprs<'arena>,
 }
 
 impl<'arena, 'env> EvalEnv<'arena, 'env> {
     pub fn new(
         elim_env: ElimEnv<'arena, 'env>,
-        local_exprs: &'env mut SharedEnv<ArcValue<'arena>>,
+        local_exprs: &'env mut LocalExprs<'arena>,
     ) -> EvalEnv<'arena, 'env> {
         EvalEnv {
+            mode: EvalMode::Lazy,
             elim_env,
             local_exprs,
         }
     }
 
+    pub fn with_mode(self, mode: EvalMode) -> Self {
+        Self { mode, ..self }
+    }
+
+    pub fn delay_or_eval(&mut self, term: &'arena Term<'arena>) -> LazyValue<'arena> {
+        match self.mode {
+            EvalMode::Lazy => self.delay(term),
+            EvalMode::Strict => LazyValue::eager(self.eval(term)),
+        }
+    }
+
+    pub fn delay(&self, term: &'arena Term<'arena>) -> LazyValue<'arena> {
+        LazyValue::delay(self.local_exprs.clone(), term)
+    }
+
     fn quote_env(&self) -> QuoteEnv<'arena, 'env> {
         QuoteEnv::new(self.elim_env, self.local_exprs.len())
     }
 
-    fn get_local_expr<'this: 'env>(&'this self, var: Index) -> &'env ArcValue<'arena> {
+    fn get_local_expr<'this: 'env>(&'this self, var: Index) -> &'env LazyValue<'arena> {
         let value = self.local_exprs.get_index(var);
         value.unwrap_or_else(|| panic_any(Error::UnboundLocalVar))
     }
@@ -287,21 +364,25 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
     /// twitter thread](https://twitter.com/brendanzab/status/1423536653658771457)).
     pub fn eval(&mut self, term: &Term<'arena>) -> ArcValue<'arena> {
         match term {
-            Term::ItemVar(span, var) => {
-                Spanned::new(*span, Arc::clone(self.elim_env.get_item_expr(*var)))
+            Term::ItemVar(_, var) => {
+                let expr = self.elim_env.get_item_expr(*var);
+                self.elim_env.force_lazy(expr)
             }
             Term::MetaVar(span, var) => match self.elim_env.get_meta_expr(*var) {
                 Some(value) => Spanned::new(*span, Arc::clone(value)),
                 None => Spanned::new(*span, Arc::new(Value::meta_var(*var))),
             },
-            Term::LocalVar(span, var) => Spanned::new(*span, Arc::clone(self.get_local_expr(*var))),
+            Term::LocalVar(_, var) => {
+                let expr = self.get_local_expr(*var);
+                self.elim_env.force_lazy(expr)
+            }
             Term::InsertedMeta(span, var, local_infos) => {
                 let head_expr = self.eval(&Term::MetaVar(*span, *var));
                 self.apply_local_infos(head_expr, local_infos)
             }
             Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)),
             Term::Let(span, _, _, def_expr, body_expr) => {
-                let def_expr = self.eval(def_expr);
+                let def_expr = self.delay_or_eval(def_expr);
                 self.local_exprs.push(def_expr);
                 let body_expr = self.eval(body_expr);
                 self.local_exprs.pop();
@@ -315,7 +396,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                 Arc::new(Value::FunType(
                     *plicity,
                     *param_name,
-                    self.eval(param_type),
+                    Arc::new(self.delay_or_eval(param_type)),
                     Closure::new(self.local_exprs.clone(), body_type),
                 )),
             ),
@@ -329,8 +410,8 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
             ),
             Term::FunApp(span, plicity, head_expr, arg_expr) => {
                 let head_expr = self.eval(head_expr);
-                let arg_expr = self.eval(arg_expr);
-                Spanned::merge(*span, self.elim_env.fun_app(*plicity, head_expr, arg_expr))
+                let arg_expr = self.delay_or_eval(arg_expr);
+                Spanned::merge(*span, self.elim_env.fun_app(*plicity, head_expr, &arg_expr))
             }
 
             Term::RecordType(span, labels, types) => {
@@ -338,7 +419,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                 Spanned::new(*span, Arc::new(Value::RecordType(labels, types)))
             }
             Term::RecordLit(span, labels, exprs) => {
-                let exprs = exprs.iter().map(|expr| self.eval(expr)).collect();
+                let exprs = exprs.iter().map(|expr| self.delay_or_eval(expr)).collect();
                 Spanned::new(*span, Arc::new(Value::RecordLit(labels, exprs)))
             }
             Term::RecordProj(span, head_expr, label) => {
@@ -347,7 +428,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
             }
 
             Term::ArrayLit(span, exprs) => {
-                let exprs = exprs.iter().map(|expr| self.eval(expr)).collect();
+                let exprs = exprs.iter().map(|expr| self.delay_or_eval(expr)).collect();
                 Spanned::new(*span, Arc::new(Value::ArrayLit(exprs)))
             }
 
@@ -356,7 +437,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                 Spanned::new(*span, Arc::new(Value::FormatRecord(labels, formats)))
             }
             Term::FormatCond(span, name, format, cond) => {
-                let format = self.eval(format);
+                let format = Arc::new(self.delay_or_eval(format));
                 let cond_expr = Closure::new(self.local_exprs.clone(), cond);
                 Spanned::new(*span, Arc::new(Value::FormatCond(*name, format, cond_expr)))
             }
@@ -386,10 +467,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
         for (info, expr) in Iterator::zip(infos.iter(), self.local_exprs.iter()) {
             head_expr = match info {
                 LocalInfo::Def => head_expr,
-                LocalInfo::Param => {
-                    self.elim_env
-                        .fun_app(Plicity::Explicit, head_expr, expr.clone())
-                }
+                LocalInfo::Param => self.elim_env.fun_app(Plicity::Explicit, head_expr, expr),
             };
         }
         head_expr
@@ -402,13 +480,13 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
 /// environment that would be needed for full evaluation.
 #[derive(Copy, Clone)]
 pub struct ElimEnv<'arena, 'env> {
-    item_exprs: &'env SliceEnv<ArcValue<'arena>>,
+    item_exprs: &'env ItemExprs<'arena>,
     meta_exprs: &'env SliceEnv<Option<ArcValue<'arena>>>,
 }
 
 impl<'arena, 'env> ElimEnv<'arena, 'env> {
     pub fn new(
-        item_exprs: &'env SliceEnv<ArcValue<'arena>>,
+        item_exprs: &'env ItemExprs<'arena>,
         meta_exprs: &'env SliceEnv<Option<ArcValue<'arena>>>,
     ) -> ElimEnv<'arena, 'env> {
         ElimEnv {
@@ -417,10 +495,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
         }
     }
 
-    pub fn eval_env(
-        &self,
-        local_exprs: &'env mut SharedEnv<ArcValue<'arena>>,
-    ) -> EvalEnv<'arena, 'env> {
+    pub fn eval_env(&self, local_exprs: &'env mut LocalExprs<'arena>) -> EvalEnv<'arena, 'env> {
         EvalEnv::new(*self, local_exprs)
     }
 
@@ -428,7 +503,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
         ConversionEnv::new(*self, local_exprs)
     }
 
-    fn get_item_expr(&self, var: Level) -> &'env ArcValue<'arena> {
+    fn get_item_expr(&self, var: Level) -> &'env LazyValue<'arena> {
         let value = self.item_exprs.get_level(var);
         value.unwrap_or_else(|| panic_any(Error::UnboundItemVar))
     }
@@ -440,7 +515,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
 
     /// Bring a value up-to-date with any new unification solutions that
     /// might now be present at the head of in the given value.
-    pub fn force(&self, value: &ArcValue<'arena>) -> ArcValue<'arena> {
+    pub fn force_metas(&self, value: &ArcValue<'arena>) -> ArcValue<'arena> {
         let mut forced_value = value.clone();
         // Attempt to force metavariables until we don't see any more.
         while let Value::Stuck(Head::MetaVar(var), spine) = forced_value.as_ref() {
@@ -456,11 +531,32 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
         forced_value
     }
 
+    /// Force the evaluation of a lazy value.
+    pub fn force_lazy(&self, value: &LazyValue<'arena>) -> ArcValue<'arena> {
+        (value.cell)
+            .get_or_init(|| match value.init.replace(None) {
+                Some(LazyInit::EvalTerm(mut local_exprs, term)) => {
+                    self.eval_env(&mut local_exprs).eval(term)
+                }
+                Some(LazyInit::ApplyElim(head, elim)) => match elim.as_ref() {
+                    Elim::RecordProj(label) => self.record_proj(self.force_lazy(&head), *label),
+                    Elim::FunApp(plicity, arg) => {
+                        self.fun_app(*plicity, self.force_lazy(&head), arg)
+                    }
+                    Elim::ConstMatch(branches) => {
+                        self.const_match(self.force_lazy(&head), branches.clone())
+                    }
+                },
+                None => panic!("Lazy instance has previously been poisoned"),
+            })
+            .clone()
+    }
+
     /// Apply a closure to a value.
     pub fn apply_closure(
         &self,
         closure: &Closure<'arena>,
-        value: ArcValue<'arena>,
+        value: LazyValue<'arena>,
     ) -> ArcValue<'arena> {
         let mut local_exprs = closure.local_exprs.clone();
         local_exprs.push(value);
@@ -474,7 +570,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
         mut telescope: Telescope<'arena>,
     ) -> Option<(
         ArcValue<'arena>,
-        impl FnOnce(ArcValue<'arena>) -> Telescope<'arena>,
+        impl FnOnce(LazyValue<'arena>) -> Telescope<'arena>,
     )> {
         let (term, terms) = telescope.terms.split_first()?;
         let mut env = self.eval_env(&mut telescope.local_exprs);
@@ -518,18 +614,18 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
         &self,
         arg_plicity: Plicity,
         mut head_expr: ArcValue<'arena>,
-        arg_expr: ArcValue<'arena>,
+        arg_expr: &LazyValue<'arena>,
     ) -> ArcValue<'arena> {
         match Arc::make_mut(&mut head_expr) {
             // Beta-reduction
             Value::FunLit(fun_plicity, _, body_expr) => {
                 assert_eq!(arg_plicity, *fun_plicity, "Plicities must be equal");
                 // FIXME: use span from head/arg exprs?
-                self.apply_closure(body_expr, arg_expr)
+                self.apply_closure(body_expr, arg_expr.clone())
             }
             // The computation is stuck, preventing further reduction
             Value::Stuck(head, spine) => {
-                spine.push(Elim::FunApp(arg_plicity, arg_expr));
+                spine.push(Elim::FunApp(arg_plicity, arg_expr.clone()));
                 match head {
                     Head::Prim(prim) => prim::step(*prim)(self, spine).unwrap_or(head_expr),
                     _ => head_expr,
@@ -543,12 +639,17 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
     /// [beta-reduction] if possible.
     ///
     /// [beta-reduction]: https://ncatlab.org/nlab/show/beta-reduction
-    pub fn record_proj(&self, mut head_expr: ArcValue<'arena>, label: Symbol) -> ArcValue<'arena> {
+    pub fn record_proj(
+        &self,
+        mut head_expr: ArcValue<'arena>, // TODO: should `head_expr` be lazy?
+        label: Symbol,
+    ) -> ArcValue<'arena> {
         match Arc::make_mut(&mut head_expr) {
             // Beta-reduction
             Value::RecordLit(labels, exprs) => (labels.iter())
                 .position(|current_label| *current_label == label)
                 .and_then(|expr_index| exprs.get(expr_index).cloned())
+                .map(|lazy_value| self.force_lazy(&lazy_value))
                 .unwrap_or_else(|| panic_any(Error::InvalidRecordProj)),
             // The computation is stuck, preventing further reduction
             Value::Stuck(_, spine) => {
@@ -580,7 +681,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
                 let mut local_exprs = branches.local_exprs.clone();
                 match branches.default_branch {
                     Some((_, default_expr)) => {
-                        local_exprs.push(head_expr);
+                        local_exprs.push(LazyValue::eager(head_expr));
                         self.eval_env(&mut local_exprs).eval(default_expr)
                     }
                     None => panic_any(Error::MissingConstDefault),
@@ -598,7 +699,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
     /// Apply an expression to an elimination spine.
     fn apply_spine(&self, head_expr: ArcValue<'arena>, spine: &[Elim<'arena>]) -> ArcValue<'arena> {
         spine.iter().fold(head_expr, |head_expr, elim| match elim {
-            Elim::FunApp(plicity, arg_expr) => self.fun_app(*plicity, head_expr, arg_expr.clone()),
+            Elim::FunApp(plicity, arg_expr) => self.fun_app(*plicity, head_expr, arg_expr),
             Elim::RecordProj(label) => self.record_proj(head_expr, *label),
             Elim::ConstMatch(split) => self.const_match(head_expr, split.clone()),
         })
@@ -610,7 +711,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> {
             Value::FormatRecord(labels, formats) | Value::FormatOverlap(labels, formats) => {
                 Value::RecordType(labels, formats.clone().apply_repr())
             }
-            Value::FormatCond(_, format, _) => return self.format_repr(format),
+            Value::FormatCond(_, format, _) => return self.format_repr(&self.force_lazy(format)),
             Value::Stuck(Head::Prim(prim), spine) => match prim::repr(*prim)(self, spine) {
                 Some(r#type) => return r#type,
                 None => Value::prim(Prim::FormatRepr, [format.clone()]),
@@ -667,7 +768,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         // NOTE: this copies more than is necessary when `'in_arena == 'out_arena`:
         // for example when copying label slices.
 
-        let value = self.elim_env.force(value);
+        let value = self.elim_env.force_metas(value);
         let span = value.span();
         match value.as_ref() {
             Value::Stuck(head, spine) => spine.iter().fold(
@@ -677,7 +778,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
                         span,
                         *plicity,
                         scope.to_scope(head_expr),
-                        scope.to_scope(self.quote(scope, arg_expr)),
+                        scope.to_scope(self.quote_lazy(scope, arg_expr)),
                     ),
                     Elim::RecordProj(label) => {
                         Term::RecordProj(span, scope.to_scope(head_expr), *label)
@@ -716,7 +817,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
                 span,
                 *plicity,
                 *param_name,
-                scope.to_scope(self.quote(scope, param_type)),
+                scope.to_scope(self.quote_lazy(scope, param_type)),
                 self.quote_closure(scope, body_type),
             ),
             Value::FunLit(plicity, param_name, body_expr) => Term::FunLit(
@@ -734,11 +835,11 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
             Value::RecordLit(labels, exprs) => Term::RecordLit(
                 span,
                 scope.to_scope_from_iter(labels.iter().copied()),
-                scope.to_scope_from_iter(exprs.iter().map(|expr| self.quote(scope, expr))),
+                scope.to_scope_from_iter((exprs.iter()).map(|expr| self.quote_lazy(scope, expr))),
             ),
             Value::ArrayLit(exprs) => Term::ArrayLit(
                 span,
-                scope.to_scope_from_iter(exprs.iter().map(|expr| self.quote(scope, expr))),
+                scope.to_scope_from_iter(exprs.iter().map(|expr| self.quote_lazy(scope, expr))),
             ),
 
             Value::FormatRecord(labels, formats) => Term::FormatRecord(
@@ -749,7 +850,7 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
             Value::FormatCond(label, format, cond) => Term::FormatCond(
                 span,
                 *label,
-                scope.to_scope(self.quote(scope, format)),
+                scope.to_scope(self.quote_lazy(scope, format)),
                 self.quote_closure(scope, cond),
             ),
             Value::FormatOverlap(labels, formats) => Term::FormatOverlap(
@@ -762,6 +863,14 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         }
     }
 
+    pub fn quote_lazy<'out_arena>(
+        &mut self,
+        scope: &'out_arena Scope<'out_arena>,
+        value: &LazyValue<'in_arena>,
+    ) -> Term<'out_arena> {
+        self.quote(scope, &self.elim_env.force_lazy(value))
+    }
+
     /// Quote an [elimination head][Head] back into a [term][Term].
     fn quote_head<'out_arena>(
         &mut self,
@@ -793,8 +902,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         scope: &'out_arena Scope<'out_arena>,
         closure: &Closure<'in_arena>,
     ) -> &'out_arena Term<'out_arena> {
-        let var = Arc::new(Value::local_var(self.local_exprs.next_level()));
-        let value = self.elim_env.apply_closure(closure, Spanned::empty(var));
+        let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.local_exprs.next_level(),
+        ))));
+        let value = self.elim_env.apply_closure(closure, var);
 
         self.push_local();
         let term = self.quote(scope, &value);
@@ -814,8 +925,10 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         let mut terms = SliceVec::new(scope, telescope.len());
 
         while let Some((value, next_telescope)) = self.elim_env.split_telescope(telescope) {
-            let var = Arc::new(Value::local_var(self.local_exprs.next_level()));
-            telescope = next_telescope(Spanned::empty(var));
+            let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+                self.local_exprs.next_level(),
+            ))));
+            telescope = next_telescope(var);
             terms.push(self.quote(scope, &value));
             self.local_exprs.push();
         }
@@ -977,10 +1090,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                         scope.to_scope(head_expr),
                         scope.to_scope(self.unfold_metas(scope, arg_expr)),
                     )),
-                    TermOrValue::Value(head_expr) => {
-                        let arg_expr = self.eval(arg_expr);
-                        TermOrValue::Value(self.elim_env.fun_app(*plicity, head_expr, arg_expr))
-                    }
+                    TermOrValue::Value(head_expr) => TermOrValue::Value(self.elim_env.fun_app(
+                        *plicity,
+                        head_expr,
+                        &LazyValue::delay(self.local_exprs.clone(), arg_expr),
+                    )),
                 }
             }
             Term::RecordProj(span, head_expr, label) => {
@@ -1024,9 +1138,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
         scope: &'out_arena Scope<'out_arena>,
         term: &Term<'arena>,
     ) -> &'out_arena Term<'out_arena> {
-        let var = Arc::new(Value::local_var(self.local_exprs.len().next_level()));
+        let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.local_exprs.len().next_level(),
+        ))));
 
-        self.local_exprs.push(Spanned::empty(var));
+        self.local_exprs.push(var);
         let term = self.unfold_metas(scope, term);
         self.local_exprs.pop();
 
@@ -1043,8 +1159,10 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
 
         let terms = scope.to_scope_from_iter(terms.iter().map(|term| {
             let term = self.unfold_metas(scope, term);
-            let var = Arc::new(Value::local_var(self.local_exprs.len().next_level()));
-            self.local_exprs.push(Spanned::empty(var));
+            let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+                self.local_exprs.len().next_level(),
+            ))));
+            self.local_exprs.push(var);
             term
         }));
 
@@ -1091,9 +1209,9 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
     ///
     /// [computationally equal]: https://ncatlab.org/nlab/show/equality#computational_equality
     /// [eta-conversion]: https://ncatlab.org/nlab/show/eta-conversion
-    pub fn is_equal(&mut self, value0: &ArcValue<'_>, value1: &ArcValue<'_>) -> bool {
-        let value0 = self.elim_env.force(value0);
-        let value1 = self.elim_env.force(value1);
+    pub fn is_equal(&mut self, value0: &ArcValue<'arena>, value1: &ArcValue<'arena>) -> bool {
+        let value0 = self.elim_env.force_metas(value0);
+        let value1 = self.elim_env.force_metas(value1);
 
         match (value0.as_ref(), value1.as_ref()) {
             // `ReportedError`s result from errors that have already been
@@ -1111,7 +1229,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
                 Value::FunType(plicity1, _, param_type1, body_type1),
             ) => {
                 plicity0 == plicity1
-                    && self.is_equal(param_type0, param_type1)
+                    && self.is_equal_lazy(param_type0, param_type1)
                     && self.is_equal_closures(body_type0, body_type1)
             }
             (Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) => {
@@ -1130,7 +1248,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
             (Value::RecordLit(labels0, exprs0), Value::RecordLit(labels1, exprs1)) => {
                 labels0 == labels1
                     && Iterator::zip(exprs0.iter(), exprs1.iter())
-                        .all(|(expr0, expr1)| self.is_equal(expr0, expr1))
+                        .all(|(expr0, expr1)| self.is_equal_lazy(expr0, expr1))
             }
             (Value::RecordLit(labels, exprs), _) => {
                 self.is_equal_record_lit(labels, exprs, &value1)
@@ -1141,7 +1259,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
 
             (Value::ArrayLit(exprs0), Value::ArrayLit(exprs1)) => {
                 Iterator::zip(exprs0.iter(), exprs1.iter())
-                    .all(|(expr0, expr1)| self.is_equal(expr0, expr1))
+                    .all(|(expr0, expr1)| self.is_equal_lazy(expr0, expr1))
             }
 
             (Value::FormatRecord(labels0, formats0), Value::FormatRecord(labels1, formats1))
@@ -1154,7 +1272,7 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
                 Value::FormatCond(label1, format1, cond1),
             ) => {
                 label0 == label1
-                    && self.is_equal(format0, format1)
+                    && self.is_equal_lazy(format0, format1)
                     && self.is_equal_closures(cond0, cond1)
             }
 
@@ -1164,13 +1282,24 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
         }
     }
 
+    pub fn is_equal_lazy(
+        &mut self,
+        value0: &LazyValue<'arena>,
+        value1: &LazyValue<'arena>,
+    ) -> bool {
+        self.is_equal(
+            &self.elim_env.force_lazy(value0),
+            &self.elim_env.force_lazy(value1),
+        )
+    }
+
     /// Check that two elimination spines are equal.
-    pub fn is_equal_spines(&mut self, spine0: &[Elim<'_>], spine1: &[Elim<'_>]) -> bool {
+    pub fn is_equal_spines(&mut self, spine0: &[Elim<'arena>], spine1: &[Elim<'arena>]) -> bool {
         spine0.len() == spine1.len()
             && Iterator::zip(spine0.iter(), spine1.iter()).all(|(elim0, elim1)| {
                 match (elim0, elim1) {
                     (Elim::FunApp(plicity0, expr0), Elim::FunApp(plicity1, expr1)) => {
-                        plicity0 == plicity1 && self.is_equal(expr0, expr1)
+                        plicity0 == plicity1 && self.is_equal_lazy(expr0, expr1)
                     }
                     (Elim::RecordProj(label0), Elim::RecordProj(label1)) => label0 == label1,
                     (Elim::ConstMatch(branches0), Elim::ConstMatch(branches1)) => {
@@ -1182,8 +1311,14 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
     }
 
     /// Check that two [closures][Closure] are equal.
-    pub fn is_equal_closures(&mut self, closure0: &Closure<'_>, closure1: &Closure<'_>) -> bool {
-        let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level())));
+    pub fn is_equal_closures(
+        &mut self,
+        closure0: &Closure<'arena>,
+        closure1: &Closure<'arena>,
+    ) -> bool {
+        let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.local_exprs.next_level(),
+        ))));
         let value0 = self.elim_env.apply_closure(closure0, var.clone());
         let value1 = self.elim_env.apply_closure(closure1, var);
 
@@ -1197,8 +1332,8 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
     /// Check that two [telescopes][Telescope] are equal.
     pub fn is_equal_telescopes(
         &mut self,
-        telescope0: &Telescope<'_>,
-        telescope1: &Telescope<'_>,
+        telescope0: &Telescope<'arena>,
+        telescope1: &Telescope<'arena>,
     ) -> bool {
         if telescope0.len() != telescope1.len() {
             return false;
@@ -1217,7 +1352,9 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
                 return false;
             }
 
-            let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level())));
+            let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+                self.local_exprs.next_level(),
+            ))));
             telescope0 = next_telescope0(var.clone());
             telescope1 = next_telescope1(var);
             self.local_exprs.push();
@@ -1230,8 +1367,8 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
     /// Check that two [constant branches][Branches] are equal.
     fn is_equal_branches<P: PartialEq + Copy>(
         &mut self,
-        branches0: &Branches<'_, P>,
-        branches1: &Branches<'_, P>,
+        branches0: &Branches<'arena, P>,
+        branches1: &Branches<'arena, P>,
     ) -> bool {
         use SplitBranches::*;
 
@@ -1267,11 +1404,13 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
     fn is_equal_fun_lit(
         &mut self,
         plicity: Plicity,
-        body_expr: &Closure<'_>,
-        value: &ArcValue<'_>,
+        body_expr: &Closure<'arena>,
+        value: &ArcValue<'arena>,
     ) -> bool {
-        let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level())));
-        let value = self.elim_env.fun_app(plicity, value.clone(), var.clone());
+        let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.local_exprs.next_level(),
+        ))));
+        let value = self.elim_env.fun_app(plicity, value.clone(), &var);
         let body_expr = self.elim_env.apply_closure(body_expr, var);
 
         self.push_local();
@@ -1289,12 +1428,12 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> {
     fn is_equal_record_lit(
         &mut self,
         labels: &[Symbol],
-        exprs: &[ArcValue<'_>],
-        value: &ArcValue<'_>,
+        exprs: &[LazyValue<'arena>],
+        value: &ArcValue<'arena>,
     ) -> bool {
         Iterator::zip(labels.iter(), exprs.iter()).all(|(label, expr)| {
             let field_value = self.elim_env.record_proj(value.clone(), *label);
-            self.is_equal(expr, &field_value)
+            self.is_equal(&self.elim_env.force_lazy(expr), &field_value)
         })
     }
 }
@@ -1349,5 +1488,6 @@ mod tests {
     #[cfg(target_pointer_width = "64")]
     fn value_size() {
         assert_eq!(std::mem::size_of::<Value>(), 72);
+        assert_eq!(std::mem::size_of::<LazyValue>(), 80);
     }
 }
diff --git a/fathom/src/driver.rs b/fathom/src/driver.rs
index 36fb4a94d..7a03a1fb5 100644
--- a/fathom/src/driver.rs
+++ b/fathom/src/driver.rs
@@ -7,6 +7,7 @@ use codespan_reporting::files::SimpleFiles;
 use codespan_reporting::term::termcolor::{BufferedStandardStream, ColorChoice, WriteColor};
 
 use crate::core::binary::{self, BufferError, ReadError};
+use crate::core::semantics::EvalMode;
 use crate::files::{FileId, Files};
 use crate::source::{ByteRange, ProgramSource, SourceTooBig, Span, MAX_SOURCE_LEN};
 use crate::surface::elaboration::ItemEnv;
@@ -264,8 +265,14 @@ impl<'surface, 'core> Driver<'surface, 'core> {
             return Status::Error;
         }
 
-        let term = context.eval_env().normalize(&self.core_scope, &term);
-        let r#type = context.eval_env().normalize(&self.core_scope, &r#type);
+        let term = context
+            .eval_env()
+            .with_mode(EvalMode::Strict)
+            .normalize(&self.core_scope, &term);
+        let r#type = context
+            .eval_env()
+            .with_mode(EvalMode::Strict)
+            .normalize(&self.core_scope, &r#type);
 
         self.surface_scope.reset(); // Reuse the surface scope for distillation
         let mut context = context.distillation_context(&self.surface_scope);
@@ -443,8 +450,8 @@ impl<'surface, 'core> Driver<'surface, 'core> {
 
     fn read_error_to_diagnostic(
         &self,
-        err: ReadError<'_>,
-        context: &mut elaboration::Context,
+        err: ReadError<'core>,
+        context: &mut elaboration::Context<'core>,
     ) -> Diagnostic<FileId> {
         match err {
             ReadError::ReadFailFormat(span) => Diagnostic::error()
diff --git a/fathom/src/surface.rs b/fathom/src/surface.rs
index 354a86c21..65c46b17d 100644
--- a/fathom/src/surface.rs
+++ b/fathom/src/surface.rs
@@ -93,7 +93,7 @@ pub enum Pattern<Range> {
     /// Boolean literal patterns
     BooleanLiteral(Range, bool),
     // TODO: Record literal patterns
-    // RecordLiteral(Range, &'arena [((Range, StringId), Pattern<'arena, Range>)]),
+    // RecordLiteral(Range, &'arena [((Range, Symbol), Pattern<'arena, Range>)]),
 }
 
 #[derive(Debug, Clone, Copy)]
diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs
index cf4a19466..3e5bd6071 100644
--- a/fathom/src/surface/elaboration.rs
+++ b/fathom/src/surface/elaboration.rs
@@ -26,7 +26,7 @@ use std::sync::Arc;
 use scoped_arena::Scope;
 
 use crate::alloc::SliceVec;
-use crate::core::semantics::{self, ArcValue, Head, Telescope, Value};
+use crate::core::semantics::{self, ArcValue, Head, LazyValue, LocalExprs, Telescope, Value};
 use crate::core::{self, prim, Const, Plicity, Prim, UIntStyle};
 use crate::env::{self, EnvLen, Level, SharedEnv, UniqueEnv};
 use crate::files::FileId;
@@ -48,7 +48,7 @@ pub struct ItemEnv<'arena> {
     /// Types of items.
     types: UniqueEnv<ArcValue<'arena>>,
     /// Expressions of items.
-    exprs: UniqueEnv<ArcValue<'arena>>,
+    exprs: UniqueEnv<LazyValue<'arena>>,
 }
 
 impl<'arena> ItemEnv<'arena> {
@@ -61,7 +61,7 @@ impl<'arena> ItemEnv<'arena> {
         }
     }
 
-    fn push_definition(&mut self, name: Symbol, r#type: ArcValue<'arena>, expr: ArcValue<'arena>) {
+    fn push_definition(&mut self, name: Symbol, r#type: ArcValue<'arena>, expr: LazyValue<'arena>) {
         self.names.push(name);
         self.types.push(r#type);
         self.exprs.push(expr);
@@ -97,7 +97,7 @@ struct LocalEnv<'arena> {
     infos: UniqueEnv<core::LocalInfo>,
     /// Expressions that will be substituted for local variables during
     /// [evaluation][semantics::EvalEnv::eval].
-    exprs: SharedEnv<ArcValue<'arena>>,
+    exprs: LocalExprs<'arena>,
 }
 
 impl<'arena> LocalEnv<'arena> {
@@ -124,22 +124,29 @@ impl<'arena> LocalEnv<'arena> {
     }
 
     /// Push a local definition onto the context.
-    fn push_def(&mut self, name: Option<Symbol>, expr: ArcValue<'arena>, r#type: ArcValue<'arena>) {
+    fn push_def(
+        &mut self,
+        name: Option<Symbol>,
+        expr: LazyValue<'arena>,
+        r#type: ArcValue<'arena>,
+    ) {
         self.names.push(name);
-        self.types.push(r#type);
         self.infos.push(core::LocalInfo::Def);
+        self.types.push(r#type);
         self.exprs.push(expr);
     }
 
     /// Push a local parameter onto the context.
-    fn push_param(&mut self, name: Option<Symbol>, r#type: ArcValue<'arena>) -> ArcValue<'arena> {
+    fn push_param(&mut self, name: Option<Symbol>, r#type: ArcValue<'arena>) -> LazyValue<'arena> {
         // An expression that refers to itself once it is pushed onto the local
         // expression environment.
-        let expr = Spanned::empty(Arc::new(Value::local_var(self.exprs.len().next_level())));
+        let expr = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.exprs.len().next_level(),
+        ))));
 
         self.names.push(name);
-        self.types.push(r#type);
         self.infos.push(core::LocalInfo::Param);
+        self.types.push(r#type);
         self.exprs.push(expr.clone());
 
         expr
@@ -255,9 +262,9 @@ pub struct Context<'arena> {
     scope: &'arena Scope<'arena>,
 
     // Commonly used values, cached to increase sharing.
-    universe: ArcValue<'static>,
-    format_type: ArcValue<'static>,
-    bool_type: ArcValue<'static>,
+    universe: ArcValue<'arena>,
+    format_type: ArcValue<'arena>,
+    bool_type: ArcValue<'arena>,
 
     /// Primitive environment.
     prim_env: prim::Env<'arena>,
@@ -418,7 +425,7 @@ impl<'arena> Context<'arena> {
         )
     }
 
-    fn pretty_value(&self, value: &ArcValue<'_>) -> String {
+    fn pretty_value(&self, value: &ArcValue<'arena>) -> String {
         let term = self.quote_env().unfolding_metas().quote(self.scope, value);
         let surface_term = self.distillation_context(self.scope).check(&term);
 
@@ -579,8 +586,8 @@ impl<'arena> Context<'arena> {
         to: &ArcValue<'arena>,
     ) -> core::Term<'arena> {
         let span = expr.span();
-        let from = self.elim_env().force(from);
-        let to = self.elim_env().force(to);
+        let from = self.elim_env().force_metas(from);
+        let to = self.elim_env().force_metas(to);
 
         match (from.as_ref(), to.as_ref()) {
             // Coerce format descriptions to their representation types by
@@ -638,7 +645,8 @@ impl<'arena> Context<'arena> {
                 Item::Def(item) => {
                     let (expr, r#type) =
                         self.synth_fun_lit(item.range, item.params, item.expr, item.r#type);
-                    let expr_value = self.eval_env().eval(&expr);
+                    let expr = self.scope.to_scope(expr);
+                    let expr_value = self.eval_env().delay(expr);
                     let type_value = self.eval_env().eval(&r#type);
 
                     self.item_env
@@ -647,7 +655,7 @@ impl<'arena> Context<'arena> {
                     items.push(core::Item::Def {
                         label: item.label.1,
                         r#type: self.scope.to_scope(r#type),
-                        expr: self.scope.to_scope(expr),
+                        expr,
                     });
                 }
                 Item::ReportedError(_) => {}
@@ -894,7 +902,7 @@ impl<'arena> Context<'arena> {
     fn push_local_def(
         &mut self,
         pattern: CheckedPattern,
-        expr: ArcValue<'arena>,
+        expr: LazyValue<'arena>,
         r#type: ArcValue<'arena>,
     ) -> Option<Symbol> {
         let name = match pattern {
@@ -921,7 +929,7 @@ impl<'arena> Context<'arena> {
         &mut self,
         pattern: CheckedPattern,
         r#type: ArcValue<'arena>,
-    ) -> (Option<Symbol>, ArcValue<'arena>) {
+    ) -> (Option<Symbol>, LazyValue<'arena>) {
         let name = match pattern {
             CheckedPattern::Binder(_, name) => Some(name),
             CheckedPattern::Placeholder(_) => None,
@@ -966,7 +974,7 @@ impl<'arena> Context<'arena> {
         expected_type: &ArcValue<'arena>,
     ) -> core::Term<'arena> {
         let file_range = self.file_range(surface_term.range());
-        let expected_type = self.elim_env().force(expected_type);
+        let expected_type = self.elim_env().force_metas(expected_type);
 
         match (surface_term, expected_type.as_ref()) {
             (Term::Paren(_, term), _) => self.check(term, &expected_type),
@@ -974,7 +982,8 @@ impl<'arena> Context<'arena> {
                 let (def_pattern, def_type, def_type_value) =
                     self.synth_ann_pattern(def_pattern, *def_type);
                 let def_expr = self.check(def_expr, &def_type_value);
-                let def_expr_value = self.eval_env().eval(&def_expr);
+                let def_expr = self.scope.to_scope(def_expr);
+                let def_expr_value = self.eval_env().delay(def_expr);
 
                 let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value); // TODO: split on constants
                 let body_expr = self.check(body_expr, &expected_type);
@@ -984,7 +993,7 @@ impl<'arena> Context<'arena> {
                     file_range.into(),
                     def_name,
                     self.scope.to_scope(def_type),
-                    self.scope.to_scope(def_expr),
+                    def_expr,
                     self.scope.to_scope(body_expr),
                 )
             }
@@ -1043,8 +1052,9 @@ impl<'arena> Context<'arena> {
                     let name_expr = Term::Name(expr_field.label.0, expr_field.label.1);
                     let expr = expr_field.expr.as_ref().unwrap_or(&name_expr);
                     let expr = self.check(expr, &r#type);
-                    types = next_types(self.eval_env().eval(&expr));
-                    exprs.push(expr);
+                    let expr = self.scope.to_scope(expr);
+                    types = next_types(self.eval_env().delay(expr));
+                    exprs.push(expr.clone());
                 }
 
                 core::Term::RecordLit(file_range.into(), labels, exprs.into())
@@ -1130,8 +1140,9 @@ impl<'arena> Context<'arena> {
                     Option::zip(elem_exprs.next(), self.elim_env().split_telescope(types))
                 {
                     let expr = self.check(elem_expr, &r#type);
-                    types = next_types(self.eval_env().eval(&expr));
-                    exprs.push(expr);
+                    let expr = self.scope.to_scope(expr);
+                    types = next_types(self.eval_env().delay(expr));
+                    exprs.push(expr.clone());
                 }
 
                 core::Term::RecordLit(file_range.into(), labels, exprs.into())
@@ -1165,7 +1176,10 @@ impl<'arena> Context<'arena> {
                     }
                 };
 
-                let len = match len_value.map(|val| val.as_ref()) {
+                let len_value = len_value.map(|len_value| self.elim_env().force_lazy(len_value));
+                let elem_type = self.elim_env().force_lazy(elem_type);
+
+                let len = match len_value.as_ref().map(|val| val.as_ref()) {
                     None => Some(elem_exprs.len() as u64),
                     Some(Value::ConstLit(Const::U8(len, _))) => Some(*len as u64),
                     Some(Value::ConstLit(Const::U16(len, _))) => Some(*len as u64),
@@ -1181,20 +1195,20 @@ impl<'arena> Context<'arena> {
                     Some(len) if elem_exprs.len() as u64 == len => core::Term::ArrayLit(
                         file_range.into(),
                         self.scope.to_scope_from_iter(
-                            (elem_exprs.iter()).map(|elem_expr| self.check(elem_expr, elem_type)),
+                            (elem_exprs.iter()).map(|elem_expr| self.check(elem_expr, &elem_type)),
                         ),
                     ),
                     _ => {
                         // Check the array elements anyway in order to report
                         // any errors inside the literal as well.
                         for elem_expr in *elem_exprs {
-                            self.check(elem_expr, elem_type);
+                            self.check(elem_expr, &elem_type);
                         }
 
                         self.push_message(Message::MismatchedArrayLength {
                             range: file_range,
                             found_len: elem_exprs.len(),
-                            expected_len: self.pretty_value(len_value.unwrap()),
+                            expected_len: self.pretty_value(&len_value.unwrap()),
                         });
 
                         core::Term::Prim(file_range.into(), Prim::ReportedError)
@@ -1275,17 +1289,18 @@ impl<'arena> Context<'arena> {
     ) -> (core::Term<'arena>, ArcValue<'arena>) {
         let file_range = self.file_range(range);
         while let Value::FunType(Plicity::Implicit, name, param_type, body_type) =
-            self.elim_env().force(&r#type).as_ref()
+            self.elim_env().force_metas(&r#type).as_ref()
         {
             let source = MetaSource::ImplicitArg(file_range, *name);
-            let arg_term = self.push_unsolved_term(source, param_type.clone());
-            let arg_value = self.eval_env().eval(&arg_term);
+            let arg_term = self.push_unsolved_term(source, self.elim_env().force_lazy(param_type));
+            let arg_term = self.scope.to_scope(arg_term);
+            let arg_value = self.eval_env().delay(arg_term);
 
             term = core::Term::FunApp(
                 file_range.into(),
                 Plicity::Implicit,
                 self.scope.to_scope(term),
-                self.scope.to_scope(arg_term),
+                arg_term,
             );
             r#type = self.elim_env().apply_closure(body_type, arg_value);
         }
@@ -1376,7 +1391,8 @@ impl<'arena> Context<'arena> {
                 let (def_pattern, def_type, def_type_value) =
                     self.synth_ann_pattern(def_pattern, *def_type);
                 let def_expr = self.check(def_expr, &def_type_value);
-                let def_expr_value = self.eval_env().eval(&def_expr);
+                let def_expr = self.scope.to_scope(def_expr);
+                let def_expr_value = self.eval_env().delay(def_expr);
 
                 let def_name = self.push_local_def(def_pattern, def_expr_value, def_type_value);
                 let (body_expr, body_type) = self.synth(body_expr);
@@ -1386,7 +1402,7 @@ impl<'arena> Context<'arena> {
                     file_range.into(),
                     def_name,
                     self.scope.to_scope(def_type),
-                    self.scope.to_scope(def_expr),
+                    def_expr,
                     self.scope.to_scope(body_expr),
                 );
 
@@ -1477,7 +1493,7 @@ impl<'arena> Context<'arena> {
                 let (mut head_expr, mut head_type) = self.synth(head_expr);
 
                 for arg in *args {
-                    head_type = self.elim_env().force(&head_type);
+                    head_type = self.elim_env().force_metas(&head_type);
 
                     match arg.plicity {
                         Plicity::Implicit => {}
@@ -1524,14 +1540,15 @@ impl<'arena> Context<'arena> {
                     let arg_range = arg.term.range();
                     head_range = ByteRange::merge(head_range, arg_range);
 
-                    let arg_expr = self.check(&arg.term, param_type);
-                    let arg_expr_value = self.eval_env().eval(&arg_expr);
+                    let arg_expr = self.check(&arg.term, &self.elim_env().force_lazy(param_type));
+                    let arg_expr = self.scope.to_scope(arg_expr);
+                    let arg_expr_value = self.eval_env().delay(arg_expr);
 
                     head_expr = core::Term::FunApp(
                         self.file_range(head_range).into(),
                         arg.plicity,
                         self.scope.to_scope(head_expr),
-                        self.scope.to_scope(arg_expr),
+                        arg_expr,
                     );
                     head_type = self.elim_env().apply_closure(body_type, arg_expr_value);
                 }
@@ -1601,7 +1618,7 @@ impl<'arena> Context<'arena> {
                 let (mut head_expr, mut head_type) = self.synth_and_insert_implicit_apps(head_expr);
 
                 'labels: for (label_range, proj_label) in *labels {
-                    head_type = self.elim_env().force(&head_type);
+                    head_type = self.elim_env().force_metas(&head_type);
                     match (&head_expr, head_type.as_ref()) {
                         // Ensure that the head of the projection is a record
                         (_, Value::RecordType(labels, types)) => {
@@ -1632,7 +1649,7 @@ impl<'arena> Context<'arena> {
                                     // looking for the field.
                                     let head_expr = head_expr_value.clone();
                                     let expr = self.elim_env().record_proj(head_expr, label);
-                                    types = next_types(expr);
+                                    types = next_types(LazyValue::eager(expr));
                                 }
                             }
                             // Couldn't find the field in the record type.
@@ -1726,16 +1743,17 @@ impl<'arena> Context<'arena> {
         let file_range = self.file_range(range);
         match params.split_first() {
             Some((param, next_params)) => {
-                let body_type = self.elim_env().force(expected_type);
+                let body_type = self.elim_env().force_metas(expected_type);
                 match body_type.as_ref() {
                     Value::FunType(param_plicity, _, param_type, next_body_type)
                         if param.plicity == *param_plicity =>
                     {
                         let range = ByteRange::merge(param.pattern.range(), body_expr.range());
+                        let param_type = self.elim_env().force_lazy(param_type);
                         let pattern = self.check_ann_pattern(
                             &param.pattern,
                             param.r#type.as_ref(),
-                            param_type,
+                            &param_type,
                         );
                         let (name, arg_expr) = self.push_local_param(pattern, param_type.clone());
 
@@ -1756,7 +1774,9 @@ impl<'arena> Context<'arena> {
                     Value::FunType(Plicity::Implicit, param_name, param_type, next_body_type)
                         if param.plicity == Plicity::Explicit =>
                     {
-                        let arg_expr = self.local_env.push_param(*param_name, param_type.clone());
+                        let arg_expr = self
+                            .local_env
+                            .push_param(*param_name, self.elim_env().force_lazy(param_type));
                         let body_type = self.elim_env().apply_closure(next_body_type, arg_expr);
                         let body_expr = self.check_fun_lit(range, params, body_expr, &body_type);
                         self.local_env.pop();
@@ -1857,8 +1877,8 @@ impl<'arena> Context<'arena> {
         // de-sugar into function application
         let (lhs_expr, lhs_type) = self.synth_and_insert_implicit_apps(lhs);
         let (rhs_expr, rhs_type) = self.synth_and_insert_implicit_apps(rhs);
-        let lhs_type = self.elim_env().force(&lhs_type);
-        let rhs_type = self.elim_env().force(&rhs_type);
+        let lhs_type = self.elim_env().force_metas(&lhs_type);
+        let rhs_type = self.elim_env().force_metas(&rhs_type);
         let operand_types = Option::zip(lhs_type.match_prim_spine(), rhs_type.match_prim_spine());
 
         let (fun, body_type) = match (op, operand_types) {
@@ -2200,7 +2220,7 @@ impl<'arena> Context<'arena> {
         let match_info = MatchInfo {
             range,
             scrutinee: self.synth_scrutinee(scrutinee_expr),
-            expected_type: self.elim_env().force(expected_type),
+            expected_type: self.elim_env().force_metas(expected_type),
         };
 
         self.elab_match(&match_info, true, equations.iter())
@@ -2238,7 +2258,7 @@ impl<'arena> Context<'arena> {
                         self.check_match_reachable(is_reachable, range);
 
                         let def_name = Some(name);
-                        let def_expr = self.eval_env().eval(match_info.scrutinee.expr);
+                        let def_expr = self.eval_env().delay(match_info.scrutinee.expr);
                         let def_type_value = match_info.scrutinee.r#type.clone();
                         let def_type = self.quote_env().quote(self.scope, &def_type_value);
 
diff --git a/fathom/src/surface/elaboration/unification.rs b/fathom/src/surface/elaboration/unification.rs
index 852c4e69a..b85a21658 100644
--- a/fathom/src/surface/elaboration/unification.rs
+++ b/fathom/src/surface/elaboration/unification.rs
@@ -21,7 +21,8 @@ use scoped_arena::Scope;
 
 use crate::alloc::SliceVec;
 use crate::core::semantics::{
-    self, ArcValue, Branches, Closure, Elim, Head, SplitBranches, Telescope, Value,
+    self, ArcValue, Branches, Closure, Elim, Head, ItemExprs, LazyValue, SplitBranches, Telescope,
+    Value,
 };
 use crate::core::{Prim, Term};
 use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv, UniqueEnv};
@@ -164,7 +165,7 @@ pub struct Context<'arena, 'env> {
     /// each call to [`Context::solve`] in order to reuse previous allocations.
     renaming: &'env mut PartialRenaming,
     /// Item expressions.
-    item_exprs: &'env SliceEnv<ArcValue<'arena>>,
+    item_exprs: &'env ItemExprs<'arena>,
     /// The length of the local environment.
     local_exprs: EnvLen,
     /// Solutions for metavariables.
@@ -175,7 +176,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
     pub fn new(
         scope: &'arena Scope<'arena>,
         renaming: &'env mut PartialRenaming,
-        item_exprs: &'env SliceEnv<ArcValue<'arena>>,
+        item_exprs: &'env ItemExprs<'arena>,
         local_exprs: EnvLen,
         meta_exprs: &'env mut SliceEnv<Option<ArcValue<'arena>>>,
     ) -> Context<'arena, 'env> {
@@ -203,8 +204,8 @@ impl<'arena, 'env> Context<'arena, 'env> {
             return Ok(());
         }
 
-        let value0 = self.elim_env().force(value0);
-        let value1 = self.elim_env().force(value1);
+        let value0 = self.elim_env().force_metas(value0);
+        let value1 = self.elim_env().force_metas(value1);
 
         match (value0.as_ref(), value1.as_ref()) {
             // `ReportedError`s result from errors that have already been
@@ -236,7 +237,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 Value::FunType(plicity0, _, param_type0, body_type0),
                 Value::FunType(plicity1, _, param_type1, body_type1),
             ) if plicity0 == plicity1 => {
-                self.unify(param_type0, param_type1)?;
+                self.unify_lazy(param_type0, param_type1)?;
                 self.unify_closures(body_type0, body_type1)
             }
             (Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1))
@@ -262,7 +263,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                     return Err(Error::Mismatch);
                 }
                 for (expr0, expr1) in Iterator::zip(exprs0.iter(), exprs1.iter()) {
-                    self.unify(expr0, expr1)?;
+                    self.unify_lazy(expr0, expr1)?;
                 }
                 Ok(())
             }
@@ -273,7 +274,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 for (elem_expr0, elem_expr1) in
                     Iterator::zip(elem_exprs0.iter(), elem_exprs1.iter())
                 {
-                    self.unify(elem_expr0, elem_expr1)?;
+                    self.unify_lazy(elem_expr0, elem_expr1)?;
                 }
                 Ok(())
             }
@@ -292,7 +293,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 if label0 != label1 {
                     return Err(Error::Mismatch);
                 }
-                self.unify(format0, format1)?;
+                self.unify_lazy(format0, format1)?;
                 self.unify_closures(cond0, cond1)
             }
 
@@ -309,6 +310,17 @@ impl<'arena, 'env> Context<'arena, 'env> {
         }
     }
 
+    pub fn unify_lazy(
+        &mut self,
+        value0: &LazyValue<'arena>,
+        value1: &LazyValue<'arena>,
+    ) -> Result<(), Error> {
+        self.unify(
+            &self.elim_env().force_lazy(value0),
+            &self.elim_env().force_lazy(value1),
+        )
+    }
+
     /// Unify two elimination spines.
     fn unify_spines(
         &mut self,
@@ -323,7 +335,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 (Elim::FunApp(plicity0, arg_expr0), Elim::FunApp(plicity1, arg_expr1))
                     if plicity0 == plicity1 =>
                 {
-                    self.unify(arg_expr0, arg_expr1)?;
+                    self.unify_lazy(arg_expr0, arg_expr1)?;
                 }
                 (Elim::RecordProj(label0), Elim::RecordProj(label1)) if label0 == label1 => {}
                 (Elim::ConstMatch(branches0), Elim::ConstMatch(branches1)) => {
@@ -343,7 +355,9 @@ impl<'arena, 'env> Context<'arena, 'env> {
         closure0: &Closure<'arena>,
         closure1: &Closure<'arena>,
     ) -> Result<(), Error> {
-        let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level())));
+        let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.local_exprs.next_level(),
+        ))));
         let value0 = self.elim_env().apply_closure(closure0, var.clone());
         let value1 = self.elim_env().apply_closure(closure1, var);
 
@@ -377,7 +391,9 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 return Err(error);
             }
 
-            let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level())));
+            let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+                self.local_exprs.next_level(),
+            ))));
             telescope0 = next_telescope0(var.clone());
             telescope1 = next_telescope1(var);
             self.local_exprs.push();
@@ -433,8 +449,10 @@ impl<'arena, 'env> Context<'arena, 'env> {
         body_expr: &Closure<'arena>,
         value: &ArcValue<'arena>,
     ) -> Result<(), Error> {
-        let var = Spanned::empty(Arc::new(Value::local_var(self.local_exprs.next_level())));
-        let value = self.elim_env().fun_app(plicity, value.clone(), var.clone());
+        let var = LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.local_exprs.next_level(),
+        ))));
+        let value = self.elim_env().fun_app(plicity, value.clone(), &var);
         let body_expr = self.elim_env().apply_closure(body_expr, var);
 
         self.local_exprs.push();
@@ -452,12 +470,12 @@ impl<'arena, 'env> Context<'arena, 'env> {
     fn unify_record_lit(
         &mut self,
         labels: &[Symbol],
-        exprs: &[ArcValue<'arena>],
+        exprs: &[LazyValue<'arena>],
         value: &ArcValue<'arena>,
     ) -> Result<(), Error> {
         for (label, expr) in Iterator::zip(labels.iter(), exprs.iter()) {
             let field_value = self.elim_env().record_proj(value.clone(), *label);
-            self.unify(expr, &field_value)?;
+            self.unify(&self.elim_env().force_lazy(expr), &field_value)?;
         }
         Ok(())
     }
@@ -499,14 +517,17 @@ impl<'arena, 'env> Context<'arena, 'env> {
 
         for elim in spine {
             match elim {
-                Elim::FunApp(_, arg_expr) => match self.elim_env().force(arg_expr).as_ref() {
-                    Value::Stuck(Head::LocalVar(source_var), spine)
-                        if spine.is_empty() && self.renaming.set_local(*source_var) => {}
-                    Value::Stuck(Head::LocalVar(source_var), _) => {
-                        return Err(SpineError::NonLinearSpine(*source_var))
+                Elim::FunApp(_, arg_expr) => {
+                    let arg_expr = self.elim_env().force_lazy(arg_expr);
+                    match self.elim_env().force_metas(&arg_expr).as_ref() {
+                        Value::Stuck(Head::LocalVar(source_var), spine)
+                            if spine.is_empty() && self.renaming.set_local(*source_var) => {}
+                        Value::Stuck(Head::LocalVar(source_var), _) => {
+                            return Err(SpineError::NonLinearSpine(*source_var))
+                        }
+                        _ => return Err(SpineError::NonLocalFunApp),
                     }
-                    _ => return Err(SpineError::NonLocalFunApp),
-                },
+                }
                 Elim::RecordProj(label) => return Err(SpineError::RecordProj(*label)),
                 Elim::ConstMatch(_) => return Err(SpineError::ConstMatch),
             }
@@ -541,7 +562,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
         meta_var: Level,
         value: &ArcValue<'arena>,
     ) -> Result<Term<'arena>, RenameError> {
-        let val = self.elim_env().force(value);
+        let val = self.elim_env().force_metas(value);
         let span = val.span();
         match val.as_ref() {
             Value::Stuck(head, spine) => {
@@ -563,7 +584,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                             span,
                             *plicity,
                             self.scope.to_scope(head_expr),
-                            self.scope.to_scope(self.rename(meta_var, arg_expr)?),
+                            self.scope.to_scope(self.rename_lazy(meta_var, arg_expr)?),
                         ),
                         Elim::RecordProj(label) => {
                             Term::RecordProj(span, self.scope.to_scope(head_expr), *label)
@@ -605,7 +626,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
             Value::Universe => Ok(Term::Universe(span)),
 
             Value::FunType(plicity, param_name, param_type, body_type) => {
-                let param_type = self.rename(meta_var, param_type)?;
+                let param_type = self.rename_lazy(meta_var, param_type)?;
                 let body_type = self.rename_closure(meta_var, body_type)?;
 
                 Ok(Term::FunType(
@@ -635,7 +656,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
             Value::RecordLit(labels, exprs) => {
                 let mut new_exprs = SliceVec::new(self.scope, exprs.len());
                 for expr in exprs {
-                    new_exprs.push(self.rename(meta_var, expr)?);
+                    new_exprs.push(self.rename_lazy(meta_var, expr)?);
                 }
 
                 Ok(Term::RecordLit(span, labels, new_exprs.into()))
@@ -644,7 +665,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
             Value::ArrayLit(elem_exprs) => {
                 let mut new_elem_exprs = SliceVec::new(self.scope, elem_exprs.len());
                 for elem_expr in elem_exprs {
-                    new_elem_exprs.push(self.rename(meta_var, elem_expr)?);
+                    new_elem_exprs.push(self.rename_lazy(meta_var, elem_expr)?);
                 }
 
                 Ok(Term::ArrayLit(span, new_elem_exprs.into()))
@@ -656,7 +677,7 @@ impl<'arena, 'env> Context<'arena, 'env> {
                 Ok(Term::FormatRecord(span, labels, formats))
             }
             Value::FormatCond(label, format, cond) => {
-                let format = self.rename(meta_var, format)?;
+                let format = self.rename_lazy(meta_var, format)?;
                 let cond = self.rename_closure(meta_var, cond)?;
                 Ok(Term::FormatCond(
                     span,
@@ -675,6 +696,14 @@ impl<'arena, 'env> Context<'arena, 'env> {
         }
     }
 
+    fn rename_lazy(
+        &mut self,
+        meta_var: Level,
+        value: &LazyValue<'arena>,
+    ) -> Result<Term<'arena>, RenameError> {
+        self.rename(meta_var, &self.elim_env().force_lazy(value))
+    }
+
     /// Rename a closure back into a [`Term`].
     fn rename_closure(
         &mut self,
@@ -747,8 +776,10 @@ impl PartialRenaming {
         self.target.clear();
     }
 
-    fn next_local_var<'arena>(&self) -> ArcValue<'arena> {
-        Spanned::empty(Arc::new(Value::local_var(self.source.len().next_level())))
+    fn next_local_var<'arena>(&self) -> LazyValue<'arena> {
+        LazyValue::eager(Spanned::empty(Arc::new(Value::local_var(
+            self.source.len().next_level(),
+        ))))
     }
 
     /// Set a local source variable to local target variable mapping, ensuring