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, + ?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, }, }, } 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_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_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 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::>() - .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), }, }, }, 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 LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (Mirror::T)<(rigid (adt LocalType))> where [] { }", + "impls may overlap:\nimpl LocalTrait < > for ^ty0_0 where [^ty0_0 : Iterator < >] { }\nimpl <> LocalTrait < > for (Mirror::T) 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)>, }, }, Constraints { @@ -169,7 +169,7 @@ fn normalize_basic() { }, known_true: true, substitution: { - ?ty_2 => (rigid (adt Vec) (Iterator::Item)), + ?ty_2 => Vec<(Iterator::Item)>, ?ty_3 => (Iterator::Item), }, }, @@ -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)>, }, }, 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), }, }, }, @@ -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), }, }, }, 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 (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 A((rigid (scalar u32)), ^ty0_0)}, got {} + 0: prove_where_clause_well_formed(for 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 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) where [] { }) Caused by: - failed to prove {@ IsLocal(CoreTrait((Unit::Assoc)<(rigid (adt FooStruct))>))} given {}, got {} + failed to prove {@ IsLocal(CoreTrait((Unit::Assoc)))} 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) where [] { }) Caused by: - failed to prove {@ IsLocal(CoreTrait((Mirror::Assoc)<(rigid (adt CoreStruct))>))} given {}, got {} + failed to prove {@ IsLocal(CoreTrait((Mirror::Assoc)))} 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 CoreTrait < (rigid (adt FooStruct)) > for ^ty0_0 where [] { }) +Error: orphan_check(impl 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 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 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 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 Foo < const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar u32))] { }) +Error: check_trait_impl(impl 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 {}