diff --git a/CHANGELOG.md b/CHANGELOG.md
index 06e7d93..fecbfa4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,20 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [v0.5.0] - 2025-06-17
+
+### Added
+* Introduced a transparent `Distance` type alias for a `squants.space.Length` value refined to be nonnegative
+* Introduced `Pixels3D` and `PixelDefinition` types
+
+### Changed
+* `iron` is now v3.0.0.
+* Removed the `ProximityComparable` trait
+* Simplified the distance types considerably, removing the `DistanceThreshold` and its subtypes
+* Simplification of the numeric refinement types, relying more directly on reference to the underlying `iron` type names
+* More general and typesafe way to define a pixel as a unit of length
+* Better definition of distance-related types
+
 ## [v0.4.1] - 2025-03-19
 
 ### Added
diff --git a/build.sbt b/build.sbt
index 7e1d764..d41260f 100644
--- a/build.sbt
+++ b/build.sbt
@@ -52,7 +52,7 @@ ThisBuild / testOptions += Tests.Argument("-oF") // full stack traces
 
 lazy val root = project
   .in(file("."))
-  .aggregate(cell, geometry, graph, imaging, io, json, numeric, pan, roi, testing, zarr)
+  .aggregate(cell, geometry, graph, imaging, io, json, numeric, pan, refinement, roi, testing, zarr)
   .enablePlugins(BuildInfoPlugin)
   .settings(commonSettings)
   .settings(noPublishSettings)
@@ -66,7 +66,12 @@ lazy val cell = defineModule("cell")(project)
   .dependsOn(numeric)
 
 lazy val geometry = defineModule("geometry")(project)
-  .dependsOn(numeric)
+  .dependsOn(numeric, refinement)
+  .settings(
+    libraryDependencies ++= Seq(
+      squants,
+    )
+  )
 
 lazy val graph = defineModule("graph")(project)
   .settings(
@@ -88,7 +93,7 @@ lazy val io = defineModule("io")(project)
   )
 
 lazy val imaging = defineModule("imaging")(project)
