--- url: /strict-typing/solver-and-migration.md description: How the solver generations differ and how to migrate files gradually. --- # Solver and Migration *Written: {{ $frontmatter.date }}* ## Learning objectives * You state what the solver proves. * You place unknown at the top and never at the bottom. * You separate suppression from any-sprinkling. * You migrate file by file without downgrades. * You name current limits before they bite. ## Prerequisites * [Modes](./modes.md) * [Narrowing and Guards](./narrowing-and-guards.md) * [Casts and Assertions](./casts-and-assertions.md) ## The solver proves assignments fit Each assignment, call, and return claims a fit. The solver checks the claim. The precise rule is constraint checking. The checker infers types, collects constraints from your code, and reports failures as diagnostics. The [luau.org types](https://luau.org/types) intro frames this as gradual checking with inference plus annotations. The [type checking](https://create.roblox.com/docs/en-us/luau/type-checking) guide frames modes as how much proof you demand. An older greedy checker and a newer constraint solver may accept different edge programs and word diagnostics differently. The newer solver reached general availability in November 2025 as default for nocheck and nonstrict with strict opt-in via the Workspace flag, per the [release announcement](https://devforum.roblox.com/t/general-release-luau%E2%80%99s-new-type-solver/4084991), with the old solver supported through 2026. You verify behavior in your Studio, not from memory. You gate on a clear Script Analysis window per touched file. You treat a new diagnostic after a Studio update as a solver change first and a code bug second. Put this Script in ServerScriptService. ```luau --!strict local function double(n: number): number return n * 2 end local got = double(21) ``` This block checks clean. You infer `got` as `number`. The solver proves the arg matches, the return matches, and the binding holds. No runtime check is added. ## Unknown sits on top, never sits at bottom `unknown` accepts everything above proof. `never` holds nothing and proves exhaustiveness below. The precise rule is top and bottom. Every type flows into `unknown`, but `unknown` flows out only through narrowing. No value inhabits `never`, so an impossible branch holds `never`. These roles are defined in [never and unknown](https://rfcs.luau.org/never-and-unknown-types.html). The [luau.org types](https://luau.org/types) intro presents `unknown` as the narrow-first top. Under nonstrict, `unknown` behaves much like `any` and lets more pass. Under strict, `unknown` demands guards. That split is by design for gradual migration. You use `unknown` for untrusted input you plan to narrow. You use `never` for impossible branches and empty cases. You use `any` only at untyped package edges. Put this Script in ServerScriptService. ```luau --!strict local function onlyNumber(raw: unknown): number if typeof(raw) == "number" then return raw end return 0 end local got = onlyNumber(5) ``` This block checks clean. You infer `got` as `number`. The guard moves `unknown` down to `number` on one branch. Without it, arithmetic on `raw` errors. Put this Script in ServerScriptService. ```luau --!strict export type Shape = { kind: "coin", amount: number } | { kind: "gem", count: number } local function label(shape: Shape): string if shape.kind == "coin" then return tostring(shape.amount) elseif shape.kind == "gem" then return tostring(shape.count) else local trap: never = shape return trap end end local got = label({ kind = "gem", count = 2 }) ``` This block checks clean. You infer `got` as `string`. The final `else` holds `never` because both members are handled. That `never` assignment proves you exhausted the union. ## Suppression hides cascades, any hides everything One root error can imply ten follow-on errors. The checker should show the root. The precise rule is internal suppression versus user `any`. The solver suppresses cascading diagnostics that follow from an already-reported failure. That mechanism is defined in [type error suppression](https://rfcs.luau.org/type-error-suppression.html). `any` is different: it suppresses checks on purpose wherever it flows. You rely on the first for readable errors. You avoid the second except at untyped edges. A suppressed cascade can hide a second real bug on the same lines. An `any` leak can hide bugs across the file. You recheck after each fix instead of trusting one pass. You fix the first reported error, then you recheck. You never sprinkle `any` to quiet a file. Put this Script in ServerScriptService. ```luau --!strict export type Box = { coins: number } local box: Box = { coins = 4 } local got = box.coins + 1 ``` This block checks clean. You infer `got` as `number`. One correct shape yields no cascade. Break the literal and the checker reports the shape root first. Later uses stay quiet until you fix it. Put this Script in ServerScriptService. ```luau --!strict local blob: any = { coins = 10 } local got = blob.coins + "bonus" ``` This block may pass the checker while failing at runtime. `any` suppresses the arithmetic check. You fix it by replacing `any` with a record type and guards from [Narrowing and Guards](./narrowing-and-guards.md). ## You migrate one file at a time The project improves file by file. No file slides backward. The precise rule is gradual strictness. You keep the project default strict for new files. You pick one legacy file, add its header, annotate its boundary, narrow its unknowns, and clear its diagnostics. Mode headers and defaults are defined in [type checking](https://create.roblox.com/docs/en-us/luau/type-checking) and summarized in [Modes](./modes.md). You never change a header to nonstrict or nocheck to hide an error. The first files are easy. Boundary modules with remote payloads and generated data take parsers and shared aliases. You budget time for those. Each migrated file protects its neighbors. Shared aliases spread precise shapes. New code starts strict and stays strict. Put this ModuleScript in ReplicatedStorage. ```luau --!strict export type Save = { coins: number } local function load(raw: unknown): Save? if typeof(raw) == "table" then local coins = (raw :: Save).coins if typeof(coins) == "number" then return { coins = coins } end end return nil end local got = load({ coins = 6 }) ``` This block checks clean. You infer `got` as `Save?`. The loader parses unknown input into a precise optional. Callers guard nil. This is the migration pattern for data edges: parse once, check everywhere downstream. ## Limits you respect up front Every checker has edges. Learn them before you rely on it. The precise rule is known gaps. Table-state rules affect growth after sealing. Function-detail checks around packs, arity, and variance produce the longest messages. Engine declaration drift can under-report nilable returns, so you guard lookups even when hover text looks total. Type functions and standard-library detail beyond core inference are larger topics mapped in the course [RFC guides](../rfcs/implemented.md). Solver wording, defaults, and coverage shift with Studio releases. Exact diagnostic strings in these chapters describe meaning; quoted strings come only from fetched docs. Other wording can differ in your Studio, so match on slot types and locations. The consequence is method. You keep repros small. You read the first error first. You isolate the failing assignment in a fresh script before editing the feature. That habit is detailed in [Diagnosing Errors](./diagnosing-errors.md). Put this Script in ServerScriptService. ```luau --!strict export type Pet = { name: string } local pet: Pet = { name = "Pip" } local name = pet.name ``` This block checks clean. You infer `name` as `string`. It is your minimal baseline: one alias, one value, one read. When a larger file fails, you shrink toward this shape until the error disappears, then you regrow. ## Common mistakes Wrong: you sprinkle any to finish migration. Put this Script in ServerScriptService. ```luau --!strict local save: any = { coins = 5 } local total = save.coins + 1 ``` This block may pass while hiding later misuse. You infer `total` as `any`. You fix it with a record plus a parser. ```luau --!strict export type Save = { coins: number } local save: Save = { coins = 5 } local total = save.coins + 1 ``` This fix checks clean. You infer `total` as `number`. Checks stay on downstream. Wrong: you downgrade the header to clear red. Put this Script in ServerScriptService. ```luau --!strict local rate: number = 2 local label = rate + "x" ``` This block errors, which is correct. Changing the header to nonstrict or nocheck would hide it. You fix the value instead. ```luau --!strict local rate: number = 2 local label = tostring(rate) .. "x" ``` This fix checks clean. You infer `label` as `string`. The mode stays strict. Wrong: you fix cascades before the root. Put this Script in ServerScriptService. ```luau --!strict export type Box = { coins: number } local box: Box = { coins = "many" } local got = box.coins + 1 ``` This block errors at the literal first. The addition diagnostic follows from that root. You fix the literal, then you recheck. Editing the addition alone cannot cure the shape. ```luau --!strict export type Box = { coins: number } local box: Box = { coins = 9 } local got = box.coins + 1 ``` This fix checks clean. You infer `got` as `number`. Root first, cascade gone. ## Exercises 1. Show unknown demanding a guard in strict. 2. Prove exhaustiveness with an else-never trap. 3. Replace an any-typed save with a record. 4. Migrate a data edge with a parse-and-return-optional loader. 5. Build a minimal repro baseline for a failing file. ::: details Solution 1 Put this Script in ServerScriptService. ```luau --!strict local function coins(raw: unknown): number if typeof(raw) == "number" then return raw end return 0 end local got = coins(8) ``` This block checks clean. You infer `got` as `number`. Remove the guard and arithmetic on `raw` errors. That contrast is the top-type rule. ::: ::: details Solution 2 Put this Script in ServerScriptService. ```luau --!strict export type Pick = { kind: "a", v: number } | { kind: "b", v: string } local function show(p: Pick): string if p.kind == "a" then return tostring(p.v) elseif p.kind == "b" then return p.v else local trap: never = p return trap end end local got = show({ kind = "a", v = 1 }) ``` This block checks clean. You infer `got` as `string`. The trap holds `never`. Add a third case and the trap errors until handled. ::: ::: details Solution 3 Put this Script in ServerScriptService. ```luau --!strict export type Save = { coins: number } local save: Save = { coins = 5 } local total = save.coins + 1 ``` This block checks clean. You infer `total` as `number`. No `any` remains. Misuse downstream now errors loudly. ::: ::: details Solution 4 Put this ModuleScript in ReplicatedStorage. ```luau --!strict export type Loot = { gems: number } local function parse(raw: unknown): Loot? if typeof(raw) == "table" then local gems = (raw :: Loot).gems if typeof(gems) == "number" then return { gems = gems } end end return nil end local got = parse({ gems = 3 }) ``` This block checks clean. You infer `got` as `Loot?`. The edge parses once. Callers narrow the optional. ::: ::: details Solution 5 Put this Script in ServerScriptService. ```luau --!strict export type Pet = { name: string } local pet: Pet = { name = "Pip" } local name = pet.name ``` This block checks clean. You infer `name` as `string`. You grow from this baseline toward the failing shape to find the breaking line. ::: ## Summary * The solver proves fits from inference plus annotations. * Unknown is the top you narrow. Never is the bottom you use for exhaustiveness. * Suppression trims cascades. Any-adding hides real bugs. * You migrate file by file and never downgrade. * You respect sealing, pack, arity, and drift limits. * Next: [Diagnosing Errors](./diagnosing-errors.md).