SafeMCP: idris2 --check does not terminate on 3 modules (same mechanism as the SafePolicy stall)

[hyperpolymath]

Summary

idris2 --check never terminates on three modules of the SafeMCP family. Each was
allowed to run 150s before being killed; none produced a diagnostic.

• src/Proven/SafeMCP.idr
• src/Proven/SafeMCP/Proofs.idr
• src/Proven/FFI/SafeMCP.idr

These are the only 3 stalls in a full 379-file per-file check census (233 clean, 143
failing with named diagnostics, 3 stalls).

This is the same mechanism as the SafePolicy stall

SafePolicy.idr exhibited an identical non-termination and has now been diagnosed. The
signature is:

data X : T -> Type where
  MkX : f y = <Bool literal> -> X y

under %default total, where f is non-structurally recursive (or otherwise not
provably total). The elaborator is asked to work with a type-level equality whose LHS it
cannot reduce and cannot show terminating.

SafeMCP.idr (241 lines, %default total at L15) ends with four such declarations:

data InjectionFree : String -> Type where
  MkInjectionFree : hasInjectionPattern s = False -> InjectionFree s

data SafeToolCall : ToolCall -> Type where
  MkSafeToolCall : areParamsSafe call = True -> SafeToolCall call

data ValidToolName : ToolName -> Type where ...

data AcceptableSize : ToolResult -> Type where
  MkAcceptableSize : isResultSizeOk result = True -> AcceptableSize result

with

hasInjectionPattern s = let lower = toLower s in any (\pat => isInfixOf pat lower) injectionPatterns
areParamsSafe call    = all (\(_, conf) => conf == None || conf == Low) (validateToolParams call)

The cure that worked on SafePolicy

Make the descent syntactic — a mutual pair that pattern-matches the record
constructor — so the size-change checker can see it. Passing the recursive call as a
function argument to concatMap/any/all gives the checker an opaque higher-order
call and it gives up.

Do NOT reach for assert_total. It silences the totality error while leaving the
elaborator the same non-total definition to diverge on. Measured: removing %default total entirely did not fix the SafePolicy stall (still 300s, rc=124).

Evidence

Per-file census and attribution:

• .claude/forensics/proven-idr-file-census-2026-08-27.txt
• .claude/forensics/proven-idr-defect-attribution-2026-08-27.txt

Measured 2026-08-27 against c83c7bf3.