docs: Add documentation about RuntimeConstraint (#187)

docs/_docs/reference/constraint.md

@@ -4,7 +4,7 @@ title: "Constraint"
 
 # Constraint
 
-In Iron, a constraint consist of a type, called "dummy" or "proxy" type, associated with a given
+In Iron, a constraint consist of a type, called "dummy" type, associated with a given
 instance of [[Constraint|io.github.iltotore.iron.Constraint]].
 
 See [Refinement](refinement.md) for usage.
@@ -113,7 +113,7 @@ final class Greater[V]
 
 Then, we can get the value of the passed type using `scala.compiletime.constValue`:
 
-```scala  sc-name:GreaterAndConstraint.scala sc-compile-with:Greater.scala
+```scala sc-name:GreaterAndConstraint.scala sc-compile-with:Greater.scala
 //{
 import io.github.iltotore.iron.*
 //}
@@ -132,7 +132,59 @@ This method is equivalent to `constValue[scala.compiletime.ops.any.ToString[V]]`
 
 Now testing the constraint:
 
-```scala  sc-compile-with:GreaterAndConstraint.scala
+```scala sc-compile-with:GreaterAndConstraint.scala
 val x: Int :| Greater[5] = 6
 val y: Int :| Greater[5] = 3 //Compile-time error: Should be greater than 5
+```
+
+## Runtime proxy
+
+Iron provides a proxy for `Constraint`, named `RuntimeConstraint`. It is used the same way as `Constraint`:
+
+```scala
+def refineRuntimeOption[A, C](value: A)(using constraint: RuntimeConstraint[A, C]): Option[A :| C] =
+  Option.when(constraint.test(value))(value.asInstanceOf[A :| C])
+
+refineRuntimeOption[Int, Positive](5) //Some(5)
+refineRuntimeOption[Int, Positive](-5) //None
+```
+
+with two advantages:
+- It does not need the summoning method (here `refineOption`) to be `inline`
+- It significantly lowers the generated bytecode and usually improves performances
+
+Therefore, it is recommended to use `RuntimeConstraint` instead of `Constraint` when using the instance at runtime.
+For example, most of `RefinedTypeOps`'s (see [New types](newtypes.md#runtime-refinement)) methods use a
+`RuntimeConstraint`.
+
+It is also recommended to use `RuntimeConstraint` to derive typeclasses, especially when using a `given` with a function
+value.
+
+```scala
+trait FromString[A]:
+
+  def fromString(text: String): Either[String, A]
+
+given [A, C](using constraint: RuntimeConstraint[A, C], instanceA: FromString[A]): FromString[A :| C] = text =>
+  instanceA
+    .fromString(text)
+    .filterOrElse(constraint.test(_), constraint.message)
+    .map(_.asInstanceOf[A :| C])
+```
+
+Note that using a `Constraint` here (and having to our given instance `inline`) will produce a warning:
+
+> An inline given alias with a function value as right-hand side can significantly increase
+generated code size. You should either drop the `inline` or rewrite the given with an
+explicit `apply` method.
+
+`RuntimeConstraint` is also useful when you need to reuse the same constraint. Here is an example from `RefinedTypeOps`:
+
+```scala
+trait RefinedTypeOps[A, C, T]:
+
+  inline def rtc: RuntimeConstraint[A, C] = ???
+
+  def option(value: A): Option[T] =
+    Option.when(rtc.test(value))(value.asInstanceOf[T])
 ```