Inductive given using Tuple.Tail can't be derived when tuple is of size >3

[fazzou]

Compiler version

3.2.2 (also tried on 3.3.0-RC3 & 3.1.3)

Minimized code

trait A[T <: Tuple] { val x: Int }
given empty: A[EmptyTuple] with { val x = 1 }
given inductive[Tup <: NonEmptyTuple](using A[Tuple.Tail[Tup]]): A[Tup] with { val x = summon[A[Tuple.Tail[Tup]]].x + 1 }

println(summon[A[(String, String, String)]].x) //this line is fine
println(summon[A[(String, String, String, String)]].x) //this line gives error

Output

> scala-cli --scala 3 test.sc
Compiling project (Scala 3.2.2, JVM)
[error] ./test.sc:6:52
[error] No given instance of type test.A[(String, String, String, String)] was found for parameter x of method summon in object Predef.
[error] I found:
[error]
[error]     test.inductive[(String, String, String, String)](
[error]       test.inductive[Tuple.Tail[(String, String, String, String)]](
[error]         /* missing */
[error]           summon[test.A[Tuple.Tail[Tuple.Tail[(String, String, String, String)]]]]
[error]       )
[error]     )
[error]
[error] But given instance inductive in object test produces a diverging implicit search when trying to match type test.A[Tuple.Tail[Tuple.Tail[(String, String, String, String)]]].
[error]
[error] Note: given instance inductive in object test was not considered because it was not imported with `import given`.
[error] println(summon[A[(String, String, String, String)]].x)
[error]                                                    ^
Error compiling project (Scala 3.2.2, JVM)
Compilation failed

Expectation

Program compiling successfully and printing

4
5

[nicolasstucki]

I got an error in both cases.

[nicolasstucki]

It seems that the match types are not getting simplified in the recursive case.

[nicolasstucki]

I tried this change

-    inferImplicit(formal, EmptyTree, span) match
+    inferImplicit(formal.simplified, EmptyTree, span) match

here https://github.com/lampepfl/dotty/blob/main/compiler/src/dotty/tools/dotc/typer/Implicits.scala#L882

This fixed the issue but started breaking uses of throws.

[odersky]

One has to be very, very careful with simplified. It is a heavy high-level operation. It can seem to fix many things, but it also forces too much which can break other things. So best not to use it in places other where it is already used today.

[fazzou]

I got an error in both cases.

Hmm for me & on scastie it seemed deterministically fail on the 2nd one, though not sure, maybe there is some context that can influence that behavior.

[prolativ]

For me the first one seems to always work too