diff --git a/explorer/ast/bindings.cpp b/explorer/ast/bindings.cpp
index 3260568e7577..27ce42a9915e 100644
--- a/explorer/ast/bindings.cpp
+++ b/explorer/ast/bindings.cpp
@@ -37,23 +37,39 @@ void Bindings::Add(Nonnull<const GenericBinding*> binding,
   }
 }
 
+void Bindings::Print(llvm::raw_ostream& out) const {
+  std::vector<std::pair<Nonnull<const GenericBinding*>, Nonnull<const Value*>>>
+      args(args_.begin(), args_.end());
+
+  std::vector<std::pair<Nonnull<const ImplBinding*>, Nonnull<const Value*>>>
+      witnesses(witnesses_.begin(), witnesses_.end());
+
+  std::stable_sort(args.begin(), args.end(), [](const auto& a, const auto& b) {
+    return a.first->index() < b.first->index();
+  });
+
+  std::stable_sort(
+      witnesses.begin(), witnesses.end(), [](const auto& a, const auto& b) {
+        return a.first->type_var()->index() < b.first->type_var()->index();
+      });
+
+  llvm::ListSeparator sep;
+  out << " >  bindings args: [";
+  for (const auto& [binding, value] : args) {
+    out << sep << "`" << *binding << "`: `" << *value << "`";
+  }
+  out << "]\n >  bindings witnesses: [";
+  for (const auto& [binding, value] : witnesses) {
+    out << sep << "`" << *binding << "`: `" << *value << "`";
+  }
+  out << "]";
+};
+
 auto Bindings::None() -> Nonnull<const Bindings*> {
   static Nonnull<const Bindings*> bindings = new Bindings;
   return bindings;
 }
 
-void Bindings::Print(llvm::raw_ostream& out) const {
-  out << "{";
-  llvm::ListSeparator sep;
-  for (const auto& [name, value] : args_) {
-    out << sep << *name << " -> " << *value;
-  }
-  for (const auto& [name, value] : witnesses_) {
-    out << sep << *name << " -> " << *value;
-  }
-  out << "}";
-}
-
 auto Bindings::SymbolicIdentity(
     Nonnull<Arena*> arena,
     llvm::ArrayRef<Nonnull<const GenericBinding*>> bindings)
diff --git a/explorer/ast/bindings.h b/explorer/ast/bindings.h
index 3d6fd07a18b0..afc210f561a7 100644
--- a/explorer/ast/bindings.h
+++ b/explorer/ast/bindings.h
@@ -8,9 +8,11 @@
 #include <map>
 #include <utility>
 
+#include "common/ostream.h"
 #include "explorer/ast/clone_context.h"
 #include "explorer/common/nonnull.h"
 #include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/StringExtras.h"
 
 namespace Carbon {
 
diff --git a/explorer/ast/pattern.h b/explorer/ast/pattern.h
index ee39270c067a..fe2934b1b79a 100644
--- a/explorer/ast/pattern.h
+++ b/explorer/ast/pattern.h
@@ -9,6 +9,7 @@
 #include <string>
 #include <vector>
 
+#include "common/check.h"
 #include "common/ostream.h"
 #include "explorer/ast/ast_node.h"
 #include "explorer/ast/ast_rtti.h"
@@ -299,7 +300,10 @@ class GenericBinding : public Pattern {
 
   // The index of this binding, which is the number of bindings that are in
   // scope at the point where this binding is declared.
-  auto index() const -> int { return *index_; }
+  auto index() const -> int {
+    CARBON_CHECK(index_);
+    return *index_;
+  }
 
   // Set the index of this binding. Should be called only during type-checking.
   void set_index(int index) {
diff --git a/explorer/interpreter/impl_scope.cpp b/explorer/interpreter/impl_scope.cpp
index d6e29f71adab..6470d7237d8f 100644
--- a/explorer/interpreter/impl_scope.cpp
+++ b/explorer/interpreter/impl_scope.cpp
@@ -415,10 +415,11 @@ auto ImplScope::TryResolveInterfaceHere(
 
 // TODO: Add indentation when printing the parents.
 void ImplScope::Print(llvm::raw_ostream& out) const {
-  out << "impl declarations: ";
-  llvm::ListSeparator sep;
+  llvm::ListSeparator sep(",\n    ");
+  out << " +  "
+      << "[";
   for (const ImplFact& impl : impl_facts_) {
-    out << sep << *(impl.type) << " as " << *(impl.interface);
+    out << sep << "`" << *(impl.type) << "` as `" << *(impl.interface) << "`";
     if (impl.sort_key) {
       out << " " << *impl.sort_key;
     }
@@ -427,10 +428,10 @@ void ImplScope::Print(llvm::raw_ostream& out) const {
     out << sep;
     llvm::ListSeparator equal(" == ");
     for (Nonnull<const Value*> value : eq->values) {
-      out << equal << *value;
+      out << equal << "`" << *value << "`";
     }
   }
-  out << "\n";
+  out << "]\n";
   if (parent_scope_) {
     out << **parent_scope_;
   }
diff --git a/explorer/interpreter/type_checker.cpp b/explorer/interpreter/type_checker.cpp
index 0569ac68fde7..0deb8f6f1379 100644
--- a/explorer/interpreter/type_checker.cpp
+++ b/explorer/interpreter/type_checker.cpp
@@ -4,7 +4,6 @@
 
 #include "explorer/interpreter/type_checker.h"
 
-#include <algorithm>
 #include <deque>
 #include <iterator>
 #include <map>
@@ -13,7 +12,6 @@
 #include <string>
 #include <string_view>
 #include <tuple>
-#include <unordered_set>
 #include <vector>
 
 #include "common/check.h"
@@ -26,7 +24,6 @@
 #include "explorer/ast/value_transform.h"
 #include "explorer/common/arena.h"
 #include "explorer/common/error_builders.h"
-#include "explorer/common/nonnull.h"
 #include "explorer/common/source_location.h"
 #include "explorer/common/trace_stream.h"
 #include "explorer/interpreter/impl_scope.h"
@@ -35,8 +32,6 @@
 #include "explorer/interpreter/pattern_match.h"
 #include "explorer/interpreter/type_structure.h"
 #include "explorer/interpreter/type_utils.h"
-#include "llvm/ADT/DenseSet.h"
-#include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/ScopeExit.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/ADT/TinyPtrVector.h"
@@ -591,8 +586,8 @@ auto TypeChecker::BuildBuiltinConversion(Nonnull<Expression*> source,
   Nonnull<const Value*> source_type = &source->static_type();
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "building builtin conversion from " << *source_type
-                   << " to " << *destination << "\n";
+    *trace_stream_ << "*** building builtin conversion from `" << *source_type
+                   << "` to `" << *destination << "`\n";
   }
 
   // Build a simple conversion that the interpreter can perform directly.
@@ -827,9 +822,10 @@ auto TypeChecker::ImplicitlyConvert(std::string_view context,
     destination = destination_constraint;
 
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "converting type " << *converted_value
-                     << " to constraint " << *destination_constraint << " for "
-                     << context << " in scope " << impl_scope << "\n";
+      *trace_stream_ << "converting type `" << *converted_value
+                     << "` to constraint `" << *destination_constraint
+                     << "` for " << context << " in scope:\n"
+                     << impl_scope << "\n";
     }
     // Note, we discard the witness. We don't actually need it in order to
     // perform the conversion, but we do want to know it exists.
@@ -903,7 +899,8 @@ auto TypeChecker::IsIntrinsicConstraintSatisfied(
                               constraint.arguments[0], impl_scope,
                               /*allow_user_defined_conversions=*/true));
       if (trace_stream_->is_enabled()) {
-        *trace_stream_ << constraint << " evaluated to " << convertible << "\n";
+        *trace_stream_ << "--- `" << constraint << "` evaluated to `"
+                       << convertible << "`\n";
       }
       return convertible;
   }
@@ -1026,12 +1023,12 @@ class TypeChecker::ArgumentDeduction {
         deduced_bindings_in_order_(bindings_to_deduce),
         trace_stream_(trace_stream) {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "performing argument deduction for bindings: ";
+      *trace_stream_ << "*** performing argument deduction for bindings: [";
       llvm::ListSeparator sep;
       for (const auto* binding : bindings_to_deduce) {
-        *trace_stream_ << sep << *binding;
+        *trace_stream_ << sep << "`" << *binding << "`";
       }
-      *trace_stream_ << "\n";
+      *trace_stream_ << "]\n";
     }
     for (const auto* binding : bindings_to_deduce) {
       deduced_values_.insert({binding, {}});
@@ -1100,7 +1097,7 @@ auto TypeChecker::ArgumentDeduction::Deduce(Nonnull<const Value*> param,
                                             bool allow_implicit_conversion)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "deducing " << *param << " from " << *arg << "\n";
+    *trace_stream_ << "*** deducing `" << *param << "` from `" << *arg << "`\n";
   }
 
   // If param is the name of a variable we're deducing, then deduce it.
@@ -1430,8 +1427,8 @@ auto TypeChecker::ArgumentDeduction::Finish(
     CARBON_ASSIGN_OR_RETURN(Nonnull<const Value*> value,
                             type_checker.InterpExp(arg));
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "evaluated generic parameter " << *binding << " as "
-                     << *value << "\n";
+      *trace_stream_ << "--- evaluated generic parameter `" << *binding
+                     << "` as `" << *value << "`\n";
     }
 
     // Find a witness for the binding if needed.
@@ -1481,15 +1478,15 @@ auto TypeChecker::ArgumentDeduction::Finish(
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "deduction succeeded with results: {";
+    *trace_stream_ << "--> deduction succeeded with results: [";
     llvm::ListSeparator sep;
     for (const auto& [binding, val] : bindings.args()) {
-      *trace_stream_ << sep << *binding << " = " << *val;
+      *trace_stream_ << sep << "`" << *binding << "` = `" << *val << "`";
     }
     for (const auto& [binding, val] : bindings.witnesses()) {
-      *trace_stream_ << sep << *binding << " = " << *val;
+      *trace_stream_ << sep << "`" << *binding << "` = `" << *val << "`";
     }
-    *trace_stream_ << "}\n";
+    *trace_stream_ << "]\n";
   }
 
   return {std::move(bindings)};
@@ -1654,8 +1651,8 @@ class TypeChecker::ConstraintTypeBuilder {
       -> ErrorOr<Success> {
     if (type_checker.trace_stream_->is_enabled()) {
       *type_checker.trace_stream_
-          << "merging " << *constraint << " into constraint with "
-          << *constraint->self_binding() << " ~> " << *self << "\n";
+          << "*** merging `" << *constraint << "` into constraint with `"
+          << *constraint->self_binding() << "` ~> `" << *self << "`\n";
     }
 
     // First substitute into the impl bindings to form the full witness for
@@ -1910,9 +1907,9 @@ class TypeChecker::ConstraintTypeBuilder {
     std::deque<Nonnull<RewriteConstraint*>> rewrite_queue;
     for (auto& rewrite : rewrite_constraints_) {
       if (type_checker.trace_stream_->is_enabled()) {
-        *type_checker.trace_stream_ << "initial rewrite of "
-                                    << *rewrite.constant << " is "
-                                    << *rewrite.converted_replacement << "\n";
+        *type_checker.trace_stream_ << "--- initial rewrite of `"
+                                    << *rewrite.constant << "` is `"
+                                    << *rewrite.converted_replacement << "`\n";
       }
       rewrite_queue.push_back(&rewrite);
     }
@@ -1949,9 +1946,9 @@ class TypeChecker::ConstraintTypeBuilder {
 
       if (!ValueEqual(rebuilt, rewrite->converted_replacement, std::nullopt)) {
         if (type_checker.trace_stream_->is_enabled()) {
-          *type_checker.trace_stream_ << "rewrote rewrite of "
-                                      << *rewrite->constant << " to "
-                                      << *rebuilt << "\n";
+          *type_checker.trace_stream_ << "--- rewrote rewrite of `"
+                                      << *rewrite->constant << "` to `"
+                                      << *rebuilt << "`\n";
         }
         rewrite->converted_replacement = rebuilt;
         // Now we've rewritten this rewrite, we might find more rewrites apply
@@ -1959,8 +1956,9 @@ class TypeChecker::ConstraintTypeBuilder {
         rewrite_queue.push_back(rewrite);
       } else {
         if (type_checker.trace_stream_->is_enabled()) {
-          *type_checker.trace_stream_ << "rewrite of " << *rewrite->constant
-                                      << " converged to " << *rebuilt << "\n";
+          *type_checker.trace_stream_
+              << "--- rewrite of `" << *rewrite->constant << "` converged to `"
+              << *rebuilt << "`\n";
         }
       }
     }
@@ -2109,8 +2107,16 @@ auto TypeChecker::Substitute(const Bindings& bindings,
   CARBON_ASSIGN_OR_RETURN(const auto* result, SubstituteImpl(bindings, type));
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "substitution of " << bindings << "\n  old: " << *type
-                   << "\n  new: " << *result << "\n";
+    *trace_stream_ << "->+ substitution of [";
+    llvm::ListSeparator sep(", ");
+    for (const auto& [name, value] : bindings.args()) {
+      *trace_stream_ << sep << "`" << *name << "` -> `" << *value << "`";
+    }
+    for (const auto& [name, value] : bindings.witnesses()) {
+      *trace_stream_ << sep << "`" << *name << "` -> `" << *value << "`";
+    }
+    *trace_stream_ << "]\n -  old: `" << *type << "`\n +  new: `" << *result
+                   << "`\n";
   }
   return result;
 }
@@ -2138,8 +2144,8 @@ class TypeChecker::SubstituteTransform
     if (it == bindings_.args().end()) {
       if (const auto* trace_stream = type_checker_->trace_stream_;
           trace_stream->is_enabled()) {
-        *trace_stream << "substitution: no value for binding " << *var_type
-                      << ", leaving alone\n";
+        *trace_stream << "--- substitution: no value for binding `" << *var_type
+                      << "`, leaving alone\n";
       }
       return var_type;
     } else {
@@ -2154,8 +2160,8 @@ class TypeChecker::SubstituteTransform
     if (it == bindings_.witnesses().end()) {
       if (const auto* trace_stream = type_checker_->trace_stream_;
           trace_stream->is_enabled()) {
-        *trace_stream << "substitution: no value for binding " << *witness
-                      << ", leaving alone\n";
+        *trace_stream << "--- substitution: no value for binding `" << *witness
+                      << "`, leaving alone\n";
       }
       return witness;
     } else {
@@ -2281,9 +2287,9 @@ class TypeChecker::SubstituteTransform
       }
       if (const auto* trace_stream = type_checker_->trace_stream_;
           trace_stream->is_enabled()) {
-        *trace_stream << "substitution: self of constraint " << *constraint
-                      << " is substituted, new type of type is "
-                      << *type_of_type << "\n";
+        *trace_stream << "--- substitution: self of constraint `" << *constraint
+                      << "` is substituted, new type of type is `"
+                      << *type_of_type << "`\n";
       }
       // TODO: Should we keep any part of the old constraint -- rewrites,
       // equality constraints, etc?
@@ -2298,7 +2304,7 @@ class TypeChecker::SubstituteTransform
     Nonnull<const ConstraintType*> new_constraint = std::move(builder).Build();
     if (const auto* trace_stream = type_checker_->trace_stream_;
         trace_stream->is_enabled()) {
-      *trace_stream << "substitution: " << *constraint << " => "
+      *trace_stream << "--- substitution: " << *constraint << " => "
                     << *new_constraint << "\n";
     }
     return new_constraint;
@@ -2347,7 +2353,7 @@ auto TypeChecker::RefineWitness(Nonnull<const Witness*> witness,
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "could not refine " << *witness << "\n";
+    *trace_stream_ << "--x could not refine `" << *witness << "`\n";
   }
   return witness;
 }
@@ -2370,10 +2376,11 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
   MatchingImplSet::Match match(&matching_impl_set_, &impl, impl_type, &iface);
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "MatchImpl: looking for " << *impl_type << " as " << iface
-                   << "\n";
-    *trace_stream_ << "checking " << *impl.type << " as "
-                   << *impl.interface << "\n";
+    *trace_stream_ << "\n========\tMatch Impl\t========\n";
+    *trace_stream_ << "*** looking for `" << *impl_type << "` as `" << iface
+                   << "`\n";
+    *trace_stream_ << "*** checking `" << *impl.type << "` as `"
+                   << *impl.interface << "` (" << source_loc << ")\n";
   }
 
   ArgumentDeduction deduction(source_loc, "match", impl.deduced, trace_stream_);
@@ -2382,7 +2389,7 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
                            /*allow_implicit_conversion=*/false);
       !e.ok()) {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "type does not match: " << e.error() << "\n";
+      *trace_stream_ << "--! type does not match: " << e.error() << "\n";
     }
     return {std::nullopt};
   }
@@ -2391,7 +2398,7 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
           impl.interface, &iface, /*allow_implicit_conversion=*/false);
       !e.ok()) {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "interface does not match: " << e.error() << "\n";
+      *trace_stream_ << "--! interface does not match: " << e.error() << "\n";
     }
     return {std::nullopt};
   }
@@ -2407,13 +2414,13 @@ auto TypeChecker::MatchImpl(const InterfaceType& iface,
                        /*diagnose_deduction_failure=*/false));
   if (!bindings_or_error) {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "impl does not match\n";
+      *trace_stream_ << "--! impl does not match\n";
     }
     return {std::nullopt};
   } else {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "matched with " << *impl.type << " as "
-                     << *impl.interface << "\n\n";
+      *trace_stream_ << "==> matched with `" << *impl.type << "` as `"
+                     << *impl.interface << "`\n\n";
     }
     CARBON_ASSIGN_OR_RETURN(
         const auto* subst_witness,
@@ -2766,12 +2773,13 @@ auto TypeChecker::TypeCheckExpImpl(Nonnull<Expression*> e,
                                    const ImplScope& impl_scope)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "checking " << e->kind() << " " << *e;
-    *trace_stream_ << "\n";
+    *trace_stream_ << "*** checking " << e->kind() << " `" << *e << "` ("
+                   << e->source_loc() << ")\n";
   }
   if (e->is_type_checked()) {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "expression has already been type-checked\n";
+      *trace_stream_ << "--- expression `" << *e
+                     << "` has already been type-checked\n";
     }
     return Success();
   }
