Create an instance of Int :| Positive from 0 without exceptions.

[GoogeTan]

Scala environment: JVM Scala version: 3.3.1 Iron version: 2.3.0

Reproduction steps Run the code:

scala> List[Int]().map(_.refine[Greater[0]]).sum
val res2:
  io.github.iltotore.iron.package$package.IronType[Int,
    io.github.iltotore.iron.constraint.numeric.Greater[0]] = 0

Expected behavior I've expected it not to compile or throw an exception in runtime.

Current behavior Invalid state accured.

[Iltotore]

What are your imports? Numeric[T] is invariant according to Scala's documentation so it could not be Scala's Numeric[Int] instance.

[GoogeTan]

Only two:

import io.github.iltotore.iron.{*, given}
import io.github.iltotore.iron.constraint.numeric.Greater

And scala's preimported packages

[GoogeTan]

In case I create my own function:

def test[T](lst : List[T])(using n : Numeric[T]) = { println(n); n.zero }

It prints:

scala> test(List[Int]().map(_.refine[Greater[0]]))
scala.math.Numeric$IntIsIntegral$@7ef7faa9
val res1:
  io.github.iltotore.iron.package$package.IronType[Int,
    io.github.iltotore.iron.constraint.numeric.Greater[0]] = 0

[Iltotore]

What happen if you make your own version of sum using the Numeric typeclass? Does using it with Int :| Positive compile?

[GoogeTan]

scala> def sum[T](lst : List[T])(using n : Numeric[T]) : T = lst.fold(n.zero)(n.plus)
def sum[T](lst: List[T])(using n: Numeric[T]): T
scala> import io.github.iltotore.iron.{*, given}
 import io.github.iltotore.iron.constraint.numeric.Greater
 import io.github.iltotore.iron.constraint.all.Positive
scala> val list = List[Int]().map(_.refine[Greater[0]])
scala> sum(list)
val res0:
  io.github.iltotore.iron.package$package.IronType[Int,
    io.github.iltotore.iron.constraint.numeric.Greater[0]] = 0
 scala> sum[Int :| Positive](List())
 scala> -- [E172] Type Error: ----------------------------------------------------------
1 |sum[Int :| Positive](List())
  |                            ^
  |    No implicit Ordering defined for io.github.iltotore.iron.IronType[Int,
  |      io.github.iltotore.iron.constraint.all.Positive].
1 error found

[Iltotore]

Fortunately, this seems to only be a "visual" bug in Scastie/REPL.

With this code in Scastie:

List.empty[Int].map(_.refine[Positive]).sum

I get 0 typed as Int :| Positive according to Scastie but if I try that (Scastie):

val x: Int :| Positive = List.empty[Int].map(_.refine[Positive]).sum

I get a compile-time error ("Value cannot be refined at compile-time because unknown etc...") as expected.

Can you try in your REPL the last example and see if it actually compiles or not?