pretty print rigid types

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,
             },
         }

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,
                 },
             },
         }

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>,
                 },
             },
         }

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,
                 },
             },

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,

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(())
+        }
+    }
+}

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};

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},

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>,
                     },
                 },
             },

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(

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>,
                     },
                 },
             },

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 {}

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 {}

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 {}

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 {}

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 {}

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 {}

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,
             },
         },
     }

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 [] { }

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 [] { }

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 < >] { }

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

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 [] { }

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 {}

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 {}

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 {}

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 {}