Add the str primitive type

Author: AzureMarker

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/test/coherence.rs

@@ -264,9 +264,9 @@ fn fundamental_traits() {
     lowering_error! {
         program {
             #[upstream] trait Sized { }
-            #[upstream] struct str { }
+            #[upstream] struct str2 { } // str is already known to be !Sized, so make a new str type
             trait Bar { }
-            impl Bar for str { }
+            impl Bar for str2 { }
             impl<T> Bar for T where T: Sized { }
         } error_msg {
             "overlapping impls of trait `Bar`"
@@ -279,9 +279,9 @@ fn fundamental_traits() {
     lowering_success! {
         program {
             #[upstream] #[fundamental] trait Sized { }
-            #[upstream] struct str { }
+            #[upstream] struct str2 { }
             trait Bar { }
-            impl Bar for str { }
+            impl Bar for str2 { }
             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,32 @@
+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" }
+    }
+}

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