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

Closed

dpmills wants to merge 15 commits into

mainfrom

dmills/type-operators

Commits on Aug 10, 2026

Type functions: state a relationship between type variables other than subtyping
dpmills
committed
5e6d673
Freshening asks a different question than `type_level`, so it needs its own
dpmills
committed
940d86b
`SharedHole`: let lowering state that two type positions are the same
dpmills
committed
04e9937
Retire `CommonBase`: an operand requirement belongs in the result rule
dpmills
committed
ea23441
The resolution memo caches one answer per variable, not one per reach set
dpmills
committed
57ffd42
Delete the resolution memo and the graph-generation counter it needed
dpmills
committed
9defc2b
An unreduced application contributes nothing to a specialization key
dpmills
committed
81a6c32
Docs: reconcile with what the machinery actually is now
dpmills
committed
d5903ce
Law 3 is totality, not coarsening — and drop the retired design from the docs
dpmills
committed
8a04d28
A rule declares whether it can answer through a cycle
dpmills
committed
c99c4f4
The cut at a cycle is an unrolling, not an iteration
dpmills
committed
a2135fe
Pin the typing of a register that reads itself
dpmills
committed
a891bf3
State the group-by key relation about the group-by, not about its binder
dpmills
committed
69656d5
Docs: cut §4.7's duplication of `reduce.rs`, and record `SharedHole`
dpmills
committed
b9daafe
Arithmetic checks its operands' base, not just that they agree
dpmills
committed
96f06fb