WIP: Check uninhabitedness through the trait solver #116247
Conversation
rustbot
added
S-waiting-on-review
This comment has been minimized.
This comment has been minimized.
| }, | ||
| ty::Alias(ty::Opaque, _) => Err(NoSolution), | ||
| // FIXME | ||
| ty::Alias(ty::Projection | ty::Inherent, _) => Err(NoSolution), |
There was a problem hiding this comment.
We never encounter ty::Inherent unless it's not well-formed.
There was a problem hiding this comment.
The only case we'd encounter ty::Projection if it's "rigid", like T::Item in fn<T: Iterator>() {}. In that case, yeah, we don't know how to tell that it's uninhabited.
| self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes) | ||
| } | ||
| }, | ||
| ty::Alias(ty::Opaque, _) => Err(NoSolution), |
There was a problem hiding this comment.
Needs a comment saying that we don't look into the hidden type of the opaque, and it would've been revealed above.
| return self.evaluate_added_goals_and_make_canonical_response(Certainty::OVERFLOW); | ||
| }; | ||
| match ty.kind() { | ||
| ty::Never => self.evaluate_added_goals_and_make_canonical_response(Certainty::Yes), |
There was a problem hiding this comment.
Needs to return ambiguity on ty::Infer(ty::TyVar(_)) -- should also ICE on fresh tys, etc.
| @@ -141,7 +141,7 @@ pub fn type_known_to_meet_bound_modulo_regions<'tcx>( | |||
| /// Ping me on zulip if you want to use this method and need help with finding | |||
| /// an appropriate replacement. | |||
| #[instrument(level = "debug", skip(infcx, param_env, pred), ret)] | |||
| fn pred_known_to_hold_modulo_regions<'tcx>( | |||
| pub fn pred_known_to_hold_modulo_regions<'tcx>( | |||
There was a problem hiding this comment.
I'd expose a type_known_to_be_uninhabited_modulo_regions instead of exposing this fn fully
| let tcx = infcx.tcx; | ||
| for ty in tys { | ||
| let response = infcx.probe(|_| { | ||
| self.evaluate_predicates_recursively( |
There was a problem hiding this comment.
Yeah, we don't do any cycle detection with these uninhabited predicates :s
| } | ||
| } | ||
| }); | ||
| match self.evaluate_uninhabited_predicate_fields(previous_stack, obligation, module, field_tys)? { |
There was a problem hiding this comment.
We're not normalizing these field tys, are we? Does the old uninhabitedness check consider normalization?
| @@ -33,6 +34,26 @@ fn is_item_raw<'tcx>( | |||
| traits::type_known_to_meet_bound_modulo_regions(&infcx, param_env, ty, trait_def_id) | |||
| } | |||
|
|
|||
| fn type_is_uninhabited_from_raw<'tcx>( | |||
There was a problem hiding this comment.
Since we're already caching this for non-infer tys, do we need to do caching in the (old) trait solver as well?
| ty::Alias(ty::Projection | ty::Inherent, _) => Err(NoSolution), | ||
| // use a query for more complex cases | ||
| // references and other types are inhabited | ||
| _ => Err(NoSolution), |
There was a problem hiding this comment.
Can you make this exhaustive just for good measure? We prefer exhaustive matches on TyKind in the new solver "just in case" 😸
| .ok() | ||
| }) | ||
| .collect(); | ||
| self.try_merge_responses(&responses).ok_or(NoSolution) |
There was a problem hiding this comment.
need to flounder if that returns None, we also return None if there are are multiple candidates which cannot be merged. In this case we want to return ambiguity instead of NoSolution
|
☔ The latest upstream changes (presumably #116384) made this pull request unmergeable. Please resolve the merge conflicts. |
Dylan-DPC
added
S-waiting-on-author
The current implementation with the type
InhabitednessPredicatedoes not handle well normalization and aliases. This PR proposes to compute uninhabitedness using the trait solver. This allows to handle those seamlessly. This also opens way for a future potential extension to uninhabitedness to coinductive cycles (references to uninhabited for instance).This implementation is still WIP and clumsy. The logic is duplicated 3 times (once the new solver, twice the old solver). I'm not sure how to reduce that. I'm also very probably using functions that are not compatible with the solvers. It may lack a cycle check somewhere in the old solver.
This also needs a few extra tests.
r? @lcnr