Inability to do a simple type match on a deduced type

[belamenso]

Compiler version

3.6.2

Minimized code

type IntLike[T] <: Boolean = T match
  case Int => true
  case _ => false
def f[T](using IntLike[T] =:= true)(a: T): Unit = ()
@main def main(): Unit = f(1)

Output

[error] -- [E172] Type Error: Main.scala:5:26 
[error] 5 |@main def main(): Unit = f(1)
[error]   |                          ^
[error]   |               Cannot prove that IntLike[T] =:= (true : Boolean).
[error]   |
[error]   |               where:    T is a type variable
[error]   |
[error]   |
[error]   |               Note: a match type could not be fully reduced:
[error]   |
[error]   |                 trying to reduce  IntLike[T]
[error]   |                 failed since selector T
[error]   |                 does not match  case Int => (true : Boolean)
[error]   |                 and cannot be shown to be disjoint from it either.
[error]   |                 Therefore, reduction cannot advance to the remaining case
[error]   |
[error]   |                   case _ => (false : Boolean)
[error] one error found

Expectation

I expect it to compile without errors. Explicitly providing the type parameter on the call-site fixes this completely:

@main def main(): Unit = f[Int](1)

[hamzaremmal]

I haven't tried it yet but I guess switching the parameter lists will also work (It has to do with how inferrence works and match type reduces).

def f[T](a: T):(using IntLike[T] =:= true) Unit = ()

cc @EugeneFlesselle @sjrd

---

EDIT: It does work