@@ -3618,9 +3626,10 @@ auto TypeChecker::TypeCheckExpImpl(Nonnull<Expression*> e,
         case Value::Kind::FunctionType: {
           const auto& fun_t = cast<FunctionType>(call.function().static_type());
           if (trace_stream_->is_enabled()) {
-            *trace_stream_ << "checking call to function of type " << fun_t
-                           << "\nwith arguments of type: "
-                           << call.argument().static_type() << "\n";
+            *trace_stream_ << "*** checking call to function of type `" << fun_t
+                           << "` with arguments of type `"
+                           << call.argument().static_type() << "` ("
+                           << call.source_loc() << ")\n";
           }
           CARBON_RETURN_IF_ERROR(DeduceCallBindings(
               call, &fun_t.parameters(), fun_t.generic_parameters(),
@@ -4262,11 +4271,11 @@ auto TypeChecker::TypeCheckPattern(
     std::optional<Nonnull<const Value*>> expected, ImplScope& impl_scope,
     ExpressionCategory enclosing_expression_category) -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "checking " << p->kind() << " " << *p;
+    *trace_stream_ << "*** checking " << p->kind() << " `" << *p << "`";
     if (expected) {
-      *trace_stream_ << ", expecting " << **expected;
+      *trace_stream_ << ", expecting `" << **expected << "`";
     }
-    *trace_stream_ << "\n";
+    *trace_stream_ << " (" << p->source_loc() << ")\n";
   }
   switch (p->kind()) {
     case PatternKind::AutoPattern:
@@ -4389,8 +4398,8 @@ auto TypeChecker::TypeCheckPattern(
                                                 expected_field_type, impl_scope,
                                                 enclosing_expression_category));
         if (trace_stream_->is_enabled()) {
-          *trace_stream_ << "finished checking tuple pattern field " << *field
-                         << "\n";
+          *trace_stream_ << "*** finished checking tuple pattern field `"
+                         << *field << "` (" << field->source_loc() << ")\n";
         }
         field_types.push_back(&field->static_type());
         field_patterns.push_back(&field->value());
@@ -4520,14 +4529,14 @@ auto TypeChecker::TypeCheckGenericBinding(GenericBinding& binding,
         builder.AddAndSubstitute(*this, constraint, symbolic_value, witness,
                                  Bindings(), /*add_lookup_contexts=*/true));
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "resolving constraint type for " << binding << " from "
-                     << *constraint << "\n";
+      *trace_stream_ << "*** resolving constraint type for `" << binding
+                     << "` from `" << *constraint << "`\n";
     }
     CARBON_RETURN_IF_ERROR(
         builder.Resolve(*this, binding.type().source_loc(), impl_scope));
     type = std::move(builder).Build();
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "resolved constraint type is " << *type << "\n";
+      *trace_stream_ << "--- resolved constraint type is `" << *type << "`\n";
     }
 
     BringImplBindingIntoScope(impl_binding, impl_scope);
@@ -4570,7 +4579,8 @@ auto TypeChecker::TypeCheckStmt(Nonnull<Statement*> s,
                                 const ImplScope& impl_scope)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "checking " << s->kind() << " " << *s << "\n";
+    *trace_stream_ << "*** checking " << s->kind() << " `" << PrintAsID(*s)
+                   << "` (" << s->source_loc() << ")\n";
   }
   switch (s->kind()) {
     case StatementKind::Match: {
@@ -4886,7 +4896,8 @@ auto TypeChecker::DeclareCallableDeclaration(Nonnull<CallableDeclaration*> f,
   const auto name = GetName(*f);
   CARBON_CHECK(name) << "Unexpected missing name for `" << *f << "`.";
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** declaring function " << *name << "\n";
+    *trace_stream_ << "*** declaring function `" << *name << "` ("
+                   << f->source_loc() << ")\n";
   }
   ImplScope function_scope(scope_info.innermost_scope);
   std::vector<Nonnull<const GenericBinding*>> all_bindings =
@@ -5003,8 +5014,9 @@ auto TypeChecker::DeclareCallableDeclaration(Nonnull<CallableDeclaration*> f,
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished declaring function " << *name << " of type "
-                   << f->static_type() << "\n";
+    *trace_stream_ << "*** finished declaring function `" << *name
+                   << "` of type `" << f->static_type() << "` ("
+                   << f->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5015,7 +5027,8 @@ auto TypeChecker::TypeCheckCallableDeclaration(Nonnull<CallableDeclaration*> f,
   auto name = GetName(*f);
   CARBON_CHECK(name) << "Unexpected missing name for `" << *f << "`.";
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** checking function " << *name << "\n";
+    *trace_stream_ << "*** checking function `" << *name << "` ("
+                   << f->source_loc() << ")\n";
   }
   // If f->return_term().is_auto(), the function body was already
   // type checked in DeclareFunctionDeclaration.
@@ -5025,6 +5038,8 @@ auto TypeChecker::TypeCheckCallableDeclaration(Nonnull<CallableDeclaration*> f,
     BringImplBindingsIntoScope(
         cast<FunctionType>(f->static_type()).impl_bindings(), function_scope);
     if (trace_stream_->is_enabled()) {
+      *trace_stream_ << "--- impl declarations for `" << PrintAsID(*f) << "` ("
+                     << f->source_loc() << ")\n";
       *trace_stream_ << function_scope;
     }
     CARBON_RETURN_IF_ERROR(TypeCheckStmt(*f->body(), function_scope));
@@ -5034,7 +5049,8 @@ auto TypeChecker::TypeCheckCallableDeclaration(Nonnull<CallableDeclaration*> f,
     }
   }
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished checking function " << *name << "\n";
+    *trace_stream_ << "*** finished checking function `" << *name << "` ("
+                   << f->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5043,7 +5059,8 @@ auto TypeChecker::DeclareClassDeclaration(Nonnull<ClassDeclaration*> class_decl,
                                           const ScopeInfo& scope_info)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** declaring class " << class_decl->name() << "\n";
+    *trace_stream_ << "*** declaring class `" << class_decl->name() << "` ("
+                   << class_decl->source_loc() << ")\n";
   }
   Nonnull<SelfDeclaration*> self = class_decl->self();
   ImplScope class_scope(scope_info.innermost_scope);
@@ -5127,6 +5144,8 @@ auto TypeChecker::DeclareClassDeclaration(Nonnull<ClassDeclaration*> class_decl,
                          std::nullopt, class_scope, ExpressionCategory::Value));
     CollectAndNumberGenericBindingsInPattern(type_params, bindings);
     if (trace_stream_->is_enabled()) {
+      *trace_stream_ << "--- impl declarations for `" << class_decl->name()
+                     << "` (" << class_decl->source_loc() << ")\n";
       *trace_stream_ << class_scope;
     }
   }
