Erased terms can't be passed to erased lambda argument

[Odomontois]

def foo(f: (erased Int) => Int): Int = {
  erased val ctx = 1
  f(ctx)
}

gives compilation error

value ctx is declared as erased, but is in fact used

dotty version : 0.13-RC1

[nicolasstucki]

With the introduction of given the syntax changed. Now this version should be rejected and the correct code would be

def foo(f: erased Int => Int): Int = ...

or

def foo(f: erased (Int, ...) => Int): Int = ...