ch:type-operators: ch:type-operators

Problem and result. Infer finite constructor kinds, compute a direct closed double power, expose the application-headed kind needed by dmap, and reject an ill-kinded application and distinct normal heads.

Representation. Represent kinds and constructors as separate trees and make kind lookup option-valued. Higher-order abstract syntax would shorten binders, but an explicit tree supports deterministic alpha-normalization and printing.

First complete version. Implement $\mathsf{Ty}$, kind arrows, constructor constants, and application. Application checks the argument kind before returning the codomain kind.

Remaining cases. Add constructor abstraction, an explicit $\mathsf{Comp}$ node with beta-normalization below binders, and term checking with conversion by alpha-equivalent normal forms. Keep kind preservation as a checked invariant of normalization.

A failing version. Treating the failed kind lookup of an ill-kinded application as a success changes its combined rejection line to FAIL. The mutation still typechecks.

Acceptance test. Require the four named lines, the exact summary, mutation rejection, and an empty audit.

Mathematical boundary. The finite run illustrates kind checking and one closed normalization. It does not implement term-level checking, or prove confluence, normalization, or decidability.