-  .dependsOn(json, numeric)
+  .dependsOn(json, numeric, refinement)
   .settings(
     libraryDependencies ++= Seq(
       iron % Test,
@@ -108,7 +113,7 @@ lazy val json = defineModule("json")(project)
   )
 
 lazy val numeric = defineModule("numeric")(project)
-  .dependsOn(pan)
+  .dependsOn(pan, refinement)
   .settings(
     libraryDependencies ++= Seq(
       iron, 
@@ -128,6 +133,14 @@ lazy val pan = defineModule("pan")(project)
     )
   )
 
+lazy val refinement = defineModule("refinement")(project)
+  .settings(
+    libraryDependencies ++= Seq(
+      iron,
+      ironScalacheck % Test,
+    )
+  )
+
 lazy val roi = defineModule("roi")(project)
   .dependsOn(geometry, numeric, zarr)
 
@@ -176,7 +189,7 @@ lazy val compileSettings = Def.settings(
   Test / console / scalacOptions := (Compile / console / scalacOptions).value,
 )
 
-lazy val versionNumber = "0.4.1"
+lazy val versionNumber = "0.5.0"
 
 lazy val metadataSettings = Def.settings(
   name := projectName,
diff --git a/modules/cell/src/main/scala/NuclearDesignation.scala b/modules/cell/src/main/scala/NuclearDesignation.scala
index 952864e..c63c27c 100644
--- a/modules/cell/src/main/scala/NuclearDesignation.scala
+++ b/modules/cell/src/main/scala/NuclearDesignation.scala
@@ -6,9 +6,9 @@ import cats.derived.*
 import cats.syntax.all.*
 
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
-import at.ac.oeaw.imba.gerlich.gerlib.syntax.all.*
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.positiveInt.given
+import at.ac.oeaw.imba.gerlich.gerlib.syntax.all.*
 
 /** Designation of whether something's in a cell nucleus or not */
 sealed trait NuclearDesignation
@@ -27,11 +27,8 @@ object NucleusNumber:
   /** Try to read the given string as a nucleus number. */
   def parse(s: String): Either[String, NucleusNumber] =
     readAsInt(s)
-      .flatMap(PositiveInt.either)
-      .bimap(
-        msg => s"Cannot parse value ($s) as nucleus number: $msg",
-        NucleusNumber.apply
-      )
+      .flatMap(i => PositiveInt.option(i).toRight(s"Cannot parse value ($s) as nucleus number"))
+      .map(NucleusNumber.apply)
 end NucleusNumber
 
 /** Helpers for working with nuclei number labels */
@@ -47,10 +44,9 @@ object NuclearDesignation:
 
   /** Attempt to read the given text as a nucleus number. */
   def parse(s: String): Either[String, NuclearDesignation] =
-    readAsInt(s).flatMap { z =>
-      if z > 0 then NucleusNumber(PositiveInt.unsafe(z)).asRight
-      else if z === 0 then OutsideNucleus.asRight
-      else s"Negative value parsed for nucleus number: $z".asLeft
+    readAsInt(s).flatMap {
+      case 0 => OutsideNucleus.asRight
+      case z => PositiveInt.either(z).map(NucleusNumber.apply)
     }
 
   /** Represent the extranuclear designation as 0, and intranuclear by the wrapped number. */
diff --git a/modules/cell/src/test/scala/TestNuclearDesignation.scala b/modules/cell/src/test/scala/TestNuclearDesignation.scala
index afe72f3..eb6f020 100644
--- a/modules/cell/src/test/scala/TestNuclearDesignation.scala
+++ b/modules/cell/src/test/scala/TestNuclearDesignation.scala
@@ -10,11 +10,18 @@ import org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
 
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.PositiveInt
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.all.given
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
 /** Tests for data type for nucleuar / non-nuclear attribution */
 class TestNuclearDesignation extends AnyFunSuite, ScalaCheckPropertyChecks, should.Matchers:
   given Arbitrary[PositiveInt] = Arbitrary:
-    Gen.choose(1, Int.MaxValue).map(PositiveInt.unsafe)
+    Gen
+      .choose(1, Int.MaxValue)
+      .map(n =>
+        PositiveInt
+          .option(n)
+          .getOrElse { throw IllegalRefinement(n, "Cannot refine as positive") }
+      )
 
   given (arbPosInt: Arbitrary[PositiveInt]) => Arbitrary[NucleusNumber] =
     Arbitrary { arbPosInt.arbitrary.map(NucleusNumber.apply) }
diff --git a/modules/geometry/src/main/scala/Distance.scala b/modules/geometry/src/main/scala/Distance.scala
index d004d4d..adbd2a3 100644
--- a/modules/geometry/src/main/scala/Distance.scala
+++ b/modules/geometry/src/main/scala/Distance.scala
@@ -1,6 +1,5 @@
 package at.ac.oeaw.imba.gerlich.gerlib.geometry
 
-import scala.math.{pow, sqrt}
 import scala.util.NotGiven
 import scala.util.chaining.* // for pipe
 import cats.*
@@ -9,91 +8,6 @@ import cats.syntax.all.*
 
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
 
-/** Something that can compare two {@code A} values w.r.t. threshold value of type {@code T}
-  */
-trait ProximityComparable[A]:
-  /** Are the two {@code A} values within threshold {@code T} of each other? */
-  def proximal: (A, A) => Boolean
-end ProximityComparable
-
-/** Helpers for working with proximity comparisons */
-object ProximityComparable:
-  extension [A](a1: A)(using ev: ProximityComparable[A])
-    infix def proximal(a2: A): Boolean = ev.proximal(a1, a2)
-
-  given contravariantForProximityComparable: Contravariant[ProximityComparable] =
-    new Contravariant[ProximityComparable]:
-      override def contramap[A, B](fa: ProximityComparable[A])(f: B => A) =
-        new ProximityComparable[B]:
-          override def proximal = (b1, b2) => fa.proximal(f(b1), f(b2))
-end ProximityComparable
-
-/** A threshold on distances, which should be nonnegative, to be semantically contextualised by the
-  * subtype
-  */
-sealed trait DistanceThreshold:
-  def get: NonnegativeReal
-
-/** Helpers for working with distance thresholds */
-object DistanceThreshold:
-  given showForDistanceThreshold: Show[DistanceThreshold] = Show.show { (t: DistanceThreshold) =>
-    val typeName = t match
-    case _: EuclideanDistance.Threshold            => "Euclidean"
-    case _: PiecewiseDistance.ConjunctiveThreshold => "Conjunctive"
-    s"${typeName}Threshold(${t.get})"
-  }
-
-  /** Define a proximity comparison for 3D points values.
-    *
-    * @tparam C
-    *   The type of raw value wrapped in a coordinate for each 3D point
-    * @param threshold
-    *   The distance beneath which to consider a given pair of points as proximal
-    * @return
-    *   An instance with which to check pairs of points for proximity, according to the given
-    *   threshold value ('think': decision boundary)
-    * @see
-    *   [[at.ac.oeaw.imba.gerlich.gerlib.geometry.Point3D]]
-    */
-  def defineProximityPointwise[C: Numeric](
-      threshold: DistanceThreshold
-  ): ProximityComparable[Point3D[C]] = threshold match
-  case t: EuclideanDistance.Threshold =>
-    new ProximityComparable[Point3D[C]]:
-      override def proximal = (a, b) =>
-        val d = EuclideanDistance.between(a, b)
-        if d.isInfinite then
-          throw new EuclideanDistance.OverflowException(
-            s"Cannot compute finite distance between $a and $b"
-          )
-        d `lessThan` t
-  case t: PiecewiseDistance.ConjunctiveThreshold =>
-    new ProximityComparable[Point3D[C]]:
-      override def proximal = PiecewiseDistance.within(t)
-
-  /** Define a proximity comparison for values of arbitrary type, according to given threshold and
-    * how to extract a 3D point value.
-    *
-    * @tparam A
-    *   The type of value from which a 3D point will be extracted for purpose of proximity check /
-    *   comparison
-    * @tparam C
-    *   The type of raw value wrapped in a coordinate for each 3D point
-    * @param threshold
-    *   The distance beneath which to consider a given pair of points as proximal
-    * @return
-    *   An instance with which to check pairs of values for proximity, according to the given
-    *   threshold value ('think': decision boundary), and how to get a 3D point from a value of type
-    *   `A`
-    * @see
-    *   [[at.ac.oeaw.imba.gerlich.gerlib.geometry.Point3D]]
-    */
-  def defineProximityPointwise[A, C: Numeric](
-      threshold: DistanceThreshold
-  ): (A => Point3D[C]) => ProximityComparable[A] =
-    defineProximityPointwise(threshold).contramap
-end DistanceThreshold
-
 /** Piecewise / by-component distance, as absolute differences
   *
   * @param x
@@ -118,7 +32,7 @@ object PiecewiseDistance:
   /** Distance threshold in which predicate comparing values to this threshold operates
     * conjunctively over components
     */
-  final case class ConjunctiveThreshold(get: NonnegativeReal) extends DistanceThreshold
+  final case class Conjunctive(get: NonnegativeReal)
 
   /** Compute the piecewise / component-wise distance between the given points.
     *
@@ -147,7 +61,7 @@ object PiecewiseDistance:
 
   /** Are points closer than given threshold along each axis? */
   def within[C: Numeric](
-      threshold: ConjunctiveThreshold
+      threshold: Conjunctive
   )(a: Point3D[C], b: Point3D[C]): Boolean =
     val d = between(a, b)
     d.getX < threshold.get && d.getY < threshold.get && d.getZ < threshold.get
@@ -159,46 +73,24 @@ object PiecewiseDistance:
     NonnegativeReal.either((a.value - b.value).toDouble.abs)
 end PiecewiseDistance
 
-/** Semantic wrapper to denote that a nonnegative real number represents a Euclidean distance
+sealed trait DistanceLike:
+  def getDistanceValue: Distance
+
+/** Semantic wrapper to denote that a nonnegative length represents a Euclidean distance
   */
-final case class EuclideanDistance private (get: NonnegativeReal):
-  final def lessThan(t: EuclideanDistance.Threshold): Boolean = get < t.get
-  final def greaterThan = !lessThan(_: EuclideanDistance.Threshold)
-  final def equalTo(t: EuclideanDistance.Threshold) =
-    !lessThan(t) && !greaterThan(t)
-  final def lteq(t: EuclideanDistance.Threshold) = lessThan(t) || equalTo(t)
-  final def gteq(t: EuclideanDistance.Threshold) = greaterThan(t) || equalTo(t)
-  final def isFinite = get.isFinite
+final case class EuclideanDistance(get: Distance) extends DistanceLike:
+  final def isFinite = get.value.isFinite
   final def isInfinite = !isFinite
+  final override def getDistanceValue: Distance = get
 end EuclideanDistance
 
 /** Helpers for working with Euclidean distances */
 object EuclideanDistance:
-  import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeReal.given // for Order
-
   /** Order distance by the wrapped value. */
-  given Order[EuclideanDistance] = Order.by(_.get)
-
-  /** When something goes wrong with a distance computation or comparison */
-  final case class OverflowException(message: String) extends Exception(message)
-
-  /** Comparison basis for Euclidean distance between points */
-  final case class Threshold(get: NonnegativeReal) extends DistanceThreshold
+  given Order[EuclideanDistance] =
+    import Distance.given_Order_Distance
+    Order.by(_.get) // use the Double backing the squants.space.Length.
 
-  // TODO: account for infinity/null-numeric cases.
-  def between[C: Numeric](a: Point3D[C], b: Point3D[C]): EuclideanDistance =
-    import scala.math.Numeric.Implicits.infixNumericOps
-    (a, b) match
-    case (Point3D(x1, y1, z1), Point3D(x2, y2, z2)) =>
-      List(x1 -> x2, y1 -> y2, z1 -> z2)
-        .foldLeft(0.0) { case (acc, (a, b)) => acc + pow((a.value - b.value).toDouble, 2) }
-        .pipe(sqrt)
-        .pipe(NonnegativeReal.unsafe)
-        .pipe(EuclideanDistance.apply)
-
-  /** Use a lens of a 3D point from arbitrary type {@code A} to compute distance between {@code A}
-    * values.
-    */
-  def between[A, C: Numeric](p: A => Point3D[C])(a1: A, a2: A): EuclideanDistance =
-    between(p(a1), p(a2))
+  def parse: String => Either[String, EuclideanDistance] =
+    s => Distance.parse(s).map(EuclideanDistance.apply)
 end EuclideanDistance
diff --git a/modules/geometry/src/main/scala/package.scala b/modules/geometry/src/main/scala/package.scala
index 6cff791..59b832b 100644
--- a/modules/geometry/src/main/scala/package.scala
+++ b/modules/geometry/src/main/scala/package.scala
@@ -1,5 +1,11 @@
 package at.ac.oeaw.imba.gerlich.gerlib
 
+import cats.Order
+import io.github.iltotore.iron.{RefinedType, RuntimeConstraint}
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
+import squants.space.Length
+
 /** Types and tools related to geometry */
 package object geometry:
   /** Centroid of a region of interest */
@@ -28,6 +34,26 @@ package object geometry:
       private[gerlib] def z: ZCoordinate[C] = c.z
   end Centroid
 
+  /** Constrain a length to be like a distance (nonnegative). */
+  given RuntimeConstraint[Length, Not[Negative]] =
+    new RuntimeConstraint(
+      _.value >= 0,
+      "Allegedly nonnegative length must actually be nonnegative."
+    )
+
+  /** Leave this alias transparent, since we just want the typelevel 'check' that the length is
+    * nonnegative; we don't want the underlying type masked.
+    */
+  type Distance = Distance.T
+
+  object Distance extends RefinedType[Length, Not[Negative]]:
+    given Order[Distance] = Order.fromOrdering
+
+    def parse(s: String): Either[String, Distance] =
+      import syntax.*
+      Length.parse(s).flatMap(either)
+  end Distance
+
   type AxisX = EuclideanAxis.X.type
 
   type AxisY = EuclideanAxis.Y.type
diff --git a/modules/geometry/src/main/scala/syntax/package.scala b/modules/geometry/src/main/scala/syntax/package.scala
index cf8ad86..5e30658 100644
--- a/modules/geometry/src/main/scala/syntax/package.scala
+++ b/modules/geometry/src/main/scala/syntax/package.scala
@@ -1,8 +1,10 @@
 package at.ac.oeaw.imba.gerlich.gerlib.geometry
 
-import cats.Monoid
+import scala.util.NotGiven
+import cats.{Monoid, Order}
 import cats.data.NonEmptyList
 import cats.syntax.all.*
+import squants.space.Length
 
 /** Syntax enrichment on values of data types related to geometry */
 package object syntax:
@@ -27,3 +29,10 @@ package object syntax:
         YCoordinate(a.y.value - b.y.value),
         ZCoordinate(a.z.value - b.z.value)
       )
+
+  extension [A: Order, C <: Coordinate[A]: [C] =>> NotGiven[C =:= Coordinate[A]]](c1: C)(using
+      ord: Order[C]
+  ) infix def max(c2: C): C = ord.max(c1, c2)
+
+  extension (L: Length.type)
+    def parse(s: String): Either[String, Length] = L(s).toEither.leftMap(_.getMessage)
diff --git a/modules/geometry/src/test/scala/TestDistance.scala b/modules/geometry/src/test/scala/TestDistance.scala
new file mode 100644
index 0000000..9b75014
--- /dev/null
+++ b/modules/geometry/src/test/scala/TestDistance.scala
@@ -0,0 +1,60 @@
+package at.ac.oeaw.imba.gerlich.gerlib.geometry
+
+import squants.space.*
+
+import org.scalacheck.{Arbitrary, Gen}
+import org.scalacheck.Arbitrary.arbitrary
+import org.scalatest.funsuite.AnyFunSuite
+import org.scalatest.matchers.should
+import org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
+
+/** Tests for the refinement of a [[squants.space.Length]] value as a distance */
+class TestDistance extends AnyFunSuite, should.Matchers, ScalaCheckPropertyChecks:
+
+  given Arbitrary[LengthUnit] = Arbitrary:
+    Gen.oneOf(
+      Angstroms,
+      Nanometers,
+      Microns,
+      Millimeters
+    )
+
+  given (Arbitrary[Double]) => Arbitrary[Length] = Arbitrary:
+    for
+      v <- arbitrary[Double]
+      u <- arbitrary[LengthUnit]
+    yield Length(v -> u.symbol).fold(throw _, identity)
+
+  test("Distance.option works if and only if the length is nonnegative."):
+    forAll { (l: Length) =>
+      (l.value < 0, Distance.option(l)) match {
+      case (false, Some(d)) => d shouldEqual l
+      case (true, None)     => succeed
+      case (_, _)           =>
+      }
+    }
+
+  test("Distance instantiation CANNOT be done with apply syntax."):
+    assertCompiles("val l: Length = Length(1 -> \"nm\").get")
+    assertTypeError(
+      "Distance(Length(1 -> \"nm\").get)"
+    ) // should be missing Constraint[Length, Not[Negative]]
+
+  test("A value typed as Distance is correctly compared to a squants.space.Length value."):
+    given Arbitrary[Distance] =
+      given Arbitrary[Double] = Arbitrary(Gen.choose(0, Double.MaxValue))
+      Arbitrary(
+        arbitrary[Length].map(l =>
+          Distance
+            .option(l)
+            .getOrElse(throw IllegalRefinement(l, "Cannot refine length as distance"))
+        )
+      )
+
+    forAll { (l: Length, d: Distance) =>
+      val dAsL: Length = d
+      l < d shouldBe l < dAsL
+    }
+
+end TestDistance
diff --git a/modules/imaging/src/main/scala/ImagingChannel.scala b/modules/imaging/src/main/scala/ImagingChannel.scala
index 0c1e170..79b0f41 100644
--- a/modules/imaging/src/main/scala/ImagingChannel.scala
+++ b/modules/imaging/src/main/scala/ImagingChannel.scala
@@ -2,13 +2,16 @@ package at.ac.oeaw.imba.gerlich.gerlib.imaging
 
 import cats.*
 import cats.derived.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.cats.given_Order_:| // for derivation of Order for wrapper type
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
 
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given
+import at.ac.oeaw.imba.gerlich.gerlib.numeric.parseThroughNonnegativeInt
 import at.ac.oeaw.imba.gerlich.gerlib.syntax.all.*
 
 /** Semantic wrapper around value representing 0-based imaging channel */
-final case class ImagingChannel(private[gerlib] get: NonnegativeInt) derives Order
+final case class ImagingChannel(private[gerlib] get: Int :| Not[Negative]) derives Order
 
 /** Helpers for working with imaging channels */
 object ImagingChannel:
diff --git a/modules/imaging/src/main/scala/ImagingTimepoint.scala b/modules/imaging/src/main/scala/ImagingTimepoint.scala
index fde467f..9565765 100644
--- a/modules/imaging/src/main/scala/ImagingTimepoint.scala
+++ b/modules/imaging/src/main/scala/ImagingTimepoint.scala
@@ -3,16 +3,20 @@ package at.ac.oeaw.imba.gerlich.gerlib.imaging
 import cats.*
 import cats.derived.*
 import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.cats.given_Order_:| // for derivation of Order for wrapper type
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
 
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
 /** Semantic wrapper around value representing 0-based imaging timepoint */
-final case class ImagingTimepoint(private[gerlib] get: NonnegativeInt) derives Order
+final case class ImagingTimepoint(private[gerlib] get: Int :| Not[Negative]) derives Order
 
 /** Helpers for working with imaging timepoints */
 object ImagingTimepoint:
-  /** Attempt to create a timepoint from an integer, first refining through {@code NonnegativeInt} .
+  /** Attempt to create a timepoint from an integer, first refining as nonnegative integer .
     */
   def fromInt: Int => Either[String, ImagingTimepoint] =
     NonnegativeInt.either.map(_.map(ImagingTimepoint.apply))
@@ -34,7 +38,11 @@ object ImagingTimepoint:
 
   /** Lift the given integer to nonnegative, then wrap as an imaging timepoint.
     */
-  def unsafeLift = NonnegativeInt.unsafe `andThen` ImagingTimepoint.apply
+  def unsafeLift = (i: Int) =>
+    NonnegativeInt.option(i) match {
+    case None    => throw IllegalRefinement(i, s"Illegal value as imaging timepoint: $i")
+    case Some(t) => ImagingTimepoint(t)
+    }
 
   extension (t: ImagingTimepoint)
     /** Attempt to create a new imaging timepoint by shifting one by the given increment.
diff --git a/modules/imaging/src/main/scala/instances/FieldOfViewLikeInstances.scala b/modules/imaging/src/main/scala/instances/FieldOfViewLikeInstances.scala
index e3900b5..30afb12 100644
--- a/modules/imaging/src/main/scala/instances/FieldOfViewLikeInstances.scala
+++ b/modules/imaging/src/main/scala/instances/FieldOfViewLikeInstances.scala
@@ -2,10 +2,12 @@ package at.ac.oeaw.imba.gerlich.gerlib.imaging
 package instances
 
 import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
 
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
 import at.ac.oeaw.imba.gerlich.gerlib.json.JsonValueWriter
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.NonnegativeInt
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given
 import at.ac.oeaw.imba.gerlich.gerlib.syntax.all.*
 
@@ -23,7 +25,7 @@ trait FieldOfViewLikeInstances:
   /** Simply show a field of view by the text representation of the underlying integer value.
     */
   given SimpleShow[FieldOfView] =
-    summon[SimpleShow[NonnegativeInt]].contramap(_.get)
+    summon[SimpleShow[Int :| Not[Negative]]].contramap(_.get)
 
   /** Simply show a position name by the underlying value. */
   given SimpleShow[PositionName] = SimpleShow.instance(_.get)
diff --git a/modules/imaging/src/main/scala/instances/ImagingChannelInstances.scala b/modules/imaging/src/main/scala/instances/ImagingChannelInstances.scala
index d6994e8..00a4632 100644
--- a/modules/imaging/src/main/scala/instances/ImagingChannelInstances.scala
+++ b/modules/imaging/src/main/scala/instances/ImagingChannelInstances.scala
@@ -2,11 +2,13 @@ package at.ac.oeaw.imba.gerlich.gerlib.imaging
 package instances
 
 import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
 
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.NonnegativeInt
 
 trait ImagingChannelInstances:
-  import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given
   given SimpleShow[ImagingChannel] =
-    summon[SimpleShow[NonnegativeInt]].contramap(_.get)
+    import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given_SimpleShow_:|
+    summon[SimpleShow[Int :| Not[Negative]]].contramap(_.get)
diff --git a/modules/imaging/src/main/scala/instances/ImagingTimepointInstances.scala b/modules/imaging/src/main/scala/instances/ImagingTimepointInstances.scala
index c78abf6..0c9ecbe 100644
--- a/modules/imaging/src/main/scala/instances/ImagingTimepointInstances.scala
+++ b/modules/imaging/src/main/scala/instances/ImagingTimepointInstances.scala
@@ -2,16 +2,19 @@ package at.ac.oeaw.imba.gerlich.gerlib.imaging
 package instances
 
 import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
+
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
 import at.ac.oeaw.imba.gerlich.gerlib.json.*
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.NonnegativeInt
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given
 
 /** Typeclass instances for working with imaging timepoint values */
 trait ImagingTimepointInstances:
   /** Simply show a timepoint by its underlying integer value. */
   given SimpleShow[ImagingTimepoint] =
-    summon[SimpleShow[NonnegativeInt]].contramap(_.get)
+    import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given_SimpleShow_:|
+    summon[SimpleShow[Int :| Not[Negative]]].contramap(_.get)
 
   given JsonValueWriter[ImagingTimepoint, ujson.Num]:
     override def apply(t: ImagingTimepoint): ujson.Num = ujson.Num(t.get)
diff --git a/modules/imaging/src/main/scala/package.scala b/modules/imaging/src/main/scala/package.scala
index 0e7265c..531b126 100644
--- a/modules/imaging/src/main/scala/package.scala
+++ b/modules/imaging/src/main/scala/package.scala
@@ -9,10 +9,14 @@ import io.github.iltotore.iron.cats.given
 import io.github.iltotore.iron.constraint.any.{Not, StrictEqual}
 import io.github.iltotore.iron.constraint.char.{Digit, Letter}
 import io.github.iltotore.iron.constraint.collection.{Empty, ForAll}
+import io.github.iltotore.iron.constraint.numeric.Negative
 import io.github.iltotore.iron.constraint.string.Match
+import squants.MetricSystem
+import squants.space.{Length, LengthUnit, Microns, Millimeters, Nanometers}
 
+import at.ac.oeaw.imba.gerlich.gerlib.geometry.{Distance, EuclideanDistance, Point3D}
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
 /** Tools and types related to imaging */
 package object imaging:
@@ -32,9 +36,9 @@ package object imaging:
         }
 
   /** Type wrapper around 0-based index of field of view (FOV) */
-  final case class FieldOfView(private[imaging] get: NonnegativeInt) extends FieldOfViewLike
+  final case class FieldOfView(private[imaging] get: Int :| Not[Negative]) extends FieldOfViewLike
       derives Order:
-    def getRawValue: NonnegativeInt = get
+    def getRawValue: Int :| Not[Negative] = get
 
   /** Helpers for working with fields of view */
   object FieldOfView:
@@ -48,8 +52,11 @@ package object imaging:
 
     /** Lift an ordinary integer into field of view wrapper, erroring if invalid.
       */
-    def unsafeLift: Int => FieldOfView =
-      NonnegativeInt.unsafe `andThen` FieldOfView.apply
+    def unsafeLift: Int => FieldOfView = i =>
+      NonnegativeInt.option(i) match {
+      case None    => throw IllegalRefinement(i, s"Illegal value as field of view: $i")
+      case Some(t) => FieldOfView(t)
+      }
   end FieldOfView
 
   private[gerlib] type PositionNamePunctuation = StrictEqual['.'] | StrictEqual['-'] |
@@ -101,4 +108,60 @@ package object imaging:
     def unsafe = (s: String) => parse(s).fold(msg => throw IllegalArgumentException(msg), identity)
   end PositionName
 
+  // TODO: try typelevel restriction of the .symbol abstract member to be "px" singleton.
+  type PixelDefinition = LengthUnit
+
+  /** A fundamental unit of length in imaging, the pixel */
+  object PixelDefinition:
+    /** Define a unit of length in pixels by specifying a physical length per pixel. */
+    def tryToDefine(l: Length): Either[String, PixelDefinition] = for
+      baseFactor <- l.unit match {
+      case Nanometers  => MetricSystem.Nano.asRight
+      case Microns     => MetricSystem.Micro.asRight
+      case Millimeters => MetricSystem.Milli.asRight
+      case u => s"Cannot resolve base conversion factor for unit ($u) from length $l".asLeft
+      }
+      specificFactor <- PositiveReal.either(l.value)
+    yield new:
+      val conversionFactor: Double = specificFactor * baseFactor
+      val symbol: String = "px"
+
+    given Show[PixelDefinition] =
+      Show.show(pxDef => s"PixelDefinition: ${pxDef(1)}")
+
+    object syntax:
+      extension (pxDef: PixelDefinition)
+        def lift[A: Numeric](a: A): Length = (pxDef: LengthUnit).apply(a)
+  end PixelDefinition
+
+  /** Rescaling of the units in 3D */
+  final case class Pixels3D(
+      private val x: PixelDefinition,
+      private val y: PixelDefinition,
+      private val z: PixelDefinition
+  ):
+    import PixelDefinition.syntax.lift
+    def liftX[A: Numeric](a: A): Length = x.lift(a)
+    def liftY[A: Numeric](a: A): Length = y.lift(a)
+    def liftZ[A: Numeric](a: A): Length = z.lift(a)
+  end Pixels3D
+
+  def euclideanDistanceBetweenImagePoints[A, C: Numeric](
+      pixels: Pixels3D
+  )(f: A => Point3D[C]): (A, A) => EuclideanDistance =
+    (a1, a2) => euclideanDistanceBetweenImagePoints(pixels)(f(a1), f(a2))
+
+  def euclideanDistanceBetweenImagePoints[C: Numeric](
+      pixels: Pixels3D
+  )(p: Point3D[C], q: Point3D[C]): EuclideanDistance =
+    import scala.math.Numeric.Implicits.infixNumericOps
+    computeDistance(
+      pixels.liftX(p.x.value - q.x.value),
+      pixels.liftY(p.y.value - q.y.value),
+      pixels.liftZ(p.z.value - q.z.value)
+    )
+
+  private def computeDistance(delX: Length, delY: Length, delZ: Length): EuclideanDistance =
+    val d = (delX * delX + delY * delY + delZ * delZ).squareRoot
+    Distance.either(d).fold(msg => throw IllegalRefinement(d, msg), EuclideanDistance.apply)
 end imaging
diff --git a/modules/imaging/src/test/scala/TestImagingInstances.scala b/modules/imaging/src/test/scala/TestImagingInstances.scala
index b2e9b05..1961ad9 100644
--- a/modules/imaging/src/test/scala/TestImagingInstances.scala
+++ b/modules/imaging/src/test/scala/TestImagingInstances.scala
@@ -6,12 +6,13 @@ import org.scalatest.matchers.*
 import org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
 
 import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
 import io.github.iltotore.iron.constraint.char.*
+import io.github.iltotore.iron.constraint.numeric.Negative
 import io.github.iltotore.iron.scalacheck.char.given
 import io.github.iltotore.iron.scalacheck.numeric.intervalArbitrary
 
 import at.ac.oeaw.imba.gerlich.gerlib.imaging.instances.fieldOfViewLike.given
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.{Nonnegative, NonnegativeInt}
 import at.ac.oeaw.imba.gerlich.gerlib.syntax.all.*
 
 /** Tests for imaging-related types' typeclass instances */
@@ -77,7 +78,7 @@ class TestImagingInstances extends AnyFunSuite, ScalaCheckPropertyChecks, should
     import at.ac.oeaw.imba.gerlich.gerlib.json.syntax.*
 
     given Arbitrary[FieldOfView] = Arbitrary {
-      intervalArbitrary[Int, Nonnegative](0, Int.MaxValue).arbitrary
+      intervalArbitrary[Int, Not[Negative]](0, Int.MaxValue).arbitrary
         .map(FieldOfView.apply)
     }
 
diff --git a/modules/io/src/main/scala/csv/instances/InstancesForGeometry.scala b/modules/io/src/main/scala/csv/instances/InstancesForGeometry.scala
index c1a1fb9..7cbec22 100644
--- a/modules/io/src/main/scala/csv/instances/InstancesForGeometry.scala
+++ b/modules/io/src/main/scala/csv/instances/InstancesForGeometry.scala
@@ -2,8 +2,10 @@ package at.ac.oeaw.imba.gerlich.gerlib.io.csv
 package instances
 
 import scala.util.NotGiven
+
 import cats.syntax.all.*
 import fs2.data.csv.*
+import squants.space.Length
 
 import at.ac.oeaw.imba.gerlich.gerlib.geometry.*
 import at.ac.oeaw.imba.gerlich.gerlib.geometry.Centroid.asPoint
@@ -62,3 +64,12 @@ trait InstancesForGeometry:
       val y = ColumnNames.yCenterColumnName[C].write(pt.y)
       val x = ColumnNames.xCenterColumnName[C].write(pt.x)
       z |+| y |+| x
+
+  given CellDecoder[Length] =
+    import at.ac.oeaw.imba.gerlich.gerlib.geometry.syntax.*
+    CellDecoder.instance(s => Length.parse(s).leftMap(msg => DecoderError(msg)))
+
+  given CellEncoder[Length] = CellEncoder.fromToString
+
+  given (dec: CellDecoder[Length]) => CellDecoder[EuclideanDistance] =
+    dec.emap(l => Distance.either(l).bimap(msg => DecoderError(msg), EuclideanDistance.apply))
diff --git a/modules/io/src/main/scala/csv/instances/InstancesForNumeric.scala b/modules/io/src/main/scala/csv/instances/InstancesForNumeric.scala
index 6d874fd..22b99d6 100644
--- a/modules/io/src/main/scala/csv/instances/InstancesForNumeric.scala
+++ b/modules/io/src/main/scala/csv/instances/InstancesForNumeric.scala
@@ -1,19 +1,32 @@
 package at.ac.oeaw.imba.gerlich.gerlib.io.csv
 package instances
 
+import cats.syntax.all.*
 import fs2.data.csv.*
 
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
+
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
+import at.ac.oeaw.imba.gerlich.gerlib.numeric.{
+  NonnegativeInt,
+  NonnegativeReal,
+  readAsDouble,
+  readAsInt
+}
 
 trait InstancesForNumeric:
-  given CellDecoder[NonnegativeInt] = liftToCellDecoder(NonnegativeInt.parse)
+  given cellDecoderForNonnegativeInt: CellDecoder[Int :| Not[Negative]] =
+    liftToCellDecoder(readAsInt.map(_.flatMap(NonnegativeInt.either)))
 
-  given (SimpleShow[NonnegativeInt]) => CellEncoder[NonnegativeInt] =
-    CellEncoder.fromSimpleShow[NonnegativeInt]
+  given (SimpleShow[Int :| Not[Negative]]) => CellEncoder[Int :| Not[Negative]] =
+    CellEncoder.fromSimpleShow[Int :| Not[Negative]]
 
-  given CellDecoder[NonnegativeReal] = liftToCellDecoder(NonnegativeReal.parse)
+  given cellDecoderForNonnegativeReal: CellDecoder[Double :| Not[Negative]] =
+    liftToCellDecoder(readAsDouble.map(_.flatMap(NonnegativeReal.either)))
 
-  given (enc: CellEncoder[Double]) => CellEncoder[NonnegativeReal] =
-    enc.contramap: (x: NonnegativeReal) =>
+  given (enc: CellEncoder[Double]) => CellEncoder[Double :| Not[Negative]] =
+    enc.contramap: (x: Double :| Not[Negative]) =>
       (x: Double)
+end InstancesForNumeric
diff --git a/modules/json/src/main/scala/instances/JsonInstancesForGeometry.scala b/modules/json/src/main/scala/instances/JsonInstancesForGeometry.scala
index 80f5e46..b8bd686 100644
--- a/modules/json/src/main/scala/instances/JsonInstancesForGeometry.scala
+++ b/modules/json/src/main/scala/instances/JsonInstancesForGeometry.scala
@@ -1,8 +1,15 @@
 package at.ac.oeaw.imba.gerlich.gerlib.json
 package instances
 
-import scala.util.NotGiven
-import at.ac.oeaw.imba.gerlich.gerlib.geometry.Coordinate
+import scala.util.{NotGiven, Try}
+import cats.data.ValidatedNel
+import cats.syntax.all.*
+import squants.space.Length
+import ujson.IncompleteParseException
+import upickle.default.*
+
+import at.ac.oeaw.imba.gerlich.gerlib.geometry.{Coordinate, Distance, DistanceLike}
+import at.ac.oeaw.imba.gerlich.gerlib.geometry.EuclideanDistance
 
 /** JSON-related typeclass instances for geometry-related data types */
 trait JsonInstancesForGeometry:
@@ -13,4 +20,61 @@ trait JsonInstancesForGeometry:
   ): JsonValueWriter[C, O] = new:
     override def apply(c: C): O = writeRaw(c.value)
 
