diff --git a/prism-compiler/programs/type_check_fails/infinite_type.test b/prism-compiler/programs/type_check_fails/infinite_type.test
new file mode 100644
index 00000000..f6109f15
--- /dev/null
+++ b/prism-compiler/programs/type_check_fails/infinite_type.test
@@ -0,0 +1 @@
+_ -> #0 #0 (#0 Type)
\ No newline at end of file
diff --git a/prism-compiler/src/lang/display.rs b/prism-compiler/src/lang/display.rs
index 36ca857e..664944d4 100644
--- a/prism-compiler/src/lang/display.rs
+++ b/prism-compiler/src/lang/display.rs
@@ -65,7 +65,7 @@ impl TcEnv {
                 write!(w, " ")?;
                 self.display(b, w, Base)?;
             }
-            PartialExpr::Free => write!(w, "_")?,
+            PartialExpr::Free => write!(w, "{{{}}}", i.0)?,
             PartialExpr::Shift(..) => unreachable!(),
         }
 
diff --git a/prism-compiler/src/lang/error.rs b/prism-compiler/src/lang/error.rs
index 610ec54f..676a381d 100644
--- a/prism-compiler/src/lang/error.rs
+++ b/prism-compiler/src/lang/error.rs
@@ -15,7 +15,7 @@ pub enum TypeError {
         arg_type: UnionIndex,
     },
     IndexOutOfBound(UnionIndex),
-    InfiniteType(UnionIndex),
+    InfiniteType(UnionIndex, UnionIndex),
     BadInfer {
         free_var: UnionIndex,
         inferred_var: UnionIndex,
@@ -23,9 +23,9 @@ pub enum TypeError {
 }
 
 impl TcEnv {
-    pub fn report(&mut self, error: &TypeError) -> Report<'static, Span> {
+    pub fn report(&mut self, error: &TypeError) -> Option<Report<'static, Span>> {
         let report = Report::build(ReportKind::Error, (), 0);
-        match error {
+        Some(match error {
             TypeError::ExpectType(i) => {
                 let ValueOrigin::TypeOf(j) = self.value_origins[i.0] else {
                     unreachable!()
@@ -106,9 +106,39 @@ impl TcEnv {
                     .with_label(label_fn)
                     .finish()
             }
-            TypeError::InfiniteType(_) => report.finish(),
+            TypeError::InfiniteType(left, right) => {
+                let (left_span, left_description) = self.label_value(*left)?;
+                let (right_span, right_description) = self.label_value(*left)?;
+
+                report.with_message("Constraint creates an infinite type")
+                    .with_label(Label::new(left_span).with_message(format!("Left side of constraint from {left_description}: {}", self.index_to_sm_string(*left))))
+                    .with_label(Label::new(right_span).with_message(format!("Right side of constraint from {right_description}: {}", self.index_to_sm_string(*right))))
+                    .with_help("If this doesn't obviously create an infinite type, I'm sorry. This is probably because of hidden constraints.")
+                    .finish()
+            },
             TypeError::BadInfer { .. } => report.finish(),
-        }
+        })
+    }
+
+    fn label_value(&self, mut value: UnionIndex) -> Option<(Span, &'static str)> {
+        let mut origin_description = "this value";
+        let span = loop {
+            match self.value_origins[value.0] {
+                ValueOrigin::SourceCode(span) => break span,
+                ValueOrigin::TypeOf(sub_value) => {
+                    assert_eq!(origin_description, "this value");
+                    origin_description = "type of this value";
+                    value = sub_value;
+                }
+                ValueOrigin::FreeSub(v) => {
+                    origin_description = "type of this value";
+                    value = v
+                },
+                ValueOrigin::FreeValueFailure(_) => return None,
+                ValueOrigin::FreeTypeFailure(_) => return None,
+            }
+        };
+        Some((span, origin_description))
     }
 }
 
@@ -119,7 +149,7 @@ pub struct AggregatedTypeError {
 impl AggregatedTypeError {
     pub fn eprint(&self, env: &mut TcEnv, input: &str) -> io::Result<()> {
         let mut input = Source::from(input);
-        for report in self.errors.iter().map(|err| env.report(err)) {
+        for report in self.errors.iter().flat_map(|err| env.report(err)) {
             report.eprint(&mut input)?;
         }
         Ok(())
diff --git a/prism-compiler/src/lang/expect_beq_internal.rs b/prism-compiler/src/lang/expect_beq_internal.rs
index 1ebdecae..b7f1bcb0 100644
--- a/prism-compiler/src/lang/expect_beq_internal.rs
+++ b/prism-compiler/src/lang/expect_beq_internal.rs
@@ -78,9 +78,9 @@ impl TcEnv {
         (i2, s2, var_map2): (UnionIndex, &Env, &mut HashMap<UniqueVariableId, usize>),
     ) -> bool {
         debug_assert!(matches!(self.values[i2.0], PartialExpr::Free));
-
+        
         if self.toxic_values.contains(&i1) {
-            self.errors.push(TypeError::InfiniteType(i1));
+            self.errors.push(TypeError::InfiniteType(i1, i2));
             return true;
         }
 
diff --git a/prism-compiler/tests/type_check.rs b/prism-compiler/tests/type_check.rs
index 16ea6980..e549cd63 100644
--- a/prism-compiler/tests/type_check.rs
+++ b/prism-compiler/tests/type_check.rs
@@ -42,7 +42,9 @@ fn test_fail([test]: [&str; 1]) {
                             env.index_to_sm_string(typ),
                             env.index_to_br_string(typ));
         }
-        Err(_) => return,
+        Err(errs) => {
+            errs.eprint(&mut env, test).unwrap()
+        },
     }
 }