Unpredictable reporting on circular type classes

[vkuncak]

On Version: 0.9.8.7-14-g7fd69e2
this code

import stainless.annotation.*
object LawAndOrder:

  def sign(i: Int): Int =
    if i > 0 then 1 
    else
      if i < 0 then -1 else 0

  sealed trait Ordering[T]:
    def compare(x: T, y: T): Int

    @law 
    def inverse(x: T, y: T): Boolean =
      sign(compare(x, y)) == -sign(compare(y, x))

/*
      @law 
      def transitive(x: T, y: T, z: T): Boolean =
        !(compare(x, y) > 0 && compare(y, z) > 0) || (compare(x, z) > 0)

      @law 
      def consistent(x: T, y: T, z: T): Boolean =
        !(compare(x, y) == 0) || (sign(compare(x, z)) == sign(compare(y, z)))
 */
  end Ordering

  val IntOrder = new Ordering[Int]:
    def compare(x: Int, y: Int) = 
      if x == y then 0
      else if x < y then -1
      else 1

  def LexOrder[A,B](ordA: Ordering[A], ordB: Ordering[B]): Ordering[(A,B)] =
    new Ordering[(A,B)] {
      def compare(x: (A, B), y: (A, B)): Int =          
        val compA = ordA.compare(x._1, y._1)          
        if compA == 0 then ordB.compare(x._2, y._2)
        else compA

      override def inverse(x: (A,B), y: (A,B)): Boolean =  
        ordA.inverse(x._1, y._1) && ordB.inverse(x._2,y._2) &&
        sign(compare(x, y)) == -sign(compare(y, x))
    }


end LawAndOrder

in two consecutive runs reports returns different error message:

kuncak@kuncak-x1yog6: (main)~/software/stainless/tmp$ stainless LawAndOrder.scala --timeout=10
[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing finished                                   
[  Info  ] Finished lowering the symbols                            
[  Info  ] Generating VCs for 17 functions...                       
[ Fatal  ] LawAndOrder.scala:13:23: Variable T 43 is not defined in context:
[ Fatal  ] Kind: argument types (call isOrdering(x, T))
[ Fatal  ] Check SAT: false
[ Fatal  ] Emit VCs: true
[ Fatal  ] Functions: isOrdering, choose$0, IntAbsToBigInt, ObjectPrimitiveSize, BigIntAbs, compare, choose$2, is$anon
[ Fatal  ] ADTs: Object
[ Fatal  ] Type Variables: 
[ Fatal  ] Term Variables:
[ Fatal  ]   A: (Object) => Boolean
[ Fatal  ]   B: (Object) => Boolean
[ Fatal  ]   thiss: { x: Object | (is$anon(x, A, B)): @dropConjunct  }
[ Fatal  ]   x: ({ x: Object | (A(x)): @dropConjunct  }, { x: Object | (B(x)): @dropConjunct  })
[ Fatal  ]   y: ({ x: Object | (A(x)): @dropConjunct  }, { x: Object | (B(x)): @dropConjunct  })
[ Fatal  ]   T: (Object) => Boolean
[ Fatal  ]   T == A
[ Fatal  ]   thiss.isInstanceOf[$anon]
[ Fatal  ]   x: Object
[ Fatal  ]   x == thiss.ordA
[ Fatal  ]   x: Object
[ Fatal  ]   x == x
[ Fatal  ] 
               def inverse(x: T, y: T): Boolean =
                                 ^
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.
kuncak@kuncak-x1yog6: (main)~/software/stainless/tmp$ stainless LawAndOrder.scala --timeout=10
[  Info  ] Finished compiling                                       
[  Info  ] Preprocessing finished                                   
[  Info  ] Finished lowering the symbols                            
[  Info  ] Generating VCs for 17 functions...                       
[ Fatal  ] LawAndOrder.scala:36:21: Call to function compare is not allowed here, because it is mutually recursive with the current function compare
                   val compA = ordA.compare(x._1, y._1)          
                               ^^^^^^^^^^^^^^^^^^^^^^^^
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.

Maybe depending on the solver the termination checker takes different paths and some of them trigger the bug.

The ability to handle the example may need some assumptions about well-formedness on type arguments that do not necessarily hold in the presence of polymorphic recursion (which we don't handle, but the termination checker is not using that fact either).