erased given not working

[japgolly]

According to https://github.com/lampepfl/dotty/blob/master/docs/docs/reference/metaprogramming/erased-terms.md, erased given should work but it's not (on M3). Snippet from the doc:

object IsOn {
  // will not exist at runtime, the compiler will only
  // require that this evidence exists at compile time
  erased given IsOn[On] = new IsOn[On]
}

Minimized code

erased given Int = 1
given erased Long = 2L

Output

[error] -- Error: /home/golly/projects/public/univeq/univeq/shared/src/main/scala-3/UnivEq.scala:28:9 
[error] 28 |  erased given Int = 1
[error]    |         ^^^^^
[error]    |         end of statement expected but 'given' found
[error] -- [E040] Syntax Error: /home/golly/projects/public/univeq/univeq/shared/src/main/scala-3/UnivEq.scala:28:15 
[error] 28 |  erased given Int = 1
[error]    |               ^^^
[error]    |               ';' expected, but identifier found
[error] -- Error: /home/golly/projects/public/univeq/univeq/shared/src/main/scala-3/UnivEq.scala:29:15 
[error] 29 |  given erased Long = 2L
[error]    |               ^^^^
[error]    |               anonymous given cannot be abstract
[error] -- [E040] Syntax Error: /home/golly/projects/public/univeq/univeq/shared/src/main/scala-3/UnivEq.scala:29:20 
[error] 29 |  given erased Long = 2L
[error]    |                    ^
[error]    |                    ';' expected, but '=' found
[error] -- [E006] Not Found Error: /home/golly/projects/public/univeq/univeq/shared/src/main/scala-3/UnivEq.scala:28:2 
[error] 28 |  erased given Int = 1
[error]    |  ^^^^^^
[error]    |  Not found: erased
[error] -- [E006] Not Found Error: /home/golly/projects/public/univeq/univeq/shared/src/main/scala-3/UnivEq.scala:29:8 
[error] 29 |  given erased Long = 2L
[error]    |        ^^^^^^
[error]    |        Not found: type erased
[error] 6 errors found
[error] 6 errors found

Expectation

erased given should compile.

[nicolasstucki]

Note that to use erased you need to add -Yerased-terms.

Currently, we do not allow erased given.

erased given Int = 1

1 |erased given Int = 1
  |             ^
  |             modifier `erased` is not allowed for this definition
1 error found

As far as I can see we could just enable it but need on givens with an =. Not sure if we can for givens with a with.

[nicolasstucki]

See #10847 (comment)

[japgolly]

Awesome, thanks @nicolasstucki !