Scala: how to force converting a statement to literal?

Question

I'm experimenting the refined type feature of scala provided in one of its library:

https://github.com/fthomas/refined

The following code represents a simple case:

  import eu.timepit.refined.auto._
  import shapeless.{Witness => W}

    type Vec5 = List[Int] Refined Size[Equal[W.`5`.T]]

    val v1: Vec5 = List(1, 2, 3, 4, 5)

    val v2: Vec5 = List(1 to 5: _*)

When attempting to compile it I got the following error:

[Error] /home/peng/git/scalaspike/common/src/test/scala/com/tribbloids/spike/refined_spike/Example.scala:32: compile-time refinement only works with literals
[Error] /home/peng/git/scalaspike/common/src/test/scala/com/tribbloids/spike/refined_spike/Example.scala:34: compile-time refinement only works with literals
[Error] /home/peng/git/scalaspike/common/src/test/scala/com/tribbloids/spike/singleton_ops_spike/Example.scala:32: Cannot prove requirement Require[...]
three errors found

It should be noted that both v1 & v2 can be easily evaluated at compile time and inlined, however scala compiler seems to refuse to do that, and for List type there seems to have no way to suggest this.

So how could this feature be useful?

Answer 1

Judging by tests the Size[Equals[X]] compile-time lifting is only implemented in macros for String literals.

And BTW, this makes sense, because author would have to evaluate the code at compile time - List(1,2,3,4,5) might look easy, but Set(1,1,2,2,3,3) would require some evaluation, and what if the code to evaluate was List(1,1,2,2,3,3).distinct - it also could be resolved in compile time but you have to set line somewhere unless you want to risk arbitrary code execution. And even in simpler cases the ADT to analyze could be hairy and error prone. Sure, it would be possible to add some "obvious special cases" but personally, I prefer that the library's author focuses on something more useful instead.