Refined and existential types for runtime values : <p>Suppose I want to map between some strings and integer identifiers, and I want my types to make it impossible to get a runtime failure because someone tried to look up an id that was out of range. Here's one straightforward API:</p>

<pre><code>trait Vocab {
  def getId(value: String): Option[Int]
  def getValue(id: Int): Option[String] 
}
</code></pre>

<p>This is annoying, though, if users will typically be getting their ids from <code>getId</code> and therefore know they're valid. The following is an improvement in that sense:</p>

<pre><code>trait Vocab[Id] {
  def getId(value: String): Option[Id]
  def getValue(id: Id): String
}
</code></pre>

<p>Now we could have something like this:</p>

<pre><code>class TagId private(val value: Int) extends AnyVal

object TagId {
  val tagCount: Int = 100

  def fromInt(id: Int): Option[TagId] =
    if (id &gt;= 0 &amp;&amp; id &lt; tagCount) Some(new TagId(id)) else None
}
</code></pre>

<p>And then our users can work with <code>Vocab[TagId]</code> and not have to worry about checking whether <code>getValue</code> lookups failed in the typical case, but they can still look up arbitrary integers if they need to. It's still pretty awkward, though, since we have to write a separate type for each kind of thing we want a vocabulary for.</p>

<p>We can also do something like this with <a href="https://github.com/fthomas/refined" rel="noreferrer">refined</a>:</p>

<pre><code>import eu.timepit.refined.api.Refined
import eu.timepit.refined.numeric.Interval.ClosedOpen
import shapeless.Witness

class Vocab(values: Vector[String]) {
  type S &lt;: Int
  type P = ClosedOpen[Witness.`0`.T, S]

  def size: S = values.size.asInstanceOf[S]

  def getId(value: String): Option[Refined[Int, P]] = values.indexOf(value) match {
    case -1 =&gt; None
    case i  =&gt; Some(Refined.unsafeApply[Int, P](i))
  }

  def getValue(id: Refined[Int, P]): String = values(id.value)
}
</code></pre>

<p>Now even though <code>S</code> isn't known at compile time, the compiler is still able to keep track of the fact that the ids it gives us are between zero and <code>S</code>, so that we don't have to worry about the possibility of failure when we go back to values (if we're using the same <code>vocab</code> instance, of course).</p>

<p>What I want is to be able to write this:</p>

<pre><code>val x = 2
val vocab = new Vocab(Vector("foo", "bar", "qux"))

eu.timepit.refined.refineV[vocab.P](x).map(vocab.getValue)
</code></pre>

<p>So that users can easily look up arbitrary integers when they really need to. This doesn't compile, though:</p>

<pre><code>scala&gt; eu.timepit.refined.refineV[vocab.P](x).map(vocab.getValue)
&lt;console&gt;:17: error: could not find implicit value for parameter v: eu.timepit.refined.api.Validate[Int,vocab.P]
       eu.timepit.refined.refineV[vocab.P](x).map(vocab.getValue)
                                          ^
</code></pre>

<p>I can make it compile by providing a <code>Witness</code> instance for <code>S</code>:</p>

<pre><code>scala&gt; implicit val witVocabS: Witness.Aux[vocab.S] = Witness.mkWitness(vocab.size)
witVocabS: shapeless.Witness.Aux[vocab.S] = shapeless.Witness$$anon$1@485aac3c

scala&gt; eu.timepit.refined.refineV[vocab.P](x).map(vocab.getValue)
res1: scala.util.Either[String,String] = Right(qux)
</code></pre>

<p>And of course it fails (at runtime but safely) when the value is out of range:</p>

<pre><code>scala&gt; val y = 3
y: Int = 3

scala&gt; println(eu.timepit.refined.refineV[vocab.P](y).map(vocab.getValue))
Left(Right predicate of (!(3 &lt; 0) &amp;&amp; (3 &lt; 3)) failed: Predicate failed: (3 &lt; 3).)
</code></pre>

<p>I could also put the witness definition inside my <code>Vocab</code> class and then import <code>vocab._</code> to make it available when I need this, but what I really want is to be able to provide <code>refineV</code> support without extra imports or definitions.</p>

<p>I've tried various stuff like this:</p>

<pre><code>object Vocab {
  implicit def witVocabS[V &lt;: Vocab](implicit
    witV: Witness.Aux[V]
  ): Witness.Aux[V#S] = Witness.mkWitness(witV.value.size)
}
</code></pre>

<p>But this still requires an explicit definition for each <code>vocab</code> instance:</p>

<pre><code>scala&gt; implicit val witVocabS: Witness.Aux[vocab.S] = Vocab.witVocabS
witVocabS: shapeless.Witness.Aux[vocab.S] = shapeless.Witness$$anon$1@1bde5374

scala&gt; eu.timepit.refined.refineV[vocab.P](x).map(vocab.getValue)
res4: scala.util.Either[String,String] = Right(qux)
</code></pre>

<p>I know I could implement <code>witVocabS</code> with a macro, but I feel like there should be a nicer way to do this kind of thing, since it seems like a pretty reasonable use case (and I'm not very familiar with refined, so it's entirely possible that I'm missing something obvious).</p>
