diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index a35dc0a8f3..fa520111d4 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -60,8 +60,9 @@ partial def toPosition (fmap : FileMap) (pos : String.Pos) : Position :=
       loop 0 (ps.size -1)
     else
       -- Some systems like the delaborator use synthetic positions without an input file,
-      -- which would violate `toPositionAux`'s invariant
-      ⟨1, pos⟩
+      -- which would violate `toPositionAux`'s invariant.
+      -- Can also happen with EOF errors, which are not strictly inside the file.
+      ⟨lines.back, pos - ps.back⟩
 
 end FileMap
 end Lean