Scala Iron, in depth: refinement types for Scala 3, compile-time and runtime refinement, new types and validating at the boundary

The problem refinement types solve

Consider a checkout service. A quantity must be between 1 and 100, a SKU must match a pattern, a username must be alphanumeric and between 3 and 20 characters. The usual approach is a validation layer at the HTTP edge followed by domain methods that take Int and String. That works until a second entry point appears, a batch import or a message consumer, that forgets one rule. Nothing in the signature def total(qty: Int, price: Long) tells the compiler, or the next developer, that qty was supposed to be validated.

The classic fix is a wrapper class with a private constructor and a smart constructor that validates. It works, but every wrapper is boilerplate, allocations can appear in hot loops, and each team writes its own conventions. Refinement types generalise the idea: a type is a base type plus a predicate, and the library supplies the smart constructors, the error messages and, where possible, compile-time checking.

First principles: base type, constraint, proof

An Iron type has two parts. The base type, such as Int or String, describes the runtime representation. The constraint, such as Greater[0] or MinLength[3], is a phantom type: it has no runtime values and exists only to name a predicate. A :| C is Iron's alias for a value of type A that has been shown to satisfy C.

The link between a constraint and its test is a given instance of Constraint[A, C], which supplies an inline test method and a message. Because the test is inline, when the argument is a compile-time constant the compiler can evaluate it during compilation, using Scala 3's inline and macro machinery described in Scala 3 macros. If it evaluates to false, compilation fails with the constraint's message. If the argument is not a constant, the compiler cannot decide, and Iron refuses the implicit conversion; you must refine explicitly.

At runtime the refined type is erased to its base type, like an opaque type: outside its defining scope the compiler treats it as distinct, but no wrapper object exists. There is no allocation and no indirection, which is why refined types are usable inside tight loops and large collections.

How a value becomes refined

The diagram shows the whole model. Literal values take the left path and never cost anything at runtime. Values from files, requests, databases and environment variables take the right path. Domain code at the bottom only accepts refined types, so it cannot be called with an unchecked value, and it contains no validation of its own.

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*

val port: Int :| Greater[0] = 8080          // literal: checked by the compiler
// val bad: Int :| Greater[0] = -1          // does not compile: the constraint fails

def fromEnv(raw: Int): Either[String, Int :| Greater[0]] =
  raw.refineEither[Greater[0]]              // runtime value: checked at runtime

val n: Int = port                           // a refined Int is still usable as an Int

The commented-out line is the point of the library. A constant that breaks the rule is a compile error, not a test failure or an incident. The last line shows the other half: a refined value is a subtype of its base type for reading, so you can pass it to any code that expects an Int. Going the other way, from Int to Int :| Greater[0], always requires a proof.

The runtime refinement methods

Iron offers several ways to refine a runtime value, and choosing between them is mostly about how you want failure represented:

For accumulating several errors at once, Iron has integration modules; the ZIO module, for example, adds refineValidation returning a ZIO Validation. The important discipline is that assume is an unchecked cast. It is the one method that can put a false value into a refined type, so keep it rare, keep it next to a comment saying who guarantees the rule, and search for it in code review.

New types: RefinedType and RefinedSubtype

Writing String :| (Alphanumeric & MinLength[3] & MaxLength[20]) in every signature is noisy, and two different concepts with the same constraint, say a username and a team name, would be interchangeable. Iron solves both with companion objects that define a new type:

import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.all.*

type Username = Username.T
object Username extends RefinedType[String, Alphanumeric & MinLength[3] & MaxLength[20]]

type Quantity = Quantity.T
object Quantity extends RefinedSubtype[Int, GreaterEqual[1] & LessEqual[100]]

val admin: Username = Username("admin")            // literal: compile-time check
val parsed: Either[String, Username] = Username.either(input)
val maybe: Option[Quantity] = Quantity.option(qtyFromForm)

def total(q: Quantity, unitPriceCents: Long): Long = q * unitPriceCents   // subtype: Int ops work

RefinedType creates an opaque new type. A Username is not a String to the compiler, so you cannot pass a team name where a username is expected, and you must be explicit when you need the underlying string. RefinedSubtype creates a subtype instead: a Quantity is still usable wherever an Int is, which is convenient for numeric types used in arithmetic. The companion provides the smart constructors: apply for compile-time checked constants, either and option for runtime values, and applyUnsafe, which does validate at runtime but throws on failure.

Choose the opaque form for identifiers and anything where mixing values up is a real bug. Choose the subtype form for measures you compute with. Constraints combine with & for all-of and | for any-of, and a type alias such as type Between[Min, Max] = GreaterEqual[Min] & LessEqual[Max] keeps them readable.

Writing your own constraint

The built-in constraints cover numbers, strings, collections and regular expressions with Match. Domain rules need your own. A constraint is an empty marker class plus a given instance:

final class Luhn

given Constraint[String, Luhn] with
  override inline def test(inline value: String): Boolean = luhnValid(value)
  override inline def message: String = "Should pass the Luhn checksum"

def luhnValid(s: String): Boolean =
  s.nonEmpty && s.forall(_.isDigit) && {
    val sum = s.reverse.map(_.asDigit).zipWithIndex.map {
      case (d, i) if i % 2 == 1 => val x = d * 2; if x > 9 then x - 9 else x
      case (d, _)               => d
    }.sum
    sum % 10 == 0
  }

type CardNumber = String :| (Luhn & MinLength[12])

Two details matter. First, test is inline, and a literal can only be checked at compile time if the compiler can evaluate the body. A call to an ordinary method such as luhnValid cannot be evaluated during compilation, so Iron cannot prove a literal card number at compile time and will not accept it as a plain assignment; refine even constants through refineEither, or refineUnsafe in tests, and the constraint works as usual at runtime. If compile-time checking of constants matters, write the test using only operations the compiler can fold. Second, the message is what users and logs will see, so write it as a sentence that explains the rule.

Worked example: validating at the boundary

The architecture that makes refinement types pay off is simple: refine once, where untrusted data enters, and use refined types everywhere else. For a JSON API using Circe, that means decoders that refine:

import io.circe.Decoder

final case class CreateOrder(user: Username, sku: String :| Match["[A-Z]{3}-[0-9]{4}"], qty: Quantity)

given Decoder[Username] = Decoder[String].emap(Username.either)
given Decoder[Quantity] = Decoder[Int].emap(Quantity.either)
given Decoder[String :| Match["[A-Z]{3}-[0-9]{4}"]] =
  Decoder[String].emap(_.refineEither[Match["[A-Z]{3}-[0-9]{4}"]])

// Inside the service nothing is re-checked:
def place(o: CreateOrder): Long = total(o.qty, priceOf(o.sku))

Follow a request through it. The body {"user":"ab","sku":"ABC-1234","qty":3} reaches the decoder. Decoder[String] succeeds, then emap(Username.either) runs the constraint, the minimum length fails, and the decoder returns a failure carrying Iron's message. The HTTP layer turns it into a 400 with a field-level error, and place is never called. With a valid body the case class is built with refined fields, and place multiplies a Quantity without any checks because it cannot receive an invalid one.

Apply the same pattern at every boundary: configuration loading, database rows, message consumers, command-line arguments. Iron publishes integration modules for several libraries, which can save writing these instances by hand; check the documentation for the one you use before adding it. Writing them manually, as above, is only a few lines and works with any library that has a map-with-failure operation.

Failure modes and gotchas

• Runtime values do not compile. Developers new to Iron try val q: Quantity = Quantity(input) and get a compile error, because input is not a constant. This is correct behaviour; use either or option.
• Arithmetic loses the refinement. a + b on two positive integers is a plain Int. Iron does not prove that the sum stays positive (and with overflow it may not). Re-refine the result if it must carry the constraint.
• Overuse of assume. Every assume is a promise the compiler cannot check. A refactor that moves validation elsewhere can silently break it.
• Compile-time cost. Constraints are evaluated by inline expansion. Large generated code with many refined literals, or complicated constraint expressions, lengthens compilation. Measure with your build tool before refining everything.
• Erasure at the edges. Refined types are erased, so Java callers, reflection-based serialisers and pattern matching on the type at runtime see only the base type. Keep refined types inside Scala code and convert explicitly at interop points.
• Rules that depend on other data. A constraint tests one value in isolation. Whether a SKU exists or a user has enough credit is a business check with I/O, not a type.

Trade-offs and when not to use it

Iron's strengths are zero runtime cost, errors caught at compile time for constants, and signatures that document rules. Its costs are a Scala 3 requirement, extra compile time, a learning curve for colleagues, and error messages that can be long when constraints are complex. Plain opaque types with a hand-written smart constructor, covered in the Scala type system article, remain a good choice when you have only a handful of domain types or need logic Iron cannot express. Tests remain necessary too: a refinement type proves a value satisfies a rule, not that the rule is the right one.

A practical balance is to refine identifiers, quantities, money amounts, percentages, ports, and anything that has caused an incident, and leave incidental strings alone.

What to do next

1. Add the Iron dependency for your Scala 3 build, pinned to a released version, and compile one module with import io.github.iltotore.iron.*.
2. Pick three domain values that have caused bugs and define them with RefinedType or RefinedSubtype.
3. Change the domain methods that use them to take the refined types, and let the compiler show you every call site that now needs a proof.
4. Refine at each boundary with either, mapping failures to user-facing errors; remove the duplicated checks you find further in.
5. Write a custom constraint for one domain rule, and test its message.
6. Add a code-review check that flags new uses of assume and refineUnsafe outside tests.