Incorrect ADT member type approximation

[mbovel]

Seems like Stainless approximate the type of FunDef.tp to Type at some point, and then can't prove it's actually a FunType.

object Test:
  sealed trait Type
  final case class AtomType(i: BigInt) extends Type
  final case class FunType(args: List[Type], res: Type) extends Type

  final case class FunDef(tp: FunType)

  def arity(funs: List[FunDef], i: BigInt) =
    require(i >= 0 && i < funs.length)
    val funDef: FunDef = funs(i)
    funDef.tp.args.length

[Warning ]  - Result for 'cast correctness' VC for arity @16:5:
[Warning ] i < BigInt("0") || i >= length[FunDef](funs) || apply[FunDef](funs, i).tp.isInstanceOf[FunType]
[Warning ] enumSubtype.scala:16:5:  => TIMEOUT
               funDef.tp.args.length
               ^^^^^^^^^^^^^^
[  Info  ] Verified: 1 / 2
[  Info  ] Done in 12.58s
[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞═════════════════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                                 ║
[  Info  ] ║ enumSubtype.scala:15:26:     arity   precond. (call apply[FunDef](funs, i))    valid    U:smt-z3  0.1 ║
[  Info  ] ║ enumSubtype.scala:16:5:      arity   cast correctness                          timeout  U:smt-z3  2.0 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 2    valid: 1    (0 from cache, 0 trivial) invalid: 0    unknown: 1    time:    2.10           ║
[  Info  ] ╚═══════════════════════════════════════════════════════════════════════════════════════════════════════╝
[  Info  ] Verification pipeline summary:
[  Info  ]   anti-aliasing, smt-z3, non-batched
[  Info  ] Shutting down executor service.

Removing extends Type after FunType solves the problem.

[mbovel]

Works if my FunDef's not in a List or, is accessed through a fixed index:

object Test2:
  sealed trait Type
  final case class AtomType(i: BigInt) extends Type
  final case class FunType(args: List[Type], res: Type) extends Type

  final case class FunDef(tp: FunType)

  def arity(funs: List[FunDef]) =
    require(funs.length > 0)
    val funDef: FunDef = funs(0)
    funDef.tp.args.length

[  Info  ] Verified: 2 / 2
[  Info  ] Done in 11.63s
[  Info  ]   ┌───────────────────┐
[  Info  ] ╔═╡ stainless summary ╞════════════════════════════════════════════════════════════════════════════════════╗
[  Info  ] ║ └───────────────────┘                                                                                    ║
[  Info  ] ║ enumSubtype.scala:15:26:   arity  precond. (call apply[FunDef](funs, BigInt("0")))  valid  U:smt-z3  0.0 ║
[  Info  ] ║ enumSubtype.scala:16:5:    arity  cast correctness                                  valid  U:smt-z3  0.1 ║
[  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[  Info  ] ║ total: 2    valid: 2    (0 from cache, 0 trivial) invalid: 0    unknown: 0    time:    0.12              ║
[  Info  ] ╚══════════════════════════════════════════════════════════════════════════════════════════════════════════╝

[samarion]

The problem is ADT constructor types don't exist in SMT world so we have to encode FunType into {x: Type | x is FunType }.

The way Inox handles refinement types in ADTs is by progressively unfolding the type and asserting at each step that it is constructed from well-typed sub-components. That's why it works for the constant index 0: Inox unfolds funs just once and you get all the right assertions to prove that funDef.tp has the right type. I expect that if you replaced 0 with 100 it would also timeout because Inox would need to perform 100 unfoldings before it had enough information to prove the property.

This could be fixed by injecting type assumptions in more places, but this would need to be done deep inside the template unfolding implementation...

A possible workaround is to define your own def getFunType(fd: FunDef): FunType = fd.tp method because IIRC dependent types are assumed on function invocation results.