@@ -5238,8 +5257,8 @@ auto TypeChecker::DeclareClassDeclaration(Nonnull<ClassDeclaration*> class_decl,
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished declaring class " << class_decl->name()
-                   << "\n";
+    *trace_stream_ << "*** finished declaring class `" << class_decl->name()
+                   << "` (" << class_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5248,13 +5267,16 @@ auto TypeChecker::TypeCheckClassDeclaration(
     Nonnull<ClassDeclaration*> class_decl, const ImplScope& impl_scope)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** checking class " << class_decl->name() << "\n";
+    *trace_stream_ << "*** checking class `" << class_decl->name() << "` ("
+                   << class_decl->source_loc() << ")\n";
   }
   ImplScope class_scope(&impl_scope);
   if (class_decl->type_params().has_value()) {
     BringPatternImplBindingsIntoScope(*class_decl->type_params(), class_scope);
   }
   if (trace_stream_->is_enabled()) {
+    *trace_stream_ << "--- impl declarations for `" << class_decl->name()
+                   << "` (" << class_decl->source_loc() << ")\n";
     *trace_stream_ << class_scope;
   }
   auto [it, inserted] =
@@ -5266,8 +5288,8 @@ auto TypeChecker::TypeCheckClassDeclaration(
     CARBON_RETURN_IF_ERROR(CollectMember(class_decl, m));
   }
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished checking class " << class_decl->name()
-                   << "\n";
+    *trace_stream_ << "*** finished checking class `" << class_decl->name()
+                   << "` (" << class_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5277,7 +5299,8 @@ auto TypeChecker::DeclareMixinDeclaration(Nonnull<MixinDeclaration*> mixin_decl,
                                           const ScopeInfo& scope_info)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** declaring mixin " << mixin_decl->name() << "\n";
+    *trace_stream_ << "*** declaring mixin `" << mixin_decl->name() << "` ("
+                   << mixin_decl->source_loc() << ")\n";
   }
   ImplScope mixin_scope(scope_info.innermost_scope);
 
@@ -5286,6 +5309,8 @@ auto TypeChecker::DeclareMixinDeclaration(Nonnull<MixinDeclaration*> mixin_decl,
         *mixin_decl->params(), PatternRequirements::Irrefutable, std::nullopt,
         mixin_scope, ExpressionCategory::Value));
     if (trace_stream_->is_enabled()) {
+      *trace_stream_ << "--- impl declarations for `" << mixin_decl->name()
+                     << "` (" << mixin_decl->source_loc() << ")\n";
       *trace_stream_ << mixin_scope;
     }
 
@@ -5311,8 +5336,8 @@ auto TypeChecker::DeclareMixinDeclaration(Nonnull<MixinDeclaration*> mixin_decl,
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished declaring mixin " << mixin_decl->name()
-                   << "\n";
+    *trace_stream_ << "*** finished declaring mixin `" << mixin_decl->name()
+                   << "` (" << mixin_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5331,19 +5356,22 @@ auto TypeChecker::TypeCheckMixinDeclaration(
   if (!inserted) {
     // This declaration has already been type checked before
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "** skipped checking mixin " << mixin_decl->name()
-                     << "\n";
+      *trace_stream_ << ">>> skipped checking mixin `" << mixin_decl->name()
+                     << "` (" << mixin_decl->source_loc() << ")\n";
     }
     return Success();
   }
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** checking mixin " << mixin_decl->name() << "\n";
+    *trace_stream_ << "*** checking mixin `" << mixin_decl->name() << "` ("
+                   << mixin_decl->source_loc() << ")\n";
   }
   ImplScope mixin_scope(&impl_scope);
   if (mixin_decl->params().has_value()) {
     BringPatternImplBindingsIntoScope(*mixin_decl->params(), mixin_scope);
   }
   if (trace_stream_->is_enabled()) {
+    *trace_stream_ << "--- impl declarations for `" << mixin_decl->name()
+                   << "` (" << mixin_decl->source_loc() << ")\n";
     *trace_stream_ << mixin_scope;
   }
   for (Nonnull<Declaration*> m : mixin_decl->members()) {
@@ -5351,8 +5379,8 @@ auto TypeChecker::TypeCheckMixinDeclaration(
     CARBON_RETURN_IF_ERROR(CollectMember(mixin_decl, m));
   }
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished checking mixin " << mixin_decl->name()
-                   << "\n";
+    *trace_stream_ << "*** finished checking mixin `" << mixin_decl->name()
+                   << "` (" << mixin_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5367,7 +5395,8 @@ auto TypeChecker::TypeCheckMixDeclaration(
     std::optional<Nonnull<const Declaration*>> enclosing_decl)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** checking " << *mix_decl << "\n";
+    *trace_stream_ << "*** checking MixDeclaration `" << PrintAsID(*mix_decl)
+                   << "` (" << mix_decl->source_loc() << ")\n";
   }
   // TODO(darshal): Check if the imports (interface mentioned in the 'for'
   // clause) of the mixin being mixed are being impl'd in the enclosed
@@ -5387,7 +5416,8 @@ auto TypeChecker::TypeCheckMixDeclaration(
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished checking " << *mix_decl << "\n";
+    *trace_stream_ << "*** finished checking `" << PrintAsID(*mix_decl) << "` ("
+                   << mix_decl->source_loc() << ")\n";
   }
 
   return Success();
@@ -5402,9 +5432,8 @@ auto TypeChecker::DeclareConstraintTypeDeclaration(
   bool is_interface = isa<InterfaceDeclaration>(constraint_decl);
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** declaring ";
-    constraint_decl->PrintID(trace_stream_->stream());
-    *trace_stream_ << "\n";
+    *trace_stream_ << "*** declaring `" << PrintAsID(*constraint_decl) << "` ("
+                   << constraint_decl->source_loc() << ")\n";
   }
   ImplScope constraint_scope(scope_info.innermost_scope);
 
@@ -5415,6 +5444,9 @@ auto TypeChecker::DeclareConstraintTypeDeclaration(
         *constraint_decl->params(), PatternRequirements::Irrefutable,
         std::nullopt, constraint_scope, ExpressionCategory::Value));
     if (trace_stream_->is_enabled()) {
+      *trace_stream_ << "--- impl declarations for `"
+                     << PrintAsID(*constraint_decl) << "` ("
+                     << constraint_decl->source_loc() << ")\n";
       *trace_stream_ << constraint_scope;
     }
     CollectAndNumberGenericBindingsInPattern(*constraint_decl->params(),
@@ -5586,9 +5618,8 @@ auto TypeChecker::DeclareConstraintTypeDeclaration(
   constraint_decl->set_constraint_type(std::move(builder).Build());
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished declaring ";
-    constraint_decl->PrintID(trace_stream_->stream());
-    *trace_stream_ << "\n";
+    *trace_stream_ << "*** finished declaring `" << PrintAsID(*constraint_decl)
+                   << "` (" << constraint_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5597,9 +5628,8 @@ auto TypeChecker::TypeCheckConstraintTypeDeclaration(
     Nonnull<ConstraintTypeDeclaration*> constraint_decl,
     const ImplScope& impl_scope) -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** checking ";
-    constraint_decl->PrintID(trace_stream_->stream());
-    *trace_stream_ << "\n";
+    *trace_stream_ << "*** checking `" << PrintAsID(*constraint_decl) << "` ("
+                   << constraint_decl->source_loc() << ")\n";
   }
   ImplScope constraint_scope(&impl_scope);
   if (constraint_decl->params().has_value()) {
@@ -5607,6 +5637,9 @@ auto TypeChecker::TypeCheckConstraintTypeDeclaration(
                                       constraint_scope);
   }
   if (trace_stream_->is_enabled()) {
+    *trace_stream_ << "--- impl declarations for `"
+                   << PrintAsID(*constraint_decl) << "` ("
+                   << constraint_decl->source_loc() << ")\n";
     *trace_stream_ << constraint_scope;
   }
   for (Nonnull<Declaration*> m : constraint_decl->members()) {
@@ -5614,9 +5647,8 @@ auto TypeChecker::TypeCheckConstraintTypeDeclaration(
         TypeCheckDeclaration(m, constraint_scope, constraint_decl));
   }
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished checking ";
-    constraint_decl->PrintID(trace_stream_->stream());
-    *trace_stream_ << "\n";
+    *trace_stream_ << "*** finished checking `" << PrintAsID(*constraint_decl)
+                   << "` (" << constraint_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5766,7 +5798,8 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
                                          bool is_template_instantiation)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "declaring " << *impl_decl << "\n";
