Change Substitution on Array to Ty and Const

jackh726 · jackh726 · commit a16d835fbab7 · 2020-10-21T21:48:27.000-04:00
diff --git a/chalk-engine/src/slg.rs b/chalk-engine/src/slg.rs
@@ -449,10 +449,9 @@ impl<I: Interner> MayInvalidate<'_, I> {
                 self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
             }
             (TyKind::Never, TyKind::Never) => false,
-            (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => substitution_a
-                .iter(interner)
-                .zip(substitution_b.iter(interner))
-                .any(|(new, current)| self.aggregate_generic_args(new, current)),
+            (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {
+                self.aggregate_tys(ty_a, ty_b) || self.aggregate_consts(const_a, const_b)
+            }
             (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {
                 self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
             }
diff --git a/chalk-engine/src/slg/aggregate.rs b/chalk-engine/src/slg/aggregate.rs
@@ -319,16 +319,11 @@ impl<I: Interner> AntiUnifier<'_, '_, I> {
                 .map(|(&name, substitution)| TyKind::Raw(name, substitution).intern(interner))
                 .unwrap_or_else(|| self.new_ty_variable()),
             (TyKind::Never, TyKind::Never) => TyKind::Never.intern(interner),
-            (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => {
-                let substitution = Substitution::from_iter(
-                    interner,
-                    substitution_a
-                        .iter(interner)
-                        .zip(substitution_b.iter(interner))
-                        .map(|(p1, p2)| self.aggregate_generic_args(p1, p2)),
-                );
-                TyKind::Array(substitution).intern(interner)
-            }
+            (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => TyKind::Array(
+                self.aggregate_tys(ty_a, ty_b),
+                self.aggregate_consts(const_a, const_b),
+            )
+            .intern(interner),
             (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => self
                 .aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)
                 .map(|(&name, substitution)| TyKind::Closure(name, substitution).intern(interner))
diff --git a/chalk-engine/src/slg/resolvent.rs b/chalk-engine/src/slg/resolvent.rs
@@ -457,8 +457,9 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
                 Zip::zip_with(self, substitution_a, substitution_b)
             }
             (TyKind::Never, TyKind::Never) => Ok(()),
-            (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => {
-                Zip::zip_with(self, substitution_a, substitution_b)
+            (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {
+                Zip::zip_with(self, ty_a, ty_b)?;
+                Zip::zip_with(self, const_a, const_b)
             }
             (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {
                 Zip::zip_with(self, id_a, id_b)?;
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
@@ -782,14 +782,9 @@ impl LowerWithEnv for Ty {
 
             Ty::Scalar { ty } => chalk_ir::TyKind::Scalar(ty.lower()).intern(interner),
 
-            Ty::Array { ty, len } => chalk_ir::TyKind::Array(chalk_ir::Substitution::from_iter(
-                interner,
-                &[
-                    ty.lower(env)?.cast(interner),
-                    len.lower(env)?.cast(interner),
-                ],
-            ))
-            .intern(interner),
+            Ty::Array { ty, len } => {
+                chalk_ir::TyKind::Array(ty.lower(env)?, len.lower(env)?).intern(interner)
+            }
 
             Ty::Slice { ty } => chalk_ir::TyKind::Slice(chalk_ir::Substitution::from_fallible(
                 interner,
diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs
@@ -467,7 +467,7 @@ impl RustIrDatabase<ChalkIr> for Program {
                 (TyKind::Ref(id_a, _), TyKind::Ref(id_b, _)) => id_a == id_b,
                 (TyKind::Raw(id_a, _), TyKind::Raw(id_b, _)) => id_a == id_b,
                 (TyKind::Never, TyKind::Never) => true,
-                (TyKind::Array(_), TyKind::Array(_)) => true,
+                (TyKind::Array(_, _), TyKind::Array(_, _)) => true,
                 (TyKind::Closure(id_a, _), TyKind::Closure(id_b, _)) => id_a == id_b,
                 (TyKind::Generator(id_a, _), TyKind::Generator(id_b, _)) => id_a == id_b,
                 (TyKind::GeneratorWitness(id_a, _), TyKind::GeneratorWitness(id_b, _)) => {
diff --git a/chalk-ir/src/could_match.rs b/chalk-ir/src/could_match.rs
@@ -65,8 +65,8 @@ where
                         TyKind::Raw(mutability_b, substitution_b),
                     ) => mutability_a == mutability_b && matches(substitution_a, substitution_b),
                     (TyKind::Never, TyKind::Never) => true,
-                    (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => {
-                        matches(substitution_a, substitution_b)
+                    (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {
+                        ty_a.could_match(interner, ty_b) && const_a.could_match(interner, const_b)
                     }
                     (
                         TyKind::Closure(id_a, substitution_a),
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
@@ -224,7 +224,7 @@ impl<I: Interner> Debug for TyKind<I> {
                 substitution,
             ),
             TyKind::Never => write!(fmt, "Never"),
-            TyKind::Array(substitution) => write!(fmt, "{{array}}<{:?}>", substitution),
+            TyKind::Array(ty, const_) => write!(fmt, "[{:?}; {:?}]", ty, const_),
             TyKind::Closure(id, substitution) => {
                 write!(fmt, "{{closure:{:?}}}<{:?}>", id, substitution)
             }
@@ -526,9 +526,7 @@ impl<'a, I: Interner> Debug for TyKindDebug<'a, I> {
                 substitution.with_angle(interner),
             ),
             TyKind::Never => write!(fmt, "Never"),
-            TyKind::Array(substitution) => {
-                write!(fmt, "{{array}}{:?}", substitution.with_angle(interner))
-            }
+            TyKind::Array(ty, const_) => write!(fmt, "[{:?}; {:?}]", ty, const_),
             TyKind::Closure(id, substitution) => write!(
                 fmt,
                 "{{closure:{:?}}}{:?}",
diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs
@@ -474,10 +474,11 @@ where
             )
             .intern(folder.target_interner()),
             TyKind::Never => TyKind::Never.intern(folder.target_interner()),
-            TyKind::Array(substitution) => {
-                TyKind::Array(substitution.fold_with(folder, outer_binder)?)
-                    .intern(folder.target_interner())
-            }
+            TyKind::Array(ty, const_) => TyKind::Array(
+                ty.fold_with(folder, outer_binder)?,
+                const_.fold_with(folder, outer_binder)?,
+            )
+            .intern(folder.target_interner()),
             TyKind::Closure(id, substitution) => TyKind::Closure(
                 id.fold_with(folder, outer_binder)?,
                 substitution.fold_with(folder, outer_binder)?,
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
@@ -465,7 +465,7 @@ pub enum TyKind<I: Interner> {
     Tuple(usize, Substitution<I>),
 
     /// an array type like `[T; N]`
-    Array(Substitution<I>),
+    Array(Ty<I>, Const<I>),
 
     /// a slice type like `[T]`
     Slice(Substitution<I>),
@@ -544,6 +544,8 @@ where
     I::InternedSubstitution: Copy,
     I::InternedVariableKinds: Copy,
     I::InternedQuantifiedWhereClauses: Copy,
+    I::InternedType: Copy,
+    I::InternedConst: Copy,
 {
 }
 
diff --git a/chalk-ir/src/visit.rs b/chalk-ir/src/visit.rs
@@ -304,7 +304,9 @@ where
                 substitution.visit_with(visitor, outer_binder)
             }
             TyKind::Never => R::new(),
-            TyKind::Array(substitution) => substitution.visit_with(visitor, outer_binder),
+            TyKind::Array(ty, const_) => ty
+                .visit_with(visitor, outer_binder)
+                .combine(const_.visit_with(visitor, outer_binder)),
             TyKind::Closure(_id, substitution) => substitution.visit_with(visitor, outer_binder),
             TyKind::Generator(_generator, substitution) => {
                 substitution.visit_with(visitor, outer_binder)
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
@@ -46,7 +46,7 @@ fn constituent_types<I: Interner>(db: &dyn RustIrDatabase<I>, ty: &TyKind<I>) ->
             .cloned()
             .collect(),
 
-        TyKind::Array(_) | TyKind::Str | TyKind::Never | TyKind::Scalar(_) => Vec::new(),
+        TyKind::Array(_, _) | TyKind::Str | TyKind::Never | TyKind::Scalar(_) => Vec::new(),
 
         TyKind::Generator(generator_id, substitution) => {
             let generator_datum = &db.generator_datum(*generator_id);
@@ -742,7 +742,7 @@ fn match_ty<I: Interner>(
         | TyKind::Slice(_)
         | TyKind::Raw(_, _)
         | TyKind::Ref(_, _)
-        | TyKind::Array(_)
+        | TyKind::Array(_, _)
         | TyKind::Never
         | TyKind::Closure(_, _)
         | TyKind::Foreign(_, _)
diff --git a/chalk-solve/src/clauses/builtin_traits/copy.rs b/chalk-solve/src/clauses/builtin_traits/copy.rs
@@ -42,14 +42,8 @@ pub fn add_copy_program_clauses<I: Interner>(
         TyKind::Tuple(arity, substitution) => {
             push_tuple_copy_conditions(db, builder, trait_ref, *arity, substitution)
         }
-        TyKind::Array(substitution) => {
-            let interner = db.interner();
-            needs_impl_for_tys(
-                db,
-                builder,
-                trait_ref,
-                iter::once(substitution.at(interner, 0).assert_ty_ref(interner).clone()),
-            );
+        TyKind::Array(ty, _) => {
+            needs_impl_for_tys(db, builder, trait_ref, iter::once(ty.clone()));
         }
         TyKind::FnDef(_, _) => {
             builder.push_fact(trait_ref.clone());
diff --git a/chalk-solve/src/clauses/builtin_traits/sized.rs b/chalk-solve/src/clauses/builtin_traits/sized.rs
@@ -78,7 +78,7 @@ pub fn add_sized_program_clauses<I: Interner>(
         TyKind::Tuple(arity, substitution) => {
             push_tuple_sized_conditions(db, builder, trait_ref, *arity, substitution)
         }
-        TyKind::Array(_)
+        TyKind::Array(_, _)
         | TyKind::Never
         | TyKind::Closure(_, _)
         | TyKind::FnDef(_, _)
diff --git a/chalk-solve/src/clauses/builtin_traits/unsize.rs b/chalk-solve/src/clauses/builtin_traits/unsize.rs
@@ -312,12 +312,11 @@ pub fn add_unsize_program_clauses<I: Interner>(
             );
         }
 
-        (TyKind::Array(array_subst), TyKind::Slice(slice_subst)) => {
-            let array_ty = array_subst.at(interner, 0);
+        (TyKind::Array(array_ty, _array_const), TyKind::Slice(slice_subst)) => {
             let slice_ty = slice_subst.at(interner, 0);
 
             let eq_goal = EqGoal {
-                a: array_ty.clone(),
+                a: array_ty.clone().cast(interner),
                 b: slice_ty.clone(),
             };
 
diff --git a/chalk-solve/src/display/ty.rs b/chalk-solve/src/display/ty.rs
@@ -128,12 +128,7 @@ impl<I: Interner> RenderAsRust<I> for TyKind<I> {
             TyKind::Generator(..) => write!(f, "<generator>"),
             TyKind::GeneratorWitness(..) => write!(f, "<generator_witness>"),
 
-            TyKind::Array(substitution) => write!(
-                f,
-                "[{}; {}]",
-                substitution.at(interner, 0).display(s),
-                substitution.at(interner, 1).display(s),
-            ),
+            TyKind::Array(ty, const_) => write!(f, "[{}; {}]", ty.display(s), const_.display(s),),
             TyKind::Dyn(dyn_ty) => {
                 // the lifetime needs to be outside of the bounds, so we
                 // introduce a new scope for the bounds
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
@@ -198,8 +198,9 @@ impl<'t, I: Interner> Unifier<'t, I> {
                 Zip::zip_with(self, substitution_a, substitution_b)
             }
             (TyKind::Never, TyKind::Never) => Ok(()),
-            (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => {
-                Zip::zip_with(self, substitution_a, substitution_b)
+            (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {
+                Zip::zip_with(self, ty_a, ty_b)?;
+                Zip::zip_with(self, const_a, const_b)
             }
             (TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {
                 Zip::zip_with(self, id_a, id_b)?;
diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
@@ -7,7 +7,7 @@ use chalk_ir::{
     cast::*,
     fold::shift::Shift,
     interner::Interner,
-    visit::{Visit, Visitor},
+    visit::{Visit, VisitResult, Visitor},
     *,
 };
 use tracing::debug;
@@ -144,9 +144,10 @@ impl<'i, I: Interner> Visitor<'i, I> for InputTypeCollector<'i, I> {
             TyKind::Never => {
                 push_ty();
             }
-            TyKind::Array(substitution) => {
+            TyKind::Array(ty, const_) => {
                 push_ty();
-                substitution.visit_with(self, outer_binder);
+                ty.visit_with(self, outer_binder)
+                    .combine(const_.visit_with(self, outer_binder))
             }
             TyKind::Closure(_id, substitution) => {
                 push_ty();

Original file line number	Diff line number	Diff line change
`@@ -449,10 +449,9 @@ impl<I: Interner> MayInvalidate<'_, I> {`
`449`	`449`	`self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)`
`450`	`450`	`}`
`451`	`451`	`(TyKind::Never, TyKind::Never) => false,`
`452`		`- (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => substitution_a`
`453`		`- .iter(interner)`
`454`		`- .zip(substitution_b.iter(interner))`
`455`		`- .any(\|(new, current)\| self.aggregate_generic_args(new, current)),`
	`452`	`+ (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {`
	`453`	`+ self.aggregate_tys(ty_a, ty_b) \|\| self.aggregate_consts(const_a, const_b)`
	`454`	`+ }`
`456`	`455`	`(TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {`
`457`	`456`	`self.aggregate_name_and_substs(id_a, substitution_a, id_b, substitution_b)`
`458`	`457`	`}`
Original file line number	Diff line number	Diff line change
`@@ -457,8 +457,9 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {`
`457`	`457`	`Zip::zip_with(self, substitution_a, substitution_b)`
`458`	`458`	`}`
`459`	`459`	`(TyKind::Never, TyKind::Never) => Ok(()),`
`460`		`- (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => {`
`461`		`- Zip::zip_with(self, substitution_a, substitution_b)`
	`460`	`+ (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {`
	`461`	`+ Zip::zip_with(self, ty_a, ty_b)?;`
	`462`	`+ Zip::zip_with(self, const_a, const_b)`
`462`	`463`	`}`
`463`	`464`	`(TyKind::Closure(id_a, substitution_a), TyKind::Closure(id_b, substitution_b)) => {`
`464`	`465`	`Zip::zip_with(self, id_a, id_b)?;`
Original file line number	Diff line number	Diff line change
`@@ -65,8 +65,8 @@ where`
`65`	`65`	`TyKind::Raw(mutability_b, substitution_b),`
`66`	`66`	`) => mutability_a == mutability_b && matches(substitution_a, substitution_b),`
`67`	`67`	`(TyKind::Never, TyKind::Never) => true,`
`68`		`- (TyKind::Array(substitution_a), TyKind::Array(substitution_b)) => {`
`69`		`- matches(substitution_a, substitution_b)`
	`68`	`+ (TyKind::Array(ty_a, const_a), TyKind::Array(ty_b, const_b)) => {`
	`69`	`+ ty_a.could_match(interner, ty_b) && const_a.could_match(interner, const_b)`
`70`	`70`	`}`
`71`	`71`	`(`
`72`	`72`	`TyKind::Closure(id_a, substitution_a),`
Original file line number	Diff line number	Diff line change
`@@ -465,7 +465,7 @@ pub enum TyKind<I: Interner> {`
`465`	`465`	`Tuple(usize, Substitution<I>),`
`466`	`466`
`467`	`467`	/// an array type like `[T; N]`
`468`		`- Array(Substitution<I>),`
	`468`	`+ Array(Ty<I>, Const<I>),`
`469`	`469`
`470`	`470`	/// a slice type like `[T]`
`471`	`471`	`Slice(Substitution<I>),`
`@@ -544,6 +544,8 @@ where`
`544`	`544`	`I::InternedSubstitution: Copy,`
`545`	`545`	`I::InternedVariableKinds: Copy,`
`546`	`546`	`I::InternedQuantifiedWhereClauses: Copy,`
	`547`	`+ I::InternedType: Copy,`
	`548`	`+ I::InternedConst: Copy,`
`547`	`549`	`{`
`548`	`550`	`}`
`549`	`551`