Implicit search produces mistyped tree

[Katrix]

Was told to create an issue for this:
https://gitter.im/lampepfl/dotty?at=5ebb35eb8c044c191498af5c

Minimized code

trait Cons[X, Y]

def solve[X, Y](using Cons[X, Y] =:= Cons[1, Cons[2, Y]]) = ()

@main def main = solve

Expectation

My first expectation for the above code was that it wouldn't compile at all. Not sure if that's the correct answer though. I'd also expect that if it did compile, I could supply the types printed by -Xprint:typer, and it would continue to compile.

The code does not compile with Scala 2.

[smarter]

That definitely shouldn't compile, -Ycheck:typer output:

Exception in thread "main" java.lang.AssertionError: assertion failed:
Found:    Cons[(1 : Int), Cons[(2 : Int), ?]] =:= Cons[(1 : Int), Cons[(2 : Int), ?]]
Required: Cons[(1 : Int), Cons[(2 : Int), ?]] =:= Cons[(1 : Int), Cons[(2 : Int), Cons[(2 : Int), ?]]]
found: ??
expected: ??
tree = <:<.refl[Cons[(1 : Int), Cons[(2 : Int), ?]]]