+    *trace_stream_ << "*** declaring `" << PrintAsID(*impl_decl) << "` ("
+                   << impl_decl->source_loc() << ")\n";
   }
 
   if (!IsTemplateSaturated(impl_decl->deduced_parameters())) {
@@ -5786,10 +5819,10 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
 
   // Bring the deduced parameters into scope.
   for (Nonnull<GenericBinding*> deduced : impl_decl->deduced_parameters()) {
-    generic_bindings.push_back(deduced);
     CARBON_RETURN_IF_ERROR(
         TypeCheckPattern(deduced, PatternRequirements::Irrefutable,
                          std::nullopt, impl_scope, ExpressionCategory::Value));
+    CollectAndNumberGenericBindingsInPattern(deduced, generic_bindings);
     CollectImplBindingsInPattern(deduced, impl_bindings);
   }
   impl_decl->set_impl_bindings(impl_bindings);
@@ -5836,15 +5869,17 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
                                  builder.GetSelfWitness(), Bindings(),
                                  /*add_lookup_contexts=*/true));
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "resolving impls constraint type for " << *impl_decl
-                     << " from " << *implemented_constraint << "\n";
+      *trace_stream_ << "*** resolving impls constraint type for `"
+                     << PrintAsID(*impl_decl) << "` from `"
+                     << *implemented_constraint << "` ("
+                     << impl_decl->source_loc() << ")\n";
     }
     CARBON_RETURN_IF_ERROR(builder.Resolve(
         *this, impl_decl->interface().source_loc(), impl_scope));
     constraint_type = std::move(builder).Build();
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "resolving impls constraint type as "
-                     << *constraint_type << "\n";
+      *trace_stream_ << "*** resolving impls constraint type as `"
+                     << *constraint_type << "`\n";
     }
     impl_decl->set_constraint_type(constraint_type);
   }
@@ -5901,8 +5936,8 @@ auto TypeChecker::DeclareImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "** finished declaring impl " << *impl_decl->impl_type()
-                   << " as " << impl_decl->interface() << "\n";
+    *trace_stream_ << "*** finished declaring impl `" << *impl_decl->impl_type()
+                   << "` as `" << impl_decl->interface() << "`\n";
   }
   return Success();
 }
@@ -5940,13 +5975,15 @@ auto TypeChecker::TypeCheckImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
     -> ErrorOr<Success> {
   if (!IsTemplateSaturated(impl_decl->deduced_parameters())) {
     if (trace_stream_->is_enabled()) {
-      *trace_stream_ << "deferring checking templated " << *impl_decl << "\n";
+      *trace_stream_ << "*** deferring checking templated `" << *impl_decl
+                     << "` (" << impl_decl->source_loc() << ")\n";
     }
     return Success();
   }
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "checking " << *impl_decl << "\n";
+    *trace_stream_ << "*** checking ImplDeclaration `" << PrintAsID(*impl_decl)
+                   << "` (" << impl_decl->source_loc() << ")\n";
   }
 
   Nonnull<const Value*> self = *impl_decl->self()->constant_value();
@@ -5970,7 +6007,8 @@ auto TypeChecker::TypeCheckImplDeclaration(Nonnull<ImplDeclaration*> impl_decl,
     CARBON_RETURN_IF_ERROR(TypeCheckDeclaration(m, member_scope, impl_decl));
   }
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "finished checking impl\n";
+    *trace_stream_ << "*** finished checking impl `" << PrintAsID(*impl_decl)
+                   << "` (" << impl_decl->source_loc() << ")\n";
   }
   return Success();
 }
@@ -5987,6 +6025,8 @@ auto TypeChecker::DeclareChoiceDeclaration(Nonnull<ChoiceDeclaration*> choice,
                          choice_scope, ExpressionCategory::Value));
     CollectAndNumberGenericBindingsInPattern(type_params, bindings);
     if (trace_stream_->is_enabled()) {
+      *trace_stream_ << "--- impl declarations for `" << PrintAsID(*choice)
+                     << "` (" << choice->source_loc() << ")\n";
       *trace_stream_ << choice_scope;
     }
   }
