TotalityCheck property failure

see: https://travis-ci.org/johnynek/bosatsu/jobs/497642577#L1280

This may be another version of list unions not having a normal form (which I guess will be true of any recursive type we support). Although, I don't think it means the totality check is wrong, I think the laws are just hard to always check since we don't have good equality on patterns.

Actually... thinking more: aren't two patterns equal if you can a - b is empty and b - a is empty? Maybe that can solve this.

[info] - a - b = c then c - b == c, because we have already removed all of b *** FAILED *** (4 seconds, 28 milliseconds)

[info]     Message: eqList.eqv(c1, c) was false fmms - (b=Tuple2([_], Tuple2(aY1m, Tuple2(((_ | _ | 2977339074909873852506211673203605072667344453293923936340368649421682839343) | Tuple2(9223372036854775807, Unit) | U(_, eRlqkvtixq, cffybfuifui, _)) | Ynpjiywz8bl([*_, 'b', _, _, 'qMycqq'], _, _, o5gytdSlm, 'fgwwOrArw'), Tuple2(csze6bd | (_ | 1 | Yaxfp(_, -86217850374853394725283764713605192424377470349271541968, _, _, 123593799423704450274051711677012628376533123844301678460)) | 168571749856275610817274295096998700578562140158857862720 | 'arut6', Tuple2(_, Unit))))) | (Tuple2(Tuple2(_ | _ | pnfz, Unit), Tuple2(lpzgp, Tuple2(Tuple2([feslotyjcq, 'kwozg7pkyn', 'e', fWm], Unit), Tuple2(_, Unit)))) | [Tuple2(_ | _, Tuple2('hvyp0mWs', Tuple2(ye | 'xhVt' | 'ow0folqfnjg', Tuple2(3757754052132570126, Tuple2('yspxwVhirhk', Tuple2(iye, Unit)))))), _, ('a9f' | yqekkHj7j) | -11075175860507799335397627768911666880 | (dm8bxgv | _ | _) | _, kusroauhi]) | [cohmxXp | _ | 'yrqaj' | q, (Xvb(_, -1614349285023064014974426739321847944242283635061747933, nan, 'ravhrt4gspf') | -7067862713461334777558978967287414430214317997807437408 | 'z9y' | _) | lvhe | [[28265216442691347340814371254725089358957573247536868482516912957549253540, 'aulh', 'bvknz', yyzrwazEI, 0], hAhXrf, _ | ndbF] | ['aofoxafQ', iBy | dzl, *_], []] | Tuple2(_, Tuple2('n', Tuple2([[*sfei], *uo3k7fy22yz, 'mqerd1ikr'], Tuple2(_, Tuple2(j, Tuple2(jpgfsun, Unit))))))) = List([], [_], [_, _], [_, _, [], _, *fmms], [_, _, [_, *_], *fmms]) - b = List([], [_], [_, _], [Tuple2(_, _), _, [], _, *fmms], [Tuple2(_ | _, Tuple2('hvyp0mWs', Tuple2(ye | 'xhVt' | 'ow0folqfnjg', Tuple2(3757754052132570126, Tuple2('yspxwVhirhk', Tuple2(iye, Unit)))))), _, [], kusroauhi, _, *fmms], [Tuple2(_, _), _, [_, *_], *fmms], [Tuple2(_ | _, Tuple2('hvyp0mWs', Tuple2(ye | 'xhVt' | 'ow0folqfnjg', Tuple2(3757754052132570126, Tuple2('yspxwVhirhk', Tuple2(iye, Unit)))))), _, [_, *_]], [Tuple2(_ | _, Tuple2('hvyp0mWs', Tuple2(ye | 'xhVt' | 'ow0folqfnjg', Tuple2(3757754052132570126, Tuple2('yspxwVhirhk', Tuple2(iye, Unit)))))), _, [_, *_], kusroauhi, _, *fmms]) diff = List([_, _, [], _, *_], [_, _, [_, *_], *_])
[info]     Location: (TotalityTest.scala:513)
[info]     Occurred when passed generated values (
[info]       arg0 = Var(fmms),
[info]       arg1 = Union(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(ListPat(List(Right(WildCard))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Var(aY1m), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(Union(Union(WildCard,NonEmptyList(WildCard, Literal(Integer(2977339074909873852506211673203605072667344453293923936340368649421682839343)))),NonEmptyList(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Literal(Integer(9223372036854775807)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(U)),List(WildCard, Var(eRlqkvtixq), Var(cffybfuifui), WildCard)))),NonEmptyList(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Ynpjiywz8bl)),List(ListPat(List(Left(None), Right(Literal(Str(b))), Right(WildCard), Right(WildCard), Right(Literal(Str(qMycqq))))), WildCard, WildCard, Var(o5gytdSlm), Literal(Str(fgwwOrArw)))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(Var(csze6bd),NonEmptyList(Union(WildCard,NonEmptyList(Literal(Integer(1)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Yaxfp)),List(WildCard, Literal(Integer(-86217850374853394725283764713605192424377470349271541968)), WildCard, WildCard, Literal(Integer(123593799423704450274051711677012628376533123844301678460)))))), Literal(Integer(168571749856275610817274295096998700578562140158857862720)), Literal(Str(arut6)))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(WildCard, PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))))))))))),NonEmptyList(Union(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(WildCard,NonEmptyList(WildCard, Var(pnfz))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Var(lpzgp), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(ListPat(List(Right(Var(feslotyjcq)), Right(Literal(Str(kwozg7pkyn))), Right(Literal(Str(e))), Right(Var(fWm)))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(WildCard, PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))))))))),NonEmptyList(ListPat(List(Right(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(WildCard,NonEmptyList(WildCard)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Literal(Str(hvyp0mWs)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(Var(ye),NonEmptyList(Literal(Str(xhVt)), Literal(Str(ow0folqfnjg)))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Literal(Integer(3757754052132570126)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Literal(Str(yspxwVhirhk)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Var(iye), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List())))))))))))))), Right(WildCard), Right(Union(Union(Literal(Str(a9f)),NonEmptyList(Var(yqekkHj7j))),NonEmptyList(Literal(Integer(-11075175860507799335397627768911666880)), Union(Var(dm8bxgv),NonEmptyList(WildCard, WildCard)), WildCard))), Right(Var(kusroauhi)))))), ListPat(List(Right(Union(Var(cohmxXp),NonEmptyList(WildCard, Literal(Str(yrqaj)), Var(q)))), Right(Union(Union(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Xvb)),List(WildCard, Literal(Integer(-1614349285023064014974426739321847944242283635061747933)), Var(nan), Literal(Str(ravhrt4gspf)))),NonEmptyList(Literal(Integer(-7067862713461334777558978967287414430214317997807437408)), Literal(Str(z9y)), WildCard)),NonEmptyList(Var(lvhe), ListPat(List(Right(ListPat(List(Right(Literal(Integer(28265216442691347340814371254725089358957573247536868482516912957549253540))), Right(Literal(Str(aulh))), Right(Literal(Str(bvknz))), Right(Var(yyzrwazEI)), Right(Literal(Integer(0)))))), Right(Var(hAhXrf)), Right(Union(WildCard,NonEmptyList(Var(ndbF)))))), ListPat(List(Right(Literal(Str(aofoxafQ))), Right(Union(Var(iBy),NonEmptyList(Var(dzl)))), Left(None)))))), Right(ListPat(List())))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(WildCard, PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Literal(Str(n)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(ListPat(List(Right(ListPat(List(Left(Some(sfei))))), Left(Some(uo3k7fy22yz)), Right(Literal(Str(mqerd1ikr))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(WildCard, PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Var(j), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Var(jpgfsun), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List())))))))))))))))
[info]     )

