Dependent types in scala. https://github.com/milessabin/shapeless/blob/topic/macro-paradise/core/src/main/scala/shapeless/snat.scala

gistfile1.scala

shapeless [0849b6f...] % sbt
[info] Loading project definition from /home/folone/workspace/shapeless/project
[info] Set current project to shapeless (in build file:/home/folone/workspace/shapeless/)
> shapeless-core/console
[warn] Credentials file /home/folone/.ivy2/.credentials does not exist
[info] Compiling 2 Scala sources to /home/folone/workspace/shapeless/core/target/scala-2.11/classes...
[info] Compiling 24 Scala sources to /home/folone/workspace/shapeless/core/target/scala-2.11/classes...
[info] Starting scala interpreter...
[info] 
Welcome to Scala version 2.11.0-20130205-141957-132e09fc2e (OpenJDK 64-Bit Server VM, Java 1.7.0_09).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import shapeless._
import shapeless._

scala> def plus[A, B, C](a: SNat[A], b: SNat[B], c: SNat[C])(implicit ssum: SSum[A, B, C]) = ssum
plus: [A, B, C](a: shapeless.SNat[A], b: shapeless.SNat[B], c: shapeless.SNat[C])(implicit ssum: shapeless.SSum[A,B,C])shapeless.SSum[A,B,C]

scala> plus(2,3,5) // 2 + 3 == 5
res0: shapeless.SSum[Int(2),Int(3),Int(5)] = $anon$1@71fb8368

scala> plus(2,3,4) // 2 + 3 /= 4
<console>:12: error: could not find implicit value for parameter ssum: shapeless.SSum[Int(2),Int(3),Int(4)]
              plus(2,3,4) // 2 + 3 /= 4
                  ^