Pre-SIP: Parametric Top

Language Design
18

I should add that while substitute is sufficiently powerful, it’s not necessarily convenient.

This example from the other thread which runs as written with opaque types:

def mdl(m: Map[Double, Logarithm]): Map[Logarithm, Double] = m

Suppose alternatively a =:= is provided and GADT-style =:= is made to work in patmat, it must be written

// supposing Logarithm.repr: Double =:= Logarithm
def mdl(m: Map[Double, Logarithm]): Map[Logarithm, Double] =
  Logarithm.repr match {
    case Refl() => m
  }

Supposing a =:= is provided but GADT-style is not made to work:

def mdl(m: Map[Double, Logarithm]): Map[Logarithm, Double] = {
  type F[A] = Map[Double, A] =:= Map[A, Double]
  Logarithm.repr.substitute[F](implicitly)(m)
}

Scala users might have some difficulty coming up with the correct F for various scenarios.