1- use chalk_ir:: {
2- Goal , InEnvironment , UCanonical
3- } ;
41use super :: search_graph:: DepthFirstNumber ;
2+ use chalk_ir:: debug;
3+ use chalk_ir:: interner:: Interner ;
4+ use chalk_ir:: { Canonical , ConstrainedSubst , Goal , InEnvironment , Substitution , UCanonical } ;
5+ use std:: fmt;
56
67pub type UCanonicalGoal < I > = UCanonical < InEnvironment < Goal < I > > > ;
78
@@ -23,3 +24,171 @@ impl Minimums {
2324 self . positive = :: std:: cmp:: min ( self . positive , minimums. positive ) ;
2425 }
2526}
27+
28+ /// A (possible) solution for a proposed goal.
29+ #[ derive( Clone , Debug , PartialEq , Eq ) ]
30+ pub enum Solution < I : Interner > {
31+ /// The goal indeed holds, and there is a unique value for all existential
32+ /// variables. In this case, we also record a set of lifetime constraints
33+ /// which must also hold for the goal to be valid.
34+ Unique ( Canonical < ConstrainedSubst < I > > ) ,
35+
36+ /// The goal may be provable in multiple ways, but regardless we may have some guidance
37+ /// for type inference. In this case, we don't return any lifetime
38+ /// constraints, since we have not "committed" to any particular solution
39+ /// yet.
40+ Ambig ( Guidance < I > ) ,
41+ }
42+
43+ /// When a goal holds ambiguously (e.g., because there are multiple possible
44+ /// solutions), we issue a set of *guidance* back to type inference.
45+ #[ derive( Clone , Debug , PartialEq , Eq ) ]
46+ pub enum Guidance < I : Interner > {
47+ /// The existential variables *must* have the given values if the goal is
48+ /// ever to hold, but that alone isn't enough to guarantee the goal will
49+ /// actually hold.
50+ Definite ( Canonical < Substitution < I > > ) ,
51+
52+ /// There are multiple plausible values for the existentials, but the ones
53+ /// here are suggested as the preferred choice heuristically. These should
54+ /// be used for inference fallback only.
55+ Suggested ( Canonical < Substitution < I > > ) ,
56+
57+ /// There's no useful information to feed back to type inference
58+ Unknown ,
59+ }
60+
61+ impl < I : Interner > Solution < I > {
62+ /// There are multiple candidate solutions, which may or may not agree on
63+ /// the values for existential variables; attempt to combine them. This
64+ /// operation does not depend on the order of its arguments.
65+ //
66+ // This actually isn't as precise as it could be, in two ways:
67+ //
68+ // a. It might be that while there are multiple distinct candidates, they
69+ // all agree about *some things*. To be maximally precise, we would
70+ // compute the intersection of what they agree on. It's not clear though
71+ // that this is actually what we want Rust's inference to do, and it's
72+ // certainly not what it does today.
73+ //
74+ // b. There might also be an ambiguous candidate and a successful candidate,
75+ // both with the same refined-goal. In that case, we could probably claim
76+ // success, since if the conditions of the ambiguous candidate were met,
77+ // we know the success would apply. Example: `?0: Clone` yields ambiguous
78+ // candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
79+ // Clone`.
80+ //
81+ // But you get the idea.
82+ pub ( crate ) fn combine ( self , other : Solution < I > , interner : & I ) -> Solution < I > {
83+ use self :: Guidance :: * ;
84+
85+ if self == other {
86+ return self ;
87+ }
88+
89+ debug ! (
90+ "combine {} with {}" ,
91+ self . display( interner) ,
92+ other. display( interner)
93+ ) ;
94+
95+ // Otherwise, always downgrade to Ambig:
96+
97+ let guidance = match ( self . into_guidance ( ) , other. into_guidance ( ) ) {
98+ ( Definite ( ref subst1) , Definite ( ref subst2) ) if subst1 == subst2 => {
99+ Definite ( subst1. clone ( ) )
100+ }
101+ ( Suggested ( ref subst1) , Suggested ( ref subst2) ) if subst1 == subst2 => {
102+ Suggested ( subst1. clone ( ) )
103+ }
104+ _ => Unknown ,
105+ } ;
106+ Solution :: Ambig ( guidance)
107+ }
108+
109+ /// View this solution purely in terms of type inference guidance
110+ pub ( crate ) fn into_guidance ( self ) -> Guidance < I > {
111+ match self {
112+ Solution :: Unique ( constrained) => Guidance :: Definite ( Canonical {
113+ value : constrained. value . subst ,
114+ binders : constrained. binders ,
115+ } ) ,
116+ Solution :: Ambig ( guidance) => guidance,
117+ }
118+ }
119+
120+ /// Extract a constrained substitution from this solution, even if ambiguous.
121+ pub ( crate ) fn constrained_subst ( & self ) -> Option < Canonical < ConstrainedSubst < I > > > {
122+ match * self {
123+ Solution :: Unique ( ref constrained) => Some ( constrained. clone ( ) ) ,
124+ Solution :: Ambig ( Guidance :: Definite ( ref canonical) )
125+ | Solution :: Ambig ( Guidance :: Suggested ( ref canonical) ) => {
126+ let value = ConstrainedSubst {
127+ subst : canonical. value . clone ( ) ,
128+ constraints : vec ! [ ] ,
129+ } ;
130+ Some ( Canonical {
131+ value,
132+ binders : canonical. binders . clone ( ) ,
133+ } )
134+ }
135+ Solution :: Ambig ( _) => None ,
136+ }
137+ }
138+
139+ /// Determine whether this solution contains type information that *must*
140+ /// hold.
141+ pub ( crate ) fn has_definite ( & self ) -> bool {
142+ match * self {
143+ Solution :: Unique ( _) => true ,
144+ Solution :: Ambig ( Guidance :: Definite ( _) ) => true ,
145+ _ => false ,
146+ }
147+ }
148+
149+ pub fn is_unique ( & self ) -> bool {
150+ match * self {
151+ Solution :: Unique ( ..) => true ,
152+ _ => false ,
153+ }
154+ }
155+
156+ pub ( crate ) fn is_ambig ( & self ) -> bool {
157+ match * self {
158+ Solution :: Ambig ( _) => true ,
159+ _ => false ,
160+ }
161+ }
162+
163+ pub fn display < ' a > ( & ' a self , interner : & ' a I ) -> SolutionDisplay < ' a , I > {
164+ SolutionDisplay {
165+ solution : self ,
166+ interner,
167+ }
168+ }
169+ }
170+
171+ pub struct SolutionDisplay < ' a , I : Interner > {
172+ solution : & ' a Solution < I > ,
173+ interner : & ' a I ,
174+ }
175+
176+ impl < ' a , I : Interner > fmt:: Display for SolutionDisplay < ' a , I > {
177+ fn fmt ( & self , f : & mut fmt:: Formatter < ' _ > ) -> Result < ( ) , fmt:: Error > {
178+ let SolutionDisplay { solution, interner } = self ;
179+ match solution {
180+ Solution :: Unique ( constrained) => write ! ( f, "Unique; {}" , constrained. display( interner) ) ,
181+ Solution :: Ambig ( Guidance :: Definite ( subst) ) => write ! (
182+ f,
183+ "Ambiguous; definite substitution {}" ,
184+ subst. display( interner)
185+ ) ,
186+ Solution :: Ambig ( Guidance :: Suggested ( subst) ) => write ! (
187+ f,
188+ "Ambiguous; suggested substitution {}" ,
189+ subst. display( interner)
190+ ) ,
191+ Solution :: Ambig ( Guidance :: Unknown ) => write ! ( f, "Ambiguous; no inference guidance" ) ,
192+ }
193+ }
194+ }
0 commit comments