Open
Description
Simplifying from @b-studios #4376 (comment):
scala> object existentials {
|
| sealed trait Exists { type R }
| type Rank2[F[_]] = (e: Exists) |=> F[e.R]
|
| type ~>[F[_], G[_]] = Rank2[[X] => F[X] => G[X]]
|
| val nat: List ~> Option = {
| case Nil => None
| // also: x isn't refined to e.R
| case x :: _ => Some(x)
| }
| }
11 | case x :: _ => Some(x)
| ^
| Found: Any(x)
| Required: evidence$1.R
Since @abgruszecki is working on GADT type refinement and using singletons, we might make progress. Since @milessabin recently said he's fixing bugs with higher-kinded types, tagging him too.