IsInstanceOf on parametric type leads to type-checking error

[jad-hamza]

Should we reject this upfront?

object IsInstanceOfParam {
  sealed abstract class A
  case class C() extends A
  def f[T <: A](a: T): Boolean = {
    a.isInstanceOf[C]
  }
}

[ Fatal  ] Run has failed with error: inox.ast.TypeOps$TypeErrorException: Type error: a is C, expected Boolean, 
[ Fatal  ] found <untyped>
[ Fatal  ] 
[ Fatal  ] Typing explanation:
[ Fatal  ] a is C is of type <untyped>
[ Fatal  ]   a is of type T

[romac]

I’d have thought that TypeEncoding would handle this properly, I’ll take a look!

[romac]

Might be related to #666. Will attempt to fix both in #685.

[romac]

The issue is that, after AdtSpecialization, we get:

def f$30[T$37 <: A$85](a$6: T$37): Boolean = a$6.isInstanceOf[{ v$11: A$85 | v$11 is C$9 }]

(A is rightly considered to be an ADT at this point)

Then, after RefinementLifting:

def f$30[T$37 <: A$85](a$6: T$37): Boolean = a$6 is C$9

On current master, after TypeEncoding:

def f$30[T$37](a$6: T$37): Boolean = a$6 is C$9

which does not type-check, obviously, since a$6 is of generic type T$37.

With #685 we get the following after TypeEncoding:

abstract class A$85
case class C$9() extends A$85

@synthetic
abstract class Object$0
case class Open$0(value$5: BigInt) extends Object$0

def f$30(T$38: (x$83: Object$0) => { b$6: Boolean | @unchecked (b$6 ==> (x$83 is A$89 && true)) }, a$6: { x$84: Object$0 | @unchecked T$38(x$84) }): Boolean = {
  a$6 is C$9
}

which does not type-check either because a$6 has type Object$0, which is unrelated to C$9.

I am not quite sure what to do about this, perhaps we should not specialize A to an ADT, because of the bound T <: A in f, which would imply relying on functions' bodies to determine whether or not to specialize a class to an ADT.

Note that, even if we do not specialize A, we get the following before/after TypeEncoding on master:

// Before
def f$30[T$37 <: A$85](a$6: T$37): Boolean = a$6.isInstanceOf[C$9]

// After
def f$30[T$37](a$6: T$37): Boolean = false

which is wrong as well.

Whereas with #685, we get:

def f$30(T$38: (x$83: Object$0) => { b$6: Boolean | @unchecked (b$6 ==> isA$0(x$83)) }, a$6: { x$84: Object$0 | @unchecked T$38(x$84) }): Boolean = {
  isC$0(a$6)
}

@unchecked @synthetic
def isA$0(x$86: Object$0): Boolean = isC$0(x$86)

@unchecked @synthetic
def isC$0(x$92: Object$0): Boolean = x$92 is C$9 && true

@synthetic
abstract class Object$0
case class C$9() extends Object$0
case class Open$0(value$5: BigInt) extends Object$0

which looks right and does indeed type-checks.

@jad-hamza @samarion What do you think?

PS: I have omitted the synthetic postcondition on f for clarity.