`Not` not working; alternative definition doesn't need to be intrinsic?

[milessabin]

The following compiles, but shouldn't,

object Test {
  import implicits.Not

  class Foo
  class Bar
  implicit def foo: Foo = ???
  implicitly[Foo]
  implicitly[Not[Foo]] // compiles, but shouldn't
  implicitly[Not[Bar]] // compiles, correctly
}

It also appears that the following traditional negation as failure encoding of Not works as it would in Scala 2,

final class Not2[T] private ()

trait LowPriorityNot2 {

  /** A fallback method used to emulate negation in Scala 2 */
  implicit def default[T]: Not2[T] = Not2.value.asInstanceOf[Not2[T]]
}
object Not2 extends LowPriorityNot2 {

  /** A value of type `Not` to signal a successful search for `Not[C]` (i.e. a failing
   *  search for `C`). A reference to this value will be explicitly constructed by
   *  Dotty's implicit search algorithm
   */
  def value: Not2[Nothing] = new Not2[Nothing]()

  /** One of two ambiguous methods used to emulate negation in Scala 2 */
  implicit def amb1[T](implicit ev: T): Not2[T] = ???

  /** One of two ambiguous methods used to emulate negation in Scala 2 */
  implicit def amb2[T](implicit ev: T): Not2[T] = ???
}

object Test {
  class Foo
  class Bar
  implicit def foo: Foo = ???
  implicitly[Foo]
  implicitly[Not2[Foo]] // does not compile, as expected under Scala 2 ambiguity rules
  implicitly[Not2[Bar]] // compiles
}

[milessabin]

Clarification: the Not[Foo] example compiles if -Xmin-implicit-search-depth < 2, and doesn't compile (as expected) if -Xmin-implicit-search-depth >= 2.

[smarter]

It also appears that the following traditional negation as failure encoding of Not works as it would in Scala 2,

You need to use Not2 as part of the implicit search of some other thing to run into trouble, see #3421 (comment) from the PR where Not was introduced for an example.

[milessabin]

It appears to depend on -Xmin-implicit-search-depth. With it set to 0 or 1 the following compiles,

object Test {
  import implicits.Not

  class Foo
  implicit def foo: Foo = ???

  def foo[T](implicit ev: Not[T]) = ???
  foo[Foo]
}

[smarter]

Yeah looks like the divergence check is broken when the expected type happens to be a wildcard at that point, we check proto.classSymbols.isEmpty (https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/typer/Implicits.scala#L1238) but classSymbols returns Nil on WildcardType (which makes sense given its documentation).

[nicolasstucki]

It looks like this is fixed

[milessabin]

Not does work now, however, as I also mentioned, the Scala 2 style negation-as-failure still works as before, so it's not all that clear to me what purpose Not serves.

[milessabin]

Correction: I see what purpose it serves ... it's not clear to me why it needs to be a compiler intrinsic.

[smarter]

Have you seen the discussion in #3421 (comment) ?

[milessabin]

@smarter maybe I'm looking at the wrong thing but on current master the negation-as-failure example in that comment behaves as I would expect it to. It's negation, and not intrinsic.