Merge pull request #466 from nathanwhit/typename-never

jackh726 · web-flow · commit 08956d44b4da · 2020-05-22T12:37:37.000-04:00
Add never type to `TypeName`
diff --git a/book/src/clauses/well_known_traits.md b/book/src/clauses/well_known_traits.md
@@ -34,10 +34,11 @@ Some common examples of auto traits are `Send` and `Sync`.
 | structs         | ⚬    | ⚬    |  ✅    | ✅     | ⚬    | ⚬  |  ⚬      |  ⚬       |   ✅         |
 | scalar types    | 📚    | 📚    | ✅     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ❌        |
 | str             | 📚    | 📚    | ⚬     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ❌        |
+| never type      | 📚   |  📚   |  ✅   |  ⚬    |  ⚬    | ⚬   |   ⚬    |  ⚬       |   ❌       |
 | trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬    | ⚬   | ⚬      |  ⚬       |    ⚬        |
 | functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬    | ❌   | ⚬      |  ⚬       |    ❌         |
-| raw ptrs        | ✅   |  ✅  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
-| immutable refs  | ✅   |  ✅  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
+| raw ptrs        | 📚   |  📚  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
+| immutable refs  | 📚   |  📚  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
 | mutable refs    | ⚬    |  ⚬   |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
 | slices          | ⚬     | ⚬    | ⚬     |   ✅    | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌       |
 | arrays❌         | ❌     | ❌    | ❌     | ❌      | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌        |
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
@@ -1438,6 +1438,12 @@ impl LowerTy for Ty {
                 substitution: chalk_ir::Substitution::empty(interner),
             })
             .intern(interner)),
+
+            Ty::Never => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
+                name: chalk_ir::TypeName::Never,
+                substitution: chalk_ir::Substitution::empty(interner),
+            })
+            .intern(interner)),
         }
     }
 }
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
@@ -167,6 +167,7 @@ impl<I: Interner> Debug for TypeName<I> {
             TypeName::FnDef(fn_def) => write!(fmt, "{:?}", fn_def),
             TypeName::Raw(mutability) => write!(fmt, "{:?}", mutability),
             TypeName::Ref(mutability) => write!(fmt, "{:?}", mutability),
+            TypeName::Never => write!(fmt, "Never"),
             TypeName::Error => write!(fmt, "{{error}}"),
         }
     }
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
@@ -175,6 +175,9 @@ pub enum TypeName<I: Interner> {
     /// the string primitive type
     Str,
 
+    /// the never type `!`
+    Never,
+
     /// 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,
diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs
@@ -222,6 +222,7 @@ pub enum Ty {
         ty: Box<Ty>,
     },
     Str,
+    Never,
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, Debug)]
diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop
@@ -224,6 +224,7 @@ TyWithoutId: Ty = {
     },
     <ScalarType> => Ty::Scalar { ty: <> },
     "str" => Ty::Str,
+    "!" => Ty::Never,
     "fn" "(" <t:Ty> ")" => Ty::ForAll {
         lifetime_names: vec![],
         ty: Box::new(t)
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
@@ -411,20 +411,19 @@ fn match_type_name<I: Interner>(
             .db
             .associated_ty_data(type_id)
             .to_program_clauses(builder),
-        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)))
-        }
-        TypeName::Slice => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
-        TypeName::Raw(_) => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
-        TypeName::Ref(_) => builder.push_fact(WellFormed::Ty(application.clone().intern(interner))),
         TypeName::FnDef(fn_def_id) => builder
             .db
             .fn_def_datum(fn_def_id)
             .to_program_clauses(builder),
+        TypeName::Tuple(_)
+        | TypeName::Scalar(_)
+        | TypeName::Str
+        | TypeName::Slice
+        | TypeName::Raw(_)
+        | TypeName::Ref(_)
+        | TypeName::Never => {
+            builder.push_fact(WellFormed::Ty(application.clone().intern(interner)))
+        }
     }
 }
 
diff --git a/chalk-solve/src/clauses/builtin_traits/copy.rs b/chalk-solve/src/clauses/builtin_traits/copy.rs
@@ -1,7 +1,7 @@
 use crate::clauses::builtin_traits::needs_impl_for_tys;
 use crate::clauses::ClauseBuilder;
 use crate::{Interner, RustIrDatabase, TraitRef};
