A common supertype for expressions of type KExpr<T : KSort>

[sergeypospelov]

Problem

Suppose we have such a map:

val locals: Map<String, KExpr<*>>

And we would like to take a local i0 which is known for sure to be an integer, so we expect a KExpr<KBv32Sort>.
We would write something like this:

val intLocal = locals.getValue("i0") as KExpr<KBv32Sort>

The problem here is that the generic part of the cast is unchecked, so if there isn't KExpr<KBv32Sort> but KExpr<KFpSort>, a runtime exception won't be thrown at this line.

Actually, a ClassCastException will be thrown in the first place, where we use intLocal as KExpr<KBv32Sort>, e.g. mkBvAdd(i0, ...), so it will be quite unexpected.

The same reasonings apply to any types of sorts.

Suggestion

I wonder, if it's possible to introduce a common supertype for all operations which produce KExpr<KBv32Sort>, e.g. KBv32Expr or something like this. As the result, we can write the following:

val intLocal = locals.getValue("i0") as KBv32Expr

The actual cast happens exactly at this line, so they won't be any unexpected exceptions.

[Saloed]

My suggestion is to define an extension function that performs a "checked" cast.

fun <T : KSort> KExpr<*>.to(sort: T): KExpr<T> = with(ctx) {
    check(this@to.sort == sort) { "Sort mismatch" }

    @Suppress("UNCHECKED_CAST")
    this@to as KExpr<T>
}

Usage example:

fun sample(expr: KExpr<*>) = with(ctx) {
    expr.to(mkBv32Sort())
    expr.to(boolSort)
    expr.to(mkArraySort(intSort, intSort))
}