diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs
index 5be7f9dbe..2440e6f51 100644
--- a/fathom/src/core/semantics.rs
+++ b/fathom/src/core/semantics.rs
@@ -953,19 +953,14 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> {
                 // The metavariable has a solution, so unfold it.
                 Some(value) => TermOrValue::Value(value.clone()),
                 // No solution was found for the metavariable.
-                // NOTE: We might want to replace this with `ReportedError`.
-                None => TermOrValue::Term(Term::MetaVar(*span, *var)),
+                None => TermOrValue::Term(Term::Prim(*span, Prim::ReportedError)),
             },
             Term::InsertedMeta(span, var, infos) => {
                 match self.elim_env.get_meta_expr(*var) {
                     // The metavariable has a solution, so unfold it.
                     Some(value) => TermOrValue::Value(self.apply_local_infos(value.clone(), infos)),
                     // No solution was found for the metavariable.
-                    // NOTE: We might want to replace this with `ReportedError`.
-                    None => {
-                        let infos = scope.to_scope_from_iter(infos.iter().copied());
-                        TermOrValue::Term(Term::InsertedMeta(*span, *var, infos))
-                    }
+                    None => TermOrValue::Term(Term::Prim(*span, Prim::ReportedError)),
                 }
             }
 
diff --git a/fathom/src/env.rs b/fathom/src/env.rs
index e4775e146..38fffcef1 100644
--- a/fathom/src/env.rs
+++ b/fathom/src/env.rs
@@ -319,6 +319,11 @@ impl<Entry> SharedEnv<Entry> {
         }
     }
 
+    /// Clear the renaming. This is useful for reusing environment allocations.
+    pub fn clear(&mut self) {
+        self.truncate(EnvLen(0));
+    }
+
     /// The length of the environment.
     pub fn len(&self) -> EnvLen {
         // SAFETY:
diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs
index cf4a19466..7786abd68 100644
--- a/fathom/src/surface/elaboration.rs
+++ b/fathom/src/surface/elaboration.rs
@@ -160,6 +160,13 @@ impl<'arena> LocalEnv<'arena> {
         self.infos.truncate(len);
         self.exprs.truncate(len);
     }
+
+    fn clear(&mut self) {
+        self.names.clear();
+        self.types.clear();
+        self.infos.clear();
+        self.exprs.clear();
+    }
 }
 
 /// The reason why a metavariable was inserted.
@@ -242,6 +249,12 @@ impl<'arena> MetaEnv<'arena> {
 
         var
     }
+
+    fn clear(&mut self) {
+        self.sources.clear();
+        self.types.clear();
+        self.exprs.clear();
+    }
 }
 
 /// Elaboration context.
@@ -630,7 +643,7 @@ impl<'arena> Context<'arena> {
         on_message: &mut dyn FnMut(Message),
     ) -> core::Module<'out_arena> {
         let elab_order = order::elaboration_order(self, surface_module);
-        let mut items = Vec::with_capacity(surface_module.items.len());
+        let mut items = SliceVec::new(scope, surface_module.items.len());
         self.item_env.reserve(surface_module.items.len());
 
         for item in elab_order.iter().copied().map(|i| &surface_module.items[i]) {
@@ -638,47 +651,45 @@ 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 (r#type, expr) = {
+                        let scope = self.scope;
+                        let mut eval_env = self.eval_env();
+                        let r#type = eval_env.unfold_metas(scope, &r#type);
+                        let expr = eval_env.unfold_metas(scope, &expr);
+                        (r#type, expr)
+                    };
+
                     let expr_value = self.eval_env().eval(&expr);
                     let type_value = self.eval_env().eval(&r#type);
 
+                    let r#type = self.eval_env().unfold_metas(scope, &r#type);
+                    let expr = self.eval_env().unfold_metas(scope, &expr);
+
+                    self.handle_messages(on_message);
+                    self.local_env.clear();
+                    self.meta_env.clear();
+                    self.renaming.clear();
+
                     self.item_env
                         .push_definition(item.label.1, type_value, expr_value);
 
                     items.push(core::Item::Def {
                         label: item.label.1,
-                        r#type: self.scope.to_scope(r#type),
-                        expr: self.scope.to_scope(expr),
+                        r#type: scope.to_scope(r#type),
+                        expr: scope.to_scope(expr),
                     });
                 }
                 Item::ReportedError(_) => {}
             }
         }
 
-        // Unfold all unification solutions
-        let items = scope.to_scope_from_iter(items.into_iter().map(|item| match item {
-            core::Item::Def {
-                label,
-                r#type,
-                expr,
-            } => {
-                // TODO: Unfold unsolved metas to reported errors
-                let r#type = self.eval_env().unfold_metas(scope, r#type);
-                let expr = self.eval_env().unfold_metas(scope, expr);
-
-                core::Item::Def {
-                    label,
-                    r#type: scope.to_scope(r#type),
-                    expr: scope.to_scope(expr),
-                }
-            }
-        }));
-
-        self.handle_messages(on_message);
-
         // TODO: Clear environments
         // TODO: Reset scopes
 
-        core::Module { items }
+        core::Module {
+            items: items.into(),
+        }
     }
 
     /// Elaborate a term, returning its synthesized type.
diff --git a/fathom/src/surface/elaboration/unification.rs b/fathom/src/surface/elaboration/unification.rs
index 852c4e69a..c867074bf 100644
--- a/fathom/src/surface/elaboration/unification.rs
+++ b/fathom/src/surface/elaboration/unification.rs
@@ -804,4 +804,9 @@ impl PartialRenaming {
         self.source.truncate(len.0);
         self.target.truncate(len.1);
     }
+
+    pub fn clear(&mut self) {
+        self.source.clear();
+        self.target.clear();
+    }
 }
diff --git a/tests/fail/elaboration/local-metavars.fathom b/tests/fail/elaboration/local-metavars.fathom
new file mode 100644
index 000000000..f3c2c07b0
--- /dev/null
+++ b/tests/fail/elaboration/local-metavars.fathom
@@ -0,0 +1,11 @@
+//~ exit-code = 1
+//~ mode = "module"
+
+// metavars in `f` are updated by type annotation because whole expression is contained in one def
+def h =
+    let f = fun x => x;
+    f : U32 -> U32;
+
+// metavars in `f` are not updated by type annotated in `g` becaues they are in different defs
+def f = fun x => x;
+def g : U32 -> U32 = f;
diff --git a/tests/fail/elaboration/local-metavars.snap b/tests/fail/elaboration/local-metavars.snap
new file mode 100644
index 000000000..679132a03
--- /dev/null
+++ b/tests/fail/elaboration/local-metavars.snap
@@ -0,0 +1,9 @@
+stdout = ''
+stderr = '''
+error: failed to infer named pattern type
+   ┌─ tests/fail/elaboration/local-metavars.fathom:10:13
+   │
+10 │ def f = fun x => x;
+   │             ^ unsolved named pattern type
+
+'''