+  given ReadWriter[String] => ReadWriter[Length] = readwriter[String].bimap(
+    _.toString,
+    s => Length(s).fold(throw _, identity)
+  )
+
+  given (ReadWriter[Length]) => ReadWriter[Distance] = readwriter[Length].bimap(
+    identity,
+    l => lengthToDistance(l).fold(throw _, identity)
+  )
+
+  given ReadWriter[Distance] => ReadWriter[DistanceLike] =
+    val valueKey = "value"
+    val typeKey = "metricType"
+    val euclideanSpecifier = "Euclidean"
+    readwriter[Map[String, ujson.Value]].bimap(
+      (_: DistanceLike) match {
+      case eucl: EuclideanDistance =>
+        Map(
+          valueKey -> write(eucl.getDistanceValue),
+          typeKey -> euclideanSpecifier
+        )
+      },
+      data =>
+        val valueNel = data
+          .get(valueKey)
+          .toRight(s"Missing value key ($valueKey) for distance")
+          .flatMap(s =>
+            Try(read[Distance](s)).toEither
+              .leftMap(e => s"Cannot decode distance value ($s): ${e.getMessage}")
+          )
+          .toValidatedNel
+        val builderNel: ValidatedNel[String, Distance => DistanceLike] = data
+          .get(typeKey)
+          .toRight(s"Missing type key ($typeKey) for distance")
+          .flatMap(s =>
+            Try(read[String](s)).toEither
+              .leftMap(_.getMessage)
+              .flatMap {
+                case `euclideanSpecifier` => EuclideanDistance.apply.asRight
+                case unknownSpecifier =>
+                  s"Unrecognized distance metric specifier ($unknownSpecifier)".asLeft
+              }
+          )
+          .toValidatedNel
+        (valueNel, builderNel)
+          .mapN { (dist, build) => build(dist) }
+          .fold(
+            messages => throw IncompleteParseException(s"Error(s): ${messages.mkString_("; ")}"),
+            identity
+          )
+    )
+
+  private def lengthToDistance(l: Length): Either[IncompleteParseException, Distance] =
+    Distance
+      .either(l)
+      .leftMap(msg => new IncompleteParseException(s"(parsing $l): $msg"))
+
 end JsonInstancesForGeometry
