fix(abi/idris): sound total decidable type equality — Types.idr now typechecks

[hyperpolymath]

Problem

The Idris 2 ABI src/abi/Types.idr never typechecked. Three issues:

1. Module/path — module Types only resolves when checked from its own directory; idris2 --check src/abi/Types.idr from the repo root fails with "Module name Types does not match file name".
2. Unsound decEqTy — all compound types (TyList/TyTuple/TyMap/TyFun) were punted to a wildcard catch-all decEqTy _ _ = No (\case Refl impossible). That's unsound (TyList a = TyList b is inhabited by Refl when a = b) and Idris rejects it under %default total ("not a valid impossible case").
3. Two holes about runtime primitives — widenPreservesSign (whose type was also malformed: Bool in a Type position) and addCommInt, both ?rhs holes that the object logic cannot discharge without believe_me.

Fix

• Added a minimal phronesis-abi.ipkg (no dependencies) so the module has a defined source root and is CI-checkable: idris2 --typecheck phronesis-abi.ipkg.
• Rewrote decEqTy soundly and totally: compound heads decided structurally via constructor injectivity, mutually with a new field-list decider decEqTys (for TyTuple/TyFun); distinct-head off-diagonal pairs enumerated (Idris won't accept Refl impossible under a wildcard).
• Removed the two primitive-arithmetic holes (not part of the type-safety core; keeping them would require a believe_me escape hatch).

Result

$ idris2 --typecheck phronesis-abi.ipkg   # exit 0, under %default total

No holes, no believe_me/assert_*/postulates. The type-safety content — intrinsic Value : PhroTy -> Type, total + sound decEqTy/decEqTys, widen, addSafe — genuinely checks. SPDX header unchanged.

This brings the fourth proof assistant green: Coq + Agda + Lean + Idris all now typecheck.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	0
🟠 High	7
🟡 Medium	23

View findings

[
  {
    "reason": "Action trufflesecurity/trufflehog@main needs attention",
    "type": "unpinned_action",
    "file": "secret-scanner.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "binary_to_term without :safe option -- deserialization attack (1 occurrences, CWE-502)",
    "type": "elixir_send_unsanitised",
    "file": "/home/runner/work/phronesis/phronesis/lib/phronesis/compiler.ex",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Nominal-only SAST in phronesis: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/phronesis/phronesis",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "Repository has 5 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 3 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 3 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 3 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 3 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence