Recursive match type fails after 3rd call when using explicit type

hmf commented 1 year ago

Compiler version

Versions 3.2.0, 3.2.1-RC2 and 3.2.1

Minimized code

Code below can be found in scastie

import scala.compiletime.ops.int

type Count0[N,T] <: Tuple = (N,T) match
  case (0,_)      => EmptyTuple
  case (N,String)      => String *: Count0[int.-[N, 1], String]
  case (N,Int)         => Int *: Count0[int.-[N, 1], Int]
  case (N,Float)       => Float *: Count0[int.-[N, 1], Float]  
  case (N,Double)      => Double *: Count0[int.-[N, 1], Double]  

type Count1[N,T] <: Tuple = (N,T) match
  case (0,T)      => EmptyTuple
  case (N,String)      => String *: Count1[int.-[N, 1], String]
  case (N,Int)         => Int *: Count1[int.-[N, 1], Int]
  case (N,Float)       => Float *: Count1[int.-[N, 1], Float]  
  case (N,Double)      => Double *: Count1[int.-[N, 1], Double]  

summon[Count0[1, Int] =:= Int *: EmptyTuple ]
summon[Count0[2, Int] =:= Int *: Int *: EmptyTuple] 
summon[Count0[3, Int] =:= Int *: Int *: Int *: EmptyTuple] 
summon[Count0[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple] 
summon[Count0[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple] 

summon[Count1[1, Int] =:= Int *: EmptyTuple ]
summon[Count1[2, Int] =:= Int *: Int *: EmptyTuple] 
// Fail from here
summon[Count1[3, Int] =:= Int *: Int *: Int *: EmptyTuple] 
summon[Count1[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple] 
summon[Count1[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple]

Output

[error] -- Error: /home/hmf/VSCodeProjects/sploty/meta/src/data/Data8.scala:380:62 -----
[error] 380 |    summon[Count1[3, Int] =:= Int *: Int *: Int *: EmptyTuple] 
[error]     |                                                              ^
[error]     |Cannot prove that Int *: Int *: data.Macros5.Count1[(2 : Int) - (1 : Int), Int] =:= (Int, Int, Int).
[error] -- Error: /home/hmf/VSCodeProjects/sploty/meta/src/data/Data8.scala:381:69 -----
[error] 381 |    summon[Count1[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple] 
[error]     |                                                                     ^
[error]     |Cannot prove that Int *: Int *: data.Macros5.Count1[(3 : Int) - (1 : Int), Int] =:= (Int, Int, Int, Int).
[error] -- Error: /home/hmf/VSCodeProjects/sploty/meta/src/data/Data8.scala:382:76 -----
[error] 382 |    summon[Count1[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple] 
[error]     |                                                                            ^
[error]     |Cannot prove that Int *: Int *: data.Macros5.Count1[(4 : Int) - (1 : Int), Int] =:= (Int, Int, Int, Int, Int).

Expectation

I expects both Count0 and Count1 to compile successfully. Removing the type T from Count0, to get Count1, seems to allow compilation to succeed, but I don't think it should change anything. Also, compilation only fails for 3 or or more recursive calls, which seems suspect.

prolativ commented 1 year ago

Also this works with case (0,T) if you change case (N,Int) to case (_,Int)

johnynek commented 1 year ago

I came to report a similar problem which I minimized as follows:

import scala.compiletime.ops

object NatExample {
  sealed trait Nat
  object Nat {
    case object Zero extends Nat
    case class Succ[N <: Nat](prev: N) extends Nat

    given zero: Zero.type = Zero
    given buildSucc[N <: Nat](using n: N): Succ[N] =
      Succ(n)

    def value[N <: Nat](using n: N): N = n

    type FromInt[I <: Int] <: Nat = I match {
      case 0 => Zero.type
      case _ =>
        ops.int.<[I, 0] match {
          case true => Nothing
          case false =>
            Succ[FromInt[ops.int.-[I, 1]]]
        }
    }

    summon[FromInt[0] =:= Zero.type]
    summon[FromInt[1] =:= Succ[Zero.type]]
    summon[FromInt[2] =:= Succ[Succ[Zero.type]]]
    summon[FromInt[3] =:= Succ[Succ[Succ[Zero.type]]]]
    summon[FromInt[4] =:= Succ[Succ[Succ[Succ[Zero.type]]]]]

    @main def test = {
      require(summon[FromInt[0]] == Zero)
      require(summon[FromInt[1]] == Succ(Zero))
      require(summon[FromInt[2]] == Succ(Succ(Zero)))
      require(summon[FromInt[3]] == Succ(Succ(Succ(Zero))))
      // we can summon 4 if we write it out:
      require(summon[Succ[Succ[Succ[Succ[Zero.type]]]]] == Succ(Succ(Succ(Succ(Zero)))))
      // we cannot summon 4 using the match type
      //require(summon[FromInt[4]] == Succ(Succ(Succ(Succ(Zero)))))
      /*
      [error] -- Error: /Users/oboykin/code/nui/core/src/main/scala-3/dev/posco/nui/SizeMacros.scala:105:32
[error] 105 |      require(summon[FromInt[4]] == Succ(Succ(Succ(Succ(Zero)))))
[error]     |                                ^
[error]     |No given instance of type dev.posco.nui.NatExample.Nat.Succ[
[error]     |  dev.posco.nui.NatExample.Nat.FromInt[(4 : Int) - (1 : Int)]
[error]     |] was found for parameter x of method summon in object Predef.
[error]     |I found:
[error]     |
[error]     |    dev.posco.nui.NatExample.Nat.buildSucc[
[error]     |      dev.posco.nui.NatExample.Nat.FromInt[(4 : Int) - (1 : Int)]
[error]     |    ](
[error]     |      dev.posco.nui.NatExample.Nat.buildSucc[
[error]     |        dev.posco.nui.NatExample.Nat.FromInt[(4 : Int) - (1 : Int) - (1 : Int)]
[error]     |      ](
[error]     |        /* missing */
[error]     |          summon[
[error]     |            dev.posco.nui.NatExample.Nat.FromInt[(4 : Int) - (1 : Int) - (1 : Int)]
[error]     |          ]
[error]     |      )
[error]     |    )
[error]     |
[error]     |But given instance buildSucc in object Nat produces a diverging implicit search when trying to match type dev.posco.nui.NatExample.Nat.FromInt[(4 : Int) - (1 : Int) - (1 : Int)].
[error]     |
[error]     |Note: given instance buildSucc in object Nat was not considered because it was not imported with `import given`.
[error] one error found
*/
    }
  }
}

dwijnand commented 1 year ago

Could easily be the same as https://github.com/lampepfl/dotty/pull/16206.

johnynek commented 1 year ago

I noticed another clue. When the repl prints the normalized type, the summon seems to work. When the repl prints a type including an uncomputed match type, summon fails.

package dev.posco.nui

import scala.quoted.*
import scala.compiletime.{erasedValue, error, ops, requireConst}

object NatExample {
  sealed trait Nat
  object Nat {
    case object Zero extends Nat
    case class Succ[N <: Nat](prev: N) extends Nat

    given zero: Zero.type = Zero
    given buildSucc[N <: Nat](using n: N): Succ[N] =
      Succ(n)

    def value[N <: Nat](using n: N): N = n

    type FromInt[I <: Int] <: Nat = I match {
      case 0 => Zero.type
      case _ =>
       // ops.int.<[I, 0] match {
         // case true => Nothing
         // case false =>
            Succ[FromInt[ops.int.-[I, 1]]]
       // }
    }

    inline def prevOf[I <: Int](inline i: I): ops.int.-[I, 1] =
      ${prevImpl('i)}

    def prevImpl[I <: Int: Type](expr: Expr[I])(using Quotes): Expr[ops.int.-[I, 1]] = {
      val prev = expr.valueOrError - 1
      // this compiles, but fails at use time
      //Expr(prev).asExprOf[ops.int.-[I, 1]]
      Expr(prev).asInstanceOf[Expr[ops.int.-[I, 1]]]
    }

    inline def fromInt[I <: Int & Singleton](inline i: I): FromInt[i.type] = {
      requireConst(i)
      inline i match {
        case _: 0 => Zero
        case _ =>
          inline if i < 0 then error("cannot convert negative to Nat")
          else {
            Succ(fromInt(prevOf[i.type](i)))
          }
      }
    }
  }
}

With the above, at the repl we get:

scala> Nat.fromInt(2)
val res9: 
  dev.posco.nui.NatExample.Nat.Succ[
    dev.posco.nui.NatExample.Nat.Succ[dev.posco.nui.NatExample.Nat.Zero.type]
  ] = Succ(Succ(Zero))

scala> summon[Nat.FromInt[2]]
val res10: 
  dev.posco.nui.NatExample.Nat.Succ[
    dev.posco.nui.NatExample.Nat.Succ[dev.posco.nui.NatExample.Nat.Zero.type]
  ] = Succ(Succ(Zero))

scala> Nat.fromInt(3)
val res11: 
  dev.posco.nui.NatExample.Nat.Succ[
    dev.posco.nui.NatExample.Nat.Succ[
      dev.posco.nui.NatExample.Nat.Succ[
        dev.posco.nui.NatExample.Nat.FromInt[1 - 1]
      ]
    ]
  ] = Succ(Succ(Succ(Zero)))

scala> summon[Nat.FromInt[3]]
-- Error: ----------------------------------------------------------------------
1 |summon[Nat.FromInt[3]]
  |                      ^
  |No given instance of type dev.posco.nui.NatExample.Nat.Succ[
  |  dev.posco.nui.NatExample.Nat.FromInt[(3 : Int) - (1 : Int)]
  |] was found for parameter x of method summon in object Predef.
  |I found:
  |
  |    dev.posco.nui.NatExample.Nat.buildSucc[
  |      dev.posco.nui.NatExample.Nat.FromInt[(3 : Int) - (1 : Int)]
  |    ](
  |      dev.posco.nui.NatExample.Nat.buildSucc[
  |        dev.posco.nui.NatExample.Nat.FromInt[(3 : Int) - (1 : Int) - (1 : Int)]
  |      ](
  |        /* missing */
  |          summon[
  |            dev.posco.nui.NatExample.Nat.FromInt[(3 : Int) - (1 : Int) - (1 : Int)]
  |          ]
  |      )
  |    )
  |
  |But no implicit values were found that match type dev.posco.nui.NatExample.Nat.FromInt[(3 : Int) - (1 : Int) - (1 : Int)].
  |
  |Note: given instance buildSucc in object Nat was not considered because it was not imported with `import given`.
1 error found

So it seems that the fact that the match type is left not fully computed, is what is causing a problem at implicit resolution time.

It seems to me, that we should be consistent: either leave match types uncomputed or fully computed. The partial computation seems strange (like it looks like we are taking 2 or 3 loops in the match recursion, then stopping).

Another possible issue is that to do implicit resolution it isn't unrolling the match type more.

Decel commented 1 year ago

So it seems that the fact that the match type is left not fully computed, is what is causing a problem at implicit resolution time.

It seems to me, that we should be consistent: either leave match types uncomputed or fully computed. The partial computation seems strange (like it looks like we are taking 2 or 3 loops in the match recursion, then stopping).

Another possible issue is that to do implicit resolution it isn't unrolling the match type more.

They are actually computed only once:

scala> import scala.compiletime.ops.int

scala> type Count[N,T] <: Tuple = (N, T) match
     |   case (0, T)      => EmptyTuple
     |   case (N, T)      => T *: Count[int.-[N, 1], T]

scala> def a: Count[3, Int] = ???
def a: Int *: Count[3 - 1, Int]

The second time happens due to a summon or implicitly call. So, the behavior is consistent.

To be honest, I am not sure how to approach this issue and whether this is an issue at all, i.e to fix this, we would ruin match types "laziness", so we couldn't write something like:

scala> type F[X] = X match
     |   case Int => String
     |   case _ => List[F[X]]

scala> def x: F[String] = ???
def x: List[F[String]]

And I think it's a loss in terms of expressivity.

johnynek commented 1 year ago

To be honest, I am not sure how to approach this issue and whether this is an issue at all, i.e to fix this, we would ruin match types "laziness", so we couldn't write something like:
scala> type F[X] = X match
     |   case Int => String
     |   case _ => List[F[X]]

scala> def x: F[String] = ???
def x: List[F[String]]
And I think it's a loss in terms of expressivity.

I would be shocked if most scala programmers would prefer to be able to write non-terminating infinite loop matches over the ability to use recursive match types with implicit resolution.

To me, loss of implicit resolution/givens with recursive match types is a huge loss for expressivity. Moreover, I would argue that match types should be required to be terminating. Having non-terminating infinite loop match types, as you have shown in your example above, seems like a really bad "feature" to protect over making match types compose with core scala features such as implicit resolution.

dwijnand commented 1 year ago

The List[F[X]] example is a minimisation of a test in the test suite, tests/pos/i15158.scala, here's a portion:

type JsonPrimitive = String | Int
type Rec[JA[_], A] = A match {
  case JsonPrimitive => JsonPrimitive | JA[Rec[JA, JsonPrimitive]]
  case Any => A | JA[Rec[JA, A]]
}

type Json = Rec[
  [A] =>> Seq[A],
  JsonPrimitive
]

It's building an infinite union type:

String | Int | Seq[
  String | Int | Seq[
    String | Int | Seq[ ...

I was hoping to be able to tie the knot in the recursion by shifting things and relying on hash-consing to share the same type instance, but it looks like Rec[JA, JsonPrimitive] type application results in a unique match type that needs to be reduced. Perhaps there's still a way to avoid forcing this recursion.

@Decel was also investigating why a simple case like

import scala.compiletime.ops.int

type Count[N,T] <: Tuple = N match
  case 0 => EmptyTuple
  case N => T *: Count[int.-[N, 1], T]

val a: Count[3, Int] = (1, 2, 3)

just works, without any patches.

scala / scala3