diff --git a/modules/json/src/test/scala/TestDistanceJsonCodec.scala b/modules/json/src/test/scala/TestDistanceJsonCodec.scala
new file mode 100644
index 0000000..9899eba
--- /dev/null
+++ b/modules/json/src/test/scala/TestDistanceJsonCodec.scala
@@ -0,0 +1,59 @@
+package at.ac.oeaw.imba.gerlich.gerlib.json
+package instances
+
+import squants.QuantityParseException
+import squants.space.*
+import upickle.default.*
+import org.scalacheck.*
+import org.scalatest.funsuite.AnyFunSuite
+import org.scalatest.matchers.should
+import org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
+
+import at.ac.oeaw.imba.gerlich.gerlib.geometry.Distance
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
+import ujson.IncompleteParseException
+
+/** Tests for positive integer refinement type */
+class TestDistanceJsonCodec extends AnyFunSuite, should.Matchers, ScalaCheckPropertyChecks:
+  test("Illegal distance fails with expected IncompleteParseException."):
+    import geometry.given // for the ReadWriter instance
+
+    forAll(
+      Table(
+        ("data", "expectedException"),
+        // Distance must carry units.
+        ("70", QuantityParseException("Unable to parse Length", "70")),
+        // Distance cannot be negative.
+        (
+          "-70 nm",
+          IncompleteParseException(
+            "(parsing -70,0 nm): Allegedly nonnegative length must actually be nonnegative."
+          )
+        )
+      )
+    ) { (data, expectedException) =>
+      val observedException = intercept[expectedException.type] { read[Distance](ujson.Str(data)) }
+      observedException shouldEqual expectedException
+    }
+
+  test("Legal distance roundtrips through JSON"):
+    import geometry.given // for the ReadWriter instance
+
+    given Arbitrary[Distance] = Arbitrary(
+      for
+        u <- Gen.oneOf(Nanometers, Microns, Millimeters)
+        v <- Gen.choose(0.0, Double.MaxValue)
+        l = unsafeBuildLength(v, u)
+      yield Distance
+        .either(l)
+        .fold(_ => throw IllegalRefinement(l, "Cannot refine length as distance"), identity)
+    )
+
+    forAll { (original: Distance) =>
+      val reparsed: Distance = read(write(original))
+      reparsed shouldEqual original
+    }
+
+  private def unsafeBuildLength(value: Int | Double, units: LengthUnit): Length =
+    Length(s"$value ${units.symbol}").fold(throw _, identity)
+end TestDistanceJsonCodec
diff --git a/modules/numeric/src/main/scala/instances/NonnegativeIntInstances.scala b/modules/numeric/src/main/scala/instances/NonnegativeIntInstances.scala
index 8dc6e1f..094175c 100644
--- a/modules/numeric/src/main/scala/instances/NonnegativeIntInstances.scala
+++ b/modules/numeric/src/main/scala/instances/NonnegativeIntInstances.scala
@@ -1,15 +1,14 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-package instances
+package at.ac.oeaw.imba.gerlich.gerlib.numeric.instances
 
