diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs
index d9df4a6c..b74ed754 100644
--- a/src/frontend/mod.rs
+++ b/src/frontend/mod.rs
@@ -20,7 +20,7 @@ pub fn parse(
     use crate::side_effects::Output;
     if include_std {
         let std_lib = parse_module("std", &without_comments(include_str!("std_lib.sg")))?;
-        expr = expr.with(std_lib)
+        expr = expr.hard_with(std_lib)
     }
     if include_builtins {
         let alloc = crate::lir::ConstExpr::StandardBuiltin(crate::lir::StandardBuiltin {
diff --git a/src/frontend/parse.rs b/src/frontend/parse.rs
index ad624d55..7dfcdaef 100644
--- a/src/frontend/parse.rs
+++ b/src/frontend/parse.rs
@@ -4475,7 +4475,7 @@ mod tests {
         assert_parse_type(
             "fun<T>(Option<T>) -> Bool",
             Some(Type::Poly(
-                vec!["T".to_string()],
+                vec![("T".to_string(), None)],
                 Type::Proc(
                     vec![Type::Apply(
                         Box::new(Type::Symbol("Option".to_string())),
@@ -4490,7 +4490,7 @@ mod tests {
         assert_parse_type(
             "fun<T>(Option<T>, Int) -> Bool",
             Some(Type::Poly(
-                vec!["T".to_string()],
+                vec![("T".to_string(), None)],
                 Type::Proc(
                     vec![
                         Type::Apply(
diff --git a/src/lir/compile.rs b/src/lir/compile.rs
index 04473aee..68e360cb 100644
--- a/src/lir/compile.rs
+++ b/src/lir/compile.rs
@@ -548,7 +548,7 @@ impl Compile for Expr {
             Self::EnumUnion(t, variant, val) => {
                 // Get the size of the tagged union.
                 let result_size = t.get_size(env)?;
-                let t = t.simplify_until_concrete(env)?;
+                let t = t.simplify_until_concrete(env, false)?;
                 if let Type::EnumUnion(fields) = t {
                     // Get the list of possible variant names.
                     let variants = fields.clone().into_keys().collect::<Vec<_>>();
@@ -843,7 +843,7 @@ impl Compile for Expr {
                     // val_type.add_monomorphized_associated_consts(env)?;
 
                     // Push the address of the struct, tuple, or union onto the stack.
-                    match val_type.simplify_until_has_members(env)? {
+                    match val_type.simplify_until_has_members(env, false)? {
                         // If the value is a struct, tuple, or union:
                         Type::Struct(_) | Type::Tuple(_) | Type::Union(_) => {
                             // Compile a reference to the inner value with the expected mutability.
@@ -928,7 +928,7 @@ impl Compile for Expr {
                     // val_type.add_monomorphized_associated_consts(env)?;
 
                     // Push the address of the struct, tuple, or union onto the stack.
-                    match val_type.simplify_until_has_members(env)? {
+                    match val_type.simplify_until_has_members(env, false)? {
                         // If the value is a struct, tuple, or union:
                         Type::Struct(_) | Type::Tuple(_) | Type::Union(_) => {
                             // Compile a reference to the inner value with the expected mutability.
@@ -1389,7 +1389,7 @@ impl Compile for ConstExpr {
             Self::EnumUnion(t, variant, val) => {
                 // Get the size of the tagged union.
                 let result_size = t.get_size(env)?;
-                let t = t.simplify_until_has_variants(env)?;
+                let t = t.simplify_until_has_variants(env, false)?;
 
                 // Get the inner list of variants and compile the expression using this information.
                 if let Type::EnumUnion(variants) = t.clone().simplify(env)? {
@@ -1463,7 +1463,7 @@ impl Compile for ConstExpr {
             Self::Of(enum_type, variant) => {
                 // Only try to simplify the type 50 times at most.
                 // This is to prevent infinite loops and to keep recursion under control.
-                match enum_type.simplify_until_has_variants(env)? {
+                match enum_type.simplify_until_has_variants(env, false)? {
                     // If the type is an enum, we can continue.
                     Type::Enum(variants) => {
                         // Get the index of the variant.
diff --git a/src/lir/env.rs b/src/lir/env.rs
index 362c2a50..5c343ba0 100644
--- a/src/lir/env.rs
+++ b/src/lir/env.rs
@@ -252,7 +252,10 @@ impl Env {
         // Go through all the types and see if any equals the given type.
         for (other_ty, consts) in associated_constants.iter() {
             if matches!(ty.is_monomorph_of(other_ty, self), Ok(true)) {
-                debug!("Type {ty} is monomorph of {other_ty}");
+                info!("Type {ty} is monomorph of {other_ty}");
+                for (name, (constant, ty)) in consts {
+                    debug!("   {name}: {ty} = {constant}")
+                }
                 let template = other_ty.clone();
 
                 let ty_params = template.get_template_params(self);
@@ -285,11 +288,11 @@ impl Env {
                     }
                 }
 
-                if ty_args.len() != ty_params.len() {
-                    debug!("Mismatched number of template arguments for {monomorph} of {template}");
-                    debug!("Expected {ty_params:?}, found {ty_args:?}");
-                    continue;
-                }
+                // if ty_args.len() != ty_params.len() {
+                //     error!("Mismatched number of template arguments for {monomorph} of {template}");
+                //     error!("Expected {ty_params:?}, found {ty_args:?}");
+                //     continue;
+                // }
 
                 debug!(
                     "Associated constants for {monomorph} are {:?}",
@@ -301,7 +304,7 @@ impl Env {
                     // let result = const_ty.apply(ty_args.clone()).simplify_until_simple(self).ok()?;
                     // let result = const_ty.apply(ty_args.clone());
                     let result = const_ty.apply(ty_args.clone().into_iter().map(|x|x.0).collect());
-                    match result.simplify_until_simple(self) {
+                    match result.simplify_until_simple(self, false) {
                         Ok(result) => {
                             debug!("Found associated const (type) {name} of type {ty} = {result}");
                             return Some(result);
@@ -314,7 +317,7 @@ impl Env {
                             // continue;
                         }
                     }
-                    // info!("Found associated const (type) {name} of type {ty} = {result}");
+                    // debug!("Found associated const (type) {name} of type {ty} = {result}");
                     // return Some(result);
                 }
 
@@ -322,11 +325,15 @@ impl Env {
                 for template_const_name in template_associated_consts.keys() {
                     debug!("   {template_const_name} != {name}");
                 }
+            } else {
+                debug!("Type {ty} is not monomorph of {other_ty}");
             }
 
             if !ty.can_decay_to(other_ty, self).unwrap_or(false) {
-                // trace!("Type {other_ty} does not equal {ty}");
+                debug!("Type {other_ty} does not equal {ty}");
                 continue;
+            } else {
+                debug!("Type {other_ty} equals {ty}");
             }
             if let Some((constant, expr_ty)) = consts.get(name) {
                 let constant = constant.clone();
@@ -337,7 +344,6 @@ impl Env {
                 return Some(expr_ty);
             }
         }
-        trace!("Could not find associated const {name} of type {ty} in {self}");
         drop(associated_constants);
 
         if let Type::Type(inner_ty) = ty {
@@ -355,11 +361,12 @@ impl Env {
                 return Some(ty);
             }
         }
+        error!("Could not find associated const {name} of type {ty} in {self}");
         None
     }
 
     pub fn get_associated_const(&self, ty: &Type, name: &str) -> Option<(ConstExpr, Type)> {
-        trace!(
+        info!(
             "Getting associated const {name} of type {ty} in {self} with types {:?}",
             self.types
         );
@@ -394,16 +401,16 @@ impl Env {
                     debug!("Failed to get monomorph template args for {monomorph} of {template}");
                     continue;
                 }
-                // for (symbol, ty) in &symbols {
-                //     debug!("----> {symbol} == {ty}");
-                // }
+                for (symbol, (ty, expected)) in &symbols {
+                    debug!("----> {symbol} == {ty}, {expected:?}");
+                }
                 let template_associated_consts = consts.clone();
                 let mut ty_args = Vec::new();
                 for (ty_param, _) in &ty_params {
                     if let Some((arg, _)) = symbols.get(ty_param) {
                         ty_args.push(arg.clone());
                     } else {
-                        continue;
+                        debug!("Could not find symbol {ty_param}");
                     }
                 }
 
@@ -416,7 +423,7 @@ impl Env {
                 if let Some((const_expr, const_ty)) = template_associated_consts.get(name) {
                     debug!("Found cached associated const pair: {const_expr} with type {const_ty}");
                     let mut result_ty = const_ty.apply(ty_args.clone());
-                    result_ty = match result_ty.simplify_until_simple(self) {
+                    result_ty = match result_ty.simplify_until_simple(self, true) {
                         Ok(result) => {
                             debug!("Found associated const {name} of type {ty} = {result}");
                             result
@@ -436,7 +443,7 @@ impl Env {
                 debug!("Could not find associated const {name} of type {ty} in {template}");
                 // return self.get_associated_const(&monomorph, name);
             } else {
-                // info!("Type {ty} is not monomorph of {other_ty}");
+                debug!("Type {ty} is not monomorph of {other_ty}");
             }
 
             if !ty.can_decay_to(other_ty, self).unwrap_or(false) {
@@ -573,7 +580,7 @@ impl Env {
     ) -> Result<(), Error> {
         debug!("Adding monomorphized associated constants of type {template} to {monomorph} with type arguments {ty_args:?} to environment");
 
-        let monomorph = if let Ok(simplified) = monomorph.simplify_until_simple(self) {
+        let monomorph = if let Ok(simplified) = monomorph.simplify_until_simple(self, false) {
             debug!("Simplified {monomorph} to {simplified}");
             simplified
         } else {
@@ -665,7 +672,7 @@ impl Env {
         expr: ConstExpr,
     ) -> Result<(), Error> {
         let associated_const_name = associated_const_name.to_string();
-        trace!("Defining associated const {associated_const_name} as {expr} to type {ty}");
+        info!("Defining associated const {associated_const_name} as {expr} to type {ty}");
         let expr_ty = expr.get_type(self)?;
         let mut associated_constants = self.associated_constants.write().unwrap();
         associated_constants
@@ -852,7 +859,9 @@ impl Env {
 
                     for (name, associated_const) in impls {
                         let templated_const =
-                            associated_const.template(template_params.clone());
+                            // associated_const.template(supplied_param_symbols.clone().into_iter().map(|x| (x, None)).collect());
+                            // associated_const.template(template_params.clone());
+                            associated_const.template(template_params.clone().into_iter().zip(supplied_param_symbols.clone().into_iter()).map(|((_, ty), param)| (param, ty)).collect());
                         self.add_associated_const(*template.clone(), name, templated_const)?;
                     }
                 } else {
@@ -1008,7 +1017,7 @@ impl Env {
                 Arc::make_mut(&mut self.consts).insert(name.clone(), ConstExpr::Type(ty.clone()));
                 Arc::make_mut(&mut self.types).insert(name.clone(), ty.clone());
 
-                if let Ok(simplified) = ty.simplify_until_concrete(self) {
+                if let Ok(simplified) = ty.simplify_until_concrete(self, false) {
                     if let Ok(size) = simplified.get_size(self) {
                         self.set_precalculated_size(simplified.clone(), size);
                     }
@@ -1048,7 +1057,7 @@ impl Env {
         }
 
         for (_, ty) in types {
-            if let Ok(simplified) = ty.simplify_until_concrete(self) {
+            if let Ok(simplified) = ty.simplify_until_concrete(self, false) {
                 if let Ok(size) = simplified.get_size(self) {
                     self.set_precalculated_size(simplified, size);
                 } else {
@@ -1283,7 +1292,7 @@ impl Env {
 
 impl Display for Env {
     fn fmt(&self, f: &mut Formatter) -> FmtResult {
-        // return Ok(());
+        return Ok(());
         writeln!(f, "Env")?;
         writeln!(f, "   Types:")?;
         for (name, ty) in self.types.iter() {
@@ -1292,10 +1301,10 @@ impl Display for Env {
             if constants.is_empty() {
                 continue;
             }
-            // writeln!(f, "         Associated constants:")?;
-            // for (name, cexpr) in constants {
-            //     writeln!(f, "            {}: {}", name, cexpr)?;
-            // }
+            writeln!(f, "         Associated constants:")?;
+            for (name, cexpr) in constants {
+                writeln!(f, "            {}: {}", name, cexpr)?;
+            }
         }
         // writeln!(f, "   Constants:")?;
         // for (i, (name, e)) in self.consts.iter().enumerate() {
diff --git a/src/lir/expr/const_expr.rs b/src/lir/expr/const_expr.rs
index b4b2f289..f715946b 100644
--- a/src/lir/expr/const_expr.rs
+++ b/src/lir/expr/const_expr.rs
@@ -105,9 +105,18 @@ impl ConstExpr {
         Self::Monomorphize(Box::new(self), ty_args)
     }
 
-    pub fn equals(&self, other: &Self) -> bool {
+    pub fn equals(&self, other: &Self, env: &Env) -> bool {
+        info!("{self} == {other} in const?");
         match (self, other) {
             (Self::Any, _) | (_, Self::Any) => true,
+            (Self::Type(Type::Any), _) | (_, Self::Type(Type::Any)) => true,
+            (Self::Symbol(name), other) | (other, Self::Symbol(name)) => {
+                if let Some(c) = env.get_const(name) {
+                    c.equals(other, env)
+                } else {
+                    &Self::Symbol(name.clone()) == other
+                }
+            }
             (a, b) => a == b,
         }
     }
@@ -391,7 +400,9 @@ impl ConstExpr {
                         }
                         *ret
                     }
-                    Self::PolyProc(proc) => Self::Proc(proc.monomorphize(ty_args.clone(), env)?),
+                    Self::PolyProc(proc) => {
+                        Self::Proc(proc.monomorphize(ty_args.clone(), env)?)
+                    },
                     Self::Declare(bindings, expr) => {
                         let mut new_env = env.clone();
                         new_env.add_compile_time_declaration(&bindings)?;
@@ -403,6 +414,7 @@ impl ConstExpr {
                         .monomorphize(ty_args.clone())
                         .eval_checked(env, i)
                         .map_err(|x| x.annotate(metadata))?,
+
                     _other => {
                         Self::Monomorphize(Box::new(expr.eval_checked(env, i)?), ty_args.clone())
                     }
@@ -580,7 +592,7 @@ impl GetType for ConstExpr {
                 debug!("Got type of container access {val} . {field}\nContainer: {val_type}");
                 // val_type.add_monomorphized_associated_consts(env)?;
                 // Get the type of the value to get the member of.
-                match &val_type.simplify_until_concrete(env)? {
+                match &val_type.simplify_until_concrete(env, false)? {
                     Type::Unit(_unit_name, inner_ty) => {
                         // Get the type of the field.
                         env.get_type_of_associated_const(inner_ty, &as_symbol?)
@@ -589,7 +601,7 @@ impl GetType for ConstExpr {
 
                     Type::Pointer(_found_mutability, t) => {
                         let val = &Expr::ConstExpr(*val);
-                        let t = t.clone().simplify_until_concrete(env)?;
+                        let t = t.clone().simplify_until_concrete(env, false)?;
                         match t.get_member_offset(&field, val, env) {
                             Ok((t, _)) => t,
                             Err(_) => {
@@ -736,6 +748,7 @@ impl GetType for ConstExpr {
                             .simplify_until_type_checks(env);
                     }
                     Self::Template(params, ret) => {
+                        debug!("Getting type of monomorphized template {self}");
                         if params.len() != ty_args.len() {
                             return Err(Error::InvalidMonomorphize(expr));
                         }
@@ -748,19 +761,25 @@ impl GetType for ConstExpr {
                                     let expected = expected_ty.clone();
                                     let found = cexpr.get_type_checked(env, i)?;
                                     if !found.equals(expected_ty, env)? {
+                                        error!("Mismatch in expected type for constant parameter");
                                         return Err(Error::MismatchedTypes { expected, found, expr: (*cexpr.clone()).into() })
                                     }
+                                    ret.substitute(param, ty_arg)
                                 }
+                                ret.substitute(param, ty_arg);
                                 new_env.define_const(param, *cexpr.clone());
                             } else {
-                                ret.substitute(param, ty_arg)
+                                ret.substitute(param, ty_arg);
+                                new_env.define_type(param, ty_arg.clone());
                             }
                         }
-                        ret.get_type_checked(&new_env, i)?
-                            .simplify_until_type_checks(env)?
+                        debug!("Result: {ret}");
+                        let ret = ret.get_type_checked(&new_env, i)?
+                            .simplify_until_poly(&new_env, false)?;
+                        ret
                     }
                     _ => {
-                        // warn!("Monomorphizing non-template: {expr}");
+                        // debug!("Monomorphizing non-template: {expr}");
                         Type::Apply(Box::new(template_ty.clone()), ty_args.clone())
                     }
                 };
@@ -942,9 +961,9 @@ impl GetType for ConstExpr {
             }
             Self::Symbol(symbol_name) if symbol_name == name => {
                 // A constant symbol cannot be substituted for a type variable.
-                warn!("Subbing {self} for {substitution}");
+                // debug!("Subbing {self} for {substitution}");
                 *self = ConstExpr::Type(substitution.clone());
-                warn!("Subbed into {self}");
+                // debug!("Subbed into {self}");
             }
             _ => {}
         }
diff --git a/src/lir/expr/declaration.rs b/src/lir/expr/declaration.rs
index fee69f97..96972bed 100644
--- a/src/lir/expr/declaration.rs
+++ b/src/lir/expr/declaration.rs
@@ -571,7 +571,9 @@ impl TypeCheck for Declaration {
 
                     for (name, associated_const) in impls {
                         let templated_const =
-                            associated_const.template(supplied_param_symbols.clone().into_iter().map(|x| (x, None)).collect());
+                            // associated_const.template(supplied_param_symbols.clone().into_iter().map(|x| (x, None)).collect());
+                            // associated_const.template(template_params.clone());
+                            associated_const.template(template_params.clone().into_iter().zip(supplied_param_symbols.clone().into_iter()).map(|((_, ty), param)| (param, ty)).collect());
                         new_env.add_associated_const(
                             *template.clone(),
                             name,
diff --git a/src/lir/expr/ops/arithmetic/mod.rs b/src/lir/expr/ops/arithmetic/mod.rs
index e1e9be24..cbdaf75e 100644
--- a/src/lir/expr/ops/arithmetic/mod.rs
+++ b/src/lir/expr/ops/arithmetic/mod.rs
@@ -204,7 +204,6 @@ impl BinaryOp for Arithmetic {
 
     /// Get the type of the result of applying this binary operation to the given types.
     fn return_type(&self, lhs: &Expr, rhs: &Expr, env: &Env) -> Result<Type, Error> {
-        error!("Can I {self} to {lhs} and {rhs} in {env}?");
         if let Expr::Annotated(lhs, metadata) = lhs {
             if let Expr::Annotated(rhs, _) = rhs {
                 return self.return_type(lhs, rhs, env);
@@ -221,7 +220,6 @@ impl BinaryOp for Arithmetic {
         let lhs_ty = lhs.get_type(env)?;
         let rhs_ty = rhs.get_type(env)?;
 
-        error!("Can I {self} to {lhs_ty} and {rhs_ty} in {env}?");
         let result = Ok(match (lhs_ty.discard_type_wrapper(), rhs_ty.discard_type_wrapper()) {
             (Type::Int, Type::Int) => Type::Int,
             (Type::Int, Type::Float) | (Type::Float, Type::Int) | (Type::Float, Type::Float) => {
@@ -298,7 +296,6 @@ impl BinaryOp for Arithmetic {
                 ))
             }
         });
-        error!("Well, can I?? {result:?}");
         result
     }
 
diff --git a/src/lir/expr/ops/comparison.rs b/src/lir/expr/ops/comparison.rs
index fdf5630a..3c76a67c 100644
--- a/src/lir/expr/ops/comparison.rs
+++ b/src/lir/expr/ops/comparison.rs
@@ -23,7 +23,7 @@ pub enum Comparison {
 impl BinaryOp for Comparison {
     /// Can this binary operation be applied to the given types?
     fn can_apply(&self, lhs: &Type, rhs: &Type, env: &Env) -> Result<bool, Error> {
-        match (lhs, self, rhs) {
+        match (&lhs.clone().discard_type_wrapper(), self, &rhs.clone().discard_type_wrapper()) {
             (Type::Int, Self::LessThan, Type::Int)
             | (Type::Int, Self::LessThanOrEqual, Type::Int)
             | (Type::Int, Self::GreaterThan, Type::Int)
diff --git a/src/lir/expr/ops/io.rs b/src/lir/expr/ops/io.rs
index c811c76c..7eb545f7 100644
--- a/src/lir/expr/ops/io.rs
+++ b/src/lir/expr/ops/io.rs
@@ -13,7 +13,7 @@ pub struct Get;
 impl UnaryOp for Get {
     /// Can this unary operation be applied to the given type?
     fn can_apply(&self, ty: &Type, env: &Env) -> Result<bool, Error> {
-        ty.simplify_until_concrete(env).map(|ty| {
+        ty.simplify_until_concrete(env, false).map(|ty| {
             if let Type::Pointer(mutability, x) = ty {
                 match *x {
                     Type::Char | Type::Int | Type::Float => mutability.is_mutable(),
@@ -100,7 +100,7 @@ impl Put {
         env: &mut Env,
         output: &mut dyn AssemblyProgram,
     ) -> Result<(), Error> {
-        let t = &t.simplify_until_concrete(env)?;
+        let t = &t.simplify_until_concrete(env, false)?;
         match t {
             Type::Type(t) => {
                 for c in format!("{}", t).chars() {
@@ -430,7 +430,7 @@ impl Put {
         env: &mut Env,
         output: &mut dyn AssemblyProgram,
     ) -> Result<(), Error> {
-        let t = &t.simplify_until_concrete(env)?;
+        let t = &t.simplify_until_concrete(env, false)?;
         match t {
             Type::Cell => {
                 output.op(CoreOp::Put(addr, Output::stdout_int()));
@@ -597,7 +597,7 @@ impl UnaryOp for Put {
         // Get the size of the type.
         let size = ty.get_size(env)? as isize;
 
-        let ty = &ty.simplify_until_concrete(env)?;
+        let ty = &ty.simplify_until_concrete(env, false)?;
 
         // Calculate the address of the expression on the stack.
         let addr = SP.deref().offset(-size + 1);
diff --git a/src/lir/expr/ops/tagged_union.rs b/src/lir/expr/ops/tagged_union.rs
index ebc80634..ac2e8d1b 100644
--- a/src/lir/expr/ops/tagged_union.rs
+++ b/src/lir/expr/ops/tagged_union.rs
@@ -12,12 +12,12 @@ impl UnaryOp for Tag {
     /// Can this unary operation be applied to the given type?
     fn can_apply(&self, ty: &Type, env: &Env) -> Result<bool, Error> {
         let ty = ty.clone().simplify(env)?;
-        Ok(ty.simplify_until_has_variants(env).is_ok())
+        Ok(ty.simplify_until_has_variants(env, false).is_ok())
     }
 
     /// Get the type of the result of applying this unary operation to the given type.
     fn return_type(&self, expr: &Expr, env: &Env) -> Result<Type, Error> {
-        let ty = expr.get_type(env)?.simplify_until_has_variants(env)?;
+        let ty = expr.get_type(env)?.simplify_until_has_variants(env, false)?;
 
         match ty {
             Type::EnumUnion(variants) => Ok(Type::Enum(variants.into_keys().collect())),
@@ -101,12 +101,12 @@ impl UnaryOp for Data {
     /// Can this unary operation be applied to the given type?
     fn can_apply(&self, ty: &Type, env: &Env) -> Result<bool, Error> {
         let ty = ty.clone().simplify(env)?;
-        Ok(ty.simplify_until_has_variants(env).is_ok())
+        Ok(ty.simplify_until_has_variants(env, false).is_ok())
     }
 
     /// Get the type of the result of applying this unary operation to the given type.
     fn return_type(&self, expr: &Expr, env: &Env) -> Result<Type, Error> {
-        let ty = expr.get_type(env)?.simplify_until_has_variants(env)?;
+        let ty = expr.get_type(env)?.simplify_until_has_variants(env, false)?;
 
         match ty {
             Type::EnumUnion(variants) => Ok(Type::Union(variants)),
diff --git a/src/lir/expr/pattern.rs b/src/lir/expr/pattern.rs
index fbf37e67..0a5c3ac4 100644
--- a/src/lir/expr/pattern.rs
+++ b/src/lir/expr/pattern.rs
@@ -70,7 +70,7 @@ impl Pattern {
         env: &Env,
     ) -> Result<Type, Error> {
         // Get the type of the expression being matched.
-        let ty = expr.get_type(env)?.simplify_until_concrete(env)?;
+        let ty = expr.get_type(env)?.simplify_until_concrete(env, false)?;
         // Get the bindings for the pattern.
         let bindings = self.get_bindings(expr, &ty, env)?;
         // Create a new environment with the bindings.
@@ -98,7 +98,7 @@ impl Pattern {
         matching_expr_ty: &Type,
         env: &Env,
     ) -> Result<bool, Error> {
-        let matching_expr_ty = &matching_expr_ty.simplify_until_concrete(env)?;
+        let matching_expr_ty = &matching_expr_ty.simplify_until_concrete(env, false)?;
         match matching_expr_ty {
             Type::Bool => {
                 // If the type is a boolean, the patterns are exhaustive if they match both `true` and `false`.
@@ -389,7 +389,7 @@ impl Pattern {
     pub fn type_check(&self, matching_expr: &Expr, branch: &Expr, env: &Env) -> Result<(), Error> {
         trace!("Type checking pattern match: {} => {}", self, branch);
         // Get the type of the expression being matched.
-        let matching_ty = matching_expr.get_type(env)?.simplify_until_concrete(env)?;
+        let matching_ty = matching_expr.get_type(env)?.simplify_until_concrete(env, false)?;
         // Get the type of the branch as a result of the match.
         let expected = self.get_branch_result_type(matching_expr, branch, env)?;
         // Type-check the expression generated to match the pattern.
@@ -498,7 +498,7 @@ impl Pattern {
         // Create a new environment with the bindings
         let mut new_env = env.clone();
         // Get the type of the expression being matched
-        let match_type = expr.get_type(env)?.simplify_until_concrete(env)?;
+        let match_type = expr.get_type(env)?.simplify_until_concrete(env, false)?;
         // Define the variable in the new environment.
         new_env.define_var(var_name.clone(), Mutability::Immutable, match_type.clone())?;
         // Generate the expression which evaluates the `match` expression.
@@ -570,7 +570,7 @@ impl Pattern {
         env: &Env,
         mut origin: usize,
     ) -> Result<HashMap<String, (Mutability, Type, usize)>, Error> {
-        let ty = &ty.simplify_until_concrete(env)?;
+        let ty = &ty.simplify_until_concrete(env, false)?;
         Ok(match (self, ty) {
             // If the pattern is a tuple, and the type is a tuple, then
             // get the bindings for each element of the tuple.
@@ -719,7 +719,7 @@ impl Pattern {
     /// Does this pattern match the given expression?
     /// This function returns an expression which evaluates to true if the expression matches the pattern.
     fn matches(&self, expr: &Expr, ty: &Type, env: &Env) -> Result<Expr, Error> {
-        let ty = &ty.simplify_until_concrete(env)?;
+        let ty = &ty.simplify_until_concrete(env, false)?;
         Ok(match (self, ty) {
             // If the pattern is a variant, and the type is a EnumUnion,
             // check if the variant matches the pattern.
@@ -879,7 +879,7 @@ impl Pattern {
     /// then this will not work correctly. This function does not check the arguments.***
     pub fn declare_let_bind(&self, expr: &Expr, ty: &Type, env: &mut Env) -> Result<(), Error> {
         // Get the type of the expression being matched.
-        let ty = &ty.simplify_until_concrete(env)?;
+        let ty = &ty.simplify_until_concrete(env, false)?;
         // Get the variable bindings for the pattern.
         // This tells us the type and mutability of each variable.
         let bindings = self.get_bindings_with_offset(expr, ty, env, 0)?;
@@ -905,7 +905,7 @@ impl Pattern {
     /// added to the environment, and will be bound to the corresponding value in
     /// the expression which is being matched.
     fn bind(&self, expr: &Expr, ty: &Type, ret: &Expr, env: &Env) -> Result<Expr, Error> {
-        let ty = &ty.simplify_until_concrete(env)?;
+        let ty = &ty.simplify_until_concrete(env, false)?;
         Ok(match (self, ty) {
             // If the pattern is a variant, and the type is a tagged union,
             // bind the pattern to the corresponding variant type in the tagged union.
diff --git a/src/lir/expr/procedure/poly.rs b/src/lir/expr/procedure/poly.rs
index 763943d7..9cd6f13b 100644
--- a/src/lir/expr/procedure/poly.rs
+++ b/src/lir/expr/procedure/poly.rs
@@ -115,20 +115,20 @@ impl PolyProcedure {
         // This is a helper function to distribute the defined type
         // arguments over the body and arguments of the function.
 
-        for ((_name, ty_param), ty_arg) in self.ty_params.iter().zip(ty_args.iter()) {
-            if let Some(ty_param) = ty_param {
-                if !ty_param.equals(&ty_arg, env)? {
-                    return Err(Error::MismatchedTypes { expected: ty_param.clone(), found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into()) })
-                }
-            } else {
-                use crate::lir::Simplify;
-                if matches!(ty_arg.clone().simplify(env)?, Type::ConstParam(..)) {
-                    return Err(Error::UnexpectedConstParam {
-                        found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into())
-                    })
-                }
-            }
-        }
+        // for ((_name, ty_param), ty_arg) in self.ty_params.iter().zip(ty_args.iter()) {
+        //     if let Some(ty_param) = ty_param {
+        //         if !ty_param.equals(&ty_arg, env)? {
+        //             return Err(Error::MismatchedTypes { expected: ty_param.clone(), found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into()) })
+        //         }
+        //     } else {
+        //         use crate::lir::Simplify;
+        //         if matches!(ty_arg.clone().simplify(env)?, Type::ConstParam(..)) {
+        //             return Err(Error::UnexpectedConstParam {
+        //                 found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into())
+        //             })
+        //         }
+        //     }
+        // }
 
         // Simplify all the type arguments until they are concrete
         let simplified_ty_args = ty_args
@@ -136,7 +136,7 @@ impl PolyProcedure {
             .into_iter()
             .map(|ty| {
                 // Simplify the type until it is concrete
-                let concrete = ty.simplify_until_concrete(env)?;
+                let concrete = ty.simplify_until_concrete(env, true)?;
                 // concrete.add_monomorphized_associated_consts(env)?;
                 Ok(concrete)
             })
@@ -153,7 +153,7 @@ impl PolyProcedure {
             );
             // Simplify the type until it is simple.
             // This reduces to the concrete version of the type application.
-            let concrete = ty.simplify_until_concrete(env)?;
+            let concrete = ty.simplify_until_concrete(env, true)?;
             // concrete.add_monomorphized_associated_consts(env)?;
             Ok(concrete)
         };
@@ -226,12 +226,18 @@ impl GetType for PolyProcedure {
 
     fn substitute(&mut self, name: &str, ty: &Type) {
         if self.type_param_names().contains(&name.to_string()) {
+            debug!("Not substituting {name} in {ty} because of symbol conflict");
             return;
         }
+        for (_, ty_arg) in &mut self.ty_params {
+            *ty_arg = ty_arg.as_mut().map(|ty_arg| ty_arg.substitute(name, ty));
+        }
+
         self.args
             .iter_mut()
             .for_each(|(_, _, t)| *t = t.substitute(name, ty));
         self.ret = self.ret.substitute(name, ty);
+        self.body.substitute(name, ty);
     }
 }
 
diff --git a/src/lir/types/check.rs b/src/lir/types/check.rs
index 1e492a44..3b0431ea 100644
--- a/src/lir/types/check.rs
+++ b/src/lir/types/check.rs
@@ -72,7 +72,7 @@ impl TypeCheck for Type {
                 len.clone().type_check(env)?;
 
                 // Check that the length is non-negative.
-                warn!("About to convert {len} to int");
+                debug!("About to convert {len} to int");
                 match len.clone().as_int(env) {
                     Ok(n) if n < 0 => {
                         // If it is negative, return an error.
@@ -158,14 +158,14 @@ impl TypeCheck for Type {
                     .try_for_each(|t| t.type_check(env))?;
 
                 // Try to confirm that the polymorphic type is a template.
-                match poly.simplify_until_poly(env)? {
+                match poly.simplify_until_poly(env, true)? {
                     Type::Symbol(name) => {
                         // Get the type definition.
                         let ty = env
                             .get_type(&name)
                             .ok_or(Error::TypeNotDefined(name.clone()))?;
                         // Check that the type is a template.
-                        match ty.simplify_until_poly(env)? {
+                        match ty.simplify_until_poly(env, true)? {
                             Type::Poly(ty_params, _) => {
                                 // Check that the number of type arguments matches the number of type parameters.
                                 if ty_args.len() != ty_params.len() {
@@ -631,7 +631,7 @@ impl TypeCheck for Expr {
                         f.type_check(env)?;
 
                         // Get the type of the function.
-                        let f_type = f.get_type(env)?.simplify_until_concrete(env)?;
+                        let f_type = f.get_type(env)?.simplify_until_concrete(env, true)?;
                         // Infer the types of the supplied arguments.
                         let mut found_arg_tys = vec![];
                         for arg in args {
@@ -686,7 +686,7 @@ impl TypeCheck for Expr {
                 }
 
                 // Get the type of the function.
-                let f_type = f.get_type(env)?.simplify_until_concrete(env)?;
+                let f_type = f.get_type(env)?.simplify_until_concrete(env, true)?;
                 // Infer the types of the supplied arguments.
                 let mut found_arg_tys = vec![];
                 for arg in args {
@@ -789,7 +789,7 @@ impl TypeCheck for Expr {
             Self::Union(t, field, val) => {
                 // Typecheck the type.
                 t.type_check(env)?;
-                let t = t.simplify_until_union(env)?;
+                let t = t.simplify_until_union(env, true)?;
                 match t {
                     Type::Union(fields) => {
                         // Confirm that the variant is a valid variant.
@@ -823,7 +823,7 @@ impl TypeCheck for Expr {
             Self::EnumUnion(t, variant, val) => {
                 // Typecheck the type
                 t.type_check(env)?;
-                let t = t.simplify_until_union(env)?;
+                let t = t.simplify_until_union(env, true)?;
 
                 match t {
                     Type::EnumUnion(fields) => {
@@ -882,7 +882,7 @@ impl TypeCheck for Expr {
                 match e_type.type_check_member(field, e, env) {
                     Ok(_) => Ok(()),
                     Err(e) => {
-                        warn!("Type {e_type} doesn't have member {field} in environment {env}");
+                        debug!("Type {e_type} doesn't have member {field} in environment {env}");
                         match field
                             .clone()
                             .as_symbol(env)
@@ -972,21 +972,21 @@ impl TypeCheck for ConstExpr {
                 match e_type.type_check_member(field, &Expr::ConstExpr(*e.clone()), env) {
                     Ok(_) => Ok(()),
                     Err(_err) => {
-                        warn!("Member {field} not found in type {e_type} in environment {env}");
+                        debug!("Member {field} not found in type {e_type} in environment {env}");
                         match field
                             .clone()
                             .as_symbol(env)
                             .map(|name| env.get_associated_const(&e_type, &name))
                         {
                             Ok(_) => {
-                                warn!("Associated constant {field} found in type {e_type} in environment {env}");
+                                debug!("Associated constant {field} found in type {e_type} in environment {env}");
                                 Ok(())
                             }
                             // Err(_) => Err(e),
                             Err(_) => {
                                 // Try to perform the member op as a regular member op.
-                                warn!("Associated constant {field} not found in type {e_type} in environment {env}");
-                                warn!("Falling back on regular member access");
+                                debug!("Associated constant {field} not found in type {e_type} in environment {env}");
+                                debug!("Falling back on regular member access");
                                 Expr::Member(Box::new(Expr::ConstExpr(*e.clone())), *field.clone())
                                     .type_check(env)
                             }
@@ -1030,27 +1030,36 @@ impl TypeCheck for ConstExpr {
                 match **expr {
                     Self::Template(ref ty_params, ref template) => {
                         // Create a new environment with the type parameters defined.
-                        let mut new_env = env.clone();
                         // Define the type parameters in the environment.
                         // new_env.define_types(
                         //     ty_params.clone().into_iter().map(|x| x.0).zip(ty_args.clone()).collect(),
                         // );
-                        for ((name, ty_param), ty_arg) in ty_params.iter().zip(ty_args) {
-                            new_env.define_type(name, match ty_param {
-                                Some(ty_param) => {
-                                    if !ty_arg.equals(ty_param, env)? {
-                                        return Err(Error::InvalidMonomorphize(self.clone()))
+
+                        let mut ret = template.clone();
+                        let mut new_env = env.clone();
+                        for ((param, ty), ty_arg) in ty_params.iter().zip(ty_args.iter()) {
+                            if let Type::ConstParam(cexpr) = ty_arg {
+                                if let Some(expected_ty) = ty {
+                                    let expected = expected_ty.clone();
+                                    let found = cexpr.get_type(env)?;
+                                    if !found.equals(expected_ty, env)? {
+                                        error!("Mismatch in expected type for constant parameter");
+                                        return Err(Error::MismatchedTypes { expected, found, expr: (*cexpr.clone()).into() })
                                     }
-                                    ty_arg.clone()
-                                }
-                                None => {
-                                    ty_arg.clone()
+                                    ret.substitute(param, ty_arg)
                                 }
-                            })
+                                ret.substitute(param, ty_arg);
+                                new_env.define_const(param, *cexpr.clone());
+                            } else {
+                                ret.substitute(param, ty_arg);
+                                new_env.define_type(param, ty_arg.clone());
+                            }
                         }
-
+                        debug!("Result: {ret}");
+                        let ret = ret.get_type(&new_env)?
+                            .simplify_until_poly(&new_env, true)?;
                         // Check the template type.
-                        template.type_check(&new_env)
+                        ret.type_check(&new_env)
                         // Ok(())
                     }
                     Self::PolyProc(ref poly) => {
@@ -1142,7 +1151,7 @@ impl TypeCheck for ConstExpr {
             // Typecheck a variant of an enum.
             Self::Of(t, variant) => {
                 let t = t
-                    .simplify_until_has_variants(env)
+                    .simplify_until_has_variants(env, true)
                     .map_err(|_| Error::VariantNotFound(t.clone(), variant.clone()))?;
 
                 match t {
@@ -1264,7 +1273,7 @@ impl TypeCheck for ConstExpr {
             // Typecheck a union literal.
             Self::Union(t, field, val) => {
                 // Confirm the type supplied is a union.
-                let t = t.simplify_until_union(env)?;
+                let t = t.simplify_until_union(env, true)?;
 
                 match t {
                     Type::Union(fields) => {
@@ -1303,7 +1312,7 @@ impl TypeCheck for ConstExpr {
             // Typecheck a tagged union literal.
             Self::EnumUnion(t, variant, val) => {
                 // Confirm the type supplied is a union.
-                let t = t.simplify_until_union(env)?;
+                let t = t.simplify_until_union(env, true)?;
                 match t {
                     Type::EnumUnion(fields) => {
                         // Confirm that the variant is a valid variant.
diff --git a/src/lir/types/inference.rs b/src/lir/types/inference.rs
index 73cfa50b..8aabc9cd 100644
--- a/src/lir/types/inference.rs
+++ b/src/lir/types/inference.rs
@@ -232,7 +232,7 @@ impl GetType for Expr {
                 // Get the type of the expression.
                 let t = expr
                     .get_type_checked(env, i)?
-                    .simplify_until_concrete(env)?;
+                    .simplify_until_concrete(env, false)?;
                 // If the type is a pointer, return the inner type of the pointer.
                 if let Type::Pointer(_, inner) = t {
                     // If the type *evaluates* to a pointer, return that inner type.
@@ -253,7 +253,7 @@ impl GetType for Expr {
                 // Get the type of the function.
                 let ty = func
                     .get_type_checked(env, i)?
-                    .simplify_until_concrete(env)?;
+                    .simplify_until_concrete(env, false)?;
                 match ty {
                     Type::Proc(_, ret) => *ret,
                     _ => return Err(Error::ApplyNonProc(self.clone())),
@@ -313,7 +313,7 @@ impl GetType for Expr {
                 // Get the type of the value to get the member of.
                 let val_type = val.get_type_checked(env, i)?;
                 // val_type.add_monomorphized_associated_consts(env)?;
-                let val_type = val_type.simplify_until_concrete(env)?;
+                let val_type = val_type.simplify_until_concrete(env, false)?;
                 // val_type.add_monomorphized_associated_consts(env)?;
                 match val_type {
                     Type::Type(ty) => {
diff --git a/src/lir/types/mod.rs b/src/lir/types/mod.rs
index 55d34505..4f65c75a 100644
--- a/src/lir/types/mod.rs
+++ b/src/lir/types/mod.rs
@@ -366,6 +366,7 @@ impl Type {
                     self.clone()
                 }
             }
+            Self::Pointer(mutability, ty) => Self::Pointer(*mutability, ty.strip_template(env).into()),
             _ => self.clone(),
         }
     }
@@ -435,8 +436,21 @@ impl Type {
                 }
             }
 
-            (Self::Array(inner1, _), Self::Array(inner2, _)) => {
+            (Self::Array(inner1, cexpr1), Self::Array(inner2, cexpr2)) => {
                 inner1.get_monomorph_template_args(inner2, matched_symbols, param_symbols, env)?;
+
+                let ty1 = match &**cexpr1 {
+                    ConstExpr::Symbol(name) => Type::Symbol(name.clone()),
+                    ConstExpr::Type(ty) => ty.clone(),
+                    otherwise => Type::ConstParam(otherwise.clone().into())
+                };
+                let ty2 = match &**cexpr2 {
+                    ConstExpr::Symbol(name) => Type::Symbol(name.clone()),
+                    ConstExpr::Type(ty) => ty.clone(),
+                    _ => return Ok(())
+                };
+
+                ty1.get_monomorph_template_args(&ty2, matched_symbols, param_symbols, env)?
             }
 
             (Self::Pointer(_, inner1), Self::Pointer(_, inner2)) => {
@@ -476,7 +490,7 @@ impl Type {
             }
 
             (Self::Apply(template, args), other) => {
-                if let Ok(Self::Poly(params, ret)) = template.simplify_until_poly(env) {
+                if let Ok(Self::Poly(params, ret)) = template.simplify_until_poly(env, false) {
                     let mut ret = *ret.clone();
                     for ((param, _), arg) in params.iter().zip(args.iter()) {
                         ret = ret.substitute(param, arg);
@@ -503,7 +517,7 @@ impl Type {
 
             (a, b) => {
                 if a != b {
-                    error!(
+                    debug!(
                         "get_monomorph_template_args: Couldn't match {} to {}",
                         self, template
                     );
@@ -515,8 +529,11 @@ impl Type {
     }
 
     pub fn is_monomorph_of(&self, template: &Self, env: &Env) -> Result<bool, Error> {
-        match (self, template) {
-            (Self::Apply(template1, _), template2) => template1.equals(template2, env),
+        debug!("{self} is mono of {template}?");
+        let result = match (self, template) {
+            (Self::Apply(template1, _), template2) => {
+                template1.equals(template2, env)
+            },
             (concrete, Self::Poly(params, result)) => {
                 let mut result = *result.clone();
                 for (param, _) in params {
@@ -538,8 +555,25 @@ impl Type {
                 Ok(false)
             }
 
+            (Self::Pointer(mut1, ty1), Self::Pointer(mut2, ty2)) => {
+                Ok(mut1 == mut2 && ty1.is_monomorph_of(ty2, env)?)
+            }
+
+            (Self::Array(elem1, len1), Self::Array(elem2, len2)) => {
+                // return Ok(elem1.is_monomorph_of(elem2, env)? && len1.get_type(env)?.equals(&len2.get_type(env)?, env)?)
+                return Ok(elem1.is_monomorph_of(elem2, env)?)
+            }
+
+            (Self::ConstParam(cexpr), other) => cexpr.get_type(env)?.equals(other, env),
+
             _ => Ok(false),
+        };
+        if result.clone().is_ok_and(|x| x) {
+            debug!("{self} is monomorph of {template}");
+        } else {
+            debug!("{self} is NOT monomorph of {template}");
         }
+        result
     }
 
     pub fn add_monomorphized_associated_consts(&self, env: &Env) -> Result<(), Error> {
@@ -548,11 +582,11 @@ impl Type {
             Self::Apply(template, args) => {
                 let simplified_args = args
                     .iter()
-                    .map(|t| t.simplify_until_concrete(env))
+                    .map(|t| t.simplify_until_concrete(env, false))
                     .collect::<Result<Vec<_>, _>>()?;
 
                 let mut mono_ty = Self::Apply(template.clone(), simplified_args.clone());
-                mono_ty = mono_ty.simplify_until_concrete(env)?;
+                mono_ty = mono_ty.simplify_until_concrete(env, false)?;
                 // warn!("add_monomorphized_associated_consts: Adding monomorphized associated consts for {self} to {}", mono_ty);
 
                 env.add_monomorphized_associated_consts(*template, mono_ty, simplified_args)?;
@@ -622,7 +656,7 @@ impl Type {
 
     pub fn get_template_params(&self, env: &Env) -> Vec<(String, Option<Type>)> {
         debug!("get_template_params: {}", self);
-        match self.simplify_until_poly(env) {
+        match self.simplify_until_poly(env, false) {
             Ok(Self::Poly(params, _)) => {
                 // debug!(
                 //     "get_template_params: {} params: {}",
@@ -768,7 +802,7 @@ impl Type {
 
     /// Is first argument of function a reference?
     pub fn is_self_param_reference(&self, env: &Env) -> Result<bool, Error> {
-        Ok(match self.simplify_until_concrete(env)? {
+        Ok(match self.simplify_until_concrete(env, false)? {
             Self::Proc(args, _) => {
                 matches!(args.first(), Some(Self::Pointer(_, _)))
             }
@@ -778,7 +812,7 @@ impl Type {
 
     /// Get the first argument's mutability (if it is a pointer)
     pub fn get_self_param_mutability(&self, env: &Env) -> Option<Mutability> {
-        match self.simplify_until_concrete(env) {
+        match self.simplify_until_concrete(env, false) {
             Ok(Self::Proc(args, _)) => {
                 if let Some(Self::Pointer(mutability, _)) = args.first() {
                     Some(*mutability)
@@ -807,7 +841,7 @@ impl Type {
     /// Simplify until the type passes the type checker.
     pub fn simplify_until_type_checks(&self, env: &Env) -> Result<Self, Error> {
         self.clone()
-            .simplify_until_matches(env, Type::Any, |t, env| t.type_check(env).map(|_| true))
+            .simplify_until_matches(env, Type::Any, |t, env| t.type_check(env).map(|_| true), true)
     }
 
     fn possibly_has_members(&self) -> bool {
@@ -826,10 +860,10 @@ impl Type {
     }
 
     /// Simplify a type until you can get its members.
-    pub fn simplify_until_has_members(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_has_members(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self
             .clone()
-            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.possibly_has_members()));
+            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.possibly_has_members()), checked);
 
         if result.is_err() {
             warn!("Couldn't simplify {} to a type with members", self);
@@ -851,10 +885,10 @@ impl Type {
     }
 
     /// Simplify a type until it's a union.
-    pub fn simplify_until_union(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_union(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self
             .clone()
-            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.is_union()));
+            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.is_union()), checked);
         if result.is_err() {
             debug!("Couldn't simplify {} to a union", self);
         }
@@ -874,10 +908,10 @@ impl Type {
     }
 
     /// Simplify a type until you can get its variants.
-    pub fn simplify_until_has_variants(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_has_variants(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self
             .clone()
-            .simplify_until_matches(env, Type::Enum(vec![]), |t, _| Ok(t.has_variants()));
+            .simplify_until_matches(env, Type::Enum(vec![]), |t, _| Ok(t.has_variants()), checked);
         if result.is_err() {
             debug!("Couldn't simplify {} to a type with variants", self);
         }
@@ -896,19 +930,19 @@ impl Type {
         false
     }
 
-    pub fn simplify_until_atomic(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_atomic(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self
             .clone()
-            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.is_atomic()));
+            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.is_atomic()), checked);
         if result.is_err() {
             debug!("Couldn't simplify {} to an atomic type", self);
         }
         result
     }
-    pub fn simplify_until_simple(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_simple(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self
             .clone()
-            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.is_simple()));
+            .simplify_until_matches(env, Type::Any, |t, _| Ok(t.is_simple()), checked);
         if result.is_err() {
             debug!("Couldn't simplify {} to a simple type", self);
         }
@@ -916,11 +950,12 @@ impl Type {
     }
 
     /// Simplify until the type is a polymorphic type.
-    pub fn simplify_until_poly(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_poly(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self.clone().simplify_until_matches(
             env,
             Type::Poly(vec![], Box::new(Type::Any)),
             |t, _| Ok(t.is_polymorphic()),
+            checked
         );
         if result.is_err() {
             debug!("Couldn't simplify {} to a polymorphic type", self);
@@ -929,10 +964,10 @@ impl Type {
     }
 
     /// Simplify until the type is concrete.
-    pub fn simplify_until_concrete(&self, env: &Env) -> Result<Self, Error> {
+    pub fn simplify_until_concrete(&self, env: &Env, checked: bool) -> Result<Self, Error> {
         let result = self
             .clone()
-            .simplify_until_matches(env, Type::Any, |t, _env| Ok(t.is_concrete()));
+            .simplify_until_matches(env, Type::Any, |t, _env| Ok(t.is_concrete()), checked);
         if result.is_err() {
             debug!("Couldn't simplify {} to a concrete type", self);
         }
@@ -949,6 +984,7 @@ impl Type {
         env: &Env,
         expected: Self,
         f: impl Fn(&Self, &Env) -> Result<bool, Error>,
+        checked: bool
     ) -> Result<Self, Error> {
         let mut simplified = self;
         // for _ in 0..Self::SIMPLIFY_RECURSION_LIMIT {
@@ -956,7 +992,7 @@ impl Type {
             if f(&simplified, env)? || simplified.is_atomic() {
                 return Ok(simplified);
             }
-            simplified = simplified.perform_template_applications(env, &mut HashMap::new())?
+            simplified = simplified.perform_template_applications(env, &mut HashMap::new(), checked)?
         }
         Err(Error::CouldntSimplify(simplified, expected))
     }
@@ -1039,7 +1075,7 @@ impl Type {
     /// Substitute all occurences of a symbol with another type.
     /// This will not traverse into let-bindings when the symbol is overshadowed.
     pub fn substitute(&self, name: &str, substitution: &Self) -> Self {
-        warn!("Subbing {name} for {substitution} in {self}");
+        // warn!("Subbing {name} for {substitution} in {self}");
         let result = match self {
             Self::Type(t) => Self::Type(Box::new(t.substitute(name, substitution))),
             Self::Let(typename, binding, ret) => Self::Let(
@@ -1066,7 +1102,7 @@ impl Type {
                 } else {
                     // Does the inner symbol use this type variable?
                     Self::Poly(
-                        ty_params.clone(),
+                        ty_params.iter().map(|(x, ty)| (x.clone(), ty.as_ref().map(|ty| ty.substitute(name, substitution)))).collect(),
                         template.substitute(name, substitution).into(),
                     )
                 }
@@ -1150,7 +1186,7 @@ impl Type {
                 Self::Pointer(*mutability, Box::new(ptr.substitute(name, substitution)))
             }
         };
-        warn!("Got back {result}");
+        // warn!("Got back {result}");
         result
     }
 
@@ -1174,7 +1210,7 @@ impl Type {
     /// For all cases right now, a decay does nothing; the representations of the types
     /// in the compiler are the same for all types of decay.
     pub fn can_decay_to(&self, desired: &Self, env: &Env) -> Result<bool, Error> {
-        trace!("Checking if {} can decay to {}", self, desired);
+        // trace!("Checking if {} can decay to {}", self, desired);
         if self.equals(desired, env)? {
             return Ok(true);
         }
@@ -1234,6 +1270,8 @@ impl Type {
                     return Ok(true);
                 }
 
+                debug!("Could not decay {self} into {desired}");
+
                 Ok(false)
             }
 
@@ -1258,7 +1296,7 @@ impl Type {
             (Self::Array(found_elem_ty, found_len), Self::Array(desired_elem_ty, expected_len)) => {
                 // Check if the element types can decay, and if the sizes are equal.
                 if found_elem_ty.can_decay_to(desired_elem_ty, env)?
-                    && found_len.clone().eval(env)?.equals(&expected_len.clone().eval(env)?)
+                    && found_len.clone().eval(env)?.equals(&expected_len.clone().eval(env)?, env)
                 {
                     trace!("{} can decay to {}", self, desired);
                     return Ok(true);
@@ -1266,7 +1304,7 @@ impl Type {
 
                 // Check if the element types are compatible, and if the sizes are equal.
                 if found_elem_ty.has_element_type(desired_elem_ty, env)?
-                    && found_len.clone().eval(env)?.equals(&expected_len.clone().eval(env)?)
+                    && found_len.clone().eval(env)?.equals(&expected_len.clone().eval(env)?, env)
                 {
                     trace!("{} can decay to {}", self, desired);
                     return Ok(true);
@@ -1472,6 +1510,7 @@ impl Type {
         &self,
         env: &Env,
         previous_applications: &mut HashMap<(Type, Vec<Type>), Type>,
+        checked: bool,
     ) -> Result<Self, Error> {
         let _before = self.to_string();
         trace!("Performing template applications on {}", self);
@@ -1482,10 +1521,10 @@ impl Type {
         Ok(match self.clone().simplify(env)? {
             Self::Apply(poly, ty_args) => {
                 let pair = (
-                    poly.perform_template_applications(env, previous_applications)?,
+                    poly.perform_template_applications(env, previous_applications, checked)?,
                     ty_args
                         .into_iter()
-                        .map(|t| t.perform_template_applications(env, previous_applications))
+                        .map(|t| t.perform_template_applications(env, previous_applications, checked))
                         .collect::<Result<Vec<_>, _>>()?,
                 );
                 if let Some(t) = previous_applications.get(&pair) {
@@ -1497,21 +1536,46 @@ impl Type {
                         Self::Poly(params, mono_ty) => {
                             let _poly = Self::Poly(params.clone(), mono_ty.clone());
                             let mut mono_ty = *mono_ty;
-                            for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
-                                if let Some(expected_ty) = expected_ty {
-                                    if !expected_ty.equals(ty_arg, env)? && !matches!(ty_arg, Type::Unit(name, ..) if param == name) {
-                                        return Err(Error::MismatchedTypes { expected: expected_ty.clone(), found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into()) })
+                            if !checked {
+                                for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
+                                    mono_ty = mono_ty.substitute(param, ty_arg);
+                                }
+                            } else {
+                                let mut new_env = env.clone();
+                                for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
+                                    new_env.define_type(param, ty_arg.clone());
+                                }
+                                for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
+                                    if let Some(expected_ty) = expected_ty {
+                                        if !expected_ty.equals(ty_arg, &new_env)? && !matches!(ty_arg, Type::Unit(name, inner) if param == name || **inner == Type::None) {
+                                            return Err(Error::MismatchedTypes { expected: expected_ty.clone(), found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into()) })
+                                        }
                                     }
+                                    mono_ty = mono_ty.substitute(param, ty_arg);
                                 }
-                                mono_ty = mono_ty.substitute(param, ty_arg);
                             }
                             mono_ty
                         }
                         Self::Symbol(s) => match env.get_type(s.as_str()).cloned() {
                             Some(Self::Poly(params, mono_ty)) => {
                                 let mut mono_ty = *mono_ty;
-                                for ((param, _), ty_arg) in params.iter().zip(ty_args.iter()) {
-                                    mono_ty = mono_ty.substitute(param, ty_arg);
+                                if !checked {
+                                    for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
+                                        mono_ty = mono_ty.substitute(param, ty_arg);
+                                    }
+                                } else {
+                                    let mut new_env = env.clone();
+                                    for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
+                                        new_env.define_type(param, ty_arg.clone());
+                                    }
+                                    for ((param, expected_ty), ty_arg) in params.iter().zip(ty_args.iter()) {
+                                        if let Some(expected_ty) = expected_ty {
+                                            if !expected_ty.equals(ty_arg, &new_env)? && !matches!(ty_arg, Type::Unit(name, inner) if param == name || **inner == Type::None) {
+                                                return Err(Error::MismatchedTypes { expected: expected_ty.clone(), found: ty_arg.clone(), expr: Expr::ConstExpr(self.clone().into()) })
+                                            }
+                                        }
+                                        mono_ty = mono_ty.substitute(param, ty_arg);
+                                    }
                                 }
                                 mono_ty
                             }
@@ -1524,13 +1588,13 @@ impl Type {
             }
             Self::Pointer(mutability, inner) => Self::Pointer(
                 mutability,
-                Box::new(inner.perform_template_applications(env, previous_applications)?),
+                Box::new(inner.perform_template_applications(env, previous_applications, checked)?),
             ),
             Self::Proc(args, ret) => Self::Proc(
                 args.into_iter()
-                    .map(|t| t.perform_template_applications(env, previous_applications))
+                    .map(|t| t.perform_template_applications(env, previous_applications, checked))
                     .collect::<Result<Vec<_>, _>>()?,
-                Box::new(ret.perform_template_applications(env, previous_applications)?),
+                Box::new(ret.perform_template_applications(env, previous_applications, checked)?),
             ),
             Self::Struct(fields) if !self.is_recursive(env)? => Self::Struct(
                 fields
@@ -1538,7 +1602,7 @@ impl Type {
                     .map(|(name, t)| {
                         Ok((
                             name,
-                            t.perform_template_applications(env, previous_applications)?,
+                            t.perform_template_applications(env, previous_applications, checked)?,
                         ))
                     })
                     .collect::<Result<BTreeMap<_, _>, Error>>()?,
@@ -1549,7 +1613,7 @@ impl Type {
                     .map(|(name, t)| {
                         Ok((
                             name,
-                            t.perform_template_applications(env, previous_applications)?,
+                            t.perform_template_applications(env, previous_applications, checked)?,
                         ))
                     })
                     .collect::<Result<BTreeMap<_, _>, Error>>()?,
@@ -1561,26 +1625,26 @@ impl Type {
                     .map(|(name, t)| {
                         Ok((
                             name,
-                            t.perform_template_applications(env, previous_applications)?,
+                            t.perform_template_applications(env, previous_applications, checked)?,
                         ))
                     })
                     .collect::<Result<BTreeMap<_, _>, Error>>()?,
             ),
 
             Self::Type(ty) if !self.is_recursive(env)? => {
-                ty.perform_template_applications(env, previous_applications)?;
+                ty.perform_template_applications(env, previous_applications, checked)?;
                 Self::Type(ty)
             }
 
             Self::Tuple(items) if !self.is_recursive(env)? => Self::Tuple(
                 items
                     .into_iter()
-                    .map(|t| t.perform_template_applications(env, previous_applications))
+                    .map(|t| t.perform_template_applications(env, previous_applications, checked))
                     .collect::<Result<Vec<_>, _>>()?,
             ),
 
             Self::Array(item_t, size) if !self.is_recursive(env)? => Self::Array(
-                Box::new(item_t.perform_template_applications(env, previous_applications)?),
+                Box::new(item_t.perform_template_applications(env, previous_applications, checked)?),
                 size,
             ),
 
@@ -1608,7 +1672,7 @@ impl Type {
             );
             return Ok(false);
         }
-        trace!("Checking if {} equals {}", self, other);
+        // trace!("Checking if {} equals {}", self, other);
 
         let i = i + 1;
 
@@ -1738,7 +1802,7 @@ impl Type {
             }
             (Self::Array(t1, size1), Self::Array(t2, size2)) => {
                 t1.equals_checked(t2, compared_symbols, env, i)?
-                    && size1.clone().eval(env)?.equals(&size2.clone().eval(env)?)
+                    && size1.clone().eval(env)?.equals(&size2.clone().eval(env)?, env)
             }
             (Self::Struct(a), Self::Struct(b)) => {
                 if a.len() != b.len() {
@@ -1806,20 +1870,20 @@ impl Type {
                 // Create a new environment.
                 let mut new_env = env.clone();
                 for ((name1, ty1), (name2, ty2)) in ty_params1.iter().zip(ty_params2.iter()) {
-                    match (ty1, ty2) {
-                        (Some(ty1), Some(ty2)) => {
-                            if !ty1.equals_checked(&ty2, compared_symbols, &new_env, i)? {
-                                return Err(Error::MismatchedTypes { expected: ty1.clone(), found: ty2.clone(), expr: Expr::ConstExpr(self.clone().into()) })
-                            }
-                        }
-                        (None, None) => {}
-                        (Some(ty1), None) => {
-                            return Err(Error::MismatchedTypes { expected: ty1.clone(), found: Self::Type(Type::Any.into()), expr: Expr::ConstExpr(self.clone().into()) })
-                        }
-                        (None, Some(ty2)) => {
-                            return Err(Error::UnexpectedConstParam { found: ty2.clone(), expr: Expr::ConstExpr(self.clone().into()) })
-                        }
-                    }
+                    // match (ty1, ty2) {
+                    //     (Some(ty1), Some(ty2)) => {
+                    //         if !ty1.equals_checked(&ty2, compared_symbols, &new_env, i)? {
+                    //             return Err(Error::MismatchedTypes { expected: ty1.clone(), found: ty2.clone(), expr: Expr::ConstExpr(self.clone().into()) })
+                    //         }
+                    //     }
+                    //     (None, None) => {}
+                    //     (Some(ty1), None) => {
+                    //         return Err(Error::MismatchedTypes { expected: ty1.clone(), found: Self::Type(Type::Any.into()), expr: Expr::ConstExpr(self.clone().into()) })
+                    //     }
+                    //     (None, Some(ty2)) => {
+                    //         return Err(Error::UnexpectedConstParam { found: ty2.clone(), expr: Expr::ConstExpr(self.clone().into()) })
+                    //     }
+                    // }
                     // In the new environment, bind the two type parameters to the same type.
                     let combined_name = format!("{name1}+{name2}");
                     let combined_ty = Self::Unit(combined_name, Box::new(Type::Any));
@@ -1875,7 +1939,7 @@ impl Type {
 
             (Self::Apply(poly, ty_args), b) | (b, Self::Apply(poly, ty_args)) => {
                 Self::Apply(poly.clone(), ty_args.clone())
-                    .simplify_until_concrete(env)?
+                    .simplify_until_concrete(env, false)?
                     .equals_checked(b, compared_symbols, env, i)?
             }
 
@@ -1883,8 +1947,8 @@ impl Type {
             (Self::ConstParam(cexpr), other) | (other, Self::ConstParam(cexpr)) => {
                 cexpr.get_type(env)?.equals_checked(other, compared_symbols, env, i)?
             },
-            _ => {
-                // trace!("{} is not equal to {}", a, b);
+            (a, b) => {
+                // error!("{} is not equal to {}", a, b);
                 false
             }
         })
@@ -1958,7 +2022,7 @@ impl Type {
             Type::Unit(_unit_name, t) => t.get_member_offset(member, expr, env),
 
             Type::Apply(_, _) | Type::Poly(_, _) => {
-                let t = self.simplify_until_concrete(env)?;
+                let t = self.simplify_until_concrete(env, true)?;
                 t.get_member_offset(member, expr, env)
             }
 
@@ -2065,7 +2129,7 @@ impl Type {
             }
 
             Type::Apply(_, _) | Type::Poly(_, _) => {
-                let t = self.simplify_until_concrete(env)?;
+                let t = self.simplify_until_concrete(env, true)?;
                 trace!("Simplified {self} to {t}");
                 t.type_check_member(member, expr, env)
             }
@@ -2123,8 +2187,16 @@ impl Simplify for Type {
             | Self::Char
             | Self::Bool
             | Self::Cell
-            | Self::Enum(_)
-            | Self::Poly(_, _) => self.clone(),
+            | Self::Enum(_) => self.clone(),
+            Self::Poly(mut ty_params, body) => {
+                for (name, ty) in &mut ty_params {
+                    // *ty = ty.map(|ty| ty.simplify_checked(env, i));
+                    if let Some(ty) = ty {
+                        *ty = ty.clone().simplify_checked(env, i)?;
+                    }
+                }
+                Self::Poly(ty_params, body)
+            }
             Self::Pointer(mutability, inner) => {
                 Self::Pointer(mutability, Box::new(inner.simplify_checked(env, i)?))
             }
@@ -2222,7 +2294,7 @@ impl Simplify for Type {
                 Self::Apply(Box::new(poly.simplify_checked(env, i)?), ty_args)
             }
         };
-        warn!("Simplified {_s} into {result}");
+        // warn!("Simplified {_s} into {result}");
         Ok(result)
     }
 }
diff --git a/src/lir/types/size.rs b/src/lir/types/size.rs
index ec01bb83..abc5812c 100644
--- a/src/lir/types/size.rs
+++ b/src/lir/types/size.rs
@@ -166,7 +166,7 @@ impl GetSize for Type {
                     return Ok(size);
                 }
 
-                let result = self.clone().simplify_until_concrete(env)?;
+                let result = self.clone().simplify_until_concrete(env, false)?;
 
                 result.get_size_checked(env, i)?
             }