From e652198715d130e25223b5568e6808cb0427da14 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 06:01:51 -0400
Subject: [PATCH 01/22] remove (public) dependency on anyhow

---
 crates/formality-core/src/lib.rs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/crates/formality-core/src/lib.rs b/crates/formality-core/src/lib.rs
index da0aa334..37d3c294 100644
--- a/crates/formality-core/src/lib.rs
+++ b/crates/formality-core/src/lib.rs
@@ -7,6 +7,7 @@
 
 // Re-export things from dependencies to avoid everybody repeating same set
 // in their Cargo.toml.
+pub use anyhow::anyhow;
 pub use anyhow::bail;
 pub use contracts::requires;
 pub use tracing::debug;
@@ -143,7 +144,7 @@ macro_rules! declare_language {
 
             /// Parses `text` as a term with no bindings in scope.
             #[track_caller]
-            pub fn try_term<T>(text: &str) -> anyhow::Result<T>
+            pub fn try_term<T>(text: &str) -> $crate::Fallible<T>
             where
                 T: Parse,
             {
@@ -155,7 +156,7 @@ macro_rules! declare_language {
             /// References to the given string will be replaced with the given parameter
             /// when parsing types, lifetimes, etc.
             #[track_caller]
-            pub fn term_with<T, B>(bindings: impl IntoIterator<Item = B>, text: &str) -> anyhow::Result<T>
+            pub fn term_with<T, B>(bindings: impl IntoIterator<Item = B>, text: &str) -> $crate::Fallible<T>
             where
                 T: Parse,
                 B: $crate::Upcast<(String, $param)>,
@@ -164,7 +165,7 @@ macro_rules! declare_language {
                 let (t, remainder) = match T::parse(&scope, text) {
                     Ok(v) => v,
                     Err(errors) => {
-                        let mut err = anyhow::anyhow!("failed to parse {text}");
+                        let mut err = $crate::anyhow!("failed to parse {text}");
                         for error in errors {
                             err = err.context(error.text.to_owned()).context(error.message);
                         }
@@ -172,7 +173,7 @@ macro_rules! declare_language {
                     }
                 };
                 if !$crate::parse::skip_whitespace(remainder).is_empty() {
-                    anyhow::bail!("extra tokens after parsing {text:?} to {t:?}: {remainder:?}");
+                    $crate::bail!("extra tokens after parsing {text:?} to {t:?}: {remainder:?}");
                 }
                 Ok(t)
             }

From ba7c76d358979f2047857b1714647da80f6e4ac0 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Wed, 1 Nov 2023 21:34:01 -0400
Subject: [PATCH 02/22] support #[variable] attribute

---
 crates/formality-core/src/parse.rs   | 33 +++++++++++++++++++++++++++-
 crates/formality-macros/src/cast.rs  | 10 +++++++--
 crates/formality-macros/src/fold.rs  | 31 ++++++++++++++++++++++----
 crates/formality-macros/src/parse.rs | 19 ++++++++++++----
 crates/formality-macros/src/term.rs  | 14 ++++++++----
 5 files changed, 92 insertions(+), 15 deletions(-)

diff --git a/crates/formality-core/src/parse.rs b/crates/formality-core/src/parse.rs
index 9e434e38..4ee50c6d 100644
--- a/crates/formality-core/src/parse.rs
+++ b/crates/formality-core/src/parse.rs
@@ -4,10 +4,11 @@ use crate::{
     binder::CoreBinder,
     cast::To,
     collections::Set,
-    language::{CoreKind, CoreParameter, Language},
+    language::{CoreKind, CoreParameter, HasKind, Language},
     set,
     term::CoreTerm,
     variable::CoreBoundVar,
+    Downcast, DowncastFrom,
 };
 use std::fmt::Debug;
 
@@ -474,3 +475,33 @@ pub fn skip_whitespace(mut text: &str) -> &str {
         }
     }
 }
+
+/// Parses a variable into a parameter. Variables don't implement Parse themselves
+/// because you can't parse a variable into a *variable*, instead, you parse it into
+/// a Parameter indicating its kind.
+#[tracing::instrument(level = "trace", ret)]
+pub fn parse_variable<'t, L, R>(
+    scope: &Scope<L>,
+    text0: &'t str,
+    type_name: &str,
+) -> ParseResult<'t, R>
+where
+    L: Language,
+    R: Debug + DowncastFrom<CoreParameter<L>>,
+{
+    let (id, text1) = identifier(text0)?;
+    match scope.lookup(&id) {
+        Some(parameter) => match parameter.downcast() {
+            Some(v) => Ok((v, text1)),
+            None => Err(ParseError::at(
+                text0,
+                format!(
+                    "wrong kind, expected a {}, found a {:?}",
+                    type_name,
+                    parameter.kind()
+                ),
+            )),
+        },
+        None => Err(ParseError::at(text0, format!("unrecognized variable"))),
+    }
+}
diff --git a/crates/formality-macros/src/cast.rs b/crates/formality-macros/src/cast.rs
index 10efa4cb..734c2a4f 100644
--- a/crates/formality-macros/src/cast.rs
+++ b/crates/formality-macros/src/cast.rs
@@ -3,11 +3,15 @@ use quote::quote;
 use syn::{Attribute, Type};
 use synstructure::VariantInfo;
 
+use crate::term::has_variable_attr;
+
 pub(crate) fn upcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
     let num_variants = s.variants().len();
     s.variants()
         .iter()
-        .filter(|v| num_variants == 1 || has_cast_attr(v.ast().attrs))
+        .filter(|v| {
+            num_variants == 1 || has_cast_attr(v.ast().attrs) || has_variable_attr(v.ast().attrs)
+        })
         .map(|v| upcast_to_variant(&s, v))
         .chain(Some(self_upcast(&s)))
         .collect()
@@ -46,7 +50,9 @@ pub(crate) fn downcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
     let num_variants = s.variants().len();
     s.variants()
         .iter()
-        .filter(|v| num_variants == 1 || has_cast_attr(v.ast().attrs))
+        .filter(|v| {
+            num_variants == 1 || has_cast_attr(v.ast().attrs) || has_variable_attr(v.ast().attrs)
+        })
         .map(|v| downcast_to_variant(&s, v))
         .chain(Some(self_downcast(&s)))
         .collect()
diff --git a/crates/formality-macros/src/fold.rs b/crates/formality-macros/src/fold.rs
index 139efbab..02375716 100644
--- a/crates/formality-macros/src/fold.rs
+++ b/crates/formality-macros/src/fold.rs
@@ -3,18 +3,41 @@ extern crate proc_macro;
 use proc_macro2::TokenStream;
 use quote::quote;
 
+use crate::term::has_variable_attr;
+
 pub(crate) fn derive_fold(mut s: synstructure::Structure) -> TokenStream {
     s.underscore_const(true);
     s.bind_with(|_| synstructure::BindStyle::Move);
 
     let substitute_body = s.each_variant(|vi| {
         let bindings = vi.bindings();
-        vi.construct(|_, index| {
-            let bind = &bindings[index];
+        if has_variable_attr(&vi.ast().attrs) {
+            if bindings.len() != 1 {
+                return syn::Error::new(
+                    vi.ast().ident.span(),
+                    "#[variable] can only be used on variants with 1 binding",
+                )
+                .into_compile_error();
+            }
+
+            let bi = &bindings[0];
+
             quote! {
-                CoreFold::substitute(#bind, substitution_fn)
+                if let Some(p) = substitution_fn(*#bi) {
+                    formality_core::Downcast::downcast(&p)
+                        .unwrap_or_else(|| panic!("ill-kinded value `{:?}`", p))
+                } else {
+                    Clone::clone(self)
+                }
             }
-        })
+        } else {
+            vi.construct(|_, index| {
+                let bind = &bindings[index];
+                quote! {
+                    CoreFold::substitute(#bind, substitution_fn)
+                }
+            })
+        }
     });
 
     // s.add_bounds(synstructure::AddBounds::None);
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 7e7f5b5e..436e92c5 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -5,7 +5,10 @@ use quote::{quote, quote_spanned};
 use syn::{spanned::Spanned, Attribute};
 use synstructure::BindingInfo;
 
-use crate::spec::{self, FieldMode, FormalitySpec, FormalitySpecOp};
+use crate::{
+    spec::{self, FieldMode, FormalitySpec, FormalitySpecOp},
+    term::has_variable_attr,
+};
 
 /// Derive the `Parse` impl, using an optional grammar supplied "from the outside".
 /// This is used by the `#[term(G)]` macro, which supplies the grammar `G`.
@@ -25,14 +28,14 @@ pub(crate) fn derive_parse_with_spec(
     let type_name = Literal::string(&format!("`{}`", s.ast().ident));
 
     if s.variants().len() == 1 {
-        stream.extend(parse_variant(&s.variants()[0], external_spec));
+        stream.extend(parse_variant(&type_name, &s.variants()[0], external_spec));
     } else {
         stream.extend(quote! {
             let mut __results = vec![];
         });
         for variant in s.variants() {
             let variant_name = as_literal(variant.ast().ident);
-            let v = parse_variant(variant, None)?;
+            let v = parse_variant(&type_name, variant, None)?;
             stream.extend(quote! {
                 __results.push({
                     let __span = tracing::span!(tracing::Level::TRACE, "parse", variant_name = #variant_name);
@@ -44,7 +47,7 @@ pub(crate) fn derive_parse_with_spec(
         stream.extend(quote! {parse::require_unambiguous(text, __results, #type_name)});
     }
 
-    let type_name = as_literal(&s.ast().ident);
+    let type_name: Literal = as_literal(&s.ast().ident);
     Ok(s.gen_impl(quote! {
         use formality_core::parse;
 
@@ -62,6 +65,7 @@ pub(crate) fn derive_parse_with_spec(
 }
 
 fn parse_variant(
+    type_name: &Literal,
     variant: &synstructure::VariantInfo,
     external_spec: Option<&FormalitySpec>,
 ) -> syn::Result<TokenStream> {
@@ -87,6 +91,13 @@ fn parse_variant(
             let ((), text) = parse::expect_keyword(#literal, text)?;
             Ok((#construct, text))
         })
+    } else if has_variable_attr(variant.ast().attrs) {
+        // Has the `#[variable]` attribute -- parse an identifier and then check to see if it is present
+        // in the scope. If so, downcast it and check that it has the correct kind.
+        Ok(quote_spanned! {
+            ast.ident.span() =>
+            parse::parse_variable(scope, text, #type_name)
+        })
     } else if crate::cast::has_cast_attr(variant.ast().attrs) {
         // Has the `#[cast]` attribute -- just parse the bindings (comma separated, if needed)
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
diff --git a/crates/formality-macros/src/term.rs b/crates/formality-macros/src/term.rs
index 72c65847..31899552 100644
--- a/crates/formality-macros/src/term.rs
+++ b/crates/formality-macros/src/term.rs
@@ -1,6 +1,6 @@
 use proc_macro2::TokenStream;
 use quote::quote;
-use syn::DeriveInput;
+use syn::{Attribute, DeriveInput};
 
 use crate::{
     cast::{downcast_impls, upcast_impls},
@@ -38,9 +38,11 @@ pub fn term(spec: Option<FormalitySpec>, mut input: DeriveInput) -> syn::Result<
 fn remove_formality_attributes(input: &mut DeriveInput) {
     if let syn::Data::Enum(v) = &mut input.data {
         for variant in &mut v.variants {
-            variant
-                .attrs
-                .retain(|attr| !attr.path().is_ident("grammar") && !attr.path().is_ident("cast"));
+            variant.attrs.retain(|attr| {
+                !attr.path().is_ident("grammar")
+                    && !attr.path().is_ident("cast")
+                    && !attr.path().is_ident("variable")
+            });
         }
     }
 }
@@ -57,3 +59,7 @@ fn derive_term(mut s: synstructure::Structure) -> TokenStream {
         }
     })
 }
+
+pub(crate) fn has_variable_attr(attrs: &[Attribute]) -> bool {
+    attrs.iter().any(|a| a.path().is_ident("variable"))
+}

From a4794c1e615ba1d07bc9888e7b6e85caaab59c01 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 06:05:18 -0400
Subject: [PATCH 03/22] propagate errors in `parse_variant`

otherwise they just get swallowed up for some reason
---
 crates/formality-macros/src/parse.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 436e92c5..ceca74e2 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -28,7 +28,7 @@ pub(crate) fn derive_parse_with_spec(
     let type_name = Literal::string(&format!("`{}`", s.ast().ident));
 
     if s.variants().len() == 1 {
-        stream.extend(parse_variant(&type_name, &s.variants()[0], external_spec));
+        stream.extend(parse_variant(&type_name, &s.variants()[0], external_spec)?);
     } else {
         stream.extend(quote! {
             let mut __results = vec![];

From a0705d937d70f727cfe2793708639546f5e8970c Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 06:05:54 -0400
Subject: [PATCH 04/22] support `$*x` without delimeter

It only makes sense though if the type `x` begins with a separator.
---
 crates/formality-core/src/parse.rs   | 35 +++++++++++++++++++++++++-
 crates/formality-macros/src/parse.rs | 37 +++++++++++++++++-----------
 crates/formality-macros/src/spec.rs  | 15 +++++++++++
 3 files changed, 71 insertions(+), 16 deletions(-)

diff --git a/crates/formality-core/src/parse.rs b/crates/formality-core/src/parse.rs
index 4ee50c6d..7d7193f3 100644
--- a/crates/formality-core/src/parse.rs
+++ b/crates/formality-core/src/parse.rs
@@ -34,6 +34,16 @@ pub trait CoreParse<L: Language>: Sized + Debug {
         Ok((result, text))
     }
 
+    /// Continue parsing instances of self while we can.
+    fn parse_while_possible<'t>(scope: &Scope<L>, mut text: &'t str) -> ParseResult<'t, Vec<Self>> {
+        let mut result = vec![];
+        while let (Some(e), text1) = Self::parse_opt(scope, text)? {
+            result.push(e);
+            text = text1;
+        }
+        Ok((result, text))
+    }
+
     /// Comma separated list with optional trailing comma.
     fn parse_comma<'t>(
         scope: &Scope<L>,
@@ -55,6 +65,23 @@ pub trait CoreParse<L: Language>: Sized + Debug {
 
         Ok((result, text))
     }
+
+    /// Try to parse the current point as `Self`. If failure occurs, check
+    /// whether we consumed any tokens -- if so, return the resulting errors we
+    /// encountered as a parse failure. Otherwise, substitute a default Self.
+    fn parse_opt<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Option<Self>> {
+        match Self::parse(scope, text) {
+            Ok((v, text)) => Ok((Some(v), text)),
+            Err(mut errs) => {
+                errs.retain(|e| e.consumed_any_since(text));
+                if errs.is_empty() {
+                    Ok((None, text))
+                } else {
+                    Err(errs)
+                }
+            }
+        }
+    }
 }
 
 /// Tracks an error that occurred while parsing.
@@ -94,6 +121,12 @@ impl<'t> ParseError<'t> {
         let o = self.offset(text);
         &text[..o]
     }
+
+    /// True if any tokens were consumed before this error occurred,
+    /// with `text` as the starting point of the parse.
+    pub fn consumed_any_since(&self, text: &str) -> bool {
+        !skip_whitespace(self.consumed_before(text)).is_empty()
+    }
 }
 
 pub type ParseResult<'t, T> = Result<(T, &'t str), Set<ParseError<'t>>>;
@@ -364,7 +397,7 @@ where
                 for e in es {
                     // only include an error if the error resulted after at least
                     // one non-whitespace character was consumed
-                    if !skip_whitespace(e.consumed_before(text)).is_empty() {
+                    if e.consumed_any_since(text) {
                         errors.insert(e);
                     }
                 }
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index ceca74e2..4930eb5e 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -161,9 +161,13 @@ fn parse_variant_with_attr(
                 name,
                 mode: FieldMode::Many,
             } => {
-                let lookahead = lookahead(name, next_op)?;
-                quote_spanned! {
-                    name.span() => let (#name, text) = parse::CoreParse::parse_many(scope, text, #lookahead)?;
+                match lookahead(next_op) {
+                    Some(lookahead) => quote_spanned! {
+                        name.span() => let (#name, text) = parse::CoreParse::parse_many(scope, text, #lookahead)?;
+                    },
+                    None => quote_spanned! {
+                        name.span() => let (#name, text) = parse::CoreParse::parse_while_possible(scope, text)?;
+                    },
                 }
             }
 
@@ -171,10 +175,18 @@ fn parse_variant_with_attr(
                 name,
                 mode: FieldMode::Comma,
             } => {
-                let lookahead = lookahead(name, next_op)?;
-                quote_spanned! {
-                    name.span() => let (#name, text) = parse::CoreParse::parse_comma(scope, text, #lookahead)?;
+                match lookahead(next_op) {
+                    Some(lookahead) => quote_spanned! {
+                        name.span() => let (#name, text) = parse::CoreParse::parse_comma(scope, text, #lookahead)?;
+                    },
+                    None => {
+                        return Err(syn::Error::new_spanned(
+                            name,
+                            "cannot use `,` without lookahead".to_string(),
+                        ));
+                    }
                 }
+                
             }
 
             spec::FormalitySpecOp::Keyword { ident } => {
@@ -203,16 +215,11 @@ fn parse_variant_with_attr(
     Ok(stream)
 }
 
-fn lookahead(for_field: &Ident, op: Option<&FormalitySpecOp>) -> syn::Result<Literal> {
+fn lookahead(op: Option<&FormalitySpecOp>) -> Option<Literal> {
     match op {
-        Some(FormalitySpecOp::Char { punct }) => Ok(Literal::character(punct.as_char())),
-        Some(FormalitySpecOp::Delimeter { text }) => Ok(Literal::character(*text)),
-        Some(FormalitySpecOp::Keyword { .. }) | Some(FormalitySpecOp::Field { .. }) | None => {
-            Err(syn::Error::new_spanned(
-                for_field,
-                "cannot use `*` or `,` without lookahead".to_string(),
-            ))
-        }
+        Some(FormalitySpecOp::Char { punct }) => Some(Literal::character(punct.as_char())),
+        Some(FormalitySpecOp::Delimeter { text }) => Some(Literal::character(*text)),
+        Some(FormalitySpecOp::Keyword { .. }) | Some(FormalitySpecOp::Field { .. }) | None => None,
     }
 }
 
diff --git a/crates/formality-macros/src/spec.rs b/crates/formality-macros/src/spec.rs
index 9faad894..8bdb532b 100644
--- a/crates/formality-macros/src/spec.rs
+++ b/crates/formality-macros/src/spec.rs
@@ -8,10 +8,12 @@ use proc_macro2::{Ident, Punct, TokenStream, TokenTree};
 /// * a field like `$foo` parses the type of the declared field
 ///     * you can also do `$*foo` to use the `parse_many` option
 /// * a character like `<` is parsed as is; a group like `[..]` parses a `[`, the contents, and then `]`
+#[derive(Debug)]
 pub struct FormalitySpec {
     pub ops: Vec<FormalitySpecOp>,
 }
 
+#[derive(Debug)]
 pub enum FormalitySpecOp {
     /// `$foo` or `$foo*` -- indicates we should parse the type of the given field.
     Field { name: Ident, mode: FieldMode },
@@ -26,9 +28,22 @@ pub enum FormalitySpecOp {
     Delimeter { text: char },
 }
 
+#[derive(Debug)]
 pub enum FieldMode {
+    /// $x -- just parse `x`
     Single,
+
+    /// $*x -- `x` is a `Vec<E>`, parse multiple `E`
+    ///
+    /// If the next op is a fixed character, stop parsing when we see that.
+    /// Otherwise parse as many we can greedily.
     Many,
+
+    /// $*x -- `x` is a `Vec<E>`, parse comma separated list of `E`
+    /// (with optonal trailing comma)
+    ///
+    /// If the next op is a fixed character, stop parsing when we see that.
+    /// Otherwise parse as many we can greedily.
     Comma,
 }
 

From c80176f771a50c29e6fb6a70f41a2218b1b52aa5 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 06:16:43 -0400
Subject: [PATCH 05/22] support optional fields

You can do `$?` to try and parse something.
This is convenient.
---
 crates/formality-macros/src/debug.rs |  2 +-
 crates/formality-macros/src/parse.rs | 11 +++++++++++
 crates/formality-macros/src/spec.rs  |  4 ++++
 3 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index 2f7de119..2cc84a05 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -149,7 +149,7 @@ fn debug_variant_with_attr(
         stream.extend(match op {
             spec::FormalitySpecOp::Field {
                 name,
-                mode: FieldMode::Single,
+                mode: FieldMode::Single | FieldMode::Optional,
             } => {
                 quote_spanned! {
                     name.span() =>
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 4930eb5e..736bd9db 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -157,6 +157,17 @@ fn parse_variant_with_attr(
                 }
             }
 
+            spec::FormalitySpecOp::Field {
+                name,
+                mode: FieldMode::Optional,
+            } => {
+                quote_spanned! {
+                    name.span() => 
+                    let (#name, text) = parse::CoreParse::parse_opt(scope, text)?;
+                    let #name = #name.unwrap_or_default();
+                }
+            }
+
             spec::FormalitySpecOp::Field {
                 name,
                 mode: FieldMode::Many,
diff --git a/crates/formality-macros/src/spec.rs b/crates/formality-macros/src/spec.rs
index 8bdb532b..5f9a656b 100644
--- a/crates/formality-macros/src/spec.rs
+++ b/crates/formality-macros/src/spec.rs
@@ -45,6 +45,9 @@ pub enum FieldMode {
     /// If the next op is a fixed character, stop parsing when we see that.
     /// Otherwise parse as many we can greedily.
     Comma,
+
+    /// $?x -- parse `x` if we can, but otherwise use `Default`
+    Optional,
 }
 
 impl syn::parse::Parse for FormalitySpec {
@@ -124,6 +127,7 @@ fn parse_variable_binding(
             let mode = match punct.as_char() {
                 ',' => FieldMode::Comma,
                 '*' => FieldMode::Many,
+                '?' => FieldMode::Optional,
                 '$' => return Ok(FormalitySpecOp::Char { punct }),
                 _ => return error(),
             };

From e515e55e12ecbcd2e82c505a382b9e299399e482 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 06:17:37 -0400
Subject: [PATCH 06/22] switch parsing for option to use parse_opt

This is a subtle change in the semantics.
---
 crates/formality-core/src/parse.rs | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/crates/formality-core/src/parse.rs b/crates/formality-core/src/parse.rs
index 7d7193f3..4b31b430 100644
--- a/crates/formality-core/src/parse.rs
+++ b/crates/formality-core/src/parse.rs
@@ -211,10 +211,7 @@ where
 {
     #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        match T::parse(scope, text) {
-            Ok((value, text)) => Ok((Some(value), text)),
-            Err(_) => Ok((None, text)),
-        }
+        T::parse_opt(scope, text)
     }
 }
 

From 2fcc2d6e6bb4383bed285aed7eb94da228a8fdea Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 06:24:54 -0400
Subject: [PATCH 07/22] get more struct about supplying external spec

---
 crates/formality-macros/src/parse.rs | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 736bd9db..916ec2a9 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -27,9 +27,19 @@ pub(crate) fn derive_parse_with_spec(
 
     let type_name = Literal::string(&format!("`{}`", s.ast().ident));
 
-    if s.variants().len() == 1 {
+    if let syn::Data::Struct(_) = s.ast().data {
+        // For structs, where there is only one variant, use the external grammar (if any).
         stream.extend(parse_variant(&type_name, &s.variants()[0], external_spec)?);
     } else {
+        // If there are multiple variants, there should not be an external grammar.
+        // Parse them all and require an unambiguous parse.
+        if external_spec.is_some() {
+            return Err(syn::Error::new_spanned(
+                &s.ast().ident,
+                "for enums provide the grammar on each variant".to_string(),
+            ));
+        }
+
         stream.extend(quote! {
             let mut __results = vec![];
         });

From 606cb2c74fa74c26fe59b8b67707876ef2da6ebe Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 08:03:17 -0400
Subject: [PATCH 08/22] extract the attrs code and better document meaning

---
 crates/formality-macros/src/attrs.rs | 56 ++++++++++++++++++++++++++++
 crates/formality-macros/src/cast.rs  | 16 ++------
 crates/formality-macros/src/debug.rs |  7 +++-
 crates/formality-macros/src/fold.rs  |  2 +-
 crates/formality-macros/src/lib.rs   |  1 +
 crates/formality-macros/src/parse.rs |  4 +-
 crates/formality-macros/src/term.rs  | 19 +---------
 7 files changed, 71 insertions(+), 34 deletions(-)
 create mode 100644 crates/formality-macros/src/attrs.rs

diff --git a/crates/formality-macros/src/attrs.rs b/crates/formality-macros/src/attrs.rs
new file mode 100644
index 00000000..36229b06
--- /dev/null
+++ b/crates/formality-macros/src/attrs.rs
@@ -0,0 +1,56 @@
+//! Functions to manipulate the custom attributes that guide our macros in various ways.
+
+use syn::{Attribute, DeriveInput};
+
+/// Checks for any kind of attribute that indicates an "is-a" relationship,
+/// e.g. `#[cast]` and `#[variable]`.
+///
+/// See [`has_cast_attr`][] and [`has_variable_attr`][] for more details.
+pub(crate) fn has_isa_attr(attrs: &[Attribute]) -> bool {
+    has_cast_attr(attrs) || has_variable_attr(attrs)
+}
+
+/// The `#[cast]` attribute is placed on enum variants with a single binding,
+/// like `enum Foo { #[cast] Bar(Bar), ... }`. It indicates that `Foo` is an
+/// extension of `Bar`, so we should permit upcasts from `Bar` to `Foo`
+/// and generally ignore the fact that `Bar` is a variant of `Foo` (for example,
+/// in debug print-outs, we don't print `Bar(...)`, we just print `...`).
+pub(crate) fn has_cast_attr(attrs: &[Attribute]) -> bool {
+    attrs.iter().any(|a| a.path().is_ident("cast"))
+}
+
+/// The `#[variable]` attribute is a special-case of `#[cast]` that is used
+/// for variables. It can only be used on a single-entry variant in some type
+/// that is up/down-castable to the language's `Parameter` type (e.g., in Rust,
+/// this could be used in `Ty`, `Lifetime`, or `Const`).
+///
+/// `#[variable]` has subtle effects on folding and parsing:
+///
+/// * When folding a variable variant, we apply the substitution function, which yields
+///   a Parameter. We then downcast that to the type needed. If that downcast
+///   fails, we panic, as that indicates an ill-kinded substitution.
+/// * When parsing a variable variant, we parse an identifier and then check the in-scope
+///   bindings for variables with that name. If any are found, we extract the result
+///   (a parameter) and downcast it. If the resulting downcast fails, that is considered
+///   a parse error (ill-kinded term).
+pub(crate) fn has_variable_attr(attrs: &[Attribute]) -> bool {
+    attrs.iter().any(|a| a.path().is_ident("variable"))
+}
+
+/// Removes all attributes from the input that are specific to formality.
+pub(crate) fn remove_formality_attributes(input: &mut DeriveInput) {
+    remove_formality_attributes_from_vec(&mut input.attrs);
+    if let syn::Data::Enum(v) = &mut input.data {
+        for variant in &mut v.variants {
+            remove_formality_attributes_from_vec(&mut variant.attrs);
+        }
+    }
+}
+
+fn remove_formality_attributes_from_vec(attrs: &mut Vec<Attribute>) {
+    attrs.retain(|attr| {
+        !attr.path().is_ident("grammar")
+            && !attr.path().is_ident("cast")
+            && !attr.path().is_ident("variable")
+    });
+}
diff --git a/crates/formality-macros/src/cast.rs b/crates/formality-macros/src/cast.rs
index 734c2a4f..11848481 100644
--- a/crates/formality-macros/src/cast.rs
+++ b/crates/formality-macros/src/cast.rs
@@ -1,17 +1,15 @@
 use proc_macro2::TokenStream;
 use quote::quote;
-use syn::{Attribute, Type};
+use syn::Type;
 use synstructure::VariantInfo;
 
-use crate::term::has_variable_attr;
+use crate::attrs::has_isa_attr;
 
 pub(crate) fn upcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
     let num_variants = s.variants().len();
     s.variants()
         .iter()
-        .filter(|v| {
-            num_variants == 1 || has_cast_attr(v.ast().attrs) || has_variable_attr(v.ast().attrs)
-        })
+        .filter(|v| num_variants == 1 || has_isa_attr(v.ast().attrs))
         .map(|v| upcast_to_variant(&s, v))
         .chain(Some(self_upcast(&s)))
         .collect()
@@ -50,9 +48,7 @@ pub(crate) fn downcast_impls(s: synstructure::Structure) -> Vec<TokenStream> {
     let num_variants = s.variants().len();
     s.variants()
         .iter()
-        .filter(|v| {
-            num_variants == 1 || has_cast_attr(v.ast().attrs) || has_variable_attr(v.ast().attrs)
-        })
+        .filter(|v| num_variants == 1 || has_isa_attr(v.ast().attrs))
         .map(|v| downcast_to_variant(&s, v))
         .chain(Some(self_downcast(&s)))
         .collect()
@@ -95,7 +91,3 @@ fn downcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStr
         }
     })
 }
-
-pub(crate) fn has_cast_attr(attrs: &[Attribute]) -> bool {
-    attrs.iter().any(|a| a.path().is_ident("cast"))
-}
diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index 2cc84a05..f0e81038 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -4,7 +4,10 @@ use proc_macro2::{Ident, Literal, TokenStream};
 use quote::{quote, quote_spanned};
 use syn::{spanned::Spanned, Attribute};
 
-use crate::spec::{self, FieldMode, FormalitySpec, FormalitySpecOp};
+use crate::{
+    attrs,
+    spec::{self, FieldMode, FormalitySpec, FormalitySpecOp},
+};
 
 /// Derive the `Parse` impl, using an optional grammar supplied "from the outside".
 /// This is used by the `#[term(G)]` macro, which supplies the grammar `G`.
@@ -62,7 +65,7 @@ fn debug_variant(
         quote! {
             write!(fmt, #literal)?;
         }
-    } else if crate::cast::has_cast_attr(variant.ast().attrs) {
+    } else if attrs::has_isa_attr(variant.ast().attrs) {
         let streams: Vec<_> = variant
             .bindings()
             .iter()
diff --git a/crates/formality-macros/src/fold.rs b/crates/formality-macros/src/fold.rs
index 02375716..9a7a1975 100644
--- a/crates/formality-macros/src/fold.rs
+++ b/crates/formality-macros/src/fold.rs
@@ -3,7 +3,7 @@ extern crate proc_macro;
 use proc_macro2::TokenStream;
 use quote::quote;
 
-use crate::term::has_variable_attr;
+use crate::attrs::has_variable_attr;
 
 pub(crate) fn derive_fold(mut s: synstructure::Structure) -> TokenStream {
     s.underscore_const(true);
diff --git a/crates/formality-macros/src/lib.rs b/crates/formality-macros/src/lib.rs
index c487a857..e231dd7b 100644
--- a/crates/formality-macros/src/lib.rs
+++ b/crates/formality-macros/src/lib.rs
@@ -5,6 +5,7 @@ use spec::FormalitySpec;
 
 extern crate proc_macro;
 
+mod attrs;
 mod cast;
 mod debug;
 mod fixed_point;
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 916ec2a9..1fb89917 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -7,7 +7,7 @@ use synstructure::BindingInfo;
 
 use crate::{
     spec::{self, FieldMode, FormalitySpec, FormalitySpecOp},
-    term::has_variable_attr,
+    attrs::{has_variable_attr, has_cast_attr},
 };
 
 /// Derive the `Parse` impl, using an optional grammar supplied "from the outside".
@@ -108,7 +108,7 @@ fn parse_variant(
             ast.ident.span() =>
             parse::parse_variable(scope, text, #type_name)
         })
-    } else if crate::cast::has_cast_attr(variant.ast().attrs) {
+    } else if has_cast_attr(variant.ast().attrs) {
         // Has the `#[cast]` attribute -- just parse the bindings (comma separated, if needed)
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
         let construct = variant.construct(field_ident);
diff --git a/crates/formality-macros/src/term.rs b/crates/formality-macros/src/term.rs
index 31899552..4f680ca3 100644
--- a/crates/formality-macros/src/term.rs
+++ b/crates/formality-macros/src/term.rs
@@ -1,8 +1,9 @@
 use proc_macro2::TokenStream;
 use quote::quote;
-use syn::{Attribute, DeriveInput};
+use syn::DeriveInput;
 
 use crate::{
+    attrs::remove_formality_attributes,
     cast::{downcast_impls, upcast_impls},
     debug::derive_debug_with_spec,
     fold::derive_fold,
@@ -35,18 +36,6 @@ pub fn term(spec: Option<FormalitySpec>, mut input: DeriveInput) -> syn::Result<
     })
 }
 
-fn remove_formality_attributes(input: &mut DeriveInput) {
-    if let syn::Data::Enum(v) = &mut input.data {
-        for variant in &mut v.variants {
-            variant.attrs.retain(|attr| {
-                !attr.path().is_ident("grammar")
-                    && !attr.path().is_ident("cast")
-                    && !attr.path().is_ident("variable")
-            });
-        }
-    }
-}
-
 fn derive_term(mut s: synstructure::Structure) -> TokenStream {
     s.underscore_const(true);
     s.bind_with(|_| synstructure::BindStyle::Move);
@@ -59,7 +48,3 @@ fn derive_term(mut s: synstructure::Structure) -> TokenStream {
         }
     })
 }
-
-pub(crate) fn has_variable_attr(attrs: &[Attribute]) -> bool {
-    attrs.iter().any(|a| a.path().is_ident("variable"))
-}

From 4460fbc9901b90d5cd8385463644aed38b46aa94 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 08:07:06 -0400
Subject: [PATCH 09/22] document the variable attr

---
 book/src/formality_core/terms.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/book/src/formality_core/terms.md b/book/src/formality_core/terms.md
index fc328019..7711e492 100644
--- a/book/src/formality_core/terms.md
+++ b/book/src/formality_core/terms.md
@@ -35,7 +35,8 @@ The `#[term]` macro says that these are terms and we should generate all the boi
 
 The `#[term]` also accepts some internal annotations:
 
-* `#[cast]` can be applied on an enum variant with a single argument. It says that we should generate upcast/downcast impls to allow conversion. In this case, between a `Variable` and an `Expr`. This would generate an impl `Variable: Upcast<Expr>` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast<Variable>` that lets you try to convert from an expression to a variable. Downcasting is *fallible*, which means that the downcast will only succeed if this is an `Expr::Variable`. If this is a `Expr::Add`, the downcast would return `None`.
+* `#[cast]` can be applied on an enum variant with a single argument. It says that this variant represents an "is-a" relationship and hence we should generate upcast/downcast impls to allow conversion. In this case, a variable is a kind of expression -- i.e,. wrapping a variable up into an expression doesn't carry any semantic meaning -- so we want variables to be upcastable to expressions (and expressions to be downcast to variables). The `#[cast]` attribute will therefore generate an impl `Variable: Upcast<Expr>` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast<Variable>` that lets you try to convert from an expression to a variable. Downcasting is *fallible*, which means that the downcast will only succeed if this is an `Expr::Variable`. If this is a `Expr::Add`, the downcast would return `None`.
+    * There is a special case version of `#[cast]` called `#[variable]`. It indicates that the variant represents a (type) variable -- we are not using it here because this an expression variable. Variables are rather specially in folding/parsing to allow for substitution, binders, etc.
 * `#[grammar]` tells the parser and pretty printer how to parse this variant. The `$v0` and `$v1` mean "recursively parse the first and second arguments". This will parse a `Box<Expr>`, which of course is implemented to just parse an `Expr`.
 
 If you are annotating a struct, the `#[term]` just accepts the grammar directly, so `#[term($name)] struct Variable`  means "to parse a variable, just parse the name field (a string)".

From 3631d6e89101e93d7ac9ba250a6d79c1aeaceaba Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 08:19:16 -0400
Subject: [PATCH 10/22] use more standard parsing terminology

not sure why I called it *op* when it's just a symbol
---
 crates/formality-macros/src/debug.rs | 31 +++++++++++++----------
 crates/formality-macros/src/parse.rs | 38 ++++++++++++++--------------
 crates/formality-macros/src/spec.rs  | 34 ++++++++++++-------------
 3 files changed, 53 insertions(+), 50 deletions(-)

diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index f0e81038..ec0241c3 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -6,7 +6,7 @@ use syn::{spanned::Spanned, Attribute};
 
 use crate::{
     attrs,
-    spec::{self, FieldMode, FormalitySpec, FormalitySpecOp},
+    spec::{self, FieldMode, FormalitySpec, FormalitySpecSymbol},
 };
 
 /// Derive the `Parse` impl, using an optional grammar supplied "from the outside".
@@ -122,23 +122,26 @@ fn debug_variant_with_attr(
 
     stream.extend(quote!(let mut sep = "";));
 
-    let mut prev_op: Option<&FormalitySpecOp> = None;
-    for op in &spec.ops {
+    let mut prev_op: Option<&FormalitySpecSymbol> = None;
+    for op in &spec.symbols {
         // insert whitespace if needed
         let suppress_space = match (prev_op, op) {
             // consecutive characters don't need spaces
-            (Some(spec::FormalitySpecOp::Char { .. }), spec::FormalitySpecOp::Char { .. }) => true,
+            (
+                Some(spec::FormalitySpecSymbol::Char { .. }),
+                spec::FormalitySpecSymbol::Char { .. },
+            ) => true,
 
             // `foo(` looks better than `foo (`
             (
-                Some(spec::FormalitySpecOp::Keyword { .. }),
-                spec::FormalitySpecOp::Delimeter { .. },
+                Some(spec::FormalitySpecSymbol::Keyword { .. }),
+                spec::FormalitySpecSymbol::Delimeter { .. },
             ) => true,
 
             // consecutive delimeters don't need spaces
             (
-                Some(spec::FormalitySpecOp::Delimeter { .. }),
-                spec::FormalitySpecOp::Delimeter { .. },
+                Some(spec::FormalitySpecSymbol::Delimeter { .. }),
+                spec::FormalitySpecSymbol::Delimeter { .. },
             ) => true,
 
             _ => false,
@@ -150,7 +153,7 @@ fn debug_variant_with_attr(
         }
 
         stream.extend(match op {
-            spec::FormalitySpecOp::Field {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Single | FieldMode::Optional,
             } => {
@@ -162,7 +165,7 @@ fn debug_variant_with_attr(
                 }
             }
 
-            spec::FormalitySpecOp::Field {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Many,
             } => {
@@ -176,7 +179,7 @@ fn debug_variant_with_attr(
                 }
             }
 
-            spec::FormalitySpecOp::Field {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Comma,
             } => {
@@ -191,7 +194,7 @@ fn debug_variant_with_attr(
                 }
             }
 
-            spec::FormalitySpecOp::Keyword { ident } => {
+            spec::FormalitySpecSymbol::Keyword { ident } => {
                 let literal = as_literal(ident);
                 quote_spanned!(ident.span() =>
                     write!(fmt, "{}", sep)?;
@@ -200,7 +203,7 @@ fn debug_variant_with_attr(
                 )
             }
 
-            spec::FormalitySpecOp::Char { punct } => {
+            spec::FormalitySpecSymbol::Char { punct } => {
                 let literal = Literal::character(punct.as_char());
                 quote_spanned!(punct.span() =>
                     write!(fmt, "{}", sep)?;
@@ -209,7 +212,7 @@ fn debug_variant_with_attr(
                 )
             }
 
-            spec::FormalitySpecOp::Delimeter { text } => match text {
+            spec::FormalitySpecSymbol::Delimeter { text } => match text {
                 '{' | '}' => {
                     let literal = Literal::character(*text);
                     quote!(
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 1fb89917..cae1de68 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -6,7 +6,7 @@ use syn::{spanned::Spanned, Attribute};
 use synstructure::BindingInfo;
 
 use crate::{
-    spec::{self, FieldMode, FormalitySpec, FormalitySpecOp},
+    spec::{self, FieldMode, FormalitySpec, FormalitySpecSymbol},
     attrs::{has_variable_attr, has_cast_attr},
 };
 
@@ -154,11 +154,11 @@ fn parse_variant_with_attr(
 ) -> syn::Result<TokenStream> {
     let mut stream = TokenStream::new();
 
-    for i in 0..spec.ops.len() {
-        let op = &spec.ops[i];
-        let next_op = spec.ops.get(i + 1);
-        stream.extend(match op {
-            spec::FormalitySpecOp::Field {
+    for i in 0..spec.symbols.len() {
+        let symbol = &spec.symbols[i];
+        let next_symbol = spec.symbols.get(i + 1);
+        stream.extend(match symbol {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Single,
             } => {
@@ -167,7 +167,7 @@ fn parse_variant_with_attr(
                 }
             }
 
-            spec::FormalitySpecOp::Field {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Optional,
             } => {
@@ -178,11 +178,11 @@ fn parse_variant_with_attr(
                 }
             }
 
-            spec::FormalitySpecOp::Field {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Many,
             } => {
-                match lookahead(next_op) {
+                match lookahead(next_symbol) {
                     Some(lookahead) => quote_spanned! {
                         name.span() => let (#name, text) = parse::CoreParse::parse_many(scope, text, #lookahead)?;
                     },
@@ -192,11 +192,11 @@ fn parse_variant_with_attr(
                 }
             }
 
-            spec::FormalitySpecOp::Field {
+            spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Comma,
             } => {
-                match lookahead(next_op) {
+                match lookahead(next_symbol) {
                     Some(lookahead) => quote_spanned! {
                         name.span() => let (#name, text) = parse::CoreParse::parse_comma(scope, text, #lookahead)?;
                     },
@@ -210,17 +210,17 @@ fn parse_variant_with_attr(
                 
             }
 
-            spec::FormalitySpecOp::Keyword { ident } => {
+            spec::FormalitySpecSymbol::Keyword { ident } => {
                 let literal = as_literal(ident);
                 quote_spanned!(ident.span() => let ((), text) = parse::expect_keyword(#literal, text)?;)
             }
 
-            spec::FormalitySpecOp::Char { punct } => {
+            spec::FormalitySpecSymbol::Char { punct } => {
                 let literal = Literal::character(punct.as_char());
                 quote_spanned!(punct.span() => let ((), text) = parse::expect_char(#literal, text)?;)
             }
 
-            spec::FormalitySpecOp::Delimeter { text } => {
+            spec::FormalitySpecSymbol::Delimeter { text } => {
                 let literal = Literal::character(*text);
                 quote!(let ((), text) = parse::expect_char(#literal, text)?;)
             }
@@ -236,11 +236,11 @@ fn parse_variant_with_attr(
     Ok(stream)
 }
 
-fn lookahead(op: Option<&FormalitySpecOp>) -> Option<Literal> {
-    match op {
-        Some(FormalitySpecOp::Char { punct }) => Some(Literal::character(punct.as_char())),
-        Some(FormalitySpecOp::Delimeter { text }) => Some(Literal::character(*text)),
-        Some(FormalitySpecOp::Keyword { .. }) | Some(FormalitySpecOp::Field { .. }) | None => None,
+fn lookahead(next_symbol: Option<&FormalitySpecSymbol>) -> Option<Literal> {
+    match next_symbol {
+        Some(FormalitySpecSymbol::Char { punct }) => Some(Literal::character(punct.as_char())),
+        Some(FormalitySpecSymbol::Delimeter { text }) => Some(Literal::character(*text)),
+        Some(FormalitySpecSymbol::Keyword { .. }) | Some(FormalitySpecSymbol::Field { .. }) | None => None,
     }
 }
 
diff --git a/crates/formality-macros/src/spec.rs b/crates/formality-macros/src/spec.rs
index 5f9a656b..23c1cf80 100644
--- a/crates/formality-macros/src/spec.rs
+++ b/crates/formality-macros/src/spec.rs
@@ -10,11 +10,11 @@ use proc_macro2::{Ident, Punct, TokenStream, TokenTree};
 /// * a character like `<` is parsed as is; a group like `[..]` parses a `[`, the contents, and then `]`
 #[derive(Debug)]
 pub struct FormalitySpec {
-    pub ops: Vec<FormalitySpecOp>,
+    pub symbols: Vec<FormalitySpecSymbol>,
 }
 
 #[derive(Debug)]
-pub enum FormalitySpecOp {
+pub enum FormalitySpecSymbol {
     /// `$foo` or `$foo*` -- indicates we should parse the type of the given field.
     Field { name: Ident, mode: FieldMode },
 
@@ -53,17 +53,17 @@ pub enum FieldMode {
 impl syn::parse::Parse for FormalitySpec {
     fn parse(input: syn::parse::ParseStream) -> syn::Result<Self> {
         let token_stream: TokenStream = input.parse()?;
-        let mut ops = vec![];
-        token_stream_to_ops(&mut ops, token_stream)?;
-        Ok(FormalitySpec { ops })
+        let mut symbols = vec![];
+        token_stream_to_symbols(&mut symbols, token_stream)?;
+        Ok(FormalitySpec { symbols })
     }
 }
 
-fn token_stream_to_ops(
-    ops: &mut Vec<FormalitySpecOp>,
+fn token_stream_to_symbols(
+    symbols: &mut Vec<FormalitySpecSymbol>,
     token_stream: TokenStream,
 ) -> syn::Result<()> {
-    use FormalitySpecOp::*;
+    use FormalitySpecSymbol::*;
 
     let mut tokens = token_stream.into_iter();
 
@@ -78,17 +78,17 @@ fn token_stream_to_ops(
                 };
 
                 if let Some(ch) = open_text {
-                    ops.push(Delimeter { text: ch });
+                    symbols.push(Delimeter { text: ch });
                 }
-                token_stream_to_ops(ops, v.stream())?;
+                token_stream_to_symbols(symbols, v.stream())?;
                 if let Some(ch) = close_text {
-                    ops.push(Delimeter { text: ch });
+                    symbols.push(Delimeter { text: ch });
                 }
             }
-            proc_macro2::TokenTree::Ident(ident) => ops.push(Keyword { ident }),
+            proc_macro2::TokenTree::Ident(ident) => symbols.push(Keyword { ident }),
             proc_macro2::TokenTree::Punct(punct) => match punct.as_char() {
-                '$' => ops.push(parse_variable_binding(punct, &mut tokens)?),
-                _ => ops.push(Char { punct }),
+                '$' => symbols.push(parse_variable_binding(punct, &mut tokens)?),
+                _ => symbols.push(Char { punct }),
             },
             proc_macro2::TokenTree::Literal(_) => {
                 let message = "unexpected literal in parse string";
@@ -109,7 +109,7 @@ fn token_stream_to_ops(
 fn parse_variable_binding(
     dollar_token: Punct,
     tokens: &mut impl Iterator<Item = TokenTree>,
-) -> syn::Result<FormalitySpecOp> {
+) -> syn::Result<FormalitySpecSymbol> {
     let error = || {
         let message = "expected field name or field mode (`,`, `*`)";
         Err(syn::Error::new(dollar_token.span(), message))
@@ -128,7 +128,7 @@ fn parse_variable_binding(
                 ',' => FieldMode::Comma,
                 '*' => FieldMode::Many,
                 '?' => FieldMode::Optional,
-                '$' => return Ok(FormalitySpecOp::Char { punct }),
+                '$' => return Ok(FormalitySpecSymbol::Char { punct }),
                 _ => return error(),
             };
 
@@ -148,5 +148,5 @@ fn parse_variable_binding(
         _ => return error(),
     };
 
-    Ok(FormalitySpecOp::Field { name, mode })
+    Ok(FormalitySpecSymbol::Field { name, mode })
 }

From 6e989ed1fd1de139e6d8d85f0f7ae4fced197055 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Thu, 2 Nov 2023 08:19:36 -0400
Subject: [PATCH 11/22] author more reference content for parsing

---
 book/src/SUMMARY.md              |  1 +
 book/src/formality_core/parse.md | 55 ++++++++++++++++++++++++++++++++
 2 files changed, 56 insertions(+)
 create mode 100644 book/src/formality_core/parse.md

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index 2f43c2a2..f7e9f6da 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -4,6 +4,7 @@
 - [`formality_core`: the Formality system](./formality_core.md)
     - [Defining your lang](./formality_core/lang.md)
     - [Defining terms with the `term` macro](./formality_core/terms.md)
+        - [Parsing reference](./formality_core/parse.md)
         - [Implementing `Fold` and `Visit` by hand](./formality_core/impl_fold_visit.md)
         - [Implementing `Parse` by hand](./formality_core/impl_parse.md)
     - [Variables](./formality_core/variables.md)
diff --git a/book/src/formality_core/parse.md b/book/src/formality_core/parse.md
new file mode 100644
index 00000000..c7928e13
--- /dev/null
+++ b/book/src/formality_core/parse.md
@@ -0,0 +1,55 @@
+# Parsing
+
+Formality's `#[term]` and `#[grammar]` attributes let you specify the grammar that will be used to parse your structs/enums.
+
+For structs, there is a single grammar, specified as part of the term:
+
+```rust
+#[term( /* grammar here */ )]
+struct MyStruct { }
+```
+
+For enums, the grammar is placed in `#[grammar]` attributes on each variant:
+
+```rust
+#[term]
+struct MyEnum {
+    #[grammar( /* grammar here */ )]
+    Foo(...),
+}
+```
+
+### Ambiguity,
+
+When parsing an enum there will be multiple possibilities. We will attempt to parse them all. If more than one succeeds, the parse is deemed ambiguous and an error is reported. If zero succeed, we will report back a parsing error, attempting to localize the problem as best we can.
+
+### Symbols
+
+A grammar consists of a series of *symbols*. Each symbol matches some text in the input string. Symbols come in two varieties:
+
+* Most things are *terminals* or *tokens*: this means they just match themselves:
+    * For example, the `*` in `#[grammar($v0 * $v1)]` is a terminal, and it means to parse a `*` from the input.
+    * Delimeters are accepted but must be matched, e.g., `( /* tokens */ )` or `[ /* tokens */ ]`.
+* Things beginning with `$` are *nonterminals* -- they parse the contents of a field. The grammar for a field is generally determined from its type.
+    * If fields have names, then `$field` should name the field.
+    * For position fields (e.g., the T and U in `Mul(Expr, Expr)`), use `$v0`, `$v1`, etc.
+    * Exception: `$$` is treated as the terminal `'$'`.
+* Nonterminals can also accept modes:
+    * `$field` -- just parse the field's type
+    * `$*field` -- the field must be a `Vec<T>` -- parse any number of `T` instances. Something like `[ $*field ]` would parse `[f1 f2 f3]`, assuming `f1`, `f2`, and `f3` are valid values for `field`.
+        * If the next token after `$*field` is a terminal, `$*` uses  it as lookahead. The grammar `[ $*field ]`, for example, would stop parsing once a `]` is observed. 
+        * If the `$*field` appears at the end of the grammar or the next symbol is a nonterminal, then the type of `field` must define a grammar that begins with some terminal or else your parsing will likely be ambiguous or infinite.
+    * `$,field` -- similar to the above, but uses a comma separated list (with optional trailing comma). So `[ $,field ]` will parse something like `[f1, f2, f3]`.
+        * Lookahead is required for `$,field` (this could be changed).
+    * `$?field` -- will parse `field` and use `Default::default()` value if not present.
+
+### Greediness
+
+Parsing is generally greedy. So `$*x` and `$,x`, for example, consume as many entries as they can, subject to lookahead. In a case like `$*f $*g`, the parser would parse as many `f` values as it could before parsing `g`. If some entry can be parsed as either `f` or `g`, the parser will not explore all possibilities. The caveat here is lookahead: given `$*f #`, for example, parsing will stop when `#` is observed, even if `f` could parse `#`.
+
+### Default grammar
+
+If no grammar is supplied, the default grammar is determined as follows:
+
+* If a `#[cast]` or `#[variable]` annotation is present, then the default grammar is just `$v0`.
+* Otherwise, the default grammar is the name of the type (for structs) or variant (for enums), followed by `()`, with the values for the fields in order. So `Mul(Expr, Expr)` would have a default grammar `mul($v0, $v1)`.

From 20ed035b96bf11f154f6816be85a3b042d6dcc16 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Fri, 3 Nov 2023 07:12:14 -0400
Subject: [PATCH 12/22] implement new parser approach

The new parser has a utility struct, Parser. It supports precedence
which lets us cleanup some of the code. The goal is to eventually
simplify the Rust types parsing code so we don't need so much scary
stuff.
---
 crates/formality-core/src/cast.rs             |  10 +
 crates/formality-core/src/language.rs         |  10 +-
 crates/formality-core/src/lib.rs              |  27 +-
 crates/formality-core/src/parse.rs            | 501 +++++---------
 crates/formality-core/src/parse/parser.rs     | 619 ++++++++++++++++++
 crates/formality-macros/src/parse.rs          | 159 ++---
 crates/formality-rust/src/trait_binder.rs     |  52 +-
 .../src/grammar/ty/parse_impls.rs             | 254 +++----
 crates/formality-types/src/lib.rs             |   9 +
 tests/associated_type_normalization.rs        |   1 +
 tests/ui/parser.stderr                        |   2 +-
 11 files changed, 1010 insertions(+), 634 deletions(-)
 create mode 100644 crates/formality-core/src/parse/parser.rs

diff --git a/crates/formality-core/src/cast.rs b/crates/formality-core/src/cast.rs
index 9be3c84f..fd9ce83c 100644
--- a/crates/formality-core/src/cast.rs
+++ b/crates/formality-core/src/cast.rs
@@ -216,6 +216,16 @@ where
     }
 }
 
+impl<T: Clone, U, E> UpcastFrom<Result<T, E>> for Result<U, E>
+where
+    T: Upcast<U>,
+    E: Clone,
+{
+    fn upcast_from(term: Result<T, E>) -> Self {
+        term.map(|t| t.upcast())
+    }
+}
+
 impl DowncastTo<()> for () {
     fn downcast_to(&self) -> Option<()> {
         Some(())
diff --git a/crates/formality-core/src/language.rs b/crates/formality-core/src/language.rs
index cd5fb375..02aeaaaf 100644
--- a/crates/formality-core/src/language.rs
+++ b/crates/formality-core/src/language.rs
@@ -22,11 +22,17 @@ pub trait Language: 'static + Copy + Ord + Hash + Debug + Default {
         + UpcastFrom<CoreExistentialVar<Self>>
         + UpcastFrom<CoreBoundVar<Self>>;
 
-    /// The character (typically `<`) used to open binders.
+    /// The token (typically `<`) used to open binders.
     const BINDING_OPEN: char;
 
-    /// The character (typically `>`) used to open binders.
+    /// The token (typically `>`) used to open binders.
     const BINDING_CLOSE: char;
+
+    /// Keywords to disallow as identifiers everywhere.
+    /// It is possible to do positional keywords too, if you want,
+    /// but it requires custom parsing impls for your types.
+    /// No fun.
+    const KEYWORDS: &'static [&'static str];
 }
 
 /// For consistency with types like `CoreVariable<L>`, we write `CoreKind<L>` instead of `Kind<L>`.
diff --git a/crates/formality-core/src/lib.rs b/crates/formality-core/src/lib.rs
index 37d3c294..53e54a13 100644
--- a/crates/formality-core/src/lib.rs
+++ b/crates/formality-core/src/lib.rs
@@ -90,6 +90,7 @@ macro_rules! declare_language {
             type Parameter = $param:ty;
             const BINDING_OPEN = $binding_open:expr;
             const BINDING_CLOSE = $binding_close:expr;
+            const KEYWORDS = [$($kw:expr),* $(,)?];
         }
     ) => {
         $(#[$the_lang_m:meta])*
@@ -105,6 +106,7 @@ macro_rules! declare_language {
                 type Parameter = $param;
                 const BINDING_OPEN: char = $binding_open;
                 const BINDING_CLOSE: char = $binding_close;
+                const KEYWORDS: &'static [&'static str] = &[$($kw),*];
             }
 
             $crate::trait_alias! {
@@ -161,21 +163,7 @@ macro_rules! declare_language {
                 T: Parse,
                 B: $crate::Upcast<(String, $param)>,
             {
-                let scope = $crate::parse::Scope::new(bindings.into_iter().map(|b| b.upcast()));
-                let (t, remainder) = match T::parse(&scope, text) {
-                    Ok(v) => v,
-                    Err(errors) => {
-                        let mut err = $crate::anyhow!("failed to parse {text}");
-                        for error in errors {
-                            err = err.context(error.text.to_owned()).context(error.message);
-                        }
-                        return Err(err);
-                    }
-                };
-                if !$crate::parse::skip_whitespace(remainder).is_empty() {
-                    $crate::bail!("extra tokens after parsing {text:?} to {t:?}: {remainder:?}");
-                }
-                Ok(t)
+                $crate::parse::core_term_with::<FormalityLang, T, B>(bindings, text)
             }
         }
     }
@@ -238,12 +226,13 @@ macro_rules! id {
 
             impl CoreParse<crate::FormalityLang> for $n {
                 fn parse<'t>(
-                    _scope: &parse::Scope<crate::FormalityLang>,
+                    scope: &parse::Scope<crate::FormalityLang>,
                     text: &'t str,
                 ) -> parse::ParseResult<'t, Self> {
-                    let (string, text) = parse::identifier(text)?;
-                    let n = $n::new(&string);
-                    Ok((n, text))
+                    $crate::parse::Parser::single_variant(scope, text, stringify!($n), |p| {
+                        let string = p.identifier()?;
+                        Ok($n::new(&string))
+                    })
                 }
             }
 
diff --git a/crates/formality-core/src/parse.rs b/crates/formality-core/src/parse.rs
index 4b31b430..3170e45c 100644
--- a/crates/formality-core/src/parse.rs
+++ b/crates/formality-core/src/parse.rs
@@ -1,85 +1,123 @@
-use std::{str::FromStr, sync::Arc};
+use std::sync::Arc;
 
 use crate::{
     binder::CoreBinder,
-    cast::To,
     collections::Set,
-    language::{CoreKind, CoreParameter, HasKind, Language},
+    language::{CoreKind, CoreParameter, Language},
     set,
     term::CoreTerm,
     variable::CoreBoundVar,
-    Downcast, DowncastFrom,
+    Fallible, Upcast, UpcastFrom, Upcasted,
 };
 use std::fmt::Debug;
 
 /// Trait for parsing a [`Term<L>`](`crate::term::Term`) as input.
-pub trait CoreParse<L: Language>: Sized + Debug {
+/// Typically this is auto-generated with the `#[term]` procedural macro,
+/// but you can implement it by hand if you want a very customized parse.
+pub trait CoreParse<L: Language>: Sized + Debug + Clone + Eq {
     /// Parse a single instance of this type, returning an error if no such
     /// instance is present.
+    ///
+    /// This is intended to be implemented by constructing
+    /// a [`Parser`][], typically with `Parser::single_variant_nonterminal`.
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self>;
+}
+
+mod parser;
+pub use parser::{skip_whitespace, ActiveVariant, Parser};
 
-    /// Parse many instances of self, expecting `close_char` to appear after the last instance
-    /// (`close_char` is not consumed).
-    fn parse_many<'t>(
-        scope: &Scope<L>,
-        mut text: &'t str,
-        close_char: char,
-    ) -> ParseResult<'t, Vec<Self>> {
-        let mut result = vec![];
-        while !skip_whitespace(text).starts_with(close_char) {
-            let (e, t) = Self::parse(scope, text)?;
-            result.push(e);
-            text = t;
+/// Parses `text` as a term with the given bindings in scope.
+///
+/// References to the given string will be replaced with the given parameter
+/// when parsing types, lifetimes, etc.
+#[track_caller]
+pub fn core_term_with<L, T, B>(bindings: impl IntoIterator<Item = B>, text: &str) -> Fallible<T>
+where
+    T: CoreParse<L>,
+    L: Language,
+    B: Upcast<(String, CoreParameter<L>)>,
+{
+    let scope = Scope::new(bindings.into_iter().map(|b| b.upcast()));
+    let parse = match T::parse(&scope, text) {
+        Ok(v) => v,
+        Err(errors) => {
+            let mut err = crate::anyhow!("failed to parse {text}");
+            for error in errors {
+                err = err.context(error.text.to_owned()).context(error.message);
+            }
+            return Err(err);
         }
-        Ok((result, text))
+    };
+    let (value, remainder) = parse.finish();
+
+    if !skip_whitespace(remainder).is_empty() {
+        crate::bail!("extra tokens after parsing {text:?} to {value:?}: {remainder:?}");
     }
 
-    /// Continue parsing instances of self while we can.
-    fn parse_while_possible<'t>(scope: &Scope<L>, mut text: &'t str) -> ParseResult<'t, Vec<Self>> {
-        let mut result = vec![];
-        while let (Some(e), text1) = Self::parse_opt(scope, text)? {
-            result.push(e);
-            text = text1;
+    Ok(value)
+}
+
+/// Record from a successful parse.
+#[derive(Debug, Clone)]
+pub struct SuccessfulParse<'t, T> {
+    /// The new point in the input, after we've consumed whatever text we have.
+    text: &'t str,
+
+    /// A list of reductions we had to perform. *Reductions* are the names
+    /// of enum variants that we have produced. For example, given an enum like `Foo { Bar(String, String) }`,
+    /// and an input `foo("hello", "world")`, the reductions that result would be
+    /// `["String", "String", "Foo::Bar"]`. This is used to resolve ambiguities
+    /// more successfully.
+    ///
+    /// Important: reductions are only recorded if they represent a significant
+    /// change. "is-a" relationships do not result in reductions. For example,
+    /// given `enum Expr { #[cast] Base(BaseExpr), ... }`, only the reductions
+    /// from `BaseExpr` would be recorded, there would be no `Expr::Base`
+    /// reduction.
+    reductions: Vec<&'static str>,
+
+    /// The value produced.
+    value: T,
+}
+
+impl<'t, T> SuccessfulParse<'t, T> {
+    #[track_caller]
+    pub fn new(text: &'t str, reductions: Vec<&'static str>, value: T) -> Self {
+        // assert!(!reductions.is_empty());
+        Self {
+            text,
+            reductions,
+            value,
         }
-        Ok((result, text))
     }
 
-    /// Comma separated list with optional trailing comma.
-    fn parse_comma<'t>(
-        scope: &Scope<L>,
-        mut text: &'t str,
-        close_char: char,
-    ) -> ParseResult<'t, Vec<Self>> {
-        let mut result = vec![];
-        while !skip_whitespace(text).starts_with(close_char) {
-            let (e, t) = Self::parse(scope, text)?;
-            result.push(e);
-            text = t;
-
-            if let Ok(((), t)) = expect_char(',', text) {
-                text = t;
-            } else {
-                break;
-            }
-        }
+    /// Extract the value parsed and the remaining text,
+    /// ignoring the reductions.
+    pub fn finish(self) -> (T, &'t str) {
+        (self.value, self.text)
+    }
 
-        Ok((result, text))
+    /// Maps the value using `op` -- this is meant for 'no-op' conversions like going from `T` to `Arc<T>`,
+    /// and hence the list of reductions does not change.
+    pub fn map<U>(self, op: impl FnOnce(T) -> U) -> SuccessfulParse<'t, U> {
+        SuccessfulParse {
+            text: self.text,
+            reductions: self.reductions,
+            value: op(self.value),
+        }
     }
+}
 
-    /// Try to parse the current point as `Self`. If failure occurs, check
-    /// whether we consumed any tokens -- if so, return the resulting errors we
-    /// encountered as a parse failure. Otherwise, substitute a default Self.
-    fn parse_opt<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Option<Self>> {
-        match Self::parse(scope, text) {
-            Ok((v, text)) => Ok((Some(v), text)),
-            Err(mut errs) => {
-                errs.retain(|e| e.consumed_any_since(text));
-                if errs.is_empty() {
-                    Ok((None, text))
-                } else {
-                    Err(errs)
-                }
-            }
+impl<'t, T, U> UpcastFrom<SuccessfulParse<'t, T>> for SuccessfulParse<'t, U>
+where
+    T: Upcast<U>,
+    T: Clone,
+{
+    fn upcast_from(term: SuccessfulParse<'t, T>) -> Self {
+        SuccessfulParse {
+            text: term.text,
+            reductions: term.reductions,
+            value: term.value.upcast(),
         }
     }
 }
@@ -106,6 +144,7 @@ impl<'t> ParseError<'t> {
     /// Creates a single parse error at the given point. Returns
     /// a set so that it can be wrapped as a [`ParseResult`].
     pub fn at(text: &'t str, message: String) -> Set<Self> {
+        let text = parser::skip_whitespace(text);
         set![ParseError { text, message }]
     }
 
@@ -129,7 +168,8 @@ impl<'t> ParseError<'t> {
     }
 }
 
-pub type ParseResult<'t, T> = Result<(T, &'t str), Set<ParseError<'t>>>;
+pub type ParseResult<'t, T> = Result<SuccessfulParse<'t, T>, Set<ParseError<'t>>>;
+pub type TokenResult<'t, T> = Result<(T, &'t str), Set<ParseError<'t>>>;
 
 /// Tracks the variables in scope at this point in parsing.
 #[derive(Clone, Debug)]
@@ -157,16 +197,16 @@ impl<L: Language> Scope<L> {
     /// Create a new scope that extends `self` with `bindings`.
     pub fn with_bindings(
         &self,
-        bindings: impl IntoIterator<Item = (String, CoreParameter<L>)>,
+        bindings: impl IntoIterator<Item = impl Upcast<(String, CoreParameter<L>)>>,
     ) -> Self {
         let mut s = self.clone();
-        s.bindings.extend(bindings);
+        s.bindings.extend(bindings.into_iter().upcasted());
         s
     }
 }
 
 /// Records a single binding, used when parsing [`Binder`].
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, PartialEq, Eq)]
 pub struct Binding<L: Language> {
     /// Name the user during during parsing
     pub name: String,
@@ -180,12 +220,13 @@ where
     L: Language,
     T: CoreParse<L>,
 {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let ((), text) = expect_char('[', text)?;
-        let (v, text) = T::parse_comma(scope, text, ']')?;
-        let ((), text) = expect_char(']', text)?;
-        Ok((v, text))
+        Parser::single_variant(scope, text, "Vec", |p| {
+            p.expect_char('[')?;
+            let v = p.comma_nonterminal()?;
+            p.expect_char(']')?;
+            Ok(v)
+        })
     }
 }
 
@@ -194,13 +235,14 @@ where
     L: Language,
     T: CoreParse<L> + Ord,
 {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let ((), text) = expect_char('{', text)?;
-        let (v, text) = T::parse_comma(scope, text, '}')?;
-        let ((), text) = expect_char('}', text)?;
-        let s = v.into_iter().collect();
-        Ok((s, text))
+        Parser::single_variant(scope, text, "Set", |p| {
+            p.expect_char('{')?;
+            let v = p.comma_nonterminal()?;
+            p.expect_char('}')?;
+            let s = v.into_iter().collect();
+            Ok(s)
+        })
     }
 }
 
@@ -209,20 +251,20 @@ where
     L: Language,
     T: CoreParse<L>,
 {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        T::parse_opt(scope, text)
+        Parser::single_variant(scope, text, "Option", |p| p.opt_nonterminal())
     }
 }
 
 /// Binding grammar is `$kind $name`, e.g., `ty Foo`.
 impl<L: Language> CoreParse<L> for Binding<L> {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let (kind, text) = <CoreKind<L>>::parse(scope, text)?;
-        let (name, text) = identifier(text)?;
-        let bound_var = CoreBoundVar::fresh(kind);
-        Ok((Binding { name, bound_var }, text))
+        Parser::single_variant(scope, text, "Binding", |p| {
+            let kind: CoreKind<L> = p.nonterminal()?;
+            let name = p.identifier()?;
+            let bound_var = CoreBoundVar::fresh(kind);
+            Ok(Binding { name, bound_var })
+        })
     }
 }
 
@@ -233,19 +275,20 @@ where
     L: Language,
     T: CoreTerm<L>,
 {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let ((), text) = expect_char(L::BINDING_OPEN, text)?;
-        let (bindings, text) = Binding::parse_comma(scope, text, '>')?;
-        let ((), text) = expect_char(L::BINDING_CLOSE, text)?;
+        Parser::single_variant(scope, text, "Binder", |p| {
+            p.expect_char(L::BINDING_OPEN)?;
+            let bindings: Vec<Binding<L>> = p.comma_nonterminal()?;
+            p.expect_char(L::BINDING_CLOSE)?;
 
-        // parse the contents with those names in scope
-        let scope1 =
-            scope.with_bindings(bindings.iter().map(|b| (b.name.clone(), b.bound_var.to())));
-        let (data, text) = T::parse(&scope1, text)?;
+            let data: T = p.with_scope(
+                scope.with_bindings(bindings.iter().map(|b| (&b.name, b.bound_var))),
+                |p| p.nonterminal(),
+            )?;
 
-        let kvis: Vec<CoreBoundVar<L>> = bindings.iter().map(|b| b.bound_var).collect();
-        Ok((CoreBinder::new(kvis, data), text))
+            let kvis: Vec<CoreBoundVar<L>> = bindings.iter().map(|b| b.bound_var).collect();
+            Ok(CoreBinder::new(kvis, data))
+        })
     }
 }
 
@@ -255,8 +298,7 @@ where
     T: CoreParse<L>,
 {
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let (data, text) = T::parse(scope, text)?;
-        Ok((Arc::new(data), text))
+        T::parse(scope, text).map(|success| success.map(Arc::new))
     }
 }
 
@@ -264,9 +306,8 @@ impl<L> CoreParse<L> for usize
 where
     L: Language,
 {
-    #[tracing::instrument(level = "trace", ret)]
-    fn parse<'t>(_scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        number(text)
+    fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
+        Parser::single_variant(scope, text, "usize", |p| p.number())
     }
 }
 
@@ -274,9 +315,8 @@ impl<L> CoreParse<L> for u32
 where
     L: Language,
 {
-    #[tracing::instrument(level = "trace", ret)]
-    fn parse<'t>(_scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        number(text)
+    fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
+        Parser::single_variant(scope, text, "u32", |p| p.number())
     }
 }
 
@@ -284,254 +324,47 @@ impl<L> CoreParse<L> for u64
 where
     L: Language,
 {
-    #[tracing::instrument(level = "trace", ret)]
-    fn parse<'t>(_scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        number(text)
-    }
-}
-
-/// Extract the next character from input, returning an error if we've reached the input.
-///
-/// Warning: does not skip whitespace.
-fn char(text: &str) -> ParseResult<'_, char> {
-    let ch = match text.chars().next() {
-        Some(c) => c,
-        None => return Err(ParseError::at(text, "unexpected end of input".to_string())),
-    };
-    Ok((ch, &text[char::len_utf8(ch)..]))
-}
-
-/// Extract a number from the input, erroring if the input does not start with a number.
-#[tracing::instrument(level = "trace", ret)]
-pub fn number<T>(text0: &str) -> ParseResult<'_, T>
-where
-    T: FromStr + Debug,
-{
-    let (id, text1) = accumulate(text0, char::is_numeric, char::is_numeric, "number")?;
-    match T::from_str(&id) {
-        Ok(t) => Ok((t, text1)),
-        Err(_) => Err(ParseError::at(text0, format!("invalid number"))),
-    }
-}
-
-/// Consume next character and require that it be `ch`.
-#[tracing::instrument(level = "trace", ret)]
-pub fn expect_char(ch: char, text0: &str) -> ParseResult<'_, ()> {
-    let text1 = skip_whitespace(text0);
-    let (ch1, text1) = char(text1)?;
-    if ch == ch1 {
-        Ok(((), text1))
-    } else {
-        Err(ParseError::at(text0, format!("expected `{}`", ch)))
-    }
-}
-
-/// Consume a comma if one is present.
-#[tracing::instrument(level = "trace", ret)]
-pub fn skip_trailing_comma(text: &str) -> &str {
-    text.strip_prefix(',').unwrap_or(text)
-}
-
-/// Extracts a maximal identifier from the start of text,
-/// following the usual rules.
-#[tracing::instrument(level = "trace", ret)]
-pub fn identifier(text: &str) -> ParseResult<'_, String> {
-    accumulate(
-        text,
-        |ch| matches!(ch, 'a'..='z' | 'A'..='Z' | '_'),
-        |ch| matches!(ch, 'a'..='z' | 'A'..='Z' | '_' | '0'..='9'),
-        "identifier",
-    )
-}
-
-/// Consume next identifier, requiring that it be equal to `expected`.
-#[tracing::instrument(level = "trace", ret)]
-pub fn expect_keyword<'t>(expected: &str, text0: &'t str) -> ParseResult<'t, ()> {
-    match identifier(text0) {
-        Ok((ident, text1)) if &*ident == expected => Ok(((), text1)),
-        _ => Err(ParseError::at(text0, format!("expected `{}`", expected))),
-    }
-}
-
-/// Reject next identifier if it is the given keyword. Consumes nothing.
-#[tracing::instrument(level = "trace", ret)]
-pub fn reject_keyword<'t>(expected: &str, text0: &'t str) -> ParseResult<'t, ()> {
-    match expect_keyword(expected, text0) {
-        Ok(_) => Err(ParseError::at(
-            text0,
-            format!("found keyword `{}`", expected),
-        )),
-        Err(_) => Ok(((), text0)),
-    }
-}
-
-/// Convenience function for use when generating code: calls the closure it is given
-/// as argument. Used to introduce new scope for name bindings.
-pub fn try_parse<'a, R>(f: impl Fn() -> ParseResult<'a, R>) -> ParseResult<'a, R> {
-    f()
-}
-
-/// Used at choice points in the grammar. Iterates over all possible parses, looking
-/// for a single successful parse. If there are multiple successful parses, that
-/// indicates an ambiguous grammar, so we panic. If there are no successful parses,
-/// tries to come up with the best error it can: it prefers errors that arise from "partially successful"
-/// parses (e.g., parses that consume some input before failing), but if there are none of those,
-/// it will give an error at `text` saying that we expected to find a `expected`.
-pub fn require_unambiguous<'t, R>(
-    text: &'t str,
-    f: impl IntoIterator<Item = ParseResult<'t, R>>,
-    expected: &'static str,
-) -> ParseResult<'t, R>
-where
-    R: std::fmt::Debug,
-{
-    let mut errors = set![];
-    let mut results = vec![];
-    for result in f {
-        match result {
-            Ok(v) => results.push(v),
-            Err(es) => {
-                for e in es {
-                    // only include an error if the error resulted after at least
-                    // one non-whitespace character was consumed
-                    if e.consumed_any_since(text) {
-                        errors.insert(e);
-                    }
-                }
-            }
-        }
-    }
-
-    if results.len() > 1 {
-        // More than one *positive* result indicates an ambiguous grammar, which is a programmer bug,
-        // not a fault of the input, so we panic (rather than returning Err)
-        panic!("parsing ambiguity: {results:?}");
-    } else if results.len() == 1 {
-        Ok(results.pop().unwrap())
-    } else if errors.is_empty() {
-        Err(ParseError::at(text, format!("{} expected", expected)))
-    } else {
-        Err(errors)
-    }
-}
-
-/// Extracts a maximal identifier from the start of text,
-/// following the usual rules.
-fn accumulate<'t>(
-    text0: &'t str,
-    start_test: impl Fn(char) -> bool,
-    continue_test: impl Fn(char) -> bool,
-    description: &'static str,
-) -> ParseResult<'t, String> {
-    let text1 = skip_whitespace(text0);
-    let mut buffer = String::new();
-
-    let (ch, text1) = char(text1)?;
-    if !start_test(ch) {
-        return Err(ParseError::at(text0, format!("{} expected", description)));
-    }
-    buffer.push(ch);
-
-    let mut text1 = text1;
-    while let Ok((ch, t)) = char(text1) {
-        if !continue_test(ch) {
-            break;
-        }
-
-        buffer.push(ch);
-        text1 = t;
-    }
-
-    Ok((buffer, text1))
-}
-
-impl<L: Language, A: CoreParse<L>, B: CoreParse<L>> CoreParse<L> for (A, B) {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let ((), text) = expect_char('(', text)?;
-        let (a, text) = A::parse(scope, text)?;
-        let ((), text) = expect_char(',', text)?;
-        let (b, text) = B::parse(scope, text)?;
-        let text = skip_trailing_comma(text);
-        let ((), text) = expect_char(')', text)?;
-        Ok(((a, b), text))
+        Parser::single_variant(scope, text, "u64", |p| p.number())
     }
 }
 
 impl<L: Language> CoreParse<L> for () {
-    #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let ((), text) = expect_char('(', text)?;
-        let ((), text) = expect_char(')', text)?;
-        Ok(((), text))
+        Parser::single_variant(scope, text, "`()`", |p| {
+            p.expect_char('(')?;
+            p.expect_char(')')?;
+            Ok(())
+        })
     }
 }
 
-impl<L: Language, A: CoreParse<L>, B: CoreParse<L>, C: CoreParse<L>> CoreParse<L> for (A, B, C) {
-    #[tracing::instrument(level = "trace", ret)]
+impl<L: Language, A: CoreParse<L>, B: CoreParse<L>> CoreParse<L> for (A, B) {
     fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
-        let ((), text) = expect_char('(', text)?;
-        let (a, text) = A::parse(scope, text)?;
-        let ((), text) = expect_char(',', text)?;
-        let (b, text) = B::parse(scope, text)?;
-        let ((), text) = expect_char(',', text)?;
-        let (c, text) = C::parse(scope, text)?;
-        let text = skip_trailing_comma(text);
-        let ((), text) = expect_char(')', text)?;
-        Ok(((a, b, c), text))
-    }
-}
-
-/// Skips leading whitespace and comments.
-pub fn skip_whitespace(mut text: &str) -> &str {
-    loop {
-        let len = text.len();
-
-        text = text.trim_start();
-
-        if text.starts_with("//") {
-            match text.find('\n') {
-                Some(index) => {
-                    text = &text[index + 1..];
-                }
-                None => {
-                    text = "";
-                }
-            }
-        }
-
-        if text.len() == len {
-            return text;
-        }
+        Parser::single_variant(scope, text, "tuple", |p| {
+            p.expect_char('(')?;
+            let a: A = p.nonterminal()?;
+            p.expect_char(',')?;
+            let b: B = p.nonterminal()?;
+            p.skip_trailing_comma();
+            p.expect_char(')')?;
+            Ok((a, b))
+        })
     }
 }
 
-/// Parses a variable into a parameter. Variables don't implement Parse themselves
-/// because you can't parse a variable into a *variable*, instead, you parse it into
-/// a Parameter indicating its kind.
-#[tracing::instrument(level = "trace", ret)]
-pub fn parse_variable<'t, L, R>(
-    scope: &Scope<L>,
-    text0: &'t str,
-    type_name: &str,
-) -> ParseResult<'t, R>
-where
-    L: Language,
-    R: Debug + DowncastFrom<CoreParameter<L>>,
-{
-    let (id, text1) = identifier(text0)?;
-    match scope.lookup(&id) {
-        Some(parameter) => match parameter.downcast() {
-            Some(v) => Ok((v, text1)),
-            None => Err(ParseError::at(
-                text0,
-                format!(
-                    "wrong kind, expected a {}, found a {:?}",
-                    type_name,
-                    parameter.kind()
-                ),
-            )),
-        },
-        None => Err(ParseError::at(text0, format!("unrecognized variable"))),
+impl<L: Language, A: CoreParse<L>, B: CoreParse<L>, C: CoreParse<L>> CoreParse<L> for (A, B, C) {
+    fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
+        Parser::single_variant(scope, text, "tuple", |p| {
+            p.expect_char('(')?;
+            let a: A = p.nonterminal()?;
+            p.expect_char(',')?;
+            let b: B = p.nonterminal()?;
+            p.expect_char(',')?;
+            let c: C = p.nonterminal()?;
+            p.skip_trailing_comma();
+            p.expect_char(')')?;
+            Ok((a, b, c))
+        })
     }
 }
diff --git a/crates/formality-core/src/parse/parser.rs b/crates/formality-core/src/parse/parser.rs
new file mode 100644
index 00000000..1224455e
--- /dev/null
+++ b/crates/formality-core/src/parse/parser.rs
@@ -0,0 +1,619 @@
+use std::fmt::Debug;
+use std::str::FromStr;
+
+use crate::{
+    language::{CoreParameter, HasKind, Language},
+    set, Downcast, DowncastFrom, Set, Upcast,
+};
+
+use super::{CoreParse, ParseError, ParseResult, Scope, SuccessfulParse, TokenResult};
+
+/// Create this struct when implementing the [`CoreParse`][] trait.
+/// Each `Parser` corresponds to some symbol in the grammar.
+/// You create a parser and then you invoke the `parse_variant`
+/// (or `parse_variant_cast`) method for each of the distinct possible parsings
+/// for that symbol. Finally you invoke `finish` to complete the parse.
+/// So e.g. if you grammar contains `Foo = Bar | Baz`, then you would
+///
+/// * create a `Parser` in the [`CoreParse`][] impl for `Foo`
+/// * invoke `parse_variant` twice, once for `Bar` and once for `Baz`
+/// * invoke `finish`
+pub struct Parser<'s, 't, T, L>
+where
+    L: Language,
+{
+    scope: &'s Scope<L>,
+    start_text: &'t str,
+    #[allow(dead_code)]
+    tracing_span: tracing::span::EnteredSpan,
+    nonterminal_name: &'static str,
+    successes: Vec<(SuccessfulParse<'t, T>, Precedence)>,
+    failures: Set<ParseError<'t>>,
+}
+
+#[derive(Debug, PartialEq, Eq, PartialOrd, Ord)]
+struct Precedence(usize);
+
+/// The "active variant" struct is the main struct
+/// you will use if you are writing custom parsing logic.
+/// It contains various methods for consuming tokens
+/// (e.g., `identifier`, `number`, `variable`).
+///
+/// The most common method is `nonterminal`,
+/// which lets you parse an instance of some other
+/// type that implements [`CoreParse`][].
+///
+/// Another common set of methods are things like
+/// `comma_nonterminal`, which parses a comma-separated
+/// list of nonterminals.
+///
+/// Note that **all** the methods of active variant skip past whitespace (and comments) implicitly
+#[derive(Clone, Debug)]
+pub struct ActiveVariant<'s, 't, L>
+where
+    L: Language,
+{
+    scope: &'s Scope<L>,
+    text: &'t str,
+    reductions: Vec<&'static str>,
+}
+
+impl<'s, 't, T, L> Parser<'s, 't, T, L>
+where
+    L: Language,
+    T: Debug + Eq,
+{
+    /// Shorthand to create a parser for a nonterminal with a single variant,
+    /// parsed by the function `op`.
+    ///
+    /// The nonterminal-name will be used as the reduction name and added after `op` completes.
+    pub fn single_variant(
+        scope: &'s Scope<L>,
+        text: &'t str,
+        nonterminal_name: &'static str,
+        op: impl FnOnce(&mut ActiveVariant<'s, 't, L>) -> Result<T, Set<ParseError<'t>>>,
+    ) -> ParseResult<'t, T> {
+        let mut result = Parser::new(scope, text, nonterminal_name);
+        result.parse_variant(nonterminal_name, 0, op);
+        result.finish()
+    }
+
+    /// Creates a new parser. You should then invoke `parse_variant` 0 or more times for
+    /// each of the possibilities and finally invoke `finish`.
+    ///
+    /// The method [`single_variant`] is more convenient if you have exactly one variant.
+    pub fn new(scope: &'s Scope<L>, text: &'t str, nonterminal_name: &'static str) -> Self {
+        let tracing_span = tracing::span!(
+            tracing::Level::TRACE,
+            "nonterminal",
+            name = nonterminal_name,
+            ?scope,
+            ?text
+        )
+        .entered();
+
+        Self {
+            scope,
+            start_text: text,
+            nonterminal_name,
+            tracing_span,
+            successes: vec![],
+            failures: set![],
+        }
+    }
+
+    /// Shorthand for `parse_variant` where the parsing operation is to
+    /// parse the type `V` and then upcast it to the desired result type.
+    pub fn parse_variant_cast<V>(&mut self, variant_precedence: usize)
+    where
+        V: CoreParse<L> + Upcast<T>,
+    {
+        let variant_name = std::any::type_name::<V>();
+        Self::parse_variant(self, variant_name, variant_precedence, |p| {
+            let v: V = p.nonterminal()?;
+            Ok(v.upcast())
+        })
+    }
+
+    /// Parses a single variant for this nonterminal.
+    /// The name of the variant is significant and will be tracked as part of the list of reductions.
+    /// The precedence is part of how we resolve conflicts: if there are two successful parses with distinct precedence, higher precedence wins.
+    /// The `op` is a closure that defines how the variant itself is parsed.
+    /// The closure `op` will be invoked with an [`ActiveVariant`][] struct that has methods for consuming identifiers, numbers, keywords, etc.
+    pub fn parse_variant(
+        &mut self,
+        variant_name: &'static str,
+        variant_precedence: usize,
+        op: impl FnOnce(&mut ActiveVariant<'s, 't, L>) -> Result<T, Set<ParseError<'t>>>,
+    ) {
+        let span = tracing::span!(
+            tracing::Level::TRACE,
+            "variant",
+            name = variant_name,
+            variant_precedence = variant_precedence
+        );
+        let guard = span.enter();
+
+        let mut active_variant = ActiveVariant {
+            scope: self.scope,
+            text: self.start_text,
+            reductions: vec![],
+        };
+        let result = op(&mut active_variant);
+
+        // Drop the guard here so that the "success" or "error" results appear outside the variant span.
+        // This makes it easier to follow along with parsing when you collapse sections.
+        drop(guard);
+
+        match result {
+            Ok(value) => {
+                active_variant.reductions.push(variant_name);
+                self.successes.push((
+                    SuccessfulParse {
+                        text: active_variant.text,
+                        reductions: active_variant.reductions,
+                        value,
+                    },
+                    Precedence(variant_precedence),
+                ));
+                tracing::trace!("success: {:?}", self.successes.last().unwrap());
+            }
+
+            Err(errs) => {
+                // If this variant encountered failures, then record them -- but careful!
+                // We only record failures where we actually consumed any tokens.
+                // This is part of our error reporting and recovery mechanism.
+                // Note that we expect (loosely) an LL(1) grammar.
+                self.failures.extend(
+                    errs.into_iter()
+                        .filter(|e| e.consumed_any_since(self.start_text))
+                        .inspect(|e| tracing::trace!("error: {e:?}")),
+                );
+            }
+        }
+    }
+
+    pub fn finish(self) -> ParseResult<'t, T> {
+        // If we did not parse anything successfully, then return an error.
+        // There are two possibilities: some of our variants may have made
+        // progress but ultimately failed. If so, self.failures will be non-empty,
+        // and we can return that. Otherwise, none of our variants made any
+        // progress at all, so we create a failure at the starting point
+        // just saying "we failed to find a X here". If this nonterminal is at
+        // the start of some larger nonterminal, that larger nonterminal will
+        // observe that we did not consume any tokens and will ignore our messawge
+        // and put its own (e.g., "failed to find a Y here").
+        if self.successes.is_empty() {
+            return if self.failures.is_empty() {
+                tracing::trace!("parsing failed: no variants were able to consume a single token");
+                Err(ParseError::at(
+                    self.start_text,
+                    format!("{} expected", self.nonterminal_name),
+                ))
+            } else {
+                tracing::trace!(
+                    "parsing failed with {} errors `{:?}`",
+                    self.failures.len(),
+                    self.failures
+                );
+                Err(self.failures)
+            };
+        }
+
+        if self.successes.len() > 1 {
+            tracing::trace!("successful parses: `{:?}`", self.successes);
+        }
+
+        // Otherwise, check if we had an unambiguous parse.
+        // This results if there exists some success S that is 'better' than every other success.
+        // We say S1 better than S2 if:
+        // * S1 has higher precedence OR
+        // * S1 parsed more tokens and in the same way (i.e., S2.reductions is a prefix of S1.reductions)
+        for (s_i, i) in self.successes.iter().zip(0..) {
+            if self
+                .successes
+                .iter()
+                .zip(0..)
+                .all(|(s_j, j)| i == j || Self::is_preferable(s_i, s_j))
+            {
+                let (s_i, _) = self.successes.into_iter().skip(i).next().unwrap();
+                tracing::trace!("best parse = `{:?}`", s_i);
+                return Ok(s_i);
+            }
+        }
+
+        panic!(
+            "ambiguous parse of `{text:?}`, possibilities are {possibilities:#?}",
+            text = self.start_text,
+            possibilities = self.successes,
+        );
+    }
+
+    fn is_preferable(
+        s_i: &(SuccessfulParse<T>, Precedence),
+        s_j: &(SuccessfulParse<T>, Precedence),
+    ) -> bool {
+        let (parse_i, prec_i) = s_i;
+        let (parse_j, prec_j) = s_j;
+
+        fn has_prefix<T: Eq>(l1: &[T], l2: &[T]) -> bool {
+            l1.len() > l2.len() && (0..l2.len()).all(|i| l1[i] == l2[i])
+        }
+
+        prec_i > prec_j || has_prefix(&parse_i.reductions, &parse_j.reductions)
+    }
+}
+
+impl<'s, 't, L> ActiveVariant<'s, 't, L>
+where
+    L: Language,
+{
+    /// The current text remaining to be consumed.
+    pub fn text(&self) -> &'t str {
+        self.text
+    }
+
+    /// Skips whitespace in the input, producing no reduction.
+    pub fn skip_whitespace(&mut self) {
+        self.text = skip_whitespace(self.text);
+    }
+
+    /// Skips a comma in the input, producing no reduction.
+    pub fn skip_trailing_comma(&mut self) {
+        self.text = skip_trailing_comma(self.text);
+    }
+
+    /// Expect *exactly* the given text (after skipping whitespace)
+    /// in the input string. Reports an error if anything else is observed.
+    /// In error case, consumes only whitespace.
+    pub fn expect_char(&mut self, char: char) -> Result<(), Set<ParseError<'t>>> {
+        self.token(|text| {
+            if text.starts_with(char) {
+                Ok(((), &text[char.len_utf8()..]))
+            } else {
+                Err(ParseError::at(text, format!("expected `{}`", char)))
+            }
+        })
+    }
+
+    /// Extracts a series of characters from the text
+    /// (after skipping whitespace).
+    /// The first character must match `start_test`
+    /// and all subsequent characters must match `continue_test`.
+    pub fn string(
+        &mut self,
+        start_test: impl Fn(char) -> bool,
+        continue_test: impl Fn(char) -> bool,
+        description: &'static str,
+    ) -> Result<String, Set<ParseError<'t>>> {
+        self.token(|text0| {
+            let mut buffer = String::new();
+
+            let (ch, text) = next_char(text0)?;
+            if !start_test(ch) {
+                return Err(ParseError::at(text0, format!("{} expected", description)));
+            }
+            buffer.push(ch);
+
+            let mut text = text;
+            while let Ok((ch, t)) = next_char(text) {
+                if !continue_test(ch) {
+                    break;
+                }
+
+                buffer.push(ch);
+                text = t;
+            }
+
+            Ok((buffer, text))
+        })
+    }
+
+    /// Consume next identifier-like string, requiring that it be equal to `expected`.
+    #[tracing::instrument(level = "trace", ret)]
+    pub fn expect_keyword(&mut self, expected: &str) -> Result<(), Set<ParseError<'t>>> {
+        let text0 = self.text;
+        match self.identifier_like_string() {
+            Ok(ident) if &*ident == expected => Ok(()),
+            _ => Err(ParseError::at(
+                skip_whitespace(text0),
+                format!("expected `{}`", expected),
+            )),
+        }
+    }
+
+    /// Reject next identifier-like string if it is one of the given list of keywords.
+    /// Does not consume any input.
+    /// You can this to implement positional keywords -- just before parsing an identifier or variable,
+    /// you can invoke `reject_custom_keywords` to reject anything that you don't want to permit in this position.
+    #[tracing::instrument(level = "trace", ret)]
+    pub fn reject_custom_keywords(&self, keywords: &[&str]) -> Result<(), Set<ParseError<'t>>> {
+        let mut this = ActiveVariant {
+            text: self.text,
+            reductions: vec![],
+            scope: self.scope,
+        };
+
+        match this.identifier_like_string() {
+            Ok(ident) => {
+                if keywords.iter().any(|&kw| kw == ident) {
+                    return Err(ParseError::at(
+                        self.text,
+                        format!("expected identified, found keyword `{ident:?}`"),
+                    ));
+                }
+
+                Ok(())
+            }
+
+            Err(_) => Ok(()),
+        }
+    }
+
+    /// Extracts a string that meets the regex for an identifier
+    /// (but it could also be a keyword).
+    #[tracing::instrument(level = "trace", ret)]
+    pub fn identifier_like_string(&mut self) -> Result<String, Set<ParseError<'t>>> {
+        self.string(
+            |ch| matches!(ch, 'a'..='z' | 'A'..='Z' | '_'),
+            |ch| matches!(ch, 'a'..='z' | 'A'..='Z' | '_' | '0'..='9'),
+            "identifier",
+        )
+    }
+
+    /// Extracts a maximal identifier from the start of text,
+    /// following the usual rules. **Disallows language keywords.**
+    /// If you want to disallow additional keywords,
+    /// see the `reject_custom_keywords` method.
+    #[tracing::instrument(level = "trace", ret)]
+    pub fn identifier(&mut self) -> Result<String, Set<ParseError<'t>>> {
+        self.reject_custom_keywords(L::KEYWORDS)?;
+        self.identifier_like_string()
+    }
+
+    /// Change the set of bindings in scope.
+    /// Invokes `op` with a new active variant.
+    pub fn with_scope<R>(
+        &mut self,
+        scope: Scope<L>,
+        op: impl FnOnce(&mut ActiveVariant<'_, 't, L>) -> R,
+    ) -> R {
+        let mut av = ActiveVariant {
+            scope: &scope,
+            text: self.text,
+            reductions: vec![],
+        };
+        let result = op(&mut av);
+        self.text = av.text;
+        self.reductions.extend(av.reductions);
+        result
+    }
+
+    /// Parses the next identifier as a variable in scope
+    /// with the kind appropriate for the return type `R`.
+    ///
+    /// **NB:** This departs from the limits of context-free
+    /// grammars -- the scope is a piece of context that affects how
+    /// our parsing proceeds!
+    ///
+    /// Variables don't implement Parse themselves
+    /// because you can't parse a variable into a *variable*,
+    /// instead, you parse it into a `Parameter`.
+    /// The parsing code then downcasts that parameter into the
+    /// type it wants (e.g., in Rust, a `Ty`).
+    /// This downcast will fail if the `Parameter` is not of the appropriate
+    /// kind (which will result in a parse error).
+    ///
+    /// This avoids "miskinding", i.e., parsing a `Ty` that contains
+    /// a lifetime variable.
+    ///
+    /// It also allows parsing where you use variables to stand for
+    /// more complex parameters, which is kind of combining parsing
+    /// and substitution and can be convenient in tests.
+    #[tracing::instrument(level = "trace", ret)]
+    pub fn variable<R>(&mut self) -> Result<R, Set<ParseError<'t>>>
+    where
+        R: Debug + DowncastFrom<CoreParameter<L>>,
+    {
+        self.skip_whitespace();
+        let type_name = std::any::type_name::<R>();
+        let text0 = self.text;
+        let id = self.identifier()?;
+        match self.scope.lookup(&id) {
+            Some(parameter) => match parameter.downcast() {
+                Some(v) => Ok(v),
+                None => Err(ParseError::at(
+                    text0,
+                    format!(
+                        "wrong kind, expected a {}, found a {:?}",
+                        type_name,
+                        parameter.kind()
+                    ),
+                )),
+            },
+            None => Err(ParseError::at(text0, format!("unrecognized variable"))),
+        }
+    }
+
+    /// Extract a number from the input, erroring if the input does not start with a number.
+    #[tracing::instrument(level = "trace", ret)]
+    pub fn number<T>(&mut self) -> Result<T, Set<ParseError<'t>>>
+    where
+        T: FromStr + std::fmt::Debug,
+    {
+        let description = std::any::type_name::<T>();
+        let text0 = self.text;
+        let s = self.string(char::is_numeric, char::is_numeric, description)?;
+        match T::from_str(&s) {
+            Ok(t) => Ok(t),
+            Err(_) => Err(ParseError::at(
+                skip_whitespace(text0),
+                format!("invalid number"),
+            )),
+        }
+    }
+
+    /// Consumes a single token from the input after skipping whitespace.
+    /// Does not record any reduction.
+    /// We don't generally record reductions for methods on parser,
+    /// the assumption is that they are implied by the nonterminal name / variant.
+    ///
+    /// The token is defined by `op`, which is a function that takes
+    /// the text and returns a result + new text.
+    ///
+    /// Tokens do not have internal
+    /// reductions, so `op` does not need to return reductions.
+    fn token<T>(
+        &mut self,
+        op: impl FnOnce(&'t str) -> TokenResult<'t, T>,
+    ) -> Result<T, Set<ParseError<'t>>> {
+        self.skip_whitespace();
+        let value;
+        (value, self.text) = op(self.text)?;
+        Ok(value)
+    }
+
+    /// Parse an instance of the given type `T` (after skipping whitespace).
+    #[track_caller]
+    pub fn nonterminal<T>(&mut self) -> Result<T, Set<ParseError<'t>>>
+    where
+        T: CoreParse<L>,
+        L: Language,
+    {
+        self.nonterminal_with(T::parse)
+    }
+
+    /// Try to parse the current point as `T` and return `None` if there is nothing there.
+    ///
+    /// **NB:**  If the parse partially succeeds, i.e., we are able to consume some tokens
+    /// but cannot completely parse, then this is an error, not a `None` result.
+    /// So for example if the grammar for `T` is `()` and the input is `"foo"`,
+    /// then we will return `None`. But if the input were `"(foo)"`, we would return an error,
+    /// because we consumed the open paren `(` from `T` but then encountered an error
+    /// looking for the closing paren `)`.
+    #[track_caller]
+    #[tracing::instrument(level = "Trace", ret)]
+    pub fn opt_nonterminal<T>(&mut self) -> Result<Option<T>, Set<ParseError<'t>>>
+    where
+        T: CoreParse<L>,
+    {
+        let text0 = self.text;
+        match self.nonterminal() {
+            Ok(v) => Ok(Some(v)),
+            Err(mut errs) => {
+                errs.retain(|e| e.consumed_any_since(text0));
+                if errs.is_empty() {
+                    // If no errors consumed anything, then self.text
+                    // must not have advanced.
+                    assert_eq!(skip_whitespace(text0), self.text);
+                    Ok(None)
+                } else {
+                    Err(errs)
+                }
+            }
+        }
+    }
+
+    /// Continue parsing instances of `T` while we can.
+    /// This is a greedy parse.
+    pub fn many_nonterminal<T>(&mut self) -> Result<Vec<T>, Set<ParseError<'t>>>
+    where
+        T: CoreParse<L>,
+    {
+        let mut result = vec![];
+        while let Some(e) = self.opt_nonterminal()? {
+            result.push(e);
+        }
+        Ok(result)
+    }
+
+    /// Parse multiple instances of `T` separated by commas.
+    #[track_caller]
+    pub fn comma_nonterminal<T>(&mut self) -> Result<Vec<T>, Set<ParseError<'t>>>
+    where
+        T: CoreParse<L>,
+    {
+        let mut result = vec![];
+        while let Some(e) = self.opt_nonterminal()? {
+            result.push(e);
+
+            if self.expect_char(',').is_err() {
+                break;
+            }
+        }
+        Ok(result)
+    }
+
+    /// Consumes a nonterminal from the input after skipping whitespace.
+    /// The nonterminal is defined by `op`, which is some parse function
+    /// that goes from text to a `ParseResult`. The `ParseResult` is assumed
+    /// to contain all the reductions (including the final reduction for
+    /// the nonterminal itself).
+    /// This is rarely used, prefer `nonterminal` when you can.
+    #[track_caller]
+    pub fn nonterminal_with<T>(
+        &mut self,
+        op: impl FnOnce(&'s Scope<L>, &'t str) -> ParseResult<'t, T>,
+    ) -> Result<T, Set<ParseError<'t>>> {
+        self.skip_whitespace();
+
+        let SuccessfulParse {
+            text,
+            reductions,
+            value,
+        } = op(self.scope, self.text)?;
+
+        // Adjust our point in the input text
+        self.text = text;
+
+        // Some value was produced, so there must have been a reduction
+        assert!(!reductions.is_empty());
+
+        // Accumulate the reductions we have done so far
+        self.reductions.extend(reductions);
+
+        // And return the value
+        Ok(value)
+    }
+}
+
+/// Extract the next character from input, returning an error if we've reached the input.
+///
+/// Warning: does not skip whitespace.
+pub fn next_char(text: &str) -> TokenResult<'_, char> {
+    let ch = match text.chars().next() {
+        Some(c) => c,
+        None => return Err(ParseError::at(text, "unexpected end of input".to_string())),
+    };
+    Ok((ch, &text[char::len_utf8(ch)..]))
+}
+
+/// Consume a comma if one is present.
+#[tracing::instrument(level = "trace", ret)]
+pub fn skip_trailing_comma(text: &str) -> &str {
+    text.strip_prefix(',').unwrap_or(text)
+}
+
+/// Skips leading whitespace and comments.
+pub fn skip_whitespace(mut text: &str) -> &str {
+    loop {
+        let len = text.len();
+
+        text = text.trim_start();
+
+        if text.starts_with("//") {
+            match text.find('\n') {
+                Some(index) => {
+                    text = &text[index + 1..];
+                }
+                None => {
+                    text = "";
+                }
+            }
+        }
+
+        if text.len() == len {
+            return text;
+        }
+    }
+}
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index cae1de68..5b392a34 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -6,8 +6,8 @@ use syn::{spanned::Spanned, Attribute};
 use synstructure::BindingInfo;
 
 use crate::{
-    spec::{self, FieldMode, FormalitySpec, FormalitySpecSymbol},
-    attrs::{has_variable_attr, has_cast_attr},
+    attrs::{has_cast_attr, has_variable_attr},
+    spec::{self, FieldMode, FormalitySpec},
 };
 
 /// Derive the `Parse` impl, using an optional grammar supplied "from the outside".
@@ -23,38 +23,30 @@ pub(crate) fn derive_parse_with_spec(
         ));
     }
 
-    let mut stream = TokenStream::new();
-
-    let type_name = Literal::string(&format!("`{}`", s.ast().ident));
-
-    if let syn::Data::Struct(_) = s.ast().data {
-        // For structs, where there is only one variant, use the external grammar (if any).
-        stream.extend(parse_variant(&type_name, &s.variants()[0], external_spec)?);
-    } else {
-        // If there are multiple variants, there should not be an external grammar.
-        // Parse them all and require an unambiguous parse.
-        if external_spec.is_some() {
-            return Err(syn::Error::new_spanned(
-                &s.ast().ident,
-                "for enums provide the grammar on each variant".to_string(),
-            ));
+    if external_spec.is_some() {
+        // Only allow external specs for structs.
+        match s.ast().data {
+            syn::Data::Struct(_) => {}
+            syn::Data::Enum(_) | syn::Data::Union(_) => {
+                return Err(syn::Error::new_spanned(
+                    &s.ast().ident,
+                    "for enums provide the grammar on each variant".to_string(),
+                ));
+            }
         }
+    }
 
-        stream.extend(quote! {
-            let mut __results = vec![];
+    let mut parse_variants = TokenStream::new();
+    for variant in s.variants() {
+        let variant_name = as_literal(variant.ast().ident);
+        let v = parse_variant(variant, external_spec)?;
+        parse_variants.extend(quote! {
+            {
+                let __span = tracing::span!(tracing::Level::TRACE, "parse", variant_name = #variant_name);
+                let __guard = __span.enter();
+                __parser.parse_variant(#variant_name, 0, |__p| { #v });
+            }
         });
-        for variant in s.variants() {
-            let variant_name = as_literal(variant.ast().ident);
-            let v = parse_variant(&type_name, variant, None)?;
-            stream.extend(quote! {
-                __results.push({
-                    let __span = tracing::span!(tracing::Level::TRACE, "parse", variant_name = #variant_name);
-                    let __guard = __span.enter();
-                    parse::try_parse(|| { #v })
-                });
-            });
-        }
-        stream.extend(quote! {parse::require_unambiguous(text, __results, #type_name)});
     }
 
     let type_name: Literal = as_literal(&s.ast().ident);
@@ -64,18 +56,15 @@ pub(crate) fn derive_parse_with_spec(
         gen impl parse::CoreParse<crate::FormalityLang> for @Self {
             fn parse<'t>(scope: &parse::Scope<crate::FormalityLang>, text: &'t str) -> parse::ParseResult<'t, Self>
             {
-                let __span = tracing::span!(tracing::Level::TRACE, "parse", type_name = #type_name, ?scope, ?text);
-                let __guard = __span.enter();
-                let __result = { #stream };
-                tracing::trace!("result = {:?}", __result);
-                __result
+                let mut __parser = parse::Parser::new(scope, text, #type_name);
+                #parse_variants;
+                __parser.finish()
             }
         }
     }))
 }
 
 fn parse_variant(
-    type_name: &Literal,
     variant: &synstructure::VariantInfo,
     external_spec: Option<&FormalitySpec>,
 ) -> syn::Result<TokenStream> {
@@ -97,37 +86,41 @@ fn parse_variant(
         // No bindings (e.g., `Foo`) -- just parse a keyword `foo`
         let literal = Literal::string(&to_parse_ident(ast.ident));
         let construct = variant.construct(|_, _| quote! {});
-        Ok(quote! {
-            let ((), text) = parse::expect_keyword(#literal, text)?;
-            Ok((#construct, text))
+        Ok(quote_spanned! {
+            ast.ident.span() =>
+            __p.expect_keyword(#literal)?;
+            Ok(#construct)
         })
     } else if has_variable_attr(variant.ast().attrs) {
         // Has the `#[variable]` attribute -- parse an identifier and then check to see if it is present
         // in the scope. If so, downcast it and check that it has the correct kind.
         Ok(quote_spanned! {
             ast.ident.span() =>
-            parse::parse_variable(scope, text, #type_name)
+            let v = __p.variable()?;
+            Ok(v)
         })
     } else if has_cast_attr(variant.ast().attrs) {
         // Has the `#[cast]` attribute -- just parse the bindings (comma separated, if needed)
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
         let construct = variant.construct(field_ident);
-        Ok(quote! {
+        Ok(quote_spanned! {
+            ast.ident.span() =>
             #(#build)*
-            Ok((#construct, text))
+            Ok(#construct)
         })
     } else {
         // Otherwise -- parse `variant(binding0, ..., bindingN)`
         let literal = Literal::string(&to_parse_ident(ast.ident));
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
         let construct = variant.construct(field_ident);
-        Ok(quote! {
-            let ((), text) = parse::expect_keyword(#literal, text)?;
-            let ((), text) = parse::expect_char('(', text)?;
+        Ok(quote_spanned! {
+            ast.ident.span() =>
+            __p.expect_keyword(#literal)?;
+            __p.expect_char('(')?;
             #(#build)*
-            let text = parse::skip_trailing_comma(text);
-            let ((), text) = parse::expect_char(')', text)?;
-            Ok((#construct, text))
+            __p.skip_trailing_comma();
+            __p.expect_char(')')?;
+            Ok(#construct)
         })
     }
 }
@@ -154,16 +147,15 @@ fn parse_variant_with_attr(
 ) -> syn::Result<TokenStream> {
     let mut stream = TokenStream::new();
 
-    for i in 0..spec.symbols.len() {
-        let symbol = &spec.symbols[i];
-        let next_symbol = spec.symbols.get(i + 1);
+    for symbol in &spec.symbols {
         stream.extend(match symbol {
             spec::FormalitySpecSymbol::Field {
                 name,
                 mode: FieldMode::Single,
             } => {
                 quote_spanned! {
-                    name.span() => let (#name, text) = parse::CoreParse::parse(scope, text)?;
+                    name.span() =>
+                    let #name = __p.nonterminal()?;
                 }
             }
 
@@ -172,8 +164,8 @@ fn parse_variant_with_attr(
                 mode: FieldMode::Optional,
             } => {
                 quote_spanned! {
-                    name.span() => 
-                    let (#name, text) = parse::CoreParse::parse_opt(scope, text)?;
+                    name.span() =>
+                    let #name = __p.opt_nonterminal()?;
                     let #name = #name.unwrap_or_default();
                 }
             }
@@ -182,13 +174,9 @@ fn parse_variant_with_attr(
                 name,
                 mode: FieldMode::Many,
             } => {
-                match lookahead(next_symbol) {
-                    Some(lookahead) => quote_spanned! {
-                        name.span() => let (#name, text) = parse::CoreParse::parse_many(scope, text, #lookahead)?;
-                    },
-                    None => quote_spanned! {
-                        name.span() => let (#name, text) = parse::CoreParse::parse_while_possible(scope, text)?;
-                    },
+                quote_spanned! {
+                    name.span() =>
+                    let #name = __p.many_nonterminal()?;
                 }
             }
 
@@ -196,33 +184,32 @@ fn parse_variant_with_attr(
                 name,
                 mode: FieldMode::Comma,
             } => {
-                match lookahead(next_symbol) {
-                    Some(lookahead) => quote_spanned! {
-                        name.span() => let (#name, text) = parse::CoreParse::parse_comma(scope, text, #lookahead)?;
-                    },
-                    None => {
-                        return Err(syn::Error::new_spanned(
-                            name,
-                            "cannot use `,` without lookahead".to_string(),
-                        ));
-                    }
+                quote_spanned! {
+                    name.span() =>
+                    let #name = __p.comma_nonterminal()?;
                 }
-                
             }
 
             spec::FormalitySpecSymbol::Keyword { ident } => {
                 let literal = as_literal(ident);
-                quote_spanned!(ident.span() => let ((), text) = parse::expect_keyword(#literal, text)?;)
+                quote_spanned!(ident.span() =>
+                    let () = __p.expect_keyword(#literal)?;
+                )
             }
 
             spec::FormalitySpecSymbol::Char { punct } => {
                 let literal = Literal::character(punct.as_char());
-                quote_spanned!(punct.span() => let ((), text) = parse::expect_char(#literal, text)?;)
+                quote_spanned!(
+                    punct.span() =>
+                    let () = __p.expect_char(#literal)?;
+                )
             }
 
             spec::FormalitySpecSymbol::Delimeter { text } => {
                 let literal = Literal::character(*text);
-                quote!(let ((), text) = parse::expect_char(#literal, text)?;)
+                quote!(
+                    let () = __p.expect_char(#literal)?;
+                )
             }
         });
     }
@@ -230,20 +217,12 @@ fn parse_variant_with_attr(
     let c = variant.construct(field_ident);
 
     stream.extend(quote! {
-        Ok((#c, text))
+        Ok(#c)
     });
 
     Ok(stream)
 }
 
-fn lookahead(next_symbol: Option<&FormalitySpecSymbol>) -> Option<Literal> {
-    match next_symbol {
-        Some(FormalitySpecSymbol::Char { punct }) => Some(Literal::character(punct.as_char())),
-        Some(FormalitySpecSymbol::Delimeter { text }) => Some(Literal::character(*text)),
-        Some(FormalitySpecSymbol::Keyword { .. }) | Some(FormalitySpecSymbol::Field { .. }) | None => None,
-    }
-}
-
 fn get_grammar_attr(attrs: &[Attribute]) -> Option<syn::Result<FormalitySpec>> {
     let attr = attrs.iter().find(|a| a.path().is_ident("grammar"))?;
     Some(attr.parse_args())
@@ -275,13 +254,17 @@ fn parse_bindings(bindings: &[BindingInfo]) -> Vec<TokenStream> {
         .map(|(b, index)| {
             let name = field_ident(b.ast(), index);
             let parse_comma = if index > 0 {
-                Some(quote!(let ((), text) = parse::expect_char(',', text)?;))
+                Some(quote_spanned!(
+                    name.span() =>
+                    __p.expect_char(',')?;
+                ))
             } else {
                 None
             };
-            quote! {
+            quote_spanned! {
+                name.span() =>
                 #parse_comma
-                let (#name, text) = parse::CoreParse::parse(scope, text)?;
+                let #name = __p.nonterminal()?;
             }
         })
         .collect()
diff --git a/crates/formality-rust/src/trait_binder.rs b/crates/formality-rust/src/trait_binder.rs
index 9845390d..bd947f7f 100644
--- a/crates/formality-rust/src/trait_binder.rs
+++ b/crates/formality-rust/src/trait_binder.rs
@@ -2,10 +2,10 @@ use std::fmt::Debug;
 
 use formality_core::{
     fold::CoreFold,
-    parse::{expect_char, Binding, CoreParse, ParseResult, Scope},
+    parse::{Binding, CoreParse, ParseResult, Parser, Scope},
     term::CoreTerm,
     visit::CoreVisit,
-    DowncastTo, To, UpcastFrom,
+    DowncastTo, UpcastFrom,
 };
 use formality_types::{
     grammar::{Binder, BoundVar, ParameterKind},
@@ -89,29 +89,29 @@ where
 {
     #[tracing::instrument(level = "trace", ret)]
     fn parse<'t>(scope: &Scope<FormalityLang>, text: &'t str) -> ParseResult<'t, Self> {
-        // parse the explicit bindings written by the user
-        let ((), text) = expect_char('<', text)?;
-        let (mut bindings, text) = Binding::parse_comma(scope, text, '>')?;
-        let ((), text) = expect_char('>', text)?;
-
-        // insert the `Self` binding at position 0
-        let bound_var = BoundVar::fresh(ParameterKind::Ty);
-        bindings.insert(
-            0,
-            Binding {
-                name: "Self".to_string(),
-                bound_var,
-            },
-        );
-
-        // parse the contents with those names in scope
-        let scope1 =
-            scope.with_bindings(bindings.iter().map(|b| (b.name.clone(), b.bound_var.to())));
-        let (data, text) = T::parse(&scope1, text)?;
-
-        let bound_vars: Vec<BoundVar> = bindings.iter().map(|b| b.bound_var).collect();
-        let explicit_binder = Binder::new(bound_vars, data);
-
-        Ok((TraitBinder { explicit_binder }, text))
+        Parser::single_variant(scope, text, "TraitBinder", |p| {
+            p.expect_char('<')?;
+            let mut bindings: Vec<Binding<FormalityLang>> = p.comma_nonterminal()?;
+            p.expect_char('>')?;
+
+            // insert the `Self` binding at position 0
+            let bound_var = BoundVar::fresh(ParameterKind::Ty);
+            bindings.insert(
+                0,
+                Binding {
+                    name: "Self".to_string(),
+                    bound_var,
+                },
+            );
+
+            // parse the contents with those names in scope
+            let scope1 = scope.with_bindings(bindings.iter().map(|b| (&b.name, &b.bound_var)));
+            let data: T = p.with_scope(scope1, |p| p.nonterminal())?;
+
+            let bound_vars: Vec<BoundVar> = bindings.iter().map(|b| b.bound_var).collect();
+            let explicit_binder = Binder::new(bound_vars, data);
+
+            Ok(TraitBinder { explicit_binder })
+        })
     }
 }
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index e77fc677..8d5353d6 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -1,10 +1,8 @@
 //! Handwritten parser impls.
 
-use formality_core::parse::{
-    self, expect_char, expect_keyword, reject_keyword, CoreParse, ParseError, ParseResult, Scope,
-};
-use formality_core::seq;
+use formality_core::parse::{ActiveVariant, CoreParse, ParseError, ParseResult, Parser, Scope};
 use formality_core::Upcast;
+use formality_core::{seq, Set};
 
 use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RigidName, Scalar, TraitId};
 
@@ -17,45 +15,18 @@ use crate::rust::FormalityLang as Rust;
 // writing tests so much more pleasant.
 impl CoreParse<Rust> for Ty {
     fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
-        // Support writing `u8` etc and treat them as keywords
-        if let Ok((scalar_ty, text1)) = ScalarId::parse(scope, text0) {
-            return Ok((scalar_ty.upcast(), text1));
-        }
-
-        // Support naming variables in scope and give that preference
-        if let Ok((p, text1)) = parse_variable(scope, text0) {
-            return match p {
-                Parameter::Ty(ty) => Ok((ty, text1)),
-                _ => Err(ParseError::at(
-                    text0,
-                    format!("expected type, found `{:?}`", p.kind()),
-                )),
-            };
-        }
-
-        parse::require_unambiguous(
-            text0,
-            vec![
-                parse::try_parse(|| parse_adt_ty(scope, text0)),
-                parse::try_parse(|| parse_assoc_ty(scope, text0)),
-                parse::try_parse(|| parse_ref_ty(scope, text0)),
-                parse::try_parse(|| parse_ref_mut_ty(scope, text0)),
-                parse::try_parse(|| parse_tuple_ty(scope, text0)),
-                parse::try_parse(|| {
-                    let (ty, text) = RigidTy::parse(scope, text0)?;
-                    Ok((Ty::new(ty), text))
-                }),
-                parse::try_parse(|| {
-                    let (ty, text) = AliasTy::parse(scope, text0)?;
-                    Ok((Ty::new(ty), text))
-                }),
-                parse::try_parse(|| {
-                    let (ty, text) = PredicateTy::parse(scope, text0)?;
-                    Ok((Ty::new(ty), text))
-                }),
-            ],
-            "`Ty`",
-        )
+        let mut parser = Parser::new(scope, text0, "Ty");
+        parser.parse_variant_cast::<ScalarId>(1);
+        parser.parse_variant("Variable", 1, |p| p.variable());
+        parser.parse_variant("Adt", 0, |p| p.nonterminal_with(parse_adt_ty));
+        parser.parse_variant("Assoc", 0, |p| p.nonterminal_with(parse_assoc_ty));
+        parser.parse_variant("Ref", 0, |p| p.nonterminal_with(parse_ref_ty));
+        parser.parse_variant("RefMut", 0, |p| p.nonterminal_with(parse_ref_mut_ty));
+        parser.parse_variant("Tuple", 0, |p| p.nonterminal_with(parse_tuple_ty));
+        parser.parse_variant_cast::<RigidTy>(0);
+        parser.parse_variant_cast::<AliasTy>(0);
+        parser.parse_variant_cast::<PredicateTy>(0);
+        parser.finish()
     }
 }
 // ANCHOR_END: ty_parse_impl
@@ -63,129 +34,103 @@ impl CoreParse<Rust> for Ty {
 #[tracing::instrument(level = "trace", ret)]
 fn parse_adt_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
     // Treat plain identifiers as adt ids, with or without parameters.
-    let ((), text) = reject_keyword("static", text)?;
-    let ((), text) = reject_keyword("const", text)?;
-    let (name, text) = AdtId::parse(scope, text)?;
-    let (parameters, text) = parse_parameters(scope, text)?;
-    Ok((Ty::rigid(name, parameters), text))
+    Parser::single_variant(scope, text, "AdtTy", |p| {
+        let name: AdtId = p.nonterminal()?;
+        let parameters: Vec<Parameter> = parse_parameters(p)?;
+        Ok(Ty::rigid(name, parameters))
+    })
 }
 
 #[tracing::instrument(level = "trace", ret)]
 fn parse_ref_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    let ((), text) = expect_char('&', text)?;
-    let (lt, text) = Lt::parse(scope, text)?;
-    let (ty, text) = Ty::parse(scope, text)?;
-    let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Shared);
-    Ok((
-        RigidTy {
+    Parser::single_variant(scope, text, "RefTy", |p| {
+        p.expect_char('&')?;
+        let lt: Lt = p.nonterminal()?;
+        let ty: Ty = p.nonterminal()?;
+        let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Shared);
+        Ok(RigidTy {
             name,
             parameters: seq![lt.upcast(), ty.upcast()],
         }
-        .upcast(),
-        text,
-    ))
+        .upcast())
+    })
 }
 
 #[tracing::instrument(level = "trace", ret)]
 fn parse_ref_mut_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    let ((), text) = expect_char('&', text)?;
-    let ((), text) = expect_keyword("mut", text)?;
-    let (lt, text) = Lt::parse(scope, text)?;
-    let (ty, text) = Ty::parse(scope, text)?;
-    let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Mut);
-    Ok((
-        RigidTy {
+    Parser::single_variant(scope, text, "RefMutTy", |p| {
+        p.expect_char('&')?;
+        p.expect_keyword("mut")?;
+        let lt: Lt = p.nonterminal()?;
+        let ty: Ty = p.nonterminal()?;
+        let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Mut);
+        Ok(RigidTy {
             name,
             parameters: seq![lt.upcast(), ty.upcast()],
         }
-        .upcast(),
-        text,
-    ))
+        .upcast())
+    })
 }
 
 #[tracing::instrument(level = "trace", ret)]
 fn parse_tuple_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    let ((), text) = expect_char('(', text)?;
-    let ((), text) = reject_keyword("rigid", text)?;
-    let ((), text) = reject_keyword("alias", text)?;
-    let ((), text) = reject_keyword("predicate", text)?;
-    let (types, text) = Ty::parse_comma(scope, text, ')')?;
-    let ((), text) = expect_char(')', text)?;
-    let name = RigidName::Tuple(types.len());
-    Ok((
-        RigidTy {
+    Parser::single_variant(scope, text, "TupleTy", |p| {
+        p.expect_char('(')?;
+        p.reject_custom_keywords(&["alias", "rigid", "predicate"])?;
+        let types: Vec<Ty> = p.comma_nonterminal()?;
+        p.expect_char(')')?;
+        let name = RigidName::Tuple(types.len());
+        Ok(RigidTy {
             name,
             parameters: types.upcast(),
         }
-        .upcast(),
-        text,
-    ))
+        .upcast())
+    })
 }
 
 #[tracing::instrument(level = "trace", ret)]
 fn parse_assoc_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
+    Parser::single_variant(scope, text, "AssocTy", |p| {
+        p.expect_char('<')?;
+        let ty0: Ty = p.nonterminal()?;
+        let () = p.expect_keyword("as")?;
+        let trait_id: TraitId = p.nonterminal()?;
+        let trait_parameters1 = parse_parameters(p)?;
+        p.expect_char('>')?;
+        p.expect_char(':')?;
+        p.expect_char(':')?;
+        let item_id: AssociatedItemId = p.nonterminal()?;
+        let item_parameters = parse_parameters(p)?;
+        let assoc_ty_id = AssociatedTyName { trait_id, item_id };
+        let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
+            .chain(trait_parameters1)
+            .chain(item_parameters)
+            .collect();
+        Ok(Ty::alias(assoc_ty_id, parameters))
+    })
     // Treat plain identifiers as adt ids, with or without parameters.
-    let ((), text) = expect_char('<', text)?;
-    let (ty0, text) = Ty::parse(scope, text)?;
-    let ((), text) = expect_keyword("as", text)?;
-    let (trait_id, text) = TraitId::parse(scope, text)?;
-    let (trait_parameters1, text) = parse_parameters(scope, text)?;
-    let ((), text) = expect_char('>', text)?;
-    let ((), text) = expect_char(':', text)?;
-    let ((), text) = expect_char(':', text)?;
-    let (item_id, text) = AssociatedItemId::parse(scope, text)?;
-    let (item_parameters, text) = parse_parameters(scope, text)?;
-
-    let assoc_ty_id = AssociatedTyName { trait_id, item_id };
-    let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
-        .chain(trait_parameters1)
-        .chain(item_parameters)
-        .collect();
-    Ok((Ty::alias(assoc_ty_id, parameters), text))
 }
 
-#[tracing::instrument(level = "trace", ret)]
-fn parse_parameters<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Vec<Parameter>> {
-    let text = match expect_char('<', text) {
-        Err(_) => return Ok((vec![], text)),
-        Ok(((), text)) => text,
-    };
-    let (parameters, text) = Parameter::parse_comma(scope, text, '>')?;
-    let ((), text) = expect_char('>', text)?;
-    Ok((parameters, text))
+fn parse_parameters<'t>(
+    p: &mut ActiveVariant<'_, 't, Rust>,
+) -> Result<Vec<Parameter>, Set<ParseError<'t>>> {
+    if let Err(_) = p.expect_char('<') {
+        return Ok(vec![]);
+    }
+    let parameters: Vec<Parameter> = p.comma_nonterminal()?;
+    p.expect_char('>')?;
+    Ok(parameters)
 }
 
 impl CoreParse<Rust> for Lt {
     fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
-        parse::require_unambiguous(
-            text0,
-            vec![
-                parse::try_parse(|| {
-                    let ((), text) = expect_keyword("static", text0)?;
-                    Ok((Lt::new(LtData::Static), text))
-                }),
-                parse::try_parse(|| {
-                    let (p, text1) = parse_variable(scope, text0)?;
-                    match p {
-                        Parameter::Lt(lt) => Ok((lt, text1)),
-                        _ => Err(ParseError::at(
-                            text0,
-                            format!("expected lifetime, found `{:?}`", p.kind()),
-                        )),
-                    }
-                }),
-            ],
-            "`Lt`",
-        )
-    }
-}
-
-#[tracing::instrument(level = "trace", ret)]
-fn parse_variable<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Parameter> {
-    let (id, text1) = parse::identifier(text0)?;
-    match scope.lookup(&id) {
-        Some(parameter) => Ok((parameter, text1)),
-        None => Err(ParseError::at(text0, format!("unrecognized variable"))),
+        let mut parser = Parser::new(scope, text0, "Lt");
+        parser.parse_variant("static", 0, |p| {
+            p.expect_keyword("static")?;
+            Ok(Lt::new(LtData::Static))
+        });
+        parser.parse_variant("variable", 0, |p| p.variable());
+        parser.finish()
     }
 }
 
@@ -193,39 +138,20 @@ fn parse_variable<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Pa
 // writing tests so much more pleasant.
 impl CoreParse<Rust> for Const {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
-        let text = parse::skip_whitespace(text);
-        if let Ok((bool, text)) = Bool::parse(scope, text) {
-            return Ok((bool.upcast(), text));
-        }
-        // Support naming variables in scope and give that preference
-        if let Ok((p, text1)) = parse_variable(scope, text) {
-            return match p {
-                Parameter::Const(c) => Ok((c, text1)),
-                _ => Err(ParseError::at(
-                    text,
-                    format!("expected type, found `{:?}`", p.kind()),
-                )),
-            };
-        }
-        parse::require_unambiguous(
-            text,
-            vec![parse::try_parse(|| parse_int(scope, text))],
-            "`Const`",
-        )
+        let mut parser: Parser<'_, '_, Const, Rust> = Parser::new(scope, text, "Ty");
+        parser.parse_variant_cast::<Bool>(1);
+        parser.parse_variant("Variable", 1, |p| p.variable());
+        parser.parse_variant("Int", 0, |p| p.nonterminal_with(parse_int));
+        parser.finish()
     }
 }
 
 #[tracing::instrument(level = "trace", ret)]
 fn parse_int<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Const> {
-    let (num, text) = text.split_once('_').ok_or_else(|| {
-        ParseError::at(
-            text,
-            format!("numeric constants must be followed by an `_` and their type"),
-        )
-    })?;
-    let n: u128 = num
-        .parse()
-        .map_err(|err| ParseError::at(num, format!("could not parse number: {err}")))?;
-    let (ty, text) = Ty::parse(scope, text)?;
-    Ok((Const::valtree(Scalar::new(n), ty), text))
+    Parser::single_variant(scope, text, "Ty", |p| {
+        let n: u128 = p.number()?;
+        p.expect_char('_')?;
+        let ty: Ty = p.nonterminal()?;
+        Ok(Const::valtree(Scalar::new(n), ty))
+    })
 }
diff --git a/crates/formality-types/src/lib.rs b/crates/formality-types/src/lib.rs
index e30835d4..6773d975 100644
--- a/crates/formality-types/src/lib.rs
+++ b/crates/formality-types/src/lib.rs
@@ -10,6 +10,15 @@ formality_core::declare_language! {
         type Parameter = crate::grammar::Parameter;
         const BINDING_OPEN = '<';
         const BINDING_CLOSE = '>';
+        const KEYWORDS = [
+            "mut",
+            "struct",
+            "enum",
+            "union",
+            "const",
+            "ty",
+            "lt",
+        ];
     }
 }
 // ANCHOR_END: declare_rust_language
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
index 06461886..030ef19f 100644
--- a/tests/associated_type_normalization.rs
+++ b/tests/associated_type_normalization.rs
@@ -1,4 +1,5 @@
 use a_mir_formality::test_where_clause;
+use formality_core::test;
 
 const MIRROR: &str = "[
     crate core {
diff --git a/tests/ui/parser.stderr b/tests/ui/parser.stderr
index 40eeaa3a..61a957c7 100644
--- a/tests/ui/parser.stderr
+++ b/tests/ui/parser.stderr
@@ -1,7 +1,7 @@
 Error: expected `:`
 
 Caused by:
-    0:  ] {}
+    0: ] {}
            }
        ]
        

From 3b605bd15d869f643708ab5a3a101115425bf576 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 08:32:01 -0400
Subject: [PATCH 13/22] support customization

---
 crates/formality-macros/src/attrs.rs  | 31 ++++++++++++++-
 crates/formality-macros/src/custom.rs | 56 +++++++++++++++++++++++++++
 crates/formality-macros/src/lib.rs    |  1 +
 crates/formality-macros/src/term.rs   | 21 ++++++++--
 4 files changed, 105 insertions(+), 4 deletions(-)
 create mode 100644 crates/formality-macros/src/custom.rs

diff --git a/crates/formality-macros/src/attrs.rs b/crates/formality-macros/src/attrs.rs
index 36229b06..c7dfadf0 100644
--- a/crates/formality-macros/src/attrs.rs
+++ b/crates/formality-macros/src/attrs.rs
@@ -1,6 +1,8 @@
 //! Functions to manipulate the custom attributes that guide our macros in various ways.
 
-use syn::{Attribute, DeriveInput};
+use syn::{spanned::Spanned, Attribute, DeriveInput};
+
+use crate::custom::Customize;
 
 /// Checks for any kind of attribute that indicates an "is-a" relationship,
 /// e.g. `#[cast]` and `#[variable]`.
@@ -37,6 +39,33 @@ pub(crate) fn has_variable_attr(attrs: &[Attribute]) -> bool {
     attrs.iter().any(|a| a.path().is_ident("variable"))
 }
 
+/// Extracts any customization attribute from a list of attributes.
+pub(crate) fn customize(attrs: &[Attribute]) -> syn::Result<Customize> {
+    let mut v: Vec<Customize> = attrs
+        .iter()
+        .filter(|a| a.path().is_ident("customize"))
+        .map(|a| a.parse_args())
+        .collect::<syn::Result<_>>()?;
+
+    if v.len() > 1 {
+        Err(syn::Error::new(
+            attrs
+                .iter()
+                .filter(|a| a.path().is_ident("customize"))
+                .skip(1)
+                .next()
+                .unwrap()
+                .path()
+                .span(),
+            "multiple customize attributes",
+        ))
+    } else if v.len() == 1 {
+        Ok(v.pop().unwrap())
+    } else {
+        Ok(Customize::default())
+    }
+}
+
 /// Removes all attributes from the input that are specific to formality.
 pub(crate) fn remove_formality_attributes(input: &mut DeriveInput) {
     remove_formality_attributes_from_vec(&mut input.attrs);
diff --git a/crates/formality-macros/src/custom.rs b/crates/formality-macros/src/custom.rs
new file mode 100644
index 00000000..38048af7
--- /dev/null
+++ b/crates/formality-macros/src/custom.rs
@@ -0,0 +1,56 @@
+use proc_macro2::TokenStream;
+
+#[derive(Default, Debug)]
+pub(crate) struct Customize {
+    pub parse: bool,
+    pub debug: bool,
+}
+
+impl syn::parse::Parse for Customize {
+    fn parse(input: syn::parse::ParseStream) -> syn::Result<Self> {
+        let mut result = Customize::default();
+
+        let token_stream: TokenStream = input.parse()?;
+        let mut tokens = token_stream.into_iter();
+        while let Some(token) = tokens.next() {
+            match token {
+                proc_macro2::TokenTree::Ident(ident) if ident == "parse" => {
+                    if result.parse {
+                        return Err(syn::Error::new(ident.span(), "already customizing parse"));
+                    }
+                    result.parse = true;
+                }
+
+                proc_macro2::TokenTree::Ident(ident) if ident == "debug" => {
+                    if result.debug {
+                        return Err(syn::Error::new(ident.span(), "already customizing debug"));
+                    }
+                    result.debug = true;
+                }
+
+                _ => {
+                    return Err(syn::Error::new(
+                        token.span(),
+                        "unexpected token in customization",
+                    ));
+                }
+            }
+
+            if let Some(token) = tokens.next() {
+                match token {
+                    proc_macro2::TokenTree::Punct(p) if p.as_char() == ',' => (),
+                    _ => {
+                        return Err(syn::Error::new(
+                            token.span(),
+                            "unexpected token in customization",
+                        ));
+                    }
+                }
+            } else {
+                break;
+            }
+        }
+
+        Ok(result)
+    }
+}
diff --git a/crates/formality-macros/src/lib.rs b/crates/formality-macros/src/lib.rs
index e231dd7b..c7a36d00 100644
--- a/crates/formality-macros/src/lib.rs
+++ b/crates/formality-macros/src/lib.rs
@@ -7,6 +7,7 @@ extern crate proc_macro;
 
 mod attrs;
 mod cast;
+mod custom;
 mod debug;
 mod fixed_point;
 mod fold;
diff --git a/crates/formality-macros/src/term.rs b/crates/formality-macros/src/term.rs
index 4f680ca3..c43d47ec 100644
--- a/crates/formality-macros/src/term.rs
+++ b/crates/formality-macros/src/term.rs
@@ -3,7 +3,7 @@ use quote::quote;
 use syn::DeriveInput;
 
 use crate::{
-    attrs::remove_formality_attributes,
+    attrs::{self, remove_formality_attributes},
     cast::{downcast_impls, upcast_impls},
     debug::derive_debug_with_spec,
     fold::derive_fold,
@@ -13,10 +13,25 @@ use crate::{
 };
 
 pub fn term(spec: Option<FormalitySpec>, mut input: DeriveInput) -> syn::Result<TokenStream> {
+    let customize = attrs::customize(&input.attrs)?;
     let fold_impl = derive_fold(synstructure::Structure::new(&input));
     let visit_impl = derive_visit(synstructure::Structure::new(&input));
-    let parse_impl = derive_parse_with_spec(synstructure::Structure::new(&input), spec.as_ref())?;
-    let debug_impl = derive_debug_with_spec(synstructure::Structure::new(&input), spec.as_ref());
+    let parse_impl = if customize.parse {
+        None
+    } else {
+        Some(derive_parse_with_spec(
+            synstructure::Structure::new(&input),
+            spec.as_ref(),
+        )?)
+    };
+    let debug_impl = if customize.debug {
+        None
+    } else {
+        Some(derive_debug_with_spec(
+            synstructure::Structure::new(&input),
+            spec.as_ref(),
+        ))
+    };
     let term_impl = derive_term(synstructure::Structure::new(&input));
     let downcast_impls = downcast_impls(synstructure::Structure::new(&input));
     let upcast_impls = upcast_impls(synstructure::Structure::new(&input));

From 6cf0caa5dbd7cf3790016bbc96854d1eb1030847 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 13:35:53 -0400
Subject: [PATCH 14/22] make it possible to customize typing

and start moving more things into macros
---
 crates/formality-macros/src/attrs.rs          |   1 +
 crates/formality-types/src/grammar/ty.rs      |  25 ++-
 .../src/grammar/ty/debug_impls.rs             |  11 --
 .../src/grammar/ty/parse_impls.rs             | 163 +++++++++---------
 .../src/grammar/ty/term_impls.rs              |  39 +----
 tests/projection.rs                           |   2 +-
 6 files changed, 95 insertions(+), 146 deletions(-)

diff --git a/crates/formality-macros/src/attrs.rs b/crates/formality-macros/src/attrs.rs
index c7dfadf0..6bf2752e 100644
--- a/crates/formality-macros/src/attrs.rs
+++ b/crates/formality-macros/src/attrs.rs
@@ -81,5 +81,6 @@ fn remove_formality_attributes_from_vec(attrs: &mut Vec<Attribute>) {
         !attr.path().is_ident("grammar")
             && !attr.path().is_ident("cast")
             && !attr.path().is_ident("variable")
+            && !attr.path().is_ident("customize")
     });
 }
diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index b96785b3..0346a1cc 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -1,4 +1,4 @@
-use formality_core::{cast_impl, term, Visit};
+use formality_core::{cast_impl, term};
 use std::sync::Arc;
 
 mod debug_impls;
@@ -11,7 +11,8 @@ use super::{
     consts::Const, AdtId, AssociatedItemId, Binder, ExistentialVar, FnId, TraitId, UniversalVar,
 };
 
-#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[term]
+#[cast]
 pub struct Ty {
     data: Arc<TyData>,
 }
@@ -97,20 +98,19 @@ impl DowncastTo<TyData> for Ty {
 
 // NB: TyData doesn't implement Fold; you fold types, not TyData,
 // because variables might not map to the same variant.
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+#[term]
+#[customize(parse)]
 pub enum TyData {
+    #[cast]
     RigidTy(RigidTy),
+    #[cast]
     AliasTy(AliasTy),
+    #[cast]
     PredicateTy(PredicateTy),
+    #[variable]
     Variable(Variable),
 }
 
-impl UpcastFrom<TyData> for TyData {
-    fn upcast_from(term: TyData) -> Self {
-        term
-    }
-}
-
 impl UpcastFrom<Ty> for TyData {
     fn upcast_from(term: Ty) -> Self {
         term.data().clone()
@@ -118,6 +118,7 @@ impl UpcastFrom<Ty> for TyData {
 }
 
 #[term((rigid $name $*parameters))]
+#[customize(parse)]
 pub struct RigidTy {
     pub name: RigidName,
     pub parameters: Parameters,
@@ -187,6 +188,7 @@ pub enum ScalarId {
 }
 
 #[term((alias $name $*parameters))]
+#[customize(parse)]
 pub struct AliasTy {
     pub name: AliasName,
     pub parameters: Parameters,
@@ -353,7 +355,6 @@ impl DowncastTo<Variable> for Parameter {
     }
 }
 
-cast_impl!(Ty);
 cast_impl!((RigidTy) <: (TyData) <: (Ty));
 cast_impl!((AliasTy) <: (TyData) <: (Ty));
 cast_impl!((ScalarId) <: (TyData) <: (Ty));
@@ -363,10 +364,6 @@ cast_impl!((AliasTy) <: (Ty) <: (Parameter));
 cast_impl!((ScalarId) <: (Ty) <: (Parameter));
 cast_impl!((PredicateTy) <: (Ty) <: (Parameter));
 cast_impl!((TyData) <: (Ty) <: (Parameter));
-cast_impl!(TyData::RigidTy(RigidTy));
-cast_impl!(TyData::AliasTy(AliasTy));
-cast_impl!(TyData::PredicateTy(PredicateTy));
-cast_impl!(TyData::Variable(Variable));
 cast_impl!((Variable) <: (TyData) <: (Ty));
 cast_impl!((UniversalVar) <: (Variable) <: (TyData));
 cast_impl!((ExistentialVar) <: (Variable) <: (TyData));
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index a266f024..793fd776 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -1,16 +1,5 @@
 use crate::grammar::Const;
 
-impl std::fmt::Debug for super::Ty {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self.data() {
-            super::TyData::RigidTy(r) => write!(f, "{r:?}"),
-            super::TyData::AliasTy(r) => write!(f, "{r:?}"),
-            super::TyData::PredicateTy(r) => write!(f, "{r:?}"),
-            super::TyData::Variable(r) => write!(f, "{r:?}"),
-        }
-    }
-}
-
 impl std::fmt::Debug for Const {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self.data() {
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index 8d5353d6..e5738f2d 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -4,25 +4,21 @@ use formality_core::parse::{ActiveVariant, CoreParse, ParseError, ParseResult, P
 use formality_core::Upcast;
 use formality_core::{seq, Set};
 
-use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RigidName, Scalar, TraitId};
+use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
 
-use super::{AliasTy, AssociatedTyName, Lt, LtData, Parameter, PredicateTy, RigidTy, ScalarId, Ty};
+use super::{
+    AliasTy, AssociatedTyName, Lt, LtData, Parameter, PredicateTy, RigidTy, ScalarId, Ty, TyData,
+};
 
 use crate::rust::FormalityLang as Rust;
 
 // ANCHOR: ty_parse_impl
 // For types, we invest some effort into parsing them decently because it makes
 // writing tests so much more pleasant.
-impl CoreParse<Rust> for Ty {
+impl CoreParse<Rust> for TyData {
     fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
         let mut parser = Parser::new(scope, text0, "Ty");
-        parser.parse_variant_cast::<ScalarId>(1);
         parser.parse_variant("Variable", 1, |p| p.variable());
-        parser.parse_variant("Adt", 0, |p| p.nonterminal_with(parse_adt_ty));
-        parser.parse_variant("Assoc", 0, |p| p.nonterminal_with(parse_assoc_ty));
-        parser.parse_variant("Ref", 0, |p| p.nonterminal_with(parse_ref_ty));
-        parser.parse_variant("RefMut", 0, |p| p.nonterminal_with(parse_ref_mut_ty));
-        parser.parse_variant("Tuple", 0, |p| p.nonterminal_with(parse_tuple_ty));
         parser.parse_variant_cast::<RigidTy>(0);
         parser.parse_variant_cast::<AliasTy>(0);
         parser.parse_variant_cast::<PredicateTy>(0);
@@ -31,84 +27,87 @@ impl CoreParse<Rust> for Ty {
 }
 // ANCHOR_END: ty_parse_impl
 
-#[tracing::instrument(level = "trace", ret)]
-fn parse_adt_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    // Treat plain identifiers as adt ids, with or without parameters.
-    Parser::single_variant(scope, text, "AdtTy", |p| {
-        let name: AdtId = p.nonterminal()?;
-        let parameters: Vec<Parameter> = parse_parameters(p)?;
-        Ok(Ty::rigid(name, parameters))
-    })
-}
+impl CoreParse<Rust> for RigidTy {
+    fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
+        let mut parser: Parser<'_, '_, RigidTy, Rust> = Parser::new(scope, text, "AliasTy");
 
-#[tracing::instrument(level = "trace", ret)]
-fn parse_ref_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    Parser::single_variant(scope, text, "RefTy", |p| {
-        p.expect_char('&')?;
-        let lt: Lt = p.nonterminal()?;
-        let ty: Ty = p.nonterminal()?;
-        let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Shared);
-        Ok(RigidTy {
-            name,
-            parameters: seq![lt.upcast(), ty.upcast()],
-        }
-        .upcast())
-    })
-}
+        parser.parse_variant_cast::<ScalarId>(1);
 
-#[tracing::instrument(level = "trace", ret)]
-fn parse_ref_mut_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    Parser::single_variant(scope, text, "RefMutTy", |p| {
-        p.expect_char('&')?;
-        p.expect_keyword("mut")?;
-        let lt: Lt = p.nonterminal()?;
-        let ty: Ty = p.nonterminal()?;
-        let name = crate::grammar::RigidName::Ref(crate::grammar::RefKind::Mut);
-        Ok(RigidTy {
-            name,
-            parameters: seq![lt.upcast(), ty.upcast()],
-        }
-        .upcast())
-    })
-}
+        parser.parse_variant("Adt", 0, |p| {
+            let name: AdtId = p.nonterminal()?;
+            let parameters: Vec<Parameter> = parse_parameters(p)?;
+            Ok(RigidTy {
+                name: name.upcast(),
+                parameters,
+            })
+        });
 
-#[tracing::instrument(level = "trace", ret)]
-fn parse_tuple_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    Parser::single_variant(scope, text, "TupleTy", |p| {
-        p.expect_char('(')?;
-        p.reject_custom_keywords(&["alias", "rigid", "predicate"])?;
-        let types: Vec<Ty> = p.comma_nonterminal()?;
-        p.expect_char(')')?;
-        let name = RigidName::Tuple(types.len());
-        Ok(RigidTy {
-            name,
-            parameters: types.upcast(),
-        }
-        .upcast())
-    })
+        parser.parse_variant("Ref", 0, |p| {
+            p.expect_char('&')?;
+            let lt: Lt = p.nonterminal()?;
+            let ty: Ty = p.nonterminal()?;
+            Ok(RigidTy {
+                name: RigidName::Ref(RefKind::Shared),
+                parameters: seq![lt.upcast(), ty.upcast()],
+            }
+            .upcast())
+        });
+
+        parser.parse_variant("RefMut", 0, |p| {
+            p.expect_char('&')?;
+            p.expect_keyword("mut")?;
+            let lt: Lt = p.nonterminal()?;
+            let ty: Ty = p.nonterminal()?;
+            Ok(RigidTy {
+                name: RigidName::Ref(RefKind::Mut),
+                parameters: seq![lt.upcast(), ty.upcast()],
+            })
+        });
+
+        parser.parse_variant("Tuple", 0, |p| {
+            p.expect_char('(')?;
+            p.reject_custom_keywords(&["alias", "rigid", "predicate"])?;
+            let types: Vec<Ty> = p.comma_nonterminal()?;
+            p.expect_char(')')?;
+            let name = RigidName::Tuple(types.len());
+            Ok(RigidTy {
+                name,
+                parameters: types.upcast(),
+            })
+        });
+
+        parser.finish()
+    }
 }
 
-#[tracing::instrument(level = "trace", ret)]
-fn parse_assoc_ty<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Ty> {
-    Parser::single_variant(scope, text, "AssocTy", |p| {
-        p.expect_char('<')?;
-        let ty0: Ty = p.nonterminal()?;
-        let () = p.expect_keyword("as")?;
-        let trait_id: TraitId = p.nonterminal()?;
-        let trait_parameters1 = parse_parameters(p)?;
-        p.expect_char('>')?;
-        p.expect_char(':')?;
-        p.expect_char(':')?;
-        let item_id: AssociatedItemId = p.nonterminal()?;
-        let item_parameters = parse_parameters(p)?;
-        let assoc_ty_id = AssociatedTyName { trait_id, item_id };
-        let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
-            .chain(trait_parameters1)
-            .chain(item_parameters)
-            .collect();
-        Ok(Ty::alias(assoc_ty_id, parameters))
-    })
-    // Treat plain identifiers as adt ids, with or without parameters.
+impl CoreParse<Rust> for AliasTy {
+    fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
+        let mut parser: Parser<'_, '_, AliasTy, Rust> = Parser::new(scope, text, "AliasTy");
+
+        parser.parse_variant("associated type", 0, |p| {
+            p.expect_char('<')?;
+            let ty0: Ty = p.nonterminal()?;
+            let () = p.expect_keyword("as")?;
+            let trait_id: TraitId = p.nonterminal()?;
+            let trait_parameters1 = parse_parameters(p)?;
+            p.expect_char('>')?;
+            p.expect_char(':')?;
+            p.expect_char(':')?;
+            let item_id: AssociatedItemId = p.nonterminal()?;
+            let item_parameters = parse_parameters(p)?;
+            let name = AssociatedTyName { trait_id, item_id };
+            let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
+                .chain(trait_parameters1)
+                .chain(item_parameters)
+                .collect();
+            Ok(AliasTy {
+                name: name.upcast(),
+                parameters,
+            })
+        });
+
+        parser.finish()
+    }
 }
 
 fn parse_parameters<'t>(
diff --git a/crates/formality-types/src/grammar/ty/term_impls.rs b/crates/formality-types/src/grammar/ty/term_impls.rs
index fe80ffcc..a336bdf0 100644
--- a/crates/formality-types/src/grammar/ty/term_impls.rs
+++ b/crates/formality-types/src/grammar/ty/term_impls.rs
@@ -1,12 +1,10 @@
-use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, Ty, TyData, ValTree};
+use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, ValTree};
 use crate::rust::Variable;
 use crate::FormalityLang;
 use formality_core::{
     fold::{CoreFold, SubstitutionFn},
     language::CoreKind,
-    term::CoreTerm,
     visit::CoreVisit,
-    Upcast,
 };
 
 use super::ParameterKind;
@@ -40,10 +38,6 @@ impl CoreVisit<FormalityLang> for LtData {
     }
 }
 
-impl CoreTerm<FormalityLang> for Ty {}
-
-impl CoreTerm<FormalityLang> for Lt {}
-
 impl formality_core::language::HasKind<FormalityLang> for Parameter {
     fn kind(&self) -> CoreKind<FormalityLang> {
         match self {
@@ -54,23 +48,6 @@ impl formality_core::language::HasKind<FormalityLang> for Parameter {
     }
 }
 
-// ANCHOR: core_fold_ty
-impl CoreFold<FormalityLang> for Ty {
-    fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
-        match self.data() {
-            TyData::RigidTy(v) => v.substitute(substitution_fn).upcast(),
-            TyData::AliasTy(v) => v.substitute(substitution_fn).upcast(),
-            TyData::PredicateTy(v) => v.substitute(substitution_fn).upcast(),
-            TyData::Variable(v) => match substitution_fn(*v) {
-                None => self.clone(),
-                Some(Parameter::Ty(t)) => t,
-                Some(param) => panic!("ill-kinded substitute: expected type, got {param:?}"),
-            },
-        }
-    }
-}
-// ANCHOR_END: core_fold_ty
-
 impl CoreFold<FormalityLang> for Const {
     fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
         match self.data() {
@@ -106,20 +83,6 @@ impl CoreFold<FormalityLang> for Lt {
     }
 }
 
-impl CoreVisit<FormalityLang> for Ty {
-    fn free_variables(&self) -> Vec<Variable> {
-        self.data().free_variables()
-    }
-
-    fn size(&self) -> usize {
-        self.data().size()
-    }
-
-    fn assert_valid(&self) {
-        self.data().assert_valid()
-    }
-}
-
 impl CoreVisit<FormalityLang> for Lt {
     fn free_variables(&self) -> Vec<Variable> {
         self.data().free_variables()
diff --git a/tests/projection.rs b/tests/projection.rs
index eaa68498..9ad30cea 100644
--- a/tests/projection.rs
+++ b/tests/projection.rs
@@ -252,7 +252,7 @@ const PROJECTION_EQUALITY: &str = "[
             type Type<> : [] where [];
         }
         trait Trait2<ty T> where [] {}
-        impl<ty T, ty U> Trait2<T> for U where [ U: Trait1<>, (alias (Trait1::Type) S) => T ] {}
+        impl<ty T, ty U> Trait2<T> for U where [ U: Trait1<>, <S as Trait1>::Type => T ] {}
         struct S<> where [] {}
         impl<> Trait1<> for S<> where [] {
             type Type<> = u32 where [];

From 449c1e3be9d4991b217d8272e58d131ba5bbf329 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 13:49:58 -0400
Subject: [PATCH 15/22] implement (and use) precedence in parsing

---
 crates/formality-macros/src/attrs.rs          | 25 ++++++---
 crates/formality-macros/src/lib.rs            |  1 +
 crates/formality-macros/src/parse.rs          | 15 +++---
 crates/formality-macros/src/precedence.rs     | 51 +++++++++++++++++++
 crates/formality-types/src/grammar/ty.rs      |  2 +-
 .../src/grammar/ty/parse_impls.rs             | 19 +------
 6 files changed, 80 insertions(+), 33 deletions(-)
 create mode 100644 crates/formality-macros/src/precedence.rs

diff --git a/crates/formality-macros/src/attrs.rs b/crates/formality-macros/src/attrs.rs
index 6bf2752e..557b45bd 100644
--- a/crates/formality-macros/src/attrs.rs
+++ b/crates/formality-macros/src/attrs.rs
@@ -2,7 +2,7 @@
 
 use syn::{spanned::Spanned, Attribute, DeriveInput};
 
-use crate::custom::Customize;
+use crate::{custom::Customize, precedence::Precedence};
 
 /// Checks for any kind of attribute that indicates an "is-a" relationship,
 /// e.g. `#[cast]` and `#[variable]`.
@@ -39,11 +39,23 @@ pub(crate) fn has_variable_attr(attrs: &[Attribute]) -> bool {
     attrs.iter().any(|a| a.path().is_ident("variable"))
 }
 
+/// Extract a `#[precedence]` level, defaults to 0
+pub(crate) fn precedence(attrs: &[Attribute]) -> syn::Result<Precedence> {
+    parse_attr_named(attrs, "precedence")
+}
+
 /// Extracts any customization attribute from a list of attributes.
 pub(crate) fn customize(attrs: &[Attribute]) -> syn::Result<Customize> {
-    let mut v: Vec<Customize> = attrs
+    parse_attr_named(attrs, "customize")
+}
+
+fn parse_attr_named<T>(attrs: &[Attribute], name: &str) -> syn::Result<T>
+where
+    T: Default + syn::parse::Parse,
+{
+    let mut v: Vec<T> = attrs
         .iter()
-        .filter(|a| a.path().is_ident("customize"))
+        .filter(|a| a.path().is_ident(name))
         .map(|a| a.parse_args())
         .collect::<syn::Result<_>>()?;
 
@@ -51,18 +63,18 @@ pub(crate) fn customize(attrs: &[Attribute]) -> syn::Result<Customize> {
         Err(syn::Error::new(
             attrs
                 .iter()
-                .filter(|a| a.path().is_ident("customize"))
+                .filter(|a| a.path().is_ident(name))
                 .skip(1)
                 .next()
                 .unwrap()
                 .path()
                 .span(),
-            "multiple customize attributes",
+            format!("multiple `{}` attributes", name),
         ))
     } else if v.len() == 1 {
         Ok(v.pop().unwrap())
     } else {
-        Ok(Customize::default())
+        Ok(T::default())
     }
 }
 
@@ -82,5 +94,6 @@ fn remove_formality_attributes_from_vec(attrs: &mut Vec<Attribute>) {
             && !attr.path().is_ident("cast")
             && !attr.path().is_ident("variable")
             && !attr.path().is_ident("customize")
+            && !attr.path().is_ident("precedence")
     });
 }
diff --git a/crates/formality-macros/src/lib.rs b/crates/formality-macros/src/lib.rs
index c7a36d00..ccce2a5d 100644
--- a/crates/formality-macros/src/lib.rs
+++ b/crates/formality-macros/src/lib.rs
@@ -12,6 +12,7 @@ mod debug;
 mod fixed_point;
 mod fold;
 mod parse;
+mod precedence;
 mod spec;
 mod term;
 mod test;
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index 5b392a34..bd05ac29 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -1,4 +1,5 @@
 extern crate proc_macro;
+
 use convert_case::{Case, Casing};
 use proc_macro2::{Ident, Literal, TokenStream};
 use quote::{quote, quote_spanned};
@@ -6,7 +7,7 @@ use syn::{spanned::Spanned, Attribute};
 use synstructure::BindingInfo;
 
 use crate::{
-    attrs::{has_cast_attr, has_variable_attr},
+    attrs::{has_cast_attr, has_variable_attr, precedence},
     spec::{self, FieldMode, FormalitySpec},
 };
 
@@ -40,13 +41,11 @@ pub(crate) fn derive_parse_with_spec(
     for variant in s.variants() {
         let variant_name = as_literal(variant.ast().ident);
         let v = parse_variant(variant, external_spec)?;
-        parse_variants.extend(quote! {
-            {
-                let __span = tracing::span!(tracing::Level::TRACE, "parse", variant_name = #variant_name);
-                let __guard = __span.enter();
-                __parser.parse_variant(#variant_name, 0, |__p| { #v });
-            }
-        });
+        let precedence = precedence(&variant.ast().attrs)?.literal();
+        parse_variants.extend(quote_spanned!(
+            variant.ast().ident.span() =>
+            __parser.parse_variant(#variant_name, #precedence, |__p| { #v });
+        ));
     }
 
     let type_name: Literal = as_literal(&s.ast().ident);
diff --git a/crates/formality-macros/src/precedence.rs b/crates/formality-macros/src/precedence.rs
new file mode 100644
index 00000000..4eee2f66
--- /dev/null
+++ b/crates/formality-macros/src/precedence.rs
@@ -0,0 +1,51 @@
+use std::str::FromStr;
+
+use proc_macro2::{Literal, TokenStream};
+use syn::spanned::Spanned;
+
+#[derive(Default, Debug)]
+pub(crate) struct Precedence {
+    pub level: usize,
+}
+
+impl Precedence {
+    pub fn literal(&self) -> Literal {
+        Literal::usize_unsuffixed(self.level)
+    }
+}
+
+impl syn::parse::Parse for Precedence {
+    fn parse(input: syn::parse::ParseStream) -> syn::Result<Self> {
+        let token_stream: TokenStream = input.parse()?;
+        let span = token_stream.span();
+        let mut tokens = token_stream.into_iter();
+
+        let Some(token) = tokens.next() else {
+            return Err(syn::Error::new(span, "precedence expected"));
+        };
+
+        let level;
+        match token {
+            proc_macro2::TokenTree::Literal(l) => {
+                let l_str = l.to_string();
+                match usize::from_str(&l_str) {
+                    Ok(l) => level = l,
+                    Err(_) => return Err(syn::Error::new(l.span(), "integer precedence expected")),
+                }
+            }
+
+            _ => {
+                return Err(syn::Error::new(
+                    token.span(),
+                    "unexpected token in precedence",
+                ));
+            }
+        }
+
+        if let Some(token) = tokens.next() {
+            return Err(syn::Error::new(token.span(), "extra tokens"));
+        }
+
+        Ok(Precedence { level })
+    }
+}
diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index 0346a1cc..e8241a38 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -99,7 +99,6 @@ impl DowncastTo<TyData> for Ty {
 // NB: TyData doesn't implement Fold; you fold types, not TyData,
 // because variables might not map to the same variant.
 #[term]
-#[customize(parse)]
 pub enum TyData {
     #[cast]
     RigidTy(RigidTy),
@@ -108,6 +107,7 @@ pub enum TyData {
     #[cast]
     PredicateTy(PredicateTy),
     #[variable]
+    #[precedence(1)]
     Variable(Variable),
 }
 
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index e5738f2d..3ea08abc 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -6,27 +6,10 @@ use formality_core::{seq, Set};
 
 use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
 
-use super::{
-    AliasTy, AssociatedTyName, Lt, LtData, Parameter, PredicateTy, RigidTy, ScalarId, Ty, TyData,
-};
+use super::{AliasTy, AssociatedTyName, Lt, LtData, Parameter, RigidTy, ScalarId, Ty};
 
 use crate::rust::FormalityLang as Rust;
 
-// ANCHOR: ty_parse_impl
-// For types, we invest some effort into parsing them decently because it makes
-// writing tests so much more pleasant.
-impl CoreParse<Rust> for TyData {
-    fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
-        let mut parser = Parser::new(scope, text0, "Ty");
-        parser.parse_variant("Variable", 1, |p| p.variable());
-        parser.parse_variant_cast::<RigidTy>(0);
-        parser.parse_variant_cast::<AliasTy>(0);
-        parser.parse_variant_cast::<PredicateTy>(0);
-        parser.finish()
-    }
-}
-// ANCHOR_END: ty_parse_impl
-
 impl CoreParse<Rust> for RigidTy {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
         let mut parser: Parser<'_, '_, RigidTy, Rust> = Parser::new(scope, text, "AliasTy");

From 1d9440391d8ba42b9369f6d99dc0d45833373542 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 14:00:53 -0400
Subject: [PATCH 16/22] make Lt use `#[term]`

---
 crates/formality-types/src/grammar/ty.rs      | 22 ++-----
 .../src/grammar/ty/debug_impls.rs             |  9 ---
 .../src/grammar/ty/parse_impls.rs             | 14 +----
 .../src/grammar/ty/term_impls.rs              | 60 +------------------
 4 files changed, 8 insertions(+), 97 deletions(-)

diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index e8241a38..0033e7c2 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -281,7 +281,8 @@ pub enum Variance {
     Invariant,
 }
 
-#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[term]
+#[cast]
 pub struct Lt {
     data: Arc<LtData>,
 }
@@ -321,22 +322,12 @@ impl DowncastTo<LtData> for Lt {
     }
 }
 
-impl UpcastFrom<LtData> for Parameter {
-    fn upcast_from(v: LtData) -> Self {
-        Lt::new(v).upcast()
-    }
-}
-
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[term]
 pub enum LtData {
     Static,
-    Variable(Variable),
-}
 
-impl UpcastFrom<LtData> for LtData {
-    fn upcast_from(term: LtData) -> Self {
-        term
-    }
+    #[variable]
+    Variable(Variable),
 }
 
 impl UpcastFrom<Variable> for Parameter {
@@ -375,11 +366,10 @@ cast_impl!((BoundVar) <: (Variable) <: (Ty));
 cast_impl!((UniversalVar) <: (Variable) <: (Parameter));
 cast_impl!((ExistentialVar) <: (Variable) <: (Parameter));
 cast_impl!((BoundVar) <: (Variable) <: (Parameter));
-cast_impl!(Lt);
-cast_impl!(LtData::Variable(Variable));
 cast_impl!((ExistentialVar) <: (Variable) <: (LtData));
 cast_impl!((UniversalVar) <: (Variable) <: (LtData));
 cast_impl!((BoundVar) <: (Variable) <: (LtData));
 cast_impl!((UniversalVar) <: (LtData) <: (Lt));
 cast_impl!((ExistentialVar) <: (LtData) <: (Lt));
 cast_impl!((BoundVar) <: (LtData) <: (Lt));
+cast_impl!((LtData) <: (Lt) <: (Parameter));
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index 793fd776..db523c69 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -8,12 +8,3 @@ impl std::fmt::Debug for Const {
         }
     }
 }
-
-impl std::fmt::Debug for super::Lt {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self.data() {
-            super::LtData::Static => write!(f, "static"),
-            super::LtData::Variable(v) => write!(f, "{:?}", v),
-        }
-    }
-}
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index 3ea08abc..619fa0da 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -6,7 +6,7 @@ use formality_core::{seq, Set};
 
 use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
 
-use super::{AliasTy, AssociatedTyName, Lt, LtData, Parameter, RigidTy, ScalarId, Ty};
+use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
 
 use crate::rust::FormalityLang as Rust;
 
@@ -104,18 +104,6 @@ fn parse_parameters<'t>(
     Ok(parameters)
 }
 
-impl CoreParse<Rust> for Lt {
-    fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
-        let mut parser = Parser::new(scope, text0, "Lt");
-        parser.parse_variant("static", 0, |p| {
-            p.expect_keyword("static")?;
-            Ok(Lt::new(LtData::Static))
-        });
-        parser.parse_variant("variable", 0, |p| p.variable());
-        parser.finish()
-    }
-}
-
 // For consts, we invest some effort into parsing them decently because it makes
 // writing tests so much more pleasant.
 impl CoreParse<Rust> for Const {
diff --git a/crates/formality-types/src/grammar/ty/term_impls.rs b/crates/formality-types/src/grammar/ty/term_impls.rs
index a336bdf0..6ca915b1 100644
--- a/crates/formality-types/src/grammar/ty/term_impls.rs
+++ b/crates/formality-types/src/grammar/ty/term_impls.rs
@@ -1,43 +1,12 @@
-use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, ValTree};
-use crate::rust::Variable;
+use crate::grammar::{Const, ConstData, Parameter, ValTree};
 use crate::FormalityLang;
 use formality_core::{
     fold::{CoreFold, SubstitutionFn},
     language::CoreKind,
-    visit::CoreVisit,
 };
 
 use super::ParameterKind;
 
-impl CoreVisit<FormalityLang> for LtData {
-    fn free_variables(&self) -> Vec<Variable> {
-        match self {
-            LtData::Variable(v) => {
-                if v.is_free() {
-                    vec![*v]
-                } else {
-                    vec![]
-                }
-            }
-            LtData::Static => vec![],
-        }
-    }
-
-    fn size(&self) -> usize {
-        match self {
-            LtData::Variable(v) => v.size(),
-            LtData::Static => 1,
-        }
-    }
-
-    fn assert_valid(&self) {
-        match self {
-            LtData::Variable(v) => v.assert_valid(),
-            LtData::Static => (),
-        }
-    }
-}
-
 impl formality_core::language::HasKind<FormalityLang> for Parameter {
     fn kind(&self) -> CoreKind<FormalityLang> {
         match self {
@@ -69,30 +38,3 @@ impl CoreFold<FormalityLang> for ValTree {
         self.clone()
     }
 }
-
-impl CoreFold<FormalityLang> for Lt {
-    fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
-        match self.data() {
-            LtData::Static => self.clone(),
-            LtData::Variable(v) => match substitution_fn(*v) {
-                None => self.clone(),
-                Some(Parameter::Lt(t)) => t,
-                Some(param) => panic!("ill-kinded substitute: expected lifetime, got {param:?}"),
-            },
-        }
-    }
-}
-
-impl CoreVisit<FormalityLang> for Lt {
-    fn free_variables(&self) -> Vec<Variable> {
-        self.data().free_variables()
-    }
-
-    fn size(&self) -> usize {
-        self.data().size()
-    }
-
-    fn assert_valid(&self) {
-        self.data().assert_valid()
-    }
-}

From 394ba0cc215a4e273baf8211567b797daf049b49 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 14:10:10 -0400
Subject: [PATCH 17/22] use `#[term]` for Const

---
 crates/formality-types/src/grammar/consts.rs  | 28 ++++++++---------
 .../src/grammar/ty/debug_impls.rs             |  9 ------
 .../src/grammar/ty/parse_impls.rs             | 31 ++++++++++---------
 .../src/grammar/ty/term_impls.rs              | 16 ----------
 tests/ui/consts/mismatch.stderr               |  4 +--
 .../consts/nonsense_rigid_const_bound.stderr  |  4 +--
 6 files changed, 34 insertions(+), 58 deletions(-)

diff --git a/crates/formality-types/src/grammar/consts.rs b/crates/formality-types/src/grammar/consts.rs
index 980c2058..496ea76f 100644
--- a/crates/formality-types/src/grammar/consts.rs
+++ b/crates/formality-types/src/grammar/consts.rs
@@ -1,11 +1,12 @@
 mod valtree;
 
 use super::{Parameter, Ty, Variable};
-use formality_core::{term, DowncastTo, Upcast, UpcastFrom, Visit};
+use formality_core::{term, DowncastTo, Upcast, UpcastFrom};
 use std::sync::Arc;
 pub use valtree::*;
 
-#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+#[term]
+#[cast]
 pub struct Const {
     data: Arc<ConstData>,
 }
@@ -39,16 +40,14 @@ impl Const {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+#[term]
+#[customize(parse)]
 pub enum ConstData {
     Value(ValTree, Ty),
-    Variable(Variable),
-}
 
-impl UpcastFrom<Self> for ConstData {
-    fn upcast_from(term: Self) -> Self {
-        term
-    }
+    #[variable]
+    #[precedence(1)]
+    Variable(Variable),
 }
 
 impl DowncastTo<ConstData> for Const {
@@ -81,15 +80,16 @@ pub enum Bool {
     False,
 }
 
-impl UpcastFrom<Bool> for Const {
+impl UpcastFrom<Bool> for ConstData {
     fn upcast_from(term: Bool) -> Self {
-        Self::new(ConstData::Value(term.upcast(), Ty::bool()))
+        ConstData::Value(term.upcast(), Ty::bool())
     }
 }
 
-impl UpcastFrom<Variable> for ConstData {
-    fn upcast_from(v: Variable) -> Self {
-        Self::Variable(v)
+impl UpcastFrom<Bool> for Const {
+    fn upcast_from(term: Bool) -> Self {
+        let c: ConstData = term.upcast();
+        Const::new(c)
     }
 }
 
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index db523c69..8b137891 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -1,10 +1 @@
-use crate::grammar::Const;
 
-impl std::fmt::Debug for Const {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self.data() {
-            crate::grammar::ConstData::Value(valtree, ty) => write!(f, "{valtree:?}_{ty:?}"),
-            crate::grammar::ConstData::Variable(r) => write!(f, "{r:?}"),
-        }
-    }
-}
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index 619fa0da..fd5f7fe1 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -4,7 +4,9 @@ use formality_core::parse::{ActiveVariant, CoreParse, ParseError, ParseResult, P
 use formality_core::Upcast;
 use formality_core::{seq, Set};
 
-use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
+use crate::grammar::{
+    AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId, ValTree,
+};
 
 use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
 
@@ -106,22 +108,21 @@ fn parse_parameters<'t>(
 
 // For consts, we invest some effort into parsing them decently because it makes
 // writing tests so much more pleasant.
-impl CoreParse<Rust> for Const {
+impl CoreParse<Rust> for ConstData {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
-        let mut parser: Parser<'_, '_, Const, Rust> = Parser::new(scope, text, "Ty");
-        parser.parse_variant_cast::<Bool>(1);
+        let mut parser: Parser<'_, '_, ConstData, Rust> = Parser::new(scope, text, "Ty");
+
         parser.parse_variant("Variable", 1, |p| p.variable());
-        parser.parse_variant("Int", 0, |p| p.nonterminal_with(parse_int));
+
+        parser.parse_variant_cast::<Bool>(1);
+
+        parser.parse_variant("Int", 0, |p| {
+            let n: u128 = p.number()?;
+            p.expect_char('_')?;
+            let ty: Ty = p.nonterminal()?;
+            Ok(ConstData::Value(Scalar::new(n).upcast(), ty))
+        });
+
         parser.finish()
     }
 }
-
-#[tracing::instrument(level = "trace", ret)]
-fn parse_int<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Const> {
-    Parser::single_variant(scope, text, "Ty", |p| {
-        let n: u128 = p.number()?;
-        p.expect_char('_')?;
-        let ty: Ty = p.nonterminal()?;
-        Ok(Const::valtree(Scalar::new(n), ty))
-    })
-}
diff --git a/crates/formality-types/src/grammar/ty/term_impls.rs b/crates/formality-types/src/grammar/ty/term_impls.rs
index 6ca915b1..a402a749 100644
--- a/crates/formality-types/src/grammar/ty/term_impls.rs
+++ b/crates/formality-types/src/grammar/ty/term_impls.rs
@@ -17,22 +17,6 @@ impl formality_core::language::HasKind<FormalityLang> for Parameter {
     }
 }
 
-impl CoreFold<FormalityLang> for Const {
-    fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
-        match self.data() {
-            ConstData::Value(v, ty) => Self::valtree(
-                v.substitute(substitution_fn),
-                ty.substitute(substitution_fn),
-            ),
-            ConstData::Variable(v) => match substitution_fn(*v) {
-                None => self.clone(),
-                Some(Parameter::Const(c)) => c,
-                Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"),
-            },
-        }
-    }
-}
-
 impl CoreFold<FormalityLang> for ValTree {
     fn substitute(&self, _substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
         self.clone()
diff --git a/tests/ui/consts/mismatch.stderr b/tests/ui/consts/mismatch.stderr
index 69c341ce..583b5210 100644
--- a/tests/ui/consts/mismatch.stderr
+++ b/tests/ui/consts/mismatch.stderr
@@ -1,4 +1,4 @@
-Error: check_trait_impl(impl <> Foo < const 42_(rigid (scalar u32)) > for (rigid (scalar u32)) where [] { })
+Error: check_trait_impl(impl <> Foo < const value(42, (rigid (scalar u32))) > for (rigid (scalar u32)) where [] { })
 
 Caused by:
-    failed to prove {Foo((rigid (scalar u32)), const 42_(rigid (scalar u32)))} given {}, got {}
+    failed to prove {Foo((rigid (scalar u32)), const value(42, (rigid (scalar u32))))} given {}, got {}
diff --git a/tests/ui/consts/nonsense_rigid_const_bound.stderr b/tests/ui/consts/nonsense_rigid_const_bound.stderr
index 88252b25..7ac9f1c1 100644
--- a/tests/ui/consts/nonsense_rigid_const_bound.stderr
+++ b/tests/ui/consts/nonsense_rigid_const_bound.stderr
@@ -1,5 +1,5 @@
 Error: check_trait(Foo)
 
 Caused by:
-    0: prove_where_clause_well_formed(type_of_const 0_(rigid (scalar bool)) is (rigid (scalar u32)))
-    1: failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(0_(rigid (scalar bool)) , (rigid (scalar u32)))}, got {}
+    0: prove_where_clause_well_formed(type_of_const value(0, (rigid (scalar bool))) is (rigid (scalar u32)))
+    1: failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(value(0, (rigid (scalar bool))) , (rigid (scalar u32)))}, got {}

From c151b287dd7ea8edb0c2f563ac9ba7d4abe9b785 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 14:14:55 -0400
Subject: [PATCH 18/22] customize debug impl for assoc ty

could be better
---
 crates/formality-types/src/grammar/ty.rs      |  2 +-
 .../src/grammar/ty/debug_impls.rs             | 23 +++++++++++++++++++
 tests/associated_type_normalization.rs        |  2 +-
 tests/coherence_overlap.rs                    | 18 ++++++++-------
 tests/projection.rs                           | 14 +++++------
 .../ui/coherence_orphan/alias_to_unit.stderr  |  4 ++--
 .../coherence_orphan/mirror_CoreStruct.stderr |  4 ++--
 7 files changed, 46 insertions(+), 21 deletions(-)

diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index 0033e7c2..32f7dbd6 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -188,7 +188,7 @@ pub enum ScalarId {
 }
 
 #[term((alias $name $*parameters))]
-#[customize(parse)]
+#[customize(parse, debug)]
 pub struct AliasTy {
     pub name: AliasName,
     pub parameters: Parameters,
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index 8b137891..0e252b75 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -1 +1,24 @@
+use super::{AliasName, AliasTy, AssociatedTyName};
+use std::fmt::Debug;
 
+impl Debug for AliasTy {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let AliasTy { name, parameters } = self;
+        match name {
+            AliasName::AssociatedTyId(AssociatedTyName { trait_id, item_id }) => {
+                // Grr, wish we would remember the number of parameters assigned to each position.
+                write!(
+                    f,
+                    "({:?}::{:?})<{}>",
+                    trait_id,
+                    item_id,
+                    parameters
+                        .iter()
+                        .map(|p| format!("{p:?}"))
+                        .collect::<Vec<String>>()
+                        .join(","),
+                )
+            }
+        }
+    }
+}
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
index 030ef19f..83630d5b 100644
--- a/tests/associated_type_normalization.rs
+++ b/tests/associated_type_normalization.rs
@@ -39,7 +39,7 @@ fn test_mirror_normalizes_u32_to_u32() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (alias (Mirror :: Assoc) (rigid (scalar u32))),
+                        ?ty_1 => (Mirror::Assoc)<(rigid (scalar u32))>,
                     },
                 },
             },
diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs
index 0efb4db8..89a51553 100644
--- a/tests/coherence_overlap.rs
+++ b/tests/coherence_overlap.rs
@@ -51,10 +51,11 @@ fn test_overlap_normalize_alias_to_LocalType() {
     // ...but it's an error if LocalType implements Iterator (figuring *this* out also
     // requires normalizing).
 
-    expect_test::expect![[r#"Err(
-    "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (alias (Mirror :: T) (rigid (adt LocalType))) where [] { }",
-)
-"#]]
+    expect_test::expect![[r#"
+        Err(
+            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (Mirror::T)<(rigid (adt LocalType))> where [] { }",
+        )
+    "#]]
     .assert_debug_eq(&test_program_ok(&gen_program(
         "impl<> Iterator<> for LocalType<> where [] {}",
     )));
@@ -111,10 +112,11 @@ fn test_overlap_alias_not_normalizable() {
 
     // ...as long as there is at least one Iterator impl, however, we do flag an error.
 
-    expect_test::expect![[r#"Err(
-    "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <ty> LocalTrait < > for (alias (Mirror :: T) ^ty0_0) where [^ty0_0 : Mirror < >] { }",
-)
-"#]] // FIXME
+    expect_test::expect![[r#"
+        Err(
+            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <ty> LocalTrait < > for (Mirror::T)<^ty0_0> where [^ty0_0 : Mirror < >] { }",
+        )
+    "#]] // FIXME
     .assert_debug_eq(&test_program_ok(&gen_program(
         "impl<> Iterator<> for u32 where[] {}",
     )));
diff --git a/tests/projection.rs b/tests/projection.rs
index 9ad30cea..1e6ec246 100644
--- a/tests/projection.rs
+++ b/tests/projection.rs
@@ -31,7 +31,7 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (alias (Iterator :: Item) (rigid (adt Vec) !ty_1)),
+                        ?ty_2 => (Iterator::Item)<(rigid (adt Vec) !ty_1)>,
                     },
                 },
                 Constraints {
@@ -110,7 +110,7 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (alias (Iterator :: Item) !ty_1),
+                        ?ty_2 => (Iterator::Item)<!ty_1>,
                     },
                 },
             },
@@ -169,8 +169,8 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (rigid (adt Vec) (alias (Iterator :: Item) !ty_1)),
-                        ?ty_3 => (alias (Iterator :: Item) !ty_1),
+                        ?ty_2 => (rigid (adt Vec) (Iterator::Item)<!ty_1>),
+                        ?ty_3 => (Iterator::Item)<!ty_1>,
                     },
                 },
             },
@@ -221,7 +221,7 @@ fn normalize_into_iterator() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (alias (IntoIterator :: Item) (rigid (adt Vec) !ty_1)),
+                        ?ty_2 => (IntoIterator::Item)<(rigid (adt Vec) !ty_1)>,
                     },
                 },
                 Constraints {
@@ -286,7 +286,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (alias (Trait1 :: Type) (rigid (adt S))),
+                        ?ty_1 => (Trait1::Type)<(rigid (adt S))>,
                     },
                 },
             },
@@ -321,7 +321,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (alias (Trait1 :: Type) (rigid (adt S))),
+                        ?ty_1 => (Trait1::Type)<(rigid (adt S))>,
                     },
                 },
             },
diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr
index b9ea4d12..da542fa3 100644
--- a/tests/ui/coherence_orphan/alias_to_unit.stderr
+++ b/tests/ui/coherence_orphan/alias_to_unit.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (alias (Unit :: Assoc) (rigid (adt FooStruct))) where [] { })
+Error: orphan_check(impl <> CoreTrait < > for (Unit::Assoc)<(rigid (adt FooStruct))> where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((alias (Unit :: Assoc) (rigid (adt FooStruct)))))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait((Unit::Assoc)<(rigid (adt FooStruct))>))} given {}, got {}
diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
index 7181c4b6..c9a365b5 100644
--- a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
+++ b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (alias (Mirror :: Assoc) (rigid (adt CoreStruct))) where [] { })
+Error: orphan_check(impl <> CoreTrait < > for (Mirror::Assoc)<(rigid (adt CoreStruct))> where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((alias (Mirror :: Assoc) (rigid (adt CoreStruct)))))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait((Mirror::Assoc)<(rigid (adt CoreStruct))>))} given {}, got {}

From 06437089161163a6a3ceadf9e7329354f7c5bc0c Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 14:27:17 -0400
Subject: [PATCH 19/22] pretty print rigid types

---
 .../src/prove/minimize/test.rs                |  2 +-
 .../src/test/eq_assumptions.rs                |  4 +-
 .../src/test/exists_constraints.rs            |  2 +-
 .../formality-prove/src/test/occurs_check.rs  |  4 +-
 crates/formality-types/src/grammar/ty.rs      |  2 +-
 .../src/grammar/ty/debug_impls.rs             | 79 +++++++++++++++++--
 .../src/grammar/ty/parse_impls.rs             |  2 +-
 .../src/grammar/ty/term_impls.rs              |  2 +-
 tests/associated_type_normalization.rs        |  4 +-
 tests/coherence_overlap.rs                    |  2 +-
 tests/projection.rs                           | 14 ++--
 tests/ui/basic_where_clauses_fail.stderr      |  6 +-
 .../CoreTrait_for_CoreStruct_in_Foo.stderr    |  4 +-
 .../ui/coherence_orphan/alias_to_unit.stderr  |  4 +-
 .../coherence_orphan/mirror_CoreStruct.stderr |  4 +-
 ...neg_CoreTrait_for_CoreStruct_in_Foo.stderr |  4 +-
 tests/ui/coherence_orphan/uncovered_T.stderr  |  4 +-
 .../T_where_Foo_not_u32_impls.stderr          |  2 +-
 ..._CoreStruct_does_not_impl_CoreTrait.stderr |  2 +-
 tests/ui/coherence_overlap/u32_T_impls.stderr |  2 +-
 .../u32_T_where_T_Is_impls.stderr             |  2 +-
 .../u32_not_u32_impls.stderr                  |  4 +-
 .../ui/coherence_overlap/u32_u32_impls.stderr |  2 +-
 tests/ui/consts/generic_mismatch.stderr       |  4 +-
 tests/ui/consts/mismatch.stderr               |  4 +-
 .../consts/nonsense_rigid_const_bound.stderr  |  4 +-
 tests/ui/fn/lifetime.stderr                   |  2 +-
 27 files changed, 118 insertions(+), 53 deletions(-)

diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs
index f8acdf00..6242d8a2 100644
--- a/crates/formality-prove/src/prove/minimize/test.rs
+++ b/crates/formality-prove/src/prove/minimize/test.rs
@@ -83,7 +83,7 @@ fn minimize_a() {
             },
             known_true: true,
             substitution: {
-                ?ty_1 => (rigid (scalar u32)),
+                ?ty_1 => u32,
                 ?ty_3 => ?ty_4,
             },
         }
diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs
index 87bd887e..306aa666 100644
--- a/crates/formality-prove/src/test/eq_assumptions.rs
+++ b/crates/formality-prove/src/test/eq_assumptions.rs
@@ -45,8 +45,8 @@ fn test_b() {
                 },
                 known_true: true,
                 substitution: {
-                    ?ty_1 => (rigid (adt Vec) (rigid (scalar u32))),
-                    ?ty_2 => (rigid (scalar u32)),
+                    ?ty_1 => Vec<u32>,
+                    ?ty_2 => u32,
                 },
             },
         }
diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs
index 34ccb5b9..5b91f0dd 100644
--- a/crates/formality-prove/src/test/exists_constraints.rs
+++ b/crates/formality-prove/src/test/exists_constraints.rs
@@ -31,7 +31,7 @@ fn exists_u_for_t() {
                 },
                 known_true: true,
                 substitution: {
-                    ?ty_1 => (rigid (adt Vec) ?ty_2),
+                    ?ty_1 => Vec<?ty_2>,
                 },
             },
         }
diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs
index 874d9d51..9b9bfaef 100644
--- a/crates/formality-prove/src/test/occurs_check.rs
+++ b/crates/formality-prove/src/test/occurs_check.rs
@@ -42,7 +42,7 @@ fn eq_variable_to_rigid() {
                 },
                 known_true: true,
                 substitution: {
-                    ?ty_1 => (rigid (adt Vec) ?ty_3),
+                    ?ty_1 => Vec<?ty_3>,
                     ?ty_2 => ?ty_3,
                 },
             },
@@ -68,7 +68,7 @@ fn eq_rigid_to_variable() {
                 },
                 known_true: true,
                 substitution: {
-                    ?ty_1 => (rigid (adt Vec) ?ty_3),
+                    ?ty_1 => Vec<?ty_3>,
                     ?ty_2 => ?ty_3,
                 },
             },
diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index 32f7dbd6..ef306ee0 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -118,7 +118,7 @@ impl UpcastFrom<Ty> for TyData {
 }
 
 #[term((rigid $name $*parameters))]
-#[customize(parse)]
+#[customize(parse, debug)]
 pub struct RigidTy {
     pub name: RigidName,
     pub parameters: Parameters,
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index 0e252b75..551b11a2 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -1,6 +1,48 @@
-use super::{AliasName, AliasTy, AssociatedTyName};
+use super::{AliasName, AliasTy, AssociatedTyName, Parameter, RefKind, RigidName, RigidTy};
 use std::fmt::Debug;
 
+impl Debug for RigidTy {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let RigidTy { name, parameters } = self;
+        match name {
+            RigidName::AdtId(name) => {
+                write!(
+                    f,
+                    "{:?}{:?}",
+                    name,
+                    PrettyParameters::new("<", ">", parameters)
+                )
+            }
+            RigidName::ScalarId(s) if parameters.is_empty() => {
+                write!(f, "{:?}", s)
+            }
+            RigidName::Ref(RefKind::Shared) if parameters.len() == 2 => {
+                write!(f, "&{:?} {:?}", parameters[0], parameters[1])
+            }
+            RigidName::Ref(RefKind::Mut) if parameters.len() == 2 => {
+                write!(f, "&mut {:?} {:?}", parameters[0], parameters[1])
+            }
+            RigidName::Tuple(arity) if parameters.len() == *arity => {
+                if *arity != 0 {
+                    write!(f, "{:?}", PrettyParameters::new("(", ")", parameters))
+                } else {
+                    // PrettyParameters would skip the separators
+                    // for 0 arity
+                    write!(f, "()")
+                }
+            }
+            _ => {
+                write!(
+                    f,
+                    "{:?}{:?}",
+                    name,
+                    PrettyParameters::new("<", ">", parameters)
+                )
+            }
+        }
+    }
+}
+
 impl Debug for AliasTy {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let AliasTy { name, parameters } = self;
@@ -9,16 +51,39 @@ impl Debug for AliasTy {
                 // Grr, wish we would remember the number of parameters assigned to each position.
                 write!(
                     f,
-                    "({:?}::{:?})<{}>",
+                    "({:?}::{:?}){:?}",
                     trait_id,
                     item_id,
-                    parameters
-                        .iter()
-                        .map(|p| format!("{p:?}"))
-                        .collect::<Vec<String>>()
-                        .join(","),
+                    PrettyParameters::new("<", ">", parameters),
                 )
             }
         }
     }
 }
+
+struct PrettyParameters<'a> {
+    open: &'a str,
+    close: &'a str,
+    p: &'a [Parameter],
+}
+impl<'a> PrettyParameters<'a> {
+    fn new(open: &'a str, close: &'a str, p: &'a [Parameter]) -> Self {
+        Self { open, close, p }
+    }
+}
+
+impl Debug for PrettyParameters<'_> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        if self.p.len() == 0 {
+            Ok(())
+        } else {
+            write!(f, "{}", self.open)?;
+            write!(f, "{:?}", self.p[0])?;
+            for p in &self.p[1..] {
+                write!(f, ", {:?}", p)?;
+            }
+            write!(f, "{}", self.close)?;
+            Ok(())
+        }
+    }
+}
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index fd5f7fe1..26bb8046 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -5,7 +5,7 @@ use formality_core::Upcast;
 use formality_core::{seq, Set};
 
 use crate::grammar::{
-    AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId, ValTree,
+    AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId,
 };
 
 use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
diff --git a/crates/formality-types/src/grammar/ty/term_impls.rs b/crates/formality-types/src/grammar/ty/term_impls.rs
index a402a749..c51e09a4 100644
--- a/crates/formality-types/src/grammar/ty/term_impls.rs
+++ b/crates/formality-types/src/grammar/ty/term_impls.rs
@@ -1,4 +1,4 @@
-use crate::grammar::{Const, ConstData, Parameter, ValTree};
+use crate::grammar::{Parameter, ValTree};
 use crate::FormalityLang;
 use formality_core::{
     fold::{CoreFold, SubstitutionFn},
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
index 83630d5b..bcb3b0f0 100644
--- a/tests/associated_type_normalization.rs
+++ b/tests/associated_type_normalization.rs
@@ -27,7 +27,7 @@ fn test_mirror_normalizes_u32_to_u32() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (rigid (scalar u32)),
+                        ?ty_1 => u32,
                     },
                 },
                 Constraints {
@@ -39,7 +39,7 @@ fn test_mirror_normalizes_u32_to_u32() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (Mirror::Assoc)<(rigid (scalar u32))>,
+                        ?ty_1 => (Mirror::Assoc)<u32>,
                     },
                 },
             },
diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs
index 89a51553..de28289b 100644
--- a/tests/coherence_overlap.rs
+++ b/tests/coherence_overlap.rs
@@ -53,7 +53,7 @@ fn test_overlap_normalize_alias_to_LocalType() {
 
     expect_test::expect![[r#"
         Err(
-            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (Mirror::T)<(rigid (adt LocalType))> where [] { }",
+            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (Mirror::T)<LocalType> where [] { }",
         )
     "#]]
     .assert_debug_eq(&test_program_ok(&gen_program(
diff --git a/tests/projection.rs b/tests/projection.rs
index 1e6ec246..1302408b 100644
--- a/tests/projection.rs
+++ b/tests/projection.rs
@@ -31,7 +31,7 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (Iterator::Item)<(rigid (adt Vec) !ty_1)>,
+                        ?ty_2 => (Iterator::Item)<Vec<!ty_1>>,
                     },
                 },
                 Constraints {
@@ -169,7 +169,7 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (rigid (adt Vec) (Iterator::Item)<!ty_1>),
+                        ?ty_2 => Vec<(Iterator::Item)<!ty_1>>,
                         ?ty_3 => (Iterator::Item)<!ty_1>,
                     },
                 },
@@ -221,7 +221,7 @@ fn normalize_into_iterator() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (IntoIterator::Item)<(rigid (adt Vec) !ty_1)>,
+                        ?ty_2 => (IntoIterator::Item)<Vec<!ty_1>>,
                     },
                 },
                 Constraints {
@@ -274,7 +274,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (rigid (scalar u32)),
+                        ?ty_1 => u32,
                     },
                 },
                 Constraints {
@@ -286,7 +286,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (Trait1::Type)<(rigid (adt S))>,
+                        ?ty_1 => (Trait1::Type)<S>,
                     },
                 },
             },
@@ -309,7 +309,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (rigid (scalar u32)),
+                        ?ty_1 => u32,
                     },
                 },
                 Constraints {
@@ -321,7 +321,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (Trait1::Type)<(rigid (adt S))>,
+                        ?ty_1 => (Trait1::Type)<S>,
                     },
                 },
             },
diff --git a/tests/ui/basic_where_clauses_fail.stderr b/tests/ui/basic_where_clauses_fail.stderr
index 2cd1a57f..da29e03a 100644
--- a/tests/ui/basic_where_clauses_fail.stderr
+++ b/tests/ui/basic_where_clauses_fail.stderr
@@ -1,6 +1,6 @@
 Error: check_trait(WellFormed)
 
 Caused by:
-    0: prove_where_clause_well_formed(for <ty> (rigid (scalar u32)) : A < ^ty0_0 >)
-    1: prove_where_clause_well_formed((rigid (scalar u32)) : A < !ty_2 >)
-    2: failed to prove {@ WellFormedTraitRef(A((rigid (scalar u32)), !ty_2))} given {for <ty> A((rigid (scalar u32)), ^ty0_0)}, got {}
+    0: prove_where_clause_well_formed(for <ty> u32 : A < ^ty0_0 >)
+    1: prove_where_clause_well_formed(u32 : A < !ty_2 >)
+    2: failed to prove {@ WellFormedTraitRef(A(u32, !ty_2))} given {for <ty> A(u32, ^ty0_0)}, got {}
diff --git a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr
index 37efae84..3ef3c848 100644
--- a/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr
+++ b/tests/ui/coherence_orphan/CoreTrait_for_CoreStruct_in_Foo.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (rigid (adt CoreStruct)) where [] { })
+Error: orphan_check(impl <> CoreTrait < > for CoreStruct where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait(CoreStruct))} given {}, got {}
diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr
index da542fa3..f45ed78b 100644
--- a/tests/ui/coherence_orphan/alias_to_unit.stderr
+++ b/tests/ui/coherence_orphan/alias_to_unit.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (Unit::Assoc)<(rigid (adt FooStruct))> where [] { })
+Error: orphan_check(impl <> CoreTrait < > for (Unit::Assoc)<FooStruct> where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((Unit::Assoc)<(rigid (adt FooStruct))>))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait((Unit::Assoc)<FooStruct>))} given {}, got {}
diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
index c9a365b5..48ca29db 100644
--- a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
+++ b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (Mirror::Assoc)<(rigid (adt CoreStruct))> where [] { })
+Error: orphan_check(impl <> CoreTrait < > for (Mirror::Assoc)<CoreStruct> where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((Mirror::Assoc)<(rigid (adt CoreStruct))>))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait((Mirror::Assoc)<CoreStruct>))} given {}, got {}
diff --git a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr b/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr
index 1b0f4c6e..081e8613 100644
--- a/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr
+++ b/tests/ui/coherence_orphan/neg_CoreTrait_for_CoreStruct_in_Foo.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check_neg(impl <> ! CoreTrait < > for (rigid (adt CoreStruct)) where [] {})
+Error: orphan_check_neg(impl <> ! CoreTrait < > for CoreStruct where [] {})
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((rigid (adt CoreStruct))))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait(CoreStruct))} given {}, got {}
diff --git a/tests/ui/coherence_orphan/uncovered_T.stderr b/tests/ui/coherence_orphan/uncovered_T.stderr
index a7ac7060..35cfc0fc 100644
--- a/tests/ui/coherence_orphan/uncovered_T.stderr
+++ b/tests/ui/coherence_orphan/uncovered_T.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <ty> CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { })
+Error: orphan_check(impl <ty> CoreTrait < FooStruct > for ^ty0_0 where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait(!ty_1, (rigid (adt FooStruct))))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait(!ty_1, FooStruct))} given {}, got {}
diff --git a/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr b/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr
index d4a3174c..ecbbe8ee 100644
--- a/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr
+++ b/tests/ui/coherence_overlap/T_where_Foo_not_u32_impls.stderr
@@ -16,7 +16,7 @@ Caused by:
             },
             known_true: true,
             substitution: {
-                ?ty_1 => (rigid (scalar u32)),
+                ?ty_1 => u32,
             },
         },
     }
diff --git a/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr b/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr
index cf1dd36d..280dfd6b 100644
--- a/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr
+++ b/tests/ui/coherence_overlap/foo_crate_cannot_assume_CoreStruct_does_not_impl_CoreTrait.stderr
@@ -1,3 +1,3 @@
 Error: impls may overlap:
 impl <ty> FooTrait < > for ^ty0_0 where [^ty0_0 : CoreTrait < >] { }
-impl <> FooTrait < > for (rigid (adt CoreStruct)) where [] { }
+impl <> FooTrait < > for CoreStruct where [] { }
diff --git a/tests/ui/coherence_overlap/u32_T_impls.stderr b/tests/ui/coherence_overlap/u32_T_impls.stderr
index 821e428b..83ac7c7c 100644
--- a/tests/ui/coherence_overlap/u32_T_impls.stderr
+++ b/tests/ui/coherence_overlap/u32_T_impls.stderr
@@ -1,3 +1,3 @@
 Error: impls may overlap:
-impl <> Foo < > for (rigid (scalar u32)) where [] { }
+impl <> Foo < > for u32 where [] { }
 impl <ty> Foo < > for ^ty0_0 where [] { }
diff --git a/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr b/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr
index d79b549e..b4bbfe86 100644
--- a/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr
+++ b/tests/ui/coherence_overlap/u32_T_where_T_Is_impls.stderr
@@ -1,3 +1,3 @@
 Error: impls may overlap:
-impl <> Foo < > for (rigid (scalar u32)) where [] { }
+impl <> Foo < > for u32 where [] { }
 impl <ty> Foo < > for ^ty0_0 where [^ty0_0 : Is < >] { }
diff --git a/tests/ui/coherence_overlap/u32_not_u32_impls.stderr b/tests/ui/coherence_overlap/u32_not_u32_impls.stderr
index 419a2da7..65398442 100644
--- a/tests/ui/coherence_overlap/u32_not_u32_impls.stderr
+++ b/tests/ui/coherence_overlap/u32_not_u32_impls.stderr
@@ -1,8 +1,8 @@
-Error: check_trait_impl(impl <> Foo < > for (rigid (scalar u32)) where [] { })
+Error: check_trait_impl(impl <> Foo < > for u32 where [] { })
 
 Caused by:
     failed to disprove
-        {! Foo((rigid (scalar u32)))}
+        {! Foo(u32)}
     given
         {}
     got
diff --git a/tests/ui/coherence_overlap/u32_u32_impls.stderr b/tests/ui/coherence_overlap/u32_u32_impls.stderr
index 8bcd6c9b..fb0aa5a5 100644
--- a/tests/ui/coherence_overlap/u32_u32_impls.stderr
+++ b/tests/ui/coherence_overlap/u32_u32_impls.stderr
@@ -1 +1 @@
-Error: duplicate impl in current crate: impl <> Foo < > for (rigid (scalar u32)) where [] { }
+Error: duplicate impl in current crate: impl <> Foo < > for u32 where [] { }
diff --git a/tests/ui/consts/generic_mismatch.stderr b/tests/ui/consts/generic_mismatch.stderr
index 0cf59a13..1b15792b 100644
--- a/tests/ui/consts/generic_mismatch.stderr
+++ b/tests/ui/consts/generic_mismatch.stderr
@@ -1,4 +1,4 @@
-Error: check_trait_impl(impl <const> Foo < const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar u32))] { })
+Error: check_trait_impl(impl <const> Foo < const ^const0_0 > for u32 where [type_of_const ^const0_0 is u32] { })
 
 Caused by:
-    failed to prove {Foo((rigid (scalar u32)), const !const_1)} given {@ ConstHasType(!const_1 , (rigid (scalar u32)))}, got {}
+    failed to prove {Foo(u32, const !const_1)} given {@ ConstHasType(!const_1 , u32)}, got {}
diff --git a/tests/ui/consts/mismatch.stderr b/tests/ui/consts/mismatch.stderr
index 583b5210..f1bf5189 100644
--- a/tests/ui/consts/mismatch.stderr
+++ b/tests/ui/consts/mismatch.stderr
@@ -1,4 +1,4 @@
-Error: check_trait_impl(impl <> Foo < const value(42, (rigid (scalar u32))) > for (rigid (scalar u32)) where [] { })
+Error: check_trait_impl(impl <> Foo < const value(42, u32) > for u32 where [] { })
 
 Caused by:
-    failed to prove {Foo((rigid (scalar u32)), const value(42, (rigid (scalar u32))))} given {}, got {}
+    failed to prove {Foo(u32, const value(42, u32))} given {}, got {}
diff --git a/tests/ui/consts/nonsense_rigid_const_bound.stderr b/tests/ui/consts/nonsense_rigid_const_bound.stderr
index 7ac9f1c1..a08f2649 100644
--- a/tests/ui/consts/nonsense_rigid_const_bound.stderr
+++ b/tests/ui/consts/nonsense_rigid_const_bound.stderr
@@ -1,5 +1,5 @@
 Error: check_trait(Foo)
 
 Caused by:
-    0: prove_where_clause_well_formed(type_of_const value(0, (rigid (scalar bool))) is (rigid (scalar u32)))
-    1: failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(value(0, (rigid (scalar bool))) , (rigid (scalar u32)))}, got {}
+    0: prove_where_clause_well_formed(type_of_const value(0, bool) is u32)
+    1: failed to prove {u32 = bool} given {@ ConstHasType(value(0, bool) , u32)}, got {}
diff --git a/tests/ui/fn/lifetime.stderr b/tests/ui/fn/lifetime.stderr
index 325d1878..7b143601 100644
--- a/tests/ui/fn/lifetime.stderr
+++ b/tests/ui/fn/lifetime.stderr
@@ -1 +1 @@
-Error: failed to prove {@ wf((rigid &(shared) !lt_1 !ty_2))} given {}, got {}
+Error: failed to prove {@ wf(&!lt_1 !ty_2)} given {}, got {}

From 05691de8f57bc98b686e274f34d7aa3af71d508c Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 16:14:22 -0400
Subject: [PATCH 20/22] adjust documentation to match current state

---
 book/src/SUMMARY.md                           |  5 ++-
 book/src/formality_core/debug.md              | 14 +++++++++
 book/src/formality_core/impl_fold_visit.md    | 22 -------------
 book/src/formality_core/parse.md              | 31 +++++++++++++++----
 .../src/grammar/ty/debug_impls.rs             |  2 ++
 .../src/grammar/ty/parse_impls.rs             |  8 +++++
 6 files changed, 51 insertions(+), 31 deletions(-)
 create mode 100644 book/src/formality_core/debug.md
 delete mode 100644 book/src/formality_core/impl_fold_visit.md

diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index f7e9f6da..d2ffd9a3 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -4,9 +4,8 @@
 - [`formality_core`: the Formality system](./formality_core.md)
     - [Defining your lang](./formality_core/lang.md)
     - [Defining terms with the `term` macro](./formality_core/terms.md)
-        - [Parsing reference](./formality_core/parse.md)
-        - [Implementing `Fold` and `Visit` by hand](./formality_core/impl_fold_visit.md)
-        - [Implementing `Parse` by hand](./formality_core/impl_parse.md)
+        - [Parsing](./formality_core/parse.md)
+        - [Customizing debug](./formality_core/debug.md)
     - [Variables](./formality_core/variables.md)
     - [Collections](./formality_core/collections.md)
     - [Judgment functions and inference rules](./formality_core/judgment_fn.md)
diff --git a/book/src/formality_core/debug.md b/book/src/formality_core/debug.md
new file mode 100644
index 00000000..deffcaa5
--- /dev/null
+++ b/book/src/formality_core/debug.md
@@ -0,0 +1,14 @@
+# Customizing the debug
+
+By default, the `#[term]` macro will generate a `Debug` impl that is guided by the `#[grammar]` attributes on your type (see the [parsing](./parse.md) section for more details). But sometimes you want to generate custom logic. You can include a `#[customize(debug)]` declaration to allow that. Most of the type, when you do this, you will also want to [customize parsing](./parse.md#customizing-the-parse), as the `RigidTy` does:
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty.rs:RigidTy_decl}}
+```
+
+Now you must simply implement `Debug` in the usual way. Here is the `RigidTy` declaration:
+
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty/debug_impls.rs:RigidTy_impl}}
+```
\ No newline at end of file
diff --git a/book/src/formality_core/impl_fold_visit.md b/book/src/formality_core/impl_fold_visit.md
deleted file mode 100644
index 5fede039..00000000
--- a/book/src/formality_core/impl_fold_visit.md
+++ /dev/null
@@ -1,22 +0,0 @@
-# Implementing `Fold` and `Visit` by hand
-
-The `#[term]` macro auto-generates impls of `Fold`, `Visit`, and `Parse`.
-But sometimes you don't want to use the macro.
-Sometimes you want to write your own code.
-One common reason is for substitution of a variable.
-For example, in the Rust model,
-the code that replaces type variables with types from a substitution
-is defined by a manual impl of `Fold`.
-Because `Fold` and `Visit` are trait aliases, you need to implement the underlying
-trait (`CoreFold`) by hand.
-Here is the custom impl of fold for `Ty` from `formality_types`:
-
-```rust
-{{#include ../../../crates/formality-types/src/grammar/ty/term_impls.rs:core_fold_ty}}
-```
-
-That same module contains other examples, such as impls of `CoreVisit`.
-
-## Derives
-
-You can also manually derive `Visit` and `Fold` instead of using `#[term]`.
\ No newline at end of file
diff --git a/book/src/formality_core/parse.md b/book/src/formality_core/parse.md
index c7928e13..b82f7a5f 100644
--- a/book/src/formality_core/parse.md
+++ b/book/src/formality_core/parse.md
@@ -19,9 +19,14 @@ struct MyEnum {
 }
 ```
 
-### Ambiguity,
+### Ambiguity and precedence
 
-When parsing an enum there will be multiple possibilities. We will attempt to parse them all. If more than one succeeds, the parse is deemed ambiguous and an error is reported. If zero succeed, we will report back a parsing error, attempting to localize the problem as best we can.
+When parsing an enum there will be multiple possibilities. We will attempt to parse them all. If more than one succeeds, the parser will attempt to resolve the ambiguity. Ambiguity can be resolved in two ways:
+
+* Explicit precedence: By default, every variant has precedence 0, but you can override this by annotating variants with `#[precedence(N)]` (where `N` is some integer). This will override the precedence for that variant. Variants with higher precedences are preferred.
+* Reduction prefix: When parsing, we track the list of things we had to parse. If there are two variants at the same precedence level, but one of them had to parse strictly more things than the other and in the same way, we'll prefer the longer one. So for example if one variant parsed a `Ty` and the other parsed a `Ty Ty`, we'd take the `Ty Ty`.
+
+Otherwise, the parser will panic and report ambiguity. The parser panics rather than returning an error because ambiguity doesn't mean that there is no way to parse the given text as the nonterminal -- rather that there are multiple ways. Errors mean that the text does not match the grammar for that nonterminal.
 
 ### Symbols
 
@@ -37,15 +42,12 @@ A grammar consists of a series of *symbols*. Each symbol matches some text in th
 * Nonterminals can also accept modes:
     * `$field` -- just parse the field's type
     * `$*field` -- the field must be a `Vec<T>` -- parse any number of `T` instances. Something like `[ $*field ]` would parse `[f1 f2 f3]`, assuming `f1`, `f2`, and `f3` are valid values for `field`.
-        * If the next token after `$*field` is a terminal, `$*` uses  it as lookahead. The grammar `[ $*field ]`, for example, would stop parsing once a `]` is observed. 
-        * If the `$*field` appears at the end of the grammar or the next symbol is a nonterminal, then the type of `field` must define a grammar that begins with some terminal or else your parsing will likely be ambiguous or infinite.
     * `$,field` -- similar to the above, but uses a comma separated list (with optional trailing comma). So `[ $,field ]` will parse something like `[f1, f2, f3]`.
-        * Lookahead is required for `$,field` (this could be changed).
     * `$?field` -- will parse `field` and use `Default::default()` value if not present.
 
 ### Greediness
 
-Parsing is generally greedy. So `$*x` and `$,x`, for example, consume as many entries as they can, subject to lookahead. In a case like `$*f $*g`, the parser would parse as many `f` values as it could before parsing `g`. If some entry can be parsed as either `f` or `g`, the parser will not explore all possibilities. The caveat here is lookahead: given `$*f #`, for example, parsing will stop when `#` is observed, even if `f` could parse `#`.
+Parsing is generally greedy. So `$*x` and `$,x`, for example, consume as many entries as they can. Typically this works best if `x` begins with some symbol that indicates whether it is present.
 
 ### Default grammar
 
@@ -53,3 +55,20 @@ If no grammar is supplied, the default grammar is determined as follows:
 
 * If a `#[cast]` or `#[variable]` annotation is present, then the default grammar is just `$v0`.
 * Otherwise, the default grammar is the name of the type (for structs) or variant (for enums), followed by `()`, with the values for the fields in order. So `Mul(Expr, Expr)` would have a default grammar `mul($v0, $v1)`.
+
+### Customizing the parse
+
+If you prefer, you can customize the parse by annotating your term with `#[customize(parse)]`. In the Rust case, for example, the parsing of `RigidTy` is customized ([as is the debug impl](./debug.md)):
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty.rs:RigidTy_decl}}
+```
+
+You must then supply an impl of `Parse` yourself. Because `Parse` is a trait alias, you actually want to implement `CoreParse<L>` for your language type `L`. Inside the code you will want to instantiate a `Parser` and then invoke `parse_variant` for every variant, finally invoking `finish`.
+
+In the Rust code, the impl for `RigidTy` looks as follows:
+
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty/parse_impls.rs:RigidTy_impl}}
+```
\ No newline at end of file
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index 551b11a2..06f6e0ca 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -1,6 +1,7 @@
 use super::{AliasName, AliasTy, AssociatedTyName, Parameter, RefKind, RigidName, RigidTy};
 use std::fmt::Debug;
 
+// ANCHOR: RigidTy_impl
 impl Debug for RigidTy {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let RigidTy { name, parameters } = self;
@@ -42,6 +43,7 @@ impl Debug for RigidTy {
         }
     }
 }
+// ANCHOR_END: RigidTy_impl
 
 impl Debug for AliasTy {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index 26bb8046..07789d1a 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -12,12 +12,18 @@ use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
 
 use crate::rust::FormalityLang as Rust;
 
+// ANCHOR: RigidTy_impl
+// Implement custom parsing for rigid types.
 impl CoreParse<Rust> for RigidTy {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
         let mut parser: Parser<'_, '_, RigidTy, Rust> = Parser::new(scope, text, "AliasTy");
 
+        // Parse a `ScalarId` (and upcast it to `RigidTy`) with the highest
+        // precedence. If someone writes `u8`, we always interpret it as a
+        // scalar-id.
         parser.parse_variant_cast::<ScalarId>(1);
 
+        // Parse something like `Id<...>` as an ADT.
         parser.parse_variant("Adt", 0, |p| {
             let name: AdtId = p.nonterminal()?;
             let parameters: Vec<Parameter> = parse_parameters(p)?;
@@ -27,6 +33,7 @@ impl CoreParse<Rust> for RigidTy {
             })
         });
 
+        // Parse `&`
         parser.parse_variant("Ref", 0, |p| {
             p.expect_char('&')?;
             let lt: Lt = p.nonterminal()?;
@@ -64,6 +71,7 @@ impl CoreParse<Rust> for RigidTy {
         parser.finish()
     }
 }
+// ANCHOR_END: RigidTy_impl
 
 impl CoreParse<Rust> for AliasTy {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {

From 941b0a8ebd4e52263260355b44389abe1acce1ea Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 16:22:26 -0400
Subject: [PATCH 21/22] describe collections

---
 book/src/formality_core/collections.md | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/book/src/formality_core/collections.md b/book/src/formality_core/collections.md
index 9385853c..b3604527 100644
--- a/book/src/formality_core/collections.md
+++ b/book/src/formality_core/collections.md
@@ -1 +1,25 @@
 # Collections
+
+When using formality, it's best to use the following collection types:
+
+* for sequences, use the standard `Vec` type
+* `formality_core::Set<T>` -- equivalent to `BTreeSet` but shorter. We use a `BTreeSet` because it has deterministic ordering for all operations.
+* `formality_core::Map<K, V>` -- equivalent to `BTreeMap` but shorter. We use a `BTreeMap` because it has deterministic ordering for all operations.
+
+## Macros
+
+We also define macros:
+
+* `seq![...]` -- equivalent to `vec![]` but permits flattening with `..` notation, as described below
+* `set![...]` -- like `seq!`, but produces a `Set`
+
+In these macros you can "flatten" things that support `IntoIterator`, so `set![..a, ..b]` will effectively perform a set union of `a` and `b`.
+
+## Casting between collections and tuples
+
+It is possible to upcast from variable tuple types to produce collections:
+
+* A `Vec<E1>` can be upcast to a `Vec<E2>` if `E1: Upcast<E2>`.
+* A `Set<E1>` can be upcast to a `Set<E2>` if `E1: Upcast<E2>`.
+* Tuples of elements (e.g., `(E1, E2)` or `(E1, E2, E3)`) can be **upcast** to sets up to a fixed arity.
+* Sets and vectors can be **downcast** to `()` and `(E, C)`, where `()` succeeds only for empty collections, and `(E, C)` extracts the first element `E` and a collection `C` with all remaining elements (note that elements in sets are always ordered, so the first element is well defined there). This is useful when writing judgment rules that operate over sequences and sets.
\ No newline at end of file

From 422e8a622bf21252bf6371f3741903ac4064bd50 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sat, 4 Nov 2023 17:50:34 -0400
Subject: [PATCH 22/22] track arity of associated items in their names

I could not cope with the bad printouts.
---
 crates/formality-rust/src/prove.rs            |  2 ++
 crates/formality-types/src/grammar/ty.rs      | 16 ++++++++++--
 .../src/grammar/ty/debug_impls.rs             | 26 ++++++++++++-------
 .../src/grammar/ty/parse_impls.rs             |  6 ++++-
 tests/associated_type_normalization.rs        |  2 +-
 tests/coherence_overlap.rs                    |  4 +--
 tests/projection.rs                           | 14 +++++-----
 .../ui/coherence_orphan/alias_to_unit.stderr  |  4 +--
 .../coherence_orphan/mirror_CoreStruct.stderr |  4 +--
 9 files changed, 52 insertions(+), 26 deletions(-)

diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
index 67e25b48..e9193567 100644
--- a/crates/formality-rust/src/prove.rs
+++ b/crates/formality-rust/src/prove.rs
@@ -204,6 +204,7 @@ impl Crate {
                                         alias: AliasTy::associated_ty(
                                             &trait_id,
                                             item_id,
+                                            assoc_vars.len(),
                                             seq![
                                                 self_ty.to(),
                                                 ..trait_parameters.iter().cloned(),
@@ -255,6 +256,7 @@ impl Crate {
                             let alias = AliasTy::associated_ty(
                                 trait_id,
                                 item_id,
+                                assoc_vars.len(),
                                 (&trait_vars, &assoc_vars),
                             );
 
diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs
index ef306ee0..0d4580d3 100644
--- a/crates/formality-types/src/grammar/ty.rs
+++ b/crates/formality-types/src/grammar/ty.rs
@@ -117,12 +117,14 @@ impl UpcastFrom<Ty> for TyData {
     }
 }
 
+// ANCHOR: RigidTy_decl
 #[term((rigid $name $*parameters))]
 #[customize(parse, debug)]
 pub struct RigidTy {
     pub name: RigidName,
     pub parameters: Parameters,
 }
+// ANCHOR_END: RigidTy_decl
 
 impl UpcastFrom<ScalarId> for RigidTy {
     fn upcast_from(s: ScalarId) -> Self {
@@ -198,15 +200,19 @@ impl AliasTy {
     pub fn associated_ty(
         trait_id: impl Upcast<TraitId>,
         item_id: impl Upcast<AssociatedItemId>,
+        item_arity: usize,
         parameters: impl Upcast<Vec<Parameter>>,
     ) -> Self {
+        let parameters: Vec<Parameter> = parameters.upcast();
+        assert!(item_arity <= parameters.len());
         AliasTy {
             name: AssociatedTyName {
                 trait_id: trait_id.upcast(),
                 item_id: item_id.upcast(),
+                item_arity,
             }
             .upcast(),
-            parameters: parameters.upcast(),
+            parameters: parameters,
         }
     }
 }
@@ -217,10 +223,16 @@ pub enum AliasName {
     AssociatedTyId(AssociatedTyName),
 }
 
-#[term(($trait_id :: $item_id))]
+#[term(($trait_id :: $item_id / $item_arity))]
 pub struct AssociatedTyName {
+    /// The trait in which the associated type was declared.
     pub trait_id: TraitId,
+
+    /// The name of the associated type.
     pub item_id: AssociatedItemId,
+
+    /// The number of parameters on the associated type (often 0).
+    pub item_arity: usize,
 }
 
 #[term]
diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs
index 06f6e0ca..15595fbe 100644
--- a/crates/formality-types/src/grammar/ty/debug_impls.rs
+++ b/crates/formality-types/src/grammar/ty/debug_impls.rs
@@ -33,12 +33,7 @@ impl Debug for RigidTy {
                 }
             }
             _ => {
-                write!(
-                    f,
-                    "{:?}{:?}",
-                    name,
-                    PrettyParameters::new("<", ">", parameters)
-                )
+                write!(f, "{:?}{:?}", name, PrettyParameters::angle(parameters))
             }
         }
     }
@@ -49,14 +44,23 @@ impl Debug for AliasTy {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let AliasTy { name, parameters } = self;
         match name {
-            AliasName::AssociatedTyId(AssociatedTyName { trait_id, item_id }) => {
+            AliasName::AssociatedTyId(AssociatedTyName {
+                trait_id,
+                item_id,
+                item_arity,
+            }) => {
+                let (trait_parameters, item_parameters) =
+                    parameters.split_at(parameters.len() - item_arity);
+                let (self_parameter, other_parameters) = trait_parameters.split_at(1);
                 // Grr, wish we would remember the number of parameters assigned to each position.
                 write!(
                     f,
-                    "({:?}::{:?}){:?}",
+                    "<{:?} as {:?}{:?}>::{:?}{:?}",
+                    self_parameter[0],
                     trait_id,
+                    PrettyParameters::angle(other_parameters),
                     item_id,
-                    PrettyParameters::new("<", ">", parameters),
+                    PrettyParameters::angle(item_parameters),
                 )
             }
         }
@@ -72,6 +76,10 @@ impl<'a> PrettyParameters<'a> {
     fn new(open: &'a str, close: &'a str, p: &'a [Parameter]) -> Self {
         Self { open, close, p }
     }
+
+    fn angle(p: &'a [Parameter]) -> Self {
+        Self::new("<", ">", p)
+    }
 }
 
 impl Debug for PrettyParameters<'_> {
diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs
index 07789d1a..4765ac1a 100644
--- a/crates/formality-types/src/grammar/ty/parse_impls.rs
+++ b/crates/formality-types/src/grammar/ty/parse_impls.rs
@@ -88,7 +88,11 @@ impl CoreParse<Rust> for AliasTy {
             p.expect_char(':')?;
             let item_id: AssociatedItemId = p.nonterminal()?;
             let item_parameters = parse_parameters(p)?;
-            let name = AssociatedTyName { trait_id, item_id };
+            let name = AssociatedTyName {
+                trait_id,
+                item_id,
+                item_arity: item_parameters.len(),
+            };
             let parameters: Vec<Parameter> = std::iter::once(ty0.upcast())
                 .chain(trait_parameters1)
                 .chain(item_parameters)
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
index bcb3b0f0..95c95721 100644
--- a/tests/associated_type_normalization.rs
+++ b/tests/associated_type_normalization.rs
@@ -39,7 +39,7 @@ fn test_mirror_normalizes_u32_to_u32() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (Mirror::Assoc)<u32>,
+                        ?ty_1 => <u32 as Mirror>::Assoc,
                     },
                 },
             },
diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs
index de28289b..aeb8f1bf 100644
--- a/tests/coherence_overlap.rs
+++ b/tests/coherence_overlap.rs
@@ -53,7 +53,7 @@ fn test_overlap_normalize_alias_to_LocalType() {
 
     expect_test::expect![[r#"
         Err(
-            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (Mirror::T)<LocalType> where [] { }",
+            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for <LocalType as Mirror>::T where [] { }",
         )
     "#]]
     .assert_debug_eq(&test_program_ok(&gen_program(
@@ -114,7 +114,7 @@ fn test_overlap_alias_not_normalizable() {
 
     expect_test::expect![[r#"
         Err(
-            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <ty> LocalTrait < > for (Mirror::T)<^ty0_0> where [^ty0_0 : Mirror < >] { }",
+            "impls may overlap:\nimpl <ty> LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <ty> LocalTrait < > for <^ty0_0 as Mirror>::T where [^ty0_0 : Mirror < >] { }",
         )
     "#]] // FIXME
     .assert_debug_eq(&test_program_ok(&gen_program(
diff --git a/tests/projection.rs b/tests/projection.rs
index 1302408b..ea3cd005 100644
--- a/tests/projection.rs
+++ b/tests/projection.rs
@@ -31,7 +31,7 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (Iterator::Item)<Vec<!ty_1>>,
+                        ?ty_2 => <Vec<!ty_1> as Iterator>::Item,
                     },
                 },
                 Constraints {
@@ -110,7 +110,7 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (Iterator::Item)<!ty_1>,
+                        ?ty_2 => <!ty_1 as Iterator>::Item,
                     },
                 },
             },
@@ -169,8 +169,8 @@ fn normalize_basic() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => Vec<(Iterator::Item)<!ty_1>>,
-                        ?ty_3 => (Iterator::Item)<!ty_1>,
+                        ?ty_2 => Vec<<!ty_1 as Iterator>::Item>,
+                        ?ty_3 => <!ty_1 as Iterator>::Item,
                     },
                 },
             },
@@ -221,7 +221,7 @@ fn normalize_into_iterator() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_2 => (IntoIterator::Item)<Vec<!ty_1>>,
+                        ?ty_2 => <Vec<!ty_1> as IntoIterator>::Item,
                     },
                 },
                 Constraints {
@@ -286,7 +286,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (Trait1::Type)<S>,
+                        ?ty_1 => <S as Trait1>::Type,
                     },
                 },
             },
@@ -321,7 +321,7 @@ fn projection_equality() {
                     },
                     known_true: true,
                     substitution: {
-                        ?ty_1 => (Trait1::Type)<S>,
+                        ?ty_1 => <S as Trait1>::Type,
                     },
                 },
             },
diff --git a/tests/ui/coherence_orphan/alias_to_unit.stderr b/tests/ui/coherence_orphan/alias_to_unit.stderr
index f45ed78b..cbb363b8 100644
--- a/tests/ui/coherence_orphan/alias_to_unit.stderr
+++ b/tests/ui/coherence_orphan/alias_to_unit.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (Unit::Assoc)<FooStruct> where [] { })
+Error: orphan_check(impl <> CoreTrait < > for <FooStruct as Unit>::Assoc where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((Unit::Assoc)<FooStruct>))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait(<FooStruct as Unit>::Assoc))} given {}, got {}
diff --git a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
index 48ca29db..0450e2d9 100644
--- a/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
+++ b/tests/ui/coherence_orphan/mirror_CoreStruct.stderr
@@ -1,4 +1,4 @@
-Error: orphan_check(impl <> CoreTrait < > for (Mirror::Assoc)<CoreStruct> where [] { })
+Error: orphan_check(impl <> CoreTrait < > for <CoreStruct as Mirror>::Assoc where [] { })
 
 Caused by:
-    failed to prove {@ IsLocal(CoreTrait((Mirror::Assoc)<CoreStruct>))} given {}, got {}
+    failed to prove {@ IsLocal(CoreTrait(<CoreStruct as Mirror>::Assoc))} given {}, got {}