Incorrect type selection due to mixin

[Bersier]

Compiler version

3.2.0

Minimized code

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[N <: NatT](n: N) extends NatT

type _0 = Zero
type _1 = Succ[_0]

given Zero = Zero()
given [N <: NatT](using n: N): Succ[N] = Succ(n)
// a variant for the previous line leading to a different error message: 
// given Succ[Zero] = Succ(Zero())

trait Mixin

class Instance[N <: NatT](using N)

trait Container[N <: NatT]:
  def instance: Instance[N]

class Refined extends Container[_1]:
  def instance: Instance[_1] & Mixin = new Instance() with Mixin

Compiler output

Found:    Instance[Zero] with Mixin {...}
Required: Instance[_1] & Mixin

Expectation

No compiler error.

The code does compile when the last line is changed to

  def instance: Instance[_1] & Mixin = new Instance[_1]() with Mixin

or when there is no mixin.

For more complex code, I've seen errors due to this that are impossible to decipher, as they wrongly assert that other using parameters are missing. Unfortunately, they are hard to reproduce with a small piece of code.

[dwijnand]

@odersky is this an inference / implicit search bug, or is there a good reason why this doesn't use the expected Instance[_1] & Mixin?

I assume there's good reason why given [N <: NatT](using n: N): Succ[N] = Succ(n) is lower precedence, as opposed to given Succ[Zero] = Succ(Zero()) which is ambiguous to given Zero.

[odersky]

Yes, givens with fewer using clauses take precedence. So this is as expected.

[dwijnand]

But what about the expected intersection type, should that drive to the use of given_Succ(using given_Zero) instead?

[odersky]

Expected types don't propagate into parents of anonymous classes.

[dwijnand]

Ah, got it, thank you.

[Bersier]

Unfortunately, while simplifying the code, I did not notice the transition to a (in-retrospect) more understandable error message. In my original code, Container notably has a given for another type, and Instance needs it as an implicit. The compiler then wrongly complains that that unrelated implicit is not present.

I wonder: if only the language developers know whether there is a bug or not, maybe that indicates an issue with the language, the compiler message, or the language documentation.

@dwijnand Is the behavior described here also intentional?

I wouldn't mind showing my code to someone on a call. But given the growing backlog of bugs, it probably won't be worth any developer's time for a while.

[dwijnand]

@dwijnand Is the behavior described here also intentional?

That seems to be fixed in main. It's possible by #15986.