Add support for RefinementType in unapply pattern

[jad-hamza]

This file fails: https://github.com/epfl-lara/bolts/blob/4cf535349deca6f2d27fefe8ba5490e1ae0f7a83/data-structures/seqs/ArrayList.scala

Edit: maybe here: https://github.com/epfl-lara/inox/blob/22de8d6b6af51fbe09bca2fc26dbdd596de8e3e8/src/main/scala/inox/ast/TypeOps.scala#L48-L83

[samarion]

You can either

1. add support for dependent types in the instantiation method, or
2. erase them with getType inside unapplyAccessor.

The first option will give better support for dependent type inference, but might be a bit more complicated.

[rjraya]

This occurred for instance in:

frontends/benchmarks/verification/valid/Count.scala

Note that 2. still gives an error, as attached.

stainless-stack-trace.txt

[samarion]

The stack trace by itself isn't very useful, please show us your code changes at least.

[rjraya]

Just added a getType call in both parameters of instantiation:

protected def unapplyAccessor(unapplied: Expr, id: Identifier, up: UnapplyPattern)(implicit s: Symbols): Expr = {
    val fd = s.lookupFunction(id)
      .filter(_.params.size == 1)
      .getOrElse(throw extraction.MalformedStainlessCode(up, "Invalid unapply accessor"))
    val unapp = up.getFunction
    val tpMap = s.instantiation(fd.params.head.tpe.getType, unapp.returnType.getType)
      .getOrElse(throw extraction.MalformedStainlessCode(up, "Unapply pattern failed type instantiation"))
    fd.typed(fd.typeArgs map tpMap).applied(Seq(unapplied))
  }

[samarion]

Hmm, that should remove all refinement types, so they are probably not the issue here.
Maybe add some print statements to debug what's going on.

[rjraya]

Complete trace of unapplyAccessor:

error.txt

[samarion]

Well those two types certainly look unifiable to me. The only issue I can think of is an id mismatch for the Option type, but I don't know where it would come from. Maybe some issue with caching?

[samarion]

I went back and looked at all your traces: I don't see any indication that instantiation is failing in unapplyAccessor. I would expect to see an exception with message "Unapply pattern failed type instantiation", but I don't see it anywhere.

In that case, the issue is probably not in unapplyAccessor, but in some other method used for UnapplyPattern typing. There are some such methods in stainless/ast/TypeOps.scala, and they probably also need the .getType calls (e.g. here).

Instead of chasing down all these instantiations, I would recommend fixing the instantiation method in Inox to support dependent types. @jad-hamza : maybe you can help Rodrigo with setting up Stainless with a local Inox?

[rjraya]

It seems like the culprit is rather: unapplyAccessorResultType who was missing 3 getTypes and unapplyAccessor who was missing one. Indeed, generalizing Inox's methods to support dependent types seems like most definitive option.