399 lines
15 KiB
Markdown
399 lines
15 KiB
Markdown
# ctt.3 — `KindMismatch` retire — Implementation Plan
|
|
|
|
> **Parent spec:** `docs/specs/2026-05-12-ct-tidy.md`
|
|
>
|
|
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
|
|
> to run this plan. Steps use `- [ ]` checkboxes for tracking.
|
|
|
|
**Goal:** Delete the `WorkspaceLoadError::KindMismatch` variant,
|
|
its helper `walk_kind_mismatch`, its dispatch site in
|
|
`validate_classdefs`, its Display arm in `crates/ail/src/main.rs`,
|
|
and the now-stale "dead-but-defensive" doc-comment on the test
|
|
that ratifies the canonical-form-rejection path. Plus two adjacent
|
|
textual-consistency edits surfaced during recon: the
|
|
`validate_classdefs` doc-comment ("Three diagnostics ..." → "Two")
|
|
and a stale `KindMismatch` mention in
|
|
`crates/ailang-check/src/lib.rs:1428`'s 22b.1-era narration.
|
|
|
|
**Architecture:** Pure mechanical deletion across two files in one
|
|
atomic edit pass. The variant deletion and the Display-arm deletion
|
|
form a lockstep producer/consumer pair — both must land before
|
|
`cargo build` is green. The existing green test
|
|
`class_param_in_applied_position_fires_canonical_form_rejection`
|
|
at `crates/ailang-core/src/workspace.rs:1888` stays unchanged; it
|
|
asserts `BareCrossModuleTypeRef`, not `KindMismatch`, so the
|
|
deletion does not affect its body.
|
|
|
|
**Tech Stack:** `ailang-core` (`workspace.rs`), `ail`
|
|
(`main.rs:workspace_error_to_diagnostic`), `ailang-check`
|
|
(`lib.rs` stale-comment reference).
|
|
|
|
**Files this plan creates or modifies:**
|
|
|
|
- Modify: `crates/ailang-core/src/workspace.rs:256-270` — delete
|
|
`KindMismatch` variant + its doc + `#[error(...)]` attribute.
|
|
- Modify: `crates/ailang-core/src/workspace.rs:791-808` — drop
|
|
`kind-mismatch` from the `validate_classdefs` doc-comment
|
|
("Three" → "Two") and delete the dispatch loop body.
|
|
- Modify: `crates/ailang-core/src/workspace.rs:844-867` — delete
|
|
`walk_kind_mismatch` helper + its doc.
|
|
- Modify: `crates/ailang-core/src/workspace.rs:1879-1887` —
|
|
delete the "dead-but-defensive" doc-comment block on
|
|
`class_param_in_applied_position_fires_canonical_form_rejection`.
|
|
The test name alone documents the remaining behaviour.
|
|
- Modify: `crates/ail/src/main.rs:1163-1182` — delete
|
|
`W::KindMismatch { .. } => ...` arm in
|
|
`workspace_error_to_diagnostic`.
|
|
- Modify: `crates/ailang-check/src/lib.rs:1427-1430` — drop the
|
|
`KindMismatch` mention from the 22b.1-era doc-comment block
|
|
(narrates which class-schema diagnostics 22b.1 deferred to 22b.2;
|
|
post-ctt.3, `KindMismatch` is retired entirely).
|
|
|
|
**Design notes (settled pre-plan):**
|
|
|
|
- Stale-comment ref at `lib.rs:1428` is in scope. Reason: the block
|
|
comment narrates iter 22b.1's deferred-to-22b.2 work and names
|
|
three class-schema diagnostics including `KindMismatch`. After
|
|
ctt.3 the diagnostic is retired; leaving the mention is
|
|
archaeological noise that would catch a future `grep KindMismatch`
|
|
unnecessarily and confuse a reader expecting the diagnostic to
|
|
exist.
|
|
- `validate_classdefs` doc-comment at `workspace.rs:791-793` is in
|
|
scope. Reason: the comment claims "Three diagnostics fire from
|
|
here" but after the dispatch-loop deletion only two will. Adjacent
|
|
textual consistency.
|
|
- "Dead-but-defensive" doc-comment at `workspace.rs:1879-1887` is
|
|
deleted entirely (no successor). Reason: the test name
|
|
`class_param_in_applied_position_fires_canonical_form_rejection`
|
|
is self-documenting (it names the input shape, the output
|
|
diagnostic-class, and the canonical-form path); a successor
|
|
rationale doc would be redundant.
|
|
|
|
---
|
|
|
|
### Task 1: Atomic deletion pass
|
|
|
|
**Files:**
|
|
- Modify: `crates/ailang-core/src/workspace.rs` (4 deletion regions)
|
|
- Modify: `crates/ail/src/main.rs:1163-1182` (1 deletion region)
|
|
- Modify: `crates/ailang-check/src/lib.rs:1427-1430` (1 textual edit)
|
|
|
|
All edits land together. Between Step 1 and Step 6 the workspace
|
|
will not compile; this is the same atomic-pass shape ctt.2 used
|
|
(see ctt.2 plan's "Build must end green at Step 8"). `cargo build`
|
|
green at Step 7.
|
|
|
|
- [ ] **Step 1: Delete `WorkspaceLoadError::KindMismatch` variant**
|
|
|
|
Apply Edit to `crates/ailang-core/src/workspace.rs`:
|
|
|
|
`old_string`:
|
|
```
|
|
/// Iter 22b.2: class-schema validation. The class parameter
|
|
/// `f` (e.g. in `class C f { foo : f Int -> f Int }`) is kind
|
|
/// `*` only — it may appear as a `Type::Var` in method
|
|
/// signatures but never as a `Type::Con` head with arguments.
|
|
/// A bare `f` used as a constructor name is a kind-mismatch.
|
|
/// Code: `kind-mismatch`.
|
|
#[error(
|
|
"kind mismatch in class `{class}`: parameter `{param}` is used in applied position \
|
|
inside method `{method}` (Decision 11 axis 5: class params are kind `*` only)"
|
|
)]
|
|
KindMismatch {
|
|
class: String,
|
|
param: String,
|
|
method: String,
|
|
defining_module: String,
|
|
},
|
|
|
|
/// Iter 22b.2: class-schema validation. A class's `superclass.type`
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
/// Iter 22b.2: class-schema validation. A class's `superclass.type`
|
|
```
|
|
|
|
Verifies: variant + its doc + its `#[error]` attribute are all
|
|
gone; the following sibling `InvalidSuperclassParam` immediately
|
|
follows. Surrounding doc preserves the next sibling intact.
|
|
|
|
If the exact `old_string` does not match (e.g. the doc-comment
|
|
wording shifted between recon and execution), the implementer
|
|
expands the `old_string` to a larger surrounding block until the
|
|
match is unambiguous.
|
|
|
|
- [ ] **Step 2: Adjust `validate_classdefs` doc-comment + delete dispatch loop**
|
|
|
|
Apply Edit to `crates/ailang-core/src/workspace.rs`:
|
|
|
|
`old_string`:
|
|
```
|
|
/// Iter 22b.2: class-schema validation. Runs before `build_registry`.
|
|
/// Three diagnostics fire from here: `kind-mismatch`,
|
|
/// `invalid-superclass-param`, `constraint-references-unbound-type-var`.
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
/// Iter 22b.2: class-schema validation. Runs before `build_registry`.
|
|
/// Two diagnostics fire from here: `invalid-superclass-param`,
|
|
/// `constraint-references-unbound-type-var`. The `kind-mismatch`
|
|
/// diagnostic was retired at ctt.3 — the malformed shape now
|
|
/// fires `BareCrossModuleTypeRef` from the canonical-form
|
|
/// validator before `validate_classdefs` runs.
|
|
```
|
|
|
|
Apply Edit to `crates/ailang-core/src/workspace.rs` (delete the
|
|
dispatch loop):
|
|
|
|
`old_string`:
|
|
```
|
|
if let Def::Class(c) = def {
|
|
for method in &c.methods {
|
|
walk_kind_mismatch(&method.ty, &c.param)
|
|
.map_err(|()| WorkspaceLoadError::KindMismatch {
|
|
class: c.name.clone(),
|
|
param: c.param.clone(),
|
|
method: method.name.clone(),
|
|
defining_module: mod_name.clone(),
|
|
})?;
|
|
}
|
|
if let Some(sc) = &c.superclass {
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
if let Def::Class(c) = def {
|
|
if let Some(sc) = &c.superclass {
|
|
```
|
|
|
|
Verifies: the `Def::Class(c)` arm's body now begins directly with
|
|
the `if let Some(sc) = &c.superclass` check; the second
|
|
`for method in &c.methods { ... }` loop (constraint-validation pass)
|
|
at line ~819 stays untouched.
|
|
|
|
- [ ] **Step 3: Delete `walk_kind_mismatch` helper**
|
|
|
|
Apply Edit to `crates/ailang-core/src/workspace.rs`:
|
|
|
|
`old_string`:
|
|
```
|
|
/// Walks a `Type` looking for any `Type::Con { name == param, args
|
|
/// non-empty }`. The class param is kind `*`; appearing as a
|
|
/// constructor with arguments is a kind-mismatch.
|
|
fn walk_kind_mismatch(t: &Type, param: &str) -> Result<(), ()> {
|
|
match t {
|
|
Type::Con { name, args } => {
|
|
if name == param && !args.is_empty() {
|
|
return Err(());
|
|
}
|
|
for a in args {
|
|
walk_kind_mismatch(a, param)?;
|
|
}
|
|
Ok(())
|
|
}
|
|
Type::Fn { params, ret, .. } => {
|
|
for p in params {
|
|
walk_kind_mismatch(p, param)?;
|
|
}
|
|
walk_kind_mismatch(ret, param)
|
|
}
|
|
Type::Forall { body, .. } => walk_kind_mismatch(body, param),
|
|
Type::Var { .. } => Ok(()),
|
|
}
|
|
}
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
```
|
|
|
|
Verifies: the entire helper fn + its doc are gone; the next item
|
|
in the file (`is_primitive_type_name` or its doc) follows
|
|
immediately.
|
|
|
|
If a trailing blank line collapses or doubles, the Boss tidies
|
|
up at commit time — not a plan-step concern.
|
|
|
|
- [ ] **Step 4: Delete "dead-but-defensive" doc-comment on the canonical-form-rejection test**
|
|
|
|
Apply Edit to `crates/ailang-core/src/workspace.rs`:
|
|
|
|
`old_string`:
|
|
```
|
|
/// ct.1: a class whose parameter `f` appears as a `Type::Con`
|
|
/// name (the malformed-but-historically-test-fixture shape used
|
|
/// to trigger `KindMismatch` pre-ct.1) is now caught earlier by
|
|
/// the canonical-type-names validator: `f` is bare,
|
|
/// non-primitive, and not a TypeDef in the owning module, so
|
|
/// `BareCrossModuleTypeRef` fires before `validate_classdefs`
|
|
/// gets a chance to run. The `KindMismatch` path stays in the
|
|
/// codebase as dead-but-defensive code; a future tidy may
|
|
/// retire it.
|
|
#[test]
|
|
fn class_param_in_applied_position_fires_canonical_form_rejection() {
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
#[test]
|
|
fn class_param_in_applied_position_fires_canonical_form_rejection() {
|
|
```
|
|
|
|
Verifies: the 9-line doc-comment is gone; `#[test]` attribute
|
|
remains immediately above the fn declaration; the test body itself
|
|
(asserting `BareCrossModuleTypeRef`) is untouched.
|
|
|
|
- [ ] **Step 5: Delete `W::KindMismatch` Display arm in `main.rs`**
|
|
|
|
Apply Edit to `crates/ail/src/main.rs`:
|
|
|
|
`old_string`:
|
|
```
|
|
W::KindMismatch {
|
|
class,
|
|
param,
|
|
method,
|
|
defining_module,
|
|
} => Some((
|
|
"kind-mismatch",
|
|
format!(
|
|
"kind mismatch in class `{class}`: parameter `{param}` is used in applied \
|
|
position inside method `{method}` (Decision 11 axis 5: class params are kind \
|
|
`*` only)"
|
|
),
|
|
defining_module.clone(),
|
|
Some(serde_json::json!({
|
|
"class": class,
|
|
"param": param,
|
|
"method": method,
|
|
})),
|
|
),
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
```
|
|
|
|
Verifies: the `W::KindMismatch` match arm is gone; the surrounding
|
|
`match` over `W::*` variants stays exhaustive by construction
|
|
(Step 1's variant deletion makes the now-absent arm a non-issue
|
|
for compile-time exhaustiveness).
|
|
|
|
Note: the exact bracket / comma sequence of the deleted arm may
|
|
vary by a trailing comma or semicolon. If the `Edit` call fails
|
|
due to a mismatched terminator, the implementer expands the
|
|
`old_string` to include the preceding sibling-arm's closing
|
|
`),` and the following sibling-arm's opening identifier (e.g.
|
|
`W::InvalidSuperclassParam {`) to anchor unambiguously, then
|
|
adjusts `new_string` to preserve those anchors.
|
|
|
|
- [ ] **Step 6: Drop `KindMismatch` mention from `lib.rs:1428` archaeology comment**
|
|
|
|
Apply Edit to `crates/ailang-check/src/lib.rs`:
|
|
|
|
`old_string`:
|
|
```
|
|
// Iter 22b.1: schema-only landing for class/instance defs.
|
|
// Class-schema validation (KindMismatch, InvalidSuperclassParam,
|
|
// ConstraintReferencesUnboundTypeVar) and instance-body
|
|
// typechecking (with class-method substitution) land in 22b.2.
|
|
```
|
|
|
|
`new_string`:
|
|
```
|
|
// Iter 22b.1: schema-only landing for class/instance defs.
|
|
// Class-schema validation (InvalidSuperclassParam,
|
|
// ConstraintReferencesUnboundTypeVar) and instance-body
|
|
// typechecking (with class-method substitution) land in 22b.2.
|
|
// ctt.3: KindMismatch retired — the malformed-class-param
|
|
// shape now fires BareCrossModuleTypeRef from the canonical-
|
|
// form validator instead.
|
|
```
|
|
|
|
Verifies: the `KindMismatch` token no longer appears in the comment;
|
|
a one-line successor sentence names where the diagnostic lives now.
|
|
|
|
- [ ] **Step 7: Build, confirm no compile errors**
|
|
|
|
Run: `cargo build --workspace`
|
|
Expected: clean build, no errors, no dead-code warnings (the
|
|
`match` on `W::*` in `main.rs:workspace_error_to_diagnostic`
|
|
stays exhaustive; the deleted variant is no longer in the source
|
|
of truth, so no orphan arm to flag).
|
|
|
|
If a compile error surfaces, it will most likely be:
|
|
- A test under `crates/` that references `KindMismatch` by name.
|
|
`grep -rn "KindMismatch\|walk_kind_mismatch" crates/` should
|
|
return zero hits after Step 6; if any hit remains, that site
|
|
is the source of the compile error and needs the same
|
|
treatment (deletion or rewording).
|
|
- A snapshot file that contains the `kind-mismatch` diagnostic
|
|
string. Recon found no such snapshot, but a `find . -name
|
|
'*.snap*' | xargs grep -l kind-mismatch` will surface one if
|
|
present.
|
|
|
|
---
|
|
|
|
### Task 2: Workspace-wide test gate
|
|
|
|
**Files:** (verification only — no edits)
|
|
|
|
- [ ] **Step 1: Verify zero residual `KindMismatch` references**
|
|
|
|
Run: `grep -rn "KindMismatch\|walk_kind_mismatch" crates/ docs/`
|
|
Expected: zero hits in `crates/`. `docs/` may carry historical
|
|
references in journals or archived design docs — those are
|
|
archaeology and stay.
|
|
|
|
If `crates/` still has hits, the deletion was incomplete and
|
|
Task 1 reopens until clean.
|
|
|
|
- [ ] **Step 2: Run the canonical-form-rejection test, confirm GREEN**
|
|
|
|
Run: `cargo test -p ailang-core class_param_in_applied_position_fires_canonical_form_rejection`
|
|
Expected: PASS. The test was already green pre-ctt.3 — the
|
|
deletion does not touch its body, only its doc-comment.
|
|
|
|
- [ ] **Step 3: Run the entire workspace test suite**
|
|
|
|
Run: `cargo test --workspace`
|
|
Expected: all tests pass.
|
|
|
|
If a previously-green test goes red: most plausible cause is a
|
|
test that observed `W::KindMismatch` shape (either in JSON output
|
|
matching `"code": "kind-mismatch"`, or in human-mode output
|
|
matching the variant's `Display` text, or in a Rust-side pattern
|
|
match against the variant). Recon found no such test; if one
|
|
surfaces, inspect and either retire it (if it was pinning the
|
|
now-retired path) or migrate its assertion to
|
|
`BareCrossModuleTypeRef` (the canonical-form-rejection successor).
|
|
|
|
- [ ] **Step 4: Bench scripts deferred to audit**
|
|
|
|
ctt.3 makes zero codegen-relevant edits — the deleted code path
|
|
is workspace-load-time-only and is structurally unreachable
|
|
pre-ctt.3. No bench movement plausibly attributable; the
|
|
milestone-close audit at the end of the ct-tidy milestone
|
|
confirms.
|
|
|
|
---
|
|
|
|
## Acceptance criteria recap (from spec)
|
|
|
|
- `WorkspaceLoadError::KindMismatch`, `walk_kind_mismatch`, its
|
|
dispatch site in `validate_classdefs`, and its `main.rs`
|
|
Display arm are all deleted. ✓ Task 1 Steps 1, 2, 3, 5.
|
|
- The existing test
|
|
`class_param_in_applied_position_fires_canonical_form_rejection`
|
|
still passes, asserting `BareCrossModuleTypeRef`. ✓ Task 2
|
|
Step 2.
|
|
- `cargo build --workspace` clean, no orphan match arms, no
|
|
dead-code warnings. ✓ Task 1 Step 7.
|
|
- `cargo test --workspace` green. ✓ Task 2 Step 3.
|
|
- `grep KindMismatch crates/` returns no hits. ✓ Task 2 Step 1.
|
|
- Adjacent textual-consistency edits (validate_classdefs
|
|
doc-comment "Three"→"Two", lib.rs:1428 archaeology comment)
|
|
are folded in. ✓ Task 1 Steps 2 and 6.
|