Struct chalk_solve::wf::WfWellKnownConstraints

struct WfWellKnownConstraints;

Defines methods to compute well-formedness goals for well-known traits (e.g. a goal for all fields of struct in a Copy impl to be Copy)

Implementations

impl WfWellKnownConstraints

pub fn struct_sized_constraint<I: Interner>( db: &dyn RustIrDatabase<I>, fields: &[Ty<I>], size_all: bool ) -> Option<Goal<I>>

Computes a goal to prove Sized constraints on a struct definition. Struct is considered well-formed (in terms of Sized) when it either has no fields or all of it’s fields except the last are proven to be Sized.

fn copy_impl_constraint<I: Interner>( solver: &mut dyn Solver<I>, db: &dyn RustIrDatabase<I>, impl_datum: &ImplDatum<I> ) -> bool

Verify constraints on a Copy implementation. Copy impl is considered well-formed for a) certain builtin types (scalar values, shared ref, etc..) b) adts which 1) have all Copy fields 2) don’t have a Drop impl

fn drop_impl_constraint<I: Interner>( solver: &mut dyn Solver<I>, db: &dyn RustIrDatabase<I>, impl_datum: &ImplDatum<I> ) -> bool

Verifies constraints on a Drop implementation Drop implementation is considered well-formed if: a) it’s implemented on an ADT b) The generic parameters of the impl’s type must all be parameters of the Drop impl itself (i.e., no specialization like impl Drop for S<Foo> {...} is allowed). c) Any bounds on the genereic parameters of the impl must be deductible from the bounds imposed by the struct definition (i.e. the implementation must be exactly as generic as the ADT definition).

struct S<T1, T2> { }
struct Foo<T> { }

impl<U1: Copy, U2: Sized> Drop for S<U2, Foo<U1>> { }

generates the following: goal derived from c):

forall<U1, U2> {
   Implemented(U1: Copy), Implemented(U2: Sized) :- FromEnv(S<U2, Foo<U1>>)
}

goal derived from b):

forall <T1, T2> {
    exists<U1, U2> {
       S<T1, T2> = S<U2, Foo<U1>>
    }
}

fn coerce_unsized_impl_constraint<I: Interner>( solver: &mut dyn Solver<I>, db: &dyn RustIrDatabase<I>, impl_datum: &ImplDatum<I> ) -> bool

Verify constraints a CoerceUnsized impl. Rules for CoerceUnsized impl to be considered well-formed:

1. pointer conversions: &[mut] T -> &[mut] U, &[mut] T -> *[mut] U, *[mut] T -> *[mut] U are considered valid if

   1. T: Unsize<U>
   2. mutability is respected, i.e. immutable -> immutable, mutable -> immutable, mutable -> mutable conversions are allowed, immutable -> mutable is not.

2. struct conversions of structures with the same definition, S<P0...Pn> -> S<Q0...Qn>. To check if this impl is legal, we would walk down the fields of S and consider their types with both substitutes. We are looking to find exactly one (non-phantom) field that has changed its type (from T to U), and expect T to be unsizeable to U, i.e. T: CoerceUnsized<U>.

   As an example, consider a struct

   struct Foo<T, U> {
       extra: T,
       ptr: *mut U,
   }

   We might have an impl that allows (e.g.) Foo<T, [i32; 3]> to be unsized to Foo<T, [i32]>. That impl would look like:

   impl<T, U: Unsize<V>, V> CoerceUnsized<Foo<T, V>> for Foo<T, U> {}

   In this case:

   • extra has type T before and type T after
   • ptr has type *mut U before and type *mut V after

   Since just one field changed, we would then check that *mut U: CoerceUnsized<*mut V> is implemented. This will work out because U: Unsize<V>, and we have a libcore rule that *mut U can be coerced to *mut V if U: Unsize<V>.

fn dispatch_from_dyn_constraint<I: Interner>( solver: &mut dyn Solver<I>, db: &dyn RustIrDatabase<I>, impl_datum: &ImplDatum<I> ) -> bool

Verify constraints of a DispatchFromDyn impl.

Rules for DispatchFromDyn impl to be considered well-formed:

• Self and the type parameter must both be references or raw pointers with the same mutabilty
• OR all the following hold:
  • Self and the type parameter must be structs
  • Self and the type parameter must have the same definitions
  • Self must not be #[repr(packed)] or #[repr(C)]
  • Self must have exactly one field which is not a 1-ZST (there may be any number of 1-ZST fields), and that field must have a different type in the type parameter (i.e., it is the field being coerced)
  • DispatchFromDyn is implemented for the type of the field being coerced.