我正在尝试在其库之一中提供的scala的改进类型功能：
https://github.com/fthomas/refined
以下代码代表一个简单的情况：
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: _*)
尝试编译时，出现以下错误：
[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.
那么，此功能怎么有用？
Judging by tests the
Size[Equals[X]]compile-time lifting is only implemented in macros forStringliterals.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, butSet(1,1,2,2,3,3)would require some evaluation, and what if the code to evaluate wasList(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.