Is it possible to use type parameters together with refineOption?

[kurnevsky]

I'm trying to do something like:

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

final case class Coord[W <: Int, H <: Int](x: Int :| Interval.Closed[0, W], y: Int :| Interval.Closed[0, H]):
  def n: Option[Coord[W, H]] =
    (y + 1).refineOption[Interval.Closed[0, H]].map(Coord(x, _))

But getting scala.compiletime.ops.int.ToDouble[H] is not a constant type; cannot take constValue. Is there some trick that would allow me to define such type? :)

[kurnevsky]

Hm, just plain if-then-else together with assume works, but maybe it can be done safer?

[Iltotore]

You can try using <: Int & Singleton for your generic types or <: Int : ValueOf this does not work (seems to be a problem with Scala's implicit resolution).

It is possible to ask for the constraint in the constructor so that the compiler knows the Constraint instance to pick: https://scastie.scala-lang.org/JZg1z4gKRpmnYeRATmCECA

Note that inline in its current implementation can be tricky with class parameters. Since it is not possible to make a class parameter inline I explicitly use summonInline in refineOption. If you want to avoid making n inline, you can use plain if as you said, eventually with a RuntimeConstraint.