From 1840c2ce79bdd2faa148c59953ae633ef629cef0 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Thu, 21 May 2020 12:56:02 -0400 Subject: [PATCH 1/5] Add `Never` to `TypeName` --- chalk-ir/src/debug.rs | 1 + chalk-ir/src/lib.rs | 3 +++ chalk-solve/src/clauses.rs | 19 +++++++++---------- 3 files changed, 13 insertions(+), 10 deletions(-) diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs index 4f535c83a3e..93517d603a8 100644 --- a/chalk-ir/src/debug.rs +++ b/chalk-ir/src/debug.rs @@ -167,6 +167,7 @@ impl Debug for TypeName { 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 index 7510d5e95c2..0bb72e029a3 100644 --- a/chalk-ir/src/lib.rs +++ b/chalk-ir/src/lib.rs @@ -175,6 +175,9 @@ pub enum TypeName { /// 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-solve/src/clauses.rs b/chalk-solve/src/clauses.rs index 50128308324..9861cf93ee0 100644 --- a/chalk-solve/src/clauses.rs +++ b/chalk-solve/src/clauses.rs @@ -404,20 +404,19 @@ fn match_type_name( .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))) + } } } From 5f2ae210b91e4ce0aba0f42f98f16ca80ce7c69a Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Thu, 21 May 2020 12:56:31 -0400 Subject: [PATCH 2/5] Parse and lower never type --- chalk-integration/src/lowering.rs | 6 ++++++ chalk-parse/src/ast.rs | 1 + chalk-parse/src/parser.lalrpop | 1 + 3 files changed, 8 insertions(+) diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs index 51023fe0954..d62a923355b 100644 --- a/chalk-integration/src/lowering.rs +++ b/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)), } } } diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs index 715649ca691..e13f6be2cf8 100644 --- a/chalk-parse/src/ast.rs +++ b/chalk-parse/src/ast.rs @@ -222,6 +222,7 @@ pub enum Ty { ty: Box, }, Str, + Never, } #[derive(Copy, Clone, PartialEq, Eq, Debug)] diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop index ecef2406f97..6ca9cd0ab01 100644 --- a/chalk-parse/src/parser.lalrpop +++ b/chalk-parse/src/parser.lalrpop @@ -224,6 +224,7 @@ TyWithoutId: Ty = { }, => Ty::Scalar { ty: <> }, "str" => Ty::Str, + "!" => Ty::Never, "fn" "(" ")" => Ty::ForAll { lifetime_names: vec![], ty: Box::new(t) From bdef1a98ca8cad3ca896b7f083ccbc6767839f51 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Thu, 21 May 2020 12:56:59 -0400 Subject: [PATCH 3/5] Don't emit copy clauses for tys with impls in core --- .../src/clauses/builtin_traits/copy.rs | 5 +- .../src/clauses/builtin_traits/sized.rs | 2 +- tests/test/refs.rs | 64 ------------------- 3 files changed, 2 insertions(+), 69 deletions(-) diff --git a/chalk-solve/src/clauses/builtin_traits/copy.rs b/chalk-solve/src/clauses/builtin_traits/copy.rs index 4e095dfe0b0..4b325049944 100644 --- 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( db: &dyn RustIrDatabase, @@ -41,9 +41,6 @@ pub fn add_copy_program_clauses( 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 index 371573b5e5e..71b7082422a 100644 --- 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( 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/refs.rs b/tests/test/refs.rs index 27d100c0edd..d6439ce5dff 100644 --- 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 []" - } - } -} From a1adb9c3dd3d8df0958b8b92ac08c5a8c568f1f6 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Thu, 21 May 2020 12:57:09 -0400 Subject: [PATCH 4/5] Add WF test for never type --- tests/test/mod.rs | 1 + tests/test/never.rs | 13 +++++++++++++ 2 files changed, 14 insertions(+) create mode 100644 tests/test/never.rs diff --git a/tests/test/mod.rs b/tests/test/mod.rs index c5ad316af6c..aa135439a32 100644 --- 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 projection; mod refs; diff --git a/tests/test/never.rs b/tests/test/never.rs new file mode 100644 index 00000000000..4c4a6e37c9d --- /dev/null +++ b/tests/test/never.rs @@ -0,0 +1,13 @@ +use super::*; + +#[test] +fn never_is_well_formed() { + test! { + program { } + goal { + WellFormed(!) + } yields { + "Unique" + } + } +} From 2cb1d43c4af293c950663935771d529b6cc48de4 Mon Sep 17 00:00:00 2001 From: Nathan Whitaker Date: Thu, 21 May 2020 13:04:20 -0400 Subject: [PATCH 5/5] Update well known traits table --- book/src/clauses/well_known_traits.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/book/src/clauses/well_known_traits.md b/book/src/clauses/well_known_traits.md index f7e1ebf9311..44f88430b68 100644 --- 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❌ | ❌ | ❌ | ❌ | ❌ | ⚬ | ⚬ | ⚬ | ⚬ | ❌ |