Open
Description
Minimized code
trait UntypedLambda[E] {
def lam(f: E => E): E
def app(e1: E, e2: E): E
}
def lam[E](f: E => E)(using ul: UntypedLambda[E]): E = ul.lam(f)
def app[E](e1: E, e2: E)(using ul: UntypedLambda[E]): E = ul.app(e1, e2)
type WithUntypedLambda[A] = UntypedLambda[A] ?=> A
type Hoas = [A] => UntypedLambda[A] ?=> A
//Doesn't work
//val example1: Hoas = [A] => lam[A](x => lam(y => app(x, y)))
//Works
val example1: Hoas = [A] => (using tc: UntypedLambda[A]) => lam[A](x => lam(y => app(x, y)))Expectation
This should work, as the polymorphic function still needs a value, it's just not shown to the user.