|
1 | 1 | use std::{fmt, iter};
|
2 | 2 |
|
3 |
| -use crate::ext::*; |
4 |
| -use crate::goal_builder::GoalBuilder; |
5 |
| -use crate::rust_ir::*; |
6 |
| -use crate::solve::Solver; |
7 |
| -use crate::split::Split; |
8 |
| -use crate::RustIrDatabase; |
9 |
| -use chalk_ir::cast::*; |
10 |
| -use chalk_ir::fold::shift::Shift; |
11 |
| -use chalk_ir::interner::Interner; |
12 |
| -use chalk_ir::visit::{Visit, Visitor}; |
13 |
| -use chalk_ir::*; |
| 3 | +use crate::{ |
| 4 | + ext::*, goal_builder::GoalBuilder, rust_ir::*, solve::Solver, split::Split, RustIrDatabase, |
| 5 | +}; |
| 6 | +use chalk_ir::{ |
| 7 | + cast::*, |
| 8 | + fold::shift::Shift, |
| 9 | + interner::Interner, |
| 10 | + visit::{Visit, Visitor}, |
| 11 | + *, |
| 12 | +}; |
14 | 13 | use tracing::debug;
|
15 | 14 |
|
16 | 15 | #[derive(Debug)]
|
@@ -338,7 +337,14 @@ where
|
338 | 337 | WellKnownTrait::Drop => {
|
339 | 338 | WfWellKnownConstraints::drop_impl_constraint(&mut *solver, self.db, &impl_datum)
|
340 | 339 | }
|
341 |
| - WellKnownTrait::Clone | WellKnownTrait::Unpin | WellKnownTrait::CoerceUnsized => true, |
| 340 | + WellKnownTrait::CoerceUnsized => { |
| 341 | + WfWellKnownConstraints::coerce_unsized_impl_constraint( |
| 342 | + &mut *solver, |
| 343 | + self.db, |
| 344 | + &impl_datum, |
| 345 | + ) |
| 346 | + } |
| 347 | + WellKnownTrait::Clone | WellKnownTrait::Unpin => true, |
342 | 348 | // You can't add a manual implementation for the following traits:
|
343 | 349 | WellKnownTrait::Fn
|
344 | 350 | | WellKnownTrait::FnOnce
|
@@ -813,4 +819,109 @@ impl WfWellKnownConstraints {
|
813 | 819 |
|
814 | 820 | solver.has_unique_solution(db, &well_formed_goal.into_closed_goal(interner))
|
815 | 821 | }
|
| 822 | + |
| 823 | + /// Verify constraints a CoerceUnsized impl. |
| 824 | + /// Rules for CoerceUnsized impl to be considered well-formed: |
| 825 | + /// a) pointer conversions: &[mut] T -> &[mut] U, &[mut] T -> *[mut] U, |
| 826 | + /// *[mut] T -> *[mut] U are considered valid if |
| 827 | + /// 1) T: Unsize<U> |
| 828 | + /// 2) mutability is respected, i.e. immutable -> immutable, mutable -> immutable, |
| 829 | + /// mutable -> mutable conversions are allowed, immutable -> mutable is not. |
| 830 | + /// b) struct conversions of structures with the same definition, `S<P0...Pn>` -> `S<Q0...Qn>`. |
| 831 | + /// To check if this impl is legal, we would walk down the fields of `S` |
| 832 | + /// and consider their types with both substitutes. We are looking to find |
| 833 | + /// exactly one (non-phantom) field that has changed its type (from T to U), and |
| 834 | + /// expect T to be unsizeable to U, i.e. T: CoerceUnsized<U>. |
| 835 | + /// |
| 836 | + /// As an example, consider a struct |
| 837 | + /// ```rust |
| 838 | + /// struct Foo<T, U> { |
| 839 | + /// extra: T, |
| 840 | + /// ptr: *mut U, |
| 841 | + /// } |
| 842 | + /// ``` |
| 843 | + /// |
| 844 | + /// We might have an impl that allows (e.g.) `Foo<T, [i32; 3]>` to be unsized |
| 845 | + /// to `Foo<T, [i32]>`. That impl would look like: |
| 846 | + /// ```rust,ignore |
| 847 | + /// impl<T, U: Unsize<V>, V> CoerceUnsized<Foo<T, V>> for Foo<T, U> {} |
| 848 | + /// ``` |
| 849 | + /// In this case: |
| 850 | + /// |
| 851 | + /// - `extra` has type `T` before and type `T` after |
| 852 | + /// - `ptr` has type `*mut U` before and type `*mut V` after |
| 853 | + /// |
| 854 | + /// Since just one field changed, we would then check that `*mut U: CoerceUnsized<*mut V>` |
| 855 | + /// is implemented. This will work out because `U: Unsize<V>`, and we have a libcore rule |
| 856 | + /// that `*mut U` can be coerced to `*mut V` if `U: Unsize<V>`. |
| 857 | + fn coerce_unsized_impl_constraint<I: Interner>( |
| 858 | + solver: &mut dyn Solver<I>, |
| 859 | + db: &dyn RustIrDatabase<I>, |
| 860 | + impl_datum: &ImplDatum<I>, |
| 861 | + ) -> bool { |
| 862 | + let interner = db.interner(); |
| 863 | + let mut gb = GoalBuilder::new(db); |
| 864 | + |
| 865 | + let (binders, impl_datum) = impl_datum.binders.as_ref().into(); |
| 866 | + |
| 867 | + let trait_ref: &TraitRef<I> = &impl_datum.trait_ref; |
| 868 | + |
| 869 | + let source = trait_ref.self_type_parameter(interner); |
| 870 | + let target = trait_ref |
| 871 | + .substitution |
| 872 | + .at(interner, 1) |
| 873 | + .assert_ty_ref(interner) |
| 874 | + .clone(); |
| 875 | + match (source.data(interner), target.data(interner)) { |
| 876 | + (TyData::Apply(source_app), TyData::Apply(target_app)) => { |
| 877 | + match (&source_app.name, &target_app.name) { |
| 878 | + (TypeName::Ref(s_m), TypeName::Ref(t_m)) |
| 879 | + | (TypeName::Ref(s_m), TypeName::Raw(t_m)) |
| 880 | + | (TypeName::Raw(s_m), TypeName::Raw(t_m)) => { |
| 881 | + if matches!((*s_m, *t_m), (Mutability::Not, Mutability::Mut)) { |
| 882 | + return false; |
| 883 | + } |
| 884 | + |
| 885 | + let source = source_app.first_type_parameter(interner).unwrap(); |
| 886 | + let target = target_app.first_type_parameter(interner).unwrap(); |
| 887 | + |
| 888 | + let unsize_trait_id = |
| 889 | + if let Some(id) = db.well_known_trait_id(WellKnownTrait::Unsize) { |
| 890 | + id |
| 891 | + } else { |
| 892 | + return false; |
| 893 | + }; |
| 894 | + |
| 895 | + let unsize_goal: Goal<I> = TraitRef { |
| 896 | + trait_id: unsize_trait_id, |
| 897 | + substitution: Substitution::from_iter( |
| 898 | + interner, |
| 899 | + [source, target].iter().cloned(), |
| 900 | + ), |
| 901 | + } |
| 902 | + .cast(interner); |
| 903 | + |
| 904 | + let unsize_goal = gb.forall( |
| 905 | + &Binders::new( |
| 906 | + binders, |
| 907 | + (unsize_goal, trait_ref, &impl_datum.where_clauses), |
| 908 | + ), |
| 909 | + (), |
| 910 | + |gb, _, (unsize_goal, trait_ref, where_clauses), ()| { |
| 911 | + let interner = gb.interner(); |
| 912 | + gb.implies( |
| 913 | + impl_wf_environment(interner, &where_clauses, &trait_ref), |
| 914 | + |_| unsize_goal, |
| 915 | + ) |
| 916 | + }, |
| 917 | + ); |
| 918 | + |
| 919 | + solver.has_unique_solution(db, &unsize_goal.into_closed_goal(interner)) |
| 920 | + } |
| 921 | + _ => false, |
| 922 | + } |
| 923 | + } |
| 924 | + _ => false, |
| 925 | + } |
| 926 | + } |
816 | 927 | }
|
0 commit comments