GADT contraint not considered for given/extension in implicit scope

[eejbyfeldt]

Compiler version

3.7.4, 3.8.1-RC1-bin-20251203-b2850be-NIGHTL

Minimized code

$ cat gadt_contraint_implicit.scala
trait Expr[T]
object Expr {
  extension (lhs: Expr[Boolean])
    infix def ||(rhs: Expr[Boolean]): Expr[Boolean] = ???
}

object test {
  sealed trait A[T]
  object Or extends A[Boolean]

  def g[T](a: A[T], lhs: Expr[T]): Expr[T] = 
    a match {
    case Or => lhs || lhs
  }
}

Output

[error] ./gadt_contraint_implicit.scala:13:16
[error] value || is not a member of Expr[T]
[error] 
[error] where:    T is a type in method g which is an alias of Boolean
[error]     case Or => lhs || lhs
[error]   

Expectation

The code some compile.

[eejbyfeldt]

If the implicit is instead in contextual scope e.g by moving the defining or adding an explicit import the code will compile. This is because as part of implicit search there is extra logic around gadt constraints for that case
https://github.com/scala/scala3/blob/main/compiler/src/dotty/tools/dotc/typer/Implicits.scala#L1691-L1696
but no similar logic is applied for implicit scope.

If the type parameter is changed to be covariant or contravariant the code will also compile. But this is because the look up will succeed after GADT approximation. But invariant type are left unchanged:

scala3/compiler/src/dotty/tools/dotc/typer/Inferencing.scala

Lines 288 to 316 in b2850be

	/** GADT approximation proceeds differently from type variable approximation.
	*
	* Essentially, what we're doing is we're inferring a type ascription that
	* will remove as many GADT-constrained types as possible. This means that
	* we want to approximate type T to type S in such a way that no matter how
	* GADT-constrained types are instantiated, T <: S. In other words, the
	* relationship _necessarily_ must hold.
	*
	* We accomplish that by:
	* - replacing covariant occurrences with upper GADT bound
	* - replacing contravariant occurrences with lower GADT bound
	* - leaving invariant occurrences alone
	*
	* Examples:
	* - If we have GADT cstr A <: Int, then for all A <: Int, Option[A] <: Option[Int].
	* Therefore, we can approximate Option[A] ~~ Option[Int].
	* - If we have A >: S <: T, then for all such A, A => A <: S => T. This
	* illustrates that it's fine to differently approximate different
	* occurrences of same type.
	* - If we have A <: Int and F <: [A] => Option[A] (note the invariance),
	* then we should approximate F[A] ~~ Option[A]. That is, we should
	* respect the invariance of the type constructor.
	* - If we have A <: Option[B] and B <: Int, we approximate A ~~
	* Option[B]. That is, we don't recurse into already approximated
	* types. Since GADT approximation is (for now) only used for member
	* selection, this behaviour is expected, as nested types cannot affect
	* member selection (note that given/extension lookup doesn't need GADT
	* approx, see gadt-approximation-interaction.scala).
	*/

The last part

Since GADT approximation is (for now) only used for member selection, this behaviour is expected, as nested types cannot affect member selection (note that given/extension lookup doesn't need GADT approx, see gadt-approximation-interaction.scala).

makes it sounds like it expected that it should work. But the test file gadt-approximation-interaction.scala only has test cases where the extension is defined as part of contextual scope.

[eejbyfeldt]

@odersky You added the fix for contextual implicit here: #14072

Maybe you know more if there are some good reason that a similar logic was not applied for implicits in implicit scope.

[odersky]

@eejbyfeldt The main logic in that PR had to do with caching eligibles. That only applies for contextual implicits. I am not sure how to generalize that to implicit scopes. Throwing away all known implicit scopes and starting from scratch could be a huge performance hit.