diff --git a/TODO.md b/TODO.md
index a295f82..89a9d9a 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,7 +1,6 @@
 
 ## TODO
 
-- [x] `newt/Problem.newt` coverage issues
 - [ ] Maybe make the editor json more compact
 - [ ] Remove erased args from primitive functions
   - But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends
@@ -13,6 +12,7 @@
   - Removes assumptions of hack in Compile.newt, but might not support other backends
   - Alternate solution would be to pull from Prelude and hard code for all backends
   - POper added to physical syntax types, but not implemented
+- [ ] Fix issue with erasure checking: `tests/aside/Quantity.newt`.
 - [x] Remove erased fields from constructor data
 - [ ] Teach magic nat / magic enum about erased args
 - [x] Update LiftLambda.newt for arg removal changes
diff --git a/tests/aside/Quantity.newt b/tests/aside/Quantity.newt
new file mode 100644
index 0000000..1e7b89a
--- /dev/null
+++ b/tests/aside/Quantity.newt
@@ -0,0 +1,14 @@
+module Quantity
+
+import Prelude
+
+
+foo : Nat → Nat
+foo x = x
+
+-- This should fail to compile
+bar : ∀ x. Nat
+bar {x} = foo x
+
+main : IO Unit
+main = printLn $ bar {S Z}