Add the str type

book/src/clauses/well_known_traits.md

@@ -33,6 +33,7 @@ Some common examples of auto traits are `Send` and `Sync`.
 | tuple types     | ✅    | ✅    | ✅     | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ❌         |
 | structs         | ⚬    | ⚬    |  ✅    | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
 | scalar types    | 📚    | 📚    | ✅     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ❌        |
+| str             | 📚    | 📚    | ⚬     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ❌        |
 | trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬    | ⚬   | ⚬      |  ⚬       |    ⚬        |
 | functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬    | ❌   | ⚬      |  ⚬       |    ❌         |
 | raw ptrs        | ✅   |  ✅  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |

chalk-integration/src/lowering.rs

@@ -1085,6 +1085,7 @@ impl LowerProjectionTy for ProjectionTy {
 }
 
 trait LowerTy {
+    /// Lower from the AST to Chalk's Rust IR
     fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Ty<ChalkIr>>;
 }
 
@@ -1257,6 +1258,12 @@ impl LowerTy for Ty {
                 ),
             })
             .intern(interner)),
+
+            Ty::Str => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
+                name: chalk_ir::TypeName::Str,
+                substitution: chalk_ir::Substitution::empty(interner),
+            })
+            .intern(interner)),
         }
     }
 }

chalk-ir/src/debug.rs

