Refining with quantification over constants does not compile

[InversionSpaces]

Describe the bug Scala environment: JVM Scala version: 3.6.4 Iron version: 3.0.1

Reproduction steps Try to compile following code:

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

def find[T, N <: Int](
  l: List[T] :| Length[StrictEqual[N]]
): Int :| Interval.ClosedOpen[-1, N] = {
  val i: Int = -1
  i.refineUnsafe
}

val l = List(1, 2, 3)
val rl: List[Int] :| Length[StrictEqual[3]] = l.refineUnsafe
println(find(rl))

scastie: https://scastie.scala-lang.org/KBkja7ekR561d0Ze59sK0Q

Expected behavior Code compiles

Current behavior Compilation error:

scala.compiletime.ops.int.ToDouble[N] is not a constant type; cannot take constValue

[Iltotore]

Hello.

Unfortunately, this seems to be a compiler bug/limitation. I tested with a value of (Scastie) and it looks like the type is widened to a Int somewhere in the process.

There was a Pre-SIP discussion in order to solve this problem few years ago. Might be useful to revive.

[InversionSpaces]

Yes, you are right, type is widened. I think it is not a compiler bug then, it is expected behaviour. Type is widened to Int because the compiled code of the function could not have access to exact type N because it is defined precisely only at the call site.

Note that inside an inline method constValue works, as function body is inlined and thus precise type is known for its body. scastie: https://scastie.scala-lang.org/XiupgOIyTWO71dWpW488tg

If method from op post is marked with inline, it no longer fails on constValue, it fails with ambigious instances for constraints, is it intended behavior? scastie: https://scastie.scala-lang.org/xe7WrW3aQTm3aKGVlN9RGA

Thinking about this further, I do not quite understand, why Iron requires compile time value if it is runtime refinement? AFAIK, scala offers a solution for exactly problem we have here, it is ValueOf type class. Requiring it from N allows us to have its value inside the body, corresponding instances will be provided at the call site by the compiler. scastie: https://scastie.scala-lang.org/PZyPwhBSS4WiMjuVqvNc0Q

[Iltotore]

I apologize for the delay. I'm currently busy and didn't have the time to answer during the last two weeks.

If method from op post is marked with inline, it no longer fails on constValue, it fails with ambigious instances for constraints, is it intended behavior?

It is not and looks like a problem with the compiler inferring Nothing somewhere. It might be possible to work this around by making on the two given instances "low-priority".

why Iron requires compile time value if it is runtime refinement?

If you mean the value represented by the type, it's just because literal types (and generics) don't exist at runtime so we must know them at compile-time to get their "value". Even ValueOf[T] needs to know T at compile-time where the given instance is created. Also it is not possible to use ValueOf for Constraints because ValueOf#value is non-inlined so it would not work when used in compile-time mode. AFAIK We'd need value to be inline and get the erased feature as non-experimental to properly make use of ValueOf in Iron.

[pawelsadlo]

its not a bug i.refineUnsafe (which is equivalent to i.refineUnsafe[Interval.ClosedOpen[-1, N]] here) tries to expand a test macro from Constraint , but N is not known when macro is expanded, thus we get scala.compiletime.ops.int.ToDouble[N] is not a constant type; cannot take constValue because there is call to constValue within macro expansion which cant be computed because as I said literal value for N is not known yet

[Iltotore]

You're right. So @InversionSpaces a good workaround would just be to ask for the RuntimeConstraint in your method like this.