-use chalk_ir::{ApplicationTy, Mutability, Substitution, TyData, TypeName};
+use chalk_ir::{ApplicationTy, Substitution, TyData, TypeName};
 
 fn push_tuple_copy_conditions<I: Interner>(
     db: &dyn RustIrDatabase<I>,
@@ -41,9 +41,6 @@ pub fn add_copy_program_clauses<I: Interner>(
             TypeName::Tuple(arity) => {
                 push_tuple_copy_conditions(db, builder, trait_ref, *arity, substitution)
             }
-            TypeName::Raw(_) | TypeName::Ref(Mutability::Not) => {
-                builder.push_fact(trait_ref.clone())
-            }
             _ => return,
         },
         TyData::Function(_) => builder.push_fact(trait_ref.clone()),
diff --git a/chalk-solve/src/clauses/builtin_traits/sized.rs b/chalk-solve/src/clauses/builtin_traits/sized.rs
@@ -74,7 +74,7 @@ pub fn add_sized_program_clauses<I: Interner>(
             TypeName::Tuple(arity) => {
                 push_tuple_sized_conditions(db, builder, trait_ref, *arity, substitution)
             }
-            TypeName::Scalar(_) | TypeName::Raw(_) | TypeName::Ref(_) => {
+            TypeName::Never | TypeName::Scalar(_) | TypeName::Raw(_) | TypeName::Ref(_) => {
                 builder.push_fact(trait_ref.clone())
             }
             _ => return,
diff --git a/tests/test/mod.rs b/tests/test/mod.rs
@@ -307,6 +307,7 @@ mod implied_bounds;
 mod impls;
 mod misc;
 mod negation;
+mod never;
 mod object_safe;
 mod opaque_types;
 mod projection;
diff --git a/tests/test/never.rs b/tests/test/never.rs
@@ -0,0 +1,13 @@
+use super::*;
+
+#[test]
+fn never_is_well_formed() {
+    test! {
+        program { }
+        goal {
+            WellFormed(!)
+        } yields {
+            "Unique"
+        }
+    }
+}
diff --git a/tests/test/refs.rs b/tests/test/refs.rs
@@ -57,67 +57,3 @@ fn mut_refs_are_sized() {
         }
     }
 }
-
-#[test]
-fn immut_refs_are_copy() {
-    test! {
-        program {
-            #[lang(copy)]
-            trait Copy { }
-        }
-
-        goal {
-            forall<'a, T> { &'a T: Copy }
-        } yields {
-            "Unique; substitution [], lifetime constraints []"
-        }
-    }
-}
-
-#[test]
-fn immut_refs_are_clone() {
-    test! {
-        program {
-            #[lang(clone)]
-            trait Clone { }
-        }
-
-        goal {
-            forall<'a, T> { &'a T: Clone }
-        } yields {
-            "Unique; substitution [], lifetime constraints []"
-        }
-    }
-}
-
-#[test]
-fn mut_refs_are_not_copy() {
-    test! {
-        program {
-            #[lang(copy)]
-            trait Copy { }
-        }
-
-        goal {
-            forall<'a, T> { not { &'a mut T: Copy } }
-        } yields {
-            "Unique; substitution [], lifetime constraints []"
-        }
-    }
-}
-
-#[test]
-fn mut_refs_are_not_clone() {
-    test! {
-        program {
-            #[lang(clone)]
-            trait Clone { }
-        }
-
-        goal {
-            forall<'a, T> { not { &'a mut T: Clone } }
-        } yields {
-            "Unique; substitution [], lifetime constraints []"
-        }
-    }
-}

Original file line number	Diff line number	Diff line change
`@@ -1438,6 +1438,12 @@ impl LowerTy for Ty {`
`1438`	`1438`	`substitution: chalk_ir::Substitution::empty(interner),`
`1439`	`1439`	`})`
`1440`	`1440`	`.intern(interner)),`
	`1441`	`+`
	`1442`	`+ Ty::Never => Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {`
	`1443`	`+ name: chalk_ir::TypeName::Never,`
	`1444`	`+ substitution: chalk_ir::Substitution::empty(interner),`
	`1445`	`+ })`
	`1446`	`+ .intern(interner)),`
`1441`	`1447`	`}`
`1442`	`1448`	`}`
`1443`	`1449`	`}`
Original file line number	Diff line number	Diff line change
`@@ -167,6 +167,7 @@ impl<I: Interner> Debug for TypeName<I> {`
`167`	`167`	`TypeName::FnDef(fn_def) => write!(fmt, "{:?}", fn_def),`
`168`	`168`	`TypeName::Raw(mutability) => write!(fmt, "{:?}", mutability),`
`169`	`169`	`TypeName::Ref(mutability) => write!(fmt, "{:?}", mutability),`
	`170`	`+ TypeName::Never => write!(fmt, "Never"),`
`170`	`171`	`TypeName::Error => write!(fmt, "{{error}}"),`
`171`	`172`	`}`
`172`	`173`	`}`
Original file line number	Diff line number	Diff line change
`@@ -222,6 +222,7 @@ pub enum Ty {`
`222`	`222`	`ty: Box<Ty>,`
`223`	`223`	`},`
`224`	`224`	`Str,`
	`225`	`+ Never,`
`225`	`226`	`}`
`226`	`227`
`227`	`228`	`#[derive(Copy, Clone, PartialEq, Eq, Debug)]`
Original file line number	Diff line number	Diff line change
`@@ -74,7 +74,7 @@ pub fn add_sized_program_clauses<I: Interner>(`
`74`	`74`	`TypeName::Tuple(arity) => {`
`75`	`75`	`push_tuple_sized_conditions(db, builder, trait_ref, *arity, substitution)`
`76`	`76`	`}`
`77`		`- TypeName::Scalar(_) \| TypeName::Raw(_) \| TypeName::Ref(_) => {`
	`77`	`+ TypeName::Never \| TypeName::Scalar(_) \| TypeName::Raw(_) \| TypeName::Ref(_) => {`
`78`	`78`	`builder.push_fact(trait_ref.clone())`
`79`	`79`	`}`
`80`	`80`	`_ => return,`