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?