Remember variable names in typechecking result

src/analyses/compare.rs

@@ -35,8 +35,14 @@ impl<'a> ComparisonState<'a> {
                     remaining_pat_depth: remaining,
                     remaining_ty_depth: self.remaining_ty_depth,
                     req: self.req.subst_pat(a, pat),
-                    left_state: self.left_state.map_continue(|pred| pred.subst_pat(a, pat)),
-                    right_state: self.right_state.map_continue(|pred| pred.subst_pat(a, pat)),
+                    left_state: self
+                        .left_state
+                        .clone()
+                        .map_continue(|pred| pred.subst_pat(a, pat)),
+                    right_state: self
+                        .right_state
+                        .clone()
+                        .map_continue(|pred| pred.subst_pat(a, pat)),
                 })
                 .collect(),
         }
@@ -55,10 +61,12 @@ impl<'a> ComparisonState<'a> {
                     req: self.req.subst_ty(a, ty),
                     left_state: self
                         .left_state
+                        .clone()
                         .map_continue(|pred| pred.subst_ty(a, ty))
                         .map_break(|res| res.subst_ty(a, ty)),
                     right_state: self
                         .right_state
+                        .clone()
                         .map_continue(|pred| pred.subst_ty(a, ty))
                         .map_break(|res| res.subst_ty(a, ty)),
                 })
