Add const eq where clauses

Author: JulianKnodt

chalk-integration/src/lowering.rs

@@ -171,6 +171,12 @@ impl LowerWithEnv for WhereClause {
                 }),
                 chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?),
             ],
+            WhereClause::ConstProjectionEq { projection, val } => {
+                vec![chalk_ir::WhereClause::ConstEq(chalk_ir::ConstEq {
+                    term: chalk_ir::AliasTy::Projection(projection.lower(env)?),
+                    ct: val.lower(env)?,
+                })]
+            }
             WhereClause::LifetimeOutlives { a, b } => {
                 vec![chalk_ir::WhereClause::LifetimeOutlives(
                     chalk_ir::LifetimeOutlives {

chalk-integration/src/lowering/env.rs

@@ -29,7 +29,8 @@ pub type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), Ass
 pub type AssociatedTyValueIds =
     BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedTyValueId<ChalkIr>>;
 
-pub type AssociatedConstLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedConstLookup>;
+pub type AssociatedConstLookups =
+    BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedConstLookup>;
 pub type AssociatedConstValueIds =
     BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedConstValueId<ChalkIr>>;
 pub type ForeignIds = BTreeMap<Ident, chalk_ir::ForeignDefId<ChalkIr>>;

chalk-integration/src/lowering/program_lowerer.rs

@@ -361,15 +361,17 @@ impl ProgramLowerer {
                     }
 
                     for acv in &impl_defn.assoc_const_values {
-                        let acv_id = self.associated_const_value_ids[&(impl_id, acv.name.str.clone())];
-                        let lookup = &self.associated_const_lookups[&(trait_id, acv.name.str.clone())];
+                        let acv_id =
+                            self.associated_const_value_ids[&(impl_id, acv.name.str.clone())];
+                        let lookup =
+                            &self.associated_const_lookups[&(trait_id, acv.name.str.clone())];
 
                         associated_const_values.insert(
-                          acv_id,
-                          Arc::new(rust_ir::AssociatedConstValue {
-                            impl_id,
-                            associated_const_id: lookup.id,
-                          }),
+                            acv_id,
+                            Arc::new(rust_ir::AssociatedConstValue {
+                                impl_id,
+                                associated_const_id: lookup.id,
+                            }),
                         );
                     }
                 }

chalk-integration/src/program.rs

@@ -9,10 +9,10 @@ use chalk_ir::{
     Substitution, TraitId, Ty, TyKind, UintTy, Variances,
 };
 use chalk_solve::rust_ir::{
-    AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId,
-    AssociatedConstValue, AssociatedConstValueId,
-    ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum,
-    ImplDatum, ImplType, OpaqueTyDatum, TraitDatum, WellKnownTrait,
+    AdtDatum, AdtRepr, AdtSizeAlign, AssociatedConstValue, AssociatedConstValueId,
+    AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind, FnDefDatum,
+    FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum, ImplType,
+    OpaqueTyDatum, TraitDatum, WellKnownTrait,
 };
 use chalk_solve::split::Split;
 use chalk_solve::RustIrDatabase;

chalk-ir/src/debug.rs

@@ -786,11 +786,18 @@ impl<I: Interner> Debug for AliasEq<I> {
     }
 }
 
+impl<I: Interner> Debug for ConstEq<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        write!(fmt, "ConstEq(const {:?} = {:?})", self.term, self.ct)
+    }
+}
+
 impl<I: Interner> Debug for WhereClause<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         match self {
             WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()),
             WhereClause::AliasEq(a) => write!(fmt, "{:?}", a),
+            WhereClause::ConstEq(a) => write!(fmt, "{:?}", a),
             WhereClause::LifetimeOutlives(l_o) => write!(fmt, "{:?}", l_o),
             WhereClause::TypeOutlives(t_o) => write!(fmt, "{:?}", t_o),
         }

chalk-ir/src/lib.rs

@@ -728,6 +728,26 @@ impl<I: Interner> TyKind<I> {
                             dyn_flags |= alias_eq.alias.compute_flags(interner);
                             dyn_flags |= alias_eq.ty.data(interner).flags;
                         }
