Refinement Types in Scala 3: What You Can Use Today

An order arrives with a quantity of -3. The JSON parses cleanly and the case class builds without complaint, while the test suite stays green because every fixture anyone ever wrote used a positive number. Three services later, the inventory job adds three units back to stock instead of reserving them, and the postmortem traces the problem to a field typed as a plain Int.

Scala 3 refinement types close that gap by putting the rule inside the type itself, so a negative quantity can't exist anywhere past the point where data enters your system. The search results around refinement types are a mess, though. The term means two different things in Scala, native compiler support is still a research prototype, and the tools you can ship today live in libraries. Here is what each piece means and what to use in production right now.

TL;DR

Scala 3 refinement types attach a rule, like "greater than zero," to a type, so invalid values fail at compile time or get rejected once at the system boundary. No released version of Scala 3 has built-in logical refinement types yet. Production teams use the Iron library, written as Int :| Positive, or opaque types with smart constructors, while native compiler support exists as a research prototype that Scala's creator helped design.

Refinement Types in Scala Mean Two Different Things

Scala uses the phrase "refinement type" for two unrelated features, and most confusion about Scala 3 refinement types comes from mixing them up.

A member refinement adds or narrows a member of an existing type. The type Ledger { type Currency = EUR } describes any Ledger whose Currency type member is EUR, so a function that expects a euro ledger will reject a dollar ledger at compile time. Member refinements are a stable part of the language and power structural typing, but member refinements say nothing about which values are valid.

A logical refinement restricts the values a type allows by attaching a predicate. A logical refinement type for positive integers accepts 5 and rejects -3, even though both are ordinary Int values. Verification tools and languages like Liquid Haskell, F*, and Dafny support logical refinements, and Scala developers get the same idea today through libraries.

scala

// Member refinement: narrows a type member, says nothing about values
trait EUR
trait Ledger:
  type Currency
 
val euroLedger: Ledger { type Currency = EUR } = ???
 
// Logical refinement (Iron): restricts which values the type allows
type Quantity = Int :| Positive

The rest of this post covers logical refinements, because logical refinements are the feature that stops bad data.

Why a Refinement Type Beats a require Check

Most Scala codebases already guard their inputs with require calls or if checks at the top of functions. A require check works, but a require check only protects the one function it sits in, and it runs every time that function runs.

scala

def reserve(sku: String, qty: Int): Unit =
  require(qty > 0, "qty must be positive")
  // the caller still sees qty: Int, so every other function has to check again
  ???

The deeper problem is that the parameter type still says Int. Every function that receives the quantity has to decide whether to trust its caller or check again, and over time teams end up with duplicated checks in some places and missing checks in others. Code review has no easy way to tell which places are which.

A refinement type moves the rule into the signature. When a function takes a Quantity instead of an Int, every caller has to supply a value that already passed the positive check, either at compile time or through validation. The check happens once, and every function downstream gets to skip it.

For an engineering org, that shift changes where bugs get caught. Invalid data either fails the build or gets rejected at the edge of the system, instead of surfacing as a production incident three services away from its source. Scala's compiler already does similar work for you through type inference that keeps code clean and safe, and refinement types push that same safety down to the level of individual values.

Four Ways to Use Scala 3 Refinement Types Today

Scala 3 does not ship built-in logical refinement types in any released version. Teams that want refinement types in production choose between four approaches, and each approach trades setup cost against how much the compiler can check.

Approach	Checks literals at compile time	Validates runtime data	Scala versions	Main limitation
Opaque types with smart constructors	No	Yes, inside the constructor	Scala 3	Every type is written and tested by hand
Iron	Yes	Yes, with refineEither and refineOption	Scala 3 only	Arithmetic on refined values returns the plain base type
Refined	Scala 2 only	Yes	Scala 2 and Scala 3	Scala 3 support is runtime only and incomplete
scala.compiletime.ops	Yes	No	Scala 3	Works only on values known during compilation

Opaque types with smart constructors are the zero-dependency option. An opaque type hides the underlying Int behind a new name, and a smart constructor that returns an Option or an Either is the only way to create one. Our Learning Scala series walks through this pattern in modeling money with types. The cost of hand-built opaque types shows up at scale, since ten constrained types mean ten constructors, ten sets of tests, and ten places for the rules to drift apart.

Refined pioneered refinement types in Scala 2, and Refined remains the right choice for codebases that still run on Scala 2. On Scala 3, Refined only supports runtime refinement, because the macros behind its compile-time checks were never ported. Teams planning a Scala 2 to Scala 3 migration should budget for replacing Refined instead of carrying it forward.

The scala.compiletime.ops package performs arithmetic and comparisons on literal types during compilation. Library authors find compiletime.ops useful for building type-level tools, but compiletime.ops can't validate a value that arrives from a request or a database, which rules it out for most application code.

For new Scala 3 work, Iron is the default choice.

How Iron Brings Refinement Types to Scala 3

The Iron library attaches a constraint to a type with the :| operator. The type Int :| Positive reads as "an Int that satisfies Positive," and Iron ships ready-made constraints for numbers, strings, and collections.

scala

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.*
 
type Quantity = Int :| Positive
 
def reserve(sku: String, qty: Quantity): Unit = ???
 
reserve("A-100", 3)   // compiles: 3 is checked during compilation
reserve("A-100", -3)  // compile error: Should be strictly positive

When a value is known at compile time, Iron checks the constraint during compilation. Passing the literal -3 to reserve fails the build with a readable error message, so a bad constant in a config object or a test fixture never reaches a running system.