@@ -142,6 +142,7 @@ impl<I: Interner> Debug for TypeName<I> {
             TypeName::Struct(id) => write!(fmt, "{:?}", id),
             TypeName::AssociatedType(assoc_ty) => write!(fmt, "{:?}", assoc_ty),
             TypeName::Scalar(scalar) => write!(fmt, "{:?}", scalar),
+            TypeName::Str => write!(fmt, "Str"),
             TypeName::Tuple(arity) => write!(fmt, "{:?}", arity),
             TypeName::OpaqueType(opaque_ty) => write!(fmt, "!{:?}", opaque_ty),
             TypeName::Slice => write!(fmt, "{{slice}}"),

chalk-ir/src/lib.rs

@@ -168,6 +168,9 @@ pub enum TypeName<I: Interner> {
     /// a placeholder for opaque types like `impl Trait`
     OpaqueType(OpaqueTyId<I>),
 
+    /// the string primitive type
+    Str,
+
     /// This can be used to represent an error, e.g. during name resolution of a type.
     /// Chalk itself will not produce this, just pass it through when given.
     Error,
@@ -966,7 +969,7 @@ pub enum WhereClause<I: Interner> {
 
 #[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner, Zip)]
 pub enum WellFormed<I: Interner> {
-    /// A predicate which is true is some trait ref is well-formed.
+    /// A predicate which is true when some trait ref is well-formed.
     /// For example, given the following trait definitions:
     ///
     /// ```notrust
@@ -981,7 +984,7 @@ pub enum WellFormed<I: Interner> {
     /// ```
     Trait(TraitRef<I>),
 
-    /// A predicate which is true is some type is well-formed.
+    /// A predicate which is true when some type is well-formed.
     /// For example, given the following type definition:
     ///
     /// ```notrust

chalk-parse/src/ast.rs

@@ -206,6 +206,7 @@ pub enum Ty {
         lifetime: Lifetime,
         ty: Box<Ty>,
     },
+    Str,
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

@@ -196,6 +196,7 @@ pub Ty: Ty = {
 
 TyWithoutFor: Ty = {
     <ScalarType> => Ty::Scalar { ty: <> },
+    "str" => Ty::Str,
     <n:Id> => Ty::Id { name: n},
     "fn" "(" <t:Ty> ")" => Ty::ForAll {
         lifetime_names: vec![],

chalk-solve/src/clauses.rs

@@ -389,6 +389,7 @@ fn match_ty<I: Interner>(
     })
 }
 
+/// Lower a Rust IR application type to logic
 fn match_type_name<I: Interner>(
     builder: &mut ClauseBuilder<'_, I>,
     interner: &I,
@@ -408,6 +409,7 @@ fn match_type_name<I: Interner>(
         TypeName::Scalar(_) => {
             builder.push_fact(WellFormed::Ty(application.clone().intern(interner)))
         }
+        TypeName::Str => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
         TypeName::Tuple(_) => {
             builder.push_fact(WellFormed::Ty(application.clone().intern(interner)))
         }

tests/lowering/mod.rs

@@ -555,7 +555,7 @@ fn slices() {
         }
 
         error_msg {
-            "parse error: UnrecognizedToken { token: (29, Token(31, \"]\"), 30), expected: [\"\\\"&\\\"\", \"\\\"(\\\"\", \"\\\"*\\\"\", \"\\\"<\\\"\", \"\\\"[\\\"\", \"\\\"bool\\\"\", \"\\\"char\\\"\", \"\\\"dyn\\\"\", \"\\\"f32\\\"\", \"\\\"f64\\\"\", \"\\\"fn\\\"\", \"\\\"for\\\"\", \"\\\"i128\\\"\", \"\\\"i16\\\"\", \"\\\"i32\\\"\", \"\\\"i64\\\"\", \"\\\"i8\\\"\", \"\\\"isize\\\"\", \"\\\"u128\\\"\", \"\\\"u16\\\"\", \"\\\"u32\\\"\", \"\\\"u64\\\"\", \"\\\"u8\\\"\", \"\\\"usize\\\"\", \"r#\\\"([A-Za-z]|_)([A-Za-z0-9]|_)*\\\"#\"] }"
+            "parse error: UnrecognizedToken { token: (29, Token(31, \"]\"), 30), expected: [\"\\\"&\\\"\", \"\\\"(\\\"\", \"\\\"*\\\"\", \"\\\"<\\\"\", \"\\\"[\\\"\", \"\\\"bool\\\"\", \"\\\"char\\\"\", \"\\\"dyn\\\"\", \"\\\"f32\\\"\", \"\\\"f64\\\"\", \"\\\"fn\\\"\", \"\\\"for\\\"\", \"\\\"i128\\\"\", \"\\\"i16\\\"\", \"\\\"i32\\\"\", \"\\\"i64\\\"\", \"\\\"i8\\\"\", \"\\\"isize\\\"\", \"\\\"str\\\"\", \"\\\"u128\\\"\", \"\\\"u16\\\"\", \"\\\"u32\\\"\", \"\\\"u64\\\"\", \"\\\"u8\\\"\", \"\\\"usize\\\"\", \"r#\\\"([A-Za-z]|_)([A-Za-z0-9]|_)*\\\"#\"] }"
         }
     }
 }

tests/test/coherence.rs

@@ -257,31 +257,30 @@ fn downstream_impl_of_fundamental_43355() {
 
 #[test]
 fn fundamental_traits() {
-    // We want to enable negative reasoning about some traits. For example, consider the str type.
-    // We know that str is never going to be Sized and we have made a decision to allow people to
-    // depend on that. The following two impls are rejected as overlapping despite the fact that we
-    // know that str will never be Sized.
+    // We want to enable negative reasoning about some traits. For example, assume we have some
+    // "Foo" type which we know is never going to be Sized (ex. str). The following two impls are
+    // rejected as overlapping despite the fact that we know that Foo will never be Sized.
     lowering_error! {
         program {
             #[upstream] trait Sized { }
-            #[upstream] struct str { }
+            #[upstream] struct Foo { }
             trait Bar { }
-            impl Bar for str { }
+            impl Bar for Foo { }
             impl<T> Bar for T where T: Sized { }
         } error_msg {
             "overlapping impls of trait `Bar`"
         }
     }
 
     // If we make Sized fundamental, we're telling the Rust compiler that it can reason negatively
-    // about it. That means that `not { str: Sized }` is provable. With that change, these two
-    // impls are now valid.
+    // about it. That means that `not { Foo: Sized }` is provable. With that change, these two impls
+    // are now valid.
     lowering_success! {
         program {
             #[upstream] #[fundamental] trait Sized { }
-            #[upstream] struct str { }
+            #[upstream] struct Foo { }
             trait Bar { }
-            impl Bar for str { }
+            impl Bar for Foo { }
             impl<T> Bar for T where T: Sized { }
         }
     }

tests/test/mod.rs

@@ -318,6 +318,7 @@ mod projection;
 mod refs;
 mod scalars;
 mod slices;
+mod string;
 mod tuples;
 mod unify;
 mod wf_goals;

tests/test/string.rs

@@ -0,0 +1,54 @@
+use super::*;
+
+#[test]
+fn str_trait_impl() {
+    test! {
+        program {
+            trait Foo {}
+            impl Foo for str {}
+        }
+
+        goal { str: Foo } yields { "Unique" }
+    }
+}
+
+#[test]
+fn str_is_well_formed() {
+    test! {
+        program {}
+        goal { WellFormed(str) } yields { "Unique" }
+    }
+}
+
+#[test]
+fn str_is_not_sized() {
+    test! {
+        program {
+            #[lang(sized)] trait Sized {}
+        }
+
+        goal { not { str: Sized } } yields { "Unique" }
+    }
+}
+
+#[test]
+fn str_is_not_copy() {
+    test! {
+        program {
+            #[lang(copy)] trait Copy {}
+        }
+
+        goal { not { str: Copy } } yields { "Unique" }
+    }
+}
+
+#[test]
+fn str_is_not_clone() {
+    test! {
+        program {
+            #[lang(clone)] trait Clone {}
+        }
+
+        goal { not { str: Clone } } yields { "Unique" }
+    }
+}

tests/test/wf_lowering.rs

@@ -576,7 +576,6 @@ fn assoc_type_recursive_bound() {
             }
 
             struct Number { }
-            struct str { } // not sized
 
             impl Foo for Number {
                 // Well-formedness checks require that the following