diff --git a/tests/lean/hidingInaccessibleNames.lean b/tests/lean/hidingInaccessibleNames.lean
index ee590f1edc..fffa3cbb52 100644
--- a/tests/lean/hidingInaccessibleNames.lean
+++ b/tests/lean/hidingInaccessibleNames.lean
@@ -5,7 +5,7 @@ def f : (xs : List Nat) → Nat → xs ≠ [] → Nat
 
 set_option pp.inaccessibleNames true in
 def f' : (xs : List Nat) → Nat → xs ≠ [] → Nat
-  | [], _, _ => _
+  | [], _, _ => _ -- TODO: figure out why hyp `Ne (α := List Nat) x✝² []` needs α
   | [a,b], _, _ => _
   | _, _, _ =>  _
 
diff --git a/tests/lean/parserPrio.lean b/tests/lean/parserPrio.lean
index 371e4a06d2..1f3c99ec52 100644
--- a/tests/lean/parserPrio.lean
+++ b/tests/lean/parserPrio.lean
@@ -23,6 +23,8 @@ syntax (name := mySingleton) "[" term "]" : term
 macro_rules (kind := mySingleton)
 | `([$a]) => `(2 * $a)
 
+-- TODO: "ambiguous, possible interpretations" error messages print with
+-- a lot of detail since most mvars have not been resolved yet
 #check [1] -- ambiguous it can be `mySingleton` or the singleton list