[ailang-parse] ailang verify: SMT sort mismatch on a record type is reported as ERROR where every comparable limitation is reported as skipped

[sunholo-voight-kampff]

ailang verify reports a hard ERROR where it means "cannot encode this shape",
for one specific case: a record type it cannot declare an SMT sort for.

What happens

! ERROR emptyParseState
  Z3 error (exit exit status 1): (error "line 18 column 315: unknown constant
  mk_MdParseState ((Seq Int) String (Seq Int) Bool (Seq Int) Bool (Seq Int) (Seq Int))
  declared: (declare-fun mk_MdParseState ((Seq Block) String ...

The generated SMT-LIB declares mk_MdParseState with one signature and then
applies it with another — (Seq Block) in the declaration against (Seq Int)
at the call site — so Z3 rejects the term outright.

The function is unremarkable; it is a record constructor with a contract that
only talks about list lengths:

type MdParseState = {
  blocks: [Block], listItems: [string], listOrdered: bool,
  tableRows: [[string]], textLines: [string],
  codeLines: [string], inCode: bool, codeLang: string
}

pure func emptyParseState() -> MdParseState
  ensures {
    listLength(result.blocks) == 0 &&
    listLength(result.listItems) == 0 &&
    listLength(result.tableRows) == 0 &&
    listLength(result.textLines) == 0
  }
= { blocks: [], listItems: [], listOrdered: false, tableRows: [],
    textLines: [], codeLines: [], inCode: false, codeLang: "" }

Repro: docparse/services/markdown_parser.ail in sunholo/ailang-parse at
v0.33.0, via ./bin/docparse --prove (which runs ailang verify over every
module). It reproduces on the previous 5-field version of the same record too,
so widening it is not the trigger — this is not a regression, just a case that
has always been misreported.

Why it is worth a small fix

Everything else the verifier cannot encode is reported as skipped, with a
helpful hint:

Hint: Z3 has no SMT-LIB encoding for std/string.split. Either remove its
use, refactor to use a supported builtin, or narrow the function's contracts.
Hint: Cross-function verification cannot encode parametric ADTs ...

Those are honest: the contract was not checked, and here is why. This one is
classified as an ERROR and prints a raw Z3 exit status plus a fragment of
SMT-LIB, which reads like the contract FAILED — a verification result — rather
than like the tool declining to try. In a 38-module --prove run over 28+
contracts, that is the one line that looks alarming and is not.

Two things would help, in order:

1. Classify an SMT sort/arity mismatch as skipped with the existing style
   of hint ("cannot encode a record containing an ADT-typed field"), not as an
   error. Same treatment as the parametric-ADT case it resembles.
2. If the mismatch is a bug rather than a limitation — the declaration says
   (Seq Block) and the application says (Seq Int), which looks like the
   record's field sorts are being derived twice and disagreeing — then the
   record encoding may be fixable and the contract actually verifiable.

Not blocking: --prove still exits usefully and every other contract is
verified or skipped normally. It is purely that the one output line most likely
to be read as "your contract is broken" is the one that means "I could not
build the sort".

Environment: AILANG v0.33.0-41-g65f287107-dirty, Z3 4.15.4 64-bit, macOS arm64.

---

Binary info (auto-attached):
ailang version: v0.33.0-41-g65f287107-dirty
binary md5: bfbdf899a56255f42732538abd873b5a
binary path: /Users/mark/.local/bin/ailang
git commit: 65f2871

---

Reported by: ailang-parse via ailang messages