From a9d9919a589adbe096ee2e4e6fdc5c52b4a72fa9 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Wed, 31 Jul 2024 13:18:18 +0300
Subject: [PATCH] [ quote ] Turn off tcinlining when quoting delays

---
 src/Core/Normalise/Quote.idr | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Core/Normalise/Quote.idr b/src/Core/Normalise/Quote.idr
index 798db02de57..6dce4ecd69c 100644
--- a/src/Core/Normalise/Quote.idr
+++ b/src/Core/Normalise/Quote.idr
@@ -217,7 +217,8 @@ mutual
       toHolesOnly : Closure vs -> Closure vs
       toHolesOnly (MkClosure opts locs env tm)
           = MkClosure ({ holesOnly := True,
-                         argHolesOnly := True } opts)
+                         argHolesOnly := True,
+                         tcInline := False } opts)
                       locs env tm
       toHolesOnly c = c
   quoteGenNF q opts defs bound env (NForce fc r arg args)