Closed DavePearce closed 7 years ago
A minimal assertion which exhibits the failure is:
type binop is ({test2.expr left, int op} b) where (b.op == 1)
type expr is (int|test2.binop this)
assert:
forall(expr e1):
if:
e1 == {left: 1, op: 1}
then:
{left: e1, op: 1} is test2.expr
This is somehow related to the invariant as, without this, it's fine. Debugging this, it seems that the truths
worklist in CoercsiveSubtypeOperator
is building like so:
TRUTHS: [!int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int, !int]
TRUTHS: [!int, !int, !int, !int, !int, !int, !int, !int, !int, !int]
That does not look good!
Looking at the outermost isSubtype()
we can see that it's being called with increasingly large tests:
CHECKING: void:false:true :> ({(expr&(expr&{int left,int op})) left,int op}&(((((!(test2.expr)&!(int))&(!(int)&!(test2.binop)))&((!(int)&!(test2.
binop))&(!(test2.binop)&(!(test2.expr)&!(int)))))&(((!(int)&!(test2.binop))&(!(test2.binop)&(!(test2.expr)&!(int))))&((!(test2.binop)&(!(test2.ex
pr)&!(int)))&((!(test2.expr)&!(int))&(!(int)&!(test2.binop))))))&((((!(int)&!(test2.binop))&(!(test2.binop)&(!(test2.expr)&!(int))))&((!(test2.bi
nop)&(!(test2.expr)&!(int)))&((!(test2.expr)&!(int))&(!(int)&!(test2.binop)))))&(((!(test2.binop)&(!(test2.expr)&!(int)))&((!(test2.expr)&!(int))
&(!(int)&!(test2.binop))))&(((!(test2.expr)&!(int))&(!(int)&!(test2.binop)))&((!(int)&!(test2.binop))&(!(test2.binop)&(!(test2.expr)&!(int)))))))
)):true:true
These just get bigger and bigger. I'm not sure where it could be getting called from though?
UPDATE: this is coming via extractReadableRecord()
from TypeTestClosure
. This must be somehow related to a lack of complex simplification?
This seems to be a critical line from the proof:
{left: e1, op: 1} is ((!expr&!int)&(!int&!binop))&((!int&!binop)&(!binop&(!expr&!int)))
Certainly, this could be simplified.
Observe that in TypeTestClosure
there is the following note:
// FIXME: at the moment, TypeSystem.intersect is not working
// properly. It's possible that using new Type.Intersection could
// potentially lead to unbounded growth of the overall type.
Type intersection = new Type.Intersection(lhsT, rhsT);
This would seem to be the heart of the problem here.
The issue with infinite loops is now closed. However, there remains some problems related to type tests.
The following is generating a
StackOverflowException
for reasons unknown: