Scope each metavar to the definition where it was generated

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)),
                 }
             }
 

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:

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,55 +643,53 @@ 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]) {
             match item {
                 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.

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();
+    }
 }

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;

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
+
+'''