+                        WhereClause::ConstEq(ct_eq) => {
+                            // TODO it's not a type projection but is that fine?
+                            // TODO do I need to add other flags here?
+                            dyn_flags |= TypeFlags::HAS_TY_PROJECTION;
+                            let const_data = ct_eq.ct.data(interner);
+                            dyn_flags |= const_data.ty.data(interner).flags
+                                | match const_data.value {
+                                    ConstValue::BoundVar(_) | ConstValue::Concrete(_) => {
+                                        TypeFlags::empty()
+                                    }
+                                    ConstValue::InferenceVar(_) => {
+                                        TypeFlags::HAS_CT_INFER
+                                            | TypeFlags::STILL_FURTHER_SPECIALIZABLE
+                                    }
+                                    ConstValue::Placeholder(_) => {
+                                        TypeFlags::HAS_CT_PLACEHOLDER
+                                            | TypeFlags::STILL_FURTHER_SPECIALIZABLE
+                                    }
+                                }
+                        }
                         WhereClause::LifetimeOutlives(lifetime_outlives) => {
                             dyn_flags |= lifetime_outlives.a.compute_flags(interner)
                                 | lifetime_outlives.b.compute_flags(interner);
@@ -1743,13 +1763,16 @@ pub enum WhereClause<I: Interner> {
     LifetimeOutlives(LifetimeOutlives<I>),
     /// Type outlives a lifetime.
     TypeOutlives(TypeOutlives<I>),
+    /// Const is equal to another const
+    ConstEq(ConstEq<I>),
 }
 
 impl<I: Interner> Copy for WhereClause<I>
 where
     I::InternedSubstitution: Copy,
     I::InternedLifetime: Copy,
     I::InternedType: Copy,
+    I::InternedConst: Copy,
 {
 }
 
@@ -1908,6 +1931,7 @@ where
     I::InternedSubstitution: Copy,
     I::InternedLifetime: Copy,
     I::InternedType: Copy,
+    I::InternedConst: Copy,
 {
 }
 
@@ -1939,6 +1963,7 @@ impl<I: Interner> WhereClause<I> {
         match self {
             WhereClause::Implemented(trait_ref) => Some(trait_ref.trait_id),
             WhereClause::AliasEq(_) => None,
+            WhereClause::ConstEq(_) => None,
             WhereClause::LifetimeOutlives(_) => None,
             WhereClause::TypeOutlives(_) => None,
         }
@@ -2046,6 +2071,26 @@ impl<I: Interner> HasInterner for AliasEq<I> {
     type Interner = I;
 }
 
+/// Proves **equality** between an alias and a type.
+#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, Zip)]
+#[allow(missing_docs)]
+pub struct ConstEq<I: Interner> {
+    /// The id for the associated type member.
+    pub term: AssocItemId<I>,
+
+    pub ct: Const<I>,
+}
+impl<I: Interner> Copy for ConstEq<I>
+where
+    I::InternedSubstitution: Copy,
+    I::InternedConst: Copy,
+{
+}
+
+impl<I: Interner> HasInterner for ConstEq<I> {
+    type Interner = I;
+}
+
 /// Indicates that the `value` is universally quantified over `N`
 /// parameters of the given kinds, where `N == self.binders.len()`. A
 /// variable with depth `i < N` refers to the value at
@@ -2610,6 +2655,7 @@ pub enum GoalData<I: Interner> {
 impl<I: Interner> Copy for GoalData<I>
 where
     I::InternedType: Copy,
+    I::InternedConst: Copy,
     I::InternedLifetime: Copy,
     I::InternedGenericArg: Copy,
     I::InternedSubstitution: Copy,

chalk-parse/src/ast.rs

@@ -455,10 +455,26 @@ impl fmt::Display for Identifier {
 
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub enum WhereClause {
-    Implemented { trait_ref: TraitRef },
-    ProjectionEq { projection: ProjectionTerm, ty: Ty },
-    LifetimeOutlives { a: Lifetime, b: Lifetime },
-    TypeOutlives { ty: Ty, lifetime: Lifetime },
+    Implemented {
+        trait_ref: TraitRef,
+    },
+    ProjectionEq {
+        projection: ProjectionTerm,
+        ty: Ty,
+    },
+    ConstProjectionEq {
+        projection: ProjectionTerm,
+        val: Const,
+    },
+
+    LifetimeOutlives {
+        a: Lifetime,
+        b: Lifetime,
+    },
+    TypeOutlives {
+        ty: Ty,
+        lifetime: Lifetime,
+    },
 }
 
 #[derive(Clone, PartialEq, Eq, Debug)]

chalk-parse/src/parser.lalrpop

@@ -588,6 +588,14 @@ InlineClause: Clause = {
 WhereClause: WhereClause = {
     <t:TraitRef<":">> => WhereClause::Implemented { trait_ref: t },
 
+    <s:Ty> ":" <t:Id> "<" "const" <name:Id> "=" <val: Const> ">" => {
+        let args = vec![GenericArg::Ty(s)];
+        let trait_ref = TraitRef { trait_name: t, args: args };
+        let projection = ProjectionTerm { trait_ref, name, args: vec![] };
+
+        WhereClause::ConstProjectionEq { projection, val }
+    },
+
     // `T: Foo<U = Bar>` -- projection equality
     <s:Ty> ":" <t:Id> "<" <a:(<Comma<GenericArg>> ",")?> <name:Id> <a2:Angle<GenericArg>>
         "=" <ty:Ty> ">" =>

tests/test/projection.rs

@@ -1116,7 +1116,7 @@ fn const_projection() {
               const ID: usize;
           }
           trait OtherTrait {}
-          impl OtherTrait for U where U: ConstTrait<ID = 3> {}
+          impl OtherTrait for U where U: ConstTrait<const ID = 3> {}
           impl ConstTrait for () {
             const ID: usize = 3;
           }