An Iron refined type is a subtype of its base type, which means a Quantity can go anywhere an Int is expected without any conversion. At runtime, an Iron refined value is just the underlying value with no wrapper object around it, so a refined Int costs no more memory than a plain Int.

Iron's main limitation shows up in arithmetic. Adding two Quantity values produces a plain Int, because the compiler can't prove the sum stays positive without extra help. Iron offers a mechanism called implication for proving relationships between constraints, but refining the result again where it matters is usually the simpler move, since a refined type should mark the values you trust rather than every intermediate number in a calculation.

Where to Validate Refinement Types in a Real System

Compile-time checks only cover literals. Real data arrives at runtime from HTTP requests, message queues, and database rows, and Iron handles those values with refineEither and refineOption.

scala

case class OrderLine(sku: String, qty: Quantity)
 
// Runs once, where raw input enters the system
def parseLine(sku: String, rawQty: Int): Either[String, OrderLine] =
  rawQty.refineEither[Positive].map(qty => OrderLine(sku, qty))
 
// Everything past this point receives an OrderLine and never checks qty again

Refinement types pay off when teams validate once, at the boundary. Decoders, request handlers, and repository layers turn raw input into refined types, and the domain core only ever sees refined values. Iron publishes integration modules for JSON libraries like Circe and ZIO JSON and for database libraries like Doobie and Skunk, so decoding a payload and refining its fields happen in the same step.

Boundary validation also hands code review a clear rule. A raw Int, String, or BigDecimal that represents a business concept inside the domain core is a smell, and reviewers can flag it on sight. Once that rule holds across a codebase, the defensive checks scattered through the core become dead code your team can delete.

The same boundary rule holds up against AI-generated code. When a coding assistant writes a call to a function that takes a Quantity, the compiler rejects a runtime Int the assistant passes without refining it first, so a skipped check fails the build instead of shipping. Refined signatures also put the business rule directly in the type the model reads, and the resulting compile errors give agentic tools a fast, precise signal to correct their own output. Code review still matters, because an assistant can bypass a constraint with Iron's unchecked escape hatches, but teams exploring Scala for AI-assisted development gain a compiler check that catches the most common shortcut.

When Refinement Types Are Not Worth the Effort

Refining everything is a mistake. Each refined type adds a concept that new team members have to learn, and Iron's compile errors take some getting used to for engineers who haven't worked with Scala 3's type-level features before.

Skip refinement types for values that never cross a system boundary, because internal values built from already-trusted inputs gain very little from another layer of proof. Skip refinement types for rules that change often, too. A credit limit or a discount ceiling that the business adjusts every quarter belongs in configuration and runtime validation, since encoding that rule in a type means a code change and a deploy every time the number moves.

Start with the handful of values behind your actual incidents. In commerce and fintech systems, money amounts, quantities, identifiers, percentages, and bounded date ranges are the usual starting points. Refining those few types captures most of the benefit, and the rest of the codebase can stay as it is until a real bug makes the case for more.

Native Refinement Types Are in Development for the Scala Compiler

Researchers at EPFL, including Scala creator Martin Odersky, have designed first-class logical refinement types for Scala 3 and built a prototype extension of the Scala 3 compiler to test the design. In the prototype, predicates are written in ordinary Scala, and refined types work with subtyping, type inference, and pattern matching instead of living in a separate library layer.

The prototype is a research implementation and is not part of any released Scala version. Until native support ships, Iron and opaque types with smart constructors are the production-ready ways to get value-level guarantees in Scala 3.

Waiting for native support would be the wrong call. Most of the effort in adopting refinement types goes into deciding which values deserve constraints and where to validate them. Those decisions don't depend on syntax, so a team that makes them with Iron today won't have to make them again if native refinement types arrive.

Want Scala 3 domain types that stop bad data at the door?

Scala Teams places senior Scala engineers who design refined domain models, boundary validation, and Scala 2 to Scala 3 migrations inside your existing team. Talk to a Scala expert.

Frequently Asked Questions

What are refinement types in Scala 3?

Refinement types in Scala 3 attach a rule to a type, such as greater than zero, so the type only accepts values that satisfy the rule. Invalid values either fail at compile time or get rejected when data enters the system. Scala 3 teams use refinement types today through the Iron library or through opaque types with smart constructors.

What is the difference between member refinements and logical refinement types in Scala?

A member refinement adds or narrows a member of a type, as in Ledger { type Currency = EUR }, and says nothing about which values are valid. A logical refinement type restricts the values a type allows using a predicate, such as an Int that must be positive. Both features are called refinement types in Scala, but only logical refinement types catch invalid data.

Does Scala 3 have built-in refinement types?

No released version of Scala 3 includes built-in logical refinement types. Researchers at EPFL, including Scala creator Martin Odersky, have built a prototype extension of the Scala 3 compiler that adds them. Production teams use the Iron library in the meantime.

Can you use refinement types in Scala 2?

Yes, Scala 2 teams use the Refined library for refinement types, including compile-time checks on literal values. Refined only supports runtime refinement on Scala 3, so teams migrating from Scala 2 to Scala 3 should plan to replace Refined with Iron.

Do refinement types add runtime overhead in Scala?

Iron refinement types add almost no runtime overhead, because an Iron refined value is the plain underlying value at runtime with no wrapper object. Compile-time checks cost nothing when the program runs. Runtime validation costs one check per value at the system boundary, which can replace repeated checks deeper in the code.

Should a Scala 3 team choose Iron or Refined?

A Scala 3 team should choose Iron because Iron supports both compile-time and runtime refinement on Scala 3 while Refined only supports runtime refinement there. Refined remains the right choice for codebases that still run on Scala 2.