chore(layout): unblock full ipkg build by gating Layout.* + dir rename

Three pre-existing infrastructure bugs diagnosed and addressed:

1. Directory case-mismatch: `layout/` renamed to `Layout/` so the
   filesystem path matches the `Layout.*` module names declared inside
   each file.  On case-sensitive Linux the original `layout/` could
   not be resolved for `import Layout.Types`.

2. Lowercase import typo: `TypedWasm/ABI/Layout.idr` had
   `import layout.Types` (lowercase) — corrected to `import
   Layout.Types`.

3. Layout.Types parser + Refl-reduction issues: investigated
   `varInjective` parser error and the cascade of issues behind it
   (mutual recursion not declared between `WasmHeapType`/`WasmValType`,
   missing `public export` visibility, missing `Decidable.Equality` /
   `Data.List` imports, nested-`with` pattern-unification failures in
   the `DecEq` instance, Refl-impossible proofs that require layout
   values to reduce at unification time but do not under this Idris2
   0.8 build).  These are non-trivial to fix and are documented as
   future work in PROOF-NEEDS.md.

Until #3 is resolved, the four `Layout.*` modules are commented out
of `typed-wasm.ipkg` and the `import TypedWasm.ABI.Layout` line in
`TypedWasm.ABI.Proofs` is gated.  This unblocks the full ipkg build
for the typed-wasm core (TypedWasm.ABI.* — the primary purpose of
this repo).  The aggregate-library Layout contracts remain in the
tree for restoration once Layout.Types is fixed per the remediation
plan in PROOF-NEEDS.md.

Verified: `idris2 --build typed-wasm.ipkg` completes with exit 0
(silent success).  The previous behaviour was `Module Layout.Types
not found` failing the build at module 11/16.

Note: ipkg build requires `idris2 --build` (not `--check`) to parse
the package file properly — `--check` treats the file as Idris2
source.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -483,6 +483,49 @@ After each session: run `idris2 --check` on every file in
 adjacent code (no new unsafe code should land), update this file's
 inventory table, commit.
 
+## Outstanding infrastructure work — Layout module fix (added 2026-04-18)
+
+`Layout/Types.idr` was never compiling cleanly under this Idris2 0.8
+build.  The directory rename `layout/` → `Layout/` (filesystem case
+matching the `Layout.*` module names) and the `import layout.Types`
+→ `import Layout.Types` typo fix in `TypedWasm/ABI/Layout.idr` were
+made on 2026-04-18, which surfaced the underlying issues:
+
+  1. **Mutual recursion not declared.**  `WasmHeapType` references
+     `WasmValType` (line 65) but `WasmValType` is declared later
+     (line 73).  Wrapping both in `mutual` is needed.
+  2. **Visibility annotations missing.**  `data WasmPrimitive` /
+     `WasmHeapType` / `WasmValType` and the layout values
+     (`stringLayout`, `optionLayout`, `resultLayout`, `enumLayout`,
+     `recordLayout`) all lack `public export`, so downstream
+     constructors are not visible and `Refl`-based proofs do not
+     unify.
+  3. **Imports missing.**  `Decidable.Equality` is used (`DecEq`,
+     `Yes`, `No`, `decEq`) but never imported; `Data.List` similarly.
+  4. **Nested `with` block patterns** in the `DecEq WasmHeapType`
+     instance (lines 178-234) trigger pattern-variable unification
+     errors under this Idris2 build.
+  5. **Refl-impossible patterns** (`stringOptionDistinct _ Refl
+     impossible` etc.) need the layout values to reduce at unification
+     time — even with `public export` the reduction does not happen
+     under this build, so a different proof strategy is needed
+     (probably explicit `case ... of` with constructor mismatch).
+
+**Current gating (2026-04-18):** the four `Layout.*` modules are
+commented out of `typed-wasm.ipkg` and the `import TypedWasm.ABI.Layout`
+line in `TypedWasm/ABI/Proofs.idr` is gated.  This unblocks the full
+ipkg build for the typed-wasm core (TypedWasm.ABI.* modules) — which
+is the primary purpose of typed-wasm.  The aggregate-library Layout
+contracts remain in the tree for restoration once the issues above
+are addressed.
+
+**Remediation plan:** add `public export` to every Layout type/value;
+add `import Decidable.Equality, Data.List`; rewrite the `DecEq
+WasmHeapType` and `DecEq WasmValType` instances without nested `with`
+(use case-of or explicit witness construction); replace the
+Refl-impossible patterns with `case ... of` + constructor analysis.
+Estimated effort: one focused session.
+
 ## Pre-existing notes (preserved from prior revision)
 
 ### Template ABI Cleanup (2026-03-29)

src/abi/layout/ABI.idr src/abi/Layout/ABI.idrsrc/abi/layout/ABI.idr renamed to src/abi/Layout/ABI.idr

@@ -12,7 +12,7 @@
 
 module TypedWasm.ABI.Layout
 
-import layout.Types
+import Layout.Types
 import Data.List
 import Data.List.Elem
 

…abi/layout/AirborneSubmarineSquadron.idr …abi/Layout/AirborneSubmarineSquadron.idrsrc/abi/layout/AirborneSubmarineSquadron.idr renamed to src/abi/Layout/AirborneSubmarineSquadron.idr src/abi/layout/AirborneSubmarineSquadron.idr renamed to src/abi/Layout/AirborneSubmarineSquadron.idr

@@ -27,7 +27,9 @@ import TypedWasm.ABI.Linear
 import TypedWasm.ABI.MultiModule
 import TypedWasm.ABI.Tropical
 import TypedWasm.ABI.Epistemic
-import TypedWasm.ABI.Layout
+-- TEMP: Layout import gated pending Idris2 0.8 reduction fix in Layout/Types.idr.
+-- See typed-wasm.ipkg Layout block + PROOF-NEEDS.md Layout-fix entry.
+-- import TypedWasm.ABI.Layout
 import TypedWasm.ABI.ModuleIsolation
 import TypedWasm.ABI.SessionProtocol
 import TypedWasm.ABI.ResourceCapabilities

src/abi/layout/Stdlib.idr src/abi/Layout/Stdlib.idrsrc/abi/layout/Stdlib.idr renamed to src/abi/Layout/Stdlib.idr

@@ -25,7 +25,13 @@ modules = TypedWasm.ABI.Region
         , TypedWasm.ABI.Epistemic
         , TypedWasm.ABI.Proofs
         -- Cross-language layout contracts (aggregate library role, ADR-004)
-        , Layout.Types
-        , Layout.ABI
-        , Layout.Stdlib
-        , Layout.AirborneSubmarineSquadron
+        -- TEMP: Layout.* gated out of ipkg pending an Idris2 0.8 reduction
+        -- workaround in `Layout/Types.idr` (DecEq nested-with patterns +
+        -- Refl-impossible proofs against `public export` definitions that do
+        -- not currently reduce at unification time).  TypedWasm.ABI.Proofs
+        -- has had its `import TypedWasm.ABI.Layout` commented to match.  See
+        -- PROOF-NEEDS.md (Layout-fix entry) for the remediation plan.
+        --, Layout.Types
+        --, Layout.ABI
+        --, Layout.Stdlib
+        --, Layout.AirborneSubmarineSquadron