Integer and float variable kinds

book/src/engine/logic.md

@@ -34,7 +34,7 @@ As either `Answer`s are found for the selected `Table`, entries on the stack are
 
 As mentioned before, whenever a new `Goal` is encounted, a new [`Table`] is
 created to store current and future answers. First, the [`Goal`] is converted into
-an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more
+an `HhGoal`. If it can be simplified, then a `Strand` with one or more
 subgoals will be generated and can be followed as above. Otherwise, if it is a
 `DomainGoal` (see above), then
 [`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses)
@@ -123,7 +123,6 @@ For much more in-depth
 
 [`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html
 [`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
-[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html
 [`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html
 [`StackEntry`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.StackEntry.html
 [`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html

book/src/engine/major_concepts.md

@@ -16,7 +16,7 @@ opaque to the engine internals. Functions in the trait are agnostic to specific
 program or environment details, since they lack a `&self` argument.
 
 To give an example, there is an associated [`Goal`] type. However, Chalk doesn't
-know how to solve this. Instead, it has to be converted an [`HhGoal`] via the
+know how to solve this. Instead, it has to be converted an `HhGoal` via the
 `Context::into_hh_goal` function. This will be coverted more in the `Goals`
 section.
 
@@ -38,7 +38,7 @@ change the state of the logic itself.
 ## Goals
 
 A "goal" in Chalk can be thought of as "something we want to prove". The engine
-itself understands [`HhGoal`]s. `HHGoal`s consist of the most basic logic,
+itself understands `HhGoal`s. `HHGoal`s consist of the most basic logic,
 such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`).
 On the other hand, `Context::Goal` represents an opaque goal generated
 externally. As such, it may contain any extra information or may be interned.
@@ -111,7 +111,6 @@ stack).
 [`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
 [`ContextOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html
 [`InferenceTable`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.InferenceTable.html
-[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html
 [`Solution`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Solution
 [`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html
 [`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html

chalk-integration/src/lowering.rs

@@ -3,7 +3,7 @@ use chalk_ir::cast::{Cast, Caster};
 use chalk_ir::interner::HasInterner;
 use chalk_ir::{
     self, AdtId, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, FnDefId, ImplId, OpaqueTyId,
-    QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId,
+    QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId, TyKind,
 };
 use chalk_parse::ast::*;
 use chalk_solve::rust_ir::{
@@ -90,7 +90,7 @@ impl<'k> Env<'k> {
         if let Some(p) = self.parameter_map.get(&name.str) {
             let b = p.skip_kind();
             return match &p.kind {
-                chalk_ir::VariableKind::Ty => Ok(chalk_ir::TyData::BoundVar(*b)
+                chalk_ir::VariableKind::Ty(_) => Ok(chalk_ir::TyData::BoundVar(*b)
                     .intern(interner)
                     .cast(interner)),
                 chalk_ir::VariableKind::Lifetime => Ok(chalk_ir::LifetimeData::BoundVar(*b)
@@ -506,7 +506,7 @@ impl LowerProgram for Program {
                             let bounds: chalk_ir::Binders<Vec<chalk_ir::Binders<_>>> = env
                                 .in_binders(
                                     Some(chalk_ir::WithKind::new(
-                                        chalk_ir::VariableKind::Ty,
+                                        chalk_ir::VariableKind::Ty(TyKind::General),
                                         Atom::from(FIXME_SELF),
                                     )),
                                     |env1| {
@@ -681,7 +681,7 @@ impl LowerParameterMap for AssocTyValue {
 impl LowerParameterMap for TraitDefn {
     fn synthetic_parameters(&self) -> Option<chalk_ir::WithKind<ChalkIr, Ident>> {
         Some(chalk_ir::WithKind::new(
-            chalk_ir::VariableKind::Ty,
+            chalk_ir::VariableKind::Ty(TyKind::General),
             Atom::from(SELF),
         ))
     }
@@ -717,9 +717,18 @@ trait LowerVariableKind {
 impl LowerVariableKind for VariableKind {
     fn lower(&self) -> chalk_ir::WithKind<ChalkIr, Ident> {
         match self {
-            VariableKind::Ty(n) => {
-                chalk_ir::WithKind::new(chalk_ir::VariableKind::Ty, n.str.clone())
-            }
+            VariableKind::Ty(n) => chalk_ir::WithKind::new(
+                chalk_ir::VariableKind::Ty(chalk_ir::TyKind::General),
+                n.str.clone(),
+            ),
+            VariableKind::IntegerTy(n) => chalk_ir::WithKind::new(
+                chalk_ir::VariableKind::Ty(chalk_ir::TyKind::Integer),
+                n.str.clone(),
+            ),
+            VariableKind::FloatTy(n) => chalk_ir::WithKind::new(
+                chalk_ir::VariableKind::Ty(chalk_ir::TyKind::Float),
+                n.str.clone(),
+            ),
             VariableKind::Lifetime(n) => {
                 chalk_ir::WithKind::new(chalk_ir::VariableKind::Lifetime, n.str.clone())
             }
@@ -1290,7 +1299,7 @@ impl LowerTy for Ty {
                 bounds: env.in_binders(
                     // FIXME: Figure out a proper name for this type parameter
                     Some(chalk_ir::WithKind::new(
-                        chalk_ir::VariableKind::Ty,
+                        chalk_ir::VariableKind::Ty(TyKind::General),
                         Atom::from(FIXME_SELF),
                     )),
                     |env| {
@@ -1820,6 +1829,8 @@ impl Kinded for VariableKind {
     fn kind(&self) -> Kind {
         match *self {
             VariableKind::Ty(_) => Kind::Ty,
+            VariableKind::IntegerTy(_) => Kind::Ty,
+            VariableKind::FloatTy(_) => Kind::Ty,
             VariableKind::Lifetime(_) => Kind::Lifetime,
             VariableKind::Const(_) => Kind::Const,
         }
@@ -1829,7 +1840,7 @@ impl Kinded for VariableKind {
 impl Kinded for chalk_ir::VariableKind<ChalkIr> {
     fn kind(&self) -> Kind {
         match self {
-            chalk_ir::VariableKind::Ty => Kind::Ty,
+            chalk_ir::VariableKind::Ty(_) => Kind::Ty,
             chalk_ir::VariableKind::Lifetime => Kind::Lifetime,
             chalk_ir::VariableKind::Const(_) => Kind::Const,
         }

chalk-ir/src/debug.rs

@@ -179,7 +179,9 @@ impl<I: Interner> Debug for TyData<I> {
         match self {
             TyData::BoundVar(db) => write!(fmt, "{:?}", db),
             TyData::Dyn(clauses) => write!(fmt, "{:?}", clauses),
-            TyData::InferenceVar(var) => write!(fmt, "{:?}", var),
+            TyData::InferenceVar(var, TyKind::General) => write!(fmt, "{:?}", var),
+            TyData::InferenceVar(var, TyKind::Integer) => write!(fmt, "{:?}i", var),
+            TyData::InferenceVar(var, TyKind::Float) => write!(fmt, "{:?}f", var),
             TyData::Apply(apply) => write!(fmt, "{:?}", apply),
             TyData::Alias(alias) => write!(fmt, "{:?}", alias),
             TyData::Placeholder(index) => write!(fmt, "{:?}", index),
@@ -276,7 +278,9 @@ impl<'a, I: Interner> Debug for VariableKindsInnerDebug<'a, I> {
                 write!(fmt, ", ")?;
             }
             match binder {
-                VariableKind::Ty => write!(fmt, "type")?,
+                VariableKind::Ty(TyKind::General) => write!(fmt, "type")?,
+                VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type")?,
+                VariableKind::Ty(TyKind::Float) => write!(fmt, "float type")?,
                 VariableKind::Lifetime => write!(fmt, "lifetime")?,
                 VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty)?,
             }
@@ -765,7 +769,9 @@ impl<I: Interner> Debug for GenericArgData<I> {
 impl<I: Interner> Debug for VariableKind<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         match self {
-            VariableKind::Ty => write!(fmt, "type"),
+            VariableKind::Ty(TyKind::General) => write!(fmt, "type"),
+            VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type"),
+            VariableKind::Ty(TyKind::Float) => write!(fmt, "float type"),
             VariableKind::Lifetime => write!(fmt, "lifetime"),
             VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty),
         }
@@ -776,7 +782,9 @@ impl<I: Interner, T: Debug> Debug for WithKind<I, T> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         let value = self.skip_kind();
         match &self.kind {
-            VariableKind::Ty => write!(fmt, "{:?} with kind type", value),
+            VariableKind::Ty(TyKind::General) => write!(fmt, "{:?} with kind type", value),
+            VariableKind::Ty(TyKind::Integer) => write!(fmt, "{:?} with kind integer type", value),
+            VariableKind::Ty(TyKind::Float) => write!(fmt, "{:?} with kind float type", value),
             VariableKind::Lifetime => write!(fmt, "{:?} with kind lifetime", value),
             VariableKind::Const(ty) => write!(fmt, "{:?} with kind {:?}", value, ty),
         }

chalk-ir/src/fold.rs

@@ -267,12 +267,13 @@ where
     fn fold_inference_ty(
         &mut self,
         var: InferenceVar,
+        kind: TyKind,
         outer_binder: DebruijnIndex,
     ) -> Fallible<Ty<TI>> {
         if self.forbid_inference_vars() {
             panic!("unexpected inference type `{:?}`", var)
         } else {
-            Ok(var.to_ty(self.target_interner()))
+            Ok(var.to_ty(self.target_interner(), kind))
         }
     }
 
@@ -416,7 +417,7 @@ where
             }
             TyData::Dyn(clauses) => Ok(TyData::Dyn(clauses.fold_with(folder, outer_binder)?)
                 .intern(folder.target_interner())),
-            TyData::InferenceVar(var) => folder.fold_inference_ty(*var, outer_binder),
+            TyData::InferenceVar(var, kind) => folder.fold_inference_ty(*var, *kind, outer_binder),
             TyData::Apply(apply) => Ok(TyData::Apply(apply.fold_with(folder, outer_binder)?)
                 .intern(folder.target_interner())),
             TyData::Placeholder(ui) => Ok(folder.fold_free_placeholder_ty(*ui, outer_binder)?),

chalk-ir/src/lib.rs

@@ -320,7 +320,7 @@ impl<I: Interner> Ty<I> {
 
     /// If this is a `TyData::InferenceVar(d)`, returns `Some(d)` else `None`.
     pub fn inference_var(&self, interner: &I) -> Option<InferenceVar> {
-        if let TyData::InferenceVar(depth) = self.data(interner) {
+        if let TyData::InferenceVar(depth, _) = self.data(interner) {
             Some(*depth)
         } else {
             None
@@ -330,7 +330,7 @@ impl<I: Interner> Ty<I> {
     /// Returns true if this is a `BoundVar` or `InferenceVar`.
     pub fn is_var(&self, interner: &I) -> bool {
         match self.data(interner) {
-            TyData::BoundVar(_) | TyData::InferenceVar(_) => true,
+            TyData::BoundVar(_) | TyData::InferenceVar(_, _) => true,
             _ => false,
         }
     }
@@ -342,6 +342,32 @@ impl<I: Interner> Ty<I> {
         }
     }
 
+    /// Returns true if this is an `IntTy` or `UintTy`
+    pub fn is_integer(&self, interner: &I) -> bool {
+        match self.data(interner) {
+            TyData::Apply(ApplicationTy {
+                name: TypeName::Scalar(Scalar::Int(_)),
+                ..
+            })
+            | TyData::Apply(ApplicationTy {
+                name: TypeName::Scalar(Scalar::Uint(_)),
+                ..
+            }) => true,
+            _ => false,
+        }
+    }
+
+    /// Returns true if this is a `FloatTy`
+    pub fn is_float(&self, interner: &I) -> bool {
+        match self.data(interner) {
+            TyData::Apply(ApplicationTy {
+                name: TypeName::Scalar(Scalar::Float(_)),
+                ..
+            }) => true,
+            _ => false,
+        }
+    }
+
     /// True if this type contains "bound" types/lifetimes, and hence
     /// needs to be shifted across binders. This is a very inefficient
     /// check, intended only for debug assertions, because I am lazy.
@@ -390,7 +416,7 @@ pub enum TyData<I: Interner> {
     BoundVar(BoundVar),
 
     /// Inference variable defined in the current inference context.
-    InferenceVar(InferenceVar),
+    InferenceVar(InferenceVar, TyKind),
 }
 
 impl<I: Interner> TyData<I> {
@@ -682,8 +708,8 @@ impl InferenceVar {
         self.index
     }
 
-    pub fn to_ty<I: Interner>(self, interner: &I) -> Ty<I> {
-        TyData::<I>::InferenceVar(self).intern(interner)
+    pub fn to_ty<I: Interner>(self, interner: &I, kind: TyKind) -> Ty<I> {
+        TyData::<I>::InferenceVar(self, kind).intern(interner)
     }
 
     pub fn to_lifetime<I: Interner>(self, interner: &I) -> Lifetime<I> {
@@ -910,17 +936,34 @@ impl<I: Interner> ApplicationTy<I> {
     }
 }
 
+/// Represents some extra knowledge we may have about the type variable.
+/// ```ignore
+/// let x: &[u32];
+/// let i = 1;
+/// x[i]
+/// ```
+/// In this example, `i` is known to be some type of integer. We can infer that
+/// it is `usize` because that is the only integer type that slices have an
+/// `Index` impl for. `i` would have a `TyKind` of `Integer` to guide the
+/// inference process.
+#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
+pub enum TyKind {
+    General,
+    Integer,
+    Float,
+}
+
 #[derive(Clone, PartialEq, Eq, Hash)]
 pub enum VariableKind<I: Interner> {
-    Ty,
+    Ty(TyKind),
     Lifetime,
     Const(Ty<I>),
 }
 
 impl<I: Interner> VariableKind<I> {
     fn to_bound_variable(&self, interner: &I, bound_var: BoundVar) -> GenericArg<I> {
         match self {
-            VariableKind::Ty => {
+            VariableKind::Ty(_) => {
                 GenericArgData::Ty(TyData::BoundVar(bound_var).intern(interner)).intern(interner)
             }
             VariableKind::Lifetime => {
@@ -1524,7 +1567,7 @@ impl<T: HasInterner> Binders<T> {
         // The new variable is at the front and everything afterwards is shifted up by 1
         let new_var = TyData::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner);
         let value = op(new_var);
-        let binders = VariableKinds::from(interner, iter::once(VariableKind::Ty));
+        let binders = VariableKinds::from(interner, iter::once(VariableKind::Ty(TyKind::General)));
         Binders { binders, value }
     }
 
@@ -1940,7 +1983,7 @@ impl<T: HasInterner> UCanonical<T> {
                 .map(|(index, pk)| {
                     let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index);
                     match &pk.kind {
-                        VariableKind::Ty => {
+                        VariableKind::Ty(_) => {
                             GenericArgData::Ty(TyData::BoundVar(bound_var).intern(interner))
                                 .intern(interner)
                         }

chalk-ir/src/visit.rs

@@ -273,7 +273,7 @@ where
                 }
             }
             TyData::Dyn(clauses) => clauses.visit_with(visitor, outer_binder),
-            TyData::InferenceVar(var) => visitor.visit_inference_var(*var, outer_binder),
+            TyData::InferenceVar(var, _) => visitor.visit_inference_var(*var, outer_binder),
             TyData::Apply(apply) => apply.visit_with(visitor, outer_binder),
             TyData::Placeholder(ui) => visitor.visit_free_placeholder(*ui, outer_binder),
             TyData::Alias(proj) => proj.visit_with(visitor, outer_binder),

chalk-ir/src/zip.rs

@@ -308,14 +308,14 @@ impl<I: Interner> Zip<I> for VariableKind<I> {
         I: 'i,
     {
         match (a, b) {
-            (VariableKind::Ty, VariableKind::Ty) => Ok(()),
+            (VariableKind::Ty(a), VariableKind::Ty(b)) if a == b => Ok(()),
             (VariableKind::Lifetime, VariableKind::Lifetime) => Ok(()),
             (VariableKind::Const(ty_a), VariableKind::Const(ty_b)) => {
                 Zip::zip_with(zipper, ty_a, ty_b)
             }
-            (VariableKind::Ty, _) | (VariableKind::Lifetime, _) | (VariableKind::Const(_), _) => {
-                panic!("zipping things of mixed kind")
-            }
+            (VariableKind::Ty(_), _)
+            | (VariableKind::Lifetime, _)
+            | (VariableKind::Const(_), _) => panic!("zipping things of mixed kind"),
         }
     }
 }

chalk-parse/src/ast.rs

@@ -100,6 +100,8 @@ pub struct OpaqueTyDefn {
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub enum VariableKind {
     Ty(Identifier),
+    IntegerTy(Identifier),
+    FloatTy(Identifier),
     Lifetime(Identifier),
     Const(Identifier),
 }

chalk-parse/src/parser.lalrpop

@@ -201,6 +201,8 @@ VariableKind: VariableKind = {
     Id => VariableKind::Ty(<>),
     LifetimeId => VariableKind::Lifetime(<>),
     "const" <id:Id> => VariableKind::Const(id),
+    "int" <id:Id> => VariableKind::IntegerTy(id),
+    "float" <id:Id> => VariableKind::FloatTy(id),
 };
 
 AssocTyValue: AssocTyValue = {

chalk-solve/src/clauses.rs

@@ -260,7 +260,7 @@ fn program_clauses_that_could_match<I: Interner>(
                         }
                         _ => {}
                     },
-                    TyData::InferenceVar(_) | TyData::BoundVar(_) => {
+                    TyData::InferenceVar(_, _) | TyData::BoundVar(_) => {
                         return Err(Floundered);
                     }
                     _ => {}
@@ -459,7 +459,7 @@ fn match_ty<I: Interner>(
                 .map(|ty| match_ty(builder, environment, &ty))
                 .collect::<Result<_, Floundered>>()?;
         }
-        TyData::BoundVar(_) | TyData::InferenceVar(_) => return Err(Floundered),
+        TyData::BoundVar(_) | TyData::InferenceVar(_, _) => return Err(Floundered),
         TyData::Dyn(_) => {}
     })
 }

chalk-solve/src/clauses/builder.rs

@@ -149,7 +149,7 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
     pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>)) {
         let interner = self.interner();
         let binders = Binders::new(
-            VariableKinds::from(interner, iter::once(VariableKind::Ty)),
+            VariableKinds::from(interner, iter::once(VariableKind::Ty(TyKind::General))),
             PhantomData::<I>,
         );
         self.push_binders(&binders, |this, PhantomData| {