diff --git a/compiler/noirc_driver/src/abi_gen.rs b/compiler/noirc_driver/src/abi_gen.rs
index fcae136349d..ad54d0f7d6b 100644
--- a/compiler/noirc_driver/src/abi_gen.rs
+++ b/compiler/noirc_driver/src/abi_gen.rs
@@ -7,6 +7,7 @@ use noirc_abi::{
     Abi, AbiErrorType, AbiParameter, AbiReturnType, AbiType, AbiValue, AbiVisibility, Sign,
 };
 use noirc_frontend::ast::{Signedness, Visibility};
+use noirc_frontend::TypeBinding;
 use noirc_frontend::{
     hir::Context,
     hir_def::{
@@ -17,7 +18,6 @@ use noirc_frontend::{
     },
     node_interner::{FuncId, NodeInterner},
 };
-use noirc_frontend::{TypeBinding, TypeVariableKind};
 
 /// Arranges a function signature and a generated circuit's return witnesses into a
 /// `noirc_abi::Abi`.
@@ -72,13 +72,18 @@ pub(super) fn abi_type_from_hir_type(context: &Context, typ: &Type) -> AbiType {
 
             AbiType::Integer { sign, width: (*bit_width).into() }
         }
-        Type::TypeVariable(binding, TypeVariableKind::IntegerOrField)
-        | Type::TypeVariable(binding, TypeVariableKind::Integer) => match &*binding.borrow() {
-            TypeBinding::Bound(typ) => abi_type_from_hir_type(context, typ),
-            TypeBinding::Unbound(_) => {
-                abi_type_from_hir_type(context, &Type::default_int_or_field_type())
+        Type::TypeVariable(binding) => {
+            if binding.is_integer() || binding.is_integer_or_field() {
+                match &*binding.borrow() {
+                    TypeBinding::Bound(typ) => abi_type_from_hir_type(context, typ),
+                    TypeBinding::Unbound(_id, _kind) => {
+                        abi_type_from_hir_type(context, &Type::default_int_or_field_type())
+                    }
+                }
+            } else {
+                unreachable!("{typ} cannot be used in the abi")
             }
-        },
+        }
         Type::Bool => AbiType::Boolean,
         Type::String(size) => {
             let size = size
@@ -106,7 +111,6 @@ pub(super) fn abi_type_from_hir_type(context: &Context, typ: &Type) -> AbiType {
         | Type::Constant(..)
         | Type::InfixExpr(..)
         | Type::TraitAsType(..)
-        | Type::TypeVariable(_, _)
         | Type::NamedGeneric(..)
         | Type::Forall(..)
         | Type::Quoted(_)
diff --git a/compiler/noirc_frontend/src/ast/expression.rs b/compiler/noirc_frontend/src/ast/expression.rs
index 095356682fd..362f94171d3 100644
--- a/compiler/noirc_frontend/src/ast/expression.rs
+++ b/compiler/noirc_frontend/src/ast/expression.rs
@@ -1,11 +1,12 @@
 use std::borrow::Cow;
 use std::fmt::Display;
 
+use thiserror::Error;
+
 use crate::ast::{
     Ident, ItemVisibility, Path, Pattern, Recoverable, Statement, StatementKind,
     UnresolvedTraitConstraint, UnresolvedType, UnresolvedTypeData, Visibility,
 };
-use crate::hir::def_collector::errors::DefCollectorErrorKind;
 use crate::node_interner::{
     ExprId, InternedExpressionKind, InternedStatementKind, QuotedTypeId, StructId,
 };
@@ -76,6 +77,13 @@ pub enum UnresolvedGeneric {
     Resolved(QuotedTypeId, Span),
 }
 
+#[derive(Error, PartialEq, Eq, Debug, Clone)]
+#[error("The only supported types of numeric generics are integers, fields, and booleans")]
+pub struct UnsupportedNumericGenericType {
+    pub ident: Ident,
+    pub typ: UnresolvedTypeData,
+}
+
 impl UnresolvedGeneric {
     pub fn span(&self) -> Span {
         match self {
@@ -85,7 +93,7 @@ impl UnresolvedGeneric {
         }
     }
 
-    pub fn kind(&self) -> Result<Kind, DefCollectorErrorKind> {
+    pub fn kind(&self) -> Result<Kind, UnsupportedNumericGenericType> {
         match self {
             UnresolvedGeneric::Variable(_) => Ok(Kind::Normal),
             UnresolvedGeneric::Numeric { typ, .. } => {
@@ -101,14 +109,14 @@ impl UnresolvedGeneric {
     fn resolve_numeric_kind_type(
         &self,
         typ: &UnresolvedType,
-    ) -> Result<Type, DefCollectorErrorKind> {
+    ) -> Result<Type, UnsupportedNumericGenericType> {
         use crate::ast::UnresolvedTypeData::{FieldElement, Integer};
 
         match typ.typ {
             FieldElement => Ok(Type::FieldElement),
             Integer(sign, bits) => Ok(Type::Integer(sign, bits)),
             // Only fields and integers are supported for numeric kinds
-            _ => Err(DefCollectorErrorKind::UnsupportedNumericGenericType {
+            _ => Err(UnsupportedNumericGenericType {
                 ident: self.ident().clone(),
                 typ: typ.typ.clone(),
             }),
diff --git a/compiler/noirc_frontend/src/elaborator/mod.rs b/compiler/noirc_frontend/src/elaborator/mod.rs
index 5f1b97f5eed..bc1976febd4 100644
--- a/compiler/noirc_frontend/src/elaborator/mod.rs
+++ b/compiler/noirc_frontend/src/elaborator/mod.rs
@@ -8,7 +8,7 @@ use crate::{
     ast::{
         BlockExpression, FunctionKind, GenericTypeArgs, Ident, NoirFunction, NoirStruct, Param,
         Path, Pattern, TraitBound, UnresolvedGeneric, UnresolvedGenerics,
-        UnresolvedTraitConstraint, UnresolvedTypeData,
+        UnresolvedTraitConstraint, UnresolvedTypeData, UnsupportedNumericGenericType,
     },
     graph::CrateId,
     hir::{
@@ -345,8 +345,9 @@ impl<'context> Elaborator<'context> {
     fn introduce_generics_into_scope(&mut self, all_generics: Vec<ResolvedGeneric>) {
         // Introduce all numeric generics into scope
         for generic in &all_generics {
-            if let Kind::Numeric(typ) = &generic.kind {
-                let definition = DefinitionKind::NumericGeneric(generic.type_var.clone());
+            if let Kind::Numeric(typ) = &generic.kind() {
+                let definition =
+                    DefinitionKind::NumericGeneric(generic.type_var.clone(), typ.clone());
                 let ident = Ident::new(generic.name.to_string(), generic.span);
                 let hir_ident = self.add_variable_decl(
                     ident, false, // mutable
@@ -461,9 +462,9 @@ impl<'context> Elaborator<'context> {
         let context = self.function_context.pop().expect("Imbalanced function_context pushes");
 
         for typ in context.type_variables {
-            if let Type::TypeVariable(variable, kind) = typ.follow_bindings() {
+            if let Type::TypeVariable(variable) = typ.follow_bindings() {
                 let msg = "TypeChecker should only track defaultable type vars";
-                variable.bind(kind.default_type().expect(msg));
+                variable.bind(variable.kind().default_type().expect(msg));
             }
         }
 
@@ -501,11 +502,12 @@ impl<'context> Elaborator<'context> {
         trait_constraints: &mut Vec<TraitConstraint>,
     ) -> Type {
         let new_generic_id = self.interner.next_type_variable_id();
-        let new_generic = TypeVariable::unbound(new_generic_id);
+
+        let new_generic = TypeVariable::unbound(new_generic_id, Kind::Normal);
         generics.push(new_generic.clone());
 
         let name = format!("impl {trait_path}");
-        let generic_type = Type::NamedGeneric(new_generic, Rc::new(name), Kind::Normal);
+        let generic_type = Type::NamedGeneric(new_generic, Rc::new(name));
         let trait_bound = TraitBound { trait_path, trait_id: None, trait_generics };
 
         if let Some(new_constraint) = self.resolve_trait_bound(&trait_bound, generic_type.clone()) {
@@ -520,19 +522,20 @@ impl<'context> Elaborator<'context> {
     pub fn add_generics(&mut self, generics: &UnresolvedGenerics) -> Generics {
         vecmap(generics, |generic| {
             let mut is_error = false;
-            let (type_var, name, kind) = match self.resolve_generic(generic) {
+            let (type_var, name) = match self.resolve_generic(generic) {
                 Ok(values) => values,
                 Err(error) => {
                     self.push_err(error);
                     is_error = true;
                     let id = self.interner.next_type_variable_id();
-                    (TypeVariable::unbound(id), Rc::new("(error)".into()), Kind::Normal)
+                    let kind = self.resolve_generic_kind(generic);
+                    (TypeVariable::unbound(id, kind), Rc::new("(error)".into()))
                 }
             };
 
             let span = generic.span();
             let name_owned = name.as_ref().clone();
-            let resolved_generic = ResolvedGeneric { name, type_var, kind, span };
+            let resolved_generic = ResolvedGeneric { name, type_var, span };
 
             // Check for name collisions of this generic
             // Checking `is_error` here prevents DuplicateDefinition errors when
@@ -557,25 +560,22 @@ impl<'context> Elaborator<'context> {
     fn resolve_generic(
         &mut self,
         generic: &UnresolvedGeneric,
-    ) -> Result<(TypeVariable, Rc<String>, Kind), ResolverError> {
+    ) -> Result<(TypeVariable, Rc<String>), ResolverError> {
         // Map the generic to a fresh type variable
         match generic {
             UnresolvedGeneric::Variable(_) | UnresolvedGeneric::Numeric { .. } => {
                 let id = self.interner.next_type_variable_id();
-                let typevar = TypeVariable::unbound(id);
-                let ident = generic.ident();
-
                 let kind = self.resolve_generic_kind(generic);
+                let typevar = TypeVariable::unbound(id, kind);
+                let ident = generic.ident();
                 let name = Rc::new(ident.0.contents.clone());
-                Ok((typevar, name, kind))
+                Ok((typevar, name))
             }
             // An already-resolved generic is only possible if it is the result of a
             // previous macro call being inserted into a generics list.
             UnresolvedGeneric::Resolved(id, span) => {
                 match self.interner.get_quoted_type(*id).follow_bindings() {
-                    Type::NamedGeneric(type_variable, name, kind) => {
-                        Ok((type_variable, name, kind))
-                    }
+                    Type::NamedGeneric(type_variable, name) => Ok((type_variable.clone(), name)),
                     other => Err(ResolverError::MacroResultInGenericsListNotAGeneric {
                         span: *span,
                         typ: other.clone(),
@@ -590,17 +590,21 @@ impl<'context> Elaborator<'context> {
     /// sure only primitive numeric types are being used.
     pub(super) fn resolve_generic_kind(&mut self, generic: &UnresolvedGeneric) -> Kind {
         if let UnresolvedGeneric::Numeric { ident, typ } = generic {
-            let typ = typ.clone();
-            let typ = if typ.is_type_expression() {
-                self.resolve_type_inner(typ, &Kind::Numeric(Box::new(Type::default_int_type())))
+            let unresolved_typ = typ.clone();
+            let typ = if unresolved_typ.is_type_expression() {
+                self.resolve_type_inner(
+                    unresolved_typ.clone(),
+                    &Kind::Numeric(Box::new(Type::default_int_type())),
+                )
             } else {
-                self.resolve_type(typ.clone())
+                self.resolve_type(unresolved_typ.clone())
             };
             if !matches!(typ, Type::FieldElement | Type::Integer(_, _)) {
-                let unsupported_typ_err = ResolverError::UnsupportedNumericGenericType {
-                    ident: ident.clone(),
-                    typ: typ.clone(),
-                };
+                let unsupported_typ_err =
+                    ResolverError::UnsupportedNumericGenericType(UnsupportedNumericGenericType {
+                        ident: ident.clone(),
+                        typ: unresolved_typ.typ.clone(),
+                    });
                 self.push_err(unsupported_typ_err);
             }
             Kind::Numeric(Box::new(typ))
@@ -735,6 +739,7 @@ impl<'context> Elaborator<'context> {
                 UnresolvedTypeData::TraitAsType(path, args) => {
                     self.desugar_impl_trait_arg(path, args, &mut generics, &mut trait_constraints)
                 }
+                // Function parameters have Kind::Normal
                 _ => self.resolve_type_inner(typ, &Kind::Normal),
             };
 
diff --git a/compiler/noirc_frontend/src/elaborator/patterns.rs b/compiler/noirc_frontend/src/elaborator/patterns.rs
index 91c4b17a857..132d1988b78 100644
--- a/compiler/noirc_frontend/src/elaborator/patterns.rs
+++ b/compiler/noirc_frontend/src/elaborator/patterns.rs
@@ -16,7 +16,7 @@ use crate::{
         stmt::HirPattern,
     },
     node_interner::{DefinitionId, DefinitionKind, ExprId, FuncId, GlobalId, TraitImplKind},
-    ResolvedGeneric, Shared, StructType, Type, TypeBindings,
+    Kind, ResolvedGeneric, Shared, StructType, Type, TypeBindings,
 };
 
 use super::{Elaborator, ResolverMeta};
@@ -489,7 +489,7 @@ impl<'context> Elaborator<'context> {
     ) -> Vec<Type> {
         let generics_with_types = generics.iter().zip(turbofish_generics);
         vecmap(generics_with_types, |(generic, unresolved_type)| {
-            self.resolve_type_inner(unresolved_type, &generic.kind)
+            self.resolve_type_inner(unresolved_type, &generic.kind())
         })
     }
 
@@ -558,13 +558,14 @@ impl<'context> Elaborator<'context> {
 
                         self.interner.add_global_reference(global_id, hir_ident.location);
                     }
-                    DefinitionKind::NumericGeneric(_) => {
+                    DefinitionKind::NumericGeneric(_, ref numeric_typ) => {
                         // Initialize numeric generics to a polymorphic integer type in case
                         // they're used in expressions. We must do this here since type_check_variable
                         // does not check definition kinds and otherwise expects parameters to
                         // already be typed.
                         if self.interner.definition_type(hir_ident.id) == Type::Error {
-                            let typ = Type::polymorphic_integer_or_field(self.interner);
+                            let type_var_kind = Kind::Numeric(numeric_typ.clone());
+                            let typ = self.type_variable_with_kind(type_var_kind);
                             self.interner.push_definition_type(hir_ident.id, typ);
                         }
                     }
diff --git a/compiler/noirc_frontend/src/elaborator/trait_impls.rs b/compiler/noirc_frontend/src/elaborator/trait_impls.rs
index 2f9c927fae6..858cfa5cdd6 100644
--- a/compiler/noirc_frontend/src/elaborator/trait_impls.rs
+++ b/compiler/noirc_frontend/src/elaborator/trait_impls.rs
@@ -153,11 +153,15 @@ impl<'context> Elaborator<'context> {
         // Substitute each generic on the trait function with the corresponding generic on the impl function
         for (
             ResolvedGeneric { type_var: trait_fn_generic, .. },
-            ResolvedGeneric { name, type_var: impl_fn_generic, kind, .. },
+            ResolvedGeneric { name, type_var: impl_fn_generic, .. },
         ) in method.direct_generics.iter().zip(&override_meta.direct_generics)
         {
-            let arg = Type::NamedGeneric(impl_fn_generic.clone(), name.clone(), kind.clone());
-            bindings.insert(trait_fn_generic.id(), (trait_fn_generic.clone(), arg));
+            let trait_fn_kind = trait_fn_generic.kind();
+            let arg = Type::NamedGeneric(impl_fn_generic.clone(), name.clone());
+            bindings.insert(
+                trait_fn_generic.id(),
+                (trait_fn_generic.clone(), trait_fn_kind.clone(), arg),
+            );
         }
 
         let mut substituted_method_ids = HashSet::default();
diff --git a/compiler/noirc_frontend/src/elaborator/traits.rs b/compiler/noirc_frontend/src/elaborator/traits.rs
index 21e2edf3822..b4042bd3e31 100644
--- a/compiler/noirc_frontend/src/elaborator/traits.rs
+++ b/compiler/noirc_frontend/src/elaborator/traits.rs
@@ -12,7 +12,7 @@ use crate::{
     hir::{def_collector::dc_crate::UnresolvedTrait, type_check::TypeCheckError},
     hir_def::{function::Parameters, traits::TraitFunction},
     node_interner::{FuncId, NodeInterner, ReferenceId, TraitId},
-    Kind, ResolvedGeneric, Type, TypeBindings, TypeVariableKind,
+    ResolvedGeneric, Type, TypeBindings,
 };
 
 use super::Elaborator;
@@ -79,8 +79,7 @@ impl<'context> Elaborator<'context> {
                 self.recover_generics(|this| {
                     let the_trait = this.interner.get_trait(trait_id);
                     let self_typevar = the_trait.self_type_typevar.clone();
-                    let self_type =
-                        Type::TypeVariable(self_typevar.clone(), TypeVariableKind::Normal);
+                    let self_type = Type::TypeVariable(self_typevar.clone());
                     let name_span = the_trait.name.span();
 
                     this.add_existing_generic(
@@ -90,7 +89,6 @@ impl<'context> Elaborator<'context> {
                             name: Rc::new("Self".to_owned()),
                             type_var: self_typevar,
                             span: name_span,
-                            kind: Kind::Normal,
                         },
                     );
                     this.self_type = Some(self_type.clone());
@@ -279,11 +277,12 @@ pub(crate) fn check_trait_impl_method_matches_declaration(
         // Substitute each generic on the trait function with the corresponding generic on the impl function
         for (
             ResolvedGeneric { type_var: trait_fn_generic, .. },
-            ResolvedGeneric { name, type_var: impl_fn_generic, kind, .. },
+            ResolvedGeneric { name, type_var: impl_fn_generic, .. },
         ) in trait_fn_meta.direct_generics.iter().zip(&meta.direct_generics)
         {
-            let arg = Type::NamedGeneric(impl_fn_generic.clone(), name.clone(), kind.clone());
-            bindings.insert(trait_fn_generic.id(), (trait_fn_generic.clone(), arg));
+            let trait_fn_kind = trait_fn_generic.kind();
+            let arg = Type::NamedGeneric(impl_fn_generic.clone(), name.clone());
+            bindings.insert(trait_fn_generic.id(), (trait_fn_generic.clone(), trait_fn_kind, arg));
         }
 
         let (declaration_type, _) = trait_fn_meta.typ.instantiate_with_bindings(bindings, interner);
diff --git a/compiler/noirc_frontend/src/elaborator/types.rs b/compiler/noirc_frontend/src/elaborator/types.rs
index 80a9133d0d7..35cd5145579 100644
--- a/compiler/noirc_frontend/src/elaborator/types.rs
+++ b/compiler/noirc_frontend/src/elaborator/types.rs
@@ -36,7 +36,7 @@ use crate::{
     },
     token::SecondaryAttribute,
     Generics, Kind, ResolvedGeneric, Type, TypeBinding, TypeBindings, TypeVariable,
-    TypeVariableKind, UnificationError,
+    UnificationError,
 };
 
 use super::{lints, Elaborator};
@@ -125,7 +125,7 @@ impl<'context> Elaborator<'context> {
                 let env = Box::new(self.resolve_type_inner(*env, kind));
 
                 match *env {
-                    Type::Unit | Type::Tuple(_) | Type::NamedGeneric(_, _, _) => {
+                    Type::Unit | Type::Tuple(_) | Type::NamedGeneric(_, _) => {
                         Type::Function(args, ret, env, unconstrained)
                     }
                     _ => {
@@ -168,14 +168,10 @@ impl<'context> Elaborator<'context> {
             _ => (),
         }
 
-        if !kind.matches_opt(resolved_type.kind()) {
+        if !kind.unifies(&resolved_type.kind()) {
             let expected_typ_err = CompilationError::TypeError(TypeCheckError::TypeKindMismatch {
                 expected_kind: kind.to_string(),
-                expr_kind: resolved_type
-                    .kind()
-                    .as_ref()
-                    .map(Kind::to_string)
-                    .unwrap_or("unknown".to_string()),
+                expr_kind: resolved_type.kind().to_string(),
                 expr_span: span,
             });
             self.errors.push((expected_typ_err, self.file));
@@ -229,7 +225,7 @@ impl<'context> Elaborator<'context> {
                     return self_type;
                 }
             } else if name == WILDCARD_TYPE {
-                return self.interner.next_type_variable();
+                return self.interner.next_type_variable_with_kind(Kind::Any);
             }
         } else if let Some(typ) = self.lookup_associated_type_on_self(&path) {
             if !args.is_empty() {
@@ -332,7 +328,7 @@ impl<'context> Elaborator<'context> {
 
         let ordered_args = expected_kinds.iter().zip(args.ordered_args);
         let ordered =
-            vecmap(ordered_args, |(generic, typ)| self.resolve_type_inner(typ, &generic.kind));
+            vecmap(ordered_args, |(generic, typ)| self.resolve_type_inner(typ, &generic.kind()));
 
         let mut associated = Vec::new();
 
@@ -376,7 +372,7 @@ impl<'context> Elaborator<'context> {
             let expected = required_args.remove(index);
             seen_args.insert(name.0.contents.clone(), name.span());
 
-            let typ = self.resolve_type_inner(typ, &expected.kind);
+            let typ = self.resolve_type_inner(typ, &expected.kind());
             resolved.push(NamedType { name, typ });
         }
 
@@ -395,7 +391,7 @@ impl<'context> Elaborator<'context> {
             let name = path.last_name();
             if let Some(generic) = self.find_generic(name) {
                 let generic = generic.clone();
-                return Some(Type::NamedGeneric(generic.type_var, generic.name, generic.kind));
+                return Some(Type::NamedGeneric(generic.type_var, generic.name));
             }
         } else if let Some(typ) = self.lookup_associated_type_on_self(path) {
             return Some(typ);
@@ -451,7 +447,7 @@ impl<'context> Elaborator<'context> {
                             });
                             return Type::Error;
                         }
-                        if let Some(result) = op.function(lhs, rhs) {
+                        if let Some(result) = op.function(lhs, rhs, &lhs_kind) {
                             Type::Constant(result, lhs_kind)
                         } else {
                             self.push_err(ResolverError::OverflowInType { lhs, op, rhs, span });
@@ -469,15 +465,13 @@ impl<'context> Elaborator<'context> {
     }
 
     fn check_kind(&mut self, typ: Type, expected_kind: &Kind, span: Span) -> Type {
-        if let Some(kind) = typ.kind() {
-            if !kind.unifies(expected_kind) {
-                self.push_err(TypeCheckError::TypeKindMismatch {
-                    expected_kind: expected_kind.to_string(),
-                    expr_kind: kind.to_string(),
-                    expr_span: span,
-                });
-                return Type::Error;
-            }
+        if !typ.kind().unifies(expected_kind) {
+            self.push_err(TypeCheckError::TypeKindMismatch {
+                expected_kind: expected_kind.to_string(),
+                expr_kind: typ.kind().to_string(),
+                expr_span: span,
+            });
+            return Type::Error;
         }
         typ
     }
@@ -579,7 +573,7 @@ impl<'context> Elaborator<'context> {
         }
 
         for constraint in self.trait_bounds.clone() {
-            if let Type::NamedGeneric(_, name, _) = &constraint.typ {
+            if let Type::NamedGeneric(_, name) = &constraint.typ {
                 // if `path` is `T::method_name`, we're looking for constraint of the form `T: SomeTrait`
                 if path.segments[0].ident.0.contents != name.as_str() {
                     continue;
@@ -696,11 +690,21 @@ impl<'context> Elaborator<'context> {
         typ
     }
 
+    /// Return a fresh integer type variable and log it
+    /// in self.type_variables to default it later.
+    pub(super) fn type_variable_with_kind(&mut self, type_var_kind: Kind) -> Type {
+        let typ = Type::type_variable_with_kind(self.interner, type_var_kind);
+        self.push_type_variable(typ.clone());
+        typ
+    }
+
     /// Translates a (possibly Unspecified) UnresolvedType to a Type.
     /// Any UnresolvedType::Unspecified encountered are replaced with fresh type variables.
     pub(super) fn resolve_inferred_type(&mut self, typ: UnresolvedType) -> Type {
         match &typ.typ {
-            UnresolvedTypeData::Unspecified => self.interner.next_type_variable(),
+            UnresolvedTypeData::Unspecified => {
+                self.interner.next_type_variable_with_kind(Kind::Any)
+            }
             _ => self.resolve_type(typ),
         }
     }
@@ -789,7 +793,7 @@ impl<'context> Elaborator<'context> {
         // Could do a single unification for the entire function type, but matching beforehand
         // lets us issue a more precise error on the individual argument that fails to type check.
         match function {
-            Type::TypeVariable(binding, TypeVariableKind::Normal) => {
+            Type::TypeVariable(binding) if binding.kind() == Kind::Normal => {
                 if let TypeBinding::Bound(typ) = &*binding.borrow() {
                     return self.bind_function_type(typ.clone(), args, span);
                 }
@@ -800,7 +804,8 @@ impl<'context> Elaborator<'context> {
                 let expected =
                     Type::Function(args, Box::new(ret.clone()), Box::new(env_type), false);
 
-                if let Err(error) = binding.try_bind(expected, span) {
+                let expected_kind = expected.kind();
+                if let Err(error) = binding.try_bind(expected, &expected_kind, span) {
                     self.push_err(error);
                 }
                 ret
@@ -820,16 +825,14 @@ impl<'context> Elaborator<'context> {
 
     pub(super) fn check_cast(&mut self, from: &Type, to: &Type, span: Span) -> Type {
         match from.follow_bindings() {
-            Type::Integer(..)
-            | Type::FieldElement
-            | Type::TypeVariable(_, TypeVariableKind::IntegerOrField)
-            | Type::TypeVariable(_, TypeVariableKind::Integer)
-            | Type::Bool => (),
+            Type::Integer(..) | Type::FieldElement | Type::Bool => (),
 
-            Type::TypeVariable(_, _) => {
+            Type::TypeVariable(var) if var.is_integer() || var.is_integer_or_field() => (),
+
+            Type::TypeVariable(_) => {
                 // NOTE: in reality the expected type can also include bool, but for the compiler's simplicity
                 // we only allow integer types. If a bool is in `from` it will need an explicit type annotation.
-                let expected = Type::polymorphic_integer_or_field(self.interner);
+                let expected = self.polymorphic_integer_or_field();
                 self.unify(from, &expected, || TypeCheckError::InvalidCast {
                     from: from.clone(),
                     span,
@@ -877,8 +880,8 @@ impl<'context> Elaborator<'context> {
 
             // Matches on TypeVariable must be first to follow any type
             // bindings.
-            (TypeVariable(var, _), other) | (other, TypeVariable(var, _)) => {
-                if let TypeBinding::Bound(binding) = &*var.borrow() {
+            (TypeVariable(var), other) | (other, TypeVariable(var)) => {
+                if let TypeBinding::Bound(ref binding) = &*var.borrow() {
                     return self.comparator_operand_type_rules(other, binding, op, span);
                 }
 
@@ -942,14 +945,14 @@ impl<'context> Elaborator<'context> {
             span,
         });
 
-        let use_impl = !lhs_type.is_numeric();
+        let use_impl = !lhs_type.is_numeric_value();
 
         // If this operator isn't valid for fields we have to possibly narrow
-        // TypeVariableKind::IntegerOrField to TypeVariableKind::Integer.
+        // Kind::IntegerOrField to Kind::Integer.
         // Doing so also ensures a type error if Field is used.
         // The is_numeric check is to allow impls for custom types to bypass this.
-        if !op.kind.is_valid_for_field_type() && lhs_type.is_numeric() {
-            let target = Type::polymorphic_integer(self.interner);
+        if !op.kind.is_valid_for_field_type() && lhs_type.is_numeric_value() {
+            let target = self.polymorphic_integer();
 
             use crate::ast::BinaryOpKind::*;
             use TypeCheckError::*;
@@ -990,22 +993,22 @@ impl<'context> Elaborator<'context> {
 
             // Matches on TypeVariable must be first so that we follow any type
             // bindings.
-            (TypeVariable(int, _), other) | (other, TypeVariable(int, _)) => {
+            (TypeVariable(int), other) | (other, TypeVariable(int)) => {
                 if op.kind == BinaryOpKind::ShiftLeft || op.kind == BinaryOpKind::ShiftRight {
                     self.unify(
                         rhs_type,
                         &Type::Integer(Signedness::Unsigned, IntegerBitSize::Eight),
                         || TypeCheckError::InvalidShiftSize { span },
                     );
-                    let use_impl = if lhs_type.is_numeric() {
-                        let integer_type = Type::polymorphic_integer(self.interner);
+                    let use_impl = if lhs_type.is_numeric_value() {
+                        let integer_type = self.polymorphic_integer();
                         self.bind_type_variables_for_infix(lhs_type, op, &integer_type, span)
                     } else {
                         true
                     };
                     return Ok((lhs_type.clone(), use_impl));
                 }
-                if let TypeBinding::Bound(binding) = &*int.borrow() {
+                if let TypeBinding::Bound(ref binding) = &*int.borrow() {
                     return self.infix_operand_type_rules(binding, op, other, span);
                 }
                 let use_impl = self.bind_type_variables_for_infix(lhs_type, op, rhs_type, span);
@@ -1090,21 +1093,21 @@ impl<'context> Elaborator<'context> {
 
                     // Matches on TypeVariable must be first so that we follow any type
                     // bindings.
-                    TypeVariable(int, _) => {
-                        if let TypeBinding::Bound(binding) = &*int.borrow() {
+                    TypeVariable(int) => {
+                        if let TypeBinding::Bound(ref binding) = &*int.borrow() {
                             return self.prefix_operand_type_rules(op, binding, span);
                         }
 
                         // The `!` prefix operator is not valid for Field, so if this is a numeric
                         // type we constrain it to just (non-Field) integer types.
-                        if matches!(op, crate::ast::UnaryOp::Not) && rhs_type.is_numeric() {
+                        if matches!(op, crate::ast::UnaryOp::Not) && rhs_type.is_numeric_value() {
                             let integer_type = Type::polymorphic_integer(self.interner);
                             self.unify(rhs_type, &integer_type, || {
                                 TypeCheckError::InvalidUnaryOp { kind: rhs_type.to_string(), span }
                             });
                         }
 
-                        Ok((rhs_type.clone(), !rhs_type.is_numeric()))
+                        Ok((rhs_type.clone(), !rhs_type.is_numeric_value()))
                     }
                     Integer(sign_x, bit_width_x) => {
                         if *op == UnaryOp::Minus && *sign_x == Signedness::Unsigned {
@@ -1186,7 +1189,11 @@ impl<'context> Elaborator<'context> {
             let object_type = object_type.substitute(&bindings);
             bindings.insert(
                 the_trait.self_type_typevar.id(),
-                (the_trait.self_type_typevar.clone(), object_type.clone()),
+                (
+                    the_trait.self_type_typevar.clone(),
+                    the_trait.self_type_typevar.kind(),
+                    object_type.clone(),
+                ),
             );
             self.interner.select_impl_for_expression(
                 expr_id,
@@ -1267,7 +1274,7 @@ impl<'context> Elaborator<'context> {
                 });
                 None
             }
-            Type::NamedGeneric(_, _, _) => {
+            Type::NamedGeneric(_, _) => {
                 self.lookup_method_in_trait_constraints(object_type, method_name, span)
             }
             // Mutable references to another type should resolve to methods of their element type.
@@ -1283,7 +1290,7 @@ impl<'context> Elaborator<'context> {
             Type::Error => None,
 
             // The type variable must be unbound at this point since follow_bindings was called
-            Type::TypeVariable(_, TypeVariableKind::Normal) => {
+            Type::TypeVariable(var) if var.kind() == Kind::Normal => {
                 self.push_err(TypeCheckError::TypeAnnotationsNeededForMethodCall { span });
                 None
             }
@@ -1630,9 +1637,9 @@ impl<'context> Elaborator<'context> {
             | Type::Bool
             | Type::Unit
             | Type::Error
-            | Type::TypeVariable(_, _)
+            | Type::TypeVariable(_)
             | Type::Constant(..)
-            | Type::NamedGeneric(_, _, _)
+            | Type::NamedGeneric(_, _)
             | Type::Quoted(_)
             | Type::Forall(_, _) => (),
 
@@ -1646,7 +1653,7 @@ impl<'context> Elaborator<'context> {
             }
 
             Type::Array(length, element_type) => {
-                if let Type::NamedGeneric(type_variable, name, _) = length.as_ref() {
+                if let Type::NamedGeneric(type_variable, name) = length.as_ref() {
                     found.insert(name.to_string(), type_variable.clone());
                 }
                 Self::find_numeric_generics_in_type(element_type, found);
@@ -1671,7 +1678,7 @@ impl<'context> Elaborator<'context> {
 
             Type::Struct(struct_type, generics) => {
                 for (i, generic) in generics.iter().enumerate() {
-                    if let Type::NamedGeneric(type_variable, name, _) = generic {
+                    if let Type::NamedGeneric(type_variable, name) = generic {
                         if struct_type.borrow().generics[i].is_numeric() {
                             found.insert(name.to_string(), type_variable.clone());
                         }
@@ -1682,7 +1689,7 @@ impl<'context> Elaborator<'context> {
             }
             Type::Alias(alias, generics) => {
                 for (i, generic) in generics.iter().enumerate() {
-                    if let Type::NamedGeneric(type_variable, name, _) = generic {
+                    if let Type::NamedGeneric(type_variable, name) = generic {
                         if alias.borrow().generics[i].is_numeric() {
                             found.insert(name.to_string(), type_variable.clone());
                         }
@@ -1693,12 +1700,12 @@ impl<'context> Elaborator<'context> {
             }
             Type::MutableReference(element) => Self::find_numeric_generics_in_type(element, found),
             Type::String(length) => {
-                if let Type::NamedGeneric(type_variable, name, _) = length.as_ref() {
+                if let Type::NamedGeneric(type_variable, name) = length.as_ref() {
                     found.insert(name.to_string(), type_variable.clone());
                 }
             }
             Type::FmtString(length, fields) => {
-                if let Type::NamedGeneric(type_variable, name, _) = length.as_ref() {
+                if let Type::NamedGeneric(type_variable, name) = length.as_ref() {
                     found.insert(name.to_string(), type_variable.clone());
                 }
                 Self::find_numeric_generics_in_type(fields, found);
@@ -1751,7 +1758,10 @@ impl<'context> Elaborator<'context> {
         for (param, arg) in the_trait.generics.iter().zip(&constraint.trait_generics.ordered) {
             // Avoid binding t = t
             if !arg.occurs(param.type_var.id()) {
-                bindings.insert(param.type_var.id(), (param.type_var.clone(), arg.clone()));
+                bindings.insert(
+                    param.type_var.id(),
+                    (param.type_var.clone(), param.kind(), arg.clone()),
+                );
             }
         }
 
@@ -1770,7 +1780,10 @@ impl<'context> Elaborator<'context> {
 
             // Avoid binding t = t
             if !arg.typ.occurs(param.type_var.id()) {
-                bindings.insert(param.type_var.id(), (param.type_var.clone(), arg.typ.clone()));
+                bindings.insert(
+                    param.type_var.id(),
+                    (param.type_var.clone(), param.kind(), arg.typ.clone()),
+                );
             }
         }
 
@@ -1779,7 +1792,8 @@ impl<'context> Elaborator<'context> {
         // to specify a redundant type annotation.
         if assumed {
             let self_type = the_trait.self_type_typevar.clone();
-            bindings.insert(self_type.id(), (self_type, constraint.typ.clone()));
+            let kind = the_trait.self_type_typevar.kind();
+            bindings.insert(self_type.id(), (self_type, kind, constraint.typ.clone()));
         }
     }
 }
diff --git a/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs b/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs
index 90deef2deb7..63c32bc7e5f 100644
--- a/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/hir_to_display_ast.rs
@@ -316,10 +316,10 @@ impl Type {
                 let name = Path::from_ident(type_def.name.clone());
                 UnresolvedTypeData::Named(name, generics, false)
             }
-            Type::TypeVariable(binding, kind) => match &*binding.borrow() {
+            Type::TypeVariable(binding) => match &*binding.borrow() {
                 TypeBinding::Bound(typ) => return typ.to_display_ast(),
-                TypeBinding::Unbound(id) => {
-                    let name = format!("var_{:?}_{}", kind, id);
+                TypeBinding::Unbound(id, type_var_kind) => {
+                    let name = format!("var_{:?}_{}", type_var_kind, id);
                     let path = Path::from_single(name, Span::empty(0));
                     let expression = UnresolvedTypeExpression::Variable(path);
                     UnresolvedTypeData::Expression(expression)
@@ -334,7 +334,7 @@ impl Type {
                 let name = Path::from_single(name.as_ref().clone(), Span::default());
                 UnresolvedTypeData::TraitAsType(name, generics)
             }
-            Type::NamedGeneric(_var, name, _kind) => {
+            Type::NamedGeneric(_var, name) => {
                 let name = Path::from_single(name.as_ref().clone(), Span::default());
                 UnresolvedTypeData::Named(name, GenericTypeArgs::default(), true)
             }
@@ -374,7 +374,7 @@ impl Type {
 
         match self.follow_bindings() {
             Type::Constant(length, _kind) => UnresolvedTypeExpression::Constant(length, span),
-            Type::NamedGeneric(_var, name, _kind) => {
+            Type::NamedGeneric(_var, name) => {
                 let path = Path::from_single(name.as_ref().clone(), span);
                 UnresolvedTypeExpression::Variable(path)
             }
diff --git a/compiler/noirc_frontend/src/hir/comptime/interpreter.rs b/compiler/noirc_frontend/src/hir/comptime/interpreter.rs
index 473e1f25e34..b981dcb348f 100644
--- a/compiler/noirc_frontend/src/hir/comptime/interpreter.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/interpreter.rs
@@ -33,9 +33,10 @@ use crate::{
             HirAssignStatement, HirConstrainStatement, HirForStatement, HirLValue, HirLetStatement,
             HirPattern, HirStatement,
         },
+        types::Kind,
     },
     node_interner::{DefinitionId, DefinitionKind, ExprId, FuncId, NodeInterner, StmtId},
-    Shared, Type, TypeBinding, TypeBindings, TypeVariableKind,
+    Shared, Type, TypeBinding, TypeBindings,
 };
 
 use super::errors::{IResult, InterpreterError};
@@ -60,7 +61,7 @@ pub struct Interpreter<'local, 'interner> {
     /// Since the interpreter monomorphizes as it interprets, we can bind over the same generic
     /// multiple times. Without this map, when one of these inner functions exits we would
     /// unbind the generic completely instead of resetting it to its previous binding.
-    bound_generics: Vec<HashMap<TypeVariable, Type>>,
+    bound_generics: Vec<HashMap<TypeVariable, (Type, Kind)>>,
 }
 
 #[allow(unused)]
@@ -87,7 +88,8 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
         // To match the monomorphizer, we need to call follow_bindings on each of
         // the instantiation bindings before we unbind the generics from the previous function.
         // This is because the instantiation bindings refer to variables from the call site.
-        for (_, binding) in instantiation_bindings.values_mut() {
+        for (_, kind, binding) in instantiation_bindings.values_mut() {
+            *kind = kind.follow_bindings();
             *binding = binding.follow_bindings();
         }
 
@@ -96,7 +98,8 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
         let mut impl_bindings =
             perform_impl_bindings(self.elaborator.interner, trait_method, function, location)?;
 
-        for (_, binding) in impl_bindings.values_mut() {
+        for (_, kind, binding) in impl_bindings.values_mut() {
+            *kind = kind.follow_bindings();
             *binding = binding.follow_bindings();
         }
 
@@ -333,8 +336,8 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
 
     fn unbind_generics_from_previous_function(&mut self) {
         if let Some(bindings) = self.bound_generics.last() {
-            for var in bindings.keys() {
-                var.unbind(var.id());
+            for (var, (_, kind)) in bindings {
+                var.unbind(var.id(), kind.clone());
             }
         }
         // Push a new bindings list for the current function
@@ -346,7 +349,7 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
         self.bound_generics.pop();
 
         if let Some(bindings) = self.bound_generics.last() {
-            for (var, binding) in bindings {
+            for (var, (binding, _kind)) in bindings {
                 var.force_bind(binding.clone());
             }
         }
@@ -358,12 +361,12 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
             .last_mut()
             .expect("remember_bindings called with no bound_generics on the stack");
 
-        for (var, binding) in main_bindings.values() {
-            bound_generics.insert(var.clone(), binding.follow_bindings());
+        for (var, kind, binding) in main_bindings.values() {
+            bound_generics.insert(var.clone(), (binding.follow_bindings(), kind.clone()));
         }
 
-        for (var, binding) in impl_bindings.values() {
-            bound_generics.insert(var.clone(), binding.follow_bindings());
+        for (var, kind, binding) in impl_bindings.values() {
+            bound_generics.insert(var.clone(), (binding.follow_bindings(), kind.clone()));
         }
     }
 
@@ -580,9 +583,9 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                     Ok(value)
                 }
             }
-            DefinitionKind::NumericGeneric(type_variable) => {
+            DefinitionKind::NumericGeneric(type_variable, numeric_typ) => {
                 let value = match &*type_variable.borrow() {
-                    TypeBinding::Unbound(_) => None,
+                    TypeBinding::Unbound(_, _) => None,
                     TypeBinding::Bound(binding) => binding.evaluate_to_u32(),
                 };
 
@@ -591,7 +594,7 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                     self.evaluate_integer((value as u128).into(), false, id)
                 } else {
                     let location = self.elaborator.interner.expr_location(&id);
-                    let typ = Type::TypeVariable(type_variable.clone(), TypeVariableKind::Normal);
+                    let typ = Type::TypeVariable(type_variable.clone());
                     Err(InterpreterError::NonIntegerArrayLength { typ, location })
                 }
             }
@@ -750,14 +753,18 @@ impl<'local, 'interner> Interpreter<'local, 'interner> {
                     Ok(Value::I64(value))
                 }
             }
-        } else if let Type::TypeVariable(variable, TypeVariableKind::IntegerOrField) = &typ {
-            Ok(Value::Field(value))
-        } else if let Type::TypeVariable(variable, TypeVariableKind::Integer) = &typ {
-            let value: u64 = value
-                .try_to_u64()
-                .ok_or(InterpreterError::IntegerOutOfRangeForType { value, typ, location })?;
-            let value = if is_negative { 0u64.wrapping_sub(value) } else { value };
-            Ok(Value::U64(value))
+        } else if let Type::TypeVariable(variable) = &typ {
+            if variable.is_integer_or_field() {
+                Ok(Value::Field(value))
+            } else if variable.is_integer() {
+                let value: u64 = value
+                    .try_to_u64()
+                    .ok_or(InterpreterError::IntegerOutOfRangeForType { value, typ, location })?;
+                let value = if is_negative { 0u64.wrapping_sub(value) } else { value };
+                Ok(Value::U64(value))
+            } else {
+                Err(InterpreterError::NonIntegerIntegerLiteral { typ, location })
+            }
         } else {
             Err(InterpreterError::NonIntegerIntegerLiteral { typ, location })
         }
diff --git a/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs b/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs
index 4c81d4c3ed3..48827c087f9 100644
--- a/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs
+++ b/compiler/noirc_frontend/src/hir/comptime/interpreter/builtin.rs
@@ -404,11 +404,11 @@ fn struct_def_add_generic(
         }
     }
 
-    let type_var = TypeVariable::unbound(interner.next_type_variable_id());
+    let type_var_kind = Kind::Normal;
+    let type_var = TypeVariable::unbound(interner.next_type_variable_id(), type_var_kind);
     let span = generic_location.span;
-    let kind = Kind::Normal;
-    let typ = Type::NamedGeneric(type_var.clone(), name.clone(), kind.clone());
-    let new_generic = ResolvedGeneric { name, type_var, span, kind };
+    let typ = Type::NamedGeneric(type_var.clone(), name.clone());
+    let new_generic = ResolvedGeneric { name, type_var, span };
     the_struct.generics.push(new_generic);
 
     Ok(Value::Type(typ))
@@ -426,7 +426,7 @@ fn struct_def_as_type(
     let struct_def = struct_def_rc.borrow();
 
     let generics = vecmap(&struct_def.generics, |generic| {
-        Type::NamedGeneric(generic.type_var.clone(), generic.name.clone(), generic.kind.clone())
+        Type::NamedGeneric(generic.type_var.clone(), generic.name.clone())
     });
 
     drop(struct_def);
@@ -1196,14 +1196,14 @@ fn zeroed(return_type: Type) -> IResult<Value> {
             Ok(Value::Pointer(Shared::new(element), false))
         }
         // Optimistically assume we can resolve this type later or that the value is unused
-        Type::TypeVariable(_, _)
+        Type::TypeVariable(_)
         | Type::Forall(_, _)
         | Type::Constant(..)
         | Type::InfixExpr(..)
         | Type::Quoted(_)
         | Type::Error
         | Type::TraitAsType(..)
-        | Type::NamedGeneric(_, _, _) => Ok(Value::Zeroed(return_type)),
+        | Type::NamedGeneric(_, _) => Ok(Value::Zeroed(return_type)),
     }
 }
 
@@ -2079,7 +2079,7 @@ fn fmtstr_quoted_contents(
 
 // fn fresh_type_variable() -> Type
 fn fresh_type_variable(interner: &NodeInterner) -> IResult<Value> {
-    Ok(Value::Type(interner.next_type_variable()))
+    Ok(Value::Type(interner.next_type_variable_with_kind(Kind::Any)))
 }
 
 // fn add_attribute<let N: u32>(self, attribute: str<N>)
diff --git a/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs b/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
index 267c9bc84b8..4d348d998b7 100644
--- a/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
+++ b/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
@@ -23,7 +23,7 @@ use crate::node_interner::{
 use crate::ast::{
     ExpressionKind, GenericTypeArgs, Ident, ItemVisibility, LetStatement, Literal, NoirFunction,
     NoirStruct, NoirTrait, NoirTypeAlias, Path, PathKind, PathSegment, UnresolvedGenerics,
-    UnresolvedTraitConstraint, UnresolvedType,
+    UnresolvedTraitConstraint, UnresolvedType, UnsupportedNumericGenericType,
 };
 
 use crate::parser::{ParserError, SortedModule};
@@ -231,12 +231,19 @@ impl From<ResolverError> for CompilationError {
         CompilationError::ResolverError(value)
     }
 }
+
 impl From<TypeCheckError> for CompilationError {
     fn from(value: TypeCheckError) -> Self {
         CompilationError::TypeError(value)
     }
 }
 
+impl From<UnsupportedNumericGenericType> for CompilationError {
+    fn from(value: UnsupportedNumericGenericType) -> Self {
+        Self::ResolverError(value.into())
+    }
+}
+
 impl DefCollector {
     pub fn new(def_map: CrateDefMap) -> DefCollector {
         DefCollector {
diff --git a/compiler/noirc_frontend/src/hir/def_collector/dc_mod.rs b/compiler/noirc_frontend/src/hir/def_collector/dc_mod.rs
index dff63e045fe..0e20ec3a304 100644
--- a/compiler/noirc_frontend/src/hir/def_collector/dc_mod.rs
+++ b/compiler/noirc_frontend/src/hir/def_collector/dc_mod.rs
@@ -530,8 +530,10 @@ impl<'a> ModCollector<'a> {
 
                             associated_types.push(ResolvedGeneric {
                                 name: Rc::new(name.to_string()),
-                                type_var: TypeVariable::unbound(type_variable_id),
-                                kind: Kind::Numeric(Box::new(typ)),
+                                type_var: TypeVariable::unbound(
+                                    type_variable_id,
+                                    Kind::Numeric(Box::new(typ)),
+                                ),
                                 span: name.span(),
                             });
                         }
@@ -555,8 +557,7 @@ impl<'a> ModCollector<'a> {
                             let type_variable_id = context.def_interner.next_type_variable_id();
                             associated_types.push(ResolvedGeneric {
                                 name: Rc::new(name.to_string()),
-                                type_var: TypeVariable::unbound(type_variable_id),
-                                kind: Kind::Normal,
+                                type_var: TypeVariable::unbound(type_variable_id, Kind::Normal),
                                 span: name.span(),
                             });
                         }
diff --git a/compiler/noirc_frontend/src/hir/def_collector/errors.rs b/compiler/noirc_frontend/src/hir/def_collector/errors.rs
index 2f47505db94..d72f493092d 100644
--- a/compiler/noirc_frontend/src/hir/def_collector/errors.rs
+++ b/compiler/noirc_frontend/src/hir/def_collector/errors.rs
@@ -1,4 +1,4 @@
-use crate::ast::{Ident, ItemVisibility, Path, UnresolvedTypeData};
+use crate::ast::{Ident, ItemVisibility, Path, UnsupportedNumericGenericType};
 use crate::hir::resolution::import::PathResolutionError;
 use crate::hir::type_check::generics::TraitGenerics;
 
@@ -71,8 +71,6 @@ pub enum DefCollectorErrorKind {
         "Either the type or the trait must be from the same crate as the trait implementation"
     )]
     TraitImplOrphaned { span: Span },
-    #[error("The only supported types of numeric generics are integers, fields, and booleans")]
-    UnsupportedNumericGenericType { ident: Ident, typ: UnresolvedTypeData },
     #[error("impl has stricter requirements than trait")]
     ImplIsStricterThanTrait {
         constraint_typ: crate::Type,
@@ -82,6 +80,8 @@ pub enum DefCollectorErrorKind {
         trait_method_name: String,
         trait_method_span: Span,
     },
+    #[error("{0}")]
+    UnsupportedNumericGenericType(#[from] UnsupportedNumericGenericType),
 }
 
 impl DefCollectorErrorKind {
@@ -90,6 +90,19 @@ impl DefCollectorErrorKind {
     }
 }
 
+impl<'a> From<&'a UnsupportedNumericGenericType> for Diagnostic {
+    fn from(error: &'a UnsupportedNumericGenericType) -> Diagnostic {
+        let name = &error.ident.0.contents;
+        let typ = &error.typ;
+
+        Diagnostic::simple_error(
+            format!("{name} has a type of {typ}. The only supported numeric generic types are `u1`, `u8`, `u16`, and `u32`."),
+            "Unsupported numeric generic type".to_string(),
+            error.ident.0.span(),
+        )
+    }
+}
+
 impl fmt::Display for DuplicateType {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         match *self {
@@ -266,15 +279,6 @@ impl<'a> From<&'a DefCollectorErrorKind> for Diagnostic {
                 "Either the type or the trait must be from the same crate as the trait implementation".into(),
                 *span,
             ),
-            DefCollectorErrorKind::UnsupportedNumericGenericType { ident, typ } => {
-                let name = &ident.0.contents;
-
-                Diagnostic::simple_error(
-                    format!("{name} has a type of {typ}. The only supported types of numeric generics are integers and fields"),
-                    "Unsupported numeric generic type".to_string(),
-                    ident.0.span(),
-                )
-            }
             DefCollectorErrorKind::ImplIsStricterThanTrait { constraint_typ, constraint_name, constraint_generics, constraint_span, trait_method_name, trait_method_span } => {
                 let constraint = format!("{}{}", constraint_name, constraint_generics);
 
@@ -286,6 +290,7 @@ impl<'a> From<&'a DefCollectorErrorKind> for Diagnostic {
                 diag.add_secondary(format!("definition of `{trait_method_name}` from trait"), *trait_method_span);
                 diag
             }
+            DefCollectorErrorKind::UnsupportedNumericGenericType(err) => err.into(),
         }
     }
 }
diff --git a/compiler/noirc_frontend/src/hir/mod.rs b/compiler/noirc_frontend/src/hir/mod.rs
index c631edfa889..015b7deb6e0 100644
--- a/compiler/noirc_frontend/src/hir/mod.rs
+++ b/compiler/noirc_frontend/src/hir/mod.rs
@@ -11,7 +11,7 @@ use crate::graph::{CrateGraph, CrateId};
 use crate::hir_def::function::FuncMeta;
 use crate::node_interner::{FuncId, NodeInterner, StructId};
 use crate::parser::ParserError;
-use crate::{Generics, Kind, ParsedModule, ResolvedGeneric, Type, TypeVariable};
+use crate::{Generics, Kind, ParsedModule, ResolvedGeneric, TypeVariable};
 use def_collector::dc_crate::CompilationError;
 use def_map::{Contract, CrateDefMap};
 use fm::{FileId, FileManager};
@@ -280,19 +280,20 @@ impl Context<'_, '_> {
         vecmap(generics, |generic| {
             // Map the generic to a fresh type variable
             let id = interner.next_type_variable_id();
-            let type_var = TypeVariable::unbound(id);
+
+            let type_var_kind = generic.kind().unwrap_or_else(|err| {
+                errors.push((err.into(), file_id));
+                // When there's an error, unify with any other kinds
+                Kind::Any
+            });
+            let type_var = TypeVariable::unbound(id, type_var_kind);
             let ident = generic.ident();
             let span = ident.0.span();
 
             // Check for name collisions of this generic
             let name = Rc::new(ident.0.contents.clone());
 
-            let kind = generic.kind().unwrap_or_else(|err| {
-                errors.push((err.into(), file_id));
-                Kind::Numeric(Box::new(Type::Error))
-            });
-
-            ResolvedGeneric { name, type_var, kind, span }
+            ResolvedGeneric { name, type_var, span }
         })
     }
 
diff --git a/compiler/noirc_frontend/src/hir/resolution/errors.rs b/compiler/noirc_frontend/src/hir/resolution/errors.rs
index f3c61a7fbe2..4e9520ad761 100644
--- a/compiler/noirc_frontend/src/hir/resolution/errors.rs
+++ b/compiler/noirc_frontend/src/hir/resolution/errors.rs
@@ -3,7 +3,10 @@ use noirc_errors::{CustomDiagnostic as Diagnostic, FileDiagnostic};
 use thiserror::Error;
 
 use crate::{
-    ast::Ident, hir::comptime::InterpreterError, parser::ParserError, usage_tracker::UnusedItem,
+    ast::{Ident, UnsupportedNumericGenericType},
+    hir::comptime::InterpreterError,
+    parser::ParserError,
+    usage_tracker::UnusedItem,
     Type,
 };
 
@@ -103,8 +106,6 @@ pub enum ResolverError {
     NoPredicatesAttributeOnUnconstrained { ident: Ident },
     #[error("#[fold] attribute is only allowed on constrained functions")]
     FoldAttributeOnUnconstrained { ident: Ident },
-    #[error("The only supported types of numeric generics are integers, fields, and booleans")]
-    UnsupportedNumericGenericType { ident: Ident, typ: Type },
     #[error("expected type, found numeric generic parameter")]
     NumericGenericUsedForType { name: String, span: Span },
     #[error("Invalid array length construction")]
@@ -133,6 +134,8 @@ pub enum ResolverError {
     MutatingComptimeInNonComptimeContext { name: String, span: Span },
     #[error("Failed to parse `{statement}` as an expression")]
     InvalidInternedStatementInExpr { statement: String, span: Span },
+    #[error("{0}")]
+    UnsupportedNumericGenericType(#[from] UnsupportedNumericGenericType),
     #[error("Type `{typ}` is more private than item `{item}`")]
     TypeIsMorePrivateThenItem { typ: String, item: String, span: Span },
 }
@@ -443,15 +446,6 @@ impl<'a> From<&'a ResolverError> for Diagnostic {
                 diag.add_note("The `#[fold]` attribute specifies whether a constrained function should be treated as a separate circuit rather than inlined into the program entry point".to_owned());
                 diag
             }
-            ResolverError::UnsupportedNumericGenericType { ident , typ } => {
-                let name = &ident.0.contents;
-
-                Diagnostic::simple_error(
-                    format!("{name} has a type of {typ}. The only supported types of numeric generics are integers, fields, and booleans."),
-                    "Unsupported numeric generic type".to_string(),
-                    ident.0.span(),
-                )
-            }
             ResolverError::NumericGenericUsedForType { name, span } => {
                 Diagnostic::simple_error(
                     format!("expected type, found numeric generic parameter {name}"),
@@ -544,6 +538,7 @@ impl<'a> From<&'a ResolverError> for Diagnostic {
                     *span,
                 )
             },
+            ResolverError::UnsupportedNumericGenericType(err) => err.into(),
             ResolverError::TypeIsMorePrivateThenItem { typ, item, span } => {
                 Diagnostic::simple_warning(
                     format!("Type `{typ}` is more private than item `{item}`"),
diff --git a/compiler/noirc_frontend/src/hir_def/traits.rs b/compiler/noirc_frontend/src/hir_def/traits.rs
index 0572ba403a1..3859db26e39 100644
--- a/compiler/noirc_frontend/src/hir_def/traits.rs
+++ b/compiler/noirc_frontend/src/hir_def/traits.rs
@@ -3,12 +3,12 @@ use rustc_hash::FxHashMap as HashMap;
 
 use crate::ast::{Ident, NoirFunction};
 use crate::hir::type_check::generics::TraitGenerics;
+use crate::ResolvedGeneric;
 use crate::{
     graph::CrateId,
     node_interner::{FuncId, TraitId, TraitMethodId},
     Generics, Type, TypeBindings, TypeVariable,
 };
-use crate::{ResolvedGeneric, TypeVariableKind};
 use fm::FileId;
 use noirc_errors::{Location, Span};
 
@@ -168,7 +168,7 @@ impl Trait {
         });
 
         TraitConstraint {
-            typ: Type::TypeVariable(self.self_type_typevar.clone(), TypeVariableKind::Normal),
+            typ: Type::TypeVariable(self.self_type_typevar.clone()),
             trait_generics: TraitGenerics { ordered, named },
             trait_id: self.id,
             span,
diff --git a/compiler/noirc_frontend/src/hir_def/types.rs b/compiler/noirc_frontend/src/hir_def/types.rs
index c170d2cc08f..8f20fe1c685 100644
--- a/compiler/noirc_frontend/src/hir_def/types.rs
+++ b/compiler/noirc_frontend/src/hir_def/types.rs
@@ -78,7 +78,7 @@ pub enum Type {
     /// is a process that replaces each NamedGeneric in a generic function with a TypeVariable.
     /// Doing this at each call site of a generic function is how they can be called with
     /// different argument types each time.
-    TypeVariable(TypeVariable, TypeVariableKind),
+    TypeVariable(TypeVariable),
 
     /// `impl Trait` when used in a type position.
     /// These are only matched based on the TraitId. The trait name parameter is only
@@ -87,7 +87,7 @@ pub enum Type {
 
     /// NamedGenerics are the 'T' or 'U' in a user-defined generic function
     /// like `fn foo<T, U>(...) {}`. Unlike TypeVariables, they cannot be bound over.
-    NamedGeneric(TypeVariable, Rc<String>, Kind),
+    NamedGeneric(TypeVariable, Rc<String>),
 
     /// A functions with arguments, a return type and environment.
     /// the environment should be `Unit` by default,
@@ -134,7 +134,25 @@ pub enum Type {
 /// is expected (such as in an array length position) are expected to be of kind `Kind::Numeric`.
 #[derive(PartialEq, Eq, Clone, Hash, Debug, PartialOrd, Ord)]
 pub enum Kind {
+    /// Can bind to any type
+    // TODO(https://github.com/noir-lang/noir/issues/6194): evaluate need for and usage of
+    Any,
+
+    /// Can bind to any type, except Type::Constant and Type::InfixExpr
     Normal,
+
+    /// A generic integer or field type. This is a more specific kind of TypeVariable
+    /// that can only be bound to Type::Field, Type::Integer, or other polymorphic integers.
+    /// This is the type of undecorated integer literals like `46`. Typing them in this way
+    /// allows them to be polymorphic over the actual integer/field type used without requiring
+    /// type annotations on each integer literal.
+    IntegerOrField,
+
+    /// A generic integer type. This is a more specific kind of TypeVariable
+    /// that can only be bound to Type::Integer, or other polymorphic integers.
+    Integer,
+
+    /// Can bind to a Type::Constant or Type::InfixExpr of the given kind
     Numeric(Box<Type>),
 }
 
@@ -150,18 +168,34 @@ impl Kind {
         matches!(self, Self::Numeric { .. })
     }
 
-    pub(crate) fn matches_opt(&self, other: Option<Self>) -> bool {
-        other.as_ref().map_or(true, |other_kind| self.unifies(other_kind))
-    }
-
     pub(crate) fn u32() -> Self {
         Self::Numeric(Box::new(Type::Integer(Signedness::Unsigned, IntegerBitSize::ThirtyTwo)))
     }
 
+    pub(crate) fn follow_bindings(&self) -> Self {
+        match self {
+            Self::Any => Self::Any,
+            Self::Normal => Self::Normal,
+            Self::Integer => Self::Integer,
+            Self::IntegerOrField => Self::IntegerOrField,
+            Self::Numeric(typ) => Self::Numeric(Box::new(typ.follow_bindings())),
+        }
+    }
+
     /// Unifies this kind with the other. Returns true on success
     pub(crate) fn unifies(&self, other: &Kind) -> bool {
         match (self, other) {
-            (Kind::Normal, Kind::Normal) => true,
+            // Kind::Any unifies with everything
+            (Kind::Any, _) | (_, Kind::Any) => true,
+
+            // Kind::Normal unifies with Kind::Integer and Kind::IntegerOrField
+            (Kind::Normal, Kind::Integer | Kind::IntegerOrField)
+            | (Kind::Integer | Kind::IntegerOrField, Kind::Normal) => true,
+
+            // Kind::Integer unifies with Kind::IntegerOrField
+            (Kind::Integer | Kind::IntegerOrField, Kind::Integer | Kind::IntegerOrField) => true,
+
+            // Kind::Numeric unifies along its Type argument
             (Kind::Numeric(lhs), Kind::Numeric(rhs)) => {
                 let mut bindings = TypeBindings::new();
                 let unifies = lhs.try_unify(rhs, &mut bindings).is_ok();
@@ -170,7 +204,9 @@ impl Kind {
                 }
                 unifies
             }
-            _ => false,
+
+            // everything unifies with itself
+            (lhs, rhs) => lhs == rhs,
         }
     }
 
@@ -181,12 +217,27 @@ impl Kind {
             Err(UnificationError)
         }
     }
+
+    /// Returns the default type this type variable should be bound to if it is still unbound
+    /// during monomorphization.
+    pub(crate) fn default_type(&self) -> Option<Type> {
+        match self {
+            Kind::Any => None,
+            Kind::IntegerOrField => Some(Type::default_int_or_field_type()),
+            Kind::Integer => Some(Type::default_int_type()),
+            Kind::Normal => None,
+            Kind::Numeric(typ) => Some(*typ.clone()),
+        }
+    }
 }
 
 impl std::fmt::Display for Kind {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
+            Kind::Any => write!(f, "any"),
             Kind::Normal => write!(f, "normal"),
+            Kind::Integer => write!(f, "int"),
+            Kind::IntegerOrField => write!(f, "intOrField"),
             Kind::Numeric(typ) => write!(f, "numeric {}", typ),
         }
     }
@@ -209,10 +260,10 @@ pub enum QuotedType {
     CtString,
 }
 
-/// A list of TypeVariableIds to bind to a type. Storing the
+/// A list of (TypeVariableId, Kind)'s to bind to a type. Storing the
 /// TypeVariable in addition to the matching TypeVariableId allows
 /// the binding to later be undone if needed.
-pub type TypeBindings = HashMap<TypeVariableId, (TypeVariable, Type)>;
+pub type TypeBindings = HashMap<TypeVariableId, (TypeVariable, Kind, Type)>;
 
 /// Represents a struct type in the type system. Each instance of this
 /// rust struct will be shared across all Type::Struct variants that represent
@@ -236,7 +287,7 @@ pub struct StructType {
 
 /// Corresponds to generic lists such as `<T, U>` in the source program.
 /// Used mainly for resolved types which no longer need information such
-/// as names or kinds.
+/// as names or kinds
 pub type GenericTypeVars = Vec<TypeVariable>;
 
 /// Corresponds to generic lists such as `<T, U>` with additional
@@ -248,17 +299,20 @@ pub type Generics = Vec<ResolvedGeneric>;
 pub struct ResolvedGeneric {
     pub name: Rc<String>,
     pub type_var: TypeVariable,
-    pub kind: Kind,
     pub span: Span,
 }
 
 impl ResolvedGeneric {
     pub fn as_named_generic(self) -> Type {
-        Type::NamedGeneric(self.type_var, self.name, self.kind)
+        Type::NamedGeneric(self.type_var, self.name)
+    }
+
+    pub fn kind(&self) -> Kind {
+        self.type_var.kind()
     }
 
     pub(crate) fn is_numeric(&self) -> bool {
-        self.kind.is_numeric()
+        self.kind().is_numeric()
     }
 }
 
@@ -326,7 +380,12 @@ impl StructType {
                     .generics
                     .iter()
                     .zip(generic_args)
-                    .map(|(old, new)| (old.type_var.id(), (old.type_var.clone(), new.clone())))
+                    .map(|(old, new)| {
+                        (
+                            old.type_var.id(),
+                            (old.type_var.clone(), old.type_var.kind(), new.clone()),
+                        )
+                    })
                     .collect();
 
                 (typ.substitute(&substitutions), i)
@@ -342,7 +401,9 @@ impl StructType {
             .generics
             .iter()
             .zip(generic_args)
-            .map(|(old, new)| (old.type_var.id(), (old.type_var.clone(), new.clone())))
+            .map(|(old, new)| {
+                (old.type_var.id(), (old.type_var.clone(), old.type_var.kind(), new.clone()))
+            })
             .collect();
 
         vecmap(&self.fields, |(name, typ)| {
@@ -380,7 +441,7 @@ impl StructType {
     /// Instantiate this struct type, returning a Vec of the new generic args (in
     /// the same order as self.generics)
     pub fn instantiate(&self, interner: &mut NodeInterner) -> Vec<Type> {
-        vecmap(&self.generics, |_| interner.next_type_variable())
+        vecmap(&self.generics, |generic| interner.next_type_variable_with_kind(generic.kind()))
     }
 }
 
@@ -454,7 +515,9 @@ impl TypeAlias {
             .generics
             .iter()
             .zip(generic_args)
-            .map(|(old, new)| (old.type_var.id(), (old.type_var.clone(), new.clone())))
+            .map(|(old, new)| {
+                (old.type_var.id(), (old.type_var.clone(), old.type_var.kind(), new.clone()))
+            })
             .collect();
 
         self.typ.substitute(&substitutions)
@@ -527,31 +590,14 @@ pub enum BinaryTypeOperator {
     Modulo,
 }
 
-#[derive(Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord)]
-pub enum TypeVariableKind {
-    /// Can bind to any type
-    Normal,
-
-    /// A generic integer or field type. This is a more specific kind of TypeVariable
-    /// that can only be bound to Type::Field, Type::Integer, or other polymorphic integers.
-    /// This is the type of undecorated integer literals like `46`. Typing them in this way
-    /// allows them to be polymorphic over the actual integer/field type used without requiring
-    /// type annotations on each integer literal.
-    IntegerOrField,
-
-    /// A generic integer type. This is a more specific kind of TypeVariable
-    /// that can only be bound to Type::Integer, or other polymorphic integers.
-    Integer,
-}
-
 /// A TypeVariable is a mutable reference that is either
 /// bound to some type, or unbound with a given TypeVariableId.
 #[derive(PartialEq, Eq, Clone, Hash, PartialOrd, Ord)]
 pub struct TypeVariable(TypeVariableId, Shared<TypeBinding>);
 
 impl TypeVariable {
-    pub fn unbound(id: TypeVariableId) -> Self {
-        TypeVariable(id, Shared::new(TypeBinding::Unbound(id)))
+    pub fn unbound(id: TypeVariableId, type_var_kind: Kind) -> Self {
+        TypeVariable(id, Shared::new(TypeBinding::Unbound(id, type_var_kind)))
     }
 
     pub fn id(&self) -> TypeVariableId {
@@ -568,19 +614,27 @@ impl TypeVariable {
             TypeBinding::Bound(binding) => {
                 unreachable!("TypeVariable::bind, cannot bind bound var {} to {}", binding, typ)
             }
-            TypeBinding::Unbound(id) => *id,
+            TypeBinding::Unbound(id, _) => *id,
         };
 
         assert!(!typ.occurs(id), "{self:?} occurs within {typ:?}");
         *self.1.borrow_mut() = TypeBinding::Bound(typ);
     }
 
-    pub fn try_bind(&self, binding: Type, span: Span) -> Result<(), TypeCheckError> {
+    pub fn try_bind(&self, binding: Type, kind: &Kind, span: Span) -> Result<(), TypeCheckError> {
+        if !binding.kind().unifies(kind) {
+            return Err(TypeCheckError::TypeKindMismatch {
+                expected_kind: format!("{}", kind),
+                expr_kind: format!("{}", binding.kind()),
+                expr_span: span,
+            });
+        }
+
         let id = match &*self.1.borrow() {
             TypeBinding::Bound(binding) => {
                 unreachable!("Expected unbound, found bound to {binding}")
             }
-            TypeBinding::Unbound(id) => *id,
+            TypeBinding::Unbound(id, _) => *id,
         };
 
         if binding.occurs(id) {
@@ -599,18 +653,47 @@ impl TypeVariable {
     /// Unbind this type variable, setting it to Unbound(id).
     ///
     /// This is generally a logic error to use outside of monomorphization.
-    pub fn unbind(&self, id: TypeVariableId) {
-        *self.1.borrow_mut() = TypeBinding::Unbound(id);
+    pub fn unbind(&self, id: TypeVariableId, type_var_kind: Kind) {
+        *self.1.borrow_mut() = TypeBinding::Unbound(id, type_var_kind);
     }
 
     /// Forcibly bind a type variable to a new type - even if the type
     /// variable is already bound to a different type. This generally
     /// a logic error to use outside of monomorphization.
+    ///
+    /// Asserts that the given type is compatible with the given Kind
     pub fn force_bind(&self, typ: Type) {
         if !typ.occurs(self.id()) {
             *self.1.borrow_mut() = TypeBinding::Bound(typ);
         }
     }
+
+    pub fn kind(&self) -> Kind {
+        match &*self.borrow() {
+            TypeBinding::Bound(binding) => binding.kind(),
+            TypeBinding::Unbound(_, type_var_kind) => type_var_kind.clone(),
+        }
+    }
+
+    /// Check that if bound, it's an integer
+    /// and if unbound, that it's a Kind::Integer
+    pub fn is_integer(&self) -> bool {
+        match &*self.borrow() {
+            TypeBinding::Bound(binding) => matches!(binding, Type::Integer(..)),
+            TypeBinding::Unbound(_, type_var_kind) => matches!(type_var_kind, Kind::Integer),
+        }
+    }
+
+    /// Check that if bound, it's an integer or field
+    /// and if unbound, that it's a Kind::IntegerOrField
+    pub fn is_integer_or_field(&self) -> bool {
+        match &*self.borrow() {
+            TypeBinding::Bound(binding) => {
+                matches!(binding, Type::Integer(..) | Type::FieldElement)
+            }
+            TypeBinding::Unbound(_, type_var_kind) => matches!(type_var_kind, Kind::IntegerOrField),
+        }
+    }
 }
 
 /// TypeBindings are the mutable insides of a TypeVariable.
@@ -618,12 +701,12 @@ impl TypeVariable {
 #[derive(Clone, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
 pub enum TypeBinding {
     Bound(Type),
-    Unbound(TypeVariableId),
+    Unbound(TypeVariableId, Kind),
 }
 
 impl TypeBinding {
     pub fn is_unbound(&self) -> bool {
-        matches!(self, TypeBinding::Unbound(_))
+        matches!(self, TypeBinding::Unbound(_, _))
     }
 }
 
@@ -647,22 +730,18 @@ impl std::fmt::Display for Type {
                 Signedness::Signed => write!(f, "i{num_bits}"),
                 Signedness::Unsigned => write!(f, "u{num_bits}"),
             },
-            Type::TypeVariable(var, TypeVariableKind::Normal) => write!(f, "{}", var.borrow()),
-            Type::TypeVariable(binding, TypeVariableKind::Integer) => {
-                if let TypeBinding::Unbound(_) = &*binding.borrow() {
-                    write!(f, "{}", Type::default_int_type())
-                } else {
-                    write!(f, "{}", binding.borrow())
-                }
-            }
-            Type::TypeVariable(binding, TypeVariableKind::IntegerOrField) => {
-                if let TypeBinding::Unbound(_) = &*binding.borrow() {
-                    // Show a Field by default if this TypeVariableKind::IntegerOrField is unbound, since that is
-                    // what they bind to by default anyway. It is less confusing than displaying it
-                    // as a generic.
-                    write!(f, "Field")
-                } else {
-                    write!(f, "{}", binding.borrow())
+            Type::TypeVariable(var) => {
+                let binding = &var.1;
+                match &*binding.borrow() {
+                    TypeBinding::Unbound(_, type_var_kind) => match type_var_kind {
+                        Kind::Any | Kind::Normal => write!(f, "{}", var.borrow()),
+                        Kind::Integer => write!(f, "{}", Type::default_int_type()),
+                        Kind::IntegerOrField => write!(f, "Field"),
+                        Kind::Numeric(_typ) => write!(f, "_"),
+                    },
+                    TypeBinding::Bound(binding) => {
+                        write!(f, "{}", binding)
+                    }
                 }
             }
             Type::Struct(s, args) => {
@@ -695,10 +774,10 @@ impl std::fmt::Display for Type {
             }
             Type::Unit => write!(f, "()"),
             Type::Error => write!(f, "error"),
-            Type::NamedGeneric(binding, name, _) => match &*binding.borrow() {
+            Type::NamedGeneric(binding, name) => match &*binding.borrow() {
                 TypeBinding::Bound(binding) => binding.fmt(f),
-                TypeBinding::Unbound(_) if name.is_empty() => write!(f, "_"),
-                TypeBinding::Unbound(_) => write!(f, "{name}"),
+                TypeBinding::Unbound(_, _) if name.is_empty() => write!(f, "_"),
+                TypeBinding::Unbound(_, _) => write!(f, "{name}"),
             },
             Type::Constant(x, _kind) => write!(f, "{x}"),
             Type::Forall(typevars, typ) => {
@@ -759,7 +838,7 @@ impl std::fmt::Display for TypeBinding {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {
             TypeBinding::Bound(typ) => typ.fmt(f),
-            TypeBinding::Unbound(id) => id.fmt(f),
+            TypeBinding::Unbound(id, _) => id.fmt(f),
         }
     }
 }
@@ -795,23 +874,25 @@ impl Type {
         Type::Integer(Signedness::Unsigned, IntegerBitSize::ThirtyTwo)
     }
 
+    pub fn type_variable_with_kind(interner: &NodeInterner, type_var_kind: Kind) -> Type {
+        let id = interner.next_type_variable_id();
+        let var = TypeVariable::unbound(id, type_var_kind);
+        Type::TypeVariable(var)
+    }
+
     pub fn type_variable(id: TypeVariableId) -> Type {
-        let var = TypeVariable::unbound(id);
-        Type::TypeVariable(var, TypeVariableKind::Normal)
+        let var = TypeVariable::unbound(id, Kind::Normal);
+        Type::TypeVariable(var)
     }
 
-    pub fn polymorphic_integer_or_field(interner: &mut NodeInterner) -> Type {
-        let id = interner.next_type_variable_id();
-        let kind = TypeVariableKind::IntegerOrField;
-        let var = TypeVariable::unbound(id);
-        Type::TypeVariable(var, kind)
+    pub fn polymorphic_integer_or_field(interner: &NodeInterner) -> Type {
+        let type_var_kind = Kind::IntegerOrField;
+        Self::type_variable_with_kind(interner, type_var_kind)
     }
 
-    pub fn polymorphic_integer(interner: &mut NodeInterner) -> Type {
-        let id = interner.next_type_variable_id();
-        let kind = TypeVariableKind::Integer;
-        let var = TypeVariable::unbound(id);
-        Type::TypeVariable(var, kind)
+    pub fn polymorphic_integer(interner: &NodeInterner) -> Type {
+        let type_var_kind = Kind::Integer;
+        Self::type_variable_with_kind(interner, type_var_kind)
     }
 
     /// A bit of an awkward name for this function - this function returns
@@ -820,9 +901,9 @@ impl Type {
     /// they shouldn't be bound over until monomorphization.
     pub fn is_bindable(&self) -> bool {
         match self {
-            Type::TypeVariable(binding, _) => match &*binding.borrow() {
+            Type::TypeVariable(binding) => match &*binding.borrow() {
                 TypeBinding::Bound(binding) => binding.is_bindable(),
-                TypeBinding::Unbound(_) => true,
+                TypeBinding::Unbound(_, _) => true,
             },
             Type::Alias(alias, args) => alias.borrow().get_type(args).is_bindable(),
             _ => false,
@@ -849,21 +930,35 @@ impl Type {
         matches!(self.follow_bindings(), Type::Integer(Signedness::Unsigned, _))
     }
 
-    pub fn is_numeric(&self) -> bool {
+    /// While Kind::is_numeric refers to numeric _types_,
+    /// this method checks for numeric _values_
+    pub fn is_numeric_value(&self) -> bool {
+        use Kind as K;
         use Type::*;
-        use TypeVariableKind as K;
-        matches!(
-            self.follow_bindings(),
-            FieldElement | Integer(..) | Bool | TypeVariable(_, K::Integer | K::IntegerOrField)
-        )
+        match self.follow_bindings() {
+            FieldElement => true,
+            Integer(..) => true,
+            Bool => true,
+            TypeVariable(var) => match &*var.borrow() {
+                TypeBinding::Bound(typ) => typ.is_numeric_value(),
+                TypeBinding::Unbound(_, type_var_kind) => {
+                    matches!(type_var_kind, K::Integer | K::IntegerOrField)
+                }
+            },
+            _ => false,
+        }
     }
 
     pub fn find_numeric_type_vars(&self, found_names: &mut Vec<String>) {
-        // Return whether the named generic has a TypeKind::Numeric and save its name
+        // Return whether the named generic has a Kind::Numeric and save its name
         let named_generic_is_numeric = |typ: &Type, found_names: &mut Vec<String>| {
-            if let Type::NamedGeneric(_, name, Kind::Numeric { .. }) = typ {
-                found_names.push(name.to_string());
-                true
+            if let Type::NamedGeneric(var, name) = typ {
+                if var.kind().is_numeric() {
+                    found_names.push(name.to_string());
+                    true
+                } else {
+                    false
+                }
             } else {
                 false
             }
@@ -879,13 +974,13 @@ impl Type {
             | Type::Forall(_, _)
             | Type::Quoted(_) => {}
 
-            Type::TypeVariable(type_var, _) => {
+            Type::TypeVariable(type_var) => {
                 if let TypeBinding::Bound(typ) = &*type_var.borrow() {
                     named_generic_is_numeric(typ, found_names);
                 }
             }
 
-            Type::NamedGeneric(_, _, _) => {
+            Type::NamedGeneric(_, _) => {
                 named_generic_is_numeric(self, found_names);
             }
 
@@ -962,8 +1057,8 @@ impl Type {
             | Type::Error => true,
 
             Type::FmtString(_, _)
-            | Type::TypeVariable(_, _)
-            | Type::NamedGeneric(_, _, _)
+            | Type::TypeVariable(_)
+            | Type::NamedGeneric(_, _)
             | Type::Function(_, _, _, _)
             | Type::MutableReference(_)
             | Type::Forall(_, _)
@@ -1005,8 +1100,8 @@ impl Type {
             | Type::Bool
             | Type::Unit
             | Type::Constant(_, _)
-            | Type::TypeVariable(_, _)
-            | Type::NamedGeneric(_, _, _)
+            | Type::TypeVariable(_)
+            | Type::NamedGeneric(_, _)
             | Type::InfixExpr(..)
             | Type::Error => true,
 
@@ -1054,7 +1149,7 @@ impl Type {
             | Type::InfixExpr(..)
             | Type::Error => true,
 
-            Type::TypeVariable(type_var, _) | Type::NamedGeneric(type_var, _, _) => {
+            Type::TypeVariable(type_var) | Type::NamedGeneric(type_var, _) => {
                 if let TypeBinding::Bound(typ) = &*type_var.borrow() {
                     typ.is_valid_for_unconstrained_boundary()
                 } else {
@@ -1094,10 +1189,10 @@ impl Type {
     pub fn generic_count(&self) -> usize {
         match self {
             Type::Forall(generics, _) => generics.len(),
-            Type::TypeVariable(type_variable, _) | Type::NamedGeneric(type_variable, _, _) => {
+            Type::TypeVariable(type_variable) | Type::NamedGeneric(type_variable, _) => {
                 match &*type_variable.borrow() {
                     TypeBinding::Bound(binding) => binding.generic_count(),
-                    TypeBinding::Unbound(_) => 0,
+                    TypeBinding::Unbound(_, _) => 0,
                 }
             }
             _ => 0,
@@ -1105,9 +1200,10 @@ impl Type {
     }
 
     /// Takes a monomorphic type and generalizes it over each of the type variables in the
-    /// given type bindings, ignoring what each type variable is bound to in the TypeBindings.
+    /// given type bindings, ignoring what each type variable is bound to in the TypeBindings
+    /// and their Kind's
     pub(crate) fn generalize_from_substitutions(self, type_bindings: TypeBindings) -> Type {
-        let polymorphic_type_vars = vecmap(type_bindings, |(_, (type_var, _))| type_var);
+        let polymorphic_type_vars = vecmap(type_bindings, |(_, (type_var, _kind, _))| type_var);
         Type::Forall(polymorphic_type_vars, Box::new(self))
     }
 
@@ -1130,15 +1226,15 @@ impl Type {
         }
     }
 
-    pub(crate) fn kind(&self) -> Option<Kind> {
+    pub(crate) fn kind(&self) -> Kind {
         match self {
-            Type::NamedGeneric(_, _, kind) => Some(kind.clone()),
-            Type::Constant(_, kind) => Some(kind.clone()),
-            Type::TypeVariable(var, _) => match *var.borrow() {
+            Type::NamedGeneric(var, _) => var.kind(),
+            Type::Constant(_, kind) => kind.clone(),
+            Type::TypeVariable(var) => match &*var.borrow() {
                 TypeBinding::Bound(ref typ) => typ.kind(),
-                TypeBinding::Unbound(_) => None,
+                TypeBinding::Unbound(_, ref type_var_kind) => type_var_kind.clone(),
             },
-            Type::InfixExpr(lhs, _op, rhs) => Some(lhs.infix_kind(rhs)),
+            Type::InfixExpr(lhs, _op, rhs) => lhs.infix_kind(rhs),
             Type::FieldElement
             | Type::Array(..)
             | Type::Slice(..)
@@ -1155,26 +1251,18 @@ impl Type {
             | Type::MutableReference(..)
             | Type::Forall(..)
             | Type::Quoted(..)
-            | Type::Error => Some(Kind::Normal),
+            | Type::Error => Kind::Normal,
         }
     }
 
-    /// if both Kind's are equal to Some(_), return that Kind,
-    ///     otherwise return a Kind error
-    /// if both Kind's are None, default to u32
-    /// if exactly one Kind is None, return the other one
+    /// Unifies self and other kinds or fails with a Kind error
     fn infix_kind(&self, other: &Self) -> Kind {
-        match (self.kind(), other.kind()) {
-            (Some(self_kind), Some(other_kind)) => {
-                if self_kind == other_kind {
-                    self_kind
-                } else {
-                    Kind::Numeric(Box::new(Type::Error))
-                }
-            }
-            (None, None) => Kind::u32(),
-            (Some(self_kind), None) => self_kind,
-            (None, Some(other_kind)) => other_kind,
+        let self_kind = self.kind();
+        let other_kind = other.kind();
+        if self_kind.unifies(&other_kind) {
+            self_kind
+        } else {
+            Kind::Numeric(Box::new(Type::Error))
         }
     }
 
@@ -1203,9 +1291,9 @@ impl Type {
                 .expect("Cannot have variable sized strings as a parameter to main"),
             Type::FmtString(_, _)
             | Type::Unit
-            | Type::TypeVariable(_, _)
+            | Type::TypeVariable(_)
             | Type::TraitAsType(..)
-            | Type::NamedGeneric(_, _, _)
+            | Type::NamedGeneric(_, _)
             | Type::Function(_, _, _, _)
             | Type::MutableReference(_)
             | Type::Forall(_, _)
@@ -1261,71 +1349,62 @@ impl Type {
     ) -> Result<(), UnificationError> {
         let target_id = match &*var.borrow() {
             TypeBinding::Bound(_) => unreachable!(),
-            TypeBinding::Unbound(id) => *id,
+            TypeBinding::Unbound(id, _) => *id,
         };
 
+        if !self.kind().unifies(&Kind::IntegerOrField) {
+            return Err(UnificationError);
+        }
+
         let this = self.substitute(bindings).follow_bindings();
         match &this {
             Type::Integer(..) => {
-                bindings.insert(target_id, (var.clone(), this));
+                bindings.insert(target_id, (var.clone(), Kind::Integer, this));
                 Ok(())
             }
             Type::FieldElement if !only_integer => {
-                bindings.insert(target_id, (var.clone(), this));
+                bindings.insert(target_id, (var.clone(), Kind::IntegerOrField, this));
                 Ok(())
             }
-            Type::TypeVariable(self_var, TypeVariableKind::IntegerOrField) => {
+            Type::TypeVariable(self_var) => {
                 let borrow = self_var.borrow();
                 match &*borrow {
                     TypeBinding::Bound(typ) => {
                         typ.try_bind_to_polymorphic_int(var, bindings, only_integer)
                     }
                     // Avoid infinitely recursive bindings
-                    TypeBinding::Unbound(id) if *id == target_id => Ok(()),
-                    TypeBinding::Unbound(new_target_id) => {
+                    TypeBinding::Unbound(ref id, _) if *id == target_id => Ok(()),
+                    TypeBinding::Unbound(ref new_target_id, Kind::IntegerOrField) => {
+                        let type_var_kind = Kind::IntegerOrField;
                         if only_integer {
+                            let var_clone = var.clone();
+                            Kind::Integer.unify(&type_var_kind)?;
                             // Integer is more specific than IntegerOrField so we bind the type
                             // variable to Integer instead.
-                            let clone = Type::TypeVariable(var.clone(), TypeVariableKind::Integer);
-                            bindings.insert(*new_target_id, (self_var.clone(), clone));
+                            let clone = Type::TypeVariable(var_clone);
+                            bindings
+                                .insert(*new_target_id, (self_var.clone(), type_var_kind, clone));
                         } else {
-                            bindings.insert(target_id, (var.clone(), this.clone()));
+                            bindings.insert(
+                                target_id,
+                                (var.clone(), Kind::IntegerOrField, this.clone()),
+                            );
                         }
                         Ok(())
                     }
-                }
-            }
-            Type::TypeVariable(self_var, TypeVariableKind::Integer) => {
-                let borrow = self_var.borrow();
-                match &*borrow {
-                    TypeBinding::Bound(typ) => {
-                        typ.try_bind_to_polymorphic_int(var, bindings, only_integer)
-                    }
-                    // Avoid infinitely recursive bindings
-                    TypeBinding::Unbound(id) if *id == target_id => Ok(()),
-                    TypeBinding::Unbound(_) => {
-                        bindings.insert(target_id, (var.clone(), this.clone()));
+                    TypeBinding::Unbound(_new_target_id, Kind::Integer) => {
+                        Kind::Integer.unify(&Kind::Integer)?;
+                        bindings.insert(target_id, (var.clone(), Kind::Integer, this.clone()));
                         Ok(())
                     }
-                }
-            }
-            Type::TypeVariable(self_var, TypeVariableKind::Normal) => {
-                let borrow = self_var.borrow();
-                match &*borrow {
-                    TypeBinding::Bound(typ) => {
-                        typ.try_bind_to_polymorphic_int(var, bindings, only_integer)
-                    }
-                    // Avoid infinitely recursive bindings
-                    TypeBinding::Unbound(id) if *id == target_id => Ok(()),
-                    TypeBinding::Unbound(new_target_id) => {
+                    TypeBinding::Unbound(new_target_id, ref type_var_kind) => {
+                        let var_clone = var.clone();
                         // Bind to the most specific type variable kind
-                        let clone_kind = if only_integer {
-                            TypeVariableKind::Integer
-                        } else {
-                            TypeVariableKind::IntegerOrField
-                        };
-                        let clone = Type::TypeVariable(var.clone(), clone_kind);
-                        bindings.insert(*new_target_id, (self_var.clone(), clone));
+                        let clone_kind =
+                            if only_integer { Kind::Integer } else { Kind::IntegerOrField };
+                        clone_kind.unify(type_var_kind)?;
+                        let clone = Type::TypeVariable(var_clone);
+                        bindings.insert(*new_target_id, (self_var.clone(), clone_kind, clone));
                         Ok(())
                     }
                 }
@@ -1335,7 +1414,7 @@ impl Type {
     }
 
     /// Try to bind the given type variable to self. Although the given type variable
-    /// is expected to be of TypeVariableKind::Normal, this binding can still fail
+    /// is expected to be of Kind::Normal, this binding can still fail
     /// if the given type variable occurs within `self` as that would create a recursive type.
     ///
     /// If successful, the binding is placed in the
@@ -1344,18 +1423,23 @@ impl Type {
         &self,
         var: &TypeVariable,
         bindings: &mut TypeBindings,
+        kind: Kind,
     ) -> Result<(), UnificationError> {
         let target_id = match &*var.borrow() {
             TypeBinding::Bound(_) => unreachable!(),
-            TypeBinding::Unbound(id) => *id,
+            TypeBinding::Unbound(id, _) => *id,
         };
 
+        if !self.kind().unifies(&kind) {
+            return Err(UnificationError);
+        }
+
         let this = self.substitute(bindings).follow_bindings();
-        if let Some(binding) = this.get_inner_type_variable() {
+        if let Some((binding, kind)) = this.get_inner_type_variable() {
             match &*binding.borrow() {
-                TypeBinding::Bound(typ) => return typ.try_bind_to(var, bindings),
+                TypeBinding::Bound(typ) => return typ.try_bind_to(var, bindings, kind),
                 // Don't recursively bind the same id to itself
-                TypeBinding::Unbound(id) if *id == target_id => return Ok(()),
+                TypeBinding::Unbound(id, _) if *id == target_id => return Ok(()),
                 _ => (),
             }
         }
@@ -1365,14 +1449,15 @@ impl Type {
         if this.occurs(target_id) {
             Err(UnificationError)
         } else {
-            bindings.insert(target_id, (var.clone(), this.clone()));
+            bindings.insert(target_id, (var.clone(), this.kind(), this.clone()));
             Ok(())
         }
     }
 
-    fn get_inner_type_variable(&self) -> Option<Shared<TypeBinding>> {
+    fn get_inner_type_variable(&self) -> Option<(Shared<TypeBinding>, Kind)> {
         match self {
-            Type::TypeVariable(var, _) | Type::NamedGeneric(var, _, _) => Some(var.1.clone()),
+            Type::TypeVariable(var) => Some((var.1.clone(), var.kind())),
+            Type::NamedGeneric(var, _) => Some((var.1.clone(), var.kind())),
             _ => None,
         }
     }
@@ -1398,7 +1483,6 @@ impl Type {
         bindings: &mut TypeBindings,
     ) -> Result<(), UnificationError> {
         use Type::*;
-        use TypeVariableKind as Kind;
 
         let lhs = match self {
             Type::InfixExpr(..) => Cow::Owned(self.canonicalize()),
@@ -1418,27 +1502,36 @@ impl Type {
                 alias.try_unify(other, bindings)
             }
 
-            (TypeVariable(var, Kind::IntegerOrField), other)
-            | (other, TypeVariable(var, Kind::IntegerOrField)) => {
-                other.try_unify_to_type_variable(var, bindings, |bindings| {
-                    let only_integer = false;
-                    other.try_bind_to_polymorphic_int(var, bindings, only_integer)
-                })
-            }
-
-            (TypeVariable(var, Kind::Integer), other)
-            | (other, TypeVariable(var, Kind::Integer)) => {
-                other.try_unify_to_type_variable(var, bindings, |bindings| {
-                    let only_integer = true;
-                    other.try_bind_to_polymorphic_int(var, bindings, only_integer)
-                })
-            }
-
-            (TypeVariable(var, Kind::Normal), other) | (other, TypeVariable(var, Kind::Normal)) => {
-                other.try_unify_to_type_variable(var, bindings, |bindings| {
-                    other.try_bind_to(var, bindings)
-                })
-            }
+            (TypeVariable(var), other) | (other, TypeVariable(var)) => match &*var.borrow() {
+                TypeBinding::Bound(typ) => {
+                    if typ.is_numeric_value() {
+                        other.try_unify_to_type_variable(var, bindings, |bindings| {
+                            let only_integer = matches!(typ, Type::Integer(..));
+                            other.try_bind_to_polymorphic_int(var, bindings, only_integer)
+                        })
+                    } else {
+                        other.try_unify_to_type_variable(var, bindings, |bindings| {
+                            other.try_bind_to(var, bindings, typ.kind())
+                        })
+                    }
+                }
+                TypeBinding::Unbound(_id, Kind::IntegerOrField) => other
+                    .try_unify_to_type_variable(var, bindings, |bindings| {
+                        let only_integer = false;
+                        other.try_bind_to_polymorphic_int(var, bindings, only_integer)
+                    }),
+                TypeBinding::Unbound(_id, Kind::Integer) => {
+                    other.try_unify_to_type_variable(var, bindings, |bindings| {
+                        let only_integer = true;
+                        other.try_bind_to_polymorphic_int(var, bindings, only_integer)
+                    })
+                }
+                TypeBinding::Unbound(_id, type_var_kind) => {
+                    other.try_unify_to_type_variable(var, bindings, |bindings| {
+                        other.try_bind_to(var, bindings, type_var_kind.clone())
+                    })
+                }
+            },
 
             (Array(len_a, elem_a), Array(len_b, elem_b)) => {
                 len_a.try_unify(len_b, bindings)?;
@@ -1479,7 +1572,7 @@ impl Type {
                 }
             }
 
-            (NamedGeneric(binding, _, _), other) | (other, NamedGeneric(binding, _, _))
+            (NamedGeneric(binding, _), other) | (other, NamedGeneric(binding, _))
                 if !binding.borrow().is_unbound() =>
             {
                 if let TypeBinding::Bound(link) = &*binding.borrow() {
@@ -1489,13 +1582,13 @@ impl Type {
                 }
             }
 
-            (NamedGeneric(binding_a, name_a, kind_a), NamedGeneric(binding_b, name_b, kind_b)) => {
+            (NamedGeneric(binding_a, name_a), NamedGeneric(binding_b, name_b)) => {
                 // Bound NamedGenerics are caught by the check above
                 assert!(binding_a.borrow().is_unbound());
                 assert!(binding_b.borrow().is_unbound());
 
                 if name_a == name_b {
-                    kind_a.unify(kind_b)
+                    binding_a.kind().unify(&binding_b.kind())
                 } else {
                     Err(UnificationError)
                 }
@@ -1541,8 +1634,9 @@ impl Type {
             }
 
             (Constant(value, kind), other) | (other, Constant(value, kind)) => {
+                // TODO(https://github.com/noir-lang/noir/pull/6137): replace evaluate_to_u32
                 if let Some(other_value) = other.evaluate_to_u32() {
-                    if *value == other_value && kind.matches_opt(other.kind()) {
+                    if *value == other_value && kind.unifies(&other.kind()) {
                         Ok(())
                     } else {
                         Err(UnificationError)
@@ -1583,18 +1677,23 @@ impl Type {
         bindings: &mut TypeBindings,
 
         // Bind the type variable to a type. This is factored out since depending on the
-        // TypeVariableKind, there are different methods to check whether the variable can
+        // Kind, there are different methods to check whether the variable can
         // bind to the given type or not.
         bind_variable: impl FnOnce(&mut TypeBindings) -> Result<(), UnificationError>,
     ) -> Result<(), UnificationError> {
         match &*type_variable.borrow() {
             // If it is already bound, unify against what it is bound to
             TypeBinding::Bound(link) => link.try_unify(self, bindings),
-            TypeBinding::Unbound(id) => {
+            TypeBinding::Unbound(id, _) => {
                 // We may have already "bound" this type variable in this call to
                 // try_unify, so check those bindings as well.
                 match bindings.get(id) {
-                    Some((_, binding)) => binding.clone().try_unify(self, bindings),
+                    Some((_, kind, binding)) => {
+                        if !kind.unifies(&binding.kind()) {
+                            return Err(UnificationError);
+                        }
+                        binding.clone().try_unify(self, bindings)
+                    }
 
                     // Otherwise, bind it
                     None => bind_variable(bindings),
@@ -1697,7 +1796,7 @@ impl Type {
     /// Apply the given type bindings, making them permanently visible for each
     /// clone of each type variable bound.
     pub fn apply_type_bindings(bindings: TypeBindings) {
-        for (type_variable, binding) in bindings.values() {
+        for (type_variable, _kind, binding) in bindings.values() {
             type_variable.bind(binding.clone());
         }
     }
@@ -1705,7 +1804,7 @@ impl Type {
     /// If this type is a Type::Constant (used in array lengths), or is bound
     /// to a Type::Constant, return the constant as a u32.
     pub fn evaluate_to_u32(&self) -> Option<u32> {
-        if let Some(binding) = self.get_inner_type_variable() {
+        if let Some((binding, _kind)) = self.get_inner_type_variable() {
             if let TypeBinding::Bound(binding) = &*binding.borrow() {
                 return binding.evaluate_to_u32();
             }
@@ -1713,11 +1812,11 @@ impl Type {
 
         match self.canonicalize() {
             Type::Array(len, _elem) => len.evaluate_to_u32(),
-            Type::Constant(x, _) => Some(x),
+            Type::Constant(x, _kind) => Some(x),
             Type::InfixExpr(lhs, op, rhs) => {
-                let lhs = lhs.evaluate_to_u32()?;
-                let rhs = rhs.evaluate_to_u32()?;
-                op.function(lhs, rhs)
+                let lhs_u32 = lhs.evaluate_to_u32()?;
+                let rhs_u32 = rhs.evaluate_to_u32()?;
+                op.function(lhs_u32, rhs_u32, &lhs.infix_kind(&rhs))
             }
             _ => None,
         }
@@ -1771,9 +1870,9 @@ impl Type {
         match self {
             Type::Forall(typevars, typ) => {
                 for var in typevars {
-                    bindings
-                        .entry(var.id())
-                        .or_insert_with(|| (var.clone(), interner.next_type_variable()));
+                    bindings.entry(var.id()).or_insert_with(|| {
+                        (var.clone(), var.kind(), interner.next_type_variable_with_kind(var.kind()))
+                    });
                 }
 
                 let instantiated = typ.force_substitute(&bindings);
@@ -1792,8 +1891,8 @@ impl Type {
                 let replacements = typevars
                     .iter()
                     .map(|var| {
-                        let new = interner.next_type_variable();
-                        (var.id(), (var.clone(), new))
+                        let new = interner.next_type_variable_with_kind(var.kind());
+                        (var.id(), (var.clone(), var.kind(), new))
                     })
                     .collect();
 
@@ -1827,7 +1926,7 @@ impl Type {
                 let replacements = typevars
                     .iter()
                     .zip(bindings)
-                    .map(|(var, binding)| (var.id(), (var.clone(), binding)))
+                    .map(|(var, binding)| (var.id(), (var.clone(), var.kind(), binding)))
                     .collect();
 
                 let instantiated = typ.substitute(&replacements);
@@ -1839,9 +1938,7 @@ impl Type {
 
     fn type_variable_id(&self) -> Option<TypeVariableId> {
         match self {
-            Type::TypeVariable(variable, _) | Type::NamedGeneric(variable, _, _) => {
-                Some(variable.0)
-            }
+            Type::TypeVariable(variable) | Type::NamedGeneric(variable, _) => Some(variable.0),
             _ => None,
         }
     }
@@ -1894,15 +1991,24 @@ impl Type {
             // type variables that have already been bound over.
             // This is needed for monomorphizing trait impl methods.
             match type_bindings.get(&binding.0) {
-                Some((_, replacement)) if substitute_bound_typevars => {
+                Some((_, _kind, replacement)) if substitute_bound_typevars => {
                     recur_on_binding(binding.0, replacement)
                 }
                 _ => match &*binding.borrow() {
                     TypeBinding::Bound(binding) => {
                         binding.substitute_helper(type_bindings, substitute_bound_typevars)
                     }
-                    TypeBinding::Unbound(id) => match type_bindings.get(id) {
-                        Some((_, replacement)) => recur_on_binding(binding.0, replacement),
+                    TypeBinding::Unbound(id, _) => match type_bindings.get(id) {
+                        Some((_, kind, replacement)) => {
+                            assert!(
+                                kind.unifies(&replacement.kind()),
+                                "while substituting (unbound): expected kind of unbound TypeVariable ({:?}) to match the kind of its binding ({:?})",
+                                kind,
+                                replacement.kind()
+                            );
+
+                            recur_on_binding(binding.0, replacement)
+                        }
                         None => self.clone(),
                     },
                 },
@@ -1928,7 +2034,7 @@ impl Type {
                 let fields = fields.substitute_helper(type_bindings, substitute_bound_typevars);
                 Type::FmtString(Box::new(size), Box::new(fields))
             }
-            Type::NamedGeneric(binding, _, _) | Type::TypeVariable(binding, _) => {
+            Type::NamedGeneric(binding, _) | Type::TypeVariable(binding) => {
                 substitute_binding(binding)
             }
             // Do not substitute_helper fields, it can lead to infinite recursion
@@ -2017,12 +2123,12 @@ impl Type {
                     || args.named.iter().any(|arg| arg.typ.occurs(target_id))
             }
             Type::Tuple(fields) => fields.iter().any(|field| field.occurs(target_id)),
-            Type::NamedGeneric(type_var, _, _) | Type::TypeVariable(type_var, _) => {
+            Type::NamedGeneric(type_var, _) | Type::TypeVariable(type_var) => {
                 match &*type_var.borrow() {
                     TypeBinding::Bound(binding) => {
                         type_var.id() == target_id || binding.occurs(target_id)
                     }
-                    TypeBinding::Unbound(id) => *id == target_id,
+                    TypeBinding::Unbound(id, _) => *id == target_id,
                 }
             }
             Type::Forall(typevars, typ) => {
@@ -2075,7 +2181,7 @@ impl Type {
                 def.borrow().get_type(args).follow_bindings()
             }
             Tuple(args) => Tuple(vecmap(args, |arg| arg.follow_bindings())),
-            TypeVariable(var, _) | NamedGeneric(var, _, _) => {
+            TypeVariable(var) | NamedGeneric(var, _) => {
                 if let TypeBinding::Bound(typ) = &*var.borrow() {
                     return typ.follow_bindings();
                 }
@@ -2114,7 +2220,7 @@ impl Type {
     }
 
     pub fn from_generics(generics: &GenericTypeVars) -> Vec<Type> {
-        vecmap(generics, |var| Type::TypeVariable(var.clone(), TypeVariableKind::Normal))
+        vecmap(generics, |var| Type::TypeVariable(var.clone()))
     }
 
     /// Replace any `Type::NamedGeneric` in this type with a `Type::TypeVariable`
@@ -2156,12 +2262,11 @@ impl Type {
                 typ.replace_named_generics_with_type_variables();
                 *self = typ;
             }
-            Type::TypeVariable(var, _) => {
+            Type::TypeVariable(var) => {
                 let var = var.borrow();
                 if let TypeBinding::Bound(binding) = &*var {
-                    let mut binding = binding.clone();
+                    let binding = binding.clone();
                     drop(var);
-                    binding.replace_named_generics_with_type_variables();
                     *self = binding;
                 }
             }
@@ -2173,7 +2278,7 @@ impl Type {
                     generic.typ.replace_named_generics_with_type_variables();
                 }
             }
-            Type::NamedGeneric(var, _, _) => {
+            Type::NamedGeneric(var, _) => {
                 let type_binding = var.borrow();
                 if let TypeBinding::Bound(binding) = &*type_binding {
                     let mut binding = binding.clone();
@@ -2182,7 +2287,7 @@ impl Type {
                     *self = binding;
                 } else {
                     drop(type_binding);
-                    *self = Type::TypeVariable(var.clone(), TypeVariableKind::Normal);
+                    *self = Type::TypeVariable(var.clone());
                 }
             }
             Type::Function(args, ret, env, _unconstrained) => {
@@ -2244,7 +2349,9 @@ fn convert_array_expression_to_slice(
 
 impl BinaryTypeOperator {
     /// Perform the actual rust numeric operation associated with this operator
-    pub fn function(self, a: u32, b: u32) -> Option<u32> {
+    // TODO(https://github.com/noir-lang/noir/pull/6137): the Kind is included
+    // since it'll be needed for size checks
+    pub fn function(self, a: u32, b: u32, _kind: &Kind) -> Option<u32> {
         match self {
             BinaryTypeOperator::Addition => a.checked_add(b),
             BinaryTypeOperator::Subtraction => a.checked_sub(b),
@@ -2270,18 +2377,6 @@ impl BinaryTypeOperator {
     }
 }
 
-impl TypeVariableKind {
-    /// Returns the default type this type variable should be bound to if it is still unbound
-    /// during monomorphization.
-    pub(crate) fn default_type(&self) -> Option<Type> {
-        match self {
-            TypeVariableKind::IntegerOrField => Some(Type::default_int_or_field_type()),
-            TypeVariableKind::Integer => Some(Type::default_int_type()),
-            TypeVariableKind::Normal => None,
-        }
-    }
-}
-
 impl From<Type> for PrintableType {
     fn from(value: Type) -> Self {
         Self::from(&value)
@@ -2309,16 +2404,15 @@ impl From<&Type> for PrintableType {
                 }
                 Signedness::Signed => PrintableType::SignedInteger { width: (*bit_width).into() },
             },
-            Type::TypeVariable(binding, TypeVariableKind::Integer) => match &*binding.borrow() {
+            Type::TypeVariable(binding) => match &*binding.borrow() {
                 TypeBinding::Bound(typ) => typ.into(),
-                TypeBinding::Unbound(_) => Type::default_int_type().into(),
-            },
-            Type::TypeVariable(binding, TypeVariableKind::IntegerOrField) => {
-                match &*binding.borrow() {
-                    TypeBinding::Bound(typ) => typ.into(),
-                    TypeBinding::Unbound(_) => Type::default_int_or_field_type().into(),
+                TypeBinding::Unbound(_, Kind::Integer) => Type::default_int_type().into(),
+                TypeBinding::Unbound(_, Kind::IntegerOrField) => {
+                    Type::default_int_or_field_type().into()
                 }
-            }
+                TypeBinding::Unbound(_, Kind::Numeric(typ)) => (*typ.clone()).into(),
+                TypeBinding::Unbound(_, Kind::Any | Kind::Normal) => unreachable!(),
+            },
             Type::Bool => PrintableType::Boolean,
             Type::String(size) => {
                 let size = size.evaluate_to_u32().expect("Cannot print variable sized strings");
@@ -2337,7 +2431,6 @@ impl From<&Type> for PrintableType {
             Type::Alias(alias, args) => alias.borrow().get_type(args).into(),
             Type::TraitAsType(..) => unreachable!(),
             Type::Tuple(types) => PrintableType::Tuple { types: vecmap(types, |typ| typ.into()) },
-            Type::TypeVariable(_, _) => unreachable!(),
             Type::NamedGeneric(..) => unreachable!(),
             Type::Forall(..) => unreachable!(),
             Type::Function(arguments, return_type, env, unconstrained) => PrintableType::Function {
@@ -2371,12 +2464,18 @@ impl std::fmt::Debug for Type {
                 Signedness::Signed => write!(f, "i{num_bits}"),
                 Signedness::Unsigned => write!(f, "u{num_bits}"),
             },
-            Type::TypeVariable(var, TypeVariableKind::Normal) => write!(f, "{:?}", var),
-            Type::TypeVariable(binding, TypeVariableKind::IntegerOrField) => {
-                write!(f, "IntOrField{:?}", binding)
-            }
-            Type::TypeVariable(binding, TypeVariableKind::Integer) => {
-                write!(f, "Int{:?}", binding)
+            Type::TypeVariable(var) => {
+                let binding = &var.1;
+                if let TypeBinding::Unbound(_, type_var_kind) = &*binding.borrow() {
+                    match type_var_kind {
+                        Kind::Any | Kind::Normal => write!(f, "{:?}", var),
+                        Kind::IntegerOrField => write!(f, "IntOrField{:?}", binding),
+                        Kind::Integer => write!(f, "Int{:?}", binding),
+                        Kind::Numeric(typ) => write!(f, "Numeric({:?}: {:?})", binding, typ),
+                    }
+                } else {
+                    write!(f, "{}", binding.borrow())
+                }
             }
             Type::Struct(s, args) => {
                 let args = vecmap(args, |arg| format!("{:?}", arg));
@@ -2406,8 +2505,8 @@ impl std::fmt::Debug for Type {
             }
             Type::Unit => write!(f, "()"),
             Type::Error => write!(f, "error"),
-            Type::NamedGeneric(binding, name, kind) => match kind {
-                Kind::Normal => {
+            Type::NamedGeneric(binding, name) => match binding.kind() {
+                Kind::Any | Kind::Normal | Kind::Integer | Kind::IntegerOrField => {
                     write!(f, "{}{:?}", name, binding)
                 }
                 Kind::Numeric(typ) => {
@@ -2467,7 +2566,8 @@ impl std::fmt::Debug for StructType {
 
 impl std::hash::Hash for Type {
     fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
-        if let Some(variable) = self.get_inner_type_variable() {
+        if let Some((variable, kind)) = self.get_inner_type_variable() {
+            kind.hash(state);
             if let TypeBinding::Bound(typ) = &*variable.borrow() {
                 typ.hash(state);
                 return;
@@ -2503,7 +2603,7 @@ impl std::hash::Hash for Type {
                 alias.hash(state);
                 args.hash(state);
             }
-            Type::TypeVariable(var, _) | Type::NamedGeneric(var, ..) => var.hash(state),
+            Type::TypeVariable(var) | Type::NamedGeneric(var, ..) => var.hash(state),
             Type::TraitAsType(trait_id, _, args) => {
                 trait_id.hash(state);
                 args.hash(state);
@@ -2532,13 +2632,19 @@ impl std::hash::Hash for Type {
 
 impl PartialEq for Type {
     fn eq(&self, other: &Self) -> bool {
-        if let Some(variable) = self.get_inner_type_variable() {
+        if let Some((variable, kind)) = self.get_inner_type_variable() {
+            if kind != other.kind() {
+                return false;
+            }
             if let TypeBinding::Bound(typ) = &*variable.borrow() {
                 return typ == other;
             }
         }
 
-        if let Some(variable) = other.get_inner_type_variable() {
+        if let Some((variable, other_kind)) = other.get_inner_type_variable() {
+            if self.kind() != other_kind {
+                return false;
+            }
             if let TypeBinding::Bound(typ) = &*variable.borrow() {
                 return self == typ;
             }
@@ -2592,8 +2698,8 @@ impl PartialEq for Type {
             // still want them to be equal for canonicalization checks in arithmetic generics.
             // Without this we'd fail the `serialize` test.
             (
-                NamedGeneric(lhs_var, _, _) | TypeVariable(lhs_var, _),
-                NamedGeneric(rhs_var, _, _) | TypeVariable(rhs_var, _),
+                NamedGeneric(lhs_var, _) | TypeVariable(lhs_var),
+                NamedGeneric(rhs_var, _) | TypeVariable(rhs_var),
             ) => lhs_var.id() == rhs_var.id(),
             _ => false,
         }
diff --git a/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs b/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
index 54b4c27a1f3..af94ef27535 100644
--- a/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
+++ b/compiler/noirc_frontend/src/hir_def/types/arithmetic.rs
@@ -20,8 +20,9 @@ impl Type {
                 if let (Some(lhs_u32), Some(rhs_u32)) =
                     (lhs.evaluate_to_u32(), rhs.evaluate_to_u32())
                 {
-                    if let Some(result) = op.function(lhs_u32, rhs_u32) {
-                        return Type::Constant(result, lhs.infix_kind(&rhs));
+                    let kind = lhs.infix_kind(&rhs);
+                    if let Some(result) = op.function(lhs_u32, rhs_u32, &kind) {
+                        return Type::Constant(result, kind);
                     }
                 }
 
@@ -68,7 +69,7 @@ impl Type {
                     queue.push(*rhs);
                 }
                 Type::Constant(new_constant, new_constant_kind) => {
-                    if let Some(result) = op.function(constant, new_constant) {
+                    if let Some(result) = op.function(constant, new_constant, &new_constant_kind) {
                         constant = result;
                     } else {
                         let constant = Type::Constant(new_constant, new_constant_kind);
@@ -205,7 +206,7 @@ impl Type {
                 if l_op == Subtraction {
                     op = op.inverse()?;
                 }
-                let result = op.function(l_const, r_const)?;
+                let result = op.function(l_const, r_const, &lhs.infix_kind(rhs))?;
                 let constant = Type::Constant(result, lhs.infix_kind(rhs));
                 Some(Type::InfixExpr(l_type, l_op, Box::new(constant)))
             }
@@ -218,7 +219,7 @@ impl Type {
                 if op == Division && (r_const == 0 || l_const % r_const != 0) {
                     None
                 } else {
-                    let result = op.function(l_const, r_const)?;
+                    let result = op.function(l_const, r_const, &lhs.infix_kind(rhs))?;
                     let constant = Box::new(Type::Constant(result, lhs.infix_kind(rhs)));
                     Some(Type::InfixExpr(l_type, l_op, constant))
                 }
diff --git a/compiler/noirc_frontend/src/monomorphization/mod.rs b/compiler/noirc_frontend/src/monomorphization/mod.rs
index fea15b26c5b..63ef807d898 100644
--- a/compiler/noirc_frontend/src/monomorphization/mod.rs
+++ b/compiler/noirc_frontend/src/monomorphization/mod.rs
@@ -21,7 +21,7 @@ use crate::{
         types,
     },
     node_interner::{self, DefinitionKind, NodeInterner, StmtId, TraitImplKind, TraitMethodId},
-    Type, TypeBinding, TypeBindings,
+    Kind, Type, TypeBinding, TypeBindings,
 };
 use acvm::{acir::AcirField, FieldElement};
 use iter_extended::{btree_map, try_vecmap, vecmap};
@@ -857,7 +857,14 @@ impl<'interner> Monomorphizer<'interner> {
         // Ensure all instantiation bindings are bound.
         // This ensures even unused type variables like `fn foo<T>() {}` have concrete types
         if let Some(bindings) = self.interner.try_get_instantiation_bindings(expr_id) {
-            for (_, binding) in bindings.values() {
+            for (_, kind, binding) in bindings.values() {
+                match kind {
+                    Kind::Any => (),
+                    Kind::Normal => (),
+                    Kind::Integer => (),
+                    Kind::IntegerOrField => (),
+                    Kind::Numeric(typ) => Self::check_type(typ, ident.location)?,
+                }
                 Self::check_type(binding, ident.location)?;
             }
         }
@@ -916,20 +923,31 @@ impl<'interner> Monomorphizer<'interner> {
                     ast::Expression::Ident(ident)
                 }
             },
-            DefinitionKind::NumericGeneric(type_variable) => {
+            DefinitionKind::NumericGeneric(type_variable, numeric_typ) => {
                 let value = match &*type_variable.borrow() {
-                    TypeBinding::Unbound(_) => {
+                    TypeBinding::Unbound(_, _) => {
                         unreachable!("Unbound type variable used in expression")
                     }
                     TypeBinding::Bound(binding) => binding.evaluate_to_u32().unwrap_or_else(|| {
                         panic!("Non-numeric type variable used in expression expecting a value")
                     }),
                 };
-
-                let value = FieldElement::from(value as u128);
                 let location = self.interner.id_location(expr_id);
+
+                if !Kind::Numeric(numeric_typ.clone())
+                    .unifies(&Kind::Numeric(Box::new(typ.clone())))
+                {
+                    let message = "ICE: Generic's kind does not match expected type";
+                    return Err(MonomorphizationError::InternalError { location, message });
+                }
+
                 let typ = Self::convert_type(&typ, ident.location)?;
-                ast::Expression::Literal(ast::Literal::Integer(value, false, typ, location))
+                ast::Expression::Literal(ast::Literal::Integer(
+                    (value as u128).into(),
+                    false,
+                    typ,
+                    location,
+                ))
             }
         };
 
@@ -967,8 +985,8 @@ impl<'interner> Monomorphizer<'interner> {
             HirType::TraitAsType(..) => {
                 unreachable!("All TraitAsType should be replaced before calling convert_type");
             }
-            HirType::NamedGeneric(binding, _, _) => {
-                if let TypeBinding::Bound(binding) = &*binding.borrow() {
+            HirType::NamedGeneric(binding, _) => {
+                if let TypeBinding::Bound(ref binding) = &*binding.borrow() {
                     return Self::convert_type(binding, location);
                 }
 
@@ -979,15 +997,18 @@ impl<'interner> Monomorphizer<'interner> {
                 ast::Type::Field
             }
 
-            HirType::TypeVariable(binding, kind) => {
-                if let TypeBinding::Bound(binding) = &*binding.borrow() {
-                    return Self::convert_type(binding, location);
-                }
+            HirType::TypeVariable(ref binding) => {
+                let type_var_kind = match &*binding.borrow() {
+                    TypeBinding::Bound(ref binding) => {
+                        return Self::convert_type(binding, location);
+                    }
+                    TypeBinding::Unbound(_, ref type_var_kind) => type_var_kind.clone(),
+                };
 
                 // Default any remaining unbound type variables.
                 // This should only happen if the variable in question is unused
                 // and within a larger generic type.
-                let default = match kind.default_type() {
+                let default = match type_var_kind.default_type() {
                     Some(typ) => typ,
                     None => return Err(MonomorphizationError::NoDefaultType { location }),
                 };
@@ -1085,23 +1106,26 @@ impl<'interner> Monomorphizer<'interner> {
             HirType::FmtString(_size, fields) => Self::check_type(fields.as_ref(), location),
             HirType::Array(_length, element) => Self::check_type(element.as_ref(), location),
             HirType::Slice(element) => Self::check_type(element.as_ref(), location),
-            HirType::NamedGeneric(binding, _, _) => {
-                if let TypeBinding::Bound(binding) = &*binding.borrow() {
+            HirType::NamedGeneric(binding, _) => {
+                if let TypeBinding::Bound(ref binding) = &*binding.borrow() {
                     return Self::check_type(binding, location);
                 }
 
                 Ok(())
             }
 
-            HirType::TypeVariable(binding, kind) => {
-                if let TypeBinding::Bound(binding) = &*binding.borrow() {
-                    return Self::check_type(binding, location);
-                }
+            HirType::TypeVariable(ref binding) => {
+                let type_var_kind = match &*binding.borrow() {
+                    TypeBinding::Bound(binding) => {
+                        return Self::check_type(binding, location);
+                    }
+                    TypeBinding::Unbound(_, ref type_var_kind) => type_var_kind.clone(),
+                };
 
                 // Default any remaining unbound type variables.
                 // This should only happen if the variable in question is unused
                 // and within a larger generic type.
-                let default = match kind.default_type() {
+                let default = match type_var_kind.default_type() {
                     Some(typ) => typ,
                     None => return Err(MonomorphizationError::NoDefaultType { location }),
                 };
@@ -1441,9 +1465,9 @@ impl<'interner> Monomorphizer<'interner> {
     fn follow_bindings(&self, bindings: &TypeBindings) -> TypeBindings {
         bindings
             .iter()
-            .map(|(id, (var, binding))| {
+            .map(|(id, (var, kind, binding))| {
                 let binding2 = binding.follow_bindings();
-                (*id, (var.clone(), binding2))
+                (*id, (var.clone(), kind.clone(), binding2))
             })
             .collect()
     }
@@ -1910,14 +1934,14 @@ fn unwrap_struct_type(
 }
 
 pub fn perform_instantiation_bindings(bindings: &TypeBindings) {
-    for (var, binding) in bindings.values() {
+    for (var, _kind, binding) in bindings.values() {
         var.force_bind(binding.clone());
     }
 }
 
 pub fn undo_instantiation_bindings(bindings: TypeBindings) {
-    for (id, (var, _)) in bindings {
-        var.unbind(id);
+    for (id, (var, kind, _)) in bindings {
+        var.unbind(id, kind);
     }
 }
 
@@ -1944,7 +1968,7 @@ pub fn perform_impl_bindings(
             interner.function_meta(&impl_method).typ.unwrap_forall().1.clone();
 
         // Make each NamedGeneric in this type bindable by replacing it with a TypeVariable
-        // with the same internal id and binding.
+        // with the same internal id, binding.
         trait_method_type.replace_named_generics_with_type_variables();
         impl_method_type.replace_named_generics_with_type_variables();
 
diff --git a/compiler/noirc_frontend/src/node_interner.rs b/compiler/noirc_frontend/src/node_interner.rs
index 295678c1412..6a7096c10c2 100644
--- a/compiler/noirc_frontend/src/node_interner.rs
+++ b/compiler/noirc_frontend/src/node_interner.rs
@@ -34,7 +34,7 @@ use crate::hir_def::expr::HirIdent;
 use crate::hir_def::stmt::HirLetStatement;
 use crate::hir_def::traits::TraitImpl;
 use crate::hir_def::traits::{Trait, TraitConstraint};
-use crate::hir_def::types::{StructType, Type};
+use crate::hir_def::types::{Kind, StructType, Type};
 use crate::hir_def::{
     expr::HirExpression,
     function::{FuncMeta, HirFunction},
@@ -44,7 +44,7 @@ use crate::locations::LocationIndices;
 use crate::token::{Attributes, SecondaryAttribute};
 use crate::GenericTypeVars;
 use crate::Generics;
-use crate::{Shared, TypeAlias, TypeBindings, TypeVariable, TypeVariableId, TypeVariableKind};
+use crate::{Shared, TypeAlias, TypeBindings, TypeVariable, TypeVariableId};
 
 /// An arbitrary number to limit the recursion depth when searching for trait impls.
 /// This is needed to stop recursing for cases such as `impl<T> Foo for T where T: Eq`
@@ -581,7 +581,7 @@ pub enum DefinitionKind {
 
     /// Generic types in functions (T, U in `fn foo<T, U>(...)` are declared as variables
     /// in scope in case they resolve to numeric generics later.
-    NumericGeneric(TypeVariable),
+    NumericGeneric(TypeVariable, Box<Type>),
 }
 
 impl DefinitionKind {
@@ -596,7 +596,7 @@ impl DefinitionKind {
             DefinitionKind::Function(_) => None,
             DefinitionKind::Global(_) => None,
             DefinitionKind::Local(id) => *id,
-            DefinitionKind::NumericGeneric(_) => None,
+            DefinitionKind::NumericGeneric(_, _) => None,
         }
     }
 }
@@ -728,7 +728,7 @@ impl NodeInterner {
             crate_id: unresolved_trait.crate_id,
             location: Location::new(unresolved_trait.trait_def.span, unresolved_trait.file_id),
             generics,
-            self_type_typevar: TypeVariable::unbound(self.next_type_variable_id()),
+            self_type_typevar: TypeVariable::unbound(self.next_type_variable_id(), Kind::Normal),
             methods: Vec::new(),
             method_ids: unresolved_trait.method_ids.clone(),
             associated_types,
@@ -1331,6 +1331,10 @@ impl NodeInterner {
         Type::type_variable(self.next_type_variable_id())
     }
 
+    pub fn next_type_variable_with_kind(&self, kind: Kind) -> Type {
+        Type::type_variable_with_kind(self, kind)
+    }
+
     pub fn store_instantiation_bindings(
         &mut self,
         expr_id: ExprId,
@@ -1732,7 +1736,16 @@ impl NodeInterner {
         // Replace each generic with a fresh type variable
         let substitutions = impl_generics
             .into_iter()
-            .map(|typevar| (typevar.id(), (typevar, self.next_type_variable())))
+            .map(|typevar| {
+                let typevar_kind = typevar.kind();
+                let typevar_id = typevar.id();
+                let substitution = (
+                    typevar,
+                    typevar_kind.clone(),
+                    self.next_type_variable_with_kind(typevar_kind),
+                );
+                (typevar_id, substitution)
+            })
             .collect();
 
         let instantiated_object_type = object_type.substitute(&substitutions);
@@ -2223,11 +2236,17 @@ impl NodeInterner {
         let trait_generics = the_trait.generics.clone();
 
         let self_type_var = the_trait.self_type_typevar.clone();
-        bindings.insert(self_type_var.id(), (self_type_var, impl_self_type));
+        bindings.insert(
+            self_type_var.id(),
+            (self_type_var.clone(), self_type_var.kind(), impl_self_type),
+        );
 
         for (trait_generic, trait_impl_generic) in trait_generics.iter().zip(trait_impl_generics) {
             let type_var = trait_generic.type_var.clone();
-            bindings.insert(type_var.id(), (type_var, trait_impl_generic.clone()));
+            bindings.insert(
+                type_var.id(),
+                (type_var, trait_generic.kind(), trait_impl_generic.clone()),
+            );
         }
 
         // Now that the normal bindings are added, we still need to bind the associated types
@@ -2236,7 +2255,10 @@ impl NodeInterner {
 
         for (trait_type, impl_type) in trait_associated_types.iter().zip(impl_associated_types) {
             let type_variable = trait_type.type_var.clone();
-            bindings.insert(type_variable.id(), (type_variable, impl_type.typ.clone()));
+            bindings.insert(
+                type_variable.id(),
+                (type_variable, trait_type.kind(), impl_type.typ.clone()),
+            );
         }
 
         bindings
@@ -2357,22 +2379,26 @@ fn get_type_method_key(typ: &Type) -> Option<TypeMethodKey> {
         Type::Array(_, _) => Some(Array),
         Type::Slice(_) => Some(Slice),
         Type::Integer(_, _) => Some(FieldOrInt),
-        Type::TypeVariable(_, TypeVariableKind::IntegerOrField) => Some(FieldOrInt),
-        Type::TypeVariable(_, TypeVariableKind::Integer) => Some(FieldOrInt),
+        Type::TypeVariable(var) => {
+            if var.is_integer() || var.is_integer_or_field() {
+                Some(FieldOrInt)
+            } else {
+                None
+            }
+        }
         Type::Bool => Some(Bool),
         Type::String(_) => Some(String),
         Type::FmtString(_, _) => Some(FmtString),
         Type::Unit => Some(Unit),
         Type::Tuple(_) => Some(Tuple),
         Type::Function(_, _, _, _) => Some(Function),
-        Type::NamedGeneric(_, _, _) => Some(Generic),
+        Type::NamedGeneric(_, _) => Some(Generic),
         Type::Quoted(quoted) => Some(Quoted(*quoted)),
         Type::MutableReference(element) => get_type_method_key(element),
         Type::Alias(alias, _) => get_type_method_key(&alias.borrow().typ),
 
         // We do not support adding methods to these types
-        Type::TypeVariable(_, _)
-        | Type::Forall(_, _)
+        Type::Forall(_, _)
         | Type::Constant(..)
         | Type::Error
         | Type::Struct(_, _)
diff --git a/compiler/noirc_frontend/src/tests.rs b/compiler/noirc_frontend/src/tests.rs
index 63013036ca9..f7ef9955550 100644
--- a/compiler/noirc_frontend/src/tests.rs
+++ b/compiler/noirc_frontend/src/tests.rs
@@ -1586,9 +1586,7 @@ fn struct_numeric_generic_in_struct() {
     assert_eq!(errors.len(), 1);
     assert!(matches!(
         errors[0].0,
-        CompilationError::DefinitionError(
-            DefCollectorErrorKind::UnsupportedNumericGenericType { .. }
-        ),
+        CompilationError::ResolverError(ResolverError::UnsupportedNumericGenericType(_)),
     ));
 }
 
@@ -1641,7 +1639,6 @@ fn bool_generic_as_loop_bound() {
     "#;
     let errors = get_program_errors(src);
     assert_eq!(errors.len(), 3);
-
     assert!(matches!(
         errors[0].0,
         CompilationError::ResolverError(ResolverError::UnsupportedNumericGenericType { .. }),
@@ -1706,7 +1703,7 @@ fn normal_generic_as_array_length() {
 #[test]
 fn numeric_generic_as_param_type() {
     let src = r#"
-    pub fn foo<let I: Field>(x: I) -> I {
+    pub fn foo<let I: u32>(x: I) -> I {
         let _q: I = 5;
         x
     }
@@ -1731,6 +1728,68 @@ fn numeric_generic_as_param_type() {
     ));
 }
 
+#[test]
+fn numeric_generic_as_unused_param_type() {
+    let src = r#"
+    pub fn foo<let I: u32>(_x: I) { }
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 1);
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. }),
+    ));
+}
+
+#[test]
+fn numeric_generic_as_unused_trait_fn_param_type() {
+    let src = r#"
+    trait Foo {
+        fn foo<let I: u32>(_x: I) { }
+    }
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 2);
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. }),
+    ));
+    // Foo is unused
+    assert!(matches!(
+        errors[1].0,
+        CompilationError::ResolverError(ResolverError::UnusedItem { .. }),
+    ));
+}
+
+#[test]
+fn numeric_generic_as_return_type() {
+    let src = r#"
+    // std::mem::zeroed() without stdlib
+    trait Zeroed {
+        fn zeroed<T>(self) -> T;
+    }
+
+    fn foo<T, let I: Field>(x: T) -> I where T: Zeroed {
+        x.zeroed()
+    }
+
+    fn main() {}
+    "#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 2);
+
+    // Error from the return type
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::TypeError(TypeCheckError::TypeKindMismatch { .. }),
+    ));
+    // foo is unused
+    assert!(matches!(
+        errors[1].0,
+        CompilationError::ResolverError(ResolverError::UnusedItem { .. }),
+    ));
+}
+
 #[test]
 fn numeric_generic_used_in_nested_type_fails() {
     let src = r#"
@@ -2385,23 +2444,6 @@ fn impl_not_found_for_inner_impl() {
     ));
 }
 
-#[test]
-fn no_super() {
-    let src = "use super::some_func;";
-    let errors = get_program_errors(src);
-    assert_eq!(errors.len(), 1);
-
-    let CompilationError::DefinitionError(DefCollectorErrorKind::PathResolutionError(
-        PathResolutionError::NoSuper(span),
-    )) = &errors[0].0
-    else {
-        panic!("Expected a 'no super' error, got {:?}", errors[0].0);
-    };
-
-    assert_eq!(span.start(), 4);
-    assert_eq!(span.end(), 9);
-}
-
 #[test]
 fn cannot_call_unconstrained_function_outside_of_unsafe() {
     let src = r#"
@@ -3035,6 +3077,35 @@ fn infer_globals_to_u32_from_type_use() {
     assert_eq!(errors.len(), 0);
 }
 
+#[test]
+fn struct_array_len() {
+    let src = r#"
+        struct Array<T, let N: u32> {
+            inner: [T; N],
+        }
+
+        impl<T, let N: u32> Array<T, N> {
+            pub fn len(self) -> u32 {
+                N as u32
+            }
+        }
+
+        fn main(xs: [Field; 2]) {
+            let ys = Array {
+                inner: xs,
+            };
+            assert(ys.len() == 2);
+        }
+    "#;
+
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 1);
+    assert!(matches!(
+        errors[0].0,
+        CompilationError::ResolverError(ResolverError::UnusedVariable { .. })
+    ));
+}
+
 #[test]
 fn non_u32_in_array_length() {
     let src = r#"
@@ -3084,7 +3155,8 @@ fn use_numeric_generic_in_trait_method() {
         }
 
         fn main() {
-            let _ = Bar{}.foo([1,2,3]);
+            let bytes: [u8; 3] = [1,2,3];
+            let _ = Bar{}.foo(bytes);
         }
     "#;
 
diff --git a/compiler/noirc_frontend/src/tests/imports.rs b/compiler/noirc_frontend/src/tests/imports.rs
index dfdc60e15e4..5ebc5b3bdbd 100644
--- a/compiler/noirc_frontend/src/tests/imports.rs
+++ b/compiler/noirc_frontend/src/tests/imports.rs
@@ -21,6 +21,23 @@ fn use_super() {
     assert_no_errors(src);
 }
 
+#[test]
+fn no_super() {
+    let src = "use super::some_func;";
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 1);
+
+    let CompilationError::DefinitionError(DefCollectorErrorKind::PathResolutionError(
+        PathResolutionError::NoSuper(span),
+    )) = &errors[0].0
+    else {
+        panic!("Expected a 'no super' error, got {:?}", errors[0].0);
+    };
+
+    assert_eq!(span.start(), 4);
+    assert_eq!(span.end(), 9);
+}
+
 #[test]
 fn use_super_in_path() {
     let src = r#"
diff --git a/compiler/noirc_frontend/src/tests/metaprogramming.rs b/compiler/noirc_frontend/src/tests/metaprogramming.rs
index d980cba5cfd..ec52310b3d6 100644
--- a/compiler/noirc_frontend/src/tests/metaprogramming.rs
+++ b/compiler/noirc_frontend/src/tests/metaprogramming.rs
@@ -2,6 +2,17 @@ use crate::hir::def_collector::dc_crate::CompilationError;
 
 use super::get_program_errors;
 
+// Regression for #5388
+#[test]
+fn comptime_let() {
+    let src = r#"fn main() {
+        comptime let my_var = 2;
+        assert_eq(my_var, 2);
+    }"#;
+    let errors = get_program_errors(src);
+    assert_eq!(errors.len(), 0);
+}
+
 #[test]
 fn comptime_type_in_runtime_code() {
     let source = "pub fn foo(_f: FunctionDefinition) {}";
diff --git a/tooling/lsp/src/requests/completion.rs b/tooling/lsp/src/requests/completion.rs
index 2db1665b639..2882cb143bf 100644
--- a/tooling/lsp/src/requests/completion.rs
+++ b/tooling/lsp/src/requests/completion.rs
@@ -581,8 +581,8 @@ impl<'a> NodeFinder<'a> {
             Type::Tuple(types) => {
                 self.complete_tuple_fields(types, self_prefix);
             }
-            Type::TypeVariable(var, _) | Type::NamedGeneric(var, _, _) => {
-                if let TypeBinding::Bound(typ) = &*var.borrow() {
+            Type::TypeVariable(var) | Type::NamedGeneric(var, _) => {
+                if let TypeBinding::Bound(ref typ) = &*var.borrow() {
                     return self.complete_type_fields_and_methods(
                         typ,
                         prefix,
@@ -1662,8 +1662,8 @@ fn get_field_type(typ: &Type, name: &str) -> Option<Type> {
             }
         }
         Type::Alias(alias_type, generics) => Some(alias_type.borrow().get_type(generics)),
-        Type::TypeVariable(var, _) | Type::NamedGeneric(var, _, _) => {
-            if let TypeBinding::Bound(typ) = &*var.borrow() {
+        Type::TypeVariable(var) | Type::NamedGeneric(var, _) => {
+            if let TypeBinding::Bound(ref typ) = &*var.borrow() {
                 get_field_type(typ, name)
             } else {
                 None
@@ -1680,7 +1680,7 @@ fn get_array_element_type(typ: Type) -> Option<Type> {
             let typ = alias_type.borrow().get_type(&generics);
             get_array_element_type(typ)
         }
-        Type::TypeVariable(var, _) | Type::NamedGeneric(var, _, _) => {
+        Type::TypeVariable(var) | Type::NamedGeneric(var, _) => {
             if let TypeBinding::Bound(typ) = &*var.borrow() {
                 get_array_element_type(typ.clone())
             } else {
diff --git a/tooling/lsp/src/requests/hover.rs b/tooling/lsp/src/requests/hover.rs
index 25a401f488e..7b1fa7352a6 100644
--- a/tooling/lsp/src/requests/hover.rs
+++ b/tooling/lsp/src/requests/hover.rs
@@ -530,7 +530,7 @@ impl<'a> TypeLinksGatherer<'a> {
                     self.gather_type_links(generic);
                 }
             }
-            Type::TypeVariable(var, _) => {
+            Type::TypeVariable(var) => {
                 self.gather_type_variable_links(var);
             }
             Type::TraitAsType(trait_id, _, generics) => {
@@ -543,7 +543,7 @@ impl<'a> TypeLinksGatherer<'a> {
                     self.gather_type_links(&named_type.typ);
                 }
             }
-            Type::NamedGeneric(var, _, _) => {
+            Type::NamedGeneric(var, _) => {
                 self.gather_type_variable_links(var);
             }
             Type::Function(args, return_type, env, _) => {
diff --git a/tooling/lsp/src/requests/inlay_hint.rs b/tooling/lsp/src/requests/inlay_hint.rs
index ea73cc688ef..e119ee0d5b6 100644
--- a/tooling/lsp/src/requests/inlay_hint.rs
+++ b/tooling/lsp/src/requests/inlay_hint.rs
@@ -17,7 +17,7 @@ use noirc_frontend::{
     hir_def::stmt::HirPattern,
     node_interner::{NodeInterner, ReferenceId},
     parser::{Item, ParsedSubModule},
-    Type, TypeBinding, TypeVariable, TypeVariableKind,
+    Kind, Type, TypeBinding, TypeVariable,
 };
 
 use crate::{utils, LspState};
@@ -459,19 +459,14 @@ fn push_type_parts(typ: &Type, parts: &mut Vec<InlayHintLabelPart>, files: &File
             parts.push(string_part("&mut "));
             push_type_parts(typ, parts, files);
         }
-        Type::TypeVariable(var, TypeVariableKind::Normal) => {
-            push_type_variable_parts(var, parts, files);
-        }
-        Type::TypeVariable(binding, TypeVariableKind::Integer) => {
-            if let TypeBinding::Unbound(_) = &*binding.borrow() {
-                push_type_parts(&Type::default_int_type(), parts, files);
-            } else {
-                push_type_variable_parts(binding, parts, files);
-            }
-        }
-        Type::TypeVariable(binding, TypeVariableKind::IntegerOrField) => {
-            if let TypeBinding::Unbound(_) = &*binding.borrow() {
-                parts.push(string_part("Field"));
+        Type::TypeVariable(binding) => {
+            if let TypeBinding::Unbound(_, kind) = &*binding.borrow() {
+                match kind {
+                    Kind::Any | Kind::Normal => push_type_variable_parts(binding, parts, files),
+                    Kind::Integer => push_type_parts(&Type::default_int_type(), parts, files),
+                    Kind::IntegerOrField => parts.push(string_part("Field")),
+                    Kind::Numeric(ref typ) => push_type_parts(typ, parts, files),
+                }
             } else {
                 push_type_variable_parts(binding, parts, files);
             }
diff --git a/tooling/lsp/src/trait_impl_method_stub_generator.rs b/tooling/lsp/src/trait_impl_method_stub_generator.rs
index 4fe039e7bd7..14b40858bb1 100644
--- a/tooling/lsp/src/trait_impl_method_stub_generator.rs
+++ b/tooling/lsp/src/trait_impl_method_stub_generator.rs
@@ -10,7 +10,7 @@ use noirc_frontend::{
     },
     hir_def::{function::FuncMeta, stmt::HirPattern, traits::Trait},
     node_interner::{FunctionModifiers, NodeInterner, ReferenceId},
-    Kind, ResolvedGeneric, Type, TypeVariableKind,
+    Kind, ResolvedGeneric, Type,
 };
 
 use crate::modules::relative_module_id_path;
@@ -290,7 +290,7 @@ impl<'a> TraitImplMethodStubGenerator<'a> {
                 self.string.push_str(&trait_.name.0.contents);
                 self.append_trait_generics(trait_generics);
             }
-            Type::TypeVariable(typevar, _) => {
+            Type::TypeVariable(typevar) => {
                 if typevar.id() == self.trait_.self_type_typevar.id() {
                     self.string.push_str("Self");
                     return;
@@ -323,8 +323,8 @@ impl<'a> TraitImplMethodStubGenerator<'a> {
 
                 self.string.push_str("error");
             }
-            Type::NamedGeneric(typevar, _name, _kind) => {
-                self.append_type(&Type::TypeVariable(typevar.clone(), TypeVariableKind::Normal));
+            Type::NamedGeneric(typevar, _name) => {
+                self.append_type(&Type::TypeVariable(typevar.clone()));
             }
             Type::Function(args, ret, env, unconstrained) => {
                 if *unconstrained {
@@ -437,9 +437,11 @@ impl<'a> TraitImplMethodStubGenerator<'a> {
     }
 
     fn append_resolved_generic(&mut self, generic: &ResolvedGeneric) {
-        match &generic.kind {
-            Kind::Normal => self.string.push_str(&generic.name),
-            Kind::Numeric(typ) => {
+        match &generic.kind() {
+            Kind::Any | Kind::Normal | Kind::Integer | Kind::IntegerOrField => {
+                self.string.push_str(&generic.name);
+            }
+            Kind::Numeric(ref typ) => {
                 self.string.push_str("let ");
                 self.string.push_str(&generic.name);
                 self.string.push_str(": ");