ch:algebraic-subtyping: ch:algebraic-subtyping

Problem and invariant. Implement the finite polar work list. Each step either records an atomic bound, discharges a lattice or rigid case, or replaces one structural constraint by its smaller premises. The result is the five outcomes recorded in appendix E.

Representation and construction. Use one closed recursive type tree and explicit constraint/result datatypes. Separate polar datatypes would enforce the invariant more strongly but duplicate constructors here. Begin with upper and lower atomic cases, storing meet-shaped upper and join-shaped lower bounds. Check a new bound against the opposite accumulated bound. This small checker rejects constraints between two distinct variables because it does not implement the transitive propagation needed to retain them soundly. Add arrow decomposition with the right domain below the left domain and the codomains in their original order. Then add join-left, meet-right, top, bottom, rigid-head, and structural occurs-check cases. Fuel derived from the input-tree size makes the executable recursion total; it is an engineering bound, not the published MLsub termination measure.

Failing version and acceptance. Comparing arrow domains left-to-right implements covariance; returning success immediately for an arrow misses a rigid mismatch nested in its codomain. Dropping successful atomic bounds accepts the inconsistent pair $\mathsf{Int}{\le }_{\mathsf{a}}a,a{\le }_{\mathsf{a}}\mathsf{Bool}$; skipping the occurs traversal admits $a{\le }_{\mathsf{a}}\mathsf{Int}\to a$, which this nonrecursive executable fragment does not implement. The named and hidden tests expose these errors. Require exact output and empty audit. Execution illustrates lemma 19.9; it proves no termination, completeness, or principality theorem.