diff --git a/tests/consts.rs b/tests/consts.rs
new file mode 100644
index 00000000..c6d324d2
--- /dev/null
+++ b/tests/consts.rs
@@ -0,0 +1,183 @@
+use formality::test_program_ok;
+use formality_macros::test;
+
+#[test]
+fn test_ok() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+                trait Bar<const C> where [type_of_const C is u32] {}
+
+                impl<const C> Foo<const C> for u32 where [type_of_const C is bool] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+fn test_holds() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+
+                impl<> Foo<const true> for u32 where [] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+fn test_mismatch() {
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "check_trait_impl(impl <> Foo < const 42_(rigid (scalar u32)) > for (rigid (scalar u32)) where [] { })",
+                source: "failed to prove {Foo((rigid (scalar u32)), const 42_(rigid (scalar u32)))} given {}, got {}",
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+
+                impl<> Foo<const 42_u32> for u32 where [] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+fn test_generic_mismatch() {
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "check_trait_impl(impl <const> Foo < const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar u32))] { })",
+                source: "failed to prove {Foo((rigid (scalar u32)), const !const_1)} given {@ ConstHasType(!const_1 , (rigid (scalar u32)))}, got {}",
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+
+                impl<const C> Foo<const C> for u32 where [type_of_const C is u32] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+fn test_trait_with_const() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+
+                trait Bar<ty T> where [T: Foo<const true>] {}
+
+                impl<> Foo<const true> for u32 where [] {}
+                impl<> Bar<u32> for u32 where [] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+fn test_trait_with_generic_const() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+
+                trait Bar<ty T, const C> where [T: Foo<const C>, type_of_const C is bool] {}
+
+                impl<const C> Foo<const C> for u32 where [type_of_const C is bool] {}
+                impl<const C> Bar<u32, const C> for u32 where [type_of_const C is bool] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+/// This test is the short version of `test_holds`, skipping
+/// substituting and directly going to a rigid constant.
+fn test_rigid_const_bound() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<> where [type_of_const true is bool] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+/// This test is the short version of `test_generic_mismatch`, skipping
+/// substituting and directly going to a wrong constant.
+fn test_nonsense_rigid_const_bound() {
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "check_trait(Foo)",
+                source: Error {
+                    context: "prove_where_clause_well_formed(type_of_const 0_(rigid (scalar bool)) is (rigid (scalar u32)))",
+                    source: "failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(0_(rigid (scalar bool)) , (rigid (scalar u32)))}, got {}",
+                },
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<> where [type_of_const true is u32] {}
+            }
+        ]",
+    ));
+}
+
+#[test]
+/// This test is wrong, but it's also not something rustc ever generates.
+/// Types on const generics only get exactly one `type_of_const` bound.
+fn test_multiple_type_of_const() {
+    expect_test::expect![[r#"
+        Ok(
+            (),
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool, type_of_const C is u32] {}
+            }
+        ]",
+    ));
+}