22
33pub ( super ) mod structural_traits;
44
5+ use std:: ops:: ControlFlow ;
6+
57use derive_where:: derive_where;
68use rustc_type_ir:: inherent:: * ;
79use rustc_type_ir:: lang_items:: TraitSolverLangItem ;
810use rustc_type_ir:: {
9- self as ty, Interner , TypeFoldable , TypeFolder , TypeSuperFoldable , TypeVisitableExt as _ ,
10- TypingMode , Upcast as _, elaborate,
11+ self as ty, Interner , TypeFoldable , TypeFolder , TypeSuperFoldable , TypeSuperVisitable ,
12+ TypeVisitable , TypeVisitableExt as _ , TypeVisitor , TypingMode , Upcast as _, elaborate,
1113} ;
1214use tracing:: instrument;
1315
14- use super :: has_only_region_constraints;
1516use super :: trait_goals:: TraitGoalProvenVia ;
17+ use super :: { has_only_region_constraints, inspect} ;
1618use crate :: delegate:: SolverDelegate ;
1719use crate :: solve:: inspect:: ProbeKind ;
1820use crate :: solve:: {
5052
5153 fn trait_def_id ( self , cx : I ) -> I :: DefId ;
5254
53- /// Try equating an assumption predicate against a goal's predicate. If it
54- /// holds, then execute the `then` callback, which should do any additional
55- /// work, then produce a response (typically by executing
56- /// [`EvalCtxt::evaluate_added_goals_and_make_canonical_response`]).
57- fn probe_and_match_goal_against_assumption (
58- ecx : & mut EvalCtxt < ' _ , D > ,
59- source : CandidateSource < I > ,
60- goal : Goal < I , Self > ,
61- assumption : I :: Clause ,
62- then : impl FnOnce ( & mut EvalCtxt < ' _ , D > ) -> QueryResult < I > ,
63- ) -> Result < Candidate < I > , NoSolution > ;
64-
6555 /// Consider a clause, which consists of a "assumption" and some "requirements",
6656 /// to satisfy a goal. If the requirements hold, then attempt to satisfy our
6757 /// goal by equating it with the assumption.
@@ -120,6 +110,68 @@ where
120110 alias_ty : ty:: AliasTy < I > ,
121111 ) -> Vec < Candidate < I > > ;
122112
113+ fn probe_and_consider_param_env_candidate (
114+ ecx : & mut EvalCtxt < ' _ , D > ,
115+ goal : Goal < I , Self > ,
116+ assumption : I :: Clause ,
117+ idx : usize ,
118+ ) -> Result < Candidate < I > , NoSolution > {
119+ Self :: fast_reject_assumption ( ecx, goal, assumption) ?;
120+
121+ ecx. probe ( |candidate : & Result < Candidate < I > , NoSolution > | match candidate {
122+ Ok ( candidate) => inspect:: ProbeKind :: TraitCandidate {
123+ source : candidate. source ,
124+ result : Ok ( candidate. result ) ,
125+ } ,
126+ Err ( NoSolution ) => inspect:: ProbeKind :: TraitCandidate {
127+ source : CandidateSource :: BuiltinImpl ( BuiltinImplSource :: Misc ) ,
128+ result : Err ( NoSolution ) ,
129+ } ,
130+ } )
131+ . enter ( |ecx| {
132+ Self :: match_assumption ( ecx, goal, assumption) ?;
133+ let source = ecx. characterize_param_env_assumption ( goal. param_env , assumption, idx) ?;
134+ Ok ( Candidate {
135+ source,
136+ result : ecx. evaluate_added_goals_and_make_canonical_response ( Certainty :: Yes ) ?,
137+ } )
138+ } )
139+ }
140+
141+ /// Try equating an assumption predicate against a goal's predicate. If it
142+ /// holds, then execute the `then` callback, which should do any additional
143+ /// work, then produce a response (typically by executing
144+ /// [`EvalCtxt::evaluate_added_goals_and_make_canonical_response`]).
145+ fn probe_and_match_goal_against_assumption (
146+ ecx : & mut EvalCtxt < ' _ , D > ,
147+ source : CandidateSource < I > ,
148+ goal : Goal < I , Self > ,
149+ assumption : I :: Clause ,
150+ then : impl FnOnce ( & mut EvalCtxt < ' _ , D > ) -> QueryResult < I > ,
151+ ) -> Result < Candidate < I > , NoSolution > {
152+ Self :: fast_reject_assumption ( ecx, goal, assumption) ?;
153+
154+ ecx. probe_trait_candidate ( source) . enter ( |ecx| {
155+ Self :: match_assumption ( ecx, goal, assumption) ?;
156+ then ( ecx)
157+ } )
158+ }
159+
160+ /// Try to reject the assumption based off of simple heuristics, such as [`ty::ClauseKind`]
161+ /// and [`I::DefId`].
162+ fn fast_reject_assumption (
163+ ecx : & mut EvalCtxt < ' _ , D > ,
164+ goal : Goal < I , Self > ,
165+ assumption : I :: Clause ,
166+ ) -> Result < ( ) , NoSolution > ;
167+
168+ /// Relate the goal and assumption.
169+ fn match_assumption (
170+ ecx : & mut EvalCtxt < ' _ , D > ,
171+ goal : Goal < I , Self > ,
172+ assumption : I :: Clause ,
173+ ) -> Result < ( ) , NoSolution > ;
174+
123175 fn consider_impl_candidate (
124176 ecx : & mut EvalCtxt < ' _ , D > ,
125177 goal : Goal < I , Self > ,
@@ -501,13 +553,7 @@ where
501553 candidates : & mut Vec < Candidate < I > > ,
502554 ) {
503555 for ( i, assumption) in goal. param_env . caller_bounds ( ) . iter ( ) . enumerate ( ) {
504- candidates. extend ( G :: probe_and_consider_implied_clause (
505- self ,
506- CandidateSource :: ParamEnv ( i) ,
507- goal,
508- assumption,
509- [ ] ,
510- ) ) ;
556+ candidates. extend ( G :: probe_and_consider_param_env_candidate ( self , goal, assumption, i) ) ;
511557 }
512558 }
513559
@@ -941,11 +987,20 @@ where
941987 // See `tests/ui/winnowing/norm-where-bound-gt-alias-bound.rs`.
942988 let mut considered_candidates: Vec < _ > = if candidates_from_env_and_bounds
943989 . iter ( )
944- . any ( |c| matches ! ( c. source, CandidateSource :: ParamEnv ( _) ) )
945- {
990+ . any ( |c| {
991+ matches ! (
992+ c. source,
993+ CandidateSource :: ParamEnv ( _) | CandidateSource :: GlobalParamEnv ( _)
994+ )
995+ } ) {
946996 candidates_from_env_and_bounds
947997 . into_iter ( )
948- . filter ( |c| matches ! ( c. source, CandidateSource :: ParamEnv ( _) ) )
998+ . filter ( |c| {
999+ matches ! (
1000+ c. source,
1001+ CandidateSource :: ParamEnv ( _) | CandidateSource :: GlobalParamEnv ( _)
1002+ )
1003+ } )
9491004 . map ( |c| c. result )
9501005 . collect ( )
9511006 } else {
@@ -974,7 +1029,12 @@ where
9741029 // (for example, and ideally only) when proving item bounds for an impl.
9751030 let candidates_from_env: Vec < _ > = candidates
9761031 . iter ( )
977- . filter ( |c| matches ! ( c. source, CandidateSource :: ParamEnv ( _) ) )
1032+ . filter ( |c| {
1033+ matches ! (
1034+ c. source,
1035+ CandidateSource :: ParamEnv ( _) | CandidateSource :: GlobalParamEnv ( _)
1036+ )
1037+ } )
9781038 . map ( |c| c. result )
9791039 . collect ( ) ;
9801040 if let Some ( response) = self . try_merge_responses ( & candidates_from_env) {
@@ -997,4 +1057,77 @@ where
9971057 }
9981058 }
9991059 }
1060+
1061+ fn characterize_param_env_assumption (
1062+ & mut self ,
1063+ param_env : I :: ParamEnv ,
1064+ assumption : I :: Clause ,
1065+ idx : usize ,
1066+ ) -> Result < CandidateSource < I > , NoSolution > {
1067+ // FIXME:
1068+ if assumption. has_bound_vars ( ) {
1069+ return Ok ( CandidateSource :: ParamEnv ( idx) ) ;
1070+ }
1071+
1072+ match assumption. visit_with ( & mut FindParamInClause { ecx : self , param_env } ) {
1073+ ControlFlow :: Break ( Err ( NoSolution ) ) => Err ( NoSolution ) ,
1074+ ControlFlow :: Break ( Ok ( ( ) ) ) => Ok ( CandidateSource :: ParamEnv ( idx) ) ,
1075+ ControlFlow :: Continue ( ( ) ) => Ok ( CandidateSource :: GlobalParamEnv ( idx) ) ,
1076+ }
1077+ }
1078+ }
1079+
1080+ struct FindParamInClause < ' a , ' b , D : SolverDelegate < Interner = I > , I : Interner > {
1081+ ecx : & ' a mut EvalCtxt < ' b , D > ,
1082+ param_env : I :: ParamEnv ,
1083+ }
1084+
1085+ impl < D , I > TypeVisitor < I > for FindParamInClause < ' _ , ' _ , D , I >
1086+ where
1087+ D : SolverDelegate < Interner = I > ,
1088+ I : Interner ,
1089+ {
1090+ type Result = ControlFlow < Result < ( ) , NoSolution > > ;
1091+
1092+ fn visit_binder < T : TypeFoldable < I > > ( & mut self , t : & ty:: Binder < I , T > ) -> Self :: Result {
1093+ self . ecx . enter_forall ( t. clone ( ) , |ecx, v| {
1094+ v. visit_with ( & mut FindParamInClause { ecx, param_env : self . param_env } )
1095+ } )
1096+ }
1097+
1098+ fn visit_ty ( & mut self , ty : I :: Ty ) -> Self :: Result {
1099+ let Ok ( ty) = self . ecx . structurally_normalize_ty ( self . param_env , ty) else {
1100+ return ControlFlow :: Break ( Err ( NoSolution ) ) ;
1101+ } ;
1102+ let ty = self . ecx . eager_resolve ( ty) ;
1103+
1104+ if let ty:: Placeholder ( _) = ty. kind ( ) {
1105+ ControlFlow :: Break ( Ok ( ( ) ) )
1106+ } else {
1107+ ty. super_visit_with ( self )
1108+ }
1109+ }
1110+
1111+ fn visit_const ( & mut self , ct : I :: Const ) -> Self :: Result {
1112+ let Ok ( ct) = self . ecx . structurally_normalize_const ( self . param_env , ct) else {
1113+ return ControlFlow :: Break ( Err ( NoSolution ) ) ;
1114+ } ;
1115+ let ct = self . ecx . eager_resolve ( ct) ;
1116+
1117+ if let ty:: ConstKind :: Placeholder ( _) = ct. kind ( ) {
1118+ ControlFlow :: Break ( Ok ( ( ) ) )
1119+ } else {
1120+ ct. super_visit_with ( self )
1121+ }
1122+ }
1123+
1124+ fn visit_region ( & mut self , r : I :: Region ) -> Self :: Result {
1125+ match r. kind ( ) {
1126+ ty:: ReStatic | ty:: ReError ( _) => ControlFlow :: Continue ( ( ) ) ,
1127+ ty:: ReVar ( _) | ty:: RePlaceholder ( _) => ControlFlow :: Break ( Ok ( ( ) ) ) ,
1128+ ty:: ReErased | ty:: ReEarlyParam ( _) | ty:: ReLateParam ( _) | ty:: ReBound ( ..) => {
1129+ unreachable ! ( )
1130+ }
1131+ }
1132+ }
10001133}
0 commit comments