Crashes when changing type parameters during instantiation with laws

[vkuncak]

I'd love if we could do this:

import stainless.lang._
import stainless.annotation._

object LawForall {
  trait Forall[T] {
    def apply(x: T): Boolean 

    @law
    def holdsFor(x: T): Boolean =
      apply(x)
  }

  trait Commutative[A] extends Forall[(A,A)] {
    def op(x: A, y: A): A

    override def apply(x: (A,A)): Boolean = {
      op(x._1,x._2) == op(x._2, x._1)
    }
  }

  val PlusCommutative = new Commutative[BigInt]() {
    def op(x: BigInt, y: BigInt) = x + y
  }
}

but we get an internal crash.

On the other hand:

• commenting the @law leads to no crash (and no vcs, as expected)
• The code below that does not use pair type works:

import stainless.lang._
import stainless.annotation._

object LawForall {
  trait Forall2[T] {
    def apply(x: T, y: T): Boolean 

    @law
    def holdsFor(x: T, y: T): Boolean =
      apply(x, y)
  }

  trait Commutative[A] extends Forall2[A] {
    def op(x: A, y: A): A

    override def apply(x: A, y: A): Boolean = {
      op(x,y) == op(y, x)
    }
  }

  object PlusCommutative extends Commutative[BigInt] {
    def op(x: BigInt, y: BigInt) = x + y
  }
}

[samarion]

Probably some bug in type encoding (which triggers because the type arguments aren't bijective in Commutative[A] extends Forall[(A,A)]). What does the crash say?

[mario-bucev]

Not TypeEncoding this time! It is the dispatching process in MethodLifting (and unrelated to @law). If we were to remove PlusCommutative, we get for the abstract apply, after MethodLifting:

def apply[T](thiss: Forall[T], x: T): Boolean = if (thiss.isInstanceOf[Commutative[_ >: Nothing <: Any]]) {
  apply[_ >: Nothing <: Any](@DropVCs thiss.asInstanceOf[Commutative[_ >: Nothing <: Any]], {
    assume(x.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)])
    @DropVCs x.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)]
  })
} else {
  apply[T](@DropVCs thiss.asInstanceOf[ForallExt[T]], x)
}

but this fails the well-formedness check. So the "problem" is really due to type arguments not being bijective. If this is working as intended, the FragmentChecker should at least reject these definitions. Otherwise, we could imagine having a phase that could (somehow) encode/unveil existential types but this seems to be an unsoundness spring. But we could then support GADTs :)

[samarion]

Hmm, why does this fail the well-formedness check?

[mario-bucev]

Due to a typing error, here is the message I get:

Ensuring well-formedness after phase MethodLifting...
i1397a.scala:5:9: Type error: if (thiss$6.isInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]]) {
  holdsFor$2[_ >: Nothing <: Any](@DropVCs thiss$6.asInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]], {
    assume(x$100.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)])
    @DropVCs x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)]
  })
} else {
  holdsFor$3[T$60](@DropVCs thiss$6.asInstanceOf[ForallExt$0[T$60]], x$100)
}, expected Boolean,
found <untyped>

Typing explanation:
if (thiss$6.isInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]]) {
  holdsFor$2[_ >: Nothing <: Any](@DropVCs thiss$6.asInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]], {
    assume(x$100.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)])
    @DropVCs x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)]
  })
} else {
  holdsFor$3[T$60](@DropVCs thiss$6.asInstanceOf[ForallExt$0[T$60]], x$100)
} is of type <untyped>
  thiss$6.isInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]] is of type Boolean
    thiss$6 is of type Forall$0[T$60]
  holdsFor$2[_ >: Nothing <: Any](@DropVCs thiss$6.asInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]], {
    assume(x$100.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)])
    @DropVCs x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)]
  }) is of type <untyped>
    @DropVCs thiss$6.asInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]] is of type CommutativeExt$0[_ >: Nothing <: Any]
      thiss$6.asInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]] is of type CommutativeExt$0[_ >: Nothing <: Any]
        thiss$6 is of type Forall$0[T$60]
    assume(x$100.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)])
    @DropVCs x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)] is of type (_ >: Nothing <: Any, _ >: Nothing <: Any)
      x$100.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)] is of type Boolean
        x$100 is of type T$60
      @DropVCs x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)] is of type (_ >: Nothing <: Any, _ >: Nothing <: Any)
        x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)] is of type (_ >: Nothing <: Any, _ >: Nothing <: Any)
          x$100 is of type T$60 because holdsFor was instantiated with A$112:=_ >: Nothing <: Any with type (CommutativeExt$0[A$112],(A$112, A$112)) => Boolean
  holdsFor$3[T$60](@DropVCs thiss$6.asInstanceOf[ForallExt$0[T$60]], x$100) is of type Boolean
    @DropVCs thiss$6.asInstanceOf[ForallExt$0[T$60]] is of type ForallExt$0[T$60]
      thiss$6.asInstanceOf[ForallExt$0[T$60]] is of type ForallExt$0[T$60]
        thiss$6 is of type Forall$0[T$60]
    x$100 is of type T$60 because holdsFor was instantiated with T$63:=T$60 with type (ForallExt$0[T$63],T$63) => Boolean
  trait Forall[T] {
        ^^^^^^^^^^^...
Well-formedness check failed after phase MethodLifting

[samarion]

Hmm, so holdsFor is the broken method in that snippet. Do you also have a failing well-formedness check for apply?

We would need to see the definition of holdsFor generated for Commutative by the law phase to understand why the function invocation isn't being typed correctly.

[mario-bucev]

The same crash occurs without @law. For the same snippet (modulo val PlusCommutative replaced with trait PlusCommutative for less clutter, and with @law removed), before MethodLifting, we have:

Click to expand

```scala @abstract @sealed sealed abstract class Forall$0[T$58] { @method(Forall$0) @derived(holdsFor$0) def holdsFor$1((x$104: T$58) @pure): Boolean = this.apply$12(x$104) @method(Forall$0) def holdsFor$0((x$100: T$58) @pure): Boolean = this.apply$12(x$100) @abstract @method(Forall$0) def apply$12((x$99: T$58) @pure): Boolean = [Boolean] } @synthetic case class ForallExt$0[T$59](__x$2: BigInt) extends Forall$0[T$59] { @extern @derived(holdsFor$0) @synthetic @method(ForallExt$0) def holdsFor$4((x$113: T$59) @pure): Boolean = [Boolean] @extern @derived(apply$12) @synthetic @method(ForallExt$0) def apply$17((x$114: T$59) @pure): Boolean = [Boolean] } @abstract @sealed sealed abstract class Commutative$0[A$106] extends Forall$0[(A$106, A$106)] { @method(Commutative$0) @derived(apply$13) def apply$14((x$105: (A$106, A$106)) @pure): Boolean = this.op$0(x$105._1, x$105._2) == this.op$0(x$105._2, x$105._1) @method(Commutative$0) def apply$13((x$102: (A$106, A$106)) @pure): Boolean = this.op$0(x$102._1, x$102._2) == this.op$0(x$102._2, x$102._1) @abstract @method(Commutative$0) def op$0((x$101: A$106) @pure, (y$21: A$106) @pure): A$106 = [A$106] } @synthetic case class CommutativeExt$0[A$107](__x$1: BigInt) extends Commutative$0[A$107] { @extern @derived(op$0) @synthetic @method(CommutativeExt$0) def op$4((x$112: A$107) @pure, (y$25: A$107) @pure): A$107 = [A$107] @extern @derived(holdsFor$0) @synthetic @method(CommutativeExt$0) def holdsFor$3((x$110: (A$107, A$107)) @pure): Boolean = [Boolean] @extern @derived(apply$13) @synthetic @method(CommutativeExt$0) def apply$16((x$111: (A$107, A$107)) @pure): Boolean = [Boolean] } @abstract @sealed sealed abstract class PlusCommutative$0 extends Commutative$0[BigInt] { @method(PlusCommutative$0) def op$1((x$103: BigInt) @pure, (y$22: BigInt) @pure): BigInt = x$103 + y$22 @method(PlusCommutative$0) @derived(op$1) def op$2((x$106: BigInt) @pure, (y$23: BigInt) @pure): BigInt = x$106 + y$23 } @synthetic case class PlusCommutativeExt$0(__x$0: BigInt) extends PlusCommutative$0 { @extern @derived(op$1) @synthetic @method(PlusCommutativeExt$0) def op$3((x$109: BigInt) @pure, (y$24: BigInt) @pure): BigInt = [BigInt] @extern @derived(holdsFor$0) @synthetic @method(PlusCommutativeExt$0) def holdsFor$2((x$107: (BigInt, BigInt)) @pure): Boolean = [Boolean] @extern @derived(apply$13) @synthetic @method(PlusCommutativeExt$0) def apply$15((x$108: (BigInt, BigInt)) @pure): Boolean = [Boolean] } ```

i.e. everything is alright.

After MethodLifting (with the definition of PlusCommutative commented in order to avoid the crash occurring while transforming), we have:

Click to expand

```scala // Dispatcher @derived(holdsFor$2) @derived(holdsFor$3) def holdsFor$0[T$60](thiss$6: Forall$0[T$60], (x$100: T$60) @pure): Boolean = if (thiss$6.isInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]]) { holdsFor$2[_ >: Nothing <: Any](@DropVCs thiss$6.asInstanceOf[CommutativeExt$0[_ >: Nothing <: Any]], { assume(x$100.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)]) @DropVCs x$100.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)] }) } else { holdsFor$3[T$60](@DropVCs thiss$6.asInstanceOf[ForallExt$0[T$60]], x$100) } @derived(holdsFor$0) def holdsFor$1[T$62](thiss$8: Forall$0[T$62], (x$104: T$62) @pure): Boolean = apply$12[T$62](thiss$8, x$104) @extern @derived(holdsFor$0) @synthetic def holdsFor$2[A$112](thiss$4: CommutativeExt$0[A$112], (x$105: (A$112, A$112)) @pure): Boolean = [Boolean] @extern @derived(holdsFor$0) @synthetic def holdsFor$3[T$63](thiss$9: ForallExt$0[T$63], (x$109: T$63) @pure): Boolean = [Boolean] /////////////////////////////////////////////////////// // Dispatcher @abstract @derived(apply$13) @derived(apply$16) def apply$12[T$61](thiss$7: Forall$0[T$61], (x$99: T$61) @pure): Boolean = if (thiss$7.isInstanceOf[Commutative$0[_ >: Nothing <: Any]]) { apply$13[_ >: Nothing <: Any](@DropVCs thiss$7.asInstanceOf[Commutative$0[_ >: Nothing <: Any]], { assume(x$99.isInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)]) @DropVCs x$99.asInstanceOf[(_ >: Nothing <: Any, _ >: Nothing <: Any)] }) } else { apply$16[T$61](@DropVCs thiss$7.asInstanceOf[ForallExt$0[T$61]], x$99) } @derived(apply$15) def apply$13[A$108](thiss$0: Commutative$0[A$108], (x$102: (A$108, A$108)) @pure): Boolean = apply$15[A$108](@DropVCs thiss$0.asInstanceOf[CommutativeExt$0[A$108]], x$102) @derived(apply$13) def apply$14[A$110](thiss$2: Commutative$0[A$110], (x$103: (A$110, A$110)) @pure): Boolean = op$0[A$110](thiss$2, x$103._1, x$103._2) == op$0[A$110](thiss$2, x$103._2, x$103._1) @extern @derived(apply$13) @synthetic def apply$15[A$111](thiss$3: CommutativeExt$0[A$111], (x$106: (A$111, A$111)) @pure): Boolean = [Boolean] @extern @derived(apply$12) @synthetic def apply$16[T$64](thiss$10: ForallExt$0[T$64], (x$108: T$64) @pure): Boolean = [Boolean] /////////////////////////////////////// @abstract @derived(op$1) def op$0[A$109](thiss$1: Commutative$0[A$109], (x$101: A$109) @pure, (y$21: A$109) @pure): A$109 = op$1[A$109](@DropVCs thiss$1.asInstanceOf[CommutativeExt$0[A$109]], x$101, y$21) @extern @derived(op$0) @synthetic def op$1[A$113](thiss$5: CommutativeExt$0[A$113], (x$107: A$113) @pure, (y$22: A$113) @pure): A$113 = [A$113] -------------Classes------------- @abstract @sealed sealed abstract class Commutative$0[A$106] extends Forall$0[(A$106, A$106)] @synthetic case class CommutativeExt$0[A$107](__x$0: BigInt) extends Commutative$0[A$107] @abstract @sealed sealed abstract class Forall$0[T$58] @synthetic case class ForallExt$0[T$59](__x$1: BigInt) extends Forall$0[T$59] ```

so apply would also fail the well-formedness check if it was checked first. Are things really "broken"? To me, it seems that everything works as expected, but that such inheritance should be instead rejected?

[samarion]

I must be missing something.

In the above trees, I would expect the definitions of apply and holdsFor dispatchers to correctly type-check, no?
In the branch where the type-checking fails, we're just invoking apply / holdsFor with the type parameter instantiated to _ >: Nothing <: Any. All the arguments seem to be cast to the right type.

[mario-bucev]

Oh, I thought that _ >: Nothing <: Any means "for some T >: Nothing <: Any" therefore we would not necessarily have the same T every time we mention such wildcard?

[samarion]

No these aren't really existentials but rather "erased" types with bounds. The idea is that we can lose a bit of precision at the type level since the semantics are precisely encoded. This might lead to spurious counter-examples when invoking abstract methods but we're still far from running into this kind of problem :)

Anyway, I believe the dispatch functions should be well-formed so we have a problem in our "simple" type checking implementation.

[mario-bucev]

I see! I'll dig into the implementation and check to see what's causing the issue.

[vkuncak]

Any updates, @mario-bucev ?

[mario-bucev]

I will resume when I'm done with the current task :)