Compiler error on valid scala code when using implicit parameters + default parmeters

[rcano]

Minimized code

  import scala.compiletime.ops.int._
  def test(i: Int = 3)(using i.type > 0 =:= true) = i
  //test(3) compiles
  //test(-2) proper compiler error
  test()

Output

 2 |  test()
   |        ^
   |        Cannot prove that (?1 : Int) > (0 : Int)
   |
   |        where:    ?1 is an unknown value of type Int
   |         =:= (true : Boolean).
one error found

Expectation

code should compile as is the case when manually passing the value

[odersky]

The definition of type > is missing here.

[rcano]

My bad, updated the example code.

[smarter]

It also fails if you do test(3: Int) because that loses the precise singleton type 3, the same thing happens with the default value because it gets desugared into a default getter:

def test$default1 = 3

and test$default1 inferred result type is Int, because we widen singletons and unions in inferred result types. I think we just need to not do that widening for default getters.

[rcano]

@smarter I noticed that, and I tried to cheat by doing

  def myDefault: 3 = 3
  def test(i: Int = myDefault)(using i.type > 0 =:= true) = i

but once again it seems it loses precision anyway.

[smarter]

yeah even then, a def for the getter will get created and its result type inferred.

[rcano]

Does this issue still need more info? or can the tag be removed?