diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
index e347a801737..63a59b97ba2 100644
--- a/chalk-solve/src/clauses.rs
+++ b/chalk-solve/src/clauses.rs
@@ -11,6 +11,7 @@ use chalk_ir::interner::Interner;
 use chalk_ir::*;
 use rustc_hash::FxHashSet;
 use std::iter;
+use std::marker::PhantomData;
 use tracing::{debug, instrument};
 
 pub mod builder;
@@ -583,7 +584,7 @@ pub fn program_clauses_that_could_match<I: Interner>(
         | DomainGoal::IsUpstream(ty)
         | DomainGoal::DownstreamType(ty)
         | DomainGoal::IsFullyVisible(ty)
-        | DomainGoal::IsLocal(ty) => match_ty(builder, environment, ty)?,
+        | DomainGoal::IsLocal(ty) => match_ty(builder, environment, &ty)?,
         DomainGoal::FromEnv(_) => (), // Computed in the environment
         DomainGoal::Normalize(Normalize { alias, ty: _ }) => match alias {
             AliasTy::Projection(proj) => {
@@ -885,43 +886,150 @@ fn match_ty<I: Interner>(
             .db
             .fn_def_datum(*fn_def_id)
             .to_program_clauses(builder, environment),
-        TyKind::Str | TyKind::Never | TyKind::Scalar(_) | TyKind::Foreign(_) => {
+        TyKind::Str
+        | TyKind::Never
+        | TyKind::Scalar(_)
+        | TyKind::Foreign(_)
+        | TyKind::Tuple(0, _) => {
             // These have no substitutions, so they are trivially WF
             builder.push_fact(WellFormed::Ty(ty.clone()));
         }
         TyKind::Raw(mutbl, _) => {
+            // forall<T> WF(*const T) :- WF(T);
             builder.push_bound_ty(|builder, ty| {
-                builder.push_fact(WellFormed::Ty(
-                    TyKind::Raw(*mutbl, ty).intern(builder.interner()),
-                ));
+                builder.push_clause(
+                    WellFormed::Ty(TyKind::Raw(*mutbl, ty.clone()).intern(builder.interner())),
+                    Some(WellFormed::Ty(ty)),
+                );
             });
         }
         TyKind::Ref(mutbl, _, _) => {
+            // forall<'a, T> WF(&'a T) :- WF(T), T: 'a
             builder.push_bound_ty(|builder, ty| {
                 builder.push_bound_lifetime(|builder, lifetime| {
-                    builder.push_fact(WellFormed::Ty(
-                        TyKind::Ref(*mutbl, lifetime, ty).intern(builder.interner()),
-                    ));
+                    let ref_ty = TyKind::Ref(*mutbl, lifetime.clone(), ty.clone())
+                        .intern(builder.interner());
+                    builder.push_clause(
+                        WellFormed::Ty(ref_ty),
+                        [
+                            DomainGoal::WellFormed(WellFormed::Ty(ty.clone())),
+                            DomainGoal::Holds(WhereClause::TypeOutlives(TypeOutlives {
+                                ty,
+                                lifetime,
+                            })),
+                        ],
+                    );
                 })
             });
         }
         TyKind::Slice(_) => {
+            // forall<T> WF([T]) :- T: Sized, WF(T)
             builder.push_bound_ty(|builder, ty| {
-                builder.push_fact(WellFormed::Ty(TyKind::Slice(ty).intern(builder.interner())));
+                let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
+                builder.push_clause(
+                    WellFormed::Ty(TyKind::Slice(ty.clone()).intern(builder.interner())),
+                    sized
+                        .map(|id| {
+                            DomainGoal::Holds(WhereClause::Implemented(TraitRef {
+                                trait_id: id,
+                                substitution: Substitution::from1(interner, ty.clone()),
+                            }))
+                        })
+                        .into_iter()
+                        .chain(Some(DomainGoal::WellFormed(WellFormed::Ty(ty)))),
+                );
             });
         }
-        TyKind::Tuple(_, _)
-        | TyKind::Array(_, _)
-        | TyKind::Closure(_, _)
-        | TyKind::Generator(_, _)
-        | TyKind::GeneratorWitness(_, _) => {
+        TyKind::Array(..) => {
+            // forall<T. const N: usize> WF([T, N]) :- T: Sized
+            let interner = builder.interner();
+            let binders = Binders::new(
+                VariableKinds::from_iter(
+                    interner,
+                    [
+                        VariableKind::Ty(TyVariableKind::General),
+                        VariableKind::Const(
+                            TyKind::Scalar(Scalar::Uint(UintTy::Usize)).intern(interner),
+                        ),
+                    ],
+                ),
+                PhantomData::<I>,
+            );
+            builder.push_binders(binders, |builder, PhantomData| {
+                let placeholders_in_scope = builder.placeholders_in_scope();
+                let placeholder_count = placeholders_in_scope.len();
+                let ty = placeholders_in_scope[placeholder_count - 2]
+                    .assert_ty_ref(interner)
+                    .clone();
+                let size = placeholders_in_scope[placeholder_count - 1]
+                    .assert_const_ref(interner)
+                    .clone();
+
+                let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
+                let array_ty = TyKind::Array(ty.clone(), size).intern(interner);
+                builder.push_clause(
+                    WellFormed::Ty(array_ty),
+                    sized
+                        .map(|id| {
+                            DomainGoal::Holds(WhereClause::Implemented(TraitRef {
+                                trait_id: id,
+                                substitution: Substitution::from1(interner, ty.clone()),
+                            }))
+                        })
+                        .into_iter()
+                        .chain(Some(DomainGoal::WellFormed(WellFormed::Ty(ty)))),
+                );
+            });
+        }
+        TyKind::Tuple(len, _) => {
+            // WF((T0, ..., Tn, U)) :- T0: Sized, ..., Tn: Sized, WF(T0), ..., WF(Tn), WF(U)
+            let interner = builder.interner();
+            let binders = Binders::new(
+                VariableKinds::from_iter(
+                    interner,
+                    iter::repeat_with(|| VariableKind::Ty(TyVariableKind::General)).take(*len),
+                ),
+                PhantomData::<I>,
+            );
+            builder.push_binders(binders, |builder, PhantomData| {
+                let placeholders_in_scope = builder.placeholders_in_scope();
+
+                let substs = Substitution::from_iter(
+                    builder.interner(),
+                    &placeholders_in_scope[placeholders_in_scope.len() - len..],
+                );
+
+                let tuple_ty = TyKind::Tuple(*len, substs.clone()).intern(interner);
+                let sized = builder.db.well_known_trait_id(WellKnownTrait::Sized);
+                builder.push_clause(
+                    WellFormed::Ty(tuple_ty),
+                    substs.as_slice(interner)[..*len - 1]
+                        .iter()
+                        .filter_map(|s| {
+                            let ty_var = s.assert_ty_ref(interner).clone();
+                            sized.map(|id| {
+                                DomainGoal::Holds(WhereClause::Implemented(TraitRef {
+                                    trait_id: id,
+                                    substitution: Substitution::from1(interner, ty_var),
+                                }))
+                            })
+                        })
+                        .chain(substs.iter(interner).map(|subst| {
+                            DomainGoal::WellFormed(WellFormed::Ty(
+                                subst.assert_ty_ref(interner).clone(),
+                            ))
+                        })),
+                );
+            });
+        }
+        TyKind::Closure(_, _) | TyKind::Generator(_, _) | TyKind::GeneratorWitness(_, _) => {
             let ty = generalize::Generalize::apply(builder.db.interner(), ty.clone());
             builder.push_binders(ty, |builder, ty| {
                 builder.push_fact(WellFormed::Ty(ty.clone()));
             });
         }
         TyKind::Placeholder(_) => {
-            builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone())));
+            builder.push_fact(WellFormed::Ty(ty.clone()));
         }
         TyKind::Alias(AliasTy::Projection(proj)) => builder
             .db
@@ -945,30 +1053,35 @@ fn match_ty<I: Interner>(
             // - Bounds on the associated types
             // - Checking that all associated types are specified, including
             //   those on supertraits.
-            // - For trait objects with GATs, check that the bounds are fully
-            //   general (`dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
+            // - For trait objects with GATs, if we allow them in the future,
+            //   check that the bounds are fully general (
+            //   `dyn for<'a> StreamingIterator<Item<'a> = &'a ()>` is OK,
             //   `dyn StreamingIterator<Item<'static> = &'static ()>` is not).
-            let bounds = dyn_ty
-                .bounds
-                .clone()
-                .substitute(interner, &[ty.clone().cast::<GenericArg<I>>(interner)]);
-
-            let mut wf_goals = Vec::new();
-
-            wf_goals.extend(bounds.iter(interner).flat_map(|bound| {
-                bound.map_ref(|bound| -> Vec<_> {
-                    match bound {
-                        WhereClause::Implemented(trait_ref) => {
-                            vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
+            let generalized_ty =
+                generalize::Generalize::apply(builder.db.interner(), dyn_ty.clone());
+            builder.push_binders(generalized_ty, |builder, dyn_ty| {
+                let bounds = dyn_ty
+                    .bounds
+                    .clone()
+                    .substitute(interner, &[ty.clone().cast::<GenericArg<I>>(interner)]);
+
+                let mut wf_goals = Vec::new();
+
+                wf_goals.extend(bounds.iter(interner).flat_map(|bound| {
+                    bound.map_ref(|bound| -> Vec<_> {
+                        match bound {
+                            WhereClause::Implemented(trait_ref) => {
+                                vec![DomainGoal::WellFormed(WellFormed::Trait(trait_ref.clone()))]
+                            }
+                            WhereClause::AliasEq(_)
+                            | WhereClause::LifetimeOutlives(_)
+                            | WhereClause::TypeOutlives(_) => vec![],
                         }
-                        WhereClause::AliasEq(_)
-                        | WhereClause::LifetimeOutlives(_)
-                        | WhereClause::TypeOutlives(_) => vec![],
-                    }
-                })
-            }));
+                    })
+                }));
 
-            builder.push_clause(WellFormed::Ty(ty.clone()), wf_goals);
+                builder.push_clause(WellFormed::Ty(ty.clone()), wf_goals);
+            });
         }
     })
 }
diff --git a/tests/lowering/mod.rs b/tests/lowering/mod.rs
index 4a454ee706d..0a74b297132 100644
--- a/tests/lowering/mod.rs
+++ b/tests/lowering/mod.rs
@@ -806,8 +806,7 @@ fn algebraic_data_types() {
                 type Owned: Borrow<Self>;
             }
 
-            // FIXME(#435) should be `B: 'a + ToOwned`
-            enum Cow<'a, B> where B: ToOwned {
+            enum Cow<'a, B> where B: ToOwned, B: 'a {
                 Borrowed(&'a B),
                 Owned(<B as ToOwned>::Owned),
             }
diff --git a/tests/test/arrays.rs b/tests/test/arrays.rs
index a6ada8c3108..b44a61b9620 100644
--- a/tests/test/arrays.rs
+++ b/tests/test/arrays.rs
@@ -102,16 +102,37 @@ fn arrays_are_not_clone_if_element_not_clone() {
 }
 
 #[test]
-fn arrays_are_well_formed() {
+fn arrays_are_well_formed_if_elem_sized() {
     test! {
-        program { }
+        program {
+            #[lang(sized)]
+            trait Sized { }
+        }
 
         goal {
             forall<const N, T> {
-                WellFormed([T; N])
+                if (T: Sized) {
+                    WellFormed([T; N])
+                }
             }
         } yields {
             "Unique"
         }
+
+        goal {
+            forall<const N, T> {
+                WellFormed([T; N])
+            }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            exists<const N, T> {
+                WellFormed([T; N])
+            }
+        } yields {
+            "Ambiguous; no inference guidance"
+        }
     }
 }
diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs
index 1c59f03e55e..d1097eebf2a 100644
--- a/tests/test/existential_types.rs
+++ b/tests/test/existential_types.rs
@@ -417,3 +417,20 @@ fn dyn_associated_type_binding() {
         }
     }
 }
+
+#[test]
+fn dyn_well_formed() {
+    test! {
+        program {
+            trait MyTrait {}
+        }
+
+        goal {
+            exists<'s> {
+                WellFormed(dyn MyTrait + 's)
+            }
+        } yields {
+            "Unique"
+        }
+    }
+}
diff --git a/tests/test/misc.rs b/tests/test/misc.rs
index 478eafc69c2..3c506d151d3 100644
--- a/tests/test/misc.rs
+++ b/tests/test/misc.rs
@@ -815,7 +815,7 @@ fn env_bound_vars() {
                 }
             }
         } yields {
-            "Unique"
+            "Ambiguous; definite substitution for<?U0> { [?0 := '^0.0] }"
         }
         goal {
             exists<'a> {
diff --git a/tests/test/refs.rs b/tests/test/refs.rs
index d6439ce5dff..969e9bfc953 100644
--- a/tests/test/refs.rs
+++ b/tests/test/refs.rs
@@ -3,12 +3,24 @@ use super::*;
 #[test]
 fn immut_refs_are_well_formed() {
     test! {
-        program { }
+        program {
+            struct A { }
+        }
 
         goal {
-            forall<'a, T> { WellFormed(&'a T) }
+            forall<'a, T> {
+                WellFormed(&'a T)
+            }
         } yields {
-            "Unique; substitution [], lifetime constraints []"
+            "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: !1_1: '!1_0 }]"
+        }
+
+        goal {
+            exists<'a> {
+                WellFormed(&'a A)
+            }
+        } yields {
+            "Unique; for<?U0> { substitution [?0 := '^0.0], lifetime constraints [InEnvironment { environment: Env([]), goal: A: '^0.0 }] }"
         }
     }
 }
