Implement normalization fallback via lowering

This commit introduces a new domain goal: `KnownProjection`. It holds
whenever you're able to directly normalize a projection, i.e. through an
impl or where clause. Normalizations are then expanded to include a
fallback precisely in the cases where `KnownProjection` cannot be proved.

Author: aturon

src/fold/mod.rs

@@ -196,7 +196,7 @@ macro_rules! enum_fold {
 }
 
 enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
-enum_fold!(DomainGoal[] { Implemented(a), Normalize(a), WellFormed(a) });
+enum_fold!(DomainGoal[] { Implemented(a), KnownProjection(a), Normalize(a), WellFormed(a) });
 enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
 enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
 enum_fold!(Constraint[] { LifetimeEq(a, b) });

src/fold/shifter.rs

@@ -34,6 +34,7 @@ up_shift_method!(Ty);
 up_shift_method!(Parameter);
 up_shift_method!(Lifetime);
 up_shift_method!(TraitRef);
+up_shift_method!(ProjectionTy);
 
 impl Folder for Shifter {
     fn fold_free_var(&mut self, depth: usize, binders: usize) -> Result<Ty> {

src/ir/debug.rs

@@ -149,6 +149,7 @@ impl Debug for DomainGoal {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match *self {
             DomainGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
+            DomainGoal::KnownProjection(ref n) => write!(fmt, "known {{ {:?} }}", n),
             DomainGoal::Implemented(ref n) => {
                 write!(fmt,
                        "{:?}: {:?}{:?}",

src/ir/mod.rs

@@ -136,6 +136,11 @@ impl Environment {
                         parameters: trait_params.to_owned()
                     };
                     push_clause(trait_ref.cast());
+
+                    // <T as Trait<U>>::Foo ===> V
+                    // ----------------------------------------------------------
+                    // known { Trait<U>::Foo<T> }
+                    push_clause(DomainGoal::KnownProjection(projection.clone()));
                 }
                 _ => {}
             }
@@ -259,6 +264,9 @@ pub struct AssociatedTyDatum {
     /// The trait this associated type is defined in.
     pub trait_id: ItemId,
 
+    /// The ID of this associated type
+    pub id: ItemId,
+
     /// Name of this associated type.
     pub name: Identifier,
 
@@ -389,6 +397,8 @@ pub struct TraitRef {
 /// decomposing this enum, and instead treat its values opaquely.
 pub enum DomainGoal {
     Implemented(TraitRef),
+    /// Is the projection something we know definitively from impls?
+    KnownProjection(ProjectionTy),
     Normalize(Normalize),
     WellFormed(WellFormed),
 }

src/lower/mod.rs

@@ -170,6 +170,7 @@ impl LowerProgram for Program {
 
                         associated_ty_data.insert(info.id, ir::AssociatedTyDatum {
                             trait_id: item_id,
+                            id: info.id,
                             name: defn.name.str,
                             parameter_kinds: parameter_kinds,
                             where_clauses: vec![ir::DomainGoal::Implemented(trait_ref)]
@@ -194,11 +195,19 @@ trait LowerParameterMap {
     fn synthetic_parameters(&self) -> Option<ir::ParameterKind<ir::Identifier>>;
     fn declared_parameters(&self) -> &[ParameterKind];
     fn all_parameters(&self) -> Vec<ir::ParameterKind<ir::Identifier>> {
+        self.synthetic_parameters()
+            .into_iter()
+            .chain(self.declared_parameters().iter().map(|id| id.lower()))
+            .collect()
+
+        /* TODO: switch to this ordering, but adjust *all* the code to match
+
         self.declared_parameters()
             .iter()
             .map(|id| id.lower())
-            .chain(self.synthetic_parameters()) // (*) see above
+            .chain(self.synthetic_parameters()) // (*) see below
             .collect()
+         */
     }
 
     fn parameter_refs(&self) -> Vec<ir::Parameter> {
@@ -756,6 +765,7 @@ impl ir::Program {
 
         program_clauses.extend(self.struct_data.values().flat_map(|d| d.to_program_clauses()));
         program_clauses.extend(self.trait_data.values().flat_map(|d| d.to_program_clauses()));
+        program_clauses.extend(self.associated_ty_data.values().flat_map(|d| d.to_program_clauses()));
 
         for datum in self.impl_data.values() {
             program_clauses.push(datum.to_program_clause());
@@ -805,6 +815,10 @@ impl ir::AssociatedTyValue {
     ///     (Vec<T>: Iterable<IntoIter<'a> = Iter<'a, T>>) :-
     ///         (Vec<T>: Iterable),  // (1)
     ///         (T: 'a)              // (2)
+    ///
+    ///     known(Iterable::IntoIter<Vec<T>, 'a>) :-
+    ///         (Vec<T>: Iterable),  // (1)
+    ///         (T: 'a)              // (2)
     /// }
     /// ```
     fn to_program_clauses(&self, impl_datum: &ir::ImplDatum) -> Vec<ir::ProgramClause> {
@@ -828,35 +842,45 @@ impl ir::AssociatedTyValue {
             .chain(self.value.value.where_clauses.clone().cast())
             .collect();
 
-        // The consequence is that the normalization holds.
-        let consequence = {
+        let projection = {
             // First add refs to the bound parameters (`'a`, in above example)
             let parameters = self.value.binders.iter().zip(0..).map(|p| p.to_parameter());
 
             // Then add the trait-ref parameters (`Vec<T>`, in above example)
             let parameters = parameters.chain(impl_trait_ref.parameters.clone());
 
-            // Construct normalization predicate
-            ir::Normalize {
-                projection: ir::ProjectionTy {
-                    associated_ty_id: self.associated_ty_id,
-                    parameters: parameters.collect(),
-                },
-                ty: self.value.value.ty.clone()
+            ir::ProjectionTy {
+                associated_ty_id: self.associated_ty_id,
+                parameters: parameters.collect(),
             }
         };
 
-        let pos_clause = ir::ProgramClause {
+        // Determine the normalization
+        let norm_clause = ir::ProgramClause {
             implication: ir::Binders {
                 binders: all_binders.clone(),
                 value: ir::ProgramClauseImplication {
-                    consequence: consequence.clone().cast(),
-                    conditions: conditions,
+                    consequence: ir::DomainGoal::Normalize(ir::Normalize {
+                        projection: projection.clone(),
+                        ty: self.value.value.ty.clone()
+                    }),
+                    conditions: conditions.clone(),
                 }
             }
         };
 
-        vec![pos_clause]
+        // Record that the projection is known
+        let known_clause = ir::ProgramClause {
+            implication: ir::Binders {
+                binders: all_binders.clone(),
+                value: ir::ProgramClauseImplication {
+                    consequence: ir::DomainGoal::KnownProjection(projection),
+                    conditions: conditions.clone(),
+                }
+            }
+        };
+
+        vec![norm_clause, known_clause]
     }
 }
 
@@ -957,3 +981,49 @@ impl ir::TraitDatum {
         vec![wf]
     }
 }
+
+impl ir::AssociatedTyDatum {
+    fn to_program_clauses(&self) -> Vec<ir::ProgramClause> {
+        // For each associated type, we have a "normalization fallback" clause.
+        //
+        // Given:
+        //
+        //    trait SomeTrait {
+        //        type Assoc;
+        //    }
+        //
+        // we generate:
+        //
+        //    ?T: SomeTrait<Assoc = (SomeTrait::Assoc)<?T>> :-
+        //      // we can't resolve the normalization through an impl clause
+        //      not { known { <?T as SomeTrait>::Assoc } }.
+
+        let binders: Vec<_> = self.parameter_kinds.iter().map(|pk| pk.map(|_| ())).collect();
+        let parameters: Vec<_> = binders.iter().zip(0..).map(|p| p.to_parameter()).collect();
+
+        let projection = ir::ProjectionTy {
+            associated_ty_id: self.id,
+            parameters: parameters.clone(),
+        };
+
+        // Construct an application from the projection. So if we have `<T as
+        // Iterator>::Item`, we would produce `(Iterator::Item)<T>`.
+        let app = ir::ApplicationTy { name: ir::TypeName::AssociatedType(self.id), parameters };
+        let fallback_ty = ir::Ty::Apply(app);
+        let norm_fallback = ir::Normalize { projection: projection.clone(), ty: fallback_ty };
+
+        let fallback = ir::ProgramClause {
+            implication: ir::Binders {
+                binders,
+                value: ir::ProgramClauseImplication {
+                    consequence: ir::DomainGoal::Normalize(norm_fallback),
+                    conditions: vec![
+                        ir::Goal::Not(Box::new(ir::DomainGoal::KnownProjection(projection).cast()))
+                    ]
+                }
+            }
+        };
+
+        vec![fallback]
+    }
+}

src/solve/test.rs

@@ -290,37 +290,23 @@ fn normalize() {
             "Unique; substitution [?0 := u32], lifetime constraints []"
         }
 
-        // TODO: re-enable this once normalization fallback is reimplemented
-
-        // goal {
-        //     forall<T> {
-        //         if (T: Iterator) {
-        //             exists<U> {
-        //                 T: Iterator<Item = U>
-        //             }
-        //         }
-        //     }
-        // } yields {
-        //     "Solution {
-        //         successful: Yes,
-        //         refined_goal: Query {
-        //             value: Constrained {
-        //                 value: [
-        //                     <!1 as Iterator>::Item ==> (Iterator::Item)<!1>
-        //                 ],
-        //                 constraints: []
-        //             },
-        //             binders: []
-        //         }
-        //     }"
-        // }
+        goal {
+            forall<T> {
+                if (T: Iterator) {
+                    exists<U> {
+                        T: Iterator<Item = U>
+                    }
+                }
+            }
+        } yields {
+            "Unique; substitution [?0 := (Iterator::Item)<!1>]"
+        }
     }
 }
 
 /// Demonstrates that, given the expected value of the associated
 /// type, we can use that to narrow down the relevant impls.
-// TODO: re-enable once normalization fallback is reimplemented
-//#[test]
+#[test]
 fn normalize_rev_infer() {
     test! {
         program {
@@ -336,18 +322,7 @@ fn normalize_rev_infer() {
                 T: Identity<Item = u32>
             }
         } yields {
-            "Solution {
-                successful: Yes,
-                refined_goal: Query {
-                    value: Constrained {
-                        value: [
-                            <u32 as Identity>::Item ==> u32
-                        ],
-                        constraints: []
-                    },
-                    binders: []
-                }
-            }"
+            "Unique; substitution [?0 := u32]"
         }
     }
 }
@@ -861,8 +836,7 @@ fn mixed_indices_match_program() {
     }
 }
 
-// TODO: re-enable once normalization fallback is reimplemented
-//#[test]
+#[test]
 fn mixed_indices_normalize_application() {
     test! {
         program {
@@ -881,15 +855,15 @@ fn mixed_indices_normalize_application() {
                 }
             }
         } yields {
-            "Solution { successful: Yes"
+            "Ambig"
         }
     }
 }
 
 #[test]
 // Test that we properly detect failure even if there are applicable impls at
 // the top level, if we can't find anything to fill in those impls with
-fn test_deep_failure() {
+fn deep_failure() {
     test! {
         program {
             struct Foo<T> {}
@@ -916,7 +890,7 @@ fn test_deep_failure() {
 #[test]
 // Test that we infer a unique solution even if it requires multiple levels of
 // search to do so
-fn test_deep_success() {
+fn deep_success() {
     test! {
         program {
             struct Foo<T> {}
@@ -938,7 +912,7 @@ fn test_deep_success() {
 
 
 #[test]
-fn test_definite_guidance() {
+fn definite_guidance() {
     test! {
         program {
             trait Display {}
@@ -964,7 +938,7 @@ fn test_definite_guidance() {
 }
 
 #[test]
-fn test_suggested_subst() {
+fn suggested_subst() {
     test! {
         program {
             trait SomeTrait<A> {}
@@ -1070,7 +1044,7 @@ fn test_suggested_subst() {
 }
 
 #[test]
-fn test_simple_negation() {
+fn simple_negation() {
     test! {
         program {
             struct i32 {}
@@ -1128,7 +1102,7 @@ fn test_simple_negation() {
 }
 
 #[test]
-fn test_deep_negation() {
+fn deep_negation() {
     test! {
         program {
             struct Foo<T> {}
@@ -1157,7 +1131,7 @@ fn test_deep_negation() {
 }
 
 #[test]
-fn test_negation_quantifiers() {
+fn negation_quantifiers() {
     test! {
         program {
             struct i32 {}

src/zip.rs

@@ -155,6 +155,6 @@ macro_rules! enum_zip {
     }
 }
 
-enum_zip!(DomainGoal { Implemented, Normalize, WellFormed });
+enum_zip!(DomainGoal { Implemented, KnownProjection, Normalize, WellFormed });
 enum_zip!(LeafGoal { DomainGoal, EqGoal });
 enum_zip!(WellFormed { Ty, TraitRef });