@@ -90,12 +98,16 @@ impl<'a> ComparisonState<'a> {
                         Ok((_rule, next)) => {
                             if next.is_empty() {
                                 let ty = *pred.expr.ty;
+                                let Pattern::Binding(_, _, name) = pred.pat else {
+                                    unreachable!()
+                                };
+                                let bindings = BindingAssignments::new([(*name, ty)]);
                                 match pred.expr.simplify(ctx).borrow_check() {
                                     Err(BorrowCheckError::OverlyGeneral(deepening)) => {
                                         return Some(deepening)
                                     }
-                                    Err(err) => Break(BorrowError(ty, err)),
-                                    Ok(_) => Break(Success(ty)),
+                                    Err(err) => Break(BorrowError(bindings, err)),
+                                    Ok(_) => Break(Success(bindings)),
                                 }
                             } else {
                                 assert_eq!(next.len(), 1); // we only deepen with arity-1 tuples
@@ -151,16 +163,16 @@ pub fn compare_rulesets<'a>(
         remaining_pat_depth: pat_depth + 1,
         remaining_ty_depth: ty_depth + 1,
         req,
-        left_state: start_state,
+        left_state: start_state.clone(),
         right_state: start_state,
     }];
     let mut complete = vec![];
     while !states.is_empty() {
         for mut state in mem::take(&mut states) {
             // Deepen each state until either completion or deepening is required.
             let opt_deepen = state.step(a, left_ruleset, right_ruleset);
-            let left_res = state.left_state;
-            let right_res = state.right_state;
+            let left_res = &state.left_state;
+            let right_res = &state.right_state;
             // No need to continue if one side already errored as expected.
             match expected_order {
                 Less if matches!(left_res, Break(TypeError(_) | BorrowError(..))) => continue,
@@ -170,24 +182,24 @@ pub fn compare_rulesets<'a>(
             match opt_deepen {
                 None => {
                     // No deepening required, hence this is a concrete predicate or both errored.
-                    let left_res = left_res.break_value().unwrap();
-                    let right_res = right_res.break_value().unwrap();
+                    let left_res = state.left_state.break_value().unwrap();
+                    let right_res = state.right_state.break_value().unwrap();
                     // Skip if the results match.
-                    match (left_res, right_res) {
-                        (Success(lty), Success(rty)) if lty == rty => continue,
+                    match (&left_res, &right_res) {
+                        (Success(ltys), Success(rtys)) if ltys == rtys => continue,
                         (TypeError(_) | BorrowError(..), TypeError(_) | BorrowError(..)) => {
                             continue
                         }
                         // These borrow errors only come from this solver, whose borrow checker is
                         // more accurate than the other. Hence if both agree on types we ignore the
                         // borrowck error.
-                        (BorrowError(lty, _), Success(rty))
-                            if right_ruleset.is_bm_based() && lty == rty =>
+                        (BorrowError(ltys, _), Success(rtys))
+                            if right_ruleset.is_bm_based() && ltys == rtys =>
                         {
                             continue
                         }
-                        (Success(lty), BorrowError(rty, _))
-                            if left_ruleset.is_bm_based() && lty == rty =>
+                        (Success(ltys), BorrowError(rtys, _))
+                            if left_ruleset.is_bm_based() && ltys == rtys =>
                         {
                             continue
                         }

src/analyses/explore/deepen.rs

@@ -27,7 +27,7 @@ impl<'a> Pattern<'a> {
                     };
                     let subpats = subnames
                         .iter()
-                        .map(|name| Pattern::Abstract(a.bump.alloc_str(name)));
+                        .map(|name| Pattern::Abstract(a.alloc_str(name)));
                     Pattern::Tuple(a.bump.alloc_slice_fill_iter(subpats))
                 };
                 [tuple]
@@ -81,7 +81,7 @@ impl<'a> Type<'a> {
                 } else {
                     // In `!many` mode, we directly expand an abstract type into a tuple or a leaf
                     // type.
-                    out.insert(0, Type::OtherNonRef(a.bump.alloc_str(&format!("C{name}"))));
+                    out.insert(0, Type::OtherNonRef(a.alloc_str(&format!("C{name}"))));
                     out.push(Type::Tuple(std::slice::from_ref(self)));
                 }
                 out
@@ -93,7 +93,7 @@ impl<'a> Type<'a> {
                     let subnames: &[&str] = &[&(name.to_string() + "0"), &(name.to_string() + "1")];
                     let subtypes = subnames
                         .iter()
-                        .map(|name| Type::Abstract(a.bump.alloc_str(&name)));
+                        .map(|name| Type::Abstract(a.alloc_str(&name)));
                     vec![Type::Tuple(a.bump.alloc_slice_fill_iter(subtypes))]
                 } else {
                     panic!("unexpected `AbstractNonRef`")

src/analyses/explore/subst.rs

@@ -87,13 +87,28 @@ impl<'a> TypingPredicate<'a> {
     }
 }
 
+impl<'a> BindingAssignments<'a> {
+    /// Replace the abstract types (if any) with the given type.
+    pub fn subst_ty(&self, a: &'a Arenas<'a>, replace: Type<'a>) -> Self {
+        Self {
+            assignments: self
+                .assignments
+                .iter()
+                .map(|(name, ty)| (*name, ty.subst(a, replace)))
+                .collect(),
+        }
+    }
+}
+
 impl<'a> TypingResult<'a> {
     /// Replace the abstract types (if any) with the given type.
     pub fn subst_ty(&self, a: &'a Arenas<'a>, replace: Type<'a>) -> Self {
-        match *self {
-            TypingResult::Success(ty) => TypingResult::Success(ty.subst(a, replace)),
-            TypingResult::BorrowError(ty, e) => TypingResult::BorrowError(ty.subst(a, replace), e),
-            TypingResult::TypeError(_) => *self,
+        match self {
+            TypingResult::Success(bindings) => TypingResult::Success(bindings.subst_ty(a, replace)),
+            TypingResult::BorrowError(bindings, e) => {
+                TypingResult::BorrowError(bindings.subst_ty(a, replace), *e)
+            }
+            TypingResult::TypeError(e) => TypingResult::TypeError(*e),
         }
     }
 }

src/ast/parser.rs

@@ -126,7 +126,7 @@ where
         .followed_by(multispace0)
         .map(|((mtbl, mode), name)| {
             // Cheat: allow parsing an abstract pattern for debugging purposes.
-            let name = ctx.bump.alloc_str(name);
+            let name = ctx.alloc_str(name);
             if name.starts_with("ap") {
                 Pattern::Abstract(name)
             } else {
@@ -199,7 +199,7 @@ where
 {
     let ident = take_while(|c: char| c.is_alphanumeric() || c == '_');
     ident.followed_by(multispace0).map(|name| {
-        let name = ctx.bump.alloc_str(name);
+        let name = ctx.alloc_str(name);
         // Cheat: allow parsing an abstract type for debugging purposes.
         if name.starts_with("AT") {
             Type::Abstract(name)

src/ast/printer.rs

@@ -297,11 +297,26 @@ impl Display for PredicateStyle {
     }
 }
 
+impl std::fmt::Display for BindingAssignments<'_> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(
+            f,
+            "{}",
+            self.assignments
+                .iter()
+                .map(|(name, ty)| format!("{name}: {ty}"))
+                .format(", ")
+        )
+    }
+}
+
 impl std::fmt::Display for TypingResult<'_> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let out = match self {
-            TypingResult::Success(ty) => format!("Success({ty})").green(),
-            TypingResult::BorrowError(ty, s) => format!("BorrowError({ty:?}, \"{s:?}\")").red(),
+            TypingResult::Success(bindings) => format!("Success({bindings})").green(),
+            TypingResult::BorrowError(bindings, s) => {
+                format!("BorrowError({bindings}, \"{s:?}\")").red()
+            }
             TypingResult::TypeError(TypeError::External(e)) => format!("TypeError(\"{e}\")").red(),
             TypingResult::TypeError(e) => format!("TypeError(\"{e:?}\")").red(),
         };

src/ast/types.rs

@@ -169,6 +169,11 @@ pub struct Arenas<'a> {
     phantom: PhantomData<&'a ()>,
 }
 
+impl<'a> Arenas<'a> {
+    pub fn alloc_str(&'a self, s: &str) -> &'a str {
+        self.bump.alloc_str(s)
+    }
+}
 impl<'a> Pattern<'a> {
     pub fn alloc(self, arenas: &'a Arenas<'a>) -> &'a Self {
         arenas.bump.alloc(self)

src/solvers/bm_based.rs

@@ -137,7 +137,12 @@ pub fn typecheck_with_formality<'a>(
     let stmt = req.to_bm_based();
     let r = Reduction::from_stmt(conf, stmt);
     match r.to_type() {
-        Ok((_ident, ty)) => Success(Type::from_bm_based(a, &ty)),
+        Ok((ident, ty)) => {
+            let ty = Type::from_bm_based(a, &ty);
+            let name = a.alloc_str(&ident.name);
+            let bindings = BindingAssignments::new([(name, ty)]);
+            Success(bindings)
+        }
         Err(e) => TypingResult::TypeError(TypeError::External(e)),
     }
 }

src/solvers/mod.rs

@@ -1,3 +1,5 @@
+use std::collections::BTreeMap;
+
 use crate::*;
 
 mod analysis;
@@ -10,10 +12,23 @@ pub use bm_based::*;
 pub use ty_based::*;
 pub use typing_rules::*;
 
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct BindingAssignments<'a> {
+    pub assignments: BTreeMap<&'a str, Type<'a>>,
+}
+
+impl<'a> BindingAssignments<'a> {
+    pub fn new(assignments: impl IntoIterator<Item = (&'a str, Type<'a>)>) -> Self {
+        Self {
+            assignments: assignments.into_iter().collect(),
+        }
+    }
+}
+
+#[derive(Debug, Clone)]
 pub enum TypingResult<'a> {
-    Success(Type<'a>),
-    BorrowError(Type<'a>, BorrowCheckError),
+    Success(BindingAssignments<'a>),
+    BorrowError(BindingAssignments<'a>, BorrowCheckError),
     TypeError(TypeError),
 }
 

src/solvers/ty_based.rs

@@ -139,10 +139,16 @@ pub fn typecheck_with_this_crate<'a>(
             assert_eq!(solver.done_predicates.len(), 1);
             let pred = solver.done_predicates[0];
             let ty = *pred.expr.ty;
+            let Pattern::Binding(_, _, name) = pred.pat else {
+                unreachable!()
+            };
+            let bindings = BindingAssignments::new([(*name, ty)]);
             match pred.expr.simplify(ctx).borrow_check() {
                 // This error isn't handled by `match-ergo-formality` so we ignore it.
-                Ok(()) | Err(BorrowCheckError::CantCopyNestedRefMut) => TypingResult::Success(ty),
-                Err(err) => TypingResult::BorrowError(ty, err),
+                Ok(()) | Err(BorrowCheckError::CantCopyNestedRefMut) => {
+                    TypingResult::Success(bindings)
+                }
+                Err(err) => TypingResult::BorrowError(bindings, err),
             }
         }
         CantStep::NoApplicableRule(_, err) => TypingResult::TypeError(err),