@@ -37,7 +49,7 @@ fn mut_refs_are_well_formed() {
         goal {
             forall<'a, T> { WellFormed(&'a mut T) }
         } yields {
-            "Unique; substitution [], lifetime constraints []"
+            "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: !1_1: '!1_0 }]"
         }
     }
 }
diff --git a/tests/test/slices.rs b/tests/test/slices.rs
index 89ea71dcf64..ea32740b72b 100644
--- a/tests/test/slices.rs
+++ b/tests/test/slices.rs
@@ -17,16 +17,24 @@ fn slices_are_not_sized() {
 }
 
 #[test]
-fn slices_are_well_formed() {
+fn slices_are_well_formed_if_elem_sized() {
     test! {
         program {
+            #[lang(sized)]
+            trait Sized { }
         }
 
         goal {
-            forall<T> { WellFormed([T]) }
+            forall<T> { if (T: Sized) { WellFormed([T]) } }
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        goal {
+            forall<T> { WellFormed([T]) }
+        } yields {
+            "No possible solution"
+        }
     }
 }
 
diff --git a/tests/test/tuples.rs b/tests/test/tuples.rs
index 77127ef1b3f..dd843c64228 100644
--- a/tests/test/tuples.rs
+++ b/tests/test/tuples.rs
@@ -230,3 +230,67 @@ fn tuples_are_clone() {
         }
     }
 }
