match on Bool passes check but codegen rejects it (no if, no working Bool branch) #70

Open
opened 2026-06-02 22:23:28 +02:00 by Brummel · 0 comments
Owner

A match whose scrutinee is a Bool passes ail check (exit 0) but is rejected at code generation:

Error: module `m`: def `countGt`: internal: match on non-ADT scrutinee (got i1); MVP supports only ADTs

Repro. A function that does (match (app gt h 5) (case true (...)) (case _ (...)))gt returns a Bool, and matching on it typechecks but cannot be lowered.

Two problems.

  1. check/codegen inconsistency. ail check accepts a program codegen cannot lower, and the failure is an internal:-prefixed error at build time rather than a clean diagnostic at check time.
  2. No working surface for branching on a Bool. There is no if, and match on Bool does not lower, so the only working path is to bypass Bool entirely and match on compare->Ordering (an ADT). That is non-obvious — a competent author (and a frontier LLM) reaches for gt + match-on-Bool first.

Suggested fix. Either (a) make match on Bool lower (treat its two values as an ADT-style match), or (b) reject it in check with a clear message pointing at compare/Ordering, and/or add an if form. At minimum the error must not be internal:.

Evidence: experiments/2026-05-12-cross-model-authoring/familiar-vs-unfamiliar/task2-countgt/ and format-findings.md.

A `match` whose scrutinee is a `Bool` passes `ail check` (exit 0) but is rejected at code generation: ``` Error: module `m`: def `countGt`: internal: match on non-ADT scrutinee (got i1); MVP supports only ADTs ``` **Repro.** A function that does `(match (app gt h 5) (case true (...)) (case _ (...)))` — `gt` returns a `Bool`, and matching on it typechecks but cannot be lowered. **Two problems.** 1. **check/codegen inconsistency.** `ail check` accepts a program codegen cannot lower, and the failure is an `internal:`-prefixed error at build time rather than a clean diagnostic at check time. 2. **No working surface for branching on a Bool.** There is no `if`, and `match` on `Bool` does not lower, so the only working path is to bypass `Bool` entirely and `match` on `compare`->`Ordering` (an ADT). That is non-obvious — a competent author (and a frontier LLM) reaches for `gt` + match-on-Bool first. **Suggested fix.** Either (a) make `match` on `Bool` lower (treat its two values as an ADT-style match), or (b) reject it in `check` with a clear message pointing at `compare`/`Ordering`, and/or add an `if` form. At minimum the error must not be `internal:`. Evidence: `experiments/2026-05-12-cross-model-authoring/familiar-vs-unfamiliar/task2-countgt/` and `format-findings.md`.
Brummel added the bug label 2026-06-02 22:23:28 +02:00
Sign in to join this conversation.