@@ -6112,8 +6152,7 @@ auto TypeChecker::TypeCheck(AST& ast) -> ErrorOr<Success> {
   llvm::SaveAndRestore<decltype(top_level_impl_scope_)>
       set_top_level_impl_scope(top_level_impl_scope_, &impl_scope);
 
-  for (int i = 0; i < static_cast<int>(ast.declarations.size()); ++i) {
-    auto* declaration = ast.declarations[i];
+  for (auto declaration : ast.declarations) {
     set_file_ctx.update_source_loc(declaration->source_loc());
     CARBON_RETURN_IF_ERROR(
         DeclareDeclaration(declaration, top_level_scope_info));
@@ -6132,7 +6171,8 @@ auto TypeChecker::TypeCheckDeclaration(
     std::optional<Nonnull<const Declaration*>> enclosing_decl)
     -> ErrorOr<Success> {
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "checking " << d->kind() << "\n";
+    *trace_stream_ << "*** checking " << d->kind() << " `" << PrintAsID(*d)
+                   << "` (" << d->source_loc() << ")\n";
   }
   switch (d->kind()) {
     case DeclarationKind::NamespaceDeclaration:
@@ -6452,9 +6492,13 @@ auto TypeChecker::InstantiateImplDeclaration(
   CARBON_CHECK(IsTemplateSaturated(*bindings));
 
   if (trace_stream_->is_enabled()) {
-    *trace_stream_ << "instantiating " << *old_impl;
+    *trace_stream_ << "*** instantiating `" << PrintAsID(*old_impl) << "` ("
+                   << old_impl->source_loc() << ")\n";
+    *trace_stream_ << *bindings << "\n";
   }
 
+  SetFileContext set_file_context(*trace_stream_, old_impl->source_loc());
+
   auto it = templates_.find(old_impl);
   CARBON_CHECK(it != templates_.end());
   const TemplateInfo& info = it->second;
diff --git a/explorer/testdata/trace/context_all.carbon b/explorer/testdata/trace/context_all.carbon
index b7681569f983..43df75e7b11e 100644
--- a/explorer/testdata/trace/context_all.carbon
+++ b/explorer/testdata/trace/context_all.carbon
@@ -15,8 +15,8 @@ fn Main() -> i32 {
 // ARGS: --trace_file=- --trace_phase=all --trace_file_context=all %s
 // NOAUTOUPDATE
 // SET-CHECK-SUBSET
-// CHECK:STDOUT: ** declaring interface As
-// CHECK:STDOUT: ** declaring function Main
+// CHECK:STDOUT: *** declaring `interface As` ({{.*}}/explorer/data/prelude.carbon:14)
+// CHECK:STDOUT: *** declaring function `Main` (context_all.carbon:11)
 // CHECK:STDOUT: interface As {
 // CHECK:STDOUT: fn Main ()-> i32 {
 // CHECK:STDOUT: --- step ExpressionAction pos: 0 `Main()` (<Main()>:0) --->
diff --git a/explorer/testdata/trace/context_main.carbon b/explorer/testdata/trace/context_main.carbon
index 1612665bdc34..79997ba8f3ee 100644
--- a/explorer/testdata/trace/context_main.carbon
+++ b/explorer/testdata/trace/context_main.carbon
@@ -43,16 +43,63 @@ fn Main() -> i32 {
 // CHECK:STDOUT: ********** resolving control flow **********
 // CHECK:STDOUT: --- flow-resolved return statement `return 0;` in `fn Main` (context_main.carbon:10)
 // CHECK:STDOUT: ********** type checking **********
-// CHECK:STDOUT: ** declaring interface TestInterface
-// CHECK:STDOUT: ** finished declaring interface TestInterface
-// CHECK:STDOUT: checking InterfaceDeclaration
-// CHECK:STDOUT: ** checking interface TestInterface
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: ** finished checking interface TestInterface
-// CHECK:STDOUT: ** declaring function Main
-// CHECK:STDOUT: checking TuplePattern ()
-// CHECK:STDOUT: checking IntTypeLiteral i32
+// CHECK:STDOUT: *** declaring `interface TestInterface` (context_main.carbon:7)
+// CHECK:STDOUT: *** finished declaring `interface TestInterface` (context_main.carbon:7)
+// CHECK:STDOUT: *** checking InterfaceDeclaration `interface TestInterface` (context_main.carbon:7)
+// CHECK:STDOUT: *** checking `interface TestInterface` (context_main.carbon:7)
+// CHECK:STDOUT: --- impl declarations for `interface TestInterface` (context_main.carbon:7)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** finished checking `interface TestInterface` (context_main.carbon:7)
+// CHECK:STDOUT: *** declaring function `Main` (context_main.carbon:11)
+// CHECK:STDOUT: *** checking TuplePattern `()` (context_main.carbon:9)
+// CHECK:STDOUT: *** checking IntTypeLiteral `i32` (context_main.carbon:9)
 // CHECK:STDOUT: (+) stack-push: ValueExpressionAction pos: 0 `i32` (context_main.carbon:9)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 0 `i32` (context_main.carbon:9) --->
 // CHECK:STDOUT: (+) stack-push: ExpressionAction pos: 0 `i32` (context_main.carbon:9)
@@ -60,25 +107,68 @@ fn Main() -> i32 {
 // CHECK:STDOUT: (-) stack-pop:  ExpressionAction pos: 0 `i32` (context_main.carbon:9)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 1 `i32` results: [`i32`]  (context_main.carbon:9) --->
 // CHECK:STDOUT: (-) stack-pop:  ValueExpressionAction pos: 1 `i32` results: [`i32`]  (context_main.carbon:9)
-// CHECK:STDOUT: ** finished declaring function Main of type fn () -> i32
-// CHECK:STDOUT: checking FunctionDeclaration
-// CHECK:STDOUT: ** checking function Main
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: checking Block {
-// CHECK:STDOUT: return 0;
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: checking ReturnExpression return 0;
-// CHECK:STDOUT: checking IntLiteral 0
-// CHECK:STDOUT: ** finished checking function Main
-// CHECK:STDOUT: checking CallExpression Main()
-// CHECK:STDOUT: checking IdentifierExpression Main
-// CHECK:STDOUT: checking TupleLiteral ()
-// CHECK:STDOUT: checking call to function of type fn () -> i32
-// CHECK:STDOUT: with arguments of type: ()
-// CHECK:STDOUT: performing argument deduction for bindings:{{ }}
-// CHECK:STDOUT: deduction succeeded with results: {}
+// CHECK:STDOUT: *** finished declaring function `Main` of type `fn () -> i32` (context_main.carbon:11)
+// CHECK:STDOUT: *** checking FunctionDeclaration `fn Main` (context_main.carbon:11)
+// CHECK:STDOUT: *** checking function `Main` (context_main.carbon:11)
+// CHECK:STDOUT: --- impl declarations for `fn Main` (context_main.carbon:11)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** checking Block `{return 0;}` (context_main.carbon:11)
+// CHECK:STDOUT: *** checking ReturnExpression `return 0;` (context_main.carbon:10)
+// CHECK:STDOUT: *** checking IntLiteral `0` (context_main.carbon:10)
+// CHECK:STDOUT: *** finished checking function `Main` (context_main.carbon:11)
+// CHECK:STDOUT: *** checking CallExpression `Main()` (<Main()>:0)
+// CHECK:STDOUT: *** checking IdentifierExpression `Main` (<Main()>:0)
+// CHECK:STDOUT: *** checking TupleLiteral `()` (<Main()>:0)
+// CHECK:STDOUT: *** checking call to function of type `fn () -> i32` with arguments of type `()` (<Main()>:0)
+// CHECK:STDOUT: *** performing argument deduction for bindings: []
+// CHECK:STDOUT: --> deduction succeeded with results: []
 // CHECK:STDOUT: ********** resolving unformed variables **********
 // CHECK:STDOUT: *** resolving-unformed in decl `interface TestInterface` (context_main.carbon:7)
 // CHECK:STDOUT: *** resolving-unformed in decl `fn Main` (context_main.carbon:11)
diff --git a/explorer/testdata/trace/context_prelude.carbon b/explorer/testdata/trace/context_prelude.carbon
index c152b4207511..4794a7f5242b 100644
--- a/explorer/testdata/trace/context_prelude.carbon
+++ b/explorer/testdata/trace/context_prelude.carbon
@@ -15,5 +15,5 @@ fn Main() -> i32 {
 // ARGS: --trace_file=- --trace_phase=all --trace_file_context=prelude %s
 // NOAUTOUPDATE
 // SET-CHECK-SUBSET
-// CHECK:STDOUT: ** declaring interface As
+// CHECK:STDOUT: *** declaring `interface As` ({{.*}}/explorer/data/prelude.carbon:14)
 // CHECK:STDOUT: interface As {
diff --git a/explorer/testdata/trace/phase_all.carbon b/explorer/testdata/trace/phase_all.carbon
index 2c7eb547c253..e45ed2c65ad2 100644
--- a/explorer/testdata/trace/phase_all.carbon
+++ b/explorer/testdata/trace/phase_all.carbon
@@ -81,19 +81,66 @@ fn Main() -> i32 {
 // CHECK:STDOUT: --- flow-resolved return statement `return (n + 1);` in `fn N.Foo` (phase_all.carbon:12)
 // CHECK:STDOUT: --- flow-resolved return statement `return x;` in `fn Main` (phase_all.carbon:17)
 // CHECK:STDOUT: ********** type checking **********
-// CHECK:STDOUT: ** declaring interface TestInterface
-// CHECK:STDOUT: ** finished declaring interface TestInterface
-// CHECK:STDOUT: checking InterfaceDeclaration
-// CHECK:STDOUT: ** checking interface TestInterface
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: ** finished checking interface TestInterface
-// CHECK:STDOUT: checking NamespaceDeclaration
-// CHECK:STDOUT: ** declaring function Foo
-// CHECK:STDOUT: checking TuplePattern (n: i32)
-// CHECK:STDOUT: checking BindingPattern n: i32
-// CHECK:STDOUT: checking ExpressionPattern i32
-// CHECK:STDOUT: checking IntTypeLiteral i32
+// CHECK:STDOUT: *** declaring `interface TestInterface` (phase_all.carbon:7)
+// CHECK:STDOUT: *** finished declaring `interface TestInterface` (phase_all.carbon:7)
+// CHECK:STDOUT: *** checking InterfaceDeclaration `interface TestInterface` (phase_all.carbon:7)
+// CHECK:STDOUT: *** checking `interface TestInterface` (phase_all.carbon:7)
+// CHECK:STDOUT: --- impl declarations for `interface TestInterface` (phase_all.carbon:7)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** finished checking `interface TestInterface` (phase_all.carbon:7)
+// CHECK:STDOUT: *** checking NamespaceDeclaration `namespace N` (phase_all.carbon:9)
+// CHECK:STDOUT: *** declaring function `Foo` (phase_all.carbon:13)
+// CHECK:STDOUT: *** checking TuplePattern `(n: i32)` (phase_all.carbon:11)
+// CHECK:STDOUT: *** checking BindingPattern `n: i32` (phase_all.carbon:11)
+// CHECK:STDOUT: *** checking ExpressionPattern `i32` (phase_all.carbon:11)
+// CHECK:STDOUT: *** checking IntTypeLiteral `i32` (phase_all.carbon:11)
 // CHECK:STDOUT: (+) stack-push: ValueExpressionAction pos: 0 `i32` (phase_all.carbon:11)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 0 `i32` (phase_all.carbon:11) --->
 // CHECK:STDOUT: (+) stack-push: ExpressionAction pos: 0 `i32` (phase_all.carbon:11)
@@ -101,8 +148,8 @@ fn Main() -> i32 {
 // CHECK:STDOUT: (-) stack-pop:  ExpressionAction pos: 0 `i32` (phase_all.carbon:11)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:11) --->
 // CHECK:STDOUT: (-) stack-pop:  ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:11)
-// CHECK:STDOUT: finished checking tuple pattern field n: i32
-// CHECK:STDOUT: checking IntTypeLiteral i32
+// CHECK:STDOUT: *** finished checking tuple pattern field `n: i32` (phase_all.carbon:11)
+// CHECK:STDOUT: *** checking IntTypeLiteral `i32` (phase_all.carbon:11)
 // CHECK:STDOUT: (+) stack-push: ValueExpressionAction pos: 0 `i32` (phase_all.carbon:11)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 0 `i32` (phase_all.carbon:11) --->
 // CHECK:STDOUT: (+) stack-push: ExpressionAction pos: 0 `i32` (phase_all.carbon:11)
@@ -110,23 +157,67 @@ fn Main() -> i32 {
 // CHECK:STDOUT: (-) stack-pop:  ExpressionAction pos: 0 `i32` (phase_all.carbon:11)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:11) --->
 // CHECK:STDOUT: (-) stack-pop:  ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:11)
-// CHECK:STDOUT: ** finished declaring function Foo of type fn (i32,) -> i32
-// CHECK:STDOUT: checking FunctionDeclaration
-// CHECK:STDOUT: ** checking function Foo
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: checking Block {
-// CHECK:STDOUT: return (n + 1);
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: checking ReturnExpression return (n + 1);
-// CHECK:STDOUT: checking OperatorExpression (n + 1)
-// CHECK:STDOUT: checking IdentifierExpression n
-// CHECK:STDOUT: checking IntLiteral 1
-// CHECK:STDOUT: ** finished checking function Foo
-// CHECK:STDOUT: ** declaring function Main
-// CHECK:STDOUT: checking TuplePattern ()
-// CHECK:STDOUT: checking IntTypeLiteral i32
+// CHECK:STDOUT: *** finished declaring function `Foo` of type `fn (i32,) -> i32` (phase_all.carbon:13)
+// CHECK:STDOUT: *** checking FunctionDeclaration `fn N.Foo` (phase_all.carbon:13)
+// CHECK:STDOUT: *** checking function `Foo` (phase_all.carbon:13)
+// CHECK:STDOUT: --- impl declarations for `fn N.Foo` (phase_all.carbon:13)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** checking Block `{return (n + 1);}` (phase_all.carbon:13)
+// CHECK:STDOUT: *** checking ReturnExpression `return (n + 1);` (phase_all.carbon:12)
+// CHECK:STDOUT: *** checking OperatorExpression `(n + 1)` (phase_all.carbon:12)
+// CHECK:STDOUT: *** checking IdentifierExpression `n` (phase_all.carbon:12)
+// CHECK:STDOUT: *** checking IntLiteral `1` (phase_all.carbon:12)
+// CHECK:STDOUT: *** finished checking function `Foo` (phase_all.carbon:13)
+// CHECK:STDOUT: *** declaring function `Main` (phase_all.carbon:18)
+// CHECK:STDOUT: *** checking TuplePattern `()` (phase_all.carbon:15)
+// CHECK:STDOUT: *** checking IntTypeLiteral `i32` (phase_all.carbon:15)
 // CHECK:STDOUT: (+) stack-push: ValueExpressionAction pos: 0 `i32` (phase_all.carbon:15)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 0 `i32` (phase_all.carbon:15) --->
 // CHECK:STDOUT: (+) stack-push: ExpressionAction pos: 0 `i32` (phase_all.carbon:15)
@@ -134,30 +225,72 @@ fn Main() -> i32 {
 // CHECK:STDOUT: (-) stack-pop:  ExpressionAction pos: 0 `i32` (phase_all.carbon:15)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:15) --->
 // CHECK:STDOUT: (-) stack-pop:  ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:15)
-// CHECK:STDOUT: ** finished declaring function Main of type fn () -> i32
-// CHECK:STDOUT: checking FunctionDeclaration
-// CHECK:STDOUT: ** checking function Main
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: checking Block {
-// CHECK:STDOUT: var x: i32 = N.Foo(0);
-// CHECK:STDOUT: return x;
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: checking VariableDefinition var x: i32 = N.Foo(0);
-// CHECK:STDOUT: checking CallExpression N.Foo(0)
-// CHECK:STDOUT: checking SimpleMemberAccessExpression N.Foo
-// CHECK:STDOUT: checking IdentifierExpression Foo
-// CHECK:STDOUT: checking TupleLiteral (0)
-// CHECK:STDOUT: checking IntLiteral 0
-// CHECK:STDOUT: checking call to function of type fn (i32,) -> i32
-// CHECK:STDOUT: with arguments of type: (i32,)
-// CHECK:STDOUT: performing argument deduction for bindings:{{ }}
-// CHECK:STDOUT: deducing i32 from i32
-// CHECK:STDOUT: deduction succeeded with results: {}
-// CHECK:STDOUT: checking BindingPattern x: i32, expecting i32
-// CHECK:STDOUT: checking ExpressionPattern i32, expecting i32
-// CHECK:STDOUT: checking IntTypeLiteral i32
+// CHECK:STDOUT: *** finished declaring function `Main` of type `fn () -> i32` (phase_all.carbon:18)
+// CHECK:STDOUT: *** checking FunctionDeclaration `fn Main` (phase_all.carbon:18)
+// CHECK:STDOUT: *** checking function `Main` (phase_all.carbon:18)
+// CHECK:STDOUT: --- impl declarations for `fn Main` (phase_all.carbon:18)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** checking Block `{var x: i32 = N.Foo(0);return x;}` (phase_all.carbon:18)
+// CHECK:STDOUT: *** checking VariableDefinition `var x: i32 = N.Foo(0);` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking CallExpression `N.Foo(0)` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking SimpleMemberAccessExpression `N.Foo` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking IdentifierExpression `Foo` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking TupleLiteral `(0)` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking IntLiteral `0` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking call to function of type `fn (i32,) -> i32` with arguments of type `(i32,)` (phase_all.carbon:16)
+// CHECK:STDOUT: *** performing argument deduction for bindings: []
+// CHECK:STDOUT: *** deducing `i32` from `i32`
+// CHECK:STDOUT: --> deduction succeeded with results: []
+// CHECK:STDOUT: *** checking BindingPattern `x: i32`, expecting `i32` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking ExpressionPattern `i32`, expecting `i32` (phase_all.carbon:16)
+// CHECK:STDOUT: *** checking IntTypeLiteral `i32` (phase_all.carbon:16)
 // CHECK:STDOUT: (+) stack-push: ValueExpressionAction pos: 0 `i32` (phase_all.carbon:16)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 0 `i32` (phase_all.carbon:16) --->
 // CHECK:STDOUT: (+) stack-push: ExpressionAction pos: 0 `i32` (phase_all.carbon:16)
@@ -165,16 +298,15 @@ fn Main() -> i32 {
 // CHECK:STDOUT: (-) stack-pop:  ExpressionAction pos: 0 `i32` (phase_all.carbon:16)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:16) --->
 // CHECK:STDOUT: (-) stack-pop:  ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_all.carbon:16)
-// CHECK:STDOUT: checking ReturnExpression return x;
-// CHECK:STDOUT: checking IdentifierExpression x
-// CHECK:STDOUT: ** finished checking function Main
-// CHECK:STDOUT: checking CallExpression Main()
-// CHECK:STDOUT: checking IdentifierExpression Main
-// CHECK:STDOUT: checking TupleLiteral ()
-// CHECK:STDOUT: checking call to function of type fn () -> i32
-// CHECK:STDOUT: with arguments of type: ()
-// CHECK:STDOUT: performing argument deduction for bindings:{{ }}
-// CHECK:STDOUT: deduction succeeded with results: {}
+// CHECK:STDOUT: *** checking ReturnExpression `return x;` (phase_all.carbon:17)
+// CHECK:STDOUT: *** checking IdentifierExpression `x` (phase_all.carbon:17)
+// CHECK:STDOUT: *** finished checking function `Main` (phase_all.carbon:18)
+// CHECK:STDOUT: *** checking CallExpression `Main()` (<Main()>:0)
+// CHECK:STDOUT: *** checking IdentifierExpression `Main` (<Main()>:0)
+// CHECK:STDOUT: *** checking TupleLiteral `()` (<Main()>:0)
+// CHECK:STDOUT: *** checking call to function of type `fn () -> i32` with arguments of type `()` (<Main()>:0)
+// CHECK:STDOUT: *** performing argument deduction for bindings: []
+// CHECK:STDOUT: --> deduction succeeded with results: []
 // CHECK:STDOUT: ********** resolving unformed variables **********
 // CHECK:STDOUT: *** resolving-unformed in decl `interface TestInterface` (phase_all.carbon:7)
 // CHECK:STDOUT: *** resolving-unformed in decl `namespace N` (phase_all.carbon:9)
diff --git a/explorer/testdata/trace/phase_type_checking.carbon b/explorer/testdata/trace/phase_type_checking.carbon
index 8902965c57b0..157d9735c0c4 100644
--- a/explorer/testdata/trace/phase_type_checking.carbon
+++ b/explorer/testdata/trace/phase_type_checking.carbon
@@ -15,16 +15,63 @@ fn Main() -> i32 {
 // ARGS: --trace_file=- --trace_phase=type_checking %s
 // AUTOUPDATE
 // CHECK:STDOUT: ********** type checking **********
-// CHECK:STDOUT: ** declaring interface TestInterface
-// CHECK:STDOUT: ** finished declaring interface TestInterface
-// CHECK:STDOUT: checking InterfaceDeclaration
-// CHECK:STDOUT: ** checking interface TestInterface
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: ** finished checking interface TestInterface
-// CHECK:STDOUT: ** declaring function Main
-// CHECK:STDOUT: checking TuplePattern ()
-// CHECK:STDOUT: checking IntTypeLiteral i32
+// CHECK:STDOUT: *** declaring `interface TestInterface` (phase_type_checking.carbon:7)
+// CHECK:STDOUT: *** finished declaring `interface TestInterface` (phase_type_checking.carbon:7)
+// CHECK:STDOUT: *** checking InterfaceDeclaration `interface TestInterface` (phase_type_checking.carbon:7)
+// CHECK:STDOUT: *** checking `interface TestInterface` (phase_type_checking.carbon:7)
+// CHECK:STDOUT: --- impl declarations for `interface TestInterface` (phase_type_checking.carbon:7)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** finished checking `interface TestInterface` (phase_type_checking.carbon:7)
+// CHECK:STDOUT: *** declaring function `Main` (phase_type_checking.carbon:11)
+// CHECK:STDOUT: *** checking TuplePattern `()` (phase_type_checking.carbon:9)
+// CHECK:STDOUT: *** checking IntTypeLiteral `i32` (phase_type_checking.carbon:9)
 // CHECK:STDOUT: (+) stack-push: ValueExpressionAction pos: 0 `i32` (phase_type_checking.carbon:9)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 0 `i32` (phase_type_checking.carbon:9) --->
 // CHECK:STDOUT: (+) stack-push: ExpressionAction pos: 0 `i32` (phase_type_checking.carbon:9)
@@ -32,23 +79,66 @@ fn Main() -> i32 {
 // CHECK:STDOUT: (-) stack-pop:  ExpressionAction pos: 0 `i32` (phase_type_checking.carbon:9)
 // CHECK:STDOUT: --- step ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_type_checking.carbon:9) --->
 // CHECK:STDOUT: (-) stack-pop:  ValueExpressionAction pos: 1 `i32` results: [`i32`]  (phase_type_checking.carbon:9)
-// CHECK:STDOUT: ** finished declaring function Main of type fn () -> i32
-// CHECK:STDOUT: checking FunctionDeclaration
-// CHECK:STDOUT: ** checking function Main
-// CHECK:STDOUT: impl declarations:{{ }}
-// CHECK:STDOUT: impl declarations: bool as interface EqWith(U = bool), i32 as interface EqWith(U = i32), String as interface EqWith(U = String), i32 as interface CompareWith(U = i32), String as interface CompareWith(U = String), i32 as interface LessWith(U = i32), String as interface LessWith(U = String), i32 as interface LessEqWith(U = i32), String as interface LessEqWith(U = String), i32 as interface GreaterWith(U = i32), String as interface GreaterWith(U = String), i32 as interface GreaterEqWith(U = i32), String as interface GreaterEqWith(U = String), i32 as interface Negate, i32 as interface AddWith(U = i32), i32 as interface SubWith(U = i32), i32 as interface MulWith(U = i32), i32 as interface DivWith(U = i32), i32 as interface ModWith(U = i32), i32 as interface BitComplement, i32 as interface BitAndWith(U = i32), i32 as interface BitOrWith(U = i32), i32 as interface BitXorWith(U = i32), i32 as interface LeftShiftWith(U = i32), i32 as interface RightShiftWith(U = i32), i32 as interface Inc, i32 as interface Dec, U as interface __EqualConverter [0], (T1,) as interface As(T = (U1,)) [0, 0, 0; 1, 1, 0, 0, 0], (T1, T2) as interface As(T = (U1, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, U1) as interface EqWith(U = (T2, U2)) [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1], (T1, T2, T3) as interface As(T = (U1, U2, U3)) [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface ImplicitAs(T = U) [0; 1, 1, 0], T as interface As(T = U) [0; 1, 1, 0], T as interface AssignWith(U = U) [0; 1, 1, 0], T as interface AddAssignWith(U = U) [0; 1, 1, 0], T as interface SubAssignWith(U = U) [0; 1, 1, 0], T as interface MulAssignWith(U = U) [0; 1, 1, 0], T as interface DivAssignWith(U = U) [0; 1, 1, 0], T as interface ModAssignWith(U = U) [0; 1, 1, 0], T as interface BitAndAssignWith(U = U) [0; 1, 1, 0], T as interface BitOrAssignWith(U = U) [0; 1, 1, 0], T as interface BitXorAssignWith(U = U) [0; 1, 1, 0], T as interface LeftShiftAssignWith(U = U) [0; 1, 1, 0], T as interface RightShiftAssignWith(U = U) [0; 1, 1, 0]
-// CHECK:STDOUT: checking Block {
-// CHECK:STDOUT: return 0;
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
-// CHECK:STDOUT: checking ReturnExpression return 0;
-// CHECK:STDOUT: checking IntLiteral 0
-// CHECK:STDOUT: ** finished checking function Main
-// CHECK:STDOUT: checking CallExpression Main()
-// CHECK:STDOUT: checking IdentifierExpression Main
-// CHECK:STDOUT: checking TupleLiteral ()
-// CHECK:STDOUT: checking call to function of type fn () -> i32
-// CHECK:STDOUT: with arguments of type: ()
-// CHECK:STDOUT: performing argument deduction for bindings:{{ }}
-// CHECK:STDOUT: deduction succeeded with results: {}
+// CHECK:STDOUT: *** finished declaring function `Main` of type `fn () -> i32` (phase_type_checking.carbon:11)
+// CHECK:STDOUT: *** checking FunctionDeclaration `fn Main` (phase_type_checking.carbon:11)
+// CHECK:STDOUT: *** checking function `Main` (phase_type_checking.carbon:11)
+// CHECK:STDOUT: --- impl declarations for `fn Main` (phase_type_checking.carbon:11)
+// CHECK:STDOUT:  +  []
+// CHECK:STDOUT:  +  [`bool` as `interface EqWith(U = bool)`,
+// CHECK:STDOUT:     `i32` as `interface EqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface EqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface CompareWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface CompareWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface LessEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface LessEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface GreaterEqWith(U = i32)`,
+// CHECK:STDOUT:     `String` as `interface GreaterEqWith(U = String)`,
+// CHECK:STDOUT:     `i32` as `interface Negate`,
+// CHECK:STDOUT:     `i32` as `interface AddWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface SubWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface MulWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface DivWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface ModWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitComplement`,
+// CHECK:STDOUT:     `i32` as `interface BitAndWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitOrWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface BitXorWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface LeftShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface RightShiftWith(U = i32)`,
+// CHECK:STDOUT:     `i32` as `interface Inc`,
+// CHECK:STDOUT:     `i32` as `interface Dec`,
+// CHECK:STDOUT:     `U` as `interface __EqualConverter` [0],
+// CHECK:STDOUT:     `(T1,)` as `interface As(T = (U1,))` [0, 0, 0; 1, 1, 0, 0, 0],
+// CHECK:STDOUT:     `(T1, T2)` as `interface As(T = (U1, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, U1)` as `interface EqWith(U = (T2, U2))` [0, 0, 0; 0, 0, 1; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1],
+// CHECK:STDOUT:     `(T1, T2, T3)` as `interface As(T = (U1, U2, U3))` [0, 0, 0; 0, 0, 1; 0, 0, 2; 1, 1, 0, 0, 0; 1, 1, 0, 0, 1; 1, 1, 0, 0, 2],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ImplicitAs(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface As(T = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface AddAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface SubAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface MulAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface DivAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface ModAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitAndAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitOrAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface BitXorAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface LeftShiftAssignWith(U = U)` [0; 1, 1, 0],
+// CHECK:STDOUT:     `T` as `interface RightShiftAssignWith(U = U)` [0; 1, 1, 0]]
+// CHECK:STDOUT: *** checking Block `{return 0;}` (phase_type_checking.carbon:11)
+// CHECK:STDOUT: *** checking ReturnExpression `return 0;` (phase_type_checking.carbon:10)
+// CHECK:STDOUT: *** checking IntLiteral `0` (phase_type_checking.carbon:10)
+// CHECK:STDOUT: *** finished checking function `Main` (phase_type_checking.carbon:11)
+// CHECK:STDOUT: *** checking CallExpression `Main()` (<Main()>:0)
+// CHECK:STDOUT: *** checking IdentifierExpression `Main` (<Main()>:0)
+// CHECK:STDOUT: *** checking TupleLiteral `()` (<Main()>:0)
+// CHECK:STDOUT: *** checking call to function of type `fn () -> i32` with arguments of type `()` (<Main()>:0)
+// CHECK:STDOUT: *** performing argument deduction for bindings: []
+// CHECK:STDOUT: --> deduction succeeded with results: []
 // CHECK:STDOUT: result: 0