From 6e694107b3588c13936ce27a8b835ba4f254ae11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Rapha=C3=ABl=20Fromentin?=
 <42907886+Iltotore@users.noreply.github.com>
Date: Mon, 30 Oct 2023 14:13:18 +0100
Subject: [PATCH] docs: Add documentation about `RuntimeConstraint` (#187)

---
 docs/_docs/reference/constraint.md | 58 ++++++++++++++++++++++++++++--
 1 file changed, 55 insertions(+), 3 deletions(-)

diff --git a/docs/_docs/reference/constraint.md b/docs/_docs/reference/constraint.md
index 5b000408..8e129227 100644
--- a/docs/_docs/reference/constraint.md
+++ b/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])
 ```
\ No newline at end of file