From 8055815a4187b85af467fdde75de35ef7a549c46 Mon Sep 17 00:00:00 2001
From: Viktor Yudov <me@spcfox.com>
Date: Wed, 4 Dec 2024 15:03:09 +0300
Subject: [PATCH] [ upstream ] Adapt to the changes in idris-lang/Idris2#3415

---
 src/Language/LSP/CodeAction/Utils.idr | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Language/LSP/CodeAction/Utils.idr b/src/Language/LSP/CodeAction/Utils.idr
index 292f6e0..c9ad755 100644
--- a/src/Language/LSP/CodeAction/Utils.idr
+++ b/src/Language/LSP/CodeAction/Utils.idr
@@ -94,7 +94,8 @@ printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do
   pure (relit l ((pack (replicate i ' ')
          ++ show lhs
          ++ " with \{showCount rig}(" ++ show wval ++ ")"
-         ++ maybe "" (\ nm => " proof " ++ show nm) prf
+            -- TODO: remove `the` after fix idris-lang/Idris2#3418
+         ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf
          ++ "\n"))
          ++ showSep "\n" cs)
 printClause l i (ImpossibleClause _ lhsraw) = do