+
+#[test]
+fn tuples_are_wf() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+        }
+
+        goal {
+            WellFormed(())
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            WellFormed((u8,))
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            WellFormed((u8, u8))
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            WellFormed(([u8],))
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            WellFormed((u8, [u8]))
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            WellFormed(([u8], u8))
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            exists<T> { WellFormed((T, u8)) }
+        } yields {
+            "Ambiguous; no inference guidance"
+        }
+
+        goal {
+            forall<T> { WellFormed((T, u8)) }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            forall<T> { if (T: Sized) { WellFormed((T, u8)) } }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
diff --git a/tests/test/wf_goals.rs b/tests/test/wf_goals.rs
index f375172e490..16577b42a69 100644
--- a/tests/test/wf_goals.rs
+++ b/tests/test/wf_goals.rs
@@ -107,3 +107,16 @@ fn drop_compatible() {
         }
     }
 }
+
+#[test]
+fn placeholder_wf() {
+    test! {
+        program { }
+
+        goal {
+            forall<T> { WellFormed(T) }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
diff --git a/tests/test/wf_lowering.rs b/tests/test/wf_lowering.rs
index fa7a250cc91..29b5bad08b2 100644
--- a/tests/test/wf_lowering.rs
+++ b/tests/test/wf_lowering.rs
@@ -1286,7 +1286,7 @@ fn coerce_unsized_struct() {
             #[lang(coerce_unsized)]
             trait CoerceUnsized<T> {}
 
-            struct Foo<'a, T> {
+            struct Foo<'a, T> where T: 'a {
                 t: &'a T
             }