-import cats.*
-import io.github.iltotore.iron.cats.given
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
 
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
 
+/** Simple typeclass instances for nonnegative integers */
 trait NonnegativeIntInstances:
-  given IntLike[NonnegativeInt]:
-    override def asInt = identity
-  given Order[NonnegativeInt] = summon[Order[NonnegativeInt]]
-  given Show[NonnegativeInt] = summon[Show[NonnegativeInt]]
-  given SimpleShow[NonnegativeInt] = SimpleShow.fromShow
+  given SimpleShow[Int :| Not[Negative]] =
+    import io.github.iltotore.iron.cats.given_Show_:|
+    SimpleShow.fromShow
 end NonnegativeIntInstances
diff --git a/modules/numeric/src/main/scala/instances/PositiveRealInstances.scala b/modules/numeric/src/main/scala/instances/PositiveRealInstances.scala
index 8c506e2..c89a5b4 100644
--- a/modules/numeric/src/main/scala/instances/PositiveRealInstances.scala
+++ b/modules/numeric/src/main/scala/instances/PositiveRealInstances.scala
@@ -1,17 +1,16 @@
 package at.ac.oeaw.imba.gerlich.gerlib.numeric
 package instances
 
-import cats.*
-import cats.syntax.all.*
-import io.github.iltotore.iron.cats.given
+import cats.Show
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.numeric.Positive
+
 import at.ac.oeaw.imba.gerlich.gerlib.SimpleShow
 
 trait PositiveRealInstances:
-  given Order[PositiveReal] = summon[Order[PositiveReal]]
-  given (ev: Show[Double]) => Show[PositiveReal] =
-    ev.contramap(identity)
-  given (Show[Double]) => SimpleShow[PositiveReal] =
+  given (Show[Double]) => SimpleShow[Double :| Positive] =
+    import io.github.iltotore.iron.cats.given_Show_:|
     SimpleShow.fromShow
-  given Subtraction[PositiveReal, Double, Double]:
-    def minus(minuend: PositiveReal)(subtrahend: Double): Double =
+  given Subtraction[Double :| Positive, Double, Double]:
+    def minus(minuend: Double :| Positive)(subtrahend: Double): Double =
       minuend - subtrahend
diff --git a/modules/numeric/src/main/scala/instances/nonnegativeInt/package.scala b/modules/numeric/src/main/scala/instances/nonnegativeInt/package.scala
index d46c8d9..da41891 100644
--- a/modules/numeric/src/main/scala/instances/nonnegativeInt/package.scala
+++ b/modules/numeric/src/main/scala/instances/nonnegativeInt/package.scala
@@ -1,4 +1,3 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-package instances
+package at.ac.oeaw.imba.gerlich.gerlib.numeric.instances
 
 package object nonnegativeInt extends NonnegativeIntInstances
diff --git a/modules/numeric/src/main/scala/package.scala b/modules/numeric/src/main/scala/package.scala
index 5e446e1..889ce38 100644
--- a/modules/numeric/src/main/scala/package.scala
+++ b/modules/numeric/src/main/scala/package.scala
@@ -2,13 +2,15 @@ package at.ac.oeaw.imba.gerlich.gerlib
 
 import scala.util.Try
 import cats.*
+import cats.data.NonEmptyList
 import cats.syntax.all.*
 
-import io.github.iltotore.iron.*
+import io.github.iltotore.iron.RefinedType
 import io.github.iltotore.iron.constraint.any.Not
 // for summoning Order[Int :| P] or Order[Double :| P]
 import io.github.iltotore.iron.constraint.numeric.*
-import io.github.iltotore.iron.macros.assertCondition
+
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
 /** Numeric tools and types */
 package object numeric:
@@ -35,130 +37,42 @@ package object numeric:
       def contramap[A, B](fa: IntLike[A])(f: B => A): IntLike[B] = new:
         def asInt: B => Int = f `andThen` fa.asInt
 
-  /** Error subtype for when refinement of a negative integer as nonnegative is attempted
-    *
-    * @param getInt
-    *   The integer to refine as nonnegative
-    * @param context
-    *   The context (e.g., purpose) in which the refinement's being attempted; this is used to craft
-    *   a more informative error message
-    */
-  final case class IllegalRefinement[A] private[numeric] (
-      rawValue: A,
-      msg: String,
-      context: Option[String]
-  ) extends IllegalArgumentException(
-        s"Cannot refine value $rawValue: $msg.${context
-            .fold("")(ctx => s" Context: $ctx")}"
+  /** Refinement type for nonnegative integers */
+  type NonnegativeInt = NonnegativeInt.T
+
+  /** Helpers for working with nonnegative integers */
+  object NonnegativeInt extends RefinedType[Int, Not[Negative]]:
+    def indexed[F[_]: Functor, A](ais: F[(A, Int)]): F[(A, NonnegativeInt)] =
+      ais.map((a, i) =>
+        a -> NonnegativeInt.either(i).fold(msg => throw IllegalRefinement(i, msg), identity)
       )
 
-  /** Builders for [[IllegalRefinement]] */
-  object IllegalRefinement:
-    /** No additional message context */
-    private[numeric] def apply[A](value: A, msg: String): IllegalRefinement[A] =
-      new IllegalRefinement(value, msg, None)
-
-    /** Add additional message context. */
-    private[numeric] def apply[A](
-        value: A,
-        msg: String,
-        ctx: String
-    ): IllegalRefinement[A] =
-      new IllegalRefinement(value, msg, ctx.some)
-
-  /** Enrich [[io.github.iltotore.iron.RefinedTypeOps]] with semantic context for error messages,
-    * and a parser.
-    *
-    * @tparam V
-    *   The type of value to refine with constraint/predicate
-    * @tparam P
-    *   The constraint/predicate by which to refine values
-    * @see
-    *   [[io.github.iltotore.iron.RefinedTypeOps]]
-    */
-  private sealed trait RefinementBuilder[V, P] extends RefinedTypeOps.Transparent[V :| P]:
-    /** Compile-time refinement of a {@code V} acc. to predicate {@code P} , with constructor-like
-      * syntax
-      *
-      * @param v
-      *   The value to test under predicate/constraint {@code P}
-      * @param constraint
-      *   The predicate under which to test a given value
-      * @see
-      *   [[io.github.iltotore.iron.autoRefine]]
-      */
-    inline def apply(inline v: V)(using
-        inline constraint: Constraint[V, P]
-    ): V :| P =
-      assertCondition(v, constraint.test(v), constraint.message)
-      IronType(v)
-
-    /** How to safely try to get a raw value {@code V} from text */
-    protected def parseRaw: String => Either[String, V]
-
-    /** Alias for {@code option} */
-    final def maybe(v: V): Option[V :| P] = option(v)
-
-    /** Provide a safe parser of {@code V :| P} from text */
-    def parse: String => Either[String, V :| P] =
-      parseRaw.map(_.flatMap(either))
-
-    /** Modify the parent trait's {@code either} member by injecting semantic context into fail
-      * message.
-      */
-    final def unsafe: V => V :| P = v =>
-      either(v).fold(msg => throw IllegalRefinement(v, msg), identity)
-
-  /** Alias to hide implementation choice of Not[Negative] vs. GreaterEqual[0] vs., e.g.,
-    * Not[Less[0]]
-    */
-  private[gerlib] type Nonnegative = Not[Negative]
+    def indexed[A](as: List[A]): List[(A, NonnegativeInt)] = indexed(as.zipWithIndex)
 
-  /** Refinement type for nonnegative integers */
-  type NonnegativeInt = Int :| Nonnegative
+    def indexed[A](as: NonEmptyList[A]): NonEmptyList[(A, NonnegativeInt)] = indexed(
+      as.zipWithIndex
+    )
 
-  /** Helpers for working with nonnegative integers */
-  object NonnegativeInt extends RefinementBuilder[Int, Nonnegative]:
-    override protected def parseRaw: String => Either[String, Int] = readAsInt
-
-    def indexed[A](as: List[A]): List[(A, NonnegativeInt)] =
-      as.zipWithIndex.map: (a, i) =>
-        a -> unsafe(i)
-
-    // Add a pair of nonnegative numbers, ensuring that the result stays as a nonnegative.
-    extension (n: NonnegativeInt)
-      infix def add(m: NonnegativeInt): NonnegativeInt =
-        either(n + m) match
-        case Left(msg) =>
-          throw new ArithmeticException(s"Uh-Oh! $n + $m = ${n + m}; $msg")
-        case Right(result) => result
+    def parse = (s: String) => Try(s.toInt).toEither.leftMap(_.getMessage).flatMap(either)
   end NonnegativeInt
 
   /** Nonnegative real number */
-  type NonnegativeReal = Double :| Nonnegative
+  type NonnegativeReal = NonnegativeReal.T
 
   /** Helpers for working with nonnegative real numbers */
-  object NonnegativeReal extends RefinementBuilder[Double, Nonnegative]:
-    override protected def parseRaw: String => Either[String, Double] =
-      readAsDouble
-  end NonnegativeReal
+  object NonnegativeReal extends RefinedType[Double, Not[Negative]]
 
   /** Refinement type for positive integers */
-  type PositiveInt = Int :| Positive
+  type PositiveInt = PositiveInt.T
 
   /** Helpers for working with positive integers */
-  object PositiveInt extends RefinementBuilder[Int, Positive]:
-    override protected def parseRaw: String => Either[String, Int] = readAsInt
-  end PositiveInt
+  object PositiveInt extends RefinedType[Int, Positive]
 
   /** Positive real number */
