track arity of associated items in their names

nikomatsakis · nikomatsakis · commit 422e8a622bf2 · 2023-11-04T17:50:34.000-04:00
I could not cope with the bad printouts.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 {}

Original file line number	Diff line number	Diff line change
`@@ -117,12 +117,14 @@ impl UpcastFrom<Ty> for TyData {`
`117`	`117`	`}`
`118`	`118`	`}`
`119`	`119`
	`120`	`+// ANCHOR: RigidTy_decl`
`120`	`121`	`#[term((rigid $name $*parameters))]`
`121`	`122`	`#[customize(parse, debug)]`
`122`	`123`	`pub struct RigidTy {`
`123`	`124`	`pub name: RigidName,`
`124`	`125`	`pub parameters: Parameters,`
`125`	`126`	`}`
	`127`	`+// ANCHOR_END: RigidTy_decl`
`126`	`128`
`127`	`129`	`impl UpcastFrom<ScalarId> for RigidTy {`
`128`	`130`	`fn upcast_from(s: ScalarId) -> Self {`
`@@ -198,15 +200,19 @@ impl AliasTy {`
`198`	`200`	`pub fn associated_ty(`
`199`	`201`	`trait_id: impl Upcast<TraitId>,`
`200`	`202`	`item_id: impl Upcast<AssociatedItemId>,`
	`203`	`+ item_arity: usize,`
`201`	`204`	`parameters: impl Upcast<Vec<Parameter>>,`
`202`	`205`	`) -> Self {`
	`206`	`+ let parameters: Vec<Parameter> = parameters.upcast();`
	`207`	`+ assert!(item_arity <= parameters.len());`
`203`	`208`	`AliasTy {`
`204`	`209`	`name: AssociatedTyName {`
`205`	`210`	`trait_id: trait_id.upcast(),`
`206`	`211`	`item_id: item_id.upcast(),`
	`212`	`+ item_arity,`
`207`	`213`	`}`
`208`	`214`	`.upcast(),`
`209`		`- parameters: parameters.upcast(),`
	`215`	`+ parameters: parameters,`
`210`	`216`	`}`
`211`	`217`	`}`
`212`	`218`	`}`
`@@ -217,10 +223,16 @@ pub enum AliasName {`
`217`	`223`	`AssociatedTyId(AssociatedTyName),`
`218`	`224`	`}`
`219`	`225`
`220`		`-#[term(($trait_id :: $item_id))]`
	`226`	`+#[term(($trait_id :: $item_id / $item_arity))]`
`221`	`227`	`pub struct AssociatedTyName {`
	`228`	`+ /// The trait in which the associated type was declared.`
`222`	`229`	`pub trait_id: TraitId,`
	`230`	`+`
	`231`	`+ /// The name of the associated type.`
`223`	`232`	`pub item_id: AssociatedItemId,`
	`233`	`+`
	`234`	`+ /// The number of parameters on the associated type (often 0).`
	`235`	`+ pub item_arity: usize,`
`224`	`236`	`}`
`225`	`237`
`226`	`238`	`#[term]`
Original file line number	Diff line number	Diff line change
`@@ -33,12 +33,7 @@ impl Debug for RigidTy {`
`33`	`33`	`}`
`34`	`34`	`}`
`35`	`35`	`_ => {`
`36`		`- write!(`
`37`		`- f,`
`38`		`- "{:?}{:?}",`
`39`		`- name,`
`40`		`- PrettyParameters::new("<", ">", parameters)`
`41`		`- )`
	`36`	`+ write!(f, "{:?}{:?}", name, PrettyParameters::angle(parameters))`
`42`	`37`	`}`
`43`	`38`	`}`
`44`	`39`	`}`
`@@ -49,14 +44,23 @@ impl Debug for AliasTy {`
`49`	`44`	`fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {`
`50`	`45`	`let AliasTy { name, parameters } = self;`
`51`	`46`	`match name {`
`52`		`- AliasName::AssociatedTyId(AssociatedTyName { trait_id, item_id }) => {`
	`47`	`+ AliasName::AssociatedTyId(AssociatedTyName {`
	`48`	`+ trait_id,`
	`49`	`+ item_id,`
	`50`	`+ item_arity,`
	`51`	`+ }) => {`
	`52`	`+ let (trait_parameters, item_parameters) =`
	`53`	`+ parameters.split_at(parameters.len() - item_arity);`
	`54`	`+ let (self_parameter, other_parameters) = trait_parameters.split_at(1);`
`53`	`55`	`// Grr, wish we would remember the number of parameters assigned to each position.`
`54`	`56`	`write!(`
`55`	`57`	`f,`
`56`		`- "({:?}::{:?}){:?}",`
	`58`	`+ "<{:?} as {:?}{:?}>::{:?}{:?}",`
	`59`	`+ self_parameter[0],`
`57`	`60`	`trait_id,`
	`61`	`+ PrettyParameters::angle(other_parameters),`
`58`	`62`	`item_id,`
`59`		`- PrettyParameters::new("<", ">", parameters),`
	`63`	`+ PrettyParameters::angle(item_parameters),`
`60`	`64`	`)`
`61`	`65`	`}`
`62`	`66`	`}`
`@@ -72,6 +76,10 @@ impl<'a> PrettyParameters<'a> {`
`72`	`76`	`fn new(open: &'a str, close: &'a str, p: &'a [Parameter]) -> Self {`
`73`	`77`	`Self { open, close, p }`
`74`	`78`	`}`
	`79`	`+`
	`80`	`+ fn angle(p: &'a [Parameter]) -> Self {`
	`81`	`+ Self::new("<", ">", p)`
	`82`	`+ }`
`75`	`83`	`}`
`76`	`84`
`77`	`85`	`impl Debug for PrettyParameters<'_> {`