constrain_go asserts the uniquely-keyed invariant it rests on

[dpmills]

constrain_go's record and variant arms look a key up with iter().find(..), so on a duplicate-keyed product the verdict depends on which copy comes first — and disagrees with the function's own trivial-equality short-circuit, which accepts t <: t where find-first demands Int <: Bool between the duplicates. Nothing in Type enforces uniqueness; the builders merely happen not to violate it. This adds a debug-only check ahead of the short-circuit, since t <: t is the case the two answer differently. No program in the suite trips it, so a builder that starts violating the invariant now fails loudly instead of silently making subtyping depend on incidental structure.

[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.}