Wrong type checking when using type definition

[samuelchassot]

I was working on the Zipper for Regex implementation, and the well-formedness check didn't pass so I minimised the example and here it is:

import stainless.collection._
import stainless.lang._
import stainless.annotation._

object VerifiedRegex {
  abstract sealed class Regex[C] {}
  case class ElementMatch[C](c: C) extends Regex[C]
  case class Star[C](reg: Regex[C]) extends Regex[C]
  case class Union[C](regOne: Regex[C], regTwo: Regex[C]) extends Regex[C]
  case class Concat[C](regOne: Regex[C], regTwo: Regex[C]) extends Regex[C]
  case class EmptyExpr[C]() extends Regex[C]
  case class EmptyLang[C]() extends Regex[C]
}

object ZipperRegex {
  import VerifiedRegex._
  type Context[C] = List[Regex[C]]
  type Zipper[C] = Set[Context[C]]

  def test[C](r: Regex[C]): Zipper[C] = {
    Set(List(r))
  }
}

And here is the error:

❯ stainless-dotty RegexZippers.scala
[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing the symbols...                             
[ Error  ] RegexZippers.scala:27:5: Type error: Set(Cons[Regex[C]](r, Nil[Regex[C]]())), expected Set[C],
[ Error  ] found Set[List[Regex[C]]]
[ Error  ] 
[ Error  ] Typing explanation:
[ Error  ] Set(Cons[Regex[C]](r, Nil[Regex[C]]())) is of type Set[List[Regex[C]]]
[ Error  ]   Cons[Regex[C]](r, Nil[Regex[C]]()) is of type Cons[Regex[C]]
[ Error  ]     r is of type Regex[C]
[ Error  ]     Nil[Regex[C]]() is of type Nil[Regex[C]]
               Set(List(r))
               ^^^^^^^^^^^^
[ Fatal  ] Well-formedness check failed after extraction
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.

When happening in the real project, the error is far more complicated and the type of the function found is <untyped> but I presume this is the same bug.

Apparently it is expecting Set[C] instead of Set[Context[C]] i.e., Set[List[Regex[C]]]

[samuelchassot]

indeed, when printing the trees, we get:

[ Debug  ] @final
[ Debug  ] def test[C](r: Regex[C]): Set[C] = Set(Cons[Regex[C]](r, Nil[Regex[C]]()))

[samuelchassot]

So the expansion of type Zipper[C] is wrong. I need to investigate why.

[samuelchassot]

As the tree is wrong before the preprocessing phase, I'm guessing the problem comes from the extraction.

[samuelchassot]

The bug comes from the extraction, in CodeExtract.scala

stainless/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala

Line 2364 in 0010368

case AppliedType(tr: TypeRef, Seq(tp)) if isSetSym(tr.symbol) =>

case AppliedType(tr: TypeRef, Seq(tp)) if isSetSym(tr.symbol) =>
        xt.SetType(extractType(tp))

in the isSetSym, the type aliases are resolved, so the type Zipper[C] is resolved to be a set symbol. However, here tp is C (in the case of type Zipper[C] = Set[List[Regex[C]]], so when extracted it is C instead of List[Regex[C]]. So it has to dealias types at that stage. I'm working on a fix.

[samuelchassot]

This bug appears also with other types treated on their own, like Map:

type TestType[A] = Map[Int, List[A]]
val t: TestType[Int] = Map(1 -> List(1, 2, 3), 2 -> List(4, 5, 6))