SortChecl: lookup in Empty Env

[philderbeast]

Found on #555.

> cabal test all
...
  undoANFSimplifyingWith id id
    id on empty env:                           OK
    id when env contains no lq_anf$* bindings: OK (0.10s)
      +++ OK, passed 500 tests.
    zero anf vars left afterwards, starting with:
      no anf vars:                             OK (0.05s)
        +++ OK, passed 500 tests.
      single-level anf vars:                   FAIL
...
        Use --quickcheck-replay=407282 --quickcheck-max-size=8 to reproduce.
        Use -p '/single-level anf vars/' to rerun this test only.

How I went about checking if it is reproducible (after adding hidden dependencies to the tasty test-suite so that I could run in it the REPL):

> stack repl liquid-fixpoint:tasty
...
:main --quickcheck-replay=407282 --quickcheck-max-size=8 "--pattern=single-level anf vars"
Tests
  undoANFSimplifyingWith id id
    zero anf vars left afterwards, starting with:
      single-level anf vars: FAIL (0.01s)
        *** Failed! Exception: 'Error [Error1 {errLoc = SS {sp_start = SourcePos {sourceName = "", sourceLine = Pos 1, sourceColumn = Pos 1}, sp_stop = SourcePos {sourceName = "", sourceLine = Pos 1, sourceColumn = Pos 1}}, errMsg = SortChecl: lookup in Empty Env }]' (after 32 tests):
        FlatAnfEnv {unFlatAnfEnv = Env {unEnv = fromList [("lq_anf$necmvtlyy",{mqgfcf : int | [(mqgfcf ~~
                            (&& [(vvhvaqbcfbr => ybzyzkjxclz);
                                 ("gltgdkgwdes" => "aouxfb");
                                 tabs vylzqqncup xpeqdfk] mod
                               || [exists [lrafyapmrw : @(-4);
                                           utznfu : Sdqrkejej;
                                           frgqwwyhggzp : func(0 , [func(1 , [@(3)]); Gdauhxtm])]
                                          . "xzecjwsu";
                                   forall [feaqzm : @(5);
                                           dszfdv : func(0 , [@(-5); rprjq; Porzvdevj])]
                                          . otygzfmkmv;
                                   tabs 3.0845977044261113 wrbzyynr]))]}),("lq_anf$gzgbktjtf",{vtnqjgfz : int | [(vtnqjgfz ~~
                              (((- ("rncexieck"))  :  func(1 , [func(0 , [frac; real]);
                                                                (frac int)])) (((lit "syanapeongfl" qgofelsxal) => "rriaxhalhsxn")  :  func(1 , [tdqzn]))))]}),("lq_anf$oqbgfllr",{evwnkc : int | [(evwnkc =
                            ((forall [rgzvzcbc : func(0 , [func(0 , [@(-5); gmknbh]);
                                                           (real num (frac num))]);
                                      rgxlexqztoo : Uppvmvipjfpo]
                                     . 1 => && [fsaeyreu; "upivdwrg"; "hmoyq"]) *
                               (- ((- (blmfxy))))))]}),("yuzjdkiklnbh",{zxcpas : int | [(zxcpas =
                            || [lq_anf$gzgbktjtf;
                                lq_anf$necmvtlyy;
                                lq_anf$oqbgfllr;
                                lq_anf$fzrutpnj;
                                lq_anf$hgdmbhzhzin;
                                lq_anf$vkjmidjrr])]}),("lq_anf$hgdmbhzhzin",{ysifnu : int | [(ysifnu ~~
                            ((qhbrtxkht 1.420470326002913e-2) && $ysuctabbsxxm -
                               ($lqwnegd[arbbk:=forall [jacfmom : func(1 , [Fkfavlwwn]);
                                                        qhyzwfeeggeo : gwwceprprd]
                                                       . exists [ojtnchtdp : Jynexgmkmr; xkgnc : Iiuncugn]
                                                                . ("lzwkhi"  :  @(-7))][lgogqljlv:=((- ($izipxn[osowgrrhjcp:=(- (|| [(coerce @(-6) ~ (func(0 , [func(0 , [int;
                                                                                                                                                                          int]);
                                                                                                                                                                (int frac)]) Qqoahw) in 2);
                                                                                                                                     && [3.8063749354727268;
                                                                                                                                         lrmfd;
                                                                                                                                         "nobtm"];
                                                                                                                                     ("cdpvqmuz" <=> "ukhqevzbduxv")]))])) exists [uwbezemb : Tqrwsgmr;
                                                                                                                                                                                   hxazh : @(-3);
                                                                                                                                                                                   ifzpg : func(0 , [func(0 , [(int frac);
                                                                                                                                                                                                               int;
                                                                                                                                                                                                               num]);
                                                                                                                                                                                                     func(1 , [frac]);
                                                                                                                                                                                                     xplphuxvk])]
                                                                                                                                                                                  . forall [dxukiciblmyv : Ztpqokxf;
                                                                                                                                                                                            vkzslawtl : func(0 , [func(0 , [func(0 , [num;
                                                                                                                                                                                                                                      int]);
                                                                                                                                                                                                                            @(0)]);
                                                                                                                                                                                                                  @(5)])]
                                                                                                                                                                                           . 5.2687182158699954)] => forall [xupmrpp : poghpzbzp;
                                                                                                                                                                                                                             bdqej : blkksoyf]
                                                                                                                                                                                                                            . ihmmsdgks)))]}),("lq_anf$fzrutpnj",{latikja : int | [(latikja ~~
                             (exists [hbugvaghudd : func(1 , [Fhpdogupsas]);
                                      gayisrf : func(1 , [(func(0 , [real; real]) func(1 , [int]))]);
                                      vvqcsvgla : func(0 , [func(1 , [num; num]); Dikqfmgtdga])]
                                     . tapp "lrqtxxgtc" (func(1 , [real;
                                                                   real]) fhqdver)  :  (rpzpxudsib func(0 , [Bxeqgryoxclw;
                                                                                                             Pztmyjmaevqv]))))]}),("lq_anf$vkjmidjrr",{dbggmgvpp : int | [(dbggmgvpp ~~
                               ((coerce @(-1) ~ Ifcmdydkn in || [(lit "uvttbjrcrtr" (Lupgai @(7)));
                                                                 4.874262773851095;
                                                                 "dytulgh"]) forall [dotiimeww : func(1 , [nypszlsisdnq]);
                                                                                     hknlonktqrlm : func(1 , [(@(-6) func(1 , [int]))])]
                                                                                    . (6.988209817035761 mod
                                                                                         "wzwgxojibq")))]})]}}
        Exception thrown while showing test case: 'Error [Error1 {errLoc = SS {sp_start = SourcePos {sourceName = "", sourceLine = Pos 1, sourceColumn = Pos 1}, sp_stop = SourcePos {sourceName = "", sourceLine = Pos 1, sourceColumn = Pos 1}}, errMsg = SortChecl: lookup in Empty Env }]'
        Use --quickcheck-replay=407282 --quickcheck-max-size=8 to reproduce.

1 out of 1 tests failed (0.02s)
*** Exception: ExitFailure 1

[philderbeast]

Here's the escaping needed (from a mac) to reproduce the failing test:

> stack test liquid-fixpoint:tasty --test-arguments "--quickcheck-replay=407282 --quickcheck-max-size=8 --pattern \"single-level anf vars\""

> cabal test liquid-fixpoint:test:tasty --test-options "--quickcheck-replay=407282 --quickcheck-max-size=8 --pattern \"single-level anf vars\" --color always" --test-show-details=always

[Fizzixnerd]

@philderbeast Thanks for the report, I'll look into it!

[philderbeast]

In one or more branches in existing PRs I needed to comment out this test as it was making the CI builds fails every round.