inconsistent support for default constructor parameters?

[mwookawa]

I'm getting inconsistencies in support for defaults in case class constructors. eg, the following crashes stainless with a missing dependency

2020.09.14 10:45:26 INFO => FAIL 2020.09.14 10:45:26 ERROR b$0 depends on missing dependencies: $default$1$1.

import stainless._
import stainless.lang._
import stainless.collection._
import stainless.lang.StaticChecks._
import stainless.annotation._
import stainless.proof._

import stainless.lang.{Some, Option, None}

case class A() {}
case class B(a: A = new A)
case class C() { val b = new B 

whereas the following more complex example compiles in stainless without error

object Aggregation {
  def lastValue = new LastValueAggregation
}

sealed trait Aggregation { def foo = 0  }

object LastValueAggregation {
  private val INITIAL_VALUE: Long = 0L
}

case class LastValueAggregation(private var lastValue: Long = LastValueAggregation.INITIAL_VALUE)
extends Aggregation
{
}

Could I get more insight as to why recovery fails for the first example? (but not the second)

[vkuncak]

This works (when you don't use default parameters):

case class A() {}
case class B(a: A = A())
case class C() { val b = B(A()) }

so the bug is triggered when supplying the default values, which happens at the point of call of the constructor. This also crashes:

object Test {
  case class B(a: Int = 0)
  def test = {
    val b = B()
    42
  }
}

[vkuncak]

Also, it looks like it is not in the actual desugaring, but in a prior sanitization phase that does not expect to see this code.