-  type PositiveReal = Double :| Positive
+  type PositiveReal = PositiveReal.T
 
   /** Helpers for working with positive real numbers */
-  object PositiveReal extends RefinementBuilder[Double, Positive]:
-    override protected def parseRaw: String => Either[String, Double] =
-      readAsDouble
-  end PositiveReal
+  object PositiveReal extends RefinedType[Double, Positive]
 
   /** Attempt to parse the given text as integer, wrapping error message as a [[scala.util.Left]]
     * for fail.
@@ -176,7 +90,7 @@ package object numeric:
     *
     * @tparam T
     *   The target type
-    * @param aName
+    * @param targetName
     *   The name of the target type, used to contextualise error message
     * @param lift
     *   How to lift raw nonnegative integer into target type
@@ -184,9 +98,11 @@ package object numeric:
     *   Either a [[scala.util.Left]]-wrapped error message, or a [[scala.util.Right]]-wrapped parsed
     *   value
     */
-  def parseThroughNonnegativeInt[T](aName: String)(
+  def parseThroughNonnegativeInt[T](targetName: String)(
       lift: NonnegativeInt => T
-  ): String => Either[String, T] =
-    s => NonnegativeInt.parse(s).bimap(msg => s"For $aName -- $msg", lift)
+  ): String => Either[String, T] = s =>
+    readAsInt(s)
+      .flatMap(NonnegativeInt.either)
+      .bimap(msg => s"For $targetName -- $msg", lift)
 
 end numeric
diff --git a/modules/numeric/src/main/scala/syntax/SyntaxForPositiveInt.scala b/modules/numeric/src/main/scala/syntax/SyntaxForPositiveInt.scala
deleted file mode 100644
index 4ccd8af..0000000
--- a/modules/numeric/src/main/scala/syntax/SyntaxForPositiveInt.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-package syntax
-
-import io.github.iltotore.iron.refineUnsafe
-
-trait SyntaxForPositiveInt:
-  /** Enable the refinement of autoRefine in client code where the import's not present.
-    */
-  extension (x: PositiveInt) def asNonnegative: NonnegativeInt = x.refineUnsafe
diff --git a/modules/numeric/src/main/scala/syntax/SyntaxForPositiveReal.scala b/modules/numeric/src/main/scala/syntax/SyntaxForPositiveReal.scala
deleted file mode 100644
index 1fb7730..0000000
--- a/modules/numeric/src/main/scala/syntax/SyntaxForPositiveReal.scala
+++ /dev/null
@@ -1,9 +0,0 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-package syntax
-
-import io.github.iltotore.iron.refineUnsafe
-
-trait SyntaxForPositiveReal:
-  /** Enable the refinement of autoRefine in client code where the import's not present.
-    */
-  extension (x: PositiveReal) def asNonnegative: NonnegativeReal = x.refineUnsafe
diff --git a/modules/numeric/src/main/scala/syntax/package.scala b/modules/numeric/src/main/scala/syntax/package.scala
deleted file mode 100644
index b961f3a..0000000
--- a/modules/numeric/src/main/scala/syntax/package.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-
-package object syntax:
-  object all extends AllSyntax
-
-  trait AllSyntax extends SyntaxForPositiveInt, SyntaxForPositiveReal
diff --git a/modules/numeric/src/main/scala/syntax/positiveInt.scala b/modules/numeric/src/main/scala/syntax/positiveInt.scala
deleted file mode 100644
index 144fc4e..0000000
--- a/modules/numeric/src/main/scala/syntax/positiveInt.scala
+++ /dev/null
@@ -1,4 +0,0 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-package syntax
-
-package object positiveInt extends SyntaxForPositiveInt
diff --git a/modules/numeric/src/main/scala/syntax/positiveReal.scala b/modules/numeric/src/main/scala/syntax/positiveReal.scala
deleted file mode 100644
index 2dc6c10..0000000
--- a/modules/numeric/src/main/scala/syntax/positiveReal.scala
+++ /dev/null
@@ -1,4 +0,0 @@
-package at.ac.oeaw.imba.gerlich.gerlib.numeric
-package syntax
-
-package object positiveReal extends SyntaxForPositiveReal
diff --git a/modules/numeric/src/test/scala/TestNonnegativeInt.scala b/modules/numeric/src/test/scala/TestNonnegativeInt.scala
index 136c37a..24db06a 100644
--- a/modules/numeric/src/test/scala/TestNonnegativeInt.scala
+++ b/modules/numeric/src/test/scala/TestNonnegativeInt.scala
@@ -1,37 +1,19 @@
 package at.ac.oeaw.imba.gerlich.gerlib.numeric
 
-import scala.annotation.nowarn
-import scala.util.Try
-import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.Negative
 import org.scalacheck.{Arbitrary, Gen}
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should
 import org.scalatest.prop.Configuration.PropertyCheckConfiguration
 import org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
 
-import io.github.iltotore.iron.constraint.any.Not
-import io.github.iltotore.iron.constraint.numeric.Negative
-import io.github.iltotore.iron.scalacheck.numeric.intervalArbitrary
-
 /** Tests for positive integer refinement type */
 class TestNonnegativeInt extends AnyFunSuite, should.Matchers, ScalaCheckPropertyChecks:
   override implicit val generatorDrivenConfig: PropertyCheckConfiguration =
     PropertyCheckConfiguration(minSuccessful = 100)
 
-  test(
-    "NonnegativeInt correctly restricts which expressions compile by direct assignment."
-  ) {
-    // NB: autoRefine is required for this (raw, non-constructor) syntax of type refinement.
-    assertCompiles(
-      "import io.github.iltotore.iron.autoRefine; val one: NonnegativeInt = 1"
-    )
-    assertTypeError("val one: NonnegativeInt = 1")
-    assertCompiles(
-      "import io.github.iltotore.iron.autoRefine; val zero: NonnegativeInt = 0"
-    )
-    assertTypeError("val moinsDeux: NonnegativeInt = -2")
-  }
-
   test(
     "NonnegativeInt correctly restricts which expressions compile by constructor syntax."
   ) {
@@ -41,80 +23,28 @@ class TestNonnegativeInt extends AnyFunSuite, should.Matchers, ScalaCheckPropert
     assertTypeError("NonnegativeInt(-2)")
   }
 
-  test("NonnegativeInt.maybe behaves correctly.") {
+  test("NonnegativeInt.option behaves correctly.") {
     forAll { (z: Int) =>
-      NonnegativeInt.maybe(z) match
+      NonnegativeInt.option(z) match
       case None if z < 0     => succeed
       case Some(n) if z >= 0 => z shouldEqual n
       case bad               => fail(s"NonnegativeInt.maybe($z) gave bad result: $bad")
     }
   }
 
-  test("NonnegativeInt.parse behaves correctly.") {
-    type InOut = (String, Either[String, NonnegativeInt])
-    def genInOutLegit: Gen[InOut] =
-      intervalArbitrary[Int, Not[Negative]](0, Int.MaxValue).arbitrary
-        .map: n =>
-          n.toString -> n.asRight
-    def genNegative: Gen[InOut] =
-      Gen
-        .choose(Int.MinValue, -1)
-        .map { z => z.toString -> "!(Should be strictly negative)".asLeft }
-    def genRandom: Gen[InOut] =
-      Arbitrary
-        .arbitrary[String]
-        .filter: s =>
-          Try:
-            s.toInt
-          .toOption.isEmpty
-        .map: s =>
-          s -> s"Cannot read as integer: $s".asLeft
-    def genInOut: Gen[InOut] = Gen.oneOf(
-      genInOutLegit,
-      genNegative,
-      genRandom
-    )
-    forAll(genInOut): (in, out) =>
-      NonnegativeInt.parse(in) shouldEqual out
-  }
-
-  test(
-    "NonnegativeInt.unsafe behaves in accordance with its safe counterpart."
-  ) {
-    forAll { (z: Int) =>
-      NonnegativeInt.either(z) match
-      case Left(_) =>
-        assertThrows[IllegalRefinement[Int]]:
-          NonnegativeInt.unsafe(z)
-      case Right(n) => n shouldEqual NonnegativeInt.unsafe(z)
-    }
-  }
-
-  test("NonnegativeInt is a transparent type alias for Int :| Not[Negative]") {
-    import io.github.iltotore.iron.{:|, autoRefine}
-    assertCompiles {
-      "val ironRef: Int :| Not[Negative] = 0; val aliased: NonnegativeInt = ironRef"
-    }
-    assertCompiles {
-      "val aliased: NonnegativeInt = NonnegativeInt(0); val ironRef: Int :| Not[Negative] = aliased"
-    }
-  }: @nowarn
-
-  test("NonnegativeInt's predicate is Not[Negative], not GreaterEqual[0]") {
-    import io.github.iltotore.iron.{:|, autoRefine}
-    import io.github.iltotore.iron.constraint.any.StrictEqual
-    import io.github.iltotore.iron.constraint.numeric.{Greater, GreaterEqual}
-    /* With GreaterEqual[0] */
-    assertCompiles:
-      "val ironRef: Int :| GreaterEqual[0] = 0"
-    assertTypeError {
-      "val ironRef: Int :| GreaterEqual[0] = 0; val aliased: NonnegativeInt = ironRef"
-    }
+  test("The SimpleShow instance for nonnegative integer just shows the number."):
+    import at.ac.oeaw.imba.gerlich.gerlib.syntax.all.*
+    import at.ac.oeaw.imba.gerlich.gerlib.numeric.instances.nonnegativeInt.given_SimpleShow_:|
+    import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
-    /* With Greater[0] | StrictEqual[0] */
-    assertCompiles { "val ironRef: Int :| (Greater[0] | StrictEqual[0]) = 0" }
-    assertTypeError {
-      "val ironRef: Int :| (Greater[0] | StrictEqual[0]) = 0; val aliased: NonnegativeInt = ironRef"
-    }
-  }: @nowarn
+    given Arbitrary[Int :| Not[Negative]] = Arbitrary:
+      Gen
+        .choose(0, Int.MaxValue)
+        .map(z =>
+          NonnegativeInt.option(z).getOrElse {
+            throw IllegalRefinement(z, "Can't refine as nonnegative")
+          }
+        )
+
+    forAll { (n: Int :| Not[Negative]) => n.show_ shouldEqual n.toString }
 end TestNonnegativeInt
diff --git a/modules/numeric/src/test/scala/TestPositiveInt.scala b/modules/numeric/src/test/scala/TestPositiveInt.scala
index 4f833f8..bec701c 100644
--- a/modules/numeric/src/test/scala/TestPositiveInt.scala
+++ b/modules/numeric/src/test/scala/TestPositiveInt.scala
@@ -1,37 +1,16 @@
 package at.ac.oeaw.imba.gerlich.gerlib.numeric
 
-import scala.annotation.nowarn
-import scala.util.Try
-import cats.syntax.all.*
-import org.scalacheck.{Arbitrary, Gen}
+import org.scalacheck.Arbitrary
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should
 import org.scalatest.prop.Configuration.PropertyCheckConfiguration
 import org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
 
-import io.github.iltotore.iron.constraint.numeric.Positive
-import io.github.iltotore.iron.scalacheck.numeric.intervalArbitrary
-
 /** Tests for positive integer refinement type */
 class TestPositiveInt extends AnyFunSuite, should.Matchers, ScalaCheckPropertyChecks:
   override implicit val generatorDrivenConfig: PropertyCheckConfiguration =
     PropertyCheckConfiguration(minSuccessful = 100)
 
-  test(
-    "PositiveInt correctly restricts which expressions compile by direct assignment."
-  ) {
-    // NB: autoRefine is required for this (raw, non-constructor) syntax of type refinement.
-    assertCompiles(
-      "import io.github.iltotore.iron.autoRefine; val one: PositiveInt = 1"
-    )
-    assertTypeError("val one: PositiveInt = 1")
-    assertTypeError("val zero: PositiveInt = 0")
-    assertTypeError(
-      "import io.github.iltotore.iron.autoRefine; val zero: PositiveInt = 0"
-    )
-    assertTypeError("val moinsDeux: PositiveInt = -2")
-  }
-
   test(
     "PositiveInt correctly restricts which expressions compile by constructor syntax."
   ) {
@@ -41,61 +20,12 @@ class TestPositiveInt extends AnyFunSuite, should.Matchers, ScalaCheckPropertyCh
     assertTypeError("PositiveInt(-2)")
   }
 
-  test("PositiveInt.maybe behaves correctly.") {
+  test("PositiveInt.option behaves correctly.") {
     forAll { (z: Int) =>
-      PositiveInt.maybe(z) match
+      PositiveInt.option(z) match
       case None if z <= 0   => succeed
       case Some(n) if z > 0 => z shouldEqual n
       case bad              => fail(s"PositiveInt.maybe($z) gave bad result: $bad")
     }
   }
-
-  test("NonnegativeInt.parse behaves correctly.") {
-    type InOut = (String, Either[String, PositiveInt])
-    def genInOutLegit: Gen[InOut] =
-      intervalArbitrary[Int, Positive](1, Int.MaxValue).arbitrary
-        .map: n =>
-          n.toString -> n.asRight
-    def genNegative: Gen[InOut] =
-      Gen
-        .choose(Int.MinValue, -1)
-        .map { z => z.toString -> "!(Should be strictly negative)".asLeft }
-    def genRandom: Gen[InOut] =
-      Arbitrary
-        .arbitrary[String]
-        .filter: s =>
-          Try:
-            s.toInt
-          .toOption.isEmpty
-        .map: s =>
-          s -> s"Cannot read as integer: $s".asLeft
-    def genInOut: Gen[InOut] = Gen.oneOf(
-      genInOutLegit,
-      genNegative,
-      genRandom
-    )
-    forAll(genInOut): (in, out) =>
-      NonnegativeInt.parse(in) shouldEqual out
-  }
-
-  test("PositiveInt.unsafe behaves in accordance with its safe counterpart.") {
-    forAll { (z: Int) =>
-      PositiveInt.either(z) match
-      case Left(_) =>
-        assertThrows[IllegalRefinement[Int]]:
-          PositiveInt.unsafe(z)
-      case Right(n) => n shouldEqual PositiveInt.unsafe(z)
-    }
-  }
-
-  test("PositiveInt is a transparent type alias for Int :| Positive") {
-    import io.github.iltotore.iron.{:|, autoRefine}
-    import io.github.iltotore.iron.constraint.numeric.Positive
-    assertCompiles {
-      "val ironRef: Int :| Positive = 1; val aliased: PositiveInt = ironRef"
-    }
-    assertCompiles {
-      "val aliased: PositiveInt = PositiveInt(1); val ironRef: Int :| Positive = aliased"
-    }
-  }: @nowarn
 end TestPositiveInt
diff --git a/modules/refinement/src/main/scala/package.scala b/modules/refinement/src/main/scala/package.scala
new file mode 100644
index 0000000..7d38c1f
--- /dev/null
+++ b/modules/refinement/src/main/scala/package.scala
@@ -0,0 +1,39 @@
+package at.ac.oeaw.imba.gerlich.gerlib
+
+import cats.syntax.all.*
+
+package object refinement:
+  /** Error subtype for when refinement of a negative integer as nonnegative is attempted
+    *
+    * @param rawValue
+    *   The value to refine
+    * @param msg
+    *   The initial refinement failure message
+    * @param context
+    *   The context (e.g., purpose) in which the refinement's being attempted; this is used to craft
+    *   a more informative error message
+    */
+  final case class IllegalRefinement[A] private[refinement] (
+      rawValue: A,
+      msg: String,
+      context: Option[String]
+  ) extends IllegalArgumentException(
+        s"Cannot refine value $rawValue: $msg.${context
+            .fold("")(ctx => s" Context: $ctx")}"
+      )
+
+  /** Builders for [[IllegalRefinement]] */
+  object IllegalRefinement:
+    /** No additional message context */
+    def apply[A](value: A, msg: String): IllegalRefinement[A] =
+      new IllegalRefinement(value, msg, None)
+
+    /** Add additional message context. */
+    private[refinement] def apply[A](
+        value: A,
+        msg: String,
+        ctx: String
+    ): IllegalRefinement[A] =
+      new IllegalRefinement(value, msg, ctx.some)
+  end IllegalRefinement
+end refinement
diff --git a/modules/roi/src/main/scala/measurement.scala b/modules/roi/src/main/scala/measurement.scala
index ad76259..256d823 100644
--- a/modules/roi/src/main/scala/measurement.scala
+++ b/modules/roi/src/main/scala/measurement.scala
@@ -2,52 +2,55 @@ package at.ac.oeaw.imba.gerlich.gerlib.roi
 
 import cats.Order
 import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.{Negative, Positive}
 
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
 
 package object measurement:
   /** Area of a region of interest */
-  opaque type Area = PositiveReal
+  opaque type Area = Double :| Positive
 
   /** Helpers for working with geometric area */
   object Area:
     extension (a: Area) private[gerlib] def toDouble: Double = a
 
     /** Semantically designate the raw numeric value as an area. */
-    def apply(a: PositiveReal): Area = a: Area
+    def apply(a: Double :| Positive): Area = a: Area
 
     /** Attempt to semantically designate the raw numeric value as an area. */
     def fromDouble(x: Double): Either[String, Area] =
       PositiveReal.either(x).map(apply)
 
     /** Use normal numeric ordering for ROI area values. */
-    given (ordPosNum: Order[PositiveReal]) => Order[Area] =
+    given (ordPosNum: Order[Double :| Positive]) => Order[Area] =
       ordPosNum.contramap(identity)
 
     /** Attempt to read the given text as a ROI area value. */
-    def parse(s: String): Either[String, Area] = PositiveReal.parse(s)
+    def parse(s: String): Either[String, Area] = readAsDouble(s).flatMap(PositiveReal.either)
   end Area
 
   /** Mean values in a region of interest */
-  opaque type MeanIntensity = NonnegativeReal
+  opaque type MeanIntensity = Double :| Not[Negative]
 
   /** Helpers for working with ROI mean intensity measurement */
   object MeanIntensity:
     extension (i: MeanIntensity) private[gerlib] def toDouble: Double = i
 
     /** Semantically designate the raw numeric value as an area. */
-    def apply(i: NonnegativeReal): MeanIntensity = i: MeanIntensity
+    def apply(i: Double :| Not[Negative]): MeanIntensity = i: MeanIntensity
 
     /** Attempt to semantically designate the raw numeric value as an area. */
     def fromDouble(x: Double): Either[String, MeanIntensity] =
       NonnegativeReal.either(x).map(apply)
 
     /** Use normal numeric ordering for ROI mean intensity values. */
-    given (ordNonNegNum: Order[NonnegativeReal]) => Order[MeanIntensity] =
+    given (ordNonNegNum: Order[Double :| Not[Negative]]) => Order[MeanIntensity] =
       ordNonNegNum.contramap(identity)
 
     /** Attempt to read the given text as a ROI mean intensity value. */
     def parse(s: String): Either[String, MeanIntensity] =
-      NonnegativeReal.parse(s)
+      readAsDouble(s).flatMap(NonnegativeReal.either)
   end MeanIntensity
 end measurement
diff --git a/modules/roi/src/test/scala/RoiTestSuite.scala b/modules/roi/src/test/scala/RoiTestSuite.scala
index 9fe5cdd..9d626be 100644
--- a/modules/roi/src/test/scala/RoiTestSuite.scala
+++ b/modules/roi/src/test/scala/RoiTestSuite.scala
@@ -3,9 +3,16 @@ package at.ac.oeaw.imba.gerlich.gerlib.roi
 import org.scalacheck.*
 
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.PositiveInt
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
 /** Functionality common to ROI-related test suites. */
 trait RoiTestSuite:
   given Arbitrary[PositiveInt] = Arbitrary:
-    Gen.posNum[Int].map(PositiveInt.unsafe)
+    Gen
+      .posNum[Int]
+      .map(n =>
+        PositiveInt
+          .option(n)
+          .getOrElse { throw IllegalRefinement(n, "Cannot refine as positive") }
+      )
 end RoiTestSuite
diff --git a/modules/testing/src/main/scala/instances/ImagingInstances.scala b/modules/testing/src/main/scala/instances/ImagingInstances.scala
index 13300ae..349a4d2 100644
--- a/modules/testing/src/main/scala/instances/ImagingInstances.scala
+++ b/modules/testing/src/main/scala/instances/ImagingInstances.scala
@@ -5,18 +5,19 @@ import cats.syntax.all.*
 import org.scalacheck.*
 
 import io.github.iltotore.iron.:|
-import io.github.iltotore.iron.constraint.any.StrictEqual
+import io.github.iltotore.iron.constraint.any.{Not, StrictEqual}
 import io.github.iltotore.iron.constraint.char.{Digit, Letter}
+import io.github.iltotore.iron.constraint.numeric.Negative
 
 import at.ac.oeaw.imba.gerlich.gerlib.imaging.*
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
 
 /** Scalacheck typeclass instances for some of the imaging datatypes */
 trait ImagingInstances extends CatsScalacheckInstances:
   /** [[org.scalacheck.Arbitrary]] instance for generating a
     * [[at.ac.oeaw.imba.gerlich.gerlib.imaging.FieldOfView]] value
     */
-  given (arbNN: Arbitrary[NonnegativeInt]) => Arbitrary[FieldOfView] = arbNN.map(FieldOfView.apply)
+  given (arbNN: Arbitrary[Int :| Not[Negative]]) => Arbitrary[FieldOfView] =
+    arbNN.map(FieldOfView.apply)
 
   /** Use the given instances of letter or digit generators as the base. */
   given (Arbitrary[Char :| Letter], Arbitrary[Char :| Digit]) => Arbitrary[PositionName] =
@@ -65,14 +66,14 @@ trait ImagingInstances extends CatsScalacheckInstances:
     * [[at.ac.oeaw.imba.gerlich.gerlib.imaging.ImagingChannel]] value
     */
   given (
-      arbNN: Arbitrary[NonnegativeInt]
+      arbNN: Arbitrary[Int :| Not[Negative]]
   ) => Arbitrary[ImagingChannel] = arbNN.map(ImagingChannel.apply)
 
   /** [[org.scalacheck.Arbitrary]] instance for generating a
     * [[at.ac.oeaw.imba.gerlich.gerlib.imaging.ImagingTimepoint]] value
     */
   given (
-      arbNN: Arbitrary[NonnegativeInt]
+      arbNN: Arbitrary[Int :| Not[Negative]]
   ) => Arbitrary[ImagingTimepoint] = arbNN.map(ImagingTimepoint.apply)
 
   given (
diff --git a/modules/testing/src/main/scala/instances/NumericInstances.scala b/modules/testing/src/main/scala/instances/NumericInstances.scala
index 3afc242..4836d3b 100644
--- a/modules/testing/src/main/scala/instances/NumericInstances.scala
+++ b/modules/testing/src/main/scala/instances/NumericInstances.scala
@@ -4,7 +4,8 @@ package instances
 import org.scalacheck.*
 
 import io.github.iltotore.iron.:|
-import io.github.iltotore.iron.constraint.numeric.Positive
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.{Negative, Positive}
 import io.github.iltotore.iron.scalacheck.numeric.intervalArbitrary
 
 import at.ac.oeaw.imba.gerlich.gerlib.numeric.*
@@ -12,6 +13,7 @@ import at.ac.oeaw.imba.gerlich.gerlib.testing.GeneratorBound.{
   Lower as LowerBound,
   Upper as UpperBound
 }
+import at.ac.oeaw.imba.gerlich.gerlib.refinement.IllegalRefinement
 
 /** Tools for writing property-based tests involving custom numeric types */
 trait NumericInstances:
@@ -24,8 +26,8 @@ trait NumericInstances:
     ): Gen[NonnegativeInt] =
       Gen
         .choose[Int](min, max)
-        .map:
-          NonnegativeInt.unsafe
+        .map: i =>
+          NonnegativeInt.either(i).fold(msg => throw IllegalRefinement(i, msg), identity)
 
   /** Choose a positive integer through the Choose[Int], then unsafely refine.
     */
@@ -33,8 +35,8 @@ trait NumericInstances:
     override def choose(min: PositiveInt, max: PositiveInt): Gen[PositiveInt] =
       Gen
         .choose[Int](min, max)
-        .map:
-          PositiveInt.unsafe
+        .map: i =>
+          PositiveInt.either(i).fold(msg => throw IllegalRefinement(i, msg), identity)
 
   /** [[org.scalacheck.Arbitrary]] instance for generating bounded numeric type, subject to the
     * given bounds.
@@ -45,15 +47,15 @@ trait NumericInstances:
   ) => Arbitrary[V :| P] =
     intervalArbitrary[V, P](lo.value, hi.value)
 
-  given nonnegativeIntArbitrary: Arbitrary[NonnegativeInt] =
-    intervalArbitrary[Int, Nonnegative](0, Int.MaxValue)
+  given nonnegativeIntArbitrary: Arbitrary[Int :| Not[Negative]] =
+    intervalArbitrary[Int, Not[Negative]](0, Int.MaxValue)
 
-  given positiveIntArbitrary: Arbitrary[PositiveInt] =
+  given positiveIntArbitrary: Arbitrary[Int :| Positive] =
     intervalArbitrary[Int, Positive](1, Int.MaxValue)
 
-  given nonnegativeRealArbitrary: Arbitrary[NonnegativeReal] =
-    intervalArbitrary[Double, Nonnegative](0, Double.MaxValue)
+  given nonnegativeRealArbitrary: Arbitrary[Double :| Not[Negative]] =
+    intervalArbitrary[Double, Not[Negative]](0, Double.MaxValue)
 
-  given positiveRealArbitrary: Arbitrary[PositiveReal] =
+  given positiveRealArbitrary: Arbitrary[Double :| Positive] =
     intervalArbitrary[Double, Positive](1 / Double.MaxValue, Double.MaxValue)
 end NumericInstances
diff --git a/modules/testing/src/main/scala/instances/RoiInstances.scala b/modules/testing/src/main/scala/instances/RoiInstances.scala
index ad0bef8..ba97414 100644
--- a/modules/testing/src/main/scala/instances/RoiInstances.scala
+++ b/modules/testing/src/main/scala/instances/RoiInstances.scala
@@ -4,13 +4,14 @@ package instances
 import scala.util.NotGiven
 import cats.Order
 import cats.syntax.all.*
+import io.github.iltotore.iron.:|
+import io.github.iltotore.iron.constraint.any.Not
+import io.github.iltotore.iron.constraint.numeric.{Negative, Positive}
 
 import org.scalacheck.*
 import at.ac.oeaw.imba.gerlich.gerlib.geometry.*
 import at.ac.oeaw.imba.gerlich.gerlib.geometry.instances.coordinate.given
 import at.ac.oeaw.imba.gerlich.gerlib.imaging.ImagingContext
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.NonnegativeReal
-import at.ac.oeaw.imba.gerlich.gerlib.numeric.PositiveReal
 import at.ac.oeaw.imba.gerlich.gerlib.roi.DetectedSpot
 import at.ac.oeaw.imba.gerlich.gerlib.roi.measurement.{Area, MeanIntensity}
 import at.ac.oeaw.imba.gerlich.gerlib.testing.instances.catsScalacheck.given
@@ -36,10 +37,10 @@ trait RoiInstances:
   ) => Arbitrary[DetectedSpot[C]] =
     (arbCtx, arbCenter, arbArea, arbIntensity).mapN(DetectedSpot.apply)
 
-  given (arbRaw: Arbitrary[PositiveReal]) => Arbitrary[Area] =
+  given (arbRaw: Arbitrary[Double :| Positive]) => Arbitrary[Area] =
     arbRaw.map(Area.apply)
 
-  given (arbRaw: Arbitrary[NonnegativeReal]) => Arbitrary[MeanIntensity] =
+  given (arbRaw: Arbitrary[Double :| Not[Negative]]) => Arbitrary[MeanIntensity] =
     arbRaw.map(MeanIntensity.apply)
 
   /** Generate an arbitrary interval along a particular axis. */
diff --git a/modules/zarr/src/main/scala/OmeZarrDimension.scala b/modules/zarr/src/main/scala/OmeZarrDimension.scala
index 2efb720..2a729f4 100644
--- a/modules/zarr/src/main/scala/OmeZarrDimension.scala
+++ b/modules/zarr/src/main/scala/OmeZarrDimension.scala
@@ -150,8 +150,7 @@ object OmeZarr:
     def fromDimensions(
         dims: NonEmptyList[OmeZarrDimension]
     ): Either[NonEmptyList[String], IndexMapping] =
-      val indexedDims =
-        dims.zipWithIndex.map((d, i) => d -> NonnegativeInt.unsafe(i))
+      val indexedDims = NonnegativeInt.indexed(dims)
       if indexedDims.length =!= 5
       then
         NonEmptyList
diff --git a/modules/zarr/src/main/scala/OmeZarrIndex.scala b/modules/zarr/src/main/scala/OmeZarrIndex.scala
index 54c9ada..d3d5bfc 100644
--- a/modules/zarr/src/main/scala/OmeZarrIndex.scala
+++ b/modules/zarr/src/main/scala/OmeZarrIndex.scala
@@ -20,21 +20,21 @@ object OmeZarrIndex:
 
   object Z:
     def fromDouble: Double => Option[Z] =
-      ((_: Double).toInt).andThen(NonnegativeInt.maybe)
+      ((_: Double).toInt).andThen(NonnegativeInt.option)
 
   /** Index into y dimension of ZARR array */
   opaque type Y = NonnegativeInt
 
   object Y:
     def fromDouble: Double => Option[Y] =
-      ((_: Double).toInt).andThen(NonnegativeInt.maybe)
+      ((_: Double).toInt).andThen(NonnegativeInt.option)
 
   /** Index into x dimension of ZARR array */
   opaque type X = NonnegativeInt
 
   object X:
     def fromDouble: Double => Option[X] =
-      ((_: Double).toInt).andThen(NonnegativeInt.maybe)
+      ((_: Double).toInt).andThen(NonnegativeInt.option)
 
   /** Index of "point" in standard OME-ZARR coordinate space */
   final case class OmeZarrStandardCoordinate(
diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index db6e23a..ed12aa0 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -7,7 +7,7 @@ object Dependencies {
         def moduleId = getModuleID(None)
         def getModuleID(name: String): ModuleID = getModuleID(Some(name))
         private def getModuleID(name: Option[String]): ModuleID = 
-            "io.github.iltotore" %% ("iron" ++ name.fold("")("-" ++ _)) % "2.6.0" 
+            "io.github.iltotore" %% ("iron" ++ name.fold("")("-" ++ _)) % "3.0.0" 
     }
 
     /** Build ModuleID for a com.lihaoyi JSON-related project. */
@@ -31,6 +31,9 @@ object Dependencies {
     lazy val uJson = HaoyiJson.getModuleId("ujson")
     lazy val uPickle = HaoyiJson.getModuleId("upickle")
     
+    /* geometry dependencies */
+    lazy val squants = "org.typelevel" %% "squants" % "1.8.3"
+
     /* graph dependencies */
     lazy val scalaGraphCore = "org.scala-graph" %% "graph-core" % "2.0.2"