Type functions: state a relationship between type variables other than subtyping

[dpmills]

The constraint solver relates type variables in exactly one way: subtyping. α <: β is the only fact it can record. That is enough whenever a rule's result type is one of its input types — max(xs) returns an element, x.f returns the field — because "is one of" is expressible as sharing a lattice position.

It is not enough for a rule whose result is computed from its inputs. Addition is the smallest example: the result of a + b is neither operand.

What went wrong without it

The encoding available was to share a variable: ∀α. α → α → α. A variable carries every lattice dimension, so this states far more than intended, and it is wrong in both directions at once.

Program	Inferred	Should be
\x -> x + 1	{Int | __elem == 1} ⇒ Int	polymorphic in x
y = 1; z = 1; y + z	{Int | __elem == 1}	Int
1 > "a"	Bool, then panics in the interpreter	rejected

The first two are the two polarities of one mistake. Operand occurrences are domains — negative positions, where refinement sets union — so one operand's refinement becomes a requirement on the other. The result occurrence is positive, where refinement sets intersect, so a refinement both operands carry survives onto the result. The second row needs two operands carrying the same refinement (intersecting a set with itself returns it), which is why it stayed hidden.

The mechanism

Type::App { fun: TypeFn, args } is the type "whatever fun computes from args" — 1 + x types as Add({Int | __elem == 1}, α).

An App denotes a type rather than constructing one: Add(Int, Int) is Int, written in a form that does not yet know it. It adds no inhabitants and no subtyping edges to the lattice, so reduction is normalization, and it is transient in the same sense as Infer — every Type that escapes inference is App-free.

Reduction is demand-driven: materializing an App resolves each argument through the ordinary pipeline and applies the rule. Nothing is deposited, so no phase ordering can make the answer wrong. A rule is a pure function of resolved argument types — no inference context, no access to the bound graph — which is also what leaves room for user-declared type schemas on UDFs later.

Four laws make a rule sound: pure, monotone in the subtype order, declares a CycleTolerance, and normalizing. They are stated in src/ccl/infer/solver/reduce.rs with what each buys inference, and summarized in src/ccl/design/type-inference.md, "4.7 Type functions".

A cycle is a recurrence in the program, and a rule says whether it can answer through one

An argument arrives cyclic when resolving it would re-enter the resolution already computing it, which is what a self-read is: x += 1 makes value(x) = join(seed, Add(value(x), 1)), a fixpoint equation, because an accumulator is one. Measured: 1,910 cyclic arguments across the suite, and adding a self-read is exactly what creates them.

So Option<Type> is Arg::Known(_) | Arg::Cyclic — the distinction a rule must reason about is not "absent" but cyclic, and there is no later point at which more is known. TypeFn::cycle_tolerance() declares Any or AllKnown and reduce enforces it centrally, so a rule that cannot answer cannot forget to say so. It is deliberately not per-position: every rule's condition is about how many arguments are cyclic rather than which.

Both of today's rules are Any, for reasons worth keeping apart — a comparison is constant on its domain so a cyclic operand costs nothing, while arithmetic loses the agreement check but keeps a usable type, which is what lets an accumulator have one.

The cut is an unrolling, not an iteration

Traced, one materialization of x := 0; x := x + 1; x reduces Add(⟨cyclic⟩, 1) → Int and then Add(Int, 1) → Int, and stops; x + x reaches three levels because each operand re-enters separately. The depth is fixed by the shape of the program, never by an iteration count, and in every shape measured the outermost frame — the one whose answer becomes the node's type — sees every argument known.

The consequence is the opposite of the familiar one. Because nothing iterates, whatever a rule answers at a cut is what the unrolling carries; there is no later pass that widens it. A rule must already be sound at the cut, not merely improvable. Both current rules are, for free: arithmetic drops to the shared base — the top of the chain the missing operand could have contributed to — and comparison is constant on its domain. A sharper rule that kept what it could see would return whatever a bounded unrolling happened to reach, sound only by accident of how far the program unrolled.

The operand requirement lives in the result rule

An operator's operands are two unrelated scheme variables. Nothing relates them, and nothing needs to: what checks them is the rule that reduces the result.

That works because of one property, which is silent when violated and so is recorded where schemes are defined: a scheme that wants its operands checked must mention them in its result. A rule runs when something materializes the application it belongs to, and an application is materialized only when some node's type reaches it. A scheme's operand variables are nobody's node type — a use records left <: α and right <: β, so α and β are reachable from the operands, but nothing walks from them. The only thing that can reach them is the result.

So 1 + "a" is rejected because the addition's result is Add(α, β); materializing the node runs the rule and finds the conflict. A comparison declaring a bare Bool mentions neither operand, so nothing ever materializes them, the rule never runs, and 1 > "a" types cleanly and then panics. A comparison's result is therefore Compare(kind, α, β), reducing to Bool for operands that share a base and to an error for those that do not.

What that costs

\x -> x + 1 no longer infers x : Int. Its result still resolves — the rule answers from the literal operand — but the parameter is determined by nothing.

That is the honest answer rather than a regression. The lambda works for any two things + accepts, so it is polymorphic in its parameter, and Type has no ∀ to say so. As a program value it is an ambiguous program, rejected downstream exactly as \x -> [x, x] already was. Inferring Int read as precision; it was a single-numeric-type lattice showing through, and it would have become wrong the moment Int + Float → Float existed.

An earlier revision of this branch bought that inference back with a self-referential bound on the scheme's own variables (α <: CommonBase(α, β)), so that resolving one operand pulled the other's base. It is gone: redundant as a guard, wrong as a claim about what makes two values addable, and — as a pull — compensating for two defects elsewhere that are fixed below it. src/ccl/design/type-inference.md, "Why not a bound on the operand variables" records the argument so it is not re-added.

Obligations that are not decidable yet are parked

constrain_go cannot compare an unreduced App against anything: reduction resolves the arguments off the bound graph, and emission runs while that graph is still being built, so an answer read there could be superseded by the next edge.

The obligation is therefore parked rather than dropped. constrain_go records it with the in-flight substitutions applied, require_sub tags it with the node to blame, and InferCtx::check_parked_obligations retries it between emission and coalesce — the point at which every edge the program implies exists. Only fully-determined obligations are checked, which keeps the retry from perturbing the graph it reads: a side still holding a variable is one the program never determined, and coalesce reports that as UnresolvedInfer.

This is what makes (1 + 2) and True and sum(["a" + "b"]) ordinary diagnostics. Accepting the obligation silently let inference return Ok, and the conflict then reached the check_pre_desugar consistency wall, which cannot distinguish a user type error from a compiler bug and panics on both.

InferCtx::constrain_and_claim is the single choke point every emission-time constrain_subtype goes through, with a debug_assert that the solver's park list is empty on the way out — a call that bypassed it would silently drop its obligation, which is the defect parking exists to fix.

The audit of the other operators

Every scheme in the registry was checked against the rule that decides it: sharing a lattice position between an input and the result is right exactly when the operator selects an existing value or merges several — the result then is one of those values, so a fact about it survives — and wrong when the operator computes a new one.

Sum, Neg, Not, Concat and BoolLogic inherit nothing; Max shares its element type and should; final_or_default and the get_prev_* accessors merge; List merges across elements; Proj selects the field, refinement included. Tests pin the table, and half their cases assert a refinement is still present, because dropping it is the same bug from the other side.

CollectionUnion is why type functions coexist with variable sharing rather than replacing it: its codomain is a real join while its domain is a real computation, and no single scheme can say both. It and Proj's FieldOf(ρ, k) are the natural next clients.

Two inference defects this exposed

Both were found by asking why the retired bound appeared to be load-bearing, and both are fixed in their own commits.

groupby never related its key domain to its key function. The lowered shape binds λ __gb_k whose only occurrence is an operand of the partition predicate's ==, so the key's type could only arrive backwards along an operator's operand relation — the wrong place for that fact to come from, and a place this PR deliberately removes. Type::SharedHole(id) lets lowering state the relation directly: a Hole with an identity, where every occurrence of one id normalizes to the same inference variable.

It is carried by the key application and by the domain of the group-by's own data_fun annotation — the two places the claim is actually about. "A partition function's domain is the type of its keys" is a fact about the group-by; __gb_k is a name this lowering invented, and a different encoding of the same construct would not have it. Annotating the domain also makes the edge directional with no new machinery: bind_annotation records inferred <: ann and a function type is contravariant in its domain, so it reduces to key_ty <: ⟨the parameter⟩ — produced keys flow into the domain, rather than the two being forced equal.

One caveat worth knowing: symbolic does not render annotations, so test_lower_groupby's snapshots do not show this relation. test_groupby_key_type_comes_from_the_key_function is what covers it.

Freshening asked type_level a question it does not answer. type_level is predicate-blind by design (it drives extrusion, where refinements are lattice-blind), but freshen_above used it to decide whether a type needs copying. A quantified variable reachable only through a nested refinement's predicate therefore short-circuited, and the specialization clone kept pointing at the definition's own variables — visible as a duplicate specialization, since the clone reached one generalized let through both the freshened variable and the original. Freshening now asks freshen_level, which counts predicates.

The strict wall could not see through an application

Making a result an App surfaced a hole this area already had: typecheck could not catch a corrupted 1 + 2 : String either, and no test noticed because the one test there used a comparison, whose result was still concrete.

Check reconciles a rule-derived type against the recorded one. For an operator scheme that type is a fresh variable whose lower bound is the App, and constrain_subtype treats an unreduced application as opaque, so the bound-closure walk stops there. Check now resolves a rule-derived type that is still a bare variable before reconciling. Narrow on purpose: every other rule rebuilds a ground type from its children, where resolving is the identity.

Errors

A reduction conflict has its own error rather than borrowing IncompatibleBounds, whose rendering is a specific claim ("won't infer an untagged sum from a collision") that is not what happened: each operand is well typed and nothing collided on a variable. Compaction returns a bag of contributions rather than a Result, so a failed reduction rides the position it poisoned (CompactType::reduce_error) and coalesce_compact raises it where a Type is produced — which is a node, with a span.

Prior work

The name is deliberately GHC's. Associated type synonyms (Chakravarty, Keller & Peyton Jones, ICFP 2005) and open type functions (Schrijvers, Peyton Jones, Chakravarty & Sulzmann, ICFP 2008) are the closest analogue; the substantive difference is that GHC's families are open, so the checker must decide entailment between unreduced applications and the rule set needs confluence and termination side conditions. Cambra's set is closed and every rule is normalizing, so there is never an equality to decide between two unreduced applications — reduce, then compare.

Reducing before comparing is the conversion discipline of a dependent type checker (Coquand, An algorithm for type-checking dependent types, 1996), restricted to a closed first-order rule set. Parking a constraint whose reduction is blocked is Agda's constraint postponement (Norell, Chalmers, 2007) at coarser granularity — retried once after emission rather than woken per-solution, which is sound because emission is a single bounded phase.

The lattice underneath is unchanged: MLsub (Dolan & Mycroft, POPL 2017) as presented by Parreaux (ICFP 2020). Because reduction is normalization, a type function adds nothing to it.

Alternatives considered — including named predicate constraints ((SameBase α β) ⇒ …, deferred rather than rejected) — are tabulated in the design doc.

[dpmills]

This change is part of the following stack:

• Monomorphization: key specializations on instantiation identity, not a resolved type #50
  • Type functions: state a relationship between type variables other than subtyping #51 ◀
    • Mutable-variable typing: an honest seed, a fixed history read-through, and a polarity-directed base #52
      • Annotations stop standing in for binder structure, and stop outliving inference #60
        • Four defects in how Mut is typed: message polarity, an unclosable refinement, and op= as a rebind #63
          • A mutable variable read is an explicit operation, not a subtyping rule #64
            • Exact and bounded binder annotations: x: T fixes the type, x <: T bounds it #62

_{Change managed by git-spice.}