From 3e7bc07f19b368804fb4607d8ea708ad457f38db Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 19 Mar 2020 12:08:21 +0100
Subject: [PATCH] fix: FileMap.toPosition: terminate if position is out of
 bounds

---
 src/Init/Lean/Data/Position.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Data/Position.lean b/src/Init/Lean/Data/Position.lean
index f0d0746d0f..04a8b82024 100644
--- a/src/Init/Lean/Data/Position.lean
+++ b/src/Init/Lean/Data/Position.lean
@@ -74,7 +74,13 @@ private partial def toPositionAux (str : String) (ps : Array Nat) (lines : Array
     else toPositionAux b m
 
 def toPosition : FileMap → String.Pos → Position
-| { source := str, positions := ps, lines := lines }, pos => toPositionAux str ps lines pos 0 (ps.size-1)
+| { source := str, positions := ps, lines := lines }, pos =>
+  if ps.size >= 2 && pos <= ps.back then
+    toPositionAux str ps lines pos 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⟩
 
 end FileMap
 end Lean