Add never type to TypeName

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❌         | ❌     | ❌    | ❌     | ❌      | ⚬   | ⚬   | ⚬      |  ⚬       |    ❌        |

chalk-integration/src/lowering.rs

@@ -1427,6 +1427,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)),
         }
     }
 }

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

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,

chalk-parse/src/ast.rs

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

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)

chalk-solve/src/clauses.rs

@@ -404,20 +404,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)))
+        }
     }
 }
 

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()),

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,

tests/test/mod.rs

@@ -307,6 +307,7 @@ mod implied_bounds;
 mod impls;
 mod misc;
 mod negation;
+mod never;
 mod object_safe;
 mod projection;
 mod refs;

tests/test/never.rs

@@ -0,0 +1,13 @@
+use super::*;
+
+#[test]
+fn never_is_well_formed() {
+    test! {
+        program { }
+        goal {
+            WellFormed(!)
+        } yields {
+            "Unique"
+        }
+    }
+}

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