Solver and Migration

Written: 2026-10-14

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
• Narrowing and Guards
• Casts and Assertions

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 intro frames this as gradual checking with inference plus annotations. The 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, 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.

--!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. The 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.

--!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.

--!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. 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.

--!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.

--!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.

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 and summarized in Modes. 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.

--!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.

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.

Put this Script in ServerScriptService.

--!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.

--!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.

--!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.

--!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.

--!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.

--!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.

--!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.

Solution 1

Put this Script in ServerScriptService.

--!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.

Solution 2

Put this Script in ServerScriptService.

--!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.

Solution 3

Put this Script in ServerScriptService.

--!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.

Solution 4

Put this ModuleScript in ReplicatedStorage.

--!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.

Solution 5

Put this Script in ServerScriptService.

--!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.