Internal type error in extraction when passing anonymous trait instance to method expecting trait

[vkuncak]

This code:

object WrapperTest:
  trait Spec {
  }

  case class Wrapper(underlying: Spec) extends Spec {
  }

  def test =
    def w: Spec = Wrapper(new Wrapper(w) { })

end WrapperTest

gives the error message below. It seems fine to reject such wrapper as it causes non-termination etc., but we seem to reject by way of an internal error and possibly by accident, so we should at least report a meaningful error to the user.

[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing the symbols...                             
[ Error  ] WrapperTest.scala:9:5: Type error: @final
[ Error  ] def w: Spec = Wrapper({
[ Error  ]   case class $anon extends Wrapper {
[ Error  ]     
[ Error  ]   
[ Error  ]     
[ Error  ]   }
[ Error  ]   $anon()
[ Error  ] })
[ Error  ] (), expected Unit,
[ Error  ] found <untyped>
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] @final
[ Error  ] def w: Spec = Wrapper({
[ Error  ]   case class $anon extends Wrapper {
[ Error  ]     
[ Error  ]   
[ Error  ]     
[ Error  ]   }
[ Error  ]   $anon()
[ Error  ] })
[ Error  ] () is of type <untyped>
[ Error  ]   Wrapper({
[ Error  ]     case class $anon extends Wrapper {
[ Error  ]       
[ Error  ]     
[ Error  ]       
[ Error  ]     }
[ Error  ]     $anon()
[ Error  ]   }) is of type <untyped>
[ Error  ]     case class $anon extends Wrapper {
[ Error  ]       
[ Error  ]     
[ Error  ]       
[ Error  ]     }
[ Error  ]     $anon() is of type $anon
[ Error  ]       $anon() is of type $anon
[ Error  ]   () is of type Unit
               def w: Spec = Wrapper(new Wrapper(w) { })
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[ Fatal  ] Well-formedness check failed after extraction
[ Error  ] Stainless terminated with an error.

[vkuncak]

Same error message if I define test as

  def test: Unit = {
    def w: Spec = Wrapper(new Wrapper(w) { })

    ()
  }

[vkuncak]

An explicit asInstanceOf test works and this passes entirely (there are no methods to cause infinite recursion):

object WrapperTest:
  trait Spec { }
  case class Wrapper(underlying: Spec) extends Spec { }
  def test: Unit = {
    def w: Wrapper = Wrapper((new Wrapper(w) { }).asInstanceOf[Wrapper])
    ()
  }
end WrapperTest

So it looks like there's some limitation in how our type checker or extractor uses expected type in the presence of subtyping with anonymous classes