SharedHole: let lowering state that two type positions are the same

[dpmills]

A groupby's key type is its key function's codomain, and the lowered shape relates them nowhere: __gb_k's only occurrence is as an operand of the partition predicate's ==, so the key's type could only arrive backwards through that comparison — making group-by key inference depend on an operator's internals.

Type::SharedHole(id) lets lowering state the relation outright: a Hole with an identity, every occurrence of one id normalizing to the same inference variable. It is transient exactly as Hole is, and groups with it everywhere outside normalize_annotation.

groupby stamps one id on the key application and on its own data_fun annotation's domain — the positions the claim is about, not the binder this desugaring invented. That also makes the edge directional for free: bind_annotation records inferred <: ann and a function is contravariant in its domain, so keys flow into the domain rather than being forced equal to it.

symbolic does not render annotations, so test_lower_groupby cannot show the relation; test_groupby_key_type_comes_from_the_key_function pins it.

[dpmills]

This change is part of the following stack:

• Freshening asks a different question than type_level, so it needs its own #71
  • SharedHole: let lowering state that two type positions are the same #72 ◀
    • Traits: state what an operator requires of its operands, not that they are the same #73
      • 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
                • constrain_go asserts the uniquely-keyed invariant it rests on #74
                  • Update the value-Case fan-out's prose to the DisjointJoin it builds #75
                  • Canonicalize each arrow's Pi binder as the solver flattens types #76
                  • Hold a refined type's refinements in one unordered set instead of nested layers #77
                  • Derive a Cast's refinements from its term instead of overwriting the target #78
                  • Add a Lean model of the CCL type system and fuzz the solver against it #79

_{Change managed by git-spice.}