[agda-mcp] get_goal/fill_hole: typecheck in place so library-embedded modules resolve (#66)

agda-dojang/data/fixtures/hier-lib/hier-lib.agda-lib

@@ -0,0 +1,2 @@
+name: hier-lib
+include: src

agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda

@@ -0,0 +1,23 @@
+-- Use.agda
+--
+-- File: agda-dojang/data/fixtures/hier-lib/src/Proofs/Use.agda
+--
+-- Description:
+--   Regression fixture for issue #66: a hierarchically-named module (`Proofs.Use`)
+--   embedded in a library (`hier-lib`) that imports across a sibling directory
+--   (`Widgets.Thing`).  This is the shape that broke the old temp-copy get_goal /
+--   fill_hole path (ModuleDefinedInOtherFile), and that the in-place implementation
+--   must handle.
+--
+--   It deliberately does NOT `open import AgdaDojang.Debug`, so exercising get_goal
+--   on it also tests the transient import injection.
+module Proofs.Use where
+
+open import Agda.Builtin.Nat
+open import Agda.Builtin.Unit
+open import Widgets.Thing
+
+-- A single hole with a local variable in context, mirroring Fixture01's `id x`.
+-- Correct fill: `thing` (a cross-directory Nat).  Ill-typed fill: `tt` (⊤ ≢ Nat).
+useIt : Nat → Nat
+useIt x = {!!}

agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda

@@ -0,0 +1,16 @@
+-- Thing.agda
+--
+-- File: agda-dojang/data/fixtures/hier-lib/src/Widgets/Thing.agda
+--
+-- Description:
+--   A trivial module in the `hier-lib` regression fixture, living under a
+--   top-level directory (`Widgets/`) distinct from the module that imports it
+--   (`Proofs.Use`).  Its only job is to be a cross-directory dependency, so that
+--   type-checking `Proofs.Use` exercises hierarchical include-path resolution.
+--   See issue #66 and agda-mcp/test/Main.hs.
+module Widgets.Thing where
+
+open import Agda.Builtin.Nat
+
+thing : Nat
+thing = 7

agda-mcp/README.md

@@ -185,7 +185,7 @@ Given a file path and hole identifier, return the hole's expected type and its l
 }
 ```
 
-**How it works**.  Injects the `reportGoalCtx` macro into the hole, runs Agda, and parses the `AGDADOJANG_REQ_BEGIN/END` marker block from stderr.
+**How it works**.  Ensures `AgdaDojang.Debug` is imported (injecting the import transiently if the file does not already import it), replaces the hole with the `reportGoalCtx` macro, typechecks the file **in place**, and parses the `AGDADOJANG_REQ_BEGIN/END` marker block.  Checking at the file's real path (rather than a scratch copy) lets hierarchically-named modules embedded in a library resolve normally; the original source is restored after the call.
 
 
 #### `fill_hole`
@@ -218,6 +218,8 @@ Submit a candidate term for a hole and receive typecheck feedback: success (hole
 }
 ```
 
+**How it works**.  Substitutes the candidate into the hole, typechecks the file **in place** (restoring the original afterwards), and reports success — tolerating unsolved metas from the file's other open holes — or the type error.  As with `get_goal`, checking at the real path lets library-embedded modules resolve.
+
 #### `check_file`
 
 Load or reload an Agda file and return all diagnostics — errors, warnings, unsolved metas, and remaining holes.
@@ -407,6 +409,18 @@ tool invocation.  This mirrors how `agda-dojang`'s Python tooling
 **Advantages:** simple, decoupled from Agda's GHC version, reuses all
 existing AgdaDojang macros without modification.
 
+**In-place typechecking.**  All four tools typecheck the file at its real
+path on disk.  `get_goal` and `fill_hole` must alter the source (inject the
+reporting macro, or substitute a candidate), so they patch the file
+transiently and restore it afterwards under `bracket_`.  The original is
+captured and rewritten as raw bytes (`Data.ByteString`), so the file is
+returned byte-for-byte — no encoding or newline round-trip — even if Agda
+errors or the call is interrupted.  Checking in place, rather than against a
+scratch copy, is what lets a hierarchically-named module embedded in a
+library resolve its own name and cross-directory imports the same way it does
+for the developer; an earlier scratch-copy approach failed on such modules
+with `ModuleDefinedInOtherFile` (issue #66).
+
 **Limitations:** each tool call spawns a new Agda process (cold
 typechecking, no persistent state).  This is acceptable for the v0 demo
 and benchmark fixtures, but will need optimization for larger files.