Skip to content

Commit

Permalink
wf-check type annotations before normalization
Browse files Browse the repository at this point in the history
  • Loading branch information
aliemjay committed Nov 9, 2023
1 parent 69f760f commit b1cb126
Show file tree
Hide file tree
Showing 3 changed files with 62 additions and 29 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -63,13 +63,16 @@ fn relate_mir_and_user_ty<'tcx>(
user_ty: Ty<'tcx>,
) -> Result<(), NoSolution> {
let cause = ObligationCause::dummy_with_span(span);
ocx.register_obligation(Obligation::new(
ocx.infcx.tcx,
cause.clone(),
param_env,
ty::ClauseKind::WellFormed(user_ty.into()),
));

let user_ty = ocx.normalize(&cause, param_env, user_ty);
ocx.eq(&cause, param_env, mir_ty, user_ty)?;

// FIXME(#104764): We should check well-formedness before normalization.
let predicate =
ty::Binder::dummy(ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(user_ty.into())));
ocx.register_obligation(Obligation::new(ocx.infcx.tcx, cause, param_env, predicate));
Ok(())
}

Expand Down Expand Up @@ -113,31 +116,38 @@ fn relate_mir_and_user_args<'tcx>(
ocx.register_obligation(Obligation::new(tcx, cause, param_env, instantiated_predicate));
}

// Now prove the well-formedness of `def_id` with `substs`.
// Note for some items, proving the WF of `ty` is not sufficient because the
// well-formedness of an item may depend on the WF of gneneric args not present in the
// item's type. Currently this is true for associated consts, e.g.:
// ```rust
// impl<T> MyTy<T> {
// const CONST: () = { /* arbitrary code that depends on T being WF */ };
// }
// ```
for arg in args {
ocx.register_obligation(Obligation::new(
tcx,
cause.clone(),
param_env,
ty::ClauseKind::WellFormed(arg),
));
}

if let Some(UserSelfTy { impl_def_id, self_ty }) = user_self_ty {
ocx.register_obligation(Obligation::new(
tcx,
cause.clone(),
param_env,
ty::ClauseKind::WellFormed(self_ty.into()),
));

let self_ty = ocx.normalize(&cause, param_env, self_ty);
let impl_self_ty = tcx.type_of(impl_def_id).instantiate(tcx, args);
let impl_self_ty = ocx.normalize(&cause, param_env, impl_self_ty);

ocx.eq(&cause, param_env, self_ty, impl_self_ty)?;
let predicate = ty::Binder::dummy(ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(
impl_self_ty.into(),
)));
ocx.register_obligation(Obligation::new(tcx, cause.clone(), param_env, predicate));
}

// In addition to proving the predicates, we have to
// prove that `ty` is well-formed -- this is because
// the WF of `ty` is predicated on the args being
// well-formed, and we haven't proven *that*. We don't
// want to prove the WF of types from `args` directly because they
// haven't been normalized.
//
// FIXME(nmatsakis): Well, perhaps we should normalize
// them? This would only be relevant if some input
// type were ill-formed but did not appear in `ty`,
// which...could happen with normalization...
let predicate =
ty::Binder::dummy(ty::PredicateKind::Clause(ty::ClauseKind::WellFormed(ty.into())));
ocx.register_obligation(Obligation::new(tcx, cause, param_env, predicate));
Ok(())
}
9 changes: 4 additions & 5 deletions tests/ui/wf/wf-associated-const.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
// check that associated consts can assume the impl header is well-formed.

// FIXME(aliemjay): we should check the impl header is WF at the use site
// but we currently don't in some cases. This is *unsound*.

trait Foo<'a, 'b, T>: Sized {
const EVIL: fn(u: &'b u32) -> &'a u32;
}
Expand All @@ -27,11 +24,13 @@ impl<'a, 'b> Evil<'a, 'b> {
// *check* that it holds at the use site.

fn evil<'a, 'b>(b: &'b u32) -> &'a u32 {
<()>::EVIL(b) // FIXME: should be an error
<()>::EVIL(b)
//~^ ERROR lifetime may not live long enough
}

fn indirect_evil<'a, 'b>(b: &'b u32) -> &'a u32 {
<IndirectEvil>::EVIL(b) // FIXME: should be an error
<IndirectEvil>::EVIL(b)
//~^ ERROR lifetime may not live long enough
}

fn inherent_evil<'a, 'b>(b: &'b u32) -> &'a u32 {
Expand Down
28 changes: 26 additions & 2 deletions tests/ui/wf/wf-associated-const.stderr
Original file line number Diff line number Diff line change
@@ -1,5 +1,29 @@
error: lifetime may not live long enough
--> $DIR/wf-associated-const.rs:38:5
--> $DIR/wf-associated-const.rs:27:5
|
LL | fn evil<'a, 'b>(b: &'b u32) -> &'a u32 {
| -- -- lifetime `'b` defined here
| |
| lifetime `'a` defined here
LL | <()>::EVIL(b)
| ^^^^^^^^^^^^^ function was supposed to return data with lifetime `'a` but it is returning data with lifetime `'b`
|
= help: consider adding the following bound: `'b: 'a`

error: lifetime may not live long enough
--> $DIR/wf-associated-const.rs:32:5
|
LL | fn indirect_evil<'a, 'b>(b: &'b u32) -> &'a u32 {
| -- -- lifetime `'b` defined here
| |
| lifetime `'a` defined here
LL | <IndirectEvil>::EVIL(b)
| ^^^^^^^^^^^^^^^^^^^^^^^ function was supposed to return data with lifetime `'a` but it is returning data with lifetime `'b`
|
= help: consider adding the following bound: `'b: 'a`

error: lifetime may not live long enough
--> $DIR/wf-associated-const.rs:37:5
|
LL | fn inherent_evil<'a, 'b>(b: &'b u32) -> &'a u32 {
| -- -- lifetime `'b` defined here
Expand All @@ -10,5 +34,5 @@ LL | <Evil>::INHERENT_EVIL(b)
|
= help: consider adding the following bound: `'b: 'a`

error: aborting due to previous error
error: aborting due to 3 previous errors

0 comments on commit b1cb126

Please sign in to comment.