Prompt:

See `name = match $names.get(0.U64) {`, it leads to a type mismatch if `.U64` is removed. Can we improve type inference so that U64 is inferred instead of Dec or would that have negative side effects like e.g. worse compile times?
```
❯ ./zig-out/bin/roc temp.roc --no-cache

┌───────────────┐
│ TYPE MISMATCH ├─ The get method on List has an incompatible type. ────────────────────────┐
└┬──────────────┘                                                                           │
 │                                                                                          │
 │  var $names = test_names_2.split_on(",")                                                 │
 │               ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾                                                 │
 └─────────────────────────────────────────────────────────────────────────── temp.roc:6:18 ┘

    The method get has the type:

        List(Str), U64 -> Try(Str, [OutOfBounds, ..])

    But I need it to have the type:

        List(Str), Dec -> [Err([OutOfBounds]), Ok(Str)]


Found 1 error and 0 warnings for temp.roc.
Roc application crashed with this message:

        runtime error
```


Fable (xhigh) Reply
```
 TL;DR

  Yes, this is fixable — it's a scoping hole in the literal-defaulting pass, not a fundamental
  inference limitation, and the fix would have negligible compile-time cost. The real
  trade-off is correctness risk in what is already the most invariant-heavy subsystem in
  Check.zig, not performance.

  Root cause

  I instrumented the defaulting rounds and traced your exact program. The failure needs three
  ingredients working together:

  1. test_names_2 is a top-level value def. Those deliberately never generalize and never run
  literal defaulting of their own — their literals stay open until module finalize so that
  other defs can constrain them. (This is load-bearing: I verified that n = 5 at top level
  correctly infers U8 when another def passes it to a U8 -> U8 function. Defaulting value defs
  eagerly would break that.)
  2. Inside main!, the .split_on dispatch on that still-open var defers, which leaves $names'
  type flex, which makes .get defer too. The U64 constraint on your 0 is trapped behind this
  pending chain.
  3. When main! hits its generalization boundary, the defaulting pass gathers open literals at
  the boundary's rank only. The chain's root (the test_names_2 var, rank 1) is excluded by
  the rank filter, so the machinery that normally handles exactly this case — it partitions
  literals into components and lets the dispatch cascade pin your 0 to U64 — never sees the
  driver. Your 0 looks completely unconstrained, becomes a "lone passive", and commits to the
  canonical default, Dec. At module finalize the chain finally fires and U64 collides with the
  already-committed Dec.

  Proof that the machinery works when scoping doesn't interfere: the identical program with
  1. test_names_2 is a top-level value def. Those deliberately never generalize and never run literal defaulting of their own — their literals
  stay open until module finalize so that other defs can constrain them. (This is load-bearing: I verified that n = 5 at top level correctly
  infers U8 when another def passes it to a U8 -> U8 function. Defaulting value defs eagerly would break that.)
  2. Inside main!, the .split_on dispatch on that still-open var defers, which leaves $names' type flex, which makes .get defer too. The U64
  constraint on your 0 is trapped behind this pending chain.
  3. When main! hits its generalization boundary, the defaulting pass gathers open literals at the boundary's rank only. The chain's root (the
  test_names_2 var, rank 1) is excluded by the rank filter, so the machinery that normally handles exactly this case — it partitions literals
  into components and lets the dispatch cascade pin your 0 to U64 — never sees the driver. Your 0 looks completely unconstrained, becomes a
  "lone passive", and commits to the canonical default, Dec. At module finalize the chain finally fires and U64 collides with the
  already-committed Dec.

  Proof that the machinery works when scoping doesn't interfere: the identical program with "a,b,c" written as a local literal inside main!
  compiles fine — there the quote is in the same universe, the quote-first rule commits it to Str, the cascade fires split_on → get, and 0
  gets U64.

  The bug class is broader than top-level defs: I reproduced it with everything local — a local s = "a,b,c" used through a dispatch chain
  inside a nested lambda hits the same premature Dec, because the lambda's boundary (rank 4) can't see the rank-2 root either. General
  statement: any literal that is an argument of a deferred dispatch chain rooted in an outer scope gets defaulted before the chain can
  constrain it.

  Fix options

  Option 1 — protect chain-reachable literals at the boundary (least invasive). The boundary already computes a "signature-reachable"
  protection set that keeps literals open. Extend the seeding: for every deferred dispatch whose receiver is still flex at an outer rank, add
  the constraint signature's reachable vars to the protected set (the transitive walk, collectReachableVars, already exists and already
  recurses through nested constraint signatures). Your 0 then stays open, generalizes with main!, and gets pinned to U64 when the chain fires
  at finalize — post-generalization pinning by the cascade is already how this machinery works today. One hole to plug: if the chain resolves
  but leaves the literal open (a method with a polymorphic index parameter), finalize skips generalized-rank literals, so these stragglers
  would need a small end-of-finalize sweep to still get their Dec fallback.

  Option 2 — rank adjustment (the classical ML answer). When a dispatch defers on an outer-rank receiver, lower every still-flex var in its
  constraint signature to the receiver's rank. The literal then simply belongs to the outer universe, and the outer boundary/finalize handles
  it with the existing component machinery — including the Dec fallback if the chain never pins it, so no straggler hole. More uniform, but it
  changes generalization decisions: a var that is both signature-reachable and chain-reachable would become shared-monomorphic instead of
  quantified, which is a subtle behavior change to audit.

  Compile-time impact

  Negligible either way. Per boundary this adds one scan of the deferred-dispatch list (the cascade's fixpoint check already iterates it
  repeatedly) plus reachability walks bounded by the pending-chain size. For scale: the boundary already iterates the module's entire
  constraint list every time it runs, just to collect eql edges. No new unification work is created — commits move to a later, better-informed
  point; the total number of commits stays the same or drops.

  The genuine cost is engineering risk: runLiteralDefaultingRounds carries carefully documented order-independence and termination proofs in
  its comments, and any fix must preserve them (Option 1's set-based protection composes naturally with those invariants; Option 2 touches
  ranks, which more code depends on). There are also minor diagnostic questions, like whether a deferred-then-defaulted literal should still
  get the "LITERAL DEFAULTED" leak warning.

  My recommendation would be Option 1 with the finalize straggler sweep. Want me to implement it, or file this analysis as an issue first?
```