-
Notifications
You must be signed in to change notification settings - Fork 50
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Incorrect ADT member type approximation #1452
Comments
Works if my 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
|
The problem is ADT constructor types don't exist in SMT world so we have to encode 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 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 |
Seems like Stainless approximate the type of
FunDef.tp
toType
at some point, and then can't prove it's actually aFunType
.Removing
extends Type
afterFunType
solves the problem.The text was updated successfully, but these errors were encountered: