Reasoning with atomic split results:
If A' ~~> A,
B' ~~> B,
Bi in spl(B)
A << Bi
then there exists Bm' ~~> Bm, s.t.
|B| << |Bm|, A << Bm << Bi
What’s next
We need to show all Bm' merges to B'
|B| << |Bm1| & |Bm2| & ... & |Bmi|
Bm1 & Bm2 & ... & Bmi << B
goal:
Bm1' & ... & Bmi' <: B'
Hard to prove
Another attempt
after realizing the counterexample in Compute the Intermediate Type, we propose the following lemma:
If A' ~~> A,
B' ~~> B,
Bi in spl(B)
A << Bi
then there exists Bm1' ~~> Bm1, Bm2' ~~> Bm2, s.t.
A << Bm1
Bm1' <: Bm2'
Bm2 << Bi
The refined testing gives the following counterexample:
test/Translate/Spec.hs:58:69:
1) split lemma precise split lemma
Falsified (after 545 tests):
STypPair mu . (((mu . (((mu . (1)) & (mu . ((1 -> mu . (I))))))) & (mu . (mu . (((1) & ((1 -> mu . (I))))))))) mu . (mu . (((((mu . (1)) & (mu . ((1 -> mu . (I)))))) & (mu . (((1) & ((1 -> mu . (I)))))))))
maybe test type
tst1a = inputTyp "(mu a. (a -> (mu b. (Top -> a)))) & (mu a. Top -> (mu b. (b -> Int) ))"
tst1b = inputTyp "mu a. (Top -> (mu b. ((b -> a) & (b -> Int))))"
mu a. a -> (
mu b. (Top -> a)
)
&
mu a. Top -> (
mu b. (b -> Int)
)
<:
mu a. Top -> (
mu b. (b -> a & b -> Int)
)