Saw this again. I need to run this down. I'm more concerned there is a real issue lurking here. Clearly it is very rare, but, possible;

[info] - a - b = c then c - b == c, because we have already removed all of b *** FAILED *** (2 seconds, 751 milliseconds)
[info]   TestFailedException was thrown during property evaluation.
[info]     Message: eqList.eqv(c1, c) was false _ - (b=[sexzvprlrk | Tuple2(['mtdiwtyuz'], Tuple2(bf, Tuple2(_ | 'pldwGc' | d37ex5 | 'ze', Tuple2(tggjLBa7pqx@'kJx', Unit)))) | GK4Xfgcipl(_, glAgD9esr, ws@_), jrtbcbtf] | [*jeirnnqtGm, Tuple2(['pcy', 38027992902547094095662547774507581670], Tuple2(p@(bff1tt | 'jpowqrg' | 3487874632454807417865993456819222103), Tuple2([*adwaiivbyjc, s3ean, _] | Tuple2('otxy', Tuple2(_, Unit)) | 21141336622304968484529379404094378038, Unit)))] | Zwez('i9h')) = List([], [_], [_, jrtbcbtf, _, *_]) - b = List([], [Tuple2([*_], _)], [Tuple2(['pcy', 38027992902547094095662547774507581670], Tuple2(_, Tuple2([], _)))], [Tuple2(['pcy', 38027992902547094095662547774507581670], Tuple2(_, Tuple2([_], _)))], [_, jrtbcbtf, _, *_]) diff = List([_])
[info]     Location: (TotalityTest.scala:501)
[info]     Occurred when passed generated values (
[info]       arg0 = WildCard,
[info]       arg1 = Union(ListPat(List(Right(Union(Var(sexzvprlrk),NonEmptyList(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(ListPat(List(Right(Literal(Str(mtdiwtyuz))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Var(bf), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(WildCard,NonEmptyList(Literal(Str(pldwGc)), Var(d37ex5), Literal(Str(ze)))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Named(tggjLBa7pqx,Literal(Str(kJx))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))))))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(GK4Xfgcipl)),List(WildCard, Var(glAgD9esr), Named(ws,WildCard)))))), Right(Var(jrtbcbtf)))),NonEmptyList(ListPat(List(Left(Some(jeirnnqtGm)), Right(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(ListPat(List(Right(Literal(Str(pcy))), Right(Literal(Integer(38027992902547094095662547774507581670))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Named(p,Union(Var(bff1tt),NonEmptyList(Literal(Str(jpowqrg)), Literal(Integer(3487874632454807417865993456819222103))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Union(ListPat(List(Left(Some(adwaiivbyjc)), Right(Var(s3ean)), Right(WildCard))),NonEmptyList(PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(Literal(Str(otxy)), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Tuple2)),List(WildCard, PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List()))))), Literal(Integer(21141336622304968484529379404094378038)))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Unit)),List())))))))))), PositionalStruct((PackageName(NonEmptyList(Bosatsu, Predef)),ConstructorName(Zwez)),List(Literal(Str(i9h))))))
[info]     )

https://travis-ci.org/johnynek/bosatsu/jobs/507415500#L1312

johnynek / bosatsu

TotalityCheck property failure #147