4 files changed, 319 insertions, 282 deletions

diff --git a/crates/hir_ty/src/infer/coerce.rs b/crates/hir_ty/src/infer/coerce.rs
index 32c7c57cd..cf0a3add4 100644
--- a/crates/hir_ty/src/infer/coerce.rs
+++ b/crates/hir_ty/src/infer/coerce.rs
@@ -4,12 +4,13 @@
 //!
 //! See: https://doc.rust-lang.org/nomicon/coercions.html
 
-use hir_def::{lang_item::LangItemTarget, type_ref::Mutability};
+use chalk_ir::{Mutability, TyVariableKind};
+use hir_def::lang_item::LangItemTarget;
 use test_utils::mark;
 
-use crate::{autoderef, traits::Solution, Obligation, Substs, TraitRef, Ty, TypeCtor};
+use crate::{autoderef, traits::Solution, Obligation, Substs, TraitRef, Ty};
 
-use super::{unify::TypeVarValue, InEnvironment, InferTy, InferenceContext};
+use super::{InEnvironment, InferenceContext};
 
 impl<'a> InferenceContext<'a> {
     /// Unify two types, but may coerce the first one to the second one
@@ -33,7 +34,7 @@ impl<'a> InferenceContext<'a> {
         } else if self.coerce(ty2, ty1) {
             ty1.clone()
         } else {
-            if let (ty_app!(TypeCtor::FnDef(_)), ty_app!(TypeCtor::FnDef(_))) = (ty1, ty2) {
+            if let (Ty::FnDef(..), Ty::FnDef(..)) = (ty1, ty2) {
                 mark::hit!(coerce_fn_reification);
                 // Special case: two function types. Try to coerce both to
                 // pointers to have a chance at getting a match. See
@@ -53,12 +54,11 @@ impl<'a> InferenceContext<'a> {
     fn coerce_inner(&mut self, mut from_ty: Ty, to_ty: &Ty) -> bool {
         match (&from_ty, to_ty) {
             // Never type will make type variable to fallback to Never Type instead of Unknown.
-            (ty_app!(TypeCtor::Never), Ty::Infer(InferTy::TypeVar(tv))) => {
-                let var = self.table.new_maybe_never_type_var();
-                self.table.var_unification_table.union_value(*tv, TypeVarValue::Known(var));
+            (Ty::Never, Ty::InferenceVar(tv, TyVariableKind::General)) => {
+                self.table.type_variable_table.set_diverging(*tv, true);
                 return true;
             }
-            (ty_app!(TypeCtor::Never), _) => return true,
+            (Ty::Never, _) => return true,
 
             // Trivial cases, this should go after `never` check to
             // avoid infer result type to be never
@@ -71,38 +71,33 @@ impl<'a> InferenceContext<'a> {
 
         // Pointer weakening and function to pointer
         match (&mut from_ty, to_ty) {
-            // `*mut T`, `&mut T, `&T`` -> `*const T`
+            // `*mut T` -> `*const T`
             // `&mut T` -> `&T`
-            // `&mut T` -> `*mut T`
-            (ty_app!(c1@TypeCtor::RawPtr(_)), ty_app!(c2@TypeCtor::RawPtr(Mutability::Shared)))
-            | (ty_app!(c1@TypeCtor::Ref(_)), ty_app!(c2@TypeCtor::RawPtr(Mutability::Shared)))
-            | (ty_app!(c1@TypeCtor::Ref(_)), ty_app!(c2@TypeCtor::Ref(Mutability::Shared)))
-            | (ty_app!(c1@TypeCtor::Ref(Mutability::Mut)), ty_app!(c2@TypeCtor::RawPtr(_))) => {
-                *c1 = *c2;
+            (Ty::Raw(m1, ..), Ty::Raw(m2 @ Mutability::Not, ..))
+            | (Ty::Ref(m1, ..), Ty::Ref(m2 @ Mutability::Not, ..)) => {
+                *m1 = *m2;
+            }
+            // `&T` -> `*const T`
+            // `&mut T` -> `*mut T`/`*const T`
+            (Ty::Ref(.., substs), &Ty::Raw(m2 @ Mutability::Not, ..))
+            | (Ty::Ref(Mutability::Mut, substs), &Ty::Raw(m2, ..)) => {
+                from_ty = Ty::Raw(m2, substs.clone());
             }
 
-            // Illegal mutablity conversion
-            (
-                ty_app!(TypeCtor::RawPtr(Mutability::Shared)),
-                ty_app!(TypeCtor::RawPtr(Mutability::Mut)),
-            )
-            | (
-                ty_app!(TypeCtor::Ref(Mutability::Shared)),
-                ty_app!(TypeCtor::Ref(Mutability::Mut)),
-            ) => return false,
+            // Illegal mutability conversion
+            (Ty::Raw(Mutability::Not, ..), Ty::Raw(Mutability::Mut, ..))
+            | (Ty::Ref(Mutability::Not, ..), Ty::Ref(Mutability::Mut, ..)) => return false,
 
             // `{function_type}` -> `fn()`
-            (ty_app!(TypeCtor::FnDef(_)), ty_app!(TypeCtor::FnPtr { .. })) => {
-                match from_ty.callable_sig(self.db) {
-                    None => return false,
-                    Some(sig) => {
-                        from_ty = Ty::fn_ptr(sig);
-                    }
+            (Ty::FnDef(..), Ty::Function { .. }) => match from_ty.callable_sig(self.db) {
+                None => return false,
+                Some(sig) => {
+                    from_ty = Ty::fn_ptr(sig);
                 }
-            }
+            },
 
-            (ty_app!(TypeCtor::Closure { .. }, params), ty_app!(TypeCtor::FnPtr { .. })) => {
-                from_ty = params[0].clone();
+            (Ty::Closure(.., substs), Ty::Function { .. }) => {
+                from_ty = substs[0].clone();
             }
 
             _ => {}
@@ -115,9 +110,7 @@ impl<'a> InferenceContext<'a> {
         // Auto Deref if cannot coerce
         match (&from_ty, to_ty) {
             // FIXME: DerefMut
-            (ty_app!(TypeCtor::Ref(_), st1), ty_app!(TypeCtor::Ref(_), st2)) => {
-                self.unify_autoderef_behind_ref(&st1[0], &st2[0])
-            }
+            (Ty::Ref(_, st1), Ty::Ref(_, st2)) => self.unify_autoderef_behind_ref(&st1[0], &st2[0]),
 
             // Otherwise, normal unify
             _ => self.unify(&from_ty, to_ty),
@@ -178,17 +171,17 @@ impl<'a> InferenceContext<'a> {
             },
         ) {
             let derefed_ty = canonicalized.decanonicalize_ty(derefed_ty.value);
-            match (&*self.resolve_ty_shallow(&derefed_ty), &*to_ty) {
-                // Stop when constructor matches.
-                (ty_app!(from_ctor, st1), ty_app!(to_ctor, st2)) if from_ctor == to_ctor => {
-                    // It will not recurse to `coerce`.
-                    return self.table.unify_substs(st1, st2, 0);
-                }
-                _ => {
-                    if self.table.unify_inner_trivial(&derefed_ty, &to_ty, 0) {
-                        return true;
-                    }
-                }
+            let from_ty = self.resolve_ty_shallow(&derefed_ty);
+            // Stop when constructor matches.
+            if from_ty.equals_ctor(&to_ty) {
+                // It will not recurse to `coerce`.
+                return match (from_ty.substs(), to_ty.substs()) {
+                    (Some(st1), Some(st2)) => self.table.unify_substs(st1, st2, 0),
+                    (None, None) => true,
+                    _ => false,
+                };
+            } else if self.table.unify_inner_trivial(&derefed_ty, &to_ty, 0) {
+                return true;
             }
         }
 
diff --git a/crates/hir_ty/src/infer/expr.rs b/crates/hir_ty/src/infer/expr.rs
index 9bf3b51b0..cf1f1038a 100644
--- a/crates/hir_ty/src/infer/expr.rs
+++ b/crates/hir_ty/src/infer/expr.rs
@@ -3,8 +3,8 @@
 use std::iter::{repeat, repeat_with};
 use std::{mem, sync::Arc};
 
+use chalk_ir::{Mutability, TyVariableKind};
 use hir_def::{
-    builtin_type::Signedness,
     expr::{Array, BinaryOp, Expr, ExprId, Literal, Statement, UnaryOp},
     path::{GenericArg, GenericArgs},
     resolver::resolver_for_expr,
@@ -15,11 +15,14 @@ use syntax::ast::RangeOp;
 use test_utils::mark;
 
 use crate::{
-    autoderef, method_resolution, op,
+    autoderef,
+    lower::lower_to_chalk_mutability,
+    method_resolution, op,
+    primitive::{self, UintTy},
     traits::{FnTrait, InEnvironment},
     utils::{generics, variant_data, Generics},
-    ApplicationTy, Binders, CallableDefId, InferTy, IntTy, Mutability, Obligation, OpaqueTyId,
-    Rawness, Substs, TraitRef, Ty, TypeCtor,
+    Binders, CallableDefId, FnPointer, FnSig, Obligation, OpaqueTyId, Rawness, Scalar, Substs,
+    TraitRef, Ty,
 };
 
 use super::{
@@ -82,10 +85,7 @@ impl<'a> InferenceContext<'a> {
             arg_tys.push(arg);
         }
         let parameters = param_builder.build();
-        let arg_ty = Ty::Apply(ApplicationTy {
-            ctor: TypeCtor::Tuple { cardinality: num_args as u16 },
-            parameters,
-        });
+        let arg_ty = Ty::Tuple(num_args, parameters);
         let substs =
             Substs::build_for_generics(&generic_params).push(ty.clone()).push(arg_ty).build();
 
@@ -120,7 +120,7 @@ impl<'a> InferenceContext<'a> {
             Expr::Missing => Ty::Unknown,
             Expr::If { condition, then_branch, else_branch } => {
                 // if let is desugared to match, so this is always simple if
-                self.infer_expr(*condition, &Expectation::has_type(Ty::simple(TypeCtor::Bool)));
+                self.infer_expr(*condition, &Expectation::has_type(Ty::Scalar(Scalar::Bool)));
 
                 let condition_diverges = mem::replace(&mut self.diverges, Diverges::Maybe);
                 let mut both_arms_diverge = Diverges::Always;
@@ -137,24 +137,33 @@ impl<'a> InferenceContext<'a> {
 
                 self.coerce_merge_branch(&then_ty, &else_ty)
             }
-            Expr::Block { statements, tail, label } => match label {
-                Some(_) => {
-                    let break_ty = self.table.new_type_var();
-                    self.breakables.push(BreakableContext {
-                        may_break: false,
-                        break_ty: break_ty.clone(),
-                        label: label.map(|label| self.body[label].name.clone()),
-                    });
-                    let ty = self.infer_block(statements, *tail, &Expectation::has_type(break_ty));
-                    let ctxt = self.breakables.pop().expect("breakable stack broken");
-                    if ctxt.may_break {
-                        ctxt.break_ty
-                    } else {
-                        ty
+            Expr::Block { statements, tail, label, id: _ } => {
+                let old_resolver = mem::replace(
+                    &mut self.resolver,
+                    resolver_for_expr(self.db.upcast(), self.owner, tgt_expr),
+                );
+                let ty = match label {
+                    Some(_) => {
+                        let break_ty = self.table.new_type_var();
+                        self.breakables.push(BreakableContext {
+                            may_break: false,
+                            break_ty: break_ty.clone(),
+                            label: label.map(|label| self.body[label].name.clone()),
+                        });
+                        let ty =
+                            self.infer_block(statements, *tail, &Expectation::has_type(break_ty));
+                        let ctxt = self.breakables.pop().expect("breakable stack broken");
+                        if ctxt.may_break {
+                            ctxt.break_ty
+                        } else {
+                            ty
+                        }
                     }
-                }
-                None => self.infer_block(statements, *tail, expected),
-            },
+                    None => self.infer_block(statements, *tail, expected),
+                };
+                self.resolver = old_resolver;
+                ty
+            }
             Expr::Unsafe { body } | Expr::Const { body } => self.infer_expr(*body, expected),
             Expr::TryBlock { body } => {
                 let _inner = self.infer_expr(*body, expected);
@@ -166,7 +175,7 @@ impl<'a> InferenceContext<'a> {
                 // existenail type AsyncBlockImplTrait<InnerType>: Future<Output = InnerType>
                 let inner_ty = self.infer_expr(*body, &Expectation::none());
                 let opaque_ty_id = OpaqueTyId::AsyncBlockTypeImplTrait(self.owner, *body);
-                Ty::apply_one(TypeCtor::OpaqueType(opaque_ty_id), inner_ty)
+                Ty::OpaqueType(opaque_ty_id, Substs::single(inner_ty))
             }
             Expr::Loop { body, label } => {
                 self.breakables.push(BreakableContext {
@@ -184,7 +193,7 @@ impl<'a> InferenceContext<'a> {
                 if ctxt.may_break {
                     ctxt.break_ty
                 } else {
-                    Ty::simple(TypeCtor::Never)
+                    Ty::Never
                 }
             }
             Expr::While { condition, body, label } => {
@@ -194,7 +203,7 @@ impl<'a> InferenceContext<'a> {
                     label: label.map(|label| self.body[label].name.clone()),
                 });
                 // while let is desugared to a match loop, so this is always simple while
-                self.infer_expr(*condition, &Expectation::has_type(Ty::simple(TypeCtor::Bool)));
+                self.infer_expr(*condition, &Expectation::has_type(Ty::Scalar(Scalar::Bool)));
                 self.infer_expr(*body, &Expectation::has_type(Ty::unit()));
                 let _ctxt = self.breakables.pop().expect("breakable stack broken");
                 // the body may not run, so it diverging doesn't mean we diverge
@@ -241,12 +250,12 @@ impl<'a> InferenceContext<'a> {
                     None => self.table.new_type_var(),
                 };
                 sig_tys.push(ret_ty.clone());
-                let sig_ty = Ty::apply(
-                    TypeCtor::FnPtr { num_args: sig_tys.len() as u16 - 1, is_varargs: false },
-                    Substs(sig_tys.clone().into()),
-                );
-                let closure_ty =
-                    Ty::apply_one(TypeCtor::Closure { def: self.owner, expr: tgt_expr }, sig_ty);
+                let sig_ty = Ty::Function(FnPointer {
+                    num_args: sig_tys.len() - 1,
+                    sig: FnSig { variadic: false },
+                    substs: Substs(sig_tys.clone().into()),
+                });
+                let closure_ty = Ty::Closure(self.owner, tgt_expr, Substs::single(sig_ty));
 
                 // Eagerly try to relate the closure type with the expected
                 // type, otherwise we often won't have enough information to
@@ -297,11 +306,8 @@ impl<'a> InferenceContext<'a> {
             Expr::Match { expr, arms } => {
                 let input_ty = self.infer_expr(*expr, &Expectation::none());
 
-                let mut result_ty = if arms.is_empty() {
-                    Ty::simple(TypeCtor::Never)
-                } else {
-                    self.table.new_type_var()
-                };
+                let mut result_ty =
+                    if arms.is_empty() { Ty::Never } else { self.table.new_type_var() };
 
                 let matchee_diverges = self.diverges;
                 let mut all_arms_diverge = Diverges::Always;
@@ -312,7 +318,7 @@ impl<'a> InferenceContext<'a> {
                     if let Some(guard_expr) = arm.guard {
                         self.infer_expr(
                             guard_expr,
-                            &Expectation::has_type(Ty::simple(TypeCtor::Bool)),
+                            &Expectation::has_type(Ty::Scalar(Scalar::Bool)),
                         );
                     }
 
@@ -330,7 +336,7 @@ impl<'a> InferenceContext<'a> {
                 let resolver = resolver_for_expr(self.db.upcast(), self.owner, tgt_expr);
                 self.infer_path(&resolver, p, tgt_expr.into()).unwrap_or(Ty::Unknown)
             }
-            Expr::Continue { .. } => Ty::simple(TypeCtor::Never),
+            Expr::Continue { .. } => Ty::Never,
             Expr::Break { expr, label } => {
                 let val_ty = if let Some(expr) = expr {
                     self.infer_expr(*expr, &Expectation::none())
@@ -355,8 +361,7 @@ impl<'a> InferenceContext<'a> {
                         expr: tgt_expr,
                     });
                 }
-
-                Ty::simple(TypeCtor::Never)
+                Ty::Never
             }
             Expr::Return { expr } => {
                 if let Some(expr) = expr {
@@ -365,14 +370,14 @@ impl<'a> InferenceContext<'a> {
                     let unit = Ty::unit();
                     self.coerce(&unit, &self.return_ty.clone());
                 }
-                Ty::simple(TypeCtor::Never)
+                Ty::Never
             }
             Expr::Yield { expr } => {
                 // FIXME: track yield type for coercion
                 if let Some(expr) = expr {
                     self.infer_expr(*expr, &Expectation::none());
                 }
-                Ty::simple(TypeCtor::Never)
+                Ty::Never
             }
             Expr::RecordLit { path, fields, spread } => {
                 let (ty, def_id) = self.resolve_variant(path.as_ref());
@@ -382,7 +387,7 @@ impl<'a> InferenceContext<'a> {
 
                 self.unify(&ty, &expected.ty);
 
-                let substs = ty.substs().unwrap_or_else(Substs::empty);
+                let substs = ty.substs().cloned().unwrap_or_else(Substs::empty);
                 let field_types = def_id.map(|it| self.db.field_types(it)).unwrap_or_default();
                 let variant_data = def_id.map(|it| variant_data(self.db.upcast(), it));
                 for (field_idx, field) in fields.iter().enumerate() {
@@ -421,30 +426,23 @@ impl<'a> InferenceContext<'a> {
                     },
                 )
                 .find_map(|derefed_ty| match canonicalized.decanonicalize_ty(derefed_ty.value) {
-                    Ty::Apply(a_ty) => match a_ty.ctor {
-                        TypeCtor::Tuple { .. } => name
-                            .as_tuple_index()
-                            .and_then(|idx| a_ty.parameters.0.get(idx).cloned()),
-                        TypeCtor::Adt(AdtId::StructId(s)) => {
-                            self.db.struct_data(s).variant_data.field(name).map(|local_id| {
-                                let field = FieldId { parent: s.into(), local_id };
-                                self.write_field_resolution(tgt_expr, field);
-                                self.db.field_types(s.into())[field.local_id]
-                                    .clone()
-                                    .subst(&a_ty.parameters)
-                            })
-                        }
-                        TypeCtor::Adt(AdtId::UnionId(u)) => {
-                            self.db.union_data(u).variant_data.field(name).map(|local_id| {
-                                let field = FieldId { parent: u.into(), local_id };
-                                self.write_field_resolution(tgt_expr, field);
-                                self.db.field_types(u.into())[field.local_id]
-                                    .clone()
-                                    .subst(&a_ty.parameters)
-                            })
-                        }
-                        _ => None,
-                    },
+                    Ty::Tuple(_, substs) => {
+                        name.as_tuple_index().and_then(|idx| substs.0.get(idx).cloned())
+                    }
+                    Ty::Adt(AdtId::StructId(s), parameters) => {
+                        self.db.struct_data(s).variant_data.field(name).map(|local_id| {
+                            let field = FieldId { parent: s.into(), local_id };
+                            self.write_field_resolution(tgt_expr, field);
+                            self.db.field_types(s.into())[field.local_id].clone().subst(&parameters)
+                        })
+                    }
+                    Ty::Adt(AdtId::UnionId(u), parameters) => {
+                        self.db.union_data(u).variant_data.field(name).map(|local_id| {
+                            let field = FieldId { parent: u.into(), local_id };
+                            self.write_field_resolution(tgt_expr, field);
+                            self.db.field_types(u.into())[field.local_id].clone().subst(&parameters)
+                        })
+                    }
                     _ => None,
                 })
                 .unwrap_or(Ty::Unknown);
@@ -466,10 +464,11 @@ impl<'a> InferenceContext<'a> {
                 cast_ty
             }
             Expr::Ref { expr, rawness, mutability } => {
+                let mutability = lower_to_chalk_mutability(*mutability);
                 let expectation = if let Some((exp_inner, exp_rawness, exp_mutability)) =
                     &expected.ty.as_reference_or_ptr()
                 {
-                    if *exp_mutability == Mutability::Mut && *mutability == Mutability::Shared {
+                    if *exp_mutability == Mutability::Mut && mutability == Mutability::Not {
                         // FIXME: throw type error - expected mut reference but found shared ref,
                         // which cannot be coerced
                     }
@@ -482,16 +481,24 @@ impl<'a> InferenceContext<'a> {
                     Expectation::none()
                 };
                 let inner_ty = self.infer_expr_inner(*expr, &expectation);
-                let ty = match rawness {
-                    Rawness::RawPtr => TypeCtor::RawPtr(*mutability),
-                    Rawness::Ref => TypeCtor::Ref(*mutability),
-                };
-                Ty::apply_one(ty, inner_ty)
+                match rawness {
+                    Rawness::RawPtr => Ty::Raw(mutability, Substs::single(inner_ty)),
+                    Rawness::Ref => Ty::Ref(mutability, Substs::single(inner_ty)),
+                }
             }
             Expr::Box { expr } => {
                 let inner_ty = self.infer_expr_inner(*expr, &Expectation::none());
                 if let Some(box_) = self.resolve_boxed_box() {
-                    Ty::apply_one(TypeCtor::Adt(box_), inner_ty)
+                    let mut sb = Substs::builder(generics(self.db.upcast(), box_.into()).len());
+                    sb = sb.push(inner_ty);
+                    match self.db.generic_defaults(box_.into()).as_ref() {
+                        [_, alloc_ty, ..] if !alloc_ty.value.is_unknown() => {
+                            sb = sb.push(alloc_ty.value.clone());
+                        }
+                        _ => (),
+                    }
+                    sb = sb.fill(repeat_with(|| self.table.new_type_var()));
+                    Ty::Adt(box_, sb.build())
                 } else {
                     Ty::Unknown
                 }
@@ -521,13 +528,11 @@ impl<'a> InferenceContext<'a> {
                     UnaryOp::Neg => {
                         match &inner_ty {
                             // Fast path for builtins
-                            Ty::Apply(ApplicationTy {
-                                ctor: TypeCtor::Int(IntTy { signedness: Signedness::Signed, .. }),
-                                ..
-                            })
-                            | Ty::Apply(ApplicationTy { ctor: TypeCtor::Float(_), .. })
-                            | Ty::Infer(InferTy::IntVar(..))
-                            | Ty::Infer(InferTy::FloatVar(..)) => inner_ty,
+                            Ty::Scalar(Scalar::Int(_))
+                            | Ty::Scalar(Scalar::Uint(_))
+                            | Ty::Scalar(Scalar::Float(_))
+                            | Ty::InferenceVar(_, TyVariableKind::Integer)
+                            | Ty::InferenceVar(_, TyVariableKind::Float) => inner_ty,
                             // Otherwise we resolve via the std::ops::Neg trait
                             _ => self
                                 .resolve_associated_type(inner_ty, self.resolve_ops_neg_output()),
@@ -536,9 +541,10 @@ impl<'a> InferenceContext<'a> {
                     UnaryOp::Not => {
                         match &inner_ty {
                             // Fast path for builtins
-                            Ty::Apply(ApplicationTy { ctor: TypeCtor::Bool, .. })
-                            | Ty::Apply(ApplicationTy { ctor: TypeCtor::Int(_), .. })
-                            | Ty::Infer(InferTy::IntVar(..)) => inner_ty,
+                            Ty::Scalar(Scalar::Bool)
+                            | Ty::Scalar(Scalar::Int(_))
+                            | Ty::Scalar(Scalar::Uint(_))
+                            | Ty::InferenceVar(_, TyVariableKind::Integer) => inner_ty,
                             // Otherwise we resolve via the std::ops::Not trait
                             _ => self
                                 .resolve_associated_type(inner_ty, self.resolve_ops_not_output()),
@@ -549,7 +555,7 @@ impl<'a> InferenceContext<'a> {
             Expr::BinaryOp { lhs, rhs, op } => match op {
                 Some(op) => {
                     let lhs_expectation = match op {
-                        BinaryOp::LogicOp(..) => Expectation::has_type(Ty::simple(TypeCtor::Bool)),
+                        BinaryOp::LogicOp(..) => Expectation::has_type(Ty::Scalar(Scalar::Bool)),
                         _ => Expectation::none(),
                     };
                     let lhs_ty = self.infer_expr(*lhs, &lhs_expectation);
@@ -580,31 +586,31 @@ impl<'a> InferenceContext<'a> {
                 let rhs_ty = rhs.map(|e| self.infer_expr(e, &rhs_expect));
                 match (range_type, lhs_ty, rhs_ty) {
                     (RangeOp::Exclusive, None, None) => match self.resolve_range_full() {
-                        Some(adt) => Ty::simple(TypeCtor::Adt(adt)),
+                        Some(adt) => Ty::Adt(adt, Substs::empty()),
                         None => Ty::Unknown,
                     },
                     (RangeOp::Exclusive, None, Some(ty)) => match self.resolve_range_to() {
-                        Some(adt) => Ty::apply_one(TypeCtor::Adt(adt), ty),
+                        Some(adt) => Ty::Adt(adt, Substs::single(ty)),
                         None => Ty::Unknown,
                     },
                     (RangeOp::Inclusive, None, Some(ty)) => {
                         match self.resolve_range_to_inclusive() {
-                            Some(adt) => Ty::apply_one(TypeCtor::Adt(adt), ty),
+                            Some(adt) => Ty::Adt(adt, Substs::single(ty)),
                             None => Ty::Unknown,
                         }
                     }
                     (RangeOp::Exclusive, Some(_), Some(ty)) => match self.resolve_range() {
-                        Some(adt) => Ty::apply_one(TypeCtor::Adt(adt), ty),
+                        Some(adt) => Ty::Adt(adt, Substs::single(ty)),
                         None => Ty::Unknown,
                     },
                     (RangeOp::Inclusive, Some(_), Some(ty)) => {
                         match self.resolve_range_inclusive() {
-                            Some(adt) => Ty::apply_one(TypeCtor::Adt(adt), ty),
+                            Some(adt) => Ty::Adt(adt, Substs::single(ty)),
                             None => Ty::Unknown,
                         }
                     }
                     (RangeOp::Exclusive, Some(ty), None) => match self.resolve_range_from() {
-                        Some(adt) => Ty::apply_one(TypeCtor::Adt(adt), ty),
+                        Some(adt) => Ty::Adt(adt, Substs::single(ty)),
                         None => Ty::Unknown,
                     },
                     (RangeOp::Inclusive, _, None) => Ty::Unknown,
@@ -638,7 +644,7 @@ impl<'a> InferenceContext<'a> {
             }
             Expr::Tuple { exprs } => {
                 let mut tys = match &expected.ty {
-                    ty_app!(TypeCtor::Tuple { .. }, st) => st
+                    Ty::Tuple(_, substs) => substs
                         .iter()
                         .cloned()
                         .chain(repeat_with(|| self.table.new_type_var()))
@@ -651,15 +657,11 @@ impl<'a> InferenceContext<'a> {
                     self.infer_expr_coerce(*expr, &Expectation::has_type(ty.clone()));
                 }
 
-                Ty::apply(TypeCtor::Tuple { cardinality: tys.len() as u16 }, Substs(tys.into()))
+                Ty::Tuple(tys.len(), Substs(tys.into()))
             }
             Expr::Array(array) => {
                 let elem_ty = match &expected.ty {
-                    // FIXME: remove when https://github.com/rust-lang/rust/issues/80501 is fixed
-                    #[allow(unreachable_patterns)]
-                    ty_app!(TypeCtor::Array, st) | ty_app!(TypeCtor::Slice, st) => {
-                        st.as_single().clone()
-                    }
+                    Ty::Array(st) | Ty::Slice(st) => st.as_single().clone(),
                     _ => self.table.new_type_var(),
                 };
 
@@ -676,30 +678,38 @@ impl<'a> InferenceContext<'a> {
                         );
                         self.infer_expr(
                             *repeat,
-                            &Expectation::has_type(Ty::simple(TypeCtor::Int(IntTy::usize()))),
+                            &Expectation::has_type(Ty::Scalar(Scalar::Uint(UintTy::Usize))),
                         );
                     }
                 }
 
-                Ty::apply_one(TypeCtor::Array, elem_ty)
+                Ty::Array(Substs::single(elem_ty))
             }
             Expr::Literal(lit) => match lit {
-                Literal::Bool(..) => Ty::simple(TypeCtor::Bool),
-                Literal::String(..) => {
-                    Ty::apply_one(TypeCtor::Ref(Mutability::Shared), Ty::simple(TypeCtor::Str))
-                }
+                Literal::Bool(..) => Ty::Scalar(Scalar::Bool),
+                Literal::String(..) => Ty::Ref(Mutability::Not, Substs::single(Ty::Str)),
                 Literal::ByteString(..) => {
-                    let byte_type = Ty::simple(TypeCtor::Int(IntTy::u8()));
-                    let array_type = Ty::apply_one(TypeCtor::Array, byte_type);
-                    Ty::apply_one(TypeCtor::Ref(Mutability::Shared), array_type)
+                    let byte_type = Ty::Scalar(Scalar::Uint(UintTy::U8));
+                    let array_type = Ty::Array(Substs::single(byte_type));
+                    Ty::Ref(Mutability::Not, Substs::single(array_type))
                 }
-                Literal::Char(..) => Ty::simple(TypeCtor::Char),
+                Literal::Char(..) => Ty::Scalar(Scalar::Char),
                 Literal::Int(_v, ty) => match ty {
-                    Some(int_ty) => Ty::simple(TypeCtor::Int((*int_ty).into())),
+                    Some(int_ty) => {
+                        Ty::Scalar(Scalar::Int(primitive::int_ty_from_builtin(*int_ty)))
+                    }
+                    None => self.table.new_integer_var(),
+                },
+                Literal::Uint(_v, ty) => match ty {
+                    Some(int_ty) => {
+                        Ty::Scalar(Scalar::Uint(primitive::uint_ty_from_builtin(*int_ty)))
+                    }
                     None => self.table.new_integer_var(),
                 },
                 Literal::Float(_v, ty) => match ty {
-                    Some(float_ty) => Ty::simple(TypeCtor::Float((*float_ty).into())),
+                    Some(float_ty) => {
+                        Ty::Scalar(Scalar::Float(primitive::float_ty_from_builtin(*float_ty)))
+                    }
                     None => self.table.new_float_var(),
                 },
             },
@@ -755,7 +765,7 @@ impl<'a> InferenceContext<'a> {
             // `!`).
             if self.diverges.is_always() {
                 // we don't even make an attempt at coercion
-                self.table.new_maybe_never_type_var()
+                self.table.new_maybe_never_var()
             } else {
                 self.coerce(&Ty::unit(), expected.coercion_target());
                 Ty::unit()
@@ -812,7 +822,7 @@ impl<'a> InferenceContext<'a> {
         // Apply autoref so the below unification works correctly
         // FIXME: return correct autorefs from lookup_method
         let actual_receiver_ty = match expected_receiver_ty.as_reference() {
-            Some((_, mutability)) => Ty::apply_one(TypeCtor::Ref(mutability), derefed_receiver_ty),
+            Some((_, mutability)) => Ty::Ref(mutability, Substs::single(derefed_receiver_ty)),
             _ => derefed_receiver_ty,
         };
         self.unify(&expected_receiver_ty, &actual_receiver_ty);
@@ -889,30 +899,26 @@ impl<'a> InferenceContext<'a> {
     }
 
     fn register_obligations_for_call(&mut self, callable_ty: &Ty) {
-        if let Ty::Apply(a_ty) = callable_ty {
-            if let TypeCtor::FnDef(def) = a_ty.ctor {
-                let generic_predicates = self.db.generic_predicates(def.into());
-                for predicate in generic_predicates.iter() {
-                    let predicate = predicate.clone().subst(&a_ty.parameters);
-                    if let Some(obligation) = Obligation::from_predicate(predicate) {
-                        self.obligations.push(obligation);
-                    }
+        if let &Ty::FnDef(def, ref parameters) = callable_ty {
+            let generic_predicates = self.db.generic_predicates(def.into());
+            for predicate in generic_predicates.iter() {
+                let predicate = predicate.clone().subst(parameters);
+                if let Some(obligation) = Obligation::from_predicate(predicate) {
+                    self.obligations.push(obligation);
                 }
-                // add obligation for trait implementation, if this is a trait method
-                match def {
-                    CallableDefId::FunctionId(f) => {
-                        if let AssocContainerId::TraitId(trait_) =
-                            f.lookup(self.db.upcast()).container
-                        {
-                            // construct a TraitDef
-                            let substs = a_ty
-                                .parameters
-                                .prefix(generics(self.db.upcast(), trait_.into()).len());
-                            self.obligations.push(Obligation::Trait(TraitRef { trait_, substs }));
-                        }
+            }
+            // add obligation for trait implementation, if this is a trait method
+            match def {
+                CallableDefId::FunctionId(f) => {
+                    if let AssocContainerId::TraitId(trait_) = f.lookup(self.db.upcast()).container
+                    {
+                        // construct a TraitDef
+                        let substs =
+                            parameters.prefix(generics(self.db.upcast(), trait_.into()).len());
+                        self.obligations.push(Obligation::Trait(TraitRef { trait_, substs }));
                     }
-                    CallableDefId::StructId(_) | CallableDefId::EnumVariantId(_) => {}
                 }
+                CallableDefId::StructId(_) | CallableDefId::EnumVariantId(_) => {}
             }
         }
     }
diff --git a/crates/hir_ty/src/infer/pat.rs b/crates/hir_ty/src/infer/pat.rs
index d974f805b..eb099311c 100644
--- a/crates/hir_ty/src/infer/pat.rs
+++ b/crates/hir_ty/src/infer/pat.rs
@@ -3,17 +3,17 @@
 use std::iter::repeat;
 use std::sync::Arc;
 
+use chalk_ir::Mutability;
 use hir_def::{
     expr::{BindingAnnotation, Expr, Literal, Pat, PatId, RecordFieldPat},
     path::Path,
-    type_ref::Mutability,
     FieldId,
 };
 use hir_expand::name::Name;
 use test_utils::mark;
 
 use super::{BindingMode, Expectation, InferenceContext};
-use crate::{utils::variant_data, Substs, Ty, TypeCtor};
+use crate::{lower::lower_to_chalk_mutability, utils::variant_data, Substs, Ty};
 
 impl<'a> InferenceContext<'a> {
     fn infer_tuple_struct_pat(
@@ -32,7 +32,7 @@ impl<'a> InferenceContext<'a> {
         }
         self.unify(&ty, expected);
 
-        let substs = ty.substs().unwrap_or_else(Substs::empty);
+        let substs = ty.substs().cloned().unwrap_or_else(Substs::empty);
 
         let field_tys = def.map(|it| self.db.field_types(it)).unwrap_or_default();
         let (pre, post) = match ellipsis {
@@ -71,7 +71,7 @@ impl<'a> InferenceContext<'a> {
 
         self.unify(&ty, expected);
 
-        let substs = ty.substs().unwrap_or_else(Substs::empty);
+        let substs = ty.substs().cloned().unwrap_or_else(Substs::empty);
 
         let field_tys = def.map(|it| self.db.field_types(it)).unwrap_or_default();
         for subpat in subpats {
@@ -103,7 +103,7 @@ impl<'a> InferenceContext<'a> {
                 expected = inner;
                 default_bm = match default_bm {
                     BindingMode::Move => BindingMode::Ref(mutability),
-                    BindingMode::Ref(Mutability::Shared) => BindingMode::Ref(Mutability::Shared),
+                    BindingMode::Ref(Mutability::Not) => BindingMode::Ref(Mutability::Not),
                     BindingMode::Ref(Mutability::Mut) => BindingMode::Ref(mutability),
                 }
             }
@@ -138,10 +138,7 @@ impl<'a> InferenceContext<'a> {
                 inner_tys.extend(expectations_iter.by_ref().take(n_uncovered_patterns).cloned());
                 inner_tys.extend(post.iter().zip(expectations_iter).map(infer_pat));
 
-                Ty::apply(
-                    TypeCtor::Tuple { cardinality: inner_tys.len() as u16 },
-                    Substs(inner_tys.into()),
-                )
+                Ty::Tuple(inner_tys.len(), Substs(inner_tys.into()))
             }
             Pat::Or(ref pats) => {
                 if let Some((first_pat, rest)) = pats.split_first() {
@@ -155,9 +152,10 @@ impl<'a> InferenceContext<'a> {
                 }
             }
             Pat::Ref { pat, mutability } => {
+                let mutability = lower_to_chalk_mutability(*mutability);
                 let expectation = match expected.as_reference() {
                     Some((inner_ty, exp_mut)) => {
-                        if *mutability != exp_mut {
+                        if mutability != exp_mut {
                             // FIXME: emit type error?
                         }
                         inner_ty
@@ -165,7 +163,7 @@ impl<'a> InferenceContext<'a> {
                     _ => &Ty::Unknown,
                 };
                 let subty = self.infer_pat(*pat, expectation, default_bm);
-                Ty::apply_one(TypeCtor::Ref(*mutability), subty)
+                Ty::Ref(mutability, Substs::single(subty))
             }
             Pat::TupleStruct { path: p, args: subpats, ellipsis } => self.infer_tuple_struct_pat(
                 p.as_ref(),
@@ -198,7 +196,7 @@ impl<'a> InferenceContext<'a> {
 
                 let bound_ty = match mode {
                     BindingMode::Ref(mutability) => {
-                        Ty::apply_one(TypeCtor::Ref(mutability), inner_ty.clone())
+                        Ty::Ref(mutability, Substs::single(inner_ty.clone()))
                     }
                     BindingMode::Move => inner_ty.clone(),
                 };
@@ -207,17 +205,17 @@ impl<'a> InferenceContext<'a> {
                 return inner_ty;
             }
             Pat::Slice { prefix, slice, suffix } => {
-                let (container_ty, elem_ty) = match &expected {
-                    ty_app!(TypeCtor::Array, st) => (TypeCtor::Array, st.as_single().clone()),
-                    ty_app!(TypeCtor::Slice, st) => (TypeCtor::Slice, st.as_single().clone()),
-                    _ => (TypeCtor::Slice, Ty::Unknown),
+                let (container_ty, elem_ty): (fn(_) -> _, _) = match &expected {
+                    Ty::Array(st) => (Ty::Array, st.as_single().clone()),
+                    Ty::Slice(st) => (Ty::Slice, st.as_single().clone()),
+                    _ => (Ty::Slice, Ty::Unknown),
                 };
 
                 for pat_id in prefix.iter().chain(suffix) {
                     self.infer_pat(*pat_id, &elem_ty, default_bm);
                 }
 
-                let pat_ty = Ty::apply_one(container_ty, elem_ty);
+                let pat_ty = container_ty(Substs::single(elem_ty));
                 if let Some(slice_pat_id) = slice {
                     self.infer_pat(*slice_pat_id, &pat_ty, default_bm);
                 }
@@ -239,7 +237,7 @@ impl<'a> InferenceContext<'a> {
                     };
 
                     let inner_ty = self.infer_pat(*inner, inner_expected, default_bm);
-                    Ty::apply_one(TypeCtor::Adt(box_adt), inner_ty)
+                    Ty::Adt(box_adt, Substs::single(inner_ty))
                 }
                 None => Ty::Unknown,
             },
diff --git a/crates/hir_ty/src/infer/unify.rs b/crates/hir_ty/src/infer/unify.rs
index 76984242e..99a89a7f3 100644
--- a/crates/hir_ty/src/infer/unify.rs
+++ b/crates/hir_ty/src/infer/unify.rs
@@ -2,14 +2,15 @@
 
 use std::borrow::Cow;
 
+use chalk_ir::{FloatTy, IntTy, TyVariableKind};
 use ena::unify::{InPlaceUnificationTable, NoError, UnifyKey, UnifyValue};
 
 use test_utils::mark;
 
 use super::{InferenceContext, Obligation};
 use crate::{
-    BoundVar, Canonical, DebruijnIndex, GenericPredicate, InEnvironment, InferTy, Substs, Ty,
-    TyKind, TypeCtor, TypeWalk,
+    BoundVar, Canonical, DebruijnIndex, GenericPredicate, InEnvironment, InferenceVar, Scalar,
+    Substs, Ty, TypeWalk,
 };
 
 impl<'a> InferenceContext<'a> {
@@ -26,7 +27,7 @@ where
     'a: 'b,
 {
     ctx: &'b mut InferenceContext<'a>,
-    free_vars: Vec<InferTy>,
+    free_vars: Vec<(InferenceVar, TyVariableKind)>,
     /// A stack of type variables that is used to detect recursive types (which
     /// are an error, but we need to protect against them to avoid stack
     /// overflows).
@@ -36,17 +37,14 @@ where
 #[derive(Debug)]
 pub(super) struct Canonicalized<T> {
     pub(super) value: Canonical<T>,
-    free_vars: Vec<InferTy>,
+    free_vars: Vec<(InferenceVar, TyVariableKind)>,
 }
 
-impl<'a, 'b> Canonicalizer<'a, 'b>
-where
-    'a: 'b,
-{
-    fn add(&mut self, free_var: InferTy) -> usize {
-        self.free_vars.iter().position(|&v| v == free_var).unwrap_or_else(|| {
+impl<'a, 'b> Canonicalizer<'a, 'b> {
+    fn add(&mut self, free_var: InferenceVar, kind: TyVariableKind) -> usize {
+        self.free_vars.iter().position(|&(v, _)| v == free_var).unwrap_or_else(|| {
             let next_index = self.free_vars.len();
-            self.free_vars.push(free_var);
+            self.free_vars.push((free_var, kind));
             next_index
         })
     }
@@ -54,11 +52,11 @@ where
     fn do_canonicalize<T: TypeWalk>(&mut self, t: T, binders: DebruijnIndex) -> T {
         t.fold_binders(
             &mut |ty, binders| match ty {
-                Ty::Infer(tv) => {
-                    let inner = tv.to_inner();
+                Ty::InferenceVar(var, kind) => {
+                    let inner = var.to_inner();
                     if self.var_stack.contains(&inner) {
                         // recursive type
-                        return tv.fallback_value();
+                        return self.ctx.table.type_variable_table.fallback_value(var, kind);
                     }
                     if let Some(known_ty) =
                         self.ctx.table.var_unification_table.inlined_probe_value(inner).known()
@@ -69,14 +67,8 @@ where
                         result
                     } else {
                         let root = self.ctx.table.var_unification_table.find(inner);
-                        let free_var = match tv {
-                            InferTy::TypeVar(_) => InferTy::TypeVar(root),
-                            InferTy::IntVar(_) => InferTy::IntVar(root),
-                            InferTy::FloatVar(_) => InferTy::FloatVar(root),
-                            InferTy::MaybeNeverTypeVar(_) => InferTy::MaybeNeverTypeVar(root),
-                        };
-                        let position = self.add(free_var);
-                        Ty::Bound(BoundVar::new(binders, position))
+                        let position = self.add(InferenceVar::from_inner(root), kind);
+                        Ty::BoundVar(BoundVar::new(binders, position))
                     }
                 }
                 _ => ty,
@@ -86,19 +78,7 @@ where
     }
 
     fn into_canonicalized<T>(self, result: T) -> Canonicalized<T> {
-        let kinds = self
-            .free_vars
-            .iter()
-            .map(|v| match v {
-                // mapping MaybeNeverTypeVar to the same kind as general ones
-                // should be fine, because as opposed to int or float type vars,
-                // they don't restrict what kind of type can go into them, they
-                // just affect fallback.
-                InferTy::TypeVar(_) | InferTy::MaybeNeverTypeVar(_) => TyKind::General,
-                InferTy::IntVar(_) => TyKind::Integer,
-                InferTy::FloatVar(_) => TyKind::Float,
-            })
-            .collect();
+        let kinds = self.free_vars.iter().map(|&(_, k)| k).collect();
         Canonicalized { value: Canonical { value: result, kinds }, free_vars: self.free_vars }
     }
 
@@ -130,9 +110,10 @@ impl<T> Canonicalized<T> {
     pub(super) fn decanonicalize_ty(&self, mut ty: Ty) -> Ty {
         ty.walk_mut_binders(
             &mut |ty, binders| {
-                if let &mut Ty::Bound(bound) = ty {
+                if let &mut Ty::BoundVar(bound) = ty {
                     if bound.debruijn >= binders {
-                        *ty = Ty::Infer(self.free_vars[bound.index]);
+                        let (v, k) = self.free_vars[bound.index];
+                        *ty = Ty::InferenceVar(v, k);
                     }
                 }
             },
@@ -152,18 +133,18 @@ impl<T> Canonicalized<T> {
                 .kinds
                 .iter()
                 .map(|k| match k {
-                    TyKind::General => ctx.table.new_type_var(),
-                    TyKind::Integer => ctx.table.new_integer_var(),
-                    TyKind::Float => ctx.table.new_float_var(),
+                    TyVariableKind::General => ctx.table.new_type_var(),
+                    TyVariableKind::Integer => ctx.table.new_integer_var(),
+                    TyVariableKind::Float => ctx.table.new_float_var(),
                 })
                 .collect(),
         );
         for (i, ty) in solution.value.into_iter().enumerate() {
-            let var = self.free_vars[i];
+            let (v, k) = self.free_vars[i];
             // eagerly replace projections in the type; we may be getting types
             // e.g. from where clauses where this hasn't happened yet
             let ty = ctx.normalize_associated_types_in(ty.clone().subst_bound_vars(&new_vars));
-            ctx.table.unify(&Ty::Infer(var), &ty);
+            ctx.table.unify(&Ty::InferenceVar(v, k), &ty);
         }
     }
 }
@@ -187,7 +168,7 @@ pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substs> {
     // (kind of hacky)
     for (i, var) in vars.iter().enumerate() {
         if &*table.resolve_ty_shallow(var) == var {
-            table.unify(var, &Ty::Bound(BoundVar::new(DebruijnIndex::INNERMOST, i)));
+            table.unify(var, &Ty::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, i)));
         }
     }
     Some(
@@ -198,31 +179,73 @@ pub(crate) fn unify(tys: &Canonical<(Ty, Ty)>) -> Option<Substs> {
 }
 
 #[derive(Clone, Debug)]
+pub(super) struct TypeVariableTable {
+    inner: Vec<TypeVariableData>,
+}
+
+impl TypeVariableTable {
+    fn push(&mut self, data: TypeVariableData) {
+        self.inner.push(data);
+    }
+
+    pub(super) fn set_diverging(&mut self, iv: InferenceVar, diverging: bool) {
+        self.inner[iv.to_inner().0 as usize].diverging = diverging;
+    }
+
+    fn is_diverging(&mut self, iv: InferenceVar) -> bool {
+        self.inner[iv.to_inner().0 as usize].diverging
+    }
+
+    fn fallback_value(&self, iv: InferenceVar, kind: TyVariableKind) -> Ty {
+        match kind {
+            _ if self.inner[iv.to_inner().0 as usize].diverging => Ty::Never,
+            TyVariableKind::General => Ty::Unknown,
+            TyVariableKind::Integer => Ty::Scalar(Scalar::Int(IntTy::I32)),
+            TyVariableKind::Float => Ty::Scalar(Scalar::Float(FloatTy::F64)),
+        }
+    }
+}
+
+#[derive(Copy, Clone, Debug)]
+pub(crate) struct TypeVariableData {
+    diverging: bool,
+}
+
+#[derive(Clone, Debug)]
 pub(crate) struct InferenceTable {
     pub(super) var_unification_table: InPlaceUnificationTable<TypeVarId>,
+    pub(super) type_variable_table: TypeVariableTable,
 }
 
 impl InferenceTable {
     pub(crate) fn new() -> Self {
-        InferenceTable { var_unification_table: InPlaceUnificationTable::new() }
+        InferenceTable {
+            var_unification_table: InPlaceUnificationTable::new(),
+            type_variable_table: TypeVariableTable { inner: Vec::new() },
+        }
+    }
+
+    fn new_var(&mut self, kind: TyVariableKind, diverging: bool) -> Ty {
+        self.type_variable_table.push(TypeVariableData { diverging });
+        let key = self.var_unification_table.new_key(TypeVarValue::Unknown);
+        assert_eq!(key.0 as usize, self.type_variable_table.inner.len() - 1);
+        Ty::InferenceVar(InferenceVar::from_inner(key), kind)
     }
 
     pub(crate) fn new_type_var(&mut self) -> Ty {
-        Ty::Infer(InferTy::TypeVar(self.var_unification_table.new_key(TypeVarValue::Unknown)))
+        self.new_var(TyVariableKind::General, false)
     }
 
     pub(crate) fn new_integer_var(&mut self) -> Ty {
-        Ty::Infer(InferTy::IntVar(self.var_unification_table.new_key(TypeVarValue::Unknown)))
+        self.new_var(TyVariableKind::Integer, false)
     }
 
     pub(crate) fn new_float_var(&mut self) -> Ty {
-        Ty::Infer(InferTy::FloatVar(self.var_unification_table.new_key(TypeVarValue::Unknown)))
+        self.new_var(TyVariableKind::Float, false)
     }
 
-    pub(crate) fn new_maybe_never_type_var(&mut self) -> Ty {
-        Ty::Infer(InferTy::MaybeNeverTypeVar(
-            self.var_unification_table.new_key(TypeVarValue::Unknown),
-        ))
+    pub(crate) fn new_maybe_never_var(&mut self) -> Ty {
+        self.new_var(TyVariableKind::General, true)
     }
 
     pub(crate) fn resolve_ty_completely(&mut self, ty: Ty) -> Ty {
@@ -257,12 +280,14 @@ impl InferenceTable {
         // try to resolve type vars first
         let ty1 = self.resolve_ty_shallow(ty1);
         let ty2 = self.resolve_ty_shallow(ty2);
-        match (&*ty1, &*ty2) {
-            (Ty::Apply(a_ty1), Ty::Apply(a_ty2)) if a_ty1.ctor == a_ty2.ctor => {
-                self.unify_substs(&a_ty1.parameters, &a_ty2.parameters, depth + 1)
+        if ty1.equals_ctor(&ty2) {
+            match (ty1.substs(), ty2.substs()) {
+                (Some(st1), Some(st2)) => self.unify_substs(st1, st2, depth + 1),
+                (None, None) => true,
+                _ => false,
             }
-
-            _ => self.unify_inner_trivial(&ty1, &ty2, depth),
+        } else {
+            self.unify_inner_trivial(&ty1, &ty2, depth)
         }
     }
 
@@ -281,31 +306,46 @@ impl InferenceTable {
                 true
             }
 
-            (Ty::Infer(InferTy::TypeVar(tv1)), Ty::Infer(InferTy::TypeVar(tv2)))
-            | (Ty::Infer(InferTy::IntVar(tv1)), Ty::Infer(InferTy::IntVar(tv2)))
-            | (Ty::Infer(InferTy::FloatVar(tv1)), Ty::Infer(InferTy::FloatVar(tv2)))
+            (
+                Ty::InferenceVar(tv1, TyVariableKind::General),
+                Ty::InferenceVar(tv2, TyVariableKind::General),
+            )
             | (
-                Ty::Infer(InferTy::MaybeNeverTypeVar(tv1)),
-                Ty::Infer(InferTy::MaybeNeverTypeVar(tv2)),
-            ) => {
+                Ty::InferenceVar(tv1, TyVariableKind::Integer),
+                Ty::InferenceVar(tv2, TyVariableKind::Integer),
+            )
+            | (
+                Ty::InferenceVar(tv1, TyVariableKind::Float),
+                Ty::InferenceVar(tv2, TyVariableKind::Float),
+            ) if self.type_variable_table.is_diverging(*tv1)
+                == self.type_variable_table.is_diverging(*tv2) =>
+            {
                 // both type vars are unknown since we tried to resolve them
-                self.var_unification_table.union(*tv1, *tv2);
+                self.var_unification_table.union(tv1.to_inner(), tv2.to_inner());
                 true
             }
 
             // The order of MaybeNeverTypeVar matters here.
             // Unifying MaybeNeverTypeVar and TypeVar will let the latter become MaybeNeverTypeVar.
             // Unifying MaybeNeverTypeVar and other concrete type will let the former become it.
-            (Ty::Infer(InferTy::TypeVar(tv)), other)
-            | (other, Ty::Infer(InferTy::TypeVar(tv)))
-            | (Ty::Infer(InferTy::MaybeNeverTypeVar(tv)), other)
-            | (other, Ty::Infer(InferTy::MaybeNeverTypeVar(tv)))
-            | (Ty::Infer(InferTy::IntVar(tv)), other @ ty_app!(TypeCtor::Int(_)))
-            | (other @ ty_app!(TypeCtor::Int(_)), Ty::Infer(InferTy::IntVar(tv)))
-            | (Ty::Infer(InferTy::FloatVar(tv)), other @ ty_app!(TypeCtor::Float(_)))
-            | (other @ ty_app!(TypeCtor::Float(_)), Ty::Infer(InferTy::FloatVar(tv))) => {
+            (Ty::InferenceVar(tv, TyVariableKind::General), other)
+            | (other, Ty::InferenceVar(tv, TyVariableKind::General))
+            | (Ty::InferenceVar(tv, TyVariableKind::Integer), other @ Ty::Scalar(Scalar::Int(_)))
+            | (other @ Ty::Scalar(Scalar::Int(_)), Ty::InferenceVar(tv, TyVariableKind::Integer))
+            | (
+                Ty::InferenceVar(tv, TyVariableKind::Integer),
+                other @ Ty::Scalar(Scalar::Uint(_)),
+            )
+            | (
+                other @ Ty::Scalar(Scalar::Uint(_)),
+                Ty::InferenceVar(tv, TyVariableKind::Integer),
+            )
+            | (Ty::InferenceVar(tv, TyVariableKind::Float), other @ Ty::Scalar(Scalar::Float(_)))
+            | (other @ Ty::Scalar(Scalar::Float(_)), Ty::InferenceVar(tv, TyVariableKind::Float)) =>
+            {
                 // the type var is unknown since we tried to resolve it
-                self.var_unification_table.union_value(*tv, TypeVarValue::Known(other.clone()));
+                self.var_unification_table
+                    .union_value(tv.to_inner(), TypeVarValue::Known(other.clone()));
                 true
             }
 
@@ -350,7 +390,7 @@ impl InferenceTable {
                 mark::hit!(type_var_resolves_to_int_var);
             }
             match &*ty {
-                Ty::Infer(tv) => {
+                Ty::InferenceVar(tv, _) => {
                     let inner = tv.to_inner();
                     match self.var_unification_table.inlined_probe_value(inner).known() {
                         Some(known_ty) => {
@@ -373,12 +413,12 @@ impl InferenceTable {
     /// known type.
     fn resolve_ty_as_possible_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty {
         ty.fold(&mut |ty| match ty {
-            Ty::Infer(tv) => {
+            Ty::InferenceVar(tv, kind) => {
                 let inner = tv.to_inner();
                 if tv_stack.contains(&inner) {
                     mark::hit!(type_var_cycles_resolve_as_possible);
                     // recursive type
-                    return tv.fallback_value();
+                    return self.type_variable_table.fallback_value(tv, kind);
                 }
                 if let Some(known_ty) =
                     self.var_unification_table.inlined_probe_value(inner).known()
@@ -400,12 +440,12 @@ impl InferenceTable {
     /// replaced by Ty::Unknown.
     fn resolve_ty_completely_inner(&mut self, tv_stack: &mut Vec<TypeVarId>, ty: Ty) -> Ty {
         ty.fold(&mut |ty| match ty {
-            Ty::Infer(tv) => {
+            Ty::InferenceVar(tv, kind) => {
                 let inner = tv.to_inner();
                 if tv_stack.contains(&inner) {
                     mark::hit!(type_var_cycles_resolve_completely);
                     // recursive type
-                    return tv.fallback_value();
+                    return self.type_variable_table.fallback_value(tv, kind);
                 }
                 if let Some(known_ty) =
                     self.var_unification_table.inlined_probe_value(inner).known()
@@ -416,7 +456,7 @@ impl InferenceTable {
                     tv_stack.pop();
                     result
                 } else {
-                    tv.fallback_value()
+                    self.type_variable_table.fallback_value(tv, kind)
                 }
             }
             _ => ty,
@@ -426,7 +466,7 @@ impl InferenceTable {
 
 /// The ID of a type variable.
 #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
-pub struct TypeVarId(pub(super) u32);
+pub(super) struct TypeVarId(pub(super) u32);
 
 impl UnifyKey for TypeVarId {
     type Value = TypeVarValue;
@@ -447,7 +487,7 @@ impl UnifyKey for TypeVarId {
 /// The value of a type variable: either we already know the type, or we don't
 /// know it yet.
 #[derive(Clone, PartialEq, Eq, Debug)]
-pub enum TypeVarValue {
+pub(super) enum TypeVarValue {
     Known(Ty),
     Unknown,
 }