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-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,21 @@ 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 +1758,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 +1926,7 @@ where
     I::InternedSubstitution: Copy,
     I::InternedLifetime: Copy,
     I::InternedType: Copy,
+    I::InternedConst: Copy,
 {
 }
 
@@ -1939,6 +1958,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 +2066,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 +2650,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

@@ -457,6 +457,8 @@ impl fmt::Display for Identifier {
 pub enum WhereClause {
     Implemented { trait_ref: TraitRef },
     ProjectionEq { projection: ProjectionTerm, ty: Ty },
+    ConstProjectionEq { projection: ProjectionTerm, val: Const },
+
     LifetimeOutlives { a: Lifetime, b: Lifetime },
     TypeOutlives { ty: Ty, lifetime